440 lines
31 KiB
XML
Executable file
440 lines
31 KiB
XML
Executable file
<?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" version="121">
|
|
<gspn name="P" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false">
|
|
<nodes>
|
|
<place marking="1" name="local_p" x="6.0" y="4.0"/>
|
|
<place name="set_true_p" x="6.0" y="13.0"/>
|
|
<place name="while_p" x="6.0" y="24.0"/>
|
|
<place name="lsfalse_p" x="6.0" y="32.0"/>
|
|
<place name="await_p" x="6.0" y="40.0"/>
|
|
<place name="l_set_true_p" x="11.0" y="44.0"/>
|
|
<place name="critical_p" x="6.0" y="53.0"/>
|
|
<place name="swiitch_turn_p" x="6.0" y="61.0"/>
|
|
<transition name="T0" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="6.55" y="29.0"/>
|
|
<transition label-x="1.5" label-y="-2.0" name="T1" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="6.55" y="37.0"/>
|
|
<transition name="await_t_p" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="6.55" y="44.0"/>
|
|
<transition name="T3" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="6.55" y="50.0"/>
|
|
<transition name="csp" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="6.55" y="58.0"/>
|
|
<transition label-x="3.5" label-y="0.0" name="ncsp" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="6.55" y="9.0"/>
|
|
<transition name="strue_p" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="6.55" y="20.0"/>
|
|
<place name="set_false_p" x="6.0" y="67.0"/>
|
|
<transition name="switch_p" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="6.55" y="64.0"/>
|
|
<transition name="T8" nservers-x="0.5" type="EXP" x="6.55" y="1.0"/>
|
|
</nodes>
|
|
<edges>
|
|
<arc head="ncsp" kind="INPUT" tail="local_p"/>
|
|
<arc head="set_true_p" kind="OUTPUT" tail="ncsp"/>
|
|
<arc head="strue_p" kind="INPUT" tail="set_true_p"/>
|
|
<arc head="while_p" kind="OUTPUT" tail="strue_p"/>
|
|
<arc head="T0" kind="INPUT" tail="while_p"/>
|
|
<arc head="lsfalse_p" kind="OUTPUT" tail="T0"/>
|
|
<arc head="T1" kind="INPUT" tail="lsfalse_p"/>
|
|
<arc head="await_p" kind="OUTPUT" tail="T1"/>
|
|
<arc head="await_t_p" kind="INPUT" tail="await_p"/>
|
|
<arc head="l_set_true_p" kind="OUTPUT" tail="await_t_p"/>
|
|
<arc head="T3" kind="INPUT" tail="while_p">
|
|
<point x="2.0" y="25.5"/>
|
|
<point x="1.5" y="51.0"/>
|
|
</arc>
|
|
<arc head="critical_p" kind="OUTPUT" tail="T3"/>
|
|
<arc head="csp" kind="INPUT" tail="critical_p"/>
|
|
<arc head="swiitch_turn_p" kind="OUTPUT" tail="csp"/>
|
|
<arc head="switch_p" kind="INPUT" tail="swiitch_turn_p"/>
|
|
<arc head="set_false_p" kind="OUTPUT" tail="switch_p"/>
|
|
<arc head="local_p" kind="OUTPUT" tail="T8">
|
|
<point x="4.5" y="3.0"/>
|
|
</arc>
|
|
<arc head="T8" kind="INPUT" tail="local_p">
|
|
<point x="9.5" y="3.5"/>
|
|
</arc>
|
|
</edges>
|
|
</gspn>
|
|
<measures gspn-name="P" name="Measures" simplified-UI="false">
|
|
<assignments/>
|
|
<greatspn/>
|
|
<formulas>
|
|
<formula comment="Basic statistics of the toolchain execution." language="STAT"/>
|
|
</formulas>
|
|
</measures>
|
|
<gspn name="Turn" show-color-cmd="false" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false">
|
|
<nodes>
|
|
<transition label-x="1.5" label-y="-2.0" name="if_turn_2" nservers-x="0.5" rotation="4.71238898038469" superpos-x="-4.0" superpos-y="-1.0" type="EXP" x="19.55" y="12.0"/>
|
|
<transition name="await_t_p" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="19.55" y="18.0"/>
|
|
<place marking="1" name="turnP" x="37.0" y="18.0"/>
|
|
<place name="turnQ" x="39.0" y="9.0"/>
|
|
<transition name="switch_turn_p2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="21.55" y="28.0"/>
|
|
<transition label-x="1.5" label-y="-2.0" name="if_turn_1" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="57.55" y="12.0"/>
|
|
<transition name="await_t_q" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="57.55" y="17.0"/>
|
|
<transition name="switch_turn_q2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="59.55" y="27.0"/>
|
|
<transition name="switch_turn_p1" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="16.55" y="28.0"/>
|
|
<transition name="switch_turn_q1" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="66.55" y="27.0"/>
|
|
</nodes>
|
|
<edges>
|
|
<arc head="if_turn_2" kind="INPUT" mult-k="1.0999023437500002" tail="turnQ">
|
|
<point x="28.0" y="9.5"/>
|
|
</arc>
|
|
<arc head="turnQ" kind="OUTPUT" tail="if_turn_2">
|
|
<point x="29.5" y="12.5"/>
|
|
</arc>
|
|
<arc head="await_t_p" kind="INPUT" tail="turnP"/>
|
|
<arc head="turnP" kind="OUTPUT" tail="await_t_p">
|
|
<point x="29.5" y="21.0"/>
|
|
</arc>
|
|
<arc head="switch_turn_p2" kind="INPUT" tail="turnP"/>
|
|
<arc head="turnQ" kind="OUTPUT" tail="switch_turn_p2"/>
|
|
<arc head="if_turn_1" kind="INPUT" mult-k="0.96669921875" tail="turnP">
|
|
<point x="48.5" y="17.0"/>
|
|
</arc>
|
|
<arc head="turnP" kind="OUTPUT" tail="if_turn_1">
|
|
<point x="47.0" y="16.5"/>
|
|
</arc>
|
|
<arc head="await_t_q" kind="INPUT" tail="turnQ"/>
|
|
<arc head="turnQ" kind="OUTPUT" tail="await_t_q">
|
|
<point x="50.5" y="12.0"/>
|
|
</arc>
|
|
<arc head="switch_turn_q2" kind="INPUT" tail="turnQ"/>
|
|
<arc head="turnP" kind="OUTPUT" tail="switch_turn_q2">
|
|
<point x="39.5" y="19.0"/>
|
|
</arc>
|
|
<arc head="switch_turn_p1" kind="INPUT" tail="turnQ"/>
|
|
<arc head="turnQ" kind="OUTPUT" tail="switch_turn_p1">
|
|
<point x="35.0" y="12.5"/>
|
|
</arc>
|
|
<arc head="switch_turn_q1" kind="INPUT" tail="turnP">
|
|
<point x="67.0" y="25.5"/>
|
|
</arc>
|
|
<arc head="turnP" kind="OUTPUT" tail="switch_turn_q1"/>
|
|
</edges>
|
|
</gspn>
|
|
<gspn name="bools" show-color-cmd="false" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false">
|
|
<nodes>
|
|
<place name="wantP_TRUE" x="17.0" y="10.0"/>
|
|
<place marking="1" name="wantP_FALSE" x="17.0" y="24.0"/>
|
|
<place marking="1" name="WantQ_TRUE" x="27.0" y="10.0"/>
|
|
<place marking="1" name="WantQ_FALSE" x="27.0" y="24.0"/>
|
|
<transition name="want_p_to_true" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="5.55" y="1.0"/>
|
|
<transition name="loop_set_false_p" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="5.55" y="10.0"/>
|
|
<transition name="loop_set_true_p" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="5.55" y="24.0"/>
|
|
<transition name="want_p_to_false" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="5.55" y="33.0"/>
|
|
<transition name="want_q_to_true" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="39.55" y="1.0"/>
|
|
<transition name="loop_set_false_q" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="39.55" y="10.0"/>
|
|
<transition name="loop_set_true_q" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="39.55" y="24.0"/>
|
|
<transition name="want_q_to_false" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="39.55" y="33.0"/>
|
|
<transition name="csp" nservers-x="0.5" type="EXP" x="17.55" y="36.0"/>
|
|
<transition name="csq" nservers-x="0.5" type="EXP" x="28.55" y="36.0"/>
|
|
</nodes>
|
|
<edges>
|
|
<arc head="want_p_to_true" kind="INPUT" tail="wantP_FALSE"/>
|
|
<arc head="wantP_TRUE" kind="OUTPUT" tail="want_p_to_true"/>
|
|
<arc head="loop_set_false_p" kind="INPUT" tail="wantP_TRUE"/>
|
|
<arc head="wantP_FALSE" kind="OUTPUT" tail="loop_set_false_p"/>
|
|
<arc head="loop_set_true_p" kind="INPUT" tail="wantP_FALSE"/>
|
|
<arc head="wantP_TRUE" kind="OUTPUT" tail="loop_set_true_p"/>
|
|
<arc head="wantP_FALSE" kind="OUTPUT" tail="want_p_to_false"/>
|
|
<arc head="want_p_to_false" kind="INPUT" tail="wantP_TRUE"/>
|
|
<arc head="want_q_to_true" kind="INPUT" tail="WantQ_FALSE"/>
|
|
<arc head="WantQ_TRUE" kind="OUTPUT" tail="want_q_to_true"/>
|
|
<arc head="loop_set_false_q" kind="INPUT" tail="WantQ_TRUE"/>
|
|
<arc head="WantQ_FALSE" kind="OUTPUT" tail="loop_set_false_q"/>
|
|
<arc head="loop_set_true_q" kind="INPUT" tail="WantQ_FALSE"/>
|
|
<arc head="WantQ_TRUE" kind="OUTPUT" tail="loop_set_true_q"/>
|
|
<arc head="WantQ_FALSE" kind="OUTPUT" tail="want_q_to_false"/>
|
|
<arc head="want_q_to_false" kind="INPUT" tail="WantQ_TRUE"/>
|
|
<arc head="csp" kind="INPUT" tail="WantQ_FALSE"/>
|
|
<arc head="WantQ_FALSE" kind="OUTPUT" tail="csp">
|
|
<point x="25.5" y="32.0"/>
|
|
</arc>
|
|
<arc head="csq" kind="INPUT" tail="wantP_FALSE"/>
|
|
<arc head="wantP_FALSE" kind="OUTPUT" tail="csq">
|
|
<point x="25.0" y="35.5"/>
|
|
</arc>
|
|
</edges>
|
|
</gspn>
|
|
<gspn name="Proc" show-color-cmd="false" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false" zoom="75">
|
|
<nodes>
|
|
<transition delay="1.000000000000000" delay-x="0.4999980000000006" delay-y="1.0000040000000001" label-y="-1.4999980000000002" name="want_p_to_true" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="9.55" y="8.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.4999980000000006" delay-y="1.000003999999997" label-y="-1.4999980000000015" name="loop_set_false_p" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="18.55" y="18.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.4999980000000006" delay-y="1.000003999999997" label-y="-1.4999980000000015" name="loop_set_true_p" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="18.55" y="28.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.4999980000000006" delay-y="0.9999979999999979" label-y="-1.5000040000000041" name="want_p_to_false" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="8.55" y="37.000002"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="1.0000040000000001" label-x="-4.0000000041118255E-6" label-y="-1.4999980000000002" name="copy_want_q_to_true" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="49.550002" y="7.999998"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="1.000003999999997" label-x="-2.0000000020559128E-6" label-y="-1.4999980000000015" name="loop_set_false_q" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="42.55" y="18.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="1.000003999999997" label-x="-2.0000000020559128E-6" label-y="-1.4999980000000015" name="loop_set_true_q" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="42.55" y="28.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="0.9999979999999979" label-x="-2.0000000020559128E-6" label-y="-1.5000040000000041" name="want_q_to_false" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="49.55" y="37.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="0.9999980000000015" label-x="1.499997999999998" label-y="-2.0000019999999985" name="if_turn_2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="18.55" y="13.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="0.9999980000000015" label-x="-2.0000000020559128E-6" label-y="-1.500003999999997" name="await_t_p" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="18.55" y="23.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.5000039999999899" delay-y="1.0000040000000041" label-x="1.9999999949504854E-6" label-y="-1.499997999999998" name="switch_turn_p2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="9.55" y="31.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.5000039999999899" delay-y="0.9999980000000015" label-x="1.50000399999999" label-y="-2.0000019999999985" name="if_turn_1" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="42.55" y="13.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.5000039999999899" delay-y="0.9999980000000015" label-x="3.999999989900971E-6" label-y="-1.4999980000000015" name="await_t_q" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="42.55" y="23.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999800000000505" delay-y="0.9999979999999979" label-x="-3.999999989900971E-6" label-y="-1.5000040000000041" name="switch_turn_q2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="49.55" y="31.0"/>
|
|
<place name="P0" x="9.0" y="3.0"/>
|
|
<place name="P1" x="9.0" y="13.0"/>
|
|
<place name="P2" x="23.0" y="15.0"/>
|
|
<place name="P3" x="23.0" y="20.0"/>
|
|
<place name="P4" x="23.0" y="26.0"/>
|
|
<transition name="cs" nservers-x="0.5" type="EXP" x="9.55" y="25.0"/>
|
|
<place name="critical" x="5.0" y="25.0"/>
|
|
<place name="P5" x="5.0" y="31.0"/>
|
|
<place name="Q0" x="49.0" y="3.0"/>
|
|
<place name="Q1" x="49.0" y="13.0"/>
|
|
<place name="P8" x="36.0" y="15.0"/>
|
|
<place name="P9" x="36.0" y="20.0"/>
|
|
<place name="P10" x="36.0" y="26.0"/>
|
|
<place name="P11" x="56.0" y="26.0"/>
|
|
<place name="P12" x="56.0" y="31.0"/>
|
|
<transition name="T0" nservers-x="0.5" type="EXP" x="49.55" y="26.0"/>
|
|
</nodes>
|
|
<edges>
|
|
<arc head="if_turn_2" kind="INPUT" tail="P1"/>
|
|
<arc head="P2" kind="OUTPUT" tail="if_turn_2"/>
|
|
<arc head="loop_set_false_p" kind="INPUT" tail="P2"/>
|
|
<arc head="P3" kind="OUTPUT" tail="loop_set_false_p"/>
|
|
<arc head="await_t_p" kind="INPUT" tail="P3"/>
|
|
<arc head="P4" kind="OUTPUT" tail="await_t_p"/>
|
|
<arc head="loop_set_true_p" kind="INPUT" tail="P4"/>
|
|
<arc head="P1" kind="OUTPUT" tail="loop_set_true_p"/>
|
|
<arc head="cs" kind="INPUT" tail="P1"/>
|
|
<arc head="critical" kind="OUTPUT" tail="cs"/>
|
|
<arc head="switch_turn_p2" kind="INPUT" tail="critical"/>
|
|
<arc head="P5" kind="OUTPUT" tail="switch_turn_p2"/>
|
|
<arc head="want_p_to_false" kind="INPUT" tail="P5"/>
|
|
<arc broken="true" head="P0" kind="OUTPUT" tail="want_p_to_false">
|
|
<point x="8.5" y="53.0"/>
|
|
<point x="1.0" y="4.5"/>
|
|
<point x="6.0" y="4.0"/>
|
|
</arc>
|
|
<arc head="want_p_to_true" kind="INPUT" tail="P0"/>
|
|
<arc head="P1" kind="OUTPUT" tail="want_p_to_true"/>
|
|
<arc head="copy_want_q_to_true" kind="INPUT" tail="Q0"/>
|
|
<arc head="Q1" kind="OUTPUT" tail="copy_want_q_to_true"/>
|
|
<arc head="if_turn_1" kind="INPUT" tail="Q1"/>
|
|
<arc head="P8" kind="OUTPUT" tail="if_turn_1"/>
|
|
<arc head="loop_set_false_q" kind="INPUT" tail="P8"/>
|
|
<arc head="P9" kind="OUTPUT" tail="loop_set_false_q"/>
|
|
<arc head="await_t_q" kind="INPUT" tail="P9"/>
|
|
<arc head="P10" kind="OUTPUT" tail="await_t_q"/>
|
|
<arc head="loop_set_true_q" kind="INPUT" tail="P10"/>
|
|
<arc head="Q1" kind="OUTPUT" tail="loop_set_true_q"/>
|
|
<arc head="T0" kind="INPUT" tail="Q1"/>
|
|
<arc head="P11" kind="OUTPUT" tail="T0"/>
|
|
<arc head="switch_turn_q2" kind="INPUT" tail="P11"/>
|
|
<arc head="P12" kind="OUTPUT" tail="switch_turn_q2"/>
|
|
<arc head="want_q_to_false" kind="INPUT" tail="P12"/>
|
|
<arc broken="true" head="Q0" kind="OUTPUT" tail="want_q_to_false">
|
|
<point x="50.0" y="43.0"/>
|
|
<point x="60.5" y="42.5"/>
|
|
<point x="67.0" y="4.0"/>
|
|
</arc>
|
|
</edges>
|
|
</gspn>
|
|
<gspn name="bools+Turn+Proc" show-color-cmd="false" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false" zoom="75">
|
|
<nodes>
|
|
<place label-x="1.7763568394002505E-15" label-y="1.4999999999999982" name="wantP_TRUE" x="53.0" y="65.999998"/>
|
|
<place label-x="-4.000000000559112E-6" label-y="1.5000059999999973" marking="1" name="wantP_FALSE" x="53.0" y="79.99999600000001"/>
|
|
<place label-x="-2.000000010937697E-6" label-y="1.4999999999999982" name="wantQ_TRUE" x="69.0" y="76.0"/>
|
|
<place label-x="-3.999999991677328E-6" label-y="1.5000059999999973" marking="1" name="WantQ_FALSE" x="69.0" y="66.0"/>
|
|
<place label-x="-1.7763568394002505E-15" label-y="1.4999940000000027" marking="1" name="turnP" x="56.0" y="33.0"/>
|
|
<place label-x="2.000000000279556E-6" label-y="1.5000000000000009" name="turnQ" x="57.0" y="23.0"/>
|
|
<place label-x="2.999997999999998" label-y="-2.0000000020559128E-6" marking="1" name="local_P" x="39.000002" y="33.000002"/>
|
|
<place label-x="-2.000002000000002" label-y="1.500002000000002" name="while_P" x="39.000002" y="42.999998"/>
|
|
<place label-x="-3.999999991677328E-6" label-y="1.4999939999999992" name="P2" x="53.0" y="45.000002"/>
|
|
<place label-x="-3.999999991677328E-6" label-y="1.4999999999999982" name="P3" x="53.0" y="50.0"/>
|
|
<place label-x="-3.999999991677328E-6" label-y="1.4999999999999982" name="P4" x="53.0" y="56.0"/>
|
|
<place label-x="-1.7763568394002505E-15" label-y="1.4999999999999982" name="critical_P" x="35.0" y="54.999998"/>
|
|
<place label-x="-3.999999998782755E-6" label-y="1.4999999999999982" name="P5" x="35.0" y="66.999998"/>
|
|
<place label-x="5.999999997285954E-6" label-y="1.4999939999999992" marking="1" name="local_Q" x="78.999998" y="33.000002"/>
|
|
<place label-x="5.999999997285954E-6" label-y="1.5000000000000053" name="while_Q" x="78.999998" y="42.999998"/>
|
|
<place label-x="-4.000000005888182E-6" label-y="1.4999939999999992" name="P8" x="66.000002" y="45.000002"/>
|
|
<place label-x="-4.000000005888182E-6" label-y="1.4999999999999982" name="P9" x="66.000002" y="50.0"/>
|
|
<place label-x="-5.999999986627813E-6" label-y="1.4999999999999982" name="P10" x="66.000002" y="56.0"/>
|
|
<place label-x="5.999999997285954E-6" label-y="1.4999999999999982" name="critical_Q" x="86.0" y="56.0"/>
|
|
<place label-x="5.999999997285954E-6" label-y="1.4999999999999982" name="P12" x="86.0" y="67.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.4999919999999989" delay-y="1.000003999999997" label-y="-1.499997999999998" name="want_p_to_true" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="39.550002" y="38.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="1.000003999999997" label-y="-1.499998000000005" name="loop_set_false_p" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="48.550002" y="48.000002"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="1.000009999999996" label-y="-1.499997999999998" name="loop_set_true_p" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="48.550002" y="57.999998"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="1.00000399999999" label-y="-1.499998000000005" name="want_p_to_false" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="38.55" y="72.999998"/>
|
|
<transition delay="1.000000000000000" delay-x="0.5000039999999899" delay-y="1.000003999999997" label-x="-4.0000000041118255E-6" label-y="-1.4999919999999989" name="want_q_to_true" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="79.55" y="38.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999800000000505" delay-y="1.000003999999997" label-x="-1.9999999949504854E-6" label-y="-1.499998000000005" name="loop_set_false_q" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="72.55000199999999" y="48.000002"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999800000000505" delay-y="1.000009999999996" label-x="-1.9999999949504854E-6" label-y="-1.499997999999998" name="loop_set_true_q" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="72.55000199999999" y="57.999998"/>
|
|
<transition delay="1.000000000000000" delay-x="0.5000039999999899" delay-y="1.00000399999999" label-x="3.999999989900971E-6" label-y="-1.499998000000005" name="want_q_to_false" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="79.549998" y="69.999998"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="0.999998000000005" label-x="1.499997999999998" label-y="-2.000001999999995" name="if_turn_2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="48.550002" y="42.999998"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="0.9999979999999979" label-x="-2.0000000020559128E-6" label-y="-1.5000040000000041" name="await_t_p" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="48.550002" y="53.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.500003999999997" delay-y="1.000009999999996" label-x="1.9999999949504854E-6" label-y="-1.499997999999998" name="switch_turn_p2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="40.55" y="64.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999800000000505" delay-y="0.999998000000005" label-x="1.499998000000005" label-y="-2.000001999999995" name="if_turn_1" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="72.55000199999999" y="42.999998"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999800000000505" delay-y="0.9999979999999979" label-x="-1.9999999949504854E-6" label-y="-1.499997999999998" name="await_t_q" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="72.55000199999999" y="53.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.5000039999999899" delay-y="1.0000040000000041" label-x="1.9999999949504854E-6" label-y="-1.499997999999998" name="switch_turn_q2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="82.55" y="64.0"/>
|
|
<transition delay="1.000000000000000" delay-x="0.49999799999999794" delay-y="1.0000040000000041" label-x="-2.0000000020559128E-6" label-y="-1.499997999999998" name="csp" nservers-x="0.5" type="EXP" x="39.550002" y="54.999998"/>
|
|
<transition delay="1.000000000000000" delay-x="0.500009999999989" delay-y="0.9999979999999979" label-x="1.9999999949504854E-6" label-y="-1.499997999999998" name="csq" nservers-x="0.5" type="EXP" x="79.549998" y="56.0"/>
|
|
<transition name="T0" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="90.55" y="64.0"/>
|
|
<transition name="switch_turn_p1" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="31.55" y="64.0"/>
|
|
<transition name="T1" nservers-x="0.5" type="EXP" x="34.55" y="28.0"/>
|
|
<transition name="T2" nservers-x="0.5" type="EXP" x="75.55" y="27.0"/>
|
|
</nodes>
|
|
<edges>
|
|
<arc head="want_p_to_true" head-magnet="0" kind="INPUT" tail="local_P" tail-magnet="0"/>
|
|
<arc head="while_P" head-magnet="0" kind="OUTPUT" tail="want_p_to_true" tail-magnet="0"/>
|
|
<arc head="loop_set_false_p" head-magnet="0" kind="INPUT" tail="P2" tail-magnet="0"/>
|
|
<arc head="P3" head-magnet="0" kind="OUTPUT" tail="loop_set_false_p" tail-magnet="0"/>
|
|
<arc head="loop_set_true_p" head-magnet="0" kind="INPUT" tail="P4" tail-magnet="0"/>
|
|
<arc head="while_P" head-magnet="0" kind="OUTPUT" tail="loop_set_true_p" tail-magnet="0"/>
|
|
<arc head="want_p_to_false" head-magnet="0" kind="INPUT" tail="P5" tail-magnet="0"/>
|
|
<arc broken="true" head="local_P" head-magnet="0" kind="OUTPUT" tail="want_p_to_false" tail-magnet="0">
|
|
<point x="38.500002" y="88.999998"/>
|
|
<point x="31.000002000000002" y="40.5"/>
|
|
<point x="36.0" y="40.000002"/>
|
|
</arc>
|
|
<arc head="want_q_to_true" head-magnet="0" kind="INPUT" tail="local_Q" tail-magnet="0"/>
|
|
<arc head="while_Q" head-magnet="0" kind="OUTPUT" tail="want_q_to_true" tail-magnet="0"/>
|
|
<arc head="loop_set_false_q" head-magnet="0" kind="INPUT" tail="P8" tail-magnet="0"/>
|
|
<arc head="P9" head-magnet="0" kind="OUTPUT" tail="loop_set_false_q" tail-magnet="0"/>
|
|
<arc head="loop_set_true_q" head-magnet="0" kind="INPUT" tail="P10" tail-magnet="0"/>
|
|
<arc head="while_Q" head-magnet="0" kind="OUTPUT" tail="loop_set_true_q" tail-magnet="0"/>
|
|
<arc head="want_q_to_false" head-magnet="0" kind="INPUT" tail="P12" tail-magnet="0"/>
|
|
<arc broken="true" head="local_Q" head-magnet="0" kind="OUTPUT" tail="want_q_to_false" tail-magnet="0">
|
|
<point x="79.999998" y="73.000002"/>
|
|
<point x="90.499998" y="72.499998"/>
|
|
<point x="97.000002" y="34.000002"/>
|
|
</arc>
|
|
<arc head="if_turn_2" head-magnet="0" kind="INPUT" tail="while_P" tail-magnet="0"/>
|
|
<arc head="P2" head-magnet="0" kind="OUTPUT" tail="if_turn_2" tail-magnet="0"/>
|
|
<arc head="await_t_p" head-magnet="0" kind="INPUT" tail="P3" tail-magnet="0"/>
|
|
<arc head="P4" head-magnet="0" kind="OUTPUT" tail="await_t_p" tail-magnet="0"/>
|
|
<arc head="switch_turn_p2" head-magnet="0" kind="INPUT" tail="critical_P" tail-magnet="0"/>
|
|
<arc head="P5" head-magnet="0" kind="OUTPUT" tail="switch_turn_p2" tail-magnet="0"/>
|
|
<arc head="if_turn_1" head-magnet="0" kind="INPUT" tail="while_Q" tail-magnet="0"/>
|
|
<arc head="P8" head-magnet="0" kind="OUTPUT" tail="if_turn_1" tail-magnet="0"/>
|
|
<arc head="await_t_q" head-magnet="0" kind="INPUT" tail="P9" tail-magnet="0"/>
|
|
<arc head="P10" head-magnet="0" kind="OUTPUT" tail="await_t_q" tail-magnet="0"/>
|
|
<arc head="switch_turn_q2" head-magnet="0" kind="INPUT" tail="critical_Q" tail-magnet="0"/>
|
|
<arc head="P12" head-magnet="0" kind="OUTPUT" tail="switch_turn_q2" tail-magnet="0"/>
|
|
<arc head="csp" head-magnet="0" kind="INPUT" tail="while_P" tail-magnet="0"/>
|
|
<arc head="critical_P" head-magnet="0" kind="OUTPUT" tail="csp" tail-magnet="0"/>
|
|
<arc head="csq" head-magnet="0" kind="INPUT" tail="while_Q" tail-magnet="0"/>
|
|
<arc head="critical_Q" head-magnet="0" kind="OUTPUT" tail="csq" tail-magnet="0"/>
|
|
<arc broken="true" head="turnQ" kind="OUTPUT" tail="switch_turn_p2"/>
|
|
<arc broken="true" head="switch_turn_p2" kind="INPUT" tail="turnP"/>
|
|
<arc broken="true" head="await_t_p" kind="INPUT" tail="turnP"/>
|
|
<arc broken="true" head="turnP" kind="OUTPUT" tail="await_t_p">
|
|
<point x="50.0" y="28.0"/>
|
|
</arc>
|
|
<arc broken="true" head="if_turn_2" kind="INPUT" tail="turnQ"/>
|
|
<arc broken="true" head="turnQ" kind="OUTPUT" tail="if_turn_2">
|
|
<point x="42.5" y="22.0"/>
|
|
</arc>
|
|
<arc broken="true" head="if_turn_1" kind="INPUT" tail="turnP"/>
|
|
<arc broken="true" head="turnP" kind="OUTPUT" tail="if_turn_1">
|
|
<point x="62.5" y="29.5"/>
|
|
</arc>
|
|
<arc broken="true" head="turnQ" kind="OUTPUT" tail="await_t_q"/>
|
|
<arc broken="true" head="await_t_q" kind="INPUT" tail="turnQ"/>
|
|
<arc broken="true" head="switch_turn_q2" kind="INPUT" tail="turnQ"/>
|
|
<arc broken="true" head="turnP" kind="OUTPUT" mult-k="1.45615234375" tail="switch_turn_q2">
|
|
<point x="75.0" y="67.0"/>
|
|
</arc>
|
|
<arc broken="true" head="wantQ_TRUE" kind="OUTPUT" mult-k="0.9139648437500001" tail="want_q_to_true">
|
|
<point x="45.39736623123227" y="55.77762683433657"/>
|
|
<point x="42.5" y="49.5"/>
|
|
</arc>
|
|
<arc broken="true" head="want_q_to_true" kind="INPUT" mult-k="0.49990234375" tail="WantQ_FALSE">
|
|
<point x="55.5" y="52.5"/>
|
|
<point x="58.67910912997621" y="56.25712897179007"/>
|
|
</arc>
|
|
<arc broken="true" head="loop_set_false_q" kind="INPUT" tail="wantQ_TRUE"/>
|
|
<arc broken="true" head="WantQ_FALSE" kind="OUTPUT" tail="loop_set_false_q">
|
|
<point x="47.0" y="68.5"/>
|
|
</arc>
|
|
<arc broken="true" head="loop_set_true_q" kind="INPUT" mult-k="0.57392578125" tail="WantQ_FALSE">
|
|
<point x="44.5" y="80.0"/>
|
|
</arc>
|
|
<arc broken="true" head="wantQ_TRUE" kind="OUTPUT" mult-k="1.1780273437499997" tail="loop_set_true_q">
|
|
<point x="40.0" y="80.0"/>
|
|
</arc>
|
|
<arc broken="true" head="WantQ_FALSE" kind="OUTPUT" tail="want_q_to_false">
|
|
<point x="63.0" y="88.0"/>
|
|
<point x="66.5" y="68.0"/>
|
|
</arc>
|
|
<arc broken="true" head="want_q_to_false" kind="INPUT" tail="wantQ_TRUE">
|
|
<point x="71.5" y="48.5"/>
|
|
<point x="44.0" y="88.0"/>
|
|
</arc>
|
|
<arc broken="true" head="wantP_TRUE" kind="OUTPUT" tail="want_p_to_true"/>
|
|
<arc broken="true" head="want_p_to_true" kind="INPUT" tail="wantP_FALSE"/>
|
|
<arc broken="true" head="wantP_FALSE" kind="OUTPUT" tail="want_p_to_false"/>
|
|
<arc broken="true" head="want_p_to_false" kind="INPUT" tail="wantP_TRUE">
|
|
<point x="80.0" y="94.5"/>
|
|
</arc>
|
|
<arc broken="true" head="wantP_TRUE" kind="OUTPUT" tail="loop_set_true_p">
|
|
<point x="79.0" y="80.0"/>
|
|
</arc>
|
|
<arc broken="true" head="loop_set_true_p" kind="INPUT" tail="wantP_FALSE">
|
|
<point x="92.0" y="84.0"/>
|
|
</arc>
|
|
<arc broken="true" head="loop_set_false_p" kind="INPUT" tail="wantP_TRUE"/>
|
|
<arc broken="true" head="wantP_FALSE" kind="OUTPUT" tail="loop_set_false_p"/>
|
|
<arc broken="true" head="csp" kind="INPUT" tail="WantQ_FALSE"/>
|
|
<arc broken="true" head="WantQ_FALSE" kind="OUTPUT" tail="csp">
|
|
<point x="1.0" y="70.5"/>
|
|
</arc>
|
|
<arc broken="true" head="csq" kind="INPUT" tail="wantP_FALSE">
|
|
<point x="47.5" y="92.0"/>
|
|
</arc>
|
|
<arc broken="true" head="wantP_FALSE" kind="OUTPUT" tail="csq">
|
|
<point x="122.0" y="74.0"/>
|
|
<point x="94.0" y="93.0"/>
|
|
<point x="54.5" y="88.5"/>
|
|
</arc>
|
|
<arc broken="true" head="if_turn_2" kind="INPUT" tail="wantQ_TRUE">
|
|
<point x="33.5" y="86.5"/>
|
|
<point x="22.0" y="60.0"/>
|
|
</arc>
|
|
<arc broken="true" head="wantQ_TRUE" kind="OUTPUT" tail="if_turn_2">
|
|
<point x="18.0" y="59.0"/>
|
|
<point x="17.5" y="54.0"/>
|
|
<point x="69.0" y="53.5"/>
|
|
<point x="63.0" y="75.5"/>
|
|
<point x="63.0" y="76.0"/>
|
|
<point x="66.5" y="88.5"/>
|
|
<point x="66.5" y="88.0"/>
|
|
</arc>
|
|
<arc broken="true" head="if_turn_1" kind="INPUT" tail="wantP_TRUE">
|
|
<point x="72.0" y="51.5"/>
|
|
</arc>
|
|
<arc broken="true" head="wantP_TRUE" kind="OUTPUT" tail="if_turn_1"/>
|
|
<arc head="T0" kind="INPUT" tail="critical_Q"/>
|
|
<arc head="P12" kind="OUTPUT" tail="T0"/>
|
|
<arc broken="true" head="T0" kind="INPUT" tail="turnP">
|
|
<point x="91.5" y="62.5"/>
|
|
</arc>
|
|
<arc broken="true" head="turnP" kind="OUTPUT" tail="T0">
|
|
<point x="91.0" y="70.5"/>
|
|
</arc>
|
|
<arc head="switch_turn_p1" kind="INPUT" tail="critical_P"/>
|
|
<arc head="P5" kind="OUTPUT" tail="switch_turn_p1"/>
|
|
<arc broken="true" head="switch_turn_p1" kind="INPUT" tail="turnQ">
|
|
<point x="31.5" y="61.0"/>
|
|
</arc>
|
|
<arc broken="true" head="turnQ" kind="OUTPUT" tail="switch_turn_p1">
|
|
<point x="30.5" y="68.0"/>
|
|
<point x="29.0" y="35.5"/>
|
|
</arc>
|
|
<arc head="T1" kind="INPUT" tail="local_P"/>
|
|
<arc head="local_P" kind="OUTPUT" tail="T1">
|
|
<point x="34.5" y="34.0"/>
|
|
</arc>
|
|
<arc head="local_Q" kind="OUTPUT" tail="T2">
|
|
<point x="80.0" y="28.0"/>
|
|
</arc>
|
|
<arc head="T2" kind="INPUT" tail="local_Q"/>
|
|
</edges>
|
|
</gspn>
|
|
<measures gspn-name="bools+Turn+Proc" name="CTL model checking of bools+Turn+Proc" rapid-type="CTL_MODEL_CHECKING" simplified-UI="true">
|
|
<assignments/>
|
|
<rgmedd2 counter-examples="true"/>
|
|
<formulas>
|
|
<formula language="STAT"/>
|
|
<formula comment="CTL formula" expr="AG(!((#critical_P == 1) && (#critical_Q == 1)))" language="CTL"/>
|
|
<formula expr="AG(#local_P== 1 -> AF(#critical_P == 1))" language="CTL"/>
|
|
<formula expr="AG(#local_Q== 1 -> AF(#critical_Q == 1))" language="CTL"/>
|
|
<formula expr="AG((#local_Q== 1 || #local_P==1) -> AF(#critical_Q == 1 || #critical_P==1))" language="CTL"/>
|
|
</formulas>
|
|
</measures>
|
|
</project>
|