UPPAAL : 시계가 멈추는 원인이 무엇입니까

Question

현재 UPPAAL 시뮬레이터를 실행 중입니다. 내 시뮬레이터는 특정 지점 이후에 코드 실행을 중단합니다. 이 시점은 내가 제공 한 선언에 따라 다릅니다. 그러나 나는 언제 시계가 멈추는 지 일반적으로 알고 싶다. 이 문제를 유발하는 것이 있습니까?

Answer 1

귀하의 질문을 정확하게 해석 할 수 있을지 모르겠습니다. 귀하의 모델을 읽을 수 있다면 정확한 조언을 드릴 수 있습니다.

문제가 무엇인지 짐작할 때, Uppaal 시뮬레이터가의 시계 변수를 늘리지 않고도 무한히 많은 이산 단계 (전환) 을 사용하는 경우가 있다고 말할 수 있습니다.

시뮬레이션의 나머지 부분이 진행되는 동안 느낌은 "시계가 멈췄다"는 것입니다. 이 경우, 시간은 실제로 멈추지 않습니다. Uppaal은 가능한 모든 경로 중에서 시계가 진화하지 않는 곳을 탐색하는 것입니다. 시뮬레이터 (또는 모델 체커)가 클록 변수를 증가시키지 않고 무한히 많은 변환을 수행 할 수 있다면 "Zeno 경로"의 예입니다.

제논 경로를 사용할 가능성을 피하기 위해 모델을 작성하는 사람은 책임을집니다.

모델에 Zeno 경로가없는 지 확실하지 않은 경우 알려진 자동화 된 방법을 사용하여 Timed Automaton에 Uenpaul이없는 Zeno 경로가 없음을 확인할 수 있습니다.

또 다른 가능성은 데드락이라는 시뮬레이터의 실행이 중지된다는 것입니다. 이 경우 문제는 시계 작동이 멈춘 것이 아니라 가능한 모든 전환이 비활성화 된 상황에 도달했기 때문입니다 (가능한 모든 가드가 활성화되지 않았거나 사용 가능한 전환의 가능한 모든 대상 상태가 어느 정도 시간이 있기 때문에 거짓 인 불변량)