UPPAAL에서 시계와 타임 아웃을 이해하려고 시도합니다.

Question

UPPAAL을 사용하여 시스템을 시간 초과 자동 완성으로 모델링해야합니다. UPPAAL이 경과 시간에 따라 시계와 가드를 관리하는 방법에 당황합니다. UPPAAL은 시계 가드를 무시하는 것처럼 보입니다. ! 내 문제는 내가 "물리적 인"접근법에서 모델링에 접근하고 있다는 것이므로이 문제에 직면하고 있습니다.

여기에 사소한 오토 마톤이 있습니다. UPPAAL 시뮬레이션을 실행하면 초기 위치와 A 위치 사이에서 영원히 반복되고 B 지점으로 이동하지 않을 것으로 예상됩니다. 그러나이 경우는 아닙니다. A와 B 사이에서 무작위로 번갈아 나타납니다 (적어도 UPPAAL 스냅 샷을 사용하여 적어도 시도 할 수는 없습니다. 리눅스 64 버전은 없다.

그래서 내가 무엇을 놓치고 있습니까? 정말로 UPPAL이 시계 가드를 다루는가?

처음으로이 문제가 발생했을 때 시도한 작업은 시간 초과를 모델링하는 것이므로 명목상의 동작이 30 초 전에 충족되지 않으면 오토 마톤은 다른 가장자리를 차지합니다.

내가 uppaal Yahoo group에이 오래전에 대한 해결책을 가지고, 당신에게

<?xml version="1.0" encoding="utf-8"?> 
<!DOCTYPE nta PUBLIC '-//Uppaal Team//DTD Flat System 1.1//EN' 'http://www.it.uu.se/research/group/darts/uppaal/flat-1_2.dtd'> 
<nta> 
    <declaration>// Place global declarations here. 

clock t;</declaration> 
    <template> 
     <name x="5" y="5">Template</name> 
     <declaration>// Place local declarations here. 
</declaration> 
     <location id="id0" x="153" y="8"> 
      <name x="170" y="0">B</name> 
     </location> 
     <location id="id1" x="0" y="119"> 
      <name x="-8" y="136">A</name> 
     </location> 
     <location id="id2" x="0" y="0"> 
     </location> 
     <init ref="id2"/> 
     <transition> 
      <source ref="id0"/> 
      <target ref="id2"/> 
      <label kind="assignment" x="60" y="-55">t:=0</label> 
      <nail x="153" y="-8"/> 
      <nail x="42" y="-102"/> 
     </transition> 
     <transition> 
      <source ref="id1"/> 
      <target ref="id2"/> 
      <label kind="assignment" x="-135" y="55">t:=0</label> 
      <nail x="-153" y="-8"/> 
     </transition> 
     <transition> 
      <source ref="id2"/> 
      <target ref="id0"/> 
      <label kind="guard" x="93" y="-17">t &gt; 30</label> 
     </transition> 
     <transition> 
      <source ref="id2"/> 
      <target ref="id1"/> 
      <label kind="guard" x="0" y="25">t&lt;30</label> 
     </transition> 
    </template> 
    <system>// Place template instantiations here. 

// List one or more processes to be composed into a system. 
system Template; 
    </system> 
    <queries> 
     <query> 
      <formula>sup: t 
      </formula> 
      <comment> 
      </comment> 
     </query> 
    </queries> 
</nta> 

Answer 1

죄송 많은 감사드립니다. 여기에 답을 붙여 넣기 때문에 다른 사람들에게 유용 할 수 있습니다.

There is nothing special in your model. 
You are probably expecting "as soon as possible" semantics where the 
automaton would take the transition as soon as it becomes enabled. Timed 
automaton is not like that: if there is no invariant (as in your example), 
then the timed automaton is allowed to delay as much as possible. 
Consequently, the behavior of your automaton includes non-deterministic 
choices: either to delay (let time pass) or take the transition. Then the 
whole point of model-checker like Uppaal is to explore all possibilities 
and that's why you see both edges (with t<30 and t>30) being exercised. 
Please note that the clock values (constraints) are different when either 
transition is taken, which means that they are executed at different 
(mutually exclusive) times. 

If you want something definitely to happen within 30 time units, i.e. do 
not allow time to pass beyond this point without anything happening and 
you have some transition enabled, then you need to add an invariant t<30 
(double-click the location and enter this expression into Invariant text 
field). 

희망이 있으면 도움이됩니다.