Пытаясь понять часы и тайм-ауты в 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

Извините, я уже давно нашел решение в 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).

Надеюсь, это кому-то поможет!