GoToUniversity

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

broadcast chan train, car;

bool arrived = false;
bool tooLate = false;

clock time;
</declaration>
    <template>
        <name x="5" y="5">Person</name>
        <declaration>// Place local declarations here.</declaration>
        <location id="id0" x="-93" y="59">
        </location>
        <location id="id1" x="-93" y="-76">
        </location>
        <location id="id2" x="0" y="-17">
            <name x="-10" y="-51">University</name>
        </location>
        <location id="id3" x="-195" y="59">
            <name x="-229" y="76">GoWithCar</name>
        </location>
        <location id="id4" x="-195" y="-76">
            <name x="-238" y="-110">GoWithTrain</name>
        </location>
        <location id="id5" x="-348" y="-17">
            <name x="-374" y="-51">Rijssen</name>
        </location>
        <branchpoint id="id6" x="-289" y="-17">
        </branchpoint>
        <init ref="id5"/>
        <transition>
            <source ref="id0"/>
            <target ref="id2"/>
            <label kind="guard" x="-59" y="25">arrived == true</label>
        </transition>
        <transition>
            <source ref="id3"/>
            <target ref="id0"/>
            <label kind="synchronisation" x="-161" y="42">car!</label>
        </transition>
        <transition>
            <source ref="id1"/>
            <target ref="id2"/>
            <label kind="guard" x="-59" y="-76">arrived == true</label>
        </transition>
        <transition>
            <source ref="id4"/>
            <target ref="id1"/>
            <label kind="synchronisation" x="-161" y="-93">train!</label>
        </transition>
        <transition>
            <source ref="id6"/>
            <target ref="id3"/>
            <label kind="probability" x="-272" y="17">1</label>
        </transition>
        <transition>
            <source ref="id6"/>
            <target ref="id4"/>
            <label kind="probability" x="-272" y="-59">4</label>
        </transition>
        <transition>
            <source ref="id5"/>
            <target ref="id6"/>
        </transition>
    </template>
    <template>
        <name>Car</name>
        <location id="id7" x="-484" y="102">
            <name x="-494" y="68">NoDelay</name>
        </location>
        <location id="id8" x="-484" y="-68">
            <name x="-494" y="-102">TrafficJam</name>
            <label kind="invariant" x="-494" y="-51">time &lt;= 85</label>
        </location>
        <location id="id9" x="-663" y="8">
            <name x="-739" y="0">GetInCar</name>
        </location>
        <branchpoint id="id10" x="-578" y="8">
        </branchpoint>
        <init ref="id9"/>
        <transition>
            <source ref="id7"/>
            <target ref="id9"/>
            <label kind="assignment" x="-646" y="102">arrived = true</label>
            <nail x="-663" y="102"/>
        </transition>
        <transition>
            <source ref="id8"/>
            <target ref="id9"/>
            <label kind="guard" x="-645" y="-102">time &gt;= 50</label>
            <label kind="assignment" x="-646" y="-136">tooLate = true,
arrived = true</label>
            <nail x="-663" y="-68"/>
        </transition>
        <transition>
            <source ref="id10"/>
            <target ref="id7"/>
            <label kind="probability" x="-561" y="42">19</label>
        </transition>
        <transition>
            <source ref="id10"/>
            <target ref="id8"/>
            <label kind="probability" x="-561" y="-34">1</label>
        </transition>
        <transition>
            <source ref="id9"/>
            <target ref="id10"/>
            <label kind="guard" x="-645" y="-26">time &gt;= 40</label>
            <label kind="synchronisation" x="-645" y="-9">car?</label>
        </transition>
    </template>
    <template>
        <name>Train</name>
        <location id="id11" x="-323" y="119">
            <name x="-333" y="85">NoDelay</name>
        </location>
        <location id="id12" x="-323" y="-8">
            <name x="-323" y="-42">TrainHasDelay</name>
            <label kind="invariant" x="-333" y="9">time &lt;= 75</label>
        </location>
        <location id="id13" x="-323" y="-127">
            <name x="-333" y="-161">TrainDoesNotDrive</name>
        </location>
        <location id="id14" x="-561" y="-8">
            <name x="-637" y="-34">GetInTrain</name>
        </location>
        <branchpoint id="id15" x="-476" y="-8">
        </branchpoint>
        <init ref="id14"/>
        <transition>
            <source ref="id11"/>
            <target ref="id14"/>
            <label kind="assignment" x="-501" y="119">arrived = true</label>
            <nail x="-561" y="119"/>
        </transition>
        <transition>
            <source ref="id12"/>
            <target ref="id14"/>
            <label kind="guard" x="-493" y="-323">time &gt;= 50</label>
            <label kind="assignment" x="-493" y="-306">tooLate = true,
arrived = true</label>
            <nail x="-127" y="-8"/>
            <nail x="-127" y="-238"/>
            <nail x="-722" y="-238"/>
            <nail x="-722" y="-8"/>
        </transition>
        <transition>
            <source ref="id13"/>
            <target ref="id14"/>
            <label kind="assignment" x="-510" y="-153">arrived = false</label>
            <nail x="-561" y="-127"/>
        </transition>
        <transition>
            <source ref="id15"/>
            <target ref="id11"/>
            <label kind="probability" x="-416" y="59">89</label>
        </transition>
        <transition>
            <source ref="id15"/>
            <target ref="id12"/>
            <label kind="probability" x="-416" y="-8">10</label>
        </transition>
        <transition>
            <source ref="id15"/>
            <target ref="id13"/>
            <label kind="probability" x="-416" y="-85">1</label>
        </transition>
        <transition>
            <source ref="id14"/>
            <target ref="id15"/>
            <label kind="guard" x="-543" y="-42">time &gt;= 45</label>
            <label kind="synchronisation" x="-543" y="-25">train?</label>
        </transition>
    </template>
    <system>system Person, Car, Train;
    </system>
    <queries>
        <query>
            <formula>simulate 100 [&lt;=500] { time }
            </formula>
            <comment>
            </comment>
        </query>
    </queries>
</nta>