126 lines
25 KiB
Text
126 lines
25 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="New project" version="121">
|
||
|
|
<gspn name="PT" show-color-cmd="false" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false" zoom="125">
|
||
|
|
<nodes>
|
||
|
|
<place label-x="3.5" label-y="-0.5" marking="1" name="Await_P" x="10.0" y="5.0"/>
|
||
|
|
<place label-y="-2.0" name="Done_P" x="10.0" y="15.0"/>
|
||
|
|
<place label-x="2.0" label-y="2.0" marking="1" name="Turn_P" x="17.0" y="7.0"/>
|
||
|
|
<place label-x="2.0" label-y="2.0" name="Turn_Q" x="19.0" y="16.0"/>
|
||
|
|
<transition name="T0" nservers-x="0.5" type="EXP" x="10.55" y="10.0"/>
|
||
|
|
<transition name="T1" nservers-x="0.5" rotation="-0.0" type="EXP" x="10.55" y="19.0"/>
|
||
|
|
<transition name="T2" nservers-x="0.5" type="EXP" x="10.55" y="1.0"/>
|
||
|
|
<place label-x="3.0" label-y="0.5" marking="1" name="Await_Q" x="28.0" y="19.0"/>
|
||
|
|
<transition name="T3" nservers-x="0.5" type="EXP" x="28.55" y="24.0"/>
|
||
|
|
<transition name="T4" nservers-x="0.5" type="EXP" x="28.55" y="14.0"/>
|
||
|
|
<place label-x="3.5" label-y="0.0" name="Done_Q" x="28.0" y="9.0"/>
|
||
|
|
<transition name="T5" nservers-x="0.5" type="EXP" x="28.55" y="5.0"/>
|
||
|
|
</nodes>
|
||
|
|
<edges>
|
||
|
|
<arc head="T0" kind="INPUT" tail="Await_P">
|
||
|
|
<point x="7.5" y="8.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Done_P" kind="OUTPUT" tail="T0">
|
||
|
|
<point x="8.0" y="13.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T0" kind="INPUT" tail="Turn_P"/>
|
||
|
|
<arc head="T1" kind="INPUT" tail="Done_P">
|
||
|
|
<point x="8.5" y="18.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Await_P" kind="OUTPUT" tail="T1">
|
||
|
|
<point x="6.5" y="20.0"/>
|
||
|
|
<point x="6.5" y="6.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Turn_Q" kind="OUTPUT" tail="T1">
|
||
|
|
<point x="18.0" y="20.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T2" kind="INPUT" tail="Await_P">
|
||
|
|
<point x="8.5" y="3.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Await_P" kind="OUTPUT" tail="T2">
|
||
|
|
<point x="13.0" y="3.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T3" kind="INPUT" tail="Await_Q">
|
||
|
|
<point x="26.5" y="23.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Await_Q" kind="OUTPUT" tail="T3">
|
||
|
|
<point x="31.0" y="23.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T4" kind="INPUT" tail="Await_Q">
|
||
|
|
<point x="32.0" y="17.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Done_Q" kind="OUTPUT" tail="T4">
|
||
|
|
<point x="32.0" y="12.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T5" kind="INPUT" tail="Done_Q">
|
||
|
|
<point x="32.0" y="7.5"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Turn_P" kind="OUTPUT" tail="T5"/>
|
||
|
|
<arc head="T4" kind="INPUT" tail="Turn_Q"/>
|
||
|
|
<arc head="Turn_Q" kind="OUTPUT" tail="T4">
|
||
|
|
<point x="24.0" y="15.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="Turn_P" kind="OUTPUT" tail="T0">
|
||
|
|
<point x="15.5" y="11.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T5" kind="INPUT" mult-k="2.6563476562500004" tail="Turn_Q">
|
||
|
|
<point x="20.5" y="15.0"/>
|
||
|
|
<point x="27.0" y="13.5"/>
|
||
|
|
<point x="26.5" y="9.0"/>
|
||
|
|
</arc>
|
||
|
|
<arc head="T1" kind="INPUT" tail="Turn_P">
|
||
|
|
<point x="13.5" y="14.5"/>
|
||
|
|
<point x="13.5" y="18.5"/>
|
||
|
|
</arc>
|
||
|
|
</edges>
|
||
|
|
</gspn>
|
||
|
|
<measures gspn-name="PT" log-uuid="d1dae8a9-a12d-40c6-bd80-ab683db44be6" name="Measures" simplified-UI="false">
|
||
|
|
<assignments/>
|
||
|
|
<rgmedd2/>
|
||
|
|
<formulas>
|
||
|
|
<formula comment="Basic statistics of the toolchain execution." language="STAT">
|
||
|
|
<result-table>
|
||
|
|
<stat-result name="STAT">
|
||
|
|
<bindings/>
|
||
|
|
<stat key="CTL_time" value="0.00226 seconds."/>
|
||
|
|
<stat key="build_time" value="0.000929 seconds."/>
|
||
|
|
<stat key="num_rs_nodes" value="11"/>
|
||
|
|
<stat key="num_tangible_markings" value="7"/>
|
||
|
|
<stat key="total_firings" value="unknown"/>
|
||
|
|
</stat-result>
|
||
|
|
</result-table>
|
||
|
|
</formula>
|
||
|
|
<formula expr="AG(!(#Done_P == 1) || !(#Done_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 (#Done_P == 1 || #Done_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 (#Done_P == 1))" language="CTL">
|
||
|
|
<result-table>
|
||
|
|
<mc-result name="MEASURE3" value="false">
|
||
|
|
<bindings/>
|
||
|
|
</mc-result>
|
||
|
|
</result-table>
|
||
|
|
</formula>
|
||
|
|
<formula expr="AG ((#Await_Q==1 ) -> AF (#Done_Q == 1))" language="CTL">
|
||
|
|
<result-table>
|
||
|
|
<mc-result name="MEASURE4" value="false">
|
||
|
|
<bindings/>
|
||
|
|
</mc-result>
|
||
|
|
</result-table>
|
||
|
|
</formula>
|
||
|
|
</formulas>
|
||
|
|
</measures>
|
||
|
|
<resource-list>
|
||
|
|
<document-log uuid="d1dae8a9-a12d-40c6-bd80-ab683db44be6">rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAATJ0AJMbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vRFNQTi1Ub29sIC1sb2FkICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNS1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLXBiYXNpcyAtZGV0ZWN0LWV4cCAtcHNmbCAtYm5kIAp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy41LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAPUExBQ0VTOiAgICAgIDYKdAAPUkFURSBQQVI6ICAgIDAKdAAPVFJBTlNJVElPTlM6IDYKdAAPTUVBU1VSRVM6ICAgIDAKdAAoTE9BRElORyBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQAAQp0AAEKdAAeQ09NUFVUSU5HIFBMQUNFIEZMT1cgQkFTSVMuLi4KdAAPTT02LCBOPTYsIE4wPTYKdAA3Q29tcHV0YXRpb24gb2YgRmxvdyBiYXNpczogc3RlcCAxLzYsIHxLfD00LCBwcm9kdWN0cz0xCnQAUxtbMUEgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAKdABSG1sxQUNvbXB1dGF0aW9uIG9mIEZsb3cgYmFzaXM6IGNvbXBsZXRlZCBpbiA0IHN0ZXBzLCB8S3w9Mi4gICAgICAgICAgICAgICAgICAgICAgCnQAKUZPVU5EIDIgVkVDVE9SUyBJTiBUSEUgUExBQ0UgRkxPVyBCQVNJUy4KdAABCnQAAQp0AC5UaGVyZSBhcmUgMiBwbGFjZXMgbm90IGNvdmVyZWQgYnkgYW55IFAtZmxvdzoKdAABCnQAJlRPVEFMIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAAnQVZPSUQgRVhQT05FTlRJQUwgR1JPV1RIIE9GIFNFTUlGTE9XUy4KdAAdQ09NUFVUSU5HIFBMQUNFIFNFTUlGTE9XUy4uLgp0AA9NPTYsIE49NiwgTjA9Ngp0AClHZW5lcmF0aW9uIG9mIFNlbWlmbG93czogc3RlcCAxLzYsIHxLfD00CnQAUxtbMUEgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAKdABQG1sxQUdlbmVyYXRpb24gb2YgU2VtaWZsb3dzOiBjb21wbGV0ZWQgaW4gNCBzdGVwcywgfEt8PTIuICAgICAgICAgICAgICAgICAgICAgIAp0ABlGT1VORCAyIFBMQUNFIFNFTUlGTE9XUy4KdAABCnQAAQp0ADJUaGVyZSBhcmUgMiBwbGFjZXMgbm90IGNvdmVyZWQgYnkgYW55IFAtc2VtaWZsb3c6CnQAAQp0ACZUT1RBTCBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQALENPTVBVVElORyBQTEFDRSBCT1VORFMgRlJPTSBQLVNFTUlGTE9XUyAuLi4KdAAnG1swWBtbMzJtIFBST0NFU1MgRVhJVEVEIE5PUk1BTExZLhtbMG0KdACkG1swbUVYRUM6IHBlcmwgLWUgJ2FsYXJtIDUgOyBleGVjICIvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9EU1BOLVRvb2wgLWxvYWQgXCIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNS1NZWFzdXJlcy5zb2x1dGlvbi9QVFwiIC1sb2FkLWJuZCAtaWxwLWJuZCIgJwp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy41LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAPUExBQ0VTOiAgICAgIDYKdAAPUkFURSBQQVI6ICAgIDAKdAAPVFJBTlNJVElPTlM6IDYKdAAPTUVBU1VSRVM6ICAgIDAKdAAoTE9BRElORyBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQAAQp0AAEKdAAVTE9BRElORyBCTkQgRklMRSAuLi4KdAAlQ09NUFVUSU5HIFBMQUNFIEJPVU5EUyBVU0lORyBJTFAgLi4uCnQAGEFsbCBwbGFjZXMgYXJlIGJvdW5kZWQuCnEAfgAkdAB/G1swbUVYRUM6IC91c3IvbG9jYWwvR3JlYXRTUE4vYmluL1JHTUVERDMgIi9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy41LU1lYXN1cmVzLnNvbHV0aW9uL1BUIiAtTUVUQSAgLWd1aS1zdGF0IC1DCnQAIFJhbmRvbSBzZWVkczogMTU4ODg2MTM4NyAxMjU3NTgKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0ABFHcmVhdFNQTi9NZWRkbHkuCnQAOCAgQ29weXJpZ2h0IChDKSAxOTg3LTIwMTgsIFVuaXZlcnNpdHkgb2YgVG9yaW5vLCBJdGFseS4KdAAxICBTZW5kIGZpbGVzIG5ldG5hbWUubmV0LCAuZGVmIHRvIGUtbWFpbCBhZGRyZXNzCnQAKyAgYmVjY3V0aUBkaS51bml0by5pdCBpZiB5b3UgZmluZCBhbnkgYnVnLgp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAH0Jhc2VkIG9uIE1FRERMWSB2ZXJzaW9uIDAuMTYuMAp0AEYgIENvcHlyaWdodCAoQykgMjAwOSwgSW93YSBTdGF0ZSBVbml2ZXJzaXR5IFJlc2VhcmNoIEZvdW5kYXRpb24sIEluYy4KdAApICB3ZWJzaXRlOiBodHRwOi8vbWVkZGx5LnNvdXJjZWZvcmdlLm5ldAp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAKVVzaW5nIHBlci1ldmVudCBzYXR1cmF0aW9uIChzYXQtcHJlZ2VuKS4KdAAbVXNpbmcgZmFzdCBOU0YgZ2VuZXJhdGlvbi4KdAARUHJvY2VzcyBJRDogMTMxMgp0AEtNT0RFTCBOQU1FOiAvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuNS1NZWFzdXJlcy5zb2x1dGlvbi9QVAp0ABsgIDYgcGxhY2VzLCA2IHRyYW5zaXRpb25zLgp0ACdVc2VkIE1lbW9yeSBmb3IgZW5jb2RpbmcgbmV0OiAzOTI1MjRLQgp0AFVPcGVuaW5nIGZpbGU6IC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy41LU1lYXN1cmVzLnNvbHV0aW9uL1BULmJuZCBPSy4KdABYT3BlbmluZyBmaWxlOiAvaG9tZS91c
|
||
|
|
</resource-list>
|
||
|
|
</project>
|