698 lines
44 KiB
Text
698 lines
44 KiB
Text
|
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
|
||
|
|
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="dekker_wn.1" version="121">
|
||
|
|
<gspn name="CPN" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false">
|
||
|
|
<nodes>
|
||
|
|
<color-class definition="{t1, t2}" name="Turn" x="2.125" y="38.0"/>
|
||
|
|
<color-class definition="{P,Q}" name="Process" x="2.125" y="40.0"/>
|
||
|
|
<color-var domain="Process" name="p" x="11.9375" y="40.0"/>
|
||
|
|
<color-var domain="Turn" name="t" x="11.9375" y="38.0"/>
|
||
|
|
<place domain="Turn" marking="<t1>" name="TURN" x="3.0" y="2.0"/>
|
||
|
|
<place name="wantP_is_TRUE" x="4.0" y="8.0"/>
|
||
|
|
<place name="wantQ_is_TRUE" x="4.0" y="18.0"/>
|
||
|
|
<place marking="1" name="wantQ_is_FALSE" x="4.0" y="23.0"/>
|
||
|
|
<place marking="1" name="wantP_is_FALSE" x="4.0" y="13.0"/>
|
||
|
|
<place domain="Process" marking="<P> + <Q>" name="local" x="30.0" y="7.0"/>
|
||
|
|
<place domain="Process" name="set" x="44.0" y="7.0"/>
|
||
|
|
<transition guard="False" name="T0" nservers-x="0.5" type="EXP" x="30.55" y="2.0"/>
|
||
|
|
<transition name="T1" nservers-x="0.5" type="EXP" x="37.55" y="7.0"/>
|
||
|
|
<transition guard="p == P" name="T2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="50.55" y="3.0"/>
|
||
|
|
<transition guard="p == Q" name="T3" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="50.55" y="11.0"/>
|
||
|
|
<place domain="Process" name="while" x="30.0" y="21.0"/>
|
||
|
|
<place domain="Process" name="setFalse" x="30.0" y="35.0"/>
|
||
|
|
<place domain="Process" name="await" x="49.0" y="35.0"/>
|
||
|
|
<place domain="Process" name="maybe_while" x="82.0" y="20.0"/>
|
||
|
|
<transition guard="p == P" guard-x="2.5" label-y="0.5" name="T4" nservers-x="0.5" type="EXP" x="56.55" y="17.0"/>
|
||
|
|
<transition guard="p == Q" name="T5" nservers-x="0.5" type="EXP" x="56.55" y="24.0"/>
|
||
|
|
<transition guard="(p == P && t == t2) || (p == Q && t == t1)" guard-y="2.0" name="T6" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="30.55" y="28.0"/>
|
||
|
|
<transition guard="p == P" guard-y="2.0" label-x="-0.5" label-y="0.0" name="T7" nservers-x="0.5" type="EXP" x="40.55" y="32.0"/>
|
||
|
|
<transition guard="p == Q" guard-y="-2.5" name="T8" nservers-x="0.5" type="EXP" x="40.55" y="39.0"/>
|
||
|
|
<transition guard="(p == P && t == t1) || (p == Q && t == t2)" guard-x="0.5" guard-y="-4.0" name="T9" nservers-x="0.5" type="EXP" x="56.55" y="35.0"/>
|
||
|
|
<transition guard="(p == P && t == t1) || (p == Q && t == t2)" guard-y="2.0" name="T10" nservers-x="0.5" rotation="3.141592653589793" type="EXP" x="19.55" y="21.0"/>
|
||
|
|
<place domain="Process" name="P0" x="62.0" y="35.0"/>
|
||
|
|
<transition guard="p == P" guard-y="-2.5" name="T11" nservers-x="0.5" type="EXP" x="72.55" y="39.0"/>
|
||
|
|
<transition guard="p == Q" name="T12" nservers-x="0.5" type="EXP" x="72.55" y="31.0"/>
|
||
|
|
<place domain="Process" name="P1" x="82.0" y="35.0"/>
|
||
|
|
<transition name="T13" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="82.55" y="28.0"/>
|
||
|
|
<transition guard="p == P" guard-x="2.0" name="T14" nservers-x="0.5" type="EXP" x="103.55" y="17.0"/>
|
||
|
|
<transition guard="p == Q" guard-x="2.0" guard-y="-2.5" name="T15" nservers-x="0.5" type="EXP" x="103.55" y="24.0"/>
|
||
|
|
<place domain="Process" name="critical" x="103.0" y="46.0"/>
|
||
|
|
<transition guard="p == P" guard-y="2.0" name="T16" nservers-x="0.5" type="EXP" x="90.55" y="44.0"/>
|
||
|
|
<transition guard="p == Q" guard-y="-2.5" name="T17" nservers-x="0.5" type="EXP" x="90.55" y="50.0"/>
|
||
|
|
<place domain="Process" name="setFalse_P" x="54.0" y="44.0"/>
|
||
|
|
<place domain="Process" name="setFalse_Q" x="54.0" y="50.0"/>
|
||
|
|
<transition name="RESET_1" nservers-x="0.5" type="EXP" x="31.55" y="44.0"/>
|
||
|
|
<transition name="RESET_2" nservers-x="0.5" type="EXP" x="31.55" y="50.0"/>
|
||
|
|
</nodes>
|
||
|
|
<edges>
|
||
|
|
<arc head="local" kind="OUTPUT" mult="<p>" tail="T0">
|
||
|
|
<point x="28.0" y="5.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T0" kind="INPUT" mult="<p>" tail="local">
|
||
|
|
<point x="34.0" y="6.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T1" kind="INPUT" mult="<p>" mult-k="0.8489257812500001" tail="local">
|
||
|
|
<point x="34.3755859375" y="8.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="set" kind="OUTPUT" mult="<p>" tail="T1"/>
|
||
|
|
<arc head="T2" kind="INPUT" mult="<p>" tail="set"/>
|
||
|
|
<arc broken="true" head="wantP_is_TRUE" kind="OUTPUT" mult-k="1.21181640625" tail="T2">
|
||
|
|
<point x="57.0" y="4.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T2" kind="INPUT" tail="wantP_is_FALSE">
|
||
|
|
<point x="20.0" y="7.0"/>
|
||
|
|
<point x="19.5" y="7.0"/>
|
||
|
|
<point x="25.0" y="3.0"/>
|
||
|
|
<point x="25.5" y="3.0"/>
|
||
|
|
<point x="38.0" y="1.0"/>
|
||
|
|
<point x="44.5" y="4.0"/>
|
||
|
|
<point x="44.5" y="5.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T3" kind="INPUT" mult="<p>" tail="set"/>
|
||
|
|
<arc broken="true" head="T3" kind="INPUT" tail="wantQ_is_FALSE">
|
||
|
|
<point x="20.5" y="11.0"/>
|
||
|
|
<point x="39.5" y="14.0"/>
|
||
|
|
<point x="39.5" y="13.5"/>
|
||
|
|
<point x="44.0" y="12.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantQ_is_TRUE" kind="OUTPUT" tail="T3">
|
||
|
|
<point x="59.0" y="12.0"/>
|
||
|
|
<point x="60.5" y="23.5"/>
|
||
|
|
<point x="39.5" y="26.5"/>
|
||
|
|
<point x="21.5" y="23.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="maybe_while" kind="OUTPUT" mult="<p>" tail="T2">
|
||
|
|
<point x="63.0" y="7.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="maybe_while" kind="OUTPUT" mult="<p>" tail="T3">
|
||
|
|
<point x="59.0" y="13.5"/>
|
||
|
|
<point x="63.0" y="13.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T4" kind="INPUT" mult="<p>" tail="maybe_while"/>
|
||
|
|
<arc head="while" kind="OUTPUT" mult="<p>" tail="T4"/>
|
||
|
|
<arc broken="true" head="T4" kind="INPUT" tail="wantQ_is_TRUE">
|
||
|
|
<point x="28.5" y="15.0"/>
|
||
|
|
<point x="36.5" y="14.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantQ_is_TRUE" kind="OUTPUT" tail="T4">
|
||
|
|
<point x="82.0" y="9.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="while" kind="OUTPUT" mult="<p>" mult-x="5.0" tail="T5"/>
|
||
|
|
<arc head="T5" kind="INPUT" mult="<p>" tail="maybe_while"/>
|
||
|
|
<arc broken="true" head="T5" kind="INPUT" tail="wantP_is_TRUE">
|
||
|
|
<point x="32.5" y="23.5"/>
|
||
|
|
<point x="61.0" y="26.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantP_is_TRUE" kind="OUTPUT" tail="T5">
|
||
|
|
<point x="53.5" y="27.5"/>
|
||
|
|
<point x="25.0" y="23.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T6" kind="INPUT" mult="<t>" mult-x="1.9970321502229496" mult-y="0.14264515358735252" tail="TURN">
|
||
|
|
<point x="24.5" y="12.0"/>
|
||
|
|
<point x="22.5" y="25.0"/>
|
||
|
|
<point x="24.0" y="26.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN" kind="OUTPUT" mult="<t>" tail="T6">
|
||
|
|
<point x="36.5" y="26.0"/>
|
||
|
|
<point x="33.5" y="38.0"/>
|
||
|
|
<point x="19.0" y="38.5"/>
|
||
|
|
<point x="19.0" y="38.0"/>
|
||
|
|
<point x="19.0" y="21.0"/>
|
||
|
|
<point x="19.0" y="20.5"/>
|
||
|
|
<point x="19.0" y="7.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T6" kind="INPUT" mult="<p>" tail="while"/>
|
||
|
|
<arc head="setFalse" kind="OUTPUT" mult="<p>" mult-x="-2.5" mult-y="2.0" tail="T6"/>
|
||
|
|
<arc head="T7" kind="INPUT" mult="<p>" tail="setFalse"/>
|
||
|
|
<arc head="await" kind="OUTPUT" mult="<p>" tail="T7"/>
|
||
|
|
<arc head="T8" kind="INPUT" mult="<p>" tail="setFalse"/>
|
||
|
|
<arc head="await" kind="OUTPUT" mult="<p>" tail="T8"/>
|
||
|
|
<arc broken="true" head="T7" kind="INPUT" tail="wantP_is_TRUE">
|
||
|
|
<point x="22.5" y="23.5"/>
|
||
|
|
<point x="39.5" y="24.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantP_is_FALSE" kind="OUTPUT" tail="T7">
|
||
|
|
<point x="48.0" y="33.5"/>
|
||
|
|
<point x="59.0" y="35.0"/>
|
||
|
|
<point x="66.0" y="46.0"/>
|
||
|
|
<point x="64.5" y="48.5"/>
|
||
|
|
<point x="48.0" y="54.5"/>
|
||
|
|
<point x="44.0" y="55.0"/>
|
||
|
|
<point x="30.0" y="49.5"/>
|
||
|
|
<point x="25.5" y="36.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T8" kind="INPUT" tail="wantQ_is_TRUE">
|
||
|
|
<point x="26.5" y="43.0"/>
|
||
|
|
<point x="34.5" y="42.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantQ_is_FALSE" kind="OUTPUT" tail="T8">
|
||
|
|
<point x="55.5" y="45.0"/>
|
||
|
|
<point x="43.5" y="52.0"/>
|
||
|
|
<point x="42.5" y="52.0"/>
|
||
|
|
<point x="26.5" y="49.5"/>
|
||
|
|
<point x="25.0" y="49.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T9" kind="INPUT" mult="<p>" tail="await"/>
|
||
|
|
<arc broken="true" head="T9" kind="INPUT" mult="<t>" tail="TURN">
|
||
|
|
<point x="23.0" y="43.5"/>
|
||
|
|
<point x="51.0" y="43.5"/>
|
||
|
|
<point x="54.5" y="35.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN" kind="OUTPUT" mult="<t>" tail="T9">
|
||
|
|
<point x="64.5" y="32.5"/>
|
||
|
|
<point x="68.5" y="31.5"/>
|
||
|
|
<point x="70.5" y="11.0"/>
|
||
|
|
<point x="47.5" y="11.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T10" kind="INPUT" mult="<p>" tail="while"/>
|
||
|
|
<arc broken="true" head="maybe_while" kind="OUTPUT" mult="<p>" mult-k="0.50009765625" tail="T10">
|
||
|
|
<point x="15.0" y="22.0"/>
|
||
|
|
<point x="15.44711650594682" y="18.923067952425427"/>
|
||
|
|
<point x="16.5" y="10.5"/>
|
||
|
|
<point x="71.5" y="15.0"/>
|
||
|
|
<point x="74.0" y="22.0"/>
|
||
|
|
<point x="68.0" y="22.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T10" kind="INPUT" mult="<t>" tail="TURN">
|
||
|
|
<point x="16.0" y="16.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN" kind="OUTPUT" mult="<t>" tail="T10">
|
||
|
|
<point x="23.0" y="19.0"/>
|
||
|
|
<point x="19.5" y="11.0"/>
|
||
|
|
<point x="12.0" y="9.5"/>
|
||
|
|
<point x="11.0" y="9.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P0" kind="OUTPUT" mult="<p>" mult-k="0.74990234375" tail="T9">
|
||
|
|
<point x="66.0" y="36.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T11" kind="INPUT" mult="<p>" tail="P0"/>
|
||
|
|
<arc head="T12" kind="INPUT" mult="<p>" tail="P0"/>
|
||
|
|
<arc head="P1" kind="OUTPUT" mult="<p>" tail="T11"/>
|
||
|
|
<arc head="P1" kind="OUTPUT" mult="<p>" tail="T12"/>
|
||
|
|
<arc broken="true" head="T11" kind="INPUT" tail="wantP_is_FALSE">
|
||
|
|
<point x="34.0" y="46.5"/>
|
||
|
|
<point x="61.0" y="43.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantP_is_TRUE" kind="OUTPUT" tail="T11">
|
||
|
|
<point x="84.5" y="44.5"/>
|
||
|
|
<point x="81.0" y="34.5"/>
|
||
|
|
<point x="59.5" y="30.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T12" kind="INPUT" tail="wantQ_is_FALSE">
|
||
|
|
<point x="64.5" y="31.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantQ_is_TRUE" kind="OUTPUT" tail="T12">
|
||
|
|
<point x="115.5" y="18.0"/>
|
||
|
|
<point x="104.5" y="22.0"/>
|
||
|
|
<point x="103.0" y="21.5"/>
|
||
|
|
<point x="77.5" y="17.0"/>
|
||
|
|
<point x="77.0" y="16.5"/>
|
||
|
|
<point x="61.5" y="0.5"/>
|
||
|
|
<point x="61.5" y="-9.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="maybe_while" kind="OUTPUT" mult="<p>" tail="T13"/>
|
||
|
|
<arc head="T13" kind="INPUT" mult="<p>" tail="P1"/>
|
||
|
|
<arc head="T14" kind="INPUT" mult="<p>" tail="maybe_while"/>
|
||
|
|
<arc head="T15" kind="INPUT" mult="<p>" tail="maybe_while"/>
|
||
|
|
<arc head="critical" kind="OUTPUT" mult="<p>" tail="T15"/>
|
||
|
|
<arc broken="true" head="T14" kind="INPUT" tail="wantQ_is_FALSE">
|
||
|
|
<point x="89.0" y="9.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantQ_is_FALSE" kind="OUTPUT" tail="T14">
|
||
|
|
<point x="115.5" y="13.0"/>
|
||
|
|
<point x="116.5" y="56.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T15" kind="INPUT" tail="wantP_is_FALSE">
|
||
|
|
<point x="27.5" y="51.0"/>
|
||
|
|
<point x="87.0" y="49.0"/>
|
||
|
|
<point x="92.5" y="28.0"/>
|
||
|
|
<point x="100.5" y="26.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantP_is_FALSE" kind="OUTPUT" tail="T15">
|
||
|
|
<point x="116.0" y="28.5"/>
|
||
|
|
<point x="115.5" y="52.0"/>
|
||
|
|
<point x="115.0" y="53.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="critical" kind="OUTPUT" mult="<p>" tail="T14"/>
|
||
|
|
<arc broken="true" head="T16" kind="INPUT" mult="<t>" tail="TURN">
|
||
|
|
<point x="31.5" y="10.0"/>
|
||
|
|
<point x="97.5" y="35.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN" kind="OUTPUT" mult="<t2>" mult-k="0.013595223426818848" mult-x="-3.3343361616134644" mult-y="1.0454928874969482" tail="T16"/>
|
||
|
|
<arc head="T16" kind="INPUT" mult="<p>" tail="critical"/>
|
||
|
|
<arc broken="true" head="T17" kind="INPUT" mult="<t>" tail="TURN">
|
||
|
|
<point x="113.0" y="30.5"/>
|
||
|
|
<point x="116.5" y="56.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T17" kind="INPUT" mult="<p>" tail="critical"/>
|
||
|
|
<arc broken="true" head="TURN" kind="OUTPUT" mult="<t1>" mult-k="0.2738975763320923" mult-x="3.0200916835275677" mult-y="2.532668928664279" tail="T17">
|
||
|
|
<point x="85.5" y="54.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="setFalse_Q" kind="OUTPUT" mult="<p>" tail="T17"/>
|
||
|
|
<arc head="setFalse_P" kind="OUTPUT" mult="<p>" tail="T16"/>
|
||
|
|
<arc head="RESET_1" kind="INPUT" mult="<p>" tail="setFalse_P"/>
|
||
|
|
<arc head="RESET_2" kind="INPUT" mult="<p>" tail="setFalse_Q"/>
|
||
|
|
<arc broken="true" head="local" kind="OUTPUT" mult="<p>" mult-x="0.2966204004347901" mult-y="3.0" tail="RESET_2">
|
||
|
|
<point x="25.0" y="51.0"/>
|
||
|
|
<point x="24.5" y="8.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="local" kind="OUTPUT" mult="<p>" tail="RESET_1">
|
||
|
|
<point x="26.5" y="45.0"/>
|
||
|
|
<point x="27.0" y="8.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="RESET_1" kind="INPUT" tail="wantP_is_TRUE">
|
||
|
|
<point x="29.0" y="43.0"/>
|
||
|
|
<point x="34.5" y="43.0"/>
|
||
|
|
<point x="41.0" y="43.5"/>
|
||
|
|
<point x="40.5" y="47.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantP_is_FALSE" kind="OUTPUT" tail="RESET_1">
|
||
|
|
<point x="25.0" y="43.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="RESET_2" kind="INPUT" tail="wantQ_is_TRUE">
|
||
|
|
<point x="47.0" y="49.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantQ_is_FALSE" kind="OUTPUT" tail="RESET_2"/>
|
||
|
|
</edges>
|
||
|
|
</gspn>
|
||
|
|
<gspn name="Unfolding of CPN">
|
||
|
|
<nodes>
|
||
|
|
<place marking="1" name="TURN_t1" x="3.0" y="2.0"/>
|
||
|
|
<place name="TURN_t2" x="3.0" y="5.0"/>
|
||
|
|
<place name="wantP_is_TRUE" x="4.0" y="8.0"/>
|
||
|
|
<place name="wantQ_is_TRUE" x="4.0" y="18.0"/>
|
||
|
|
<place marking="1" name="wantQ_is_FALSE" x="4.0" y="23.0"/>
|
||
|
|
<place marking="1" name="wantP_is_FALSE" x="4.0" y="13.0"/>
|
||
|
|
<place marking="1" name="local_P" x="30.0" y="7.0"/>
|
||
|
|
<place marking="1" name="local_Q" x="30.0" y="10.0"/>
|
||
|
|
<place name="set_P" x="44.0" y="7.0"/>
|
||
|
|
<place name="set_Q" x="44.0" y="10.0"/>
|
||
|
|
<place name="while_P" x="30.0" y="21.0"/>
|
||
|
|
<place name="while_Q" x="30.0" y="24.0"/>
|
||
|
|
<place name="setFalse_P" x="30.0" y="35.0"/>
|
||
|
|
<place name="setFalse_Q" x="30.0" y="38.0"/>
|
||
|
|
<place name="await_P" x="49.0" y="35.0"/>
|
||
|
|
<place name="await_Q" x="49.0" y="38.0"/>
|
||
|
|
<place name="maybe_while_P" x="82.0" y="20.0"/>
|
||
|
|
<place name="maybe_while_Q" x="82.0" y="23.0"/>
|
||
|
|
<place name="P0_P" x="62.0" y="35.0"/>
|
||
|
|
<place name="P0_Q" x="62.0" y="38.0"/>
|
||
|
|
<place name="P1_P" x="82.0" y="35.0"/>
|
||
|
|
<place name="P1_Q" x="82.0" y="38.0"/>
|
||
|
|
<place name="critical_P" x="103.0" y="46.0"/>
|
||
|
|
<place name="critical_Q" x="103.0" y="49.0"/>
|
||
|
|
<place name="setFalse_P_P" x="54.0" y="44.0"/>
|
||
|
|
<place name="setFalse_P_Q" x="54.0" y="47.0"/>
|
||
|
|
<place name="setFalse_Q_P" x="54.0" y="50.0"/>
|
||
|
|
<place name="setFalse_Q_Q" x="54.0" y="53.0"/>
|
||
|
|
<transition name="T1_p_P" nservers-x="0.5" type="EXP" x="37.55" y="7.0"/>
|
||
|
|
<transition name="T1_p_Q" nservers-x="0.5" type="EXP" x="37.55" y="10.0"/>
|
||
|
|
<transition name="T2_p_P" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="50.55" y="3.0"/>
|
||
|
|
<transition name="T3_p_Q" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="50.55" y="14.0"/>
|
||
|
|
<transition name="T4_p_P" nservers-x="0.5" type="EXP" x="56.55" y="17.0"/>
|
||
|
|
<transition name="T5_p_Q" nservers-x="0.5" type="EXP" x="56.55" y="27.0"/>
|
||
|
|
<transition name="T6_p_P_t_t2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="33.55" y="28.0"/>
|
||
|
|
<transition name="T6_p_Q_t_t1" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="30.55" y="31.0"/>
|
||
|
|
<transition name="T7_p_P" nservers-x="0.5" type="EXP" x="40.55" y="32.0"/>
|
||
|
|
<transition name="T8_p_Q" nservers-x="0.5" type="EXP" x="40.55" y="42.0"/>
|
||
|
|
<transition name="T9_p_P_t_t1" nservers-x="0.5" type="EXP" x="56.55" y="35.0"/>
|
||
|
|
<transition name="T9_p_Q_t_t2" nservers-x="0.5" type="EXP" x="59.55" y="38.0"/>
|
||
|
|
<transition name="T10_p_P_t_t1" nservers-x="0.5" rotation="3.141592653589793" type="EXP" x="19.55" y="21.0"/>
|
||
|
|
<transition name="T10_p_Q_t_t2" nservers-x="0.5" rotation="3.141592653589793" type="EXP" x="22.55" y="24.0"/>
|
||
|
|
<transition name="T11_p_P" nservers-x="0.5" type="EXP" x="72.55" y="39.0"/>
|
||
|
|
<transition name="T12_p_Q" nservers-x="0.5" type="EXP" x="72.55" y="34.0"/>
|
||
|
|
<transition name="T13_p_P" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="82.55" y="28.0"/>
|
||
|
|
<transition name="T13_p_Q" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="82.55" y="31.0"/>
|
||
|
|
<transition name="T14_p_P" nservers-x="0.5" type="EXP" x="103.55" y="17.0"/>
|
||
|
|
<transition name="T15_p_Q" nservers-x="0.5" type="EXP" x="103.55" y="27.0"/>
|
||
|
|
<transition name="T16_p_P_t_t1" nservers-x="0.5" type="EXP" x="90.55" y="44.0"/>
|
||
|
|
<transition name="T16_p_P_t_t2" nservers-x="0.5" type="EXP" x="93.55" y="44.0"/>
|
||
|
|
<transition name="T17_p_Q_t_t1" nservers-x="0.5" type="EXP" x="90.55" y="53.0"/>
|
||
|
|
<transition name="T17_p_Q_t_t2" nservers-x="0.5" type="EXP" x="93.55" y="53.0"/>
|
||
|
|
<transition name="RESET_1_p_P" nservers-x="0.5" type="EXP" x="31.55" y="44.0"/>
|
||
|
|
<transition name="RESET_1_p_Q" nservers-x="0.5" type="EXP" x="31.55" y="47.0"/>
|
||
|
|
<transition name="RESET_2_p_P" nservers-x="0.5" type="EXP" x="31.55" y="50.0"/>
|
||
|
|
<transition name="RESET_2_p_Q" nservers-x="0.5" type="EXP" x="31.55" y="53.0"/>
|
||
|
|
</nodes>
|
||
|
|
<edges>
|
||
|
|
<arc head="T1_p_P" kind="INPUT" tail="local_P">
|
||
|
|
<point x="34.3755859375" y="8.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="set_P" kind="OUTPUT" tail="T1_p_P"/>
|
||
|
|
<arc head="T1_p_Q" kind="INPUT" tail="local_Q">
|
||
|
|
<point x="34.3755859375" y="11.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="set_Q" kind="OUTPUT" tail="T1_p_Q"/>
|
||
|
|
<arc broken="true" head="T2_p_P" kind="INPUT" tail="wantP_is_FALSE">
|
||
|
|
<point x="20.0" y="7.0"/>
|
||
|
|
<point x="19.5" y="7.0"/>
|
||
|
|
<point x="25.0" y="3.0"/>
|
||
|
|
<point x="25.5" y="3.0"/>
|
||
|
|
<point x="38.0" y="1.0"/>
|
||
|
|
<point x="44.5" y="4.0"/>
|
||
|
|
<point x="44.5" y="5.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantP_is_TRUE" kind="OUTPUT" tail="T2_p_P">
|
||
|
|
<point x="57.0" y="4.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="maybe_while_P" kind="OUTPUT" tail="T2_p_P">
|
||
|
|
<point x="63.0" y="7.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T2_p_P" kind="INPUT" tail="set_P"/>
|
||
|
|
<arc broken="true" head="wantQ_is_TRUE" kind="OUTPUT" tail="T3_p_Q">
|
||
|
|
<point x="59.0" y="15.0"/>
|
||
|
|
<point x="60.5" y="26.5"/>
|
||
|
|
<point x="39.5" y="29.5"/>
|
||
|
|
<point x="21.5" y="26.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="maybe_while_Q" kind="OUTPUT" tail="T3_p_Q">
|
||
|
|
<point x="59.0" y="16.5"/>
|
||
|
|
<point x="63.0" y="16.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T3_p_Q" kind="INPUT" tail="wantQ_is_FALSE">
|
||
|
|
<point x="20.5" y="14.0"/>
|
||
|
|
<point x="39.5" y="17.0"/>
|
||
|
|
<point x="39.5" y="16.5"/>
|
||
|
|
<point x="44.0" y="15.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T3_p_Q" kind="INPUT" tail="set_Q"/>
|
||
|
|
<arc broken="true" head="T4_p_P" kind="INPUT" tail="wantQ_is_TRUE">
|
||
|
|
<point x="28.5" y="15.0"/>
|
||
|
|
<point x="36.5" y="14.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="while_P" kind="OUTPUT" tail="T4_p_P"/>
|
||
|
|
<arc broken="true" head="wantQ_is_TRUE" kind="OUTPUT" tail="T4_p_P">
|
||
|
|
<point x="82.0" y="9.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T4_p_P" kind="INPUT" tail="maybe_while_P"/>
|
||
|
|
<arc broken="true" head="wantP_is_TRUE" kind="OUTPUT" tail="T5_p_Q">
|
||
|
|
<point x="53.5" y="30.5"/>
|
||
|
|
<point x="25.0" y="26.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T5_p_Q" kind="INPUT" tail="wantP_is_TRUE">
|
||
|
|
<point x="32.5" y="26.5"/>
|
||
|
|
<point x="61.0" y="29.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T5_p_Q" kind="INPUT" tail="maybe_while_Q"/>
|
||
|
|
<arc head="while_Q" kind="OUTPUT" tail="T5_p_Q"/>
|
||
|
|
<arc broken="true" head="T6_p_P_t_t2" kind="INPUT" tail="TURN_t2">
|
||
|
|
<point x="27.5" y="12.0"/>
|
||
|
|
<point x="25.5" y="25.0"/>
|
||
|
|
<point x="27.0" y="26.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN_t2" kind="OUTPUT" tail="T6_p_P_t_t2">
|
||
|
|
<point x="39.5" y="26.0"/>
|
||
|
|
<point x="36.5" y="38.0"/>
|
||
|
|
<point x="22.0" y="38.5"/>
|
||
|
|
<point x="22.0" y="38.0"/>
|
||
|
|
<point x="22.0" y="21.0"/>
|
||
|
|
<point x="22.0" y="20.5"/>
|
||
|
|
<point x="22.0" y="7.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T6_p_P_t_t2" kind="INPUT" tail="while_P"/>
|
||
|
|
<arc head="setFalse_P" kind="OUTPUT" tail="T6_p_P_t_t2"/>
|
||
|
|
<arc broken="true" head="T6_p_Q_t_t1" kind="INPUT" tail="TURN_t1">
|
||
|
|
<point x="24.5" y="15.0"/>
|
||
|
|
<point x="22.5" y="28.0"/>
|
||
|
|
<point x="24.0" y="29.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN_t1" kind="OUTPUT" tail="T6_p_Q_t_t1">
|
||
|
|
<point x="36.5" y="29.0"/>
|
||
|
|
<point x="33.5" y="41.0"/>
|
||
|
|
<point x="19.0" y="41.5"/>
|
||
|
|
<point x="19.0" y="41.0"/>
|
||
|
|
<point x="19.0" y="24.0"/>
|
||
|
|
<point x="19.0" y="23.5"/>
|
||
|
|
<point x="19.0" y="10.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T6_p_Q_t_t1" kind="INPUT" tail="while_Q"/>
|
||
|
|
<arc head="setFalse_Q" kind="OUTPUT" tail="T6_p_Q_t_t1"/>
|
||
|
|
<arc head="T7_p_P" kind="INPUT" tail="setFalse_P"/>
|
||
|
|
<arc broken="true" head="wantP_is_FALSE" kind="OUTPUT" tail="T7_p_P">
|
||
|
|
<point x="48.0" y="33.5"/>
|
||
|
|
<point x="59.0" y="35.0"/>
|
||
|
|
<point x="66.0" y="46.0"/>
|
||
|
|
<point x="64.5" y="48.5"/>
|
||
|
|
<point x="48.0" y="54.5"/>
|
||
|
|
<point x="44.0" y="55.0"/>
|
||
|
|
<point x="30.0" y="49.5"/>
|
||
|
|
<point x="25.5" y="36.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="await_P" kind="OUTPUT" tail="T7_p_P"/>
|
||
|
|
<arc broken="true" head="T7_p_P" kind="INPUT" tail="wantP_is_TRUE">
|
||
|
|
<point x="22.5" y="23.5"/>
|
||
|
|
<point x="39.5" y="24.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantQ_is_FALSE" kind="OUTPUT" tail="T8_p_Q">
|
||
|
|
<point x="55.5" y="48.0"/>
|
||
|
|
<point x="43.5" y="55.0"/>
|
||
|
|
<point x="42.5" y="55.0"/>
|
||
|
|
<point x="26.5" y="52.5"/>
|
||
|
|
<point x="25.0" y="52.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T8_p_Q" kind="INPUT" tail="setFalse_Q"/>
|
||
|
|
<arc broken="true" head="T8_p_Q" kind="INPUT" tail="wantQ_is_TRUE">
|
||
|
|
<point x="26.5" y="46.0"/>
|
||
|
|
<point x="34.5" y="45.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="await_Q" kind="OUTPUT" tail="T8_p_Q"/>
|
||
|
|
<arc broken="true" head="T9_p_P_t_t1" kind="INPUT" tail="TURN_t1">
|
||
|
|
<point x="23.0" y="43.5"/>
|
||
|
|
<point x="51.0" y="43.5"/>
|
||
|
|
<point x="54.5" y="35.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN_t1" kind="OUTPUT" tail="T9_p_P_t_t1">
|
||
|
|
<point x="64.5" y="32.5"/>
|
||
|
|
<point x="68.5" y="31.5"/>
|
||
|
|
<point x="70.5" y="11.0"/>
|
||
|
|
<point x="47.5" y="11.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P0_P" kind="OUTPUT" tail="T9_p_P_t_t1">
|
||
|
|
<point x="66.0" y="36.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T9_p_P_t_t1" kind="INPUT" tail="await_P"/>
|
||
|
|
<arc broken="true" head="T9_p_Q_t_t2" kind="INPUT" tail="TURN_t2">
|
||
|
|
<point x="26.0" y="46.5"/>
|
||
|
|
<point x="54.0" y="46.5"/>
|
||
|
|
<point x="57.5" y="38.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN_t2" kind="OUTPUT" tail="T9_p_Q_t_t2">
|
||
|
|
<point x="67.5" y="35.5"/>
|
||
|
|
<point x="71.5" y="34.5"/>
|
||
|
|
<point x="73.5" y="14.0"/>
|
||
|
|
<point x="50.5" y="14.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P0_Q" kind="OUTPUT" tail="T9_p_Q_t_t2">
|
||
|
|
<point x="69.0" y="39.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T9_p_Q_t_t2" kind="INPUT" tail="await_Q"/>
|
||
|
|
<arc broken="true" head="T10_p_P_t_t1" kind="INPUT" tail="TURN_t1">
|
||
|
|
<point x="16.0" y="16.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN_t1" kind="OUTPUT" tail="T10_p_P_t_t1">
|
||
|
|
<point x="23.0" y="19.0"/>
|
||
|
|
<point x="19.5" y="11.0"/>
|
||
|
|
<point x="12.0" y="9.5"/>
|
||
|
|
<point x="11.0" y="9.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="maybe_while_P" kind="OUTPUT" tail="T10_p_P_t_t1">
|
||
|
|
<point x="15.0" y="22.0"/>
|
||
|
|
<point x="15.44711650594682" y="18.923067952425427"/>
|
||
|
|
<point x="16.5" y="10.5"/>
|
||
|
|
<point x="71.5" y="15.0"/>
|
||
|
|
<point x="74.0" y="22.0"/>
|
||
|
|
<point x="68.0" y="22.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T10_p_P_t_t1" kind="INPUT" tail="while_P"/>
|
||
|
|
<arc broken="true" head="T10_p_Q_t_t2" kind="INPUT" tail="TURN_t2">
|
||
|
|
<point x="19.0" y="19.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN_t2" kind="OUTPUT" tail="T10_p_Q_t_t2">
|
||
|
|
<point x="26.0" y="22.0"/>
|
||
|
|
<point x="22.5" y="14.0"/>
|
||
|
|
<point x="15.0" y="12.5"/>
|
||
|
|
<point x="14.0" y="12.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="maybe_while_Q" kind="OUTPUT" tail="T10_p_Q_t_t2">
|
||
|
|
<point x="18.0" y="25.0"/>
|
||
|
|
<point x="18.44711650594682" y="21.923067952425427"/>
|
||
|
|
<point x="19.5" y="13.5"/>
|
||
|
|
<point x="74.5" y="18.0"/>
|
||
|
|
<point x="77.0" y="25.0"/>
|
||
|
|
<point x="71.0" y="25.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T10_p_Q_t_t2" kind="INPUT" tail="while_Q"/>
|
||
|
|
<arc head="P1_P" kind="OUTPUT" tail="T11_p_P"/>
|
||
|
|
<arc broken="true" head="wantP_is_TRUE" kind="OUTPUT" tail="T11_p_P">
|
||
|
|
<point x="84.5" y="44.5"/>
|
||
|
|
<point x="81.0" y="34.5"/>
|
||
|
|
<point x="59.5" y="30.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T11_p_P" kind="INPUT" tail="P0_P"/>
|
||
|
|
<arc broken="true" head="T11_p_P" kind="INPUT" tail="wantP_is_FALSE">
|
||
|
|
<point x="34.0" y="46.5"/>
|
||
|
|
<point x="61.0" y="43.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantQ_is_TRUE" kind="OUTPUT" tail="T12_p_Q">
|
||
|
|
<point x="115.5" y="21.0"/>
|
||
|
|
<point x="104.5" y="25.0"/>
|
||
|
|
<point x="103.0" y="24.5"/>
|
||
|
|
<point x="77.5" y="20.0"/>
|
||
|
|
<point x="77.0" y="19.5"/>
|
||
|
|
<point x="61.5" y="3.5"/>
|
||
|
|
<point x="61.5" y="-6.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P1_Q" kind="OUTPUT" tail="T12_p_Q"/>
|
||
|
|
<arc broken="true" head="T12_p_Q" kind="INPUT" tail="wantQ_is_FALSE">
|
||
|
|
<point x="64.5" y="34.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T12_p_Q" kind="INPUT" tail="P0_Q"/>
|
||
|
|
<arc head="maybe_while_P" kind="OUTPUT" tail="T13_p_P"/>
|
||
|
|
<arc head="T13_p_P" kind="INPUT" tail="P1_P"/>
|
||
|
|
<arc head="maybe_while_Q" kind="OUTPUT" tail="T13_p_Q"/>
|
||
|
|
<arc head="T13_p_Q" kind="INPUT" tail="P1_Q"/>
|
||
|
|
<arc head="T14_p_P" kind="INPUT" tail="maybe_while_P"/>
|
||
|
|
<arc broken="true" head="T14_p_P" kind="INPUT" tail="wantQ_is_FALSE">
|
||
|
|
<point x="89.0" y="9.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantQ_is_FALSE" kind="OUTPUT" tail="T14_p_P">
|
||
|
|
<point x="115.5" y="13.0"/>
|
||
|
|
<point x="116.5" y="56.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="critical_P" kind="OUTPUT" tail="T14_p_P"/>
|
||
|
|
<arc head="T15_p_Q" kind="INPUT" tail="maybe_while_Q"/>
|
||
|
|
<arc broken="true" head="wantP_is_FALSE" kind="OUTPUT" tail="T15_p_Q">
|
||
|
|
<point x="116.0" y="31.5"/>
|
||
|
|
<point x="115.5" y="55.0"/>
|
||
|
|
<point x="115.0" y="56.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T15_p_Q" kind="INPUT" tail="wantP_is_FALSE">
|
||
|
|
<point x="27.5" y="54.0"/>
|
||
|
|
<point x="87.0" y="52.0"/>
|
||
|
|
<point x="92.5" y="31.0"/>
|
||
|
|
<point x="100.5" y="29.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="critical_Q" kind="OUTPUT" tail="T15_p_Q"/>
|
||
|
|
<arc head="T16_p_P_t_t1" kind="INPUT" tail="critical_P"/>
|
||
|
|
<arc broken="true" head="T16_p_P_t_t1" kind="INPUT" tail="TURN_t1">
|
||
|
|
<point x="31.5" y="10.0"/>
|
||
|
|
<point x="97.5" y="35.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN_t2" kind="OUTPUT" tail="T16_p_P_t_t1"/>
|
||
|
|
<arc head="setFalse_P_P" kind="OUTPUT" tail="T16_p_P_t_t1"/>
|
||
|
|
<arc head="T16_p_P_t_t2" kind="INPUT" tail="critical_P"/>
|
||
|
|
<arc broken="true" head="T16_p_P_t_t2" kind="INPUT" tail="TURN_t2">
|
||
|
|
<point x="34.5" y="10.0"/>
|
||
|
|
<point x="100.5" y="35.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="TURN_t2" kind="OUTPUT" tail="T16_p_P_t_t2"/>
|
||
|
|
<arc head="setFalse_P_P" kind="OUTPUT" tail="T16_p_P_t_t2"/>
|
||
|
|
<arc head="T17_p_Q_t_t1" kind="INPUT" tail="critical_Q"/>
|
||
|
|
<arc broken="true" head="T17_p_Q_t_t1" kind="INPUT" tail="TURN_t1">
|
||
|
|
<point x="113.0" y="33.5"/>
|
||
|
|
<point x="116.5" y="59.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="setFalse_Q_Q" kind="OUTPUT" tail="T17_p_Q_t_t1"/>
|
||
|
|
<arc broken="true" head="TURN_t1" kind="OUTPUT" tail="T17_p_Q_t_t1">
|
||
|
|
<point x="85.5" y="57.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T17_p_Q_t_t2" kind="INPUT" tail="critical_Q"/>
|
||
|
|
<arc broken="true" head="T17_p_Q_t_t2" kind="INPUT" tail="TURN_t2">
|
||
|
|
<point x="116.0" y="33.5"/>
|
||
|
|
<point x="119.5" y="59.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="setFalse_Q_Q" kind="OUTPUT" tail="T17_p_Q_t_t2"/>
|
||
|
|
<arc broken="true" head="TURN_t1" kind="OUTPUT" tail="T17_p_Q_t_t2">
|
||
|
|
<point x="88.5" y="57.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="local_P" kind="OUTPUT" tail="RESET_1_p_P">
|
||
|
|
<point x="26.5" y="45.0"/>
|
||
|
|
<point x="27.0" y="8.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantP_is_FALSE" kind="OUTPUT" tail="RESET_1_p_P">
|
||
|
|
<point x="25.0" y="43.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="RESET_1_p_P" kind="INPUT" tail="setFalse_P_P"/>
|
||
|
|
<arc broken="true" head="RESET_1_p_P" kind="INPUT" tail="wantP_is_TRUE">
|
||
|
|
<point x="29.0" y="43.0"/>
|
||
|
|
<point x="34.5" y="43.0"/>
|
||
|
|
<point x="41.0" y="43.5"/>
|
||
|
|
<point x="40.5" y="47.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="local_Q" kind="OUTPUT" tail="RESET_1_p_Q">
|
||
|
|
<point x="26.5" y="48.0"/>
|
||
|
|
<point x="27.0" y="11.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="wantP_is_FALSE" kind="OUTPUT" tail="RESET_1_p_Q">
|
||
|
|
<point x="25.0" y="46.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="RESET_1_p_Q" kind="INPUT" tail="setFalse_P_Q"/>
|
||
|
|
<arc broken="true" head="RESET_1_p_Q" kind="INPUT" tail="wantP_is_TRUE">
|
||
|
|
<point x="29.0" y="46.0"/>
|
||
|
|
<point x="34.5" y="46.0"/>
|
||
|
|
<point x="41.0" y="46.5"/>
|
||
|
|
<point x="40.5" y="50.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="local_P" kind="OUTPUT" tail="RESET_2_p_P">
|
||
|
|
<point x="25.0" y="51.0"/>
|
||
|
|
<point x="24.5" y="8.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="RESET_2_p_P" kind="INPUT" tail="wantQ_is_TRUE">
|
||
|
|
<point x="47.0" y="49.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="RESET_2_p_P" kind="INPUT" tail="setFalse_Q_P"/>
|
||
|
|
<arc broken="true" head="wantQ_is_FALSE" kind="OUTPUT" tail="RESET_2_p_P"/>
|
||
|
|
<arc broken="true" head="local_Q" kind="OUTPUT" tail="RESET_2_p_Q">
|
||
|
|
<point x="25.0" y="54.0"/>
|
||
|
|
<point x="24.5" y="11.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="RESET_2_p_Q" kind="INPUT" tail="wantQ_is_TRUE">
|
||
|
|
<point x="47.0" y="52.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="RESET_2_p_Q" kind="INPUT" tail="setFalse_Q_Q"/>
|
||
|
|
<arc broken="true" head="wantQ_is_FALSE" kind="OUTPUT" tail="RESET_2_p_Q"/>
|
||
|
|
</edges>
|
||
|
|
</gspn>
|
||
|
|
<measures gspn-name="Unfolding of CPN" log-uuid="12fe4391-13ad-4c6c-b684-f19bf0053c19" name="CTL model checking of Unfolding of CPN" rapid-type="CTL_MODEL_CHECKING" simplified-UI="true">
|
||
|
|
<assignments/>
|
||
|
|
<rgmedd2 counter-examples="true"/>
|
||
|
|
<formulas>
|
||
|
|
<formula language="STAT">
|
||
|
|
<result-table>
|
||
|
|
<stat-result name="STAT">
|
||
|
|
<bindings/>
|
||
|
|
<stat key="CTL_time" value="0.012137 seconds."/>
|
||
|
|
<stat key="build_time" value="0.004212 seconds."/>
|
||
|
|
<stat key="num_rs_nodes" value="209"/>
|
||
|
|
<stat key="num_tangible_markings" value="126"/>
|
||
|
|
<stat key="total_firings" value="unknown"/>
|
||
|
|
</stat-result>
|
||
|
|
</result-table>
|
||
|
|
</formula>
|
||
|
|
<formula comment="CTL formula" expr="AG( #critical_P != 1 || #critical_Q != 1)" language="CTL">
|
||
|
|
<result-table>
|
||
|
|
<mc-result name="MEASURE1" value="true">
|
||
|
|
<bindings/>
|
||
|
|
</mc-result>
|
||
|
|
</result-table>
|
||
|
|
</formula>
|
||
|
|
<formula expr="AG ((#await_P==1 || #await_Q == 1) -> AF (#critical_P == 1 || #critical_Q == 1))" language="CTL">
|
||
|
|
<result-table>
|
||
|
|
<mc-result name="MEASURE2" value="false">
|
||
|
|
<bindings/>
|
||
|
|
</mc-result>
|
||
|
|
</result-table>
|
||
|
|
</formula>
|
||
|
|
<formula expr="AG (#await_P==1 -> AF (#critical_P == 1))" language="CTL">
|
||
|
|
<result-table>
|
||
|
|
<mc-result name="MEASURE0" value="false">
|
||
|
|
<bindings/>
|
||
|
|
</mc-result>
|
||
|
|
</result-table>
|
||
|
|
</formula>
|
||
|
|
</formulas>
|
||
|
|
</measures>
|
||
|
|
<resource-list>
|
||
|
|
<document-log uuid="12fe4391-13ad-4c6c-b684-f19bf0053c19">rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAAKB0AMcbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vRFNQTi1Ub29sIC1sb2FkICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zL2Rla2tlcl93bi4xLUNUTCBtb2RlbCBjaGVja2luZyBvZiBVbmZvbGRpbmcgb2YgQ1BOLnNvbHV0aW9uL1VuZm9sZGluZyBvZiBDUE4iIC1wYmFzaXMgLWRldGVjdC1leHAgLXBzZmwgLWJuZCAKdACkG1sxbRtbNG1MT0FESU5HIFBFVFJJIE5FVCAvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zL2Rla2tlcl93bi4xLUNUTCBtb2RlbCBjaGVja2luZyBvZiBVbmZvbGRpbmcgb2YgQ1BOLnNvbHV0aW9uL1VuZm9sZGluZyBvZiBDUE4gKG5ldC9kZWYpLi4uG1syMm0bWzI0bQp0AA9NQVJLSU5HIFBBUjogMAp0ABBQTEFDRVM6ICAgICAgMjgKdAAPUkFURSBQQVI6ICAgIDAKdAAQVFJBTlNJVElPTlM6IDI4CnQAD01FQVNVUkVTOiAgICAwCnQAKExPQURJTkcgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0AAEKdAABCnQAHkNPTVBVVElORyBQTEFDRSBGTE9XIEJBU0lTLi4uCnQAEk09MjgsIE49MjgsIE4wPTI4CnQAOUNvbXB1dGF0aW9uIG9mIEZsb3cgYmFzaXM6IHN0ZXAgMS8yOCwgfEt8PTI2LCBwcm9kdWN0cz0xCnQAUxtbMUEgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAKdABTG1sxQUNvbXB1dGF0aW9uIG9mIEZsb3cgYmFzaXM6IGNvbXBsZXRlZCBpbiAyMSBzdGVwcywgfEt8PTcuICAgICAgICAgICAgICAgICAgICAgIAp0AEBGT1VORCA3IFZFQ1RPUlMgSU4gVEhFIFBMQUNFIEZMT1cgQkFTSVMgKDQgc2VtaWZsb3dzLCAzIGZsb3dzKS4KdAABCnQAAQp0ACdBbGwgcGxhY2VzIGFyZSBjb3ZlcmVkIGJ5IHNvbWUgUC1mbG93Lgp0AAEKdAAmVE9UQUwgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0ACdBVk9JRCBFWFBPTkVOVElBTCBHUk9XVEggT0YgU0VNSUZMT1dTLgp0AB1DT01QVVRJTkcgUExBQ0UgU0VNSUZMT1dTLi4uCnQAEk09MjgsIE49MjgsIE4wPTI4CnQAK0dlbmVyYXRpb24gb2YgU2VtaWZsb3dzOiBzdGVwIDEvMjgsIHxLfD0yNgp0AFMbWzFBICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgCnQAUhtbMUFHZW5lcmF0aW9uIG9mIFNlbWlmbG93czogY29tcGxldGVkIGluIDIxIHN0ZXBzLCB8S3w9MTAuICAgICAgICAgICAgICAgICAgICAgIAp0ABpGT1VORCAxMCBQTEFDRSBTRU1JRkxPV1MuCnQAAQp0AAEKdAArQWxsIHBsYWNlcyBhcmUgY292ZXJlZCBieSBzb21lIFAtc2VtaWZsb3cuCnQAAQp0ACZUT1RBTCBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQALENPTVBVVElORyBQTEFDRSBCT1VORFMgRlJPTSBQLVNFTUlGTE9XUyAuLi4KdAAnG1swWBtbMzJtIFBST0NFU1MgRVhJVEVEIE5PUk1BTExZLhtbMG0KdADYG1swbUVYRUM6IHBlcmwgLWUgJ2FsYXJtIDUgOyBleGVjICIvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9EU1BOLVRvb2wgLWxvYWQgXCIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zL2Rla2tlcl93bi4xLUNUTCBtb2RlbCBjaGVja2luZyBvZiBVbmZvbGRpbmcgb2YgQ1BOLnNvbHV0aW9uL1VuZm9sZGluZyBvZiBDUE5cIiAtbG9hZC1ibmQgLWlscC1ibmQiICcKdACkG1sxbRtbNG1MT0FESU5HIFBFVFJJIE5FVCAvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zL2Rla2tlcl93bi4xLUNUTCBtb2RlbCBjaGVja2luZyBvZiBVbmZvbGRpbmcgb2YgQ1BOLnNvbHV0aW9uL1VuZm9sZGluZyBvZiBDUE4gKG5ldC9kZWYpLi4uG1syMm0bWzI0bQp0AA9NQVJLSU5HIFBBUjogMAp0ABBQTEFDRVM6ICAgICAgMjgKdAAPUkFURSBQQVI6ICAgIDAKdAAQVFJBTlNJVElPTlM6IDI4CnQAD01FQVNVUkVTOiAgICAwCnQAKExPQURJTkcgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0AAEKdAABCnQAFUxPQURJTkcgQk5EIEZJTEUgLi4uCnQAJUNPTVBVVElORyBQTEFDRSBCT1VORFMgVVNJTkcgSUxQIC4uLgp0ABhBbGwgcGxhY2VzIGFyZSBib3VuZGVkLgpxAH4AJHQArBtbMG1FWEVDOiAvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9SR01FREQzICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zL2Rla2tlcl93bi4xLUNUTCBtb2RlbCBjaGVja2luZyBvZiBVbmZvbGRpbmcgb2YgQ1BOLnNvbHV0aW9uL1VuZm9sZGluZyBvZiBDUE4iIC1NRVRBICAtYyAtQwp0ACBSYW5kb20gc2VlZHM6IDE1ODkxMjE1MzQgNzU0MzA2CnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAARR3JlYXRTUE4vTWVkZGx5Lgp0ADggIENvcHlyaWdodCAoQykgMTk4Ny0yMDE4LCBVbml2ZXJzaXR5IG9mIFRvcmlubywgSXRhbHkuCnQAMSAgU2VuZCBmaWxlcyBuZXRuYW1lLm5ldCwgLmRlZiB0byBlLW1haWwgYWRkcmVzcwp0ACsgIGJlY2N1dGlAZGkudW5pdG8uaXQgaWYgeW91IGZpbmQgYW55IGJ1Zy4KdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AB9CYXNlZCBvbiBNRURETFkgdmVyc2lvbiAwLjE2LjAKdABGICBDb3B5cmlnaHQgKEMpIDIwMDksIElvd2EgU3RhdGUgVW5pdmVyc2l0eSBSZXNlYXJjaCBGb3VuZGF0aW9uLCBJbmMuCnQAKSAgd2Vic2l0ZTogaHR0cDovL21lZGRseS5zb3VyY2Vmb3JnZS5uZXQKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0AClVc2luZyBwZXItZXZlbnQgc2F0dXJhdGlvbiAoc2F0LXByZWdlbikuCnQAG1VzaW5nIGZhc3QgTlNGIGdlbmVyYXRpb24uCnQAE
|
||
|
|
</resource-list>
|
||
|
|
</project>
|