<?xml version="1.0" encoding="UTF-8"?>
<nta>
<declaration>urgent chan urgent_chan;chan parallel0;int [0,1] var_parallel0;clock x;int CitizenType=1;</declaration>
<template>
<name>System</name>
<location id="Exception">
<name id="Exception"/>
</location>
<location id="Init_Interaction0_Login_interaction">
<name id="Init_Interaction0_Login_interaction"/>
</location>
<location id="End_Interaction0_Login_interaction_Init_Parallel0">
<name id="End_Interaction0_Login_interaction_Init_Parallel0"/>
</location>
<location id="Init_Interaction1_CitizenInfo_interaction">
<name id="Init_Interaction1_CitizenInfo_interaction"/>
<label kind="invariant">var_parallel0==0</label>
</location>
<location id="End_Interaction1_CitizenInfo_interaction">
<name id="End_Interaction1_CitizenInfo_interaction"/>
<label kind="invariant">var_parallel0==0</label>
</location>
<location id="End_Parallel0_Init_Interaction3_RegisterVoter_interaction">
<name id="End_Parallel0_Init_Interaction3_RegisterVoter_interaction"/>
<label kind="invariant">x &lt;= 6</label>
</location>
<location id="End_Interaction3_RegisterVoter_interaction_Init_Interaction4_RegisterList_interaction">
<name id="End_Interaction3_RegisterVoter_interaction_Init_Interaction4_RegisterList_interaction"/>
</location>
<location id="End_Interaction4_RegisterList_interaction_Init_Choice0">
<name id="End_Interaction4_RegisterList_interaction_Init_Choice0"/>
</location>
<Choice_inv>
<inv>Inf</inv>
<inv>Inf</inv>
</Choice_inv>
<location id="Init_Interaction5_RegisterLocal_interaction">
<name id="Init_Interaction5_RegisterLocal_interaction"/>
</location>
<location id="End_Interaction5_RegisterLocal_interaction">
<name id="End_Interaction5_RegisterLocal_interaction"/>
</location>
<location id="End_Workunit0">
<name id="End_Workunit0"/>
</location>
<location id="Init_Interaction6_RegisterFederal_interaction">
<name id="Init_Interaction6_RegisterFederal_interaction"/>
</location>
<location id="End_Interaction6_RegisterFederal_interaction">
<name id="End_Interaction6_RegisterFederal_interaction"/>
</location>
<location id="End_Workunit1">
<name id="End_Workunit1"/>
</location>
<location id="End_Choice0">
<name id="End_Choice0"/>
</location>
<transition>
<source ref="Init_Interaction0_Login_interaction"/>
<target ref="End_Interaction0_Login_interaction"/>
</transition>
<transition>
<label kind="synchronisation">parallel0!</label>
<label kind="assignment">var_parallel0=0</label>
<source ref="Init_Parallel0"/>
<target ref="Init_Interaction1_CitizenInfo_interaction"/>
</transition>
<transition>
<source ref="Init_Interaction1_CitizenInfo_interaction"/>
<target ref="End_Interaction1_CitizenInfo_interaction"/>
</transition>
<transition>
<label kind="synchronisation">parallel0!</label>
<source ref="End_Interaction1_CitizenInfo_interaction"/>
<target ref="End_Parallel0"/>
</transition>
<transition>
<label kind="guard">x == 6</label>
<source ref="Init_Interaction3_RegisterVoter_interaction"/>
<target ref="Exception"/>
</transition>
<transition>
<label kind="guard">x &lt;= 5</label>
<source ref="Init_Interaction3_RegisterVoter_interaction"/>
<target ref="End_Interaction3_RegisterVoter_interaction"/>
</transition>
<transition>
<source ref="Init_Interaction4_RegisterList_interaction"/>
<target ref="End_Interaction4_RegisterList_interaction"/>
</transition>
<transition>
<label kind="guard">CitizenType==1</label>
<source ref="Init_Choice0"/>
<target ref="Init_Interaction5_RegisterLocal_interaction"/>
</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>
<label kind="synchronisation">urgent_chan!</label>
<source ref="End_Workunit0"/>
<target ref="End_Choice0"/>
</transition>
<transition>
<label kind="guard">CitizenType!=1</label>
<source ref="Init_Choice0"/>
<target ref="Init_Interaction6_RegisterFederal_interaction"/>
</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>
<label kind="synchronisation">urgent_chan!</label>
<source ref="End_Workunit1"/>
<target ref="End_Choice0"/>
</transition>
</template>
<template>
<name>Par_System0</name>
<location id="Exception">
<name id="Exception"/>
</location>
<location id="Init_Parallel0">
<name id="Init_Parallel0"/>
</location>
<location id="Init_Interaction2_ProceduresInfo_interaction">
<name id="Init_Interaction2_ProceduresInfo_interaction"/>
<label kind="invariant">var_parallel0==0</label>
</location>
<location id="End_Interaction2_ProceduresInfo_interaction">
<name id="End_Interaction2_ProceduresInfo_interaction"/>
<label kind="invariant">var_parallel0==0</label>
</location>
<transition>
<label kind="synchronisation">parallel0?</label>
<source ref="Init_Parallel0"/>
<target ref="Init_Interaction2_ProceduresInfo_interaction"/>
</transition>
<transition>
<source ref="Init_Interaction2_ProceduresInfo_interaction"/>
<target ref="End_Interaction2_ProceduresInfo_interaction"/>
</transition>
<transition>
<label kind="synchronisation">parallel0?</label>
<source ref="End_Interaction2_ProceduresInfo_interaction"/>
<target ref="Init_Parallel0"/>
</transition>
</template>
<template>
<name>Urgent_System</name>
<location id="Urgent">
<name id="Urgent"/>
</location>
<transition>
<label kind="synchronisation">urgent_chan?</label>
<source ref="Urgent"/>
<target ref="Urgent"/>
</transition>
</template>
<instantiation/>
<system>System;</system>
</nta>
