model-checking - UPPAAL のクロックとタイムアウトを理解しようとしている

Question

UPPAAL を使用してシステムを時限オートマトンとしてモデル化する必要がありますが、UPPAAL が経過時間に応じてクロックとガードを管理する方法に本当に戸惑っています。UPPAAL はクロック ガードを無視しているように見えます! 私の問題は、非常に「物理的な」アプローチからモデリングに取り組んでいることであり、この種の問題に直面していると思います。

ここに簡単なオートマトンがあります。UPPAAL シミュレーションで実行すると、最初の場所と A の場所の間で永久にループし、B に移動することはないと予想されます。 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>