332 lines
38 KiB
Text
332 lines
38 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="Alg3-2" version="121">
|
||
|
|
<gspn name="ProcP" show-color-cmd="false" show-fluid-cmd="false" view-rates="false">
|
||
|
|
<nodes>
|
||
|
|
<place label-x="-2.0" label-y="0.0" marking="1" name="P0" x="7.0" y="2.0"/>
|
||
|
|
<place label-x="-2.5" label-y="0.5" name="P1" x="7.0" y="9.0"/>
|
||
|
|
<place label-x="-2.5" label-y="0.0" name="P2" x="7.0" y="16.0"/>
|
||
|
|
<place label-x="-2.5" label-y="0.0" name="P3" x="7.0" y="24.0"/>
|
||
|
|
<transition label-x="-2.5" label-y="0.0" name="ncsP" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="7.55" y="6.0"/>
|
||
|
|
<transition label-x="3.5" label-y="1.0" name="isTurnP" nservers-x="0.5" rotation="4.71238898038469" superpos-x="4.0" superpos-y="-0.5" superposition-tags="LisTurnP" type="EXP" x="7.55" y="13.0"/>
|
||
|
|
<transition label-x="-2.5" label-y="0.0" name="csP" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="7.55" y="20.0"/>
|
||
|
|
<transition name="T1" nservers-x="0.5" type="EXP" x="11.55" y="3.0"/>
|
||
|
|
<transition label-x="2.0" label-y="0.0" name="T0" nservers-x="0.5" rotation="1.5707963267948966" superpos-x="3.0" superpos-y="-1.0" superposition-tags="LsetTurnQ" type="EXP" x="7.55" y="29.0"/>
|
||
|
|
</nodes>
|
||
|
|
<edges>
|
||
|
|
<arc head="ncsP" kind="INPUT" tail="P0">
|
||
|
|
<point x="8.0" y="6.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="isTurnP" kind="INPUT" tail="P1"/>
|
||
|
|
<arc head="P1" kind="OUTPUT" tail="ncsP"/>
|
||
|
|
<arc head="P2" kind="OUTPUT" tail="isTurnP"/>
|
||
|
|
<arc head="csP" kind="INPUT" tail="P2"/>
|
||
|
|
<arc head="P3" kind="OUTPUT" tail="csP"/>
|
||
|
|
<arc head="T1" kind="INPUT" tail="P0">
|
||
|
|
<point x="9.5" y="5.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P0" kind="OUTPUT" tail="T1">
|
||
|
|
<point x="11.0" y="2.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T0" kind="INPUT" tail="P3"/>
|
||
|
|
<arc head="P0" kind="OUTPUT" tail="T0">
|
||
|
|
<point x="8.0" y="33.5"/>
|
||
|
|
<point x="2.0" y="32.5"/>
|
||
|
|
<point x="2.0" y="2.5"/>
|
||
|
|
<point x="6.5" y="1.0"/>
|
||
|
|
</arc>
|
||
|
|
</edges>
|
||
|
|
</gspn>
|
||
|
|
<gspn name="ProcQ" show-color-cmd="false" show-fluid-cmd="false" view-rates="false" zoom="75">
|
||
|
|
<nodes>
|
||
|
|
<place label-x="-2.0" label-y="0.0" marking="1" name="Q0" x="7.0" y="2.0"/>
|
||
|
|
<place label-x="-2.5" label-y="0.5" name="Q1" x="7.0" y="9.0"/>
|
||
|
|
<place label-x="-2.5" label-y="0.0" name="Q2" x="7.0" y="16.0"/>
|
||
|
|
<place label-x="-2.5" label-y="0.0" name="Q3" x="7.0" y="24.0"/>
|
||
|
|
<transition label-x="-2.5" label-y="0.0" name="ncsQ" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="7.55" y="6.0"/>
|
||
|
|
<transition label-x="3.5" label-y="1.0" name="isTurnQ" nservers-x="0.5" rotation="4.71238898038469" superpos-x="4.0" superpos-y="-0.5" superposition-tags="LisTurnQ" type="EXP" x="7.55" y="13.0"/>
|
||
|
|
<transition label-x="-2.5" label-y="0.0" name="csQ" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="7.55" y="20.0"/>
|
||
|
|
<transition name="T1" nservers-x="0.5" type="EXP" x="11.55" y="3.0"/>
|
||
|
|
<transition label-x="2.0" label-y="0.0" name="T0" nservers-x="0.5" rotation="1.5707963267948966" superpos-x="3.0" superpos-y="-1.0" superposition-tags="LsetTurnP" type="EXP" x="7.55" y="29.0"/>
|
||
|
|
</nodes>
|
||
|
|
<edges>
|
||
|
|
<arc head="ncsQ" kind="INPUT" tail="Q0">
|
||
|
|
<point x="8.0" y="6.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="isTurnQ" kind="INPUT" tail="Q1"/>
|
||
|
|
<arc head="Q1" kind="OUTPUT" tail="ncsQ"/>
|
||
|
|
<arc head="Q2" kind="OUTPUT" tail="isTurnQ"/>
|
||
|
|
<arc head="csQ" kind="INPUT" tail="Q2"/>
|
||
|
|
<arc head="Q3" kind="OUTPUT" tail="csQ"/>
|
||
|
|
<arc head="T1" kind="INPUT" tail="Q0">
|
||
|
|
<point x="9.5" y="5.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Q0" kind="OUTPUT" tail="T1">
|
||
|
|
<point x="11.0" y="2.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T0" kind="INPUT" tail="Q3"/>
|
||
|
|
<arc head="Q0" kind="OUTPUT" tail="T0">
|
||
|
|
<point x="8.0" y="33.5"/>
|
||
|
|
<point x="2.0" y="32.5"/>
|
||
|
|
<point x="2.0" y="2.5"/>
|
||
|
|
<point x="6.5" y="1.0"/>
|
||
|
|
</arc>
|
||
|
|
</edges>
|
||
|
|
</gspn>
|
||
|
|
<gspn name="Turn" show-color-cmd="false" show-fluid-cmd="false" view-rates="false">
|
||
|
|
<nodes>
|
||
|
|
<transition label-x="-2.0" label-y="0.0" name="isTurnP" nservers-x="0.5" rotation="4.71238898038469" superpos-x="-3.0" superpos-y="1.5" superposition-tags="LisTurnP" type="EXP" x="10.55" y="4.0"/>
|
||
|
|
<transition label-x="3.0" label-y="0.0" name="isTurnQ" nservers-x="0.5" rotation="4.71238898038469" superpos-x="2.5" superpos-y="2.0" superposition-tags="LisTurnQ" type="EXP" x="8.55" y="19.0"/>
|
||
|
|
<place marking="1" name="TurnP" x="18.0" y="7.0"/>
|
||
|
|
<place name="TurnQ" x="17.0" y="18.0"/>
|
||
|
|
<transition label-x="-4.0" label-y="1.5" name="T1" nservers-x="0.5" rotation="4.71238898038469" superpos-x="-4.0" superpos-y="0.0" superposition-tags="LsetTurnQ" type="EXP" x="13.55" y="13.0"/>
|
||
|
|
<transition label-x="3.0" label-y="0.5" name="VsetTurnP" nservers-x="0.5" rotation="4.71238898038469" superpos-x="3.0" superpos-y="2.0" superposition-tags="LsetTurnP" type="EXP" x="23.55" y="12.0"/>
|
||
|
|
<transition name="VsetTurnPbis" nservers-x="0.5" superposition-tags="LsetTurnP" type="EXP" x="27.55" y="5.0"/>
|
||
|
|
<transition label-y="3.0" name="T2" nservers-x="0.5" superpos-x="0.5" superpos-y="2.0" superposition-tags="LsetTurnQ" type="EXP" x="26.55" y="19.0"/>
|
||
|
|
</nodes>
|
||
|
|
<edges>
|
||
|
|
<arc head="T1" kind="INPUT" tail="TurnP"/>
|
||
|
|
<arc head="TurnQ" kind="OUTPUT" tail="T1"/>
|
||
|
|
<arc head="VsetTurnP" kind="INPUT" tail="TurnQ"/>
|
||
|
|
<arc head="TurnP" kind="OUTPUT" tail="VsetTurnP">
|
||
|
|
<point x="24.0" y="12.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="isTurnP" kind="INPUT" tail="TurnP">
|
||
|
|
<point x="14.0" y="10.5"/>
|
||
|
|
<point x="12.5" y="11.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="TurnP" kind="OUTPUT" tail="isTurnP">
|
||
|
|
<point x="13.5" y="6.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="VsetTurnPbis" kind="INPUT" tail="TurnP">
|
||
|
|
<point x="22.5" y="8.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="TurnP" kind="OUTPUT" tail="VsetTurnPbis">
|
||
|
|
<point x="22.0" y="4.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T2" kind="INPUT" mult-k="0.7405273437500001" tail="TurnQ">
|
||
|
|
<point x="22.5" y="21.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="TurnQ" kind="OUTPUT" mult-k="0.0" tail="T2"/>
|
||
|
|
<arc head="isTurnQ" kind="INPUT" mult-k="0.0" tail="TurnQ">
|
||
|
|
<point x="10.5" y="18.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="TurnQ" kind="OUTPUT" mult-k="0.99990234375" tail="isTurnQ"/>
|
||
|
|
</edges>
|
||
|
|
</gspn>
|
||
|
|
<gspn name="ProcP+ProcQ" show-color-cmd="false" show-fluid-cmd="false" view-rates="false">
|
||
|
|
<nodes>
|
||
|
|
<place label-x="-1.9999960000000012" label-y="0.0" marking="1" name="P0" x="6.999998000000001" y="2.0"/>
|
||
|
|
<place label-x="-2.500000000000001" label-y="0.49999800000000155" name="P1" x="6.999998000000001" y="9.000001999999999"/>
|
||
|
|
<place label-x="-2.500000000000001" label-y="-1.7763568394002505E-15" name="P2" x="6.999998000000001" y="15.999998000000001"/>
|
||
|
|
<place label-x="-2.500000000000001" label-y="5.999999997285954E-6" name="P3" x="6.999998000000001" y="23.999996000000003"/>
|
||
|
|
<place label-x="-1.9999979999999997" label-y="-1.7763568394002505E-15" marking="1" name="Q0" x="40.999998" y="2.0"/>
|
||
|
|
<place label-x="-2.5000019999999967" label-y="0.4999979999999962" name="Q1" x="40.999998" y="9.000002000000002"/>
|
||
|
|
<place label-x="-2.5000019999999967" label-y="5.329070518200751E-15" name="Q2" x="40.999998" y="15.999997999999998"/>
|
||
|
|
<place label-x="-2.5000019999999967" label-y="-1.7763568394002505E-15" name="Q3" x="40.999998" y="24.000002000000002"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000039999999979" delay-y="0.9999979999999997" label-x="-2.500000000000001" label-y="-3.9999999996709334E-6" name="ncsP" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="7.549998" y="6.000002"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000039999999979" delay-y="1.000003999999997" label-x="3.500000000000001" label-y="1.000003999999997" name="isTurnP" nservers-x="0.5" rotation="1.5707963267948966" superposition-tags="LisTurnP" type="EXP" x="7.549998" y="12.999998000000001"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000039999999979" delay-y="0.9999980000000015" label-x="-2.4999980000000006" label-y="1.999999998503199E-6" name="csP" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="7.549998" y="20.0"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.4999980000000015" delay-y="0.9999979999999997" label-x="0.1562519999999985" label-y="-1.5000040000000006" name="T11" nservers-x="0.5" type="EXP" x="11.55" y="3.0000020000000003"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000039999999979" delay-y="0.9999979999999979" label-x="2.156250000000001" label-y="2.0000000020559128E-6" name="T01" nservers-x="0.5" rotation="1.5707963267948966" superposition-tags="LsetTurnQ" type="EXP" x="7.549998" y="29.0"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000040000000041" delay-y="0.9999979999999979" label-x="-2.499997999999998" label-y="-4.0000000041118255E-6" name="ncsQ" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="41.549997999999995" y="6.000002000000002"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000040000000041" delay-y="1.0000040000000041" label-x="3.500002000000002" label-y="1.0000040000000041" name="isTurnQ" nservers-x="0.5" rotation="1.5707963267948966" superposition-tags="LisTurnQ" type="EXP" x="41.549997999999995" y="12.999997999999998"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000040000000041" delay-y="0.9999979999999979" label-x="-2.499995999999996" label-y="2.0000000020559128E-6" name="csQ" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="41.549997999999995" y="20.0"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.49999799999999794" delay-y="0.9999979999999979" label-x="2.0000000020559128E-6" label-y="-1.5000040000000041" name="T1" nservers-x="0.5" type="EXP" x="45.55" y="3.000002000000002"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000040000000041" delay-y="0.9999979999999979" label-x="2.0" label-y="2.0000000020559128E-6" name="T0" nservers-x="0.5" rotation="1.5707963267948966" superposition-tags="LsetTurnP" type="EXP" x="41.549997999999995" y="29.0"/>
|
||
|
|
</nodes>
|
||
|
|
<edges>
|
||
|
|
<arc head="ncsP" head-magnet="0" kind="INPUT" tail="P0" tail-magnet="0">
|
||
|
|
<point x="7.999998000000001" y="6.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P1" head-magnet="0" kind="OUTPUT" tail="ncsP" tail-magnet="0"/>
|
||
|
|
<arc head="isTurnP" head-magnet="0" kind="INPUT" tail="P1" tail-magnet="0"/>
|
||
|
|
<arc head="P2" head-magnet="0" kind="OUTPUT" tail="isTurnP" tail-magnet="0"/>
|
||
|
|
<arc head="csP" head-magnet="0" kind="INPUT" tail="P2" tail-magnet="0"/>
|
||
|
|
<arc head="P3" head-magnet="0" kind="OUTPUT" tail="csP" tail-magnet="0"/>
|
||
|
|
<arc head="T11" head-magnet="0" kind="INPUT" tail="P0" tail-magnet="0">
|
||
|
|
<point x="9.499998000000001" y="5.500002"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P0" head-magnet="0" kind="OUTPUT" tail="T11" tail-magnet="0">
|
||
|
|
<point x="10.999998000000001" y="1.999998"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T01" head-magnet="0" kind="INPUT" tail="P3" tail-magnet="0"/>
|
||
|
|
<arc head="P0" head-magnet="0" kind="OUTPUT" tail="T01" tail-magnet="0">
|
||
|
|
<point x="7.999998000000001" y="33.499998"/>
|
||
|
|
<point x="1.999998" y="32.500002"/>
|
||
|
|
<point x="1.999998" y="2.5000020000000003"/>
|
||
|
|
<point x="6.499998000000001" y="1.000002"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="ncsQ" head-magnet="0" kind="INPUT" tail="Q0" tail-magnet="0">
|
||
|
|
<point x="41.999998" y="6.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Q1" head-magnet="0" kind="OUTPUT" tail="ncsQ" tail-magnet="0"/>
|
||
|
|
<arc head="isTurnQ" head-magnet="0" kind="INPUT" tail="Q1" tail-magnet="0"/>
|
||
|
|
<arc head="Q2" head-magnet="0" kind="OUTPUT" tail="isTurnQ" tail-magnet="0"/>
|
||
|
|
<arc head="csQ" head-magnet="0" kind="INPUT" tail="Q2" tail-magnet="0"/>
|
||
|
|
<arc head="Q3" head-magnet="0" kind="OUTPUT" tail="csQ" tail-magnet="0"/>
|
||
|
|
<arc head="T1" head-magnet="0" kind="INPUT" tail="Q0" tail-magnet="0">
|
||
|
|
<point x="43.499998" y="5.500002000000002"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Q0" head-magnet="0" kind="OUTPUT" tail="T1" tail-magnet="0">
|
||
|
|
<point x="44.999998" y="1.999997999999998"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T0" head-magnet="0" kind="INPUT" tail="Q3" tail-magnet="0"/>
|
||
|
|
<arc head="Q0" head-magnet="0" kind="OUTPUT" tail="T0" tail-magnet="0">
|
||
|
|
<point x="41.999998" y="33.499998"/>
|
||
|
|
<point x="35.999998" y="32.500002"/>
|
||
|
|
<point x="35.999998" y="2.500002000000002"/>
|
||
|
|
<point x="40.499998" y="1.000002000000002"/>
|
||
|
|
</arc>
|
||
|
|
</edges>
|
||
|
|
</gspn>
|
||
|
|
<gspn name="ProcP+ProcQ+Turn" show-color-cmd="false" show-fluid-cmd="false" view-rates="false" zoom="125">
|
||
|
|
<nodes>
|
||
|
|
<place label-x="-1.9999960000000012" label-y="0.0" marking="1" name="P0" x="6.999998000000001" y="2.0"/>
|
||
|
|
<place label-x="-2.500000000000001" label-y="0.49999800000000155" name="P1" x="6.999998000000001" y="9.000001999999999"/>
|
||
|
|
<place label-x="-2.500000000000001" label-y="-1.7763568394002505E-15" name="P2" x="6.999998000000001" y="15.999998000000001"/>
|
||
|
|
<place label-x="-2.500000000000001" label-y="5.999999997285954E-6" name="P3" x="6.999998000000001" y="23.999996000000003"/>
|
||
|
|
<place label-x="-1.9999920000000007" label-y="0.0" marking="1" name="Q0" x="40.999994" y="2.0"/>
|
||
|
|
<place label-x="-2.4999959999999977" label-y="0.49999800000000155" name="Q1" x="40.999994" y="9.000001999999999"/>
|
||
|
|
<place label-x="-2.4999959999999977" label-y="-1.7763568394002505E-15" name="Q2" x="40.999994" y="15.999998000000001"/>
|
||
|
|
<place label-x="-2.4999959999999977" label-y="-1.7763568394002505E-15" name="Q3" x="40.999994" y="24.000002000000002"/>
|
||
|
|
<place label-x="-2.0000000020559128E-6" label-y="-2.499997999999998" marking="1" name="TurnP" x="23.000002000000002" y="9.999997999999998"/>
|
||
|
|
<place label-y="-2.500002000000002" name="TurnQ" x="22.0" y="21.000002000000002"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000039999999979" delay-y="0.9999979999999997" label-x="-2.500000000000001" label-y="-3.9999999996709334E-6" name="ncsP" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="7.549998" y="6.000002"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000039999999979" delay-y="1.000003999999997" label-x="3.500000000000001" label-y="1.000003999999997" name="isTurnP" nservers-x="0.5" rotation="1.5707963267948966" superposition-tags="LisTurnP" type="EXP" x="7.549998" y="12.999998000000001"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000039999999979" delay-y="0.9999980000000015" label-x="-2.4999980000000006" label-y="1.999999998503199E-6" name="csP" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="7.549998" y="20.0"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.4999980000000015" delay-y="0.9999979999999997" label-x="0.1562519999999985" label-y="-1.5000040000000006" name="T11" nservers-x="0.5" type="EXP" x="11.55" y="3.0000020000000003"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.5000039999999979" delay-y="0.9999979999999979" label-x="2.312500000000001" label-y="2.0000000020559128E-6" name="T011" nservers-x="0.5" rotation="1.5707963267948966" superposition-tags="LsetTurnQ" type="EXP" x="7.549998" y="29.0"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.500003999999997" delay-y="0.9999919999999989" label-x="2.15625" label-y="1.9999999949504854E-6" name="T01" nservers-x="0.5" rotation="1.5707963267948966" superposition-tags="LsetTurnQ" type="EXP" x="14.55" y="31.0"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.500003999999997" delay-y="0.9999979999999997" label-x="-2.499991999999999" label-y="-3.9999999996709334E-6" name="ncsQ" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="41.549994" y="6.000002"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.500003999999997" delay-y="1.000003999999997" label-x="3.500008000000001" label-y="1.000003999999997" name="isTurnQ" nservers-x="0.5" rotation="1.5707963267948966" superposition-tags="LisTurnQ" type="EXP" x="41.549994" y="12.999998000000001"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.500003999999997" delay-y="0.9999980000000015" label-x="-2.499996000000003" label-y="1.999999998503199E-6" name="csQ" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="41.549994" y="20.0"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.4999919999999989" delay-y="0.9999979999999997" label-x="-4.0000000041118255E-6" label-y="-1.5000040000000006" name="T1" nservers-x="0.5" type="EXP" x="45.550002" y="3.0000020000000003"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.500003999999997" delay-y="0.9999979999999979" label-x="2.15625" label-y="2.0000000020559128E-6" name="T02" nservers-x="0.5" rotation="1.5707963267948966" superpos-x="5.999999999062311E-6" superpos-y="1.5" superposition-tags="LsetTurnP" type="EXP" x="41.549994" y="29.0"/>
|
||
|
|
<transition delay="1.000000" delay-x="0.500003999999997" delay-y="0.9999919999999989" label-x="2.0" label-y="1.9999999949504854E-6" name="T0" nservers-x="0.5" rotation="1.5707963267948966" superpos-x="1.5" superpos-y="-1.5" superposition-tags="LsetTurnP" type="EXP" x="46.55" y="30.0"/>
|
||
|
|
</nodes>
|
||
|
|
<edges>
|
||
|
|
<arc head="ncsP" head-magnet="0" kind="INPUT" tail="P0" tail-magnet="0">
|
||
|
|
<point x="7.999998000000001" y="6.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P1" head-magnet="0" kind="OUTPUT" tail="ncsP" tail-magnet="0"/>
|
||
|
|
<arc broken="true" head="isTurnP" head-magnet="0" kind="INPUT" tail="TurnP" tail-magnet="0">
|
||
|
|
<point x="20.645899999999997" y="12.677051999999996"/>
|
||
|
|
<point x="-16.5661" y="-15.462060000000001"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="isTurnP" head-magnet="0" kind="INPUT" tail="P1" tail-magnet="0"/>
|
||
|
|
<arc broken="true" head="TurnP" head-magnet="0" kind="OUTPUT" tail="isTurnP" tail-magnet="0">
|
||
|
|
<point x="-14.537944" y="5.433900000000001"/>
|
||
|
|
<point x="20.382134" y="28.013310000000004"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P2" head-magnet="0" kind="OUTPUT" tail="isTurnP" tail-magnet="0"/>
|
||
|
|
<arc head="csP" head-magnet="0" kind="INPUT" tail="P2" tail-magnet="0"/>
|
||
|
|
<arc head="P3" head-magnet="0" kind="OUTPUT" tail="csP" tail-magnet="0"/>
|
||
|
|
<arc head="T11" head-magnet="0" kind="INPUT" tail="P0" tail-magnet="0">
|
||
|
|
<point x="9.499998000000001" y="5.500002"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P0" head-magnet="0" kind="OUTPUT" tail="T11" tail-magnet="0">
|
||
|
|
<point x="10.999998000000001" y="1.999998"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T011" head-magnet="0" kind="INPUT" tail="TurnP" tail-magnet="0">
|
||
|
|
<point x="21.599306" y="13.880825999999999"/>
|
||
|
|
<point x="-16.5661" y="0.537942000000001"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T011" head-magnet="0" kind="INPUT" tail="P3" tail-magnet="0"/>
|
||
|
|
<arc broken="true" head="TurnQ" head-magnet="0" kind="OUTPUT" tail="T011" tail-magnet="0">
|
||
|
|
<point x="-8.537944" y="18.433902"/>
|
||
|
|
<point x="26.657396" y="34.071737999999996"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P0" head-magnet="0" kind="OUTPUT" tail="T011" tail-magnet="0">
|
||
|
|
<point x="7.999998000000001" y="33.499998"/>
|
||
|
|
<point x="1.999998" y="32.500002"/>
|
||
|
|
<point x="1.999998" y="2.5000020000000003"/>
|
||
|
|
<point x="6.499998000000001" y="1.000002"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T01" head-magnet="0" kind="INPUT" tail="TurnQ" tail-magnet="0">
|
||
|
|
<point x="28.778087999999997" y="22.321157999999997"/>
|
||
|
|
<point x="-11.066099999999999" y="1.537944000000003"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T01" head-magnet="0" kind="INPUT" mult-x="0.500001000000001" mult-y="-0.4999980000000015" tail="P3" tail-magnet="0"/>
|
||
|
|
<arc broken="true" head="TurnQ" head-magnet="0" kind="OUTPUT" mult-x="1.755448816374134" mult-y="0.023581791367075056" tail="T01" tail-magnet="0">
|
||
|
|
<point x="19.462055999999997" y="29.433904"/>
|
||
|
|
<point x="57.72706199999999" y="45.91411599999999"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="P0" head-magnet="0" kind="OUTPUT" tail="T01" tail-magnet="0">
|
||
|
|
<point x="7.999998000000001" y="33.499998"/>
|
||
|
|
<point x="1.999998" y="32.500002"/>
|
||
|
|
<point x="1.999998" y="2.5000020000000003"/>
|
||
|
|
<point x="6.499998000000001" y="1.000002"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="ncsQ" head-magnet="0" kind="INPUT" tail="Q0" tail-magnet="0">
|
||
|
|
<point x="41.999994" y="6.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Q1" head-magnet="0" kind="OUTPUT" tail="ncsQ" tail-magnet="0"/>
|
||
|
|
<arc broken="true" head="isTurnQ" head-magnet="0" kind="INPUT" tail="TurnQ" tail-magnet="0">
|
||
|
|
<point x="19.282891999999997" y="21.504384"/>
|
||
|
|
<point x="17.433895999999997" y="-15.462060000000001"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="isTurnQ" head-magnet="0" kind="INPUT" tail="Q1" tail-magnet="0"/>
|
||
|
|
<arc broken="true" head="TurnQ" head-magnet="0" kind="OUTPUT" tail="isTurnQ" tail-magnet="0">
|
||
|
|
<point x="17.962052" y="4.433900000000001"/>
|
||
|
|
<point x="17.772937999999996" y="39.41411599999999"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Q2" head-magnet="0" kind="OUTPUT" tail="isTurnQ" tail-magnet="0"/>
|
||
|
|
<arc head="csQ" head-magnet="0" kind="INPUT" tail="Q2" tail-magnet="0"/>
|
||
|
|
<arc head="Q3" head-magnet="0" kind="OUTPUT" tail="csQ" tail-magnet="0"/>
|
||
|
|
<arc head="T1" head-magnet="0" kind="INPUT" tail="Q0" tail-magnet="0">
|
||
|
|
<point x="43.499994" y="5.500002"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Q0" head-magnet="0" kind="OUTPUT" tail="T1" tail-magnet="0">
|
||
|
|
<point x="44.999994" y="1.999998"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T02" head-magnet="0" kind="INPUT" tail="TurnQ" tail-magnet="0">
|
||
|
|
<point x="18.151652" y="25.848350000000003"/>
|
||
|
|
<point x="9.933895999999997" y="7.037942000000001"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T02" head-magnet="0" kind="INPUT" tail="Q3" tail-magnet="0"/>
|
||
|
|
<arc broken="true" head="TurnP" head-magnet="0" kind="OUTPUT" tail="T02" tail-magnet="0">
|
||
|
|
<point x="34.462052" y="12.933902000000003"/>
|
||
|
|
<point x="41.928259999999995" y="22.842608"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Q0" head-magnet="0" kind="OUTPUT" tail="T02" tail-magnet="0">
|
||
|
|
<point x="41.999994" y="33.499998"/>
|
||
|
|
<point x="35.999994" y="32.500002"/>
|
||
|
|
<point x="35.999994" y="2.5000020000000003"/>
|
||
|
|
<point x="40.499994" y="1.000002"/>
|
||
|
|
</arc>
|
||
|
|
<arc broken="true" head="T0" head-magnet="0" kind="INPUT" tail="TurnP" tail-magnet="0">
|
||
|
|
<point x="17.212310000000002" y="8.530332000000001"/>
|
||
|
|
<point x="9.933895999999997" y="0.037944000000003086"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T0" head-magnet="0" kind="INPUT" mult-x="2.9999999995311555E-6" mult-y="-1.500001000000001" tail="Q3" tail-magnet="0"/>
|
||
|
|
<arc broken="true" head="TurnP" head-magnet="0" kind="OUTPUT" tail="T0" tail-magnet="0">
|
||
|
|
<point x="39.962052" y="40.433904"/>
|
||
|
|
<point x="44.0" y="42.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Q0" head-magnet="0" kind="OUTPUT" tail="T0" tail-magnet="0">
|
||
|
|
<point x="41.999994" y="33.499998"/>
|
||
|
|
<point x="35.999994" y="32.500002"/>
|
||
|
|
<point x="35.999994" y="2.5000020000000003"/>
|
||
|
|
<point x="40.499994" y="1.000002"/>
|
||
|
|
</arc>
|
||
|
|
</edges>
|
||
|
|
</gspn>
|
||
|
|
<measures gspn-name="ProcP+ProcQ+Turn" log-uuid="3fcaeaaf-ce1c-4dcb-b7c0-0891fdd6c319" name="CTL model checking of ProcP+ProcQ+Turn" rapid-type="CTL_MODEL_CHECKING" simplified-UI="true">
|
||
|
|
<assignments/>
|
||
|
|
<rgmedd2 counter-examples="true"/>
|
||
|
|
<formulas>
|
||
|
|
<formula language="STAT"/>
|
||
|
|
<formula comment="CTL formula" expr="AG ( #P2==1 -> AF (#P3 == 1))" language="CTL">
|
||
|
|
<result-table>
|
||
|
|
<mc-result name="MEASURE0" value="false">
|
||
|
|
<bindings/>
|
||
|
|
</mc-result>
|
||
|
|
</result-table>
|
||
|
|
</formula>
|
||
|
|
</formulas>
|
||
|
|
</measures>
|
||
|
|
<resource-list>
|
||
|
|
<document-log uuid="3fcaeaaf-ce1c-4dcb-b7c0-0891fdd6c319">rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAAN50ALYbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vcGludmFyICIvaG9tZS91c2VyL3VuaXRvL1llYXJJL1NlY29uZFNlbS9WUEMvbGFicy9hbmFsaXNpLzMuMi9BbGczLTItQ1RMIG1vZGVsIGNoZWNraW5nIG9mIFByb2NQK1Byb2NRK1R1cm4uc29sdXRpb24vUHJvY1ArUHJvY1ErVHVybiIgLWRldGVjdC1leHAgCnQAAQp0AJhQbGFjZSBpbnZhcmlhbnRzIGZvciBuZXQgL2hvbWUvdXNlci91bml0by9ZZWFySS9TZWNvbmRTZW0vVlBDL2xhYnMvYW5hbGlzaS8zLjIvQWxnMy0yLUNUTCBtb2RlbCBjaGVja2luZyBvZiBQcm9jUCtQcm9jUStUdXJuLnNvbHV0aW9uL1Byb2NQK1Byb2NRK1R1cm46CnQAAQp0ABUgICBRMCAgIFExICAgUTIgICBRMwp0ABEgICBUdXJuUCAgIFR1cm5RCnQAFSAgIFAwICAgUDEgICBQMiAgIFAzCnQAAQp0ACtBTEwgcGxhY2VzIGFyZSBjb3ZlcmVkIGJ5IHNvbWUgUC1pbnZhcmlhbnQKdAABCnQAJxtbMFgbWzMybSBQUk9DRVNTIEVYSVRFRCBOT1JNQUxMWS4bWzBtCnQAtBtbMG1FWEVDOiAvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9zdHJ1Y3QgIi9ob21lL3VzZXIvdW5pdG8vWWVhckkvU2Vjb25kU2VtL1ZQQy9sYWJzL2FuYWxpc2kvMy4yL0FsZzMtMi1DVEwgbW9kZWwgY2hlY2tpbmcgb2YgUHJvY1ArUHJvY1ErVHVybi5zb2x1dGlvbi9Qcm9jUCtQcm9jUStUdXJuIiAtb25seS1ibmQgCnEAfgAMdAC7G1swbUVYRUM6IC91c3IvbG9jYWwvR3JlYXRTUE4vYmluL0RTUE4tVG9vbCAtbG9hZCAiL2hvbWUvdXNlci91bml0by9ZZWFySS9TZWNvbmRTZW0vVlBDL2xhYnMvYW5hbGlzaS8zLjIvQWxnMy0yLUNUTCBtb2RlbCBjaGVja2luZyBvZiBQcm9jUCtQcm9jUStUdXJuLnNvbHV0aW9uL1Byb2NQK1Byb2NRK1R1cm4iIC1wYmFzaXMgCnQArxtbMW0bWzRtTE9BRElORyBQRVRSSSBORVQgL2hvbWUvdXNlci91bml0by9ZZWFySS9TZWNvbmRTZW0vVlBDL2xhYnMvYW5hbGlzaS8zLjIvQWxnMy0yLUNUTCBtb2RlbCBjaGVja2luZyBvZiBQcm9jUCtQcm9jUStUdXJuLnNvbHV0aW9uL1Byb2NQK1Byb2NRK1R1cm4gKG5ldC9kZWYpLi4uG1syMm0bWzI0bQp0AA9NQVJLSU5HIFBBUjogMAp0ABBQTEFDRVM6ICAgICAgMTAKdAAPUkFURSBQQVI6ICAgIDAKdAAQVFJBTlNJVElPTlM6IDEyCnQAD01FQVNVUkVTOiAgICAwCnQAKExPQURJTkcgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0AAEKdAABCnQAHkNPTVBVVElORyBQTEFDRSBGTE9XIEJBU0lTLi4uCnQAOENvbXB1dGF0aW9uIG9mIEZsb3cgYmFzaXM6IHN0ZXAgMS8xMiwgfEt8PTgsIHByb2R1Y3RzPTEKdABTG1sxQSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAp0AFIbWzFBQ29tcHV0YXRpb24gb2YgRmxvdyBiYXNpczogY29tcGxldGVkIGluIDcgc3RlcHMsIHxLfD0zLiAgICAgICAgICAgICAgICAgICAgICAKdAApRk9VTkQgMyBWRUNUT1JTIElOIFRIRSBQTEFDRSBGTE9XIEJBU0lTLgp0AAEKdAABCnQAKEFsbCBwbGFjZXMgYXJlIGNvdmVyZWQgYnkgc29tZSBQLWZsb3dzLgp0AAEKdAAmVE9UQUwgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQpxAH4ADHQAtxtbMG1FWEVDOiAvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9SR01FREQyICIvaG9tZS91c2VyL3VuaXRvL1llYXJJL1NlY29uZFNlbS9WUEMvbGFicy9hbmFsaXNpLzMuMi9BbGczLTItQ1RMIG1vZGVsIGNoZWNraW5nIG9mIFByb2NQK1Byb2NRK1R1cm4uc29sdXRpb24vUHJvY1ArUHJvY1ErVHVybiIgLU1FVEEgIC1jIC1DCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAAnVVNFIDogIFJHTUVERDIgIDxuZXRuYW1lPiBbb3B0aW9ucy4uLl0KdAABCnQAFU9wdGlvbnMgZGVzY3JpcHRpb246CnQAKiAgLUMgICAgICAgICAgIGVuYWJsZSBDVEwgbW9kZWwgY2hlY2tpbmcuCnQASiAgLWMgICAgICAgICAgIHByaW50IGNvdW50ZXItZXhhbXBsZXMgYW5kIHdpdG5lc3NlcyBvZiBlYWNoIENUTCBmb3JtdWxhcy4KdAA6ICAtaCAgICAgICAgICAgc3BlY2lmeSB0aGUgTWVkZGx5IGNhY2hlIHNpemUsIGluIGVudHJpZXMuCnQAOiAgLWYgICAgICAgICAgIHNwZWNpZnkgdGhlIGZpbGUgY29udGFpbmluZyBDVEwgZm9ybXVsYWUuIAp0ADUgIC1tb25vLW5zZiAgICBVc2UgbW9ub2xpdGhpYyBOU0YgZm9yIFJTIGdlbmVyYXRpb24uCnQAQyAgLWV2ZW50LW5zZiAgIFVzZSBwZXItZXZlbnQgUlMgZ2VuZXJhdGlvbiAoc2F0LXByZWdlbikuIFtkZWZhdWx0XQp0AD8gIC1tcGFyIDxtcGFyPiA8dmFsPiAgQ2hhbmdlIHRoZSB2YWx1ZSBvZiBhIG1hcmtpbmcgcGFyYW1ldGVyLgp0ADwgIC1ycGFyIDxycGFyPiA8dmFsPiAgQ2hhbmdlIHRoZSB2YWx1ZSBvZiBhIHJhdGUgcGFyYW1ldGVyLgp0AE8gIC1vICAgICAgICAgICBTYXZlIFJTIGFuZCBDVEwgcmVzdWx0cyBvbiBhIGZpbGUgKDxuZXRuYW1lPi5ycyBhbmQgLmN0bG91dHB1dCkKdABBICAtdmFyb3JkKC1vbmx5KSAgUHJpbnQgdmFyaWFibGUgb3JkZXJpbmcgKGFuZCBvcHRpb25hbGx5IHF1aXQpLgp0AEAgIC1tZXRyaWNzKC1vbmx5KSBQcmludCBvcmRlcmluZyBtZXRyaWNzIChhbmQgb3B0aW9uYWxseSBxdWl0KS4KdAA+ICAtb3JkZXItaW1hZ2UgU2F2ZSBhIGJpdG1hcCByZXByZXNlbnRpbmcgdGhlIHZhcmlhYmxlIG9yZGVyLgp0AAEKdAAkQXZhaWxhYmxlIHZhcmlhYmxlIG9yZGVyIGhldXJpc3RpYzoKdABHICAtRiAgICAgICAgICAgUmVhZCB0aGUgdmFyaWFibGUgb3JkZXIgZnJvbSB0aGUgPG5ldG5hbWU+LnBsYWNlIGZpbGUuIAp0AEMgIC1QICAgICAgICAgICBEZXJpdmUgb3JkZXIgdXNpbmcgdGhlIFAtc2VtaWZsb3dzIGNoYWluaW5nIG1ldGhvZC4KdAAtICAtRlIgICAgICAgICAgVXNlIHN0YW5kYXJkIEZPUkNFIGFsZ29yaXRobS4KdAA1I
|
||
|
|
</resource-list>
|
||
|
|
</project>
|