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

Question

我需要使用 UPPAAL 将系统建模为定时自动机，我对 UPPAAL 根据经过的时间管理时钟和守卫的方式感到非常困惑：看起来 UPPAAL 只是忽略了时钟守卫！我想我的问题是我正在从一种非常 "physical" 的方法进行建模，所以我面临着这类问题。

所以这是一个简单的自动机。当运行进行 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 Yahoo group 上找到了解决方案。我把答案贴在这里，这样对其他人有用：

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

希望这对某人有所帮助！

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

Trying to understand clocks and timeouts in UPPAAL

model-checking