<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE nta PUBLIC "-//Uppaal Team//DTD Flat System 1.0//EN" "http://www.docs.uu.se/docs/rtmv/uppaal/xml/flat-1_0.dtd">
<nta>
<declaration>urgent chan urgent_chan;chan parallel0;int [0,1] var_parallel0;clock x;int CitizenType=1;</declaration>
<template>
<name>System</name>
<declaration/>
<location id="Exception">
<name>Exception</name>
</location>
<location id="Init_Interaction0_Login_interaction">
<name>Init_Interaction0_Login_interaction</name>
</location>
<location id="Init_Parallel0">
<name>Init_Parallel0</name>
</location>
<location id="Init_Interaction1_CitizenInfo_interaction">
<name>Init_Interaction1_CitizenInfo_interaction</name>
</location>
<location id="End_Interaction1_CitizenInfo_interaction">
<name>End_Interaction1_CitizenInfo_interaction</name>
</location>
<location id="Init_Interaction3_RegisterVoter_interaction">
<name>Init_Interaction3_RegisterVoter_interaction</name>
<label kind="invariant">(x &lt;= 6)</label>
</location>
<location id="Init_Interaction4_RegisterList_interaction">
<name>Init_Interaction4_RegisterList_interaction</name>
</location>
<location id="Init_Choice0">
<name>Init_Choice0</name>
</location>
<location id="Init_Interaction5_RegisterLocal_interaction">
<name>Init_Interaction5_RegisterLocal_interaction</name>
</location>
<location id="End_Interaction5_RegisterLocal_interaction">
<name>End_Interaction5_RegisterLocal_interaction</name>
</location>
<location id="End_Workunit0">
<name>End_Workunit0</name>
</location>
<location id="Init_Interaction6_RegisterFederal_interaction">
<name>Init_Interaction6_RegisterFederal_interaction</name>
</location>
<location id="End_Interaction6_RegisterFederal_interaction">
<name>End_Interaction6_RegisterFederal_interaction</name>
</location>
<location id="End_Workunit1">
<name>End_Workunit1</name>
</location>
<location id="End_Choice0">
<name>End_Choice0</name>
</location>
<init ref="Init_Interaction0_Login_interaction"/>
<transition>
<source ref="Init_Interaction1_CitizenInfo_interaction"/>
<target ref="Exception"/>
<label kind="guard">var_parallel0==1</label>
<label kind="synchronisation">urgent_chan!</label>
</transition>
<transition>
<source ref="End_Interaction1_CitizenInfo_interaction"/>
<target ref="Exception"/>
<label kind="guard">var_parallel0==1</label>
<label kind="synchronisation">urgent_chan!</label>
</transition>
<transition>
<source ref="Init_Interaction0_Login_interaction"/>
<target ref="Init_Parallel0"/>
</transition>
<transition>
<source ref="Init_Parallel0"/>
<target ref="Init_Interaction1_CitizenInfo_interaction"/>
<label kind="synchronisation">parallel0!</label>
<label kind="assignment">var_parallel0=0</label>
</transition>
<transition>
<source ref="Init_Interaction1_CitizenInfo_interaction"/>
<target ref="End_Interaction1_CitizenInfo_interaction"/>
<label kind="guard">(var_parallel0==0)</label>
</transition>
<transition>
<source ref="End_Interaction1_CitizenInfo_interaction"/>
<target ref="Init_Interaction3_RegisterVoter_interaction"/>
<label kind="synchronisation">parallel0!</label>
<label kind="assignment">x=0</label>
<label kind="guard">(var_parallel0==0)</label>
</transition>
<transition>
<source ref="Init_Interaction3_RegisterVoter_interaction"/>
<target ref="Exception"/>
<label kind="guard">(x == 6)</label>
</transition>
<transition>
<source ref="Init_Interaction3_RegisterVoter_interaction"/>
<target ref="Init_Interaction4_RegisterList_interaction"/>
<label kind="guard">(x &lt;= 5)</label>
</transition>
<transition>
<source ref="Init_Interaction4_RegisterList_interaction"/>
<target ref="Init_Choice0"/>
</transition>
<transition>
<source ref="Init_Choice0"/>
<target ref="Init_Interaction5_RegisterLocal_interaction"/>
<label kind="guard">(CitizenType==1)</label>
</transition>
<transition>
<source ref="Init_Interaction5_RegisterLocal_interaction"/>
<target ref="End_Interaction5_RegisterLocal_interaction"/>
</transition>
<transition>
<source ref="End_Interaction5_RegisterLocal_interaction"/>
<target ref="End_Workunit0"/>
</transition>
<transition>
<source ref="End_Workunit0"/>
<target ref="End_Choice0"/>
<label kind="synchronisation">urgent_chan!</label>
</transition>
<transition>
<source ref="Init_Choice0"/>
<target ref="Init_Interaction6_RegisterFederal_interaction"/>
<label kind="guard">(CitizenType!=1)</label>
</transition>
<transition>
<source ref="Init_Interaction6_RegisterFederal_interaction"/>
<target ref="End_Interaction6_RegisterFederal_interaction"/>
</transition>
<transition>
<source ref="End_Interaction6_RegisterFederal_interaction"/>
<target ref="End_Workunit1"/>
</transition>
<transition>
<source ref="End_Workunit1"/>
<target ref="End_Choice0"/>
<label kind="synchronisation">urgent_chan!</label>
</transition>
</template>
<template>
<name>Par_System0</name>
<declaration/>
<location id="Exception">
<name>Exception</name>
</location>
<location id="Init_Parallel0">
<name>Init_Parallel0</name>
</location>
<location id="Init_Interaction2_ProceduresInfo_interaction">
<name>Init_Interaction2_ProceduresInfo_interaction</name>
</location>
<location id="End_Interaction2_ProceduresInfo_interaction">
<name>End_Interaction2_ProceduresInfo_interaction</name>
</location>
<init ref="Init_Parallel0"/>
<transition>
<source ref="Init_Interaction2_ProceduresInfo_interaction"/>
<target ref="Exception"/>
<label kind="guard">var_parallel0==1</label>
<label kind="synchronisation">urgent_chan!</label>
</transition>
<transition>
<source ref="End_Interaction2_ProceduresInfo_interaction"/>
<target ref="Exception"/>
<label kind="guard">var_parallel0==1</label>
<label kind="synchronisation">urgent_chan!</label>
</transition>
<transition>
<source ref="Init_Parallel0"/>
<target ref="Init_Interaction2_ProceduresInfo_interaction"/>
<label kind="synchronisation">parallel0?</label>
</transition>
<transition>
<source ref="Init_Interaction2_ProceduresInfo_interaction"/>
<target ref="End_Interaction2_ProceduresInfo_interaction"/>
<label kind="guard">(var_parallel0==0)</label>
</transition>
<transition>
<source ref="End_Interaction2_ProceduresInfo_interaction"/>
<target ref="Init_Parallel0"/>
<label kind="synchronisation">parallel0?</label>
<label kind="guard">(var_parallel0==0)</label>
</transition>
</template>
<template>
<name>Urgent_System</name>
<declaration/>
<location id="Urgent">
<name>Urgent</name>
</location>
<init ref="Urgent"/>
<transition>
<source ref="Urgent"/>
<target ref="Urgent"/>
<label kind="synchronisation">urgent_chan?</label>
</transition>
</template>
<instantiation/>
<system>system Par_System0, Urgent_System, System;</system>
</nta>
