<?xml version="1.0" encoding="UTF-8"?>
<nta>
<declaration>urgent chan <urgent>urgent_chan, </urgent>chan <canales>parallel0, </canales>int [0,1] <boolean>var_parallel0, </boolean>int <int>CitizenType=1, </int>clock <reloj>x, </reloj>
</declaration>
<template>
<name>System</name>
<location id="Exception">
<name id="Exception"/>
</location>
<SEQUENCE>
<location id="Init_Interaction0_Login_interaction" type="interaction">
<name id="Init_Interaction0_Login_interaction"/>
</location>
<location id="End_Interaction0_Login_interaction" type="interaction">
<name id="End_Interaction0_Login_interaction"/>
</location> <location id="Init_Parallel0" type="Parallel">
<name id="Init_Parallel0"/>
</location>
<PARALLEL id="0">
<SEQUENCE>
<location id="Init_Interaction1_CitizenInfo_interaction" type="interaction">
<name id="Init_Interaction1_CitizenInfo_interaction"/>
</location>
<location id="End_Interaction1_CitizenInfo_interaction" type="interaction">
<name id="End_Interaction1_CitizenInfo_interaction"/>
</location> </SEQUENCE> </PARALLEL>
<location id="End_Parallel0" type="Parallel">
<name id="End_Parallel0"/>
</location> <location id="Init_Interaction3_RegisterVoter_interaction" type="interaction">
<label kind="invariant">x &lt;= 6</label>
<name id="Init_Interaction3_RegisterVoter_interaction"/>
</location>
<location id="End_Interaction3_RegisterVoter_interaction" type="interaction">
<name id="End_Interaction3_RegisterVoter_interaction"/>
</location> <location id="Init_Interaction4_RegisterList_interaction" type="interaction">
<name id="Init_Interaction4_RegisterList_interaction"/>
</location>
<location id="End_Interaction4_RegisterList_interaction" type="interaction">
<name id="End_Interaction4_RegisterList_interaction"/>
</location> <location id="Init_Choice0" type="Choice">
<name id="Init_Choice0"/>
</location>
<CHOICE>
<CHOICECHILDIN id="0" hijo="1"/>
<location id="Init_Workunit0" type="workunit">
<name id="Init_Workunit0"/>
</location>
<WORKUNIT>
<SEQUENCE>
<location id="Init_Interaction5_RegisterLocal_interaction" type="interaction">
<name id="Init_Interaction5_RegisterLocal_interaction"/>
</location>
<location id="End_Interaction5_RegisterLocal_interaction" type="interaction">
<name id="End_Interaction5_RegisterLocal_interaction"/>
</location> </SEQUENCE> </WORKUNIT>
<location id="End_Workunit0" type="workunit">
<name id="End_Workunit0"/>
</location> <CHOICECHILDOUT id="0" hijo="1"/>
<CHOICECHILDIN id="0" hijo="2"/>
<location id="Init_Workunit1" type="workunit">
<name id="Init_Workunit1"/>
</location>
<WORKUNIT>
<SEQUENCE>
<location id="Init_Interaction6_RegisterFederal_interaction" type="interaction">
<name id="Init_Interaction6_RegisterFederal_interaction"/>
</location>
<location id="End_Interaction6_RegisterFederal_interaction" type="interaction">
<name id="End_Interaction6_RegisterFederal_interaction"/>
</location> </SEQUENCE> </WORKUNIT>
<location id="End_Workunit1" type="workunit">
<name id="End_Workunit1"/>
</location> <CHOICECHILDOUT id="0" hijo="2"/>
</CHOICE>
<location id="End_Choice0" type="Choice">
<name id="End_Choice0"/>
</location> </SEQUENCE>
<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=""/>
</transition>
<transition>
<source ref="Init_Interaction1_CitizenInfo_interaction"/>
<target ref="End_Interaction1_CitizenInfo_interaction"/>
</transition>
<transition>
<label kind="synchronisation">parallel0!</label>
<source ref=""/>
<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>
<source ref="Init_Choice0"/>
<target ref=""/>
</transition>
<CHOICECHILDIN id="0" hijo="1"/>
<transition>
<label kind="guard">CitizenType==1</label>
<source ref="Init_Workunit0"/>
<target ref=""/>
</transition>
<WORKUNITIN id="0" repeat="" restriccion="CitizenType==1"/>
<transition>
<source ref="Init_Interaction5_RegisterLocal_interaction"/>
<target ref="End_Interaction5_RegisterLocal_interaction"/>
</transition>
<WORKUNITOUT id="0" repeat="" restriccion="CitizenType==1"/>
<transition>
<source ref=""/>
<target ref="End_Workunit0"/>
</transition>
<CHOICECHILDOUT id="0" hijo="1"/>
<transition>
<label kind="synchronisation">urgent_chan!</label>
<source ref=""/>
<target ref="End_Choice0"/>
</transition>
<transition>
<source ref="Init_Choice0"/>
<target ref=""/>
</transition>
<CHOICECHILDIN id="0" hijo="2"/>
<transition>
<label kind="guard">CitizenType!=1</label>
<source ref="Init_Workunit1"/>
<target ref=""/>
</transition>
<WORKUNITIN id="1" repeat="" restriccion="CitizenType!=1"/>
<transition>
<source ref="Init_Interaction6_RegisterFederal_interaction"/>
<target ref="End_Interaction6_RegisterFederal_interaction"/>
</transition>
<WORKUNITOUT id="1" repeat="" restriccion="CitizenType!=1"/>
<transition>
<source ref=""/>
<target ref="End_Workunit1"/>
</transition>
<CHOICECHILDOUT id="0" hijo="2"/>
<transition>
<label kind="synchronisation">urgent_chan!</label>
<source ref=""/>
<target ref="End_Choice0"/>
</transition>
</template>
<template>
<name>Par_System0</name>
<location id="Exception">
<name id="Exception"/>
</location>
<location id="Init_Parallel0" type="Parallel">
<name id="Init_Parallel0"/>
</location>
<PARALLEL id="0">
<SEQUENCE>
<location id="Init_Interaction2_ProceduresInfo_interaction" type="interaction">
<name id="Init_Interaction2_ProceduresInfo_interaction"/>
</location>
<location id="End_Interaction2_ProceduresInfo_interaction" type="interaction">
<name id="End_Interaction2_ProceduresInfo_interaction"/>
</location> </SEQUENCE> </PARALLEL>
<transition>
<label kind="synchronisation">parallel0?</label>
<source ref="Init_Parallel0"/>
<target ref=""/>
</transition>
<transition>
<source ref="Init_Interaction2_ProceduresInfo_interaction"/>
<target ref="End_Interaction2_ProceduresInfo_interaction"/>
</transition>
<transition>
<label kind="synchronisation">parallel0?</label>
<source ref=""/>
<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>
