0

我需要使用 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>
4

1 回答 1

0

抱歉，我很久以前就在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).

希望这对某人有帮助！

于 2015-03-18T08:48:40.993 回答