试图理解UPPAAL中的时钟和超时

Question

我需要用UPPAAL将一个系统建模为一个计时自动机，我对UPPAAL根据经过的时间来管理时钟和警卫的方式感到非常困惑:看起来UPPAAL只是忽略时钟保护！我想我的问题是，我是从一种非常“物理”的方法来接近建模的，所以我面临着这样的问题。

所以这里有一个微不足道的自动机。在UPPAAL模拟上运行时，我希望它在初始位置和A位置之间永远循环，永远不会转到B。但情况并非如此:它在A和B之间随机交替(至少使用最新的UPPAAL快照；我不能尝试发行版本，因为没有Linux 64版本)。

那我错过了什么？UPPAAL如何对待时钟警卫？

当我第一次遇到这个问题时，我想要做的是建立一个超时模型，所以如果30秒前不满足标准行为的保护，那么自动机就会有不同的优势。

非常感谢

<?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

对不起，很久以前我在uppaal雅虎集团上找到了一个解决方案。我把答案粘贴在这里，这样对其他人是有用的：

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).

希望这对某人有帮助！