UniTO/anno3/vpc/consegne/3/3.9.PNPRO

224 lines
23 KiB
Text
Raw Permalink Normal View History

2020-05-08 19:23:51 +02:00
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="3.9" version="121">
<gspn name="PT" show-color-cmd="false" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false" zoom="75">
<nodes>
<place label-x="3.0" label-y="0.0" marking="1" name="local_P" x="19.0" y="9.0"/>
<place label-x="3.0" label-y="0.0" name="setTrue_P" x="19.0" y="17.0"/>
<place label-x="4.0" label-y="1.0" name="critical_P" x="19.0" y="38.0"/>
<place label-x="3.0" label-y="0.5" name="setFalse_P" x="19.0" y="45.0"/>
<place marking="1" name="wantP_FALSE" x="46.0" y="45.0"/>
<place label-x="5.0" label-y="0.0" name="wantP_TRUE" x="27.0" y="44.0"/>
<transition name="T0" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="19.55" y="13.0"/>
<transition label-y="2.0" name="reset_transition" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="19.55" y="48.0"/>
<transition name="T3" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="19.55" y="41.0"/>
<transition name="T2" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="19.55" y="22.0"/>
<transition name="T00" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="11.55" y="7.0"/>
<place name="While" x="19.0" y="26.0"/>
<transition name="T1" nservers-x="0.5" rotation="5.759586531581287" type="EXP" x="5.55" y="30.0"/>
<transition name="T4" nservers-x="0.5" rotation="1.0471975511965979" type="EXP" x="29.55" y="29.0"/>
<place name="P0" x="23.0" y="31.0"/>
<transition name="T5" nservers-x="0.5" type="EXP" x="19.55" y="33.0"/>
<place marking="1" name="wantQ_FALSE" x="44.0" y="16.0"/>
<place name="wantQ_TRUE" x="46.0" y="28.0"/>
<place label-x="3.0" label-y="0.0" marking="1" name="local_Q" x="64.0" y="8.0"/>
<place label-x="4.5" label-y="0.0" name="setTrue_Q" x="64.0" y="16.0"/>
<place label-x="4.0" label-y="1.0" name="critical_Q" x="64.0" y="37.0"/>
<place label-x="3.0" label-y="0.5" name="setFalse_Q" x="64.0" y="44.0"/>
<transition name="T15" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="64.55" y="12.0"/>
<transition label-y="2.0" name="reset_Transition" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="64.55" y="47.0"/>
<transition name="T9" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="64.55" y="40.0"/>
<transition name="T12" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="64.55" y="21.0"/>
<transition name="T100" nservers-x="0.5" rotation="1.5707963267948966" type="EXP" x="56.55" y="6.0"/>
<place label-x="1.5" label-y="2.0" name="While_" x="64.0" y="25.0"/>
<transition name="T11" nservers-x="0.5" type="EXP" x="64.55" y="32.0"/>
<transition label-x="-8.0" label-y="-22.0" name="T6" nservers-x="0.5" rotation="5.497787143782139" type="EXP" x="55.55" y="29.0"/>
<place name="P1" x="52.0" y="37.0"/>
<transition name="T7" nservers-x="0.5" type="EXP" x="78.55" y="30.0"/>
</nodes>
<edges>
<arc head="T0" kind="INPUT" tail="local_P"/>
<arc head="T00" kind="INPUT" tail="local_P">
<point x="16.5" y="7.5"/>
</arc>
<arc head="local_P" kind="OUTPUT" tail="T00"/>
<arc head="T2" kind="INPUT" tail="setTrue_P"/>
<arc head="T3" kind="INPUT" tail="critical_P"/>
<arc head="setFalse_P" kind="OUTPUT" tail="T3"/>
<arc head="reset_transition" kind="INPUT" tail="setFalse_P">
<point x="20.0" y="47.5"/>
</arc>
<arc broken="true" head="local_P" kind="OUTPUT" mult-k="0.81396484375" tail="reset_transition">
<point x="4.5" y="49.0"/>
<point x="4.5" y="10.0"/>
</arc>
<arc head="wantP_FALSE" kind="OUTPUT" mult-k="0.8772460937500001" tail="reset_transition">
<point x="35.0" y="49.0"/>
</arc>
<arc head="reset_transition" kind="INPUT" tail="wantP_TRUE"/>
<arc broken="true" head="wantP_TRUE" kind="OUTPUT" mult-k="1.25830078125" tail="T2">
<point x="14.0" y="24.0"/>
</arc>
<arc broken="true" head="T2" kind="INPUT" mult-k="0.8180664062500002" tail="wantP_FALSE">
<point x="27.0" y="22.0"/>
</arc>
<arc head="setTrue_P" kind="OUTPUT" tail="T0"/>
<arc head="While" kind="OUTPUT" tail="T2"/>
<arc head="T4" kind="INPUT" tail="While"/>
<arc broken="true" head="T4" kind="INPUT" tail="wantP_TRUE">
<point x="50.5" y="21.5"/>
</arc>
<arc head="P0" kind="OUTPUT" tail="T4"/>
<arc head="T5" kind="INPUT" tail="P0"/>
<arc head="While" kind="OUTPUT" tail="T5"/>
<arc broken="true" head="wantP_TRUE" kind="OUTPUT" tail="T5">
<point x="3.0" y="36.5"/>
<point x="2.0" y="55.5"/>
<point x="46.5" y="54.5"/>
</arc>
<arc broken="true" head="wantP_FALSE" kind="OUTPUT" tail="T4">
<point x="38.5" y="34.0"/>
<point x="50.0" y="44.5"/>
</arc>
<arc head="T1" kind="INPUT" tail="While"/>
<arc head="critical_P" kind="OUTPUT" mult-k="2.1618164062499994" tail="T1">
<point x="9.0" y="38.0"/>
<point x="11.5" y="39.5"/>
</arc>
<arc broken="true" head="T4" kind="INPUT" tail="wantQ_TRUE">
<point x="35.5" y="19.5"/>
<point x="26.5" y="21.5"/>
</arc>
<arc broken="true" head="wantQ_TRUE" kind="OUTPUT" tail="T4">
<point x="19.5" y="39.5"/>
<point x="28.0" y="38.0"/>
</arc>
<arc broken="true" head="T1" kind="INPUT" tail="wantQ_FALSE">
<point x="15.0" y="17.5"/>
</arc>
<arc broken="true" head="wantQ_FALSE" kind="OUTPUT" tail="T1">
<point x="3.5" y="33.5"/>
</arc>
<arc broken="true" head="T5" kind="INPUT" mult-k="0.7194335937500002" mult-x="0.1373107910156257" mult-y="1.8943603515624972" tail="wantP_FALSE">
<point x="24.5" y="37.5"/>
</arc>
<arc head="T15" kind="INPUT" tail="local_Q"/>
<arc head="T100" kind="INPUT" tail="local_Q">
<point x="61.5" y="6.5"/>
</arc>
<arc head="local_Q" kind="OUTPUT" tail="T100"/>
<arc head="T12" kind="INPUT" tail="setTrue_Q"/>
<arc head="T9" kind="INPUT" tail="critical_Q"/>
<arc head="setFalse_Q" kind="OUTPUT" tail="T9"/>
<arc head="reset_Transition" kind="INPUT" tail="setFalse_Q">
<point x="65.0" y="46.5"/>
</arc>
<arc broken="true" head="local_Q" kind="OUTPUT" mult-k="0.81396484375" tail="reset_Transition">
<point x="45.0" y="48.0"/>
<point x="45.0" y="9.0"/>
</arc>
<arc head="setTrue_Q" kind="OUTPUT" tail="T15"/>
<arc head="While_" kind="OUTPUT" tail="T12"/>
<arc head="While_" kind="OUTPUT" tail="T11"/>
<arc head="P1" kind="OUTPUT" tail="T6"/>
<arc head="T11" kind="INPUT" mult-k="0.9971679687499999" tail="P1">
<point x="65.0" y="35.5"/>
</arc>
<arc head="T6" kind="INPUT" tail="While_"/>
<arc broken="true" head="T6" kind="INPUT" tail="wantP_TRUE">
<point x="55.5" y="24.5"/>
</arc>
<arc broken="true" head="wantP_TRUE" kind="OUTPUT" tail="T6">
<point x="60.0" y="30.0"/>
<point x="60.0" y="44.0"/>
</arc>
<arc head="wantQ_FALSE" kind="OUTPUT" tail="T6"/>
<arc head="T6" kind="INPUT" tail="wantQ_TRUE"/>
<arc broken="true" head="wantQ_TRUE" kind="OUTPUT" tail="T11">
<point x="74.5" y="35.5"/>
<point x="55.5" y="41.0"/>
</arc>
<arc broken="true" head="T11" kind="INPUT" mult-k="0.5958007812500001" tail="wantQ_FALSE">
<point x="60.5" y="37.5"/>
<point x="61.552734375" y="33.0421875"/>
</arc>
<arc head="T7" kind="INPUT" tail="While_"/>
<arc head="critical_Q" kind="OUTPUT" tail="T7">
<point x="79.0" y="38.0"/>
</arc>
<arc broken="true" head="T7" kind="INPUT" tail="wantP_FALSE">
<point x="38.0" y="24.0"/>
<point x="79.0" y="19.5"/>
</arc>
<arc broken="true" head="wantP_FALSE" kind="OUTPUT" tail="T7">
<point x="81.0" y="31.0"/>
<point x="80.5" y="54.0"/>
<point x="66.0" y="55.0"/>
<point x="43.5" y="54.5"/>
</arc>
<arc broken="true" head="T12" kind="INPUT" tail="wantQ_FALSE"/>
<arc broken="true" head="wantQ_TRUE" kind="OUTPUT" tail="T12">
<point x="82.0" y="22.0"/>
<point x="84.0" y="50.0"/>
<point x="58.5" y="51.5"/>
<point x="57.5" y="51.0"/>
</arc>
</edges>
</gspn>
<measures gspn-name="PT" log-uuid="6f805270-eebf-4e60-9f63-b0460bdc2145" name="Measures" simplified-UI="false">
<assignments/>
<rgmedd2 counter-examples="true"/>
<formulas>
<formula comment="Basic statistics of the toolchain execution." language="STAT">
<result-table>
<stat-result name="STAT">
<bindings/>
<stat key="CTL_time" value="0.007783 seconds."/>
<stat key="build_time" value="0.001285 seconds."/>
<stat key="num_rs_nodes" value="47"/>
<stat key="num_tangible_markings" value="37"/>
<stat key="total_firings" value="unknown"/>
</stat-result>
</result-table>
</formula>
<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 ((#setTrue_P==1 || #setTrue_Q == 1) -&gt; AF (#critical_P == 1 || #critical_Q == 1)) " language="CTL">
<result-table>
<mc-result name="MEASURE0" value="false">
<bindings/>
</mc-result>
</result-table>
</formula>
<formula expr="AG(#setTrue_P == 1 -&gt; EF(#critical_Q==1 || #critical_P == 1))" language="CTL">
<result-table>
<mc-result name="MEASURE3" value="false">
<bindings/>
</mc-result>
</result-table>
</formula>
<formula expr="AG (#setTrue_P ==1 -&gt; AF (#critical_P == 1))" language="CTL">
<result-table>
<mc-result name="MEASURE4" value="false">
<bindings/>
</mc-result>
</result-table>
</formula>
<formula expr="AG (#setTrue_Q==1 -&gt; AF (#critical_Q == 1))" language="CTL">
<result-table>
<mc-result name="MEASURE0" value="false">
<bindings/>
</mc-result>
</result-table>
</formula>
</formulas>
</measures>
<resource-list>
<document-log uuid="6f805270-eebf-4e60-9f63-b0460bdc2145">rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAAMF0AJMbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vRFNQTi1Ub29sIC1sb2FkICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuOS1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLXBiYXNpcyAtZGV0ZWN0LWV4cCAtcHNmbCAtYm5kIAp0AHAbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy45LU1lYXN1cmVzLnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDAKdAAQUExBQ0VTOiAgICAgIDE2CnQAD1JBVEUgUEFSOiAgICAwCnQAEFRSQU5TSVRJT05TOiAxNgp0AA9NRUFTVVJFUzogICAgMAp0AChMT0FESU5HIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAABCnQAAQp0AB5DT01QVVRJTkcgUExBQ0UgRkxPVyBCQVNJUy4uLgp0ABJNPTE2LCBOPTE2LCBOMD0xNgp0ADlDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBzdGVwIDEvMTYsIHxLfD0xNCwgcHJvZHVjdHM9MQp0AFMbWzFBICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgCnQAUxtbMUFDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBjb21wbGV0ZWQgaW4gMTEgc3RlcHMsIHxLfD01LiAgICAgICAgICAgICAgICAgICAgICAKdABARk9VTkQgNSBWRUNUT1JTIElOIFRIRSBQTEFDRSBGTE9XIEJBU0lTICg0IHNlbWlmbG93cywgMSBmbG93cykuCnQAAQp0AAEKdAAnQWxsIHBsYWNlcyBhcmUgY292ZXJlZCBieSBzb21lIFAtZmxvdy4KdAABCnQAJlRPVEFMIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAAnQVZPSUQgRVhQT05FTlRJQUwgR1JPV1RIIE9GIFNFTUlGTE9XUy4KdAAdQ09NUFVUSU5HIFBMQUNFIFNFTUlGTE9XUy4uLgp0ABJNPTE2LCBOPTE2LCBOMD0xNgp0ACtHZW5lcmF0aW9uIG9mIFNlbWlmbG93czogc3RlcCAxLzE2LCB8S3w9MTQKdABTG1sxQSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAp0AFEbWzFBR2VuZXJhdGlvbiBvZiBTZW1pZmxvd3M6IGNvbXBsZXRlZCBpbiAxMSBzdGVwcywgfEt8PTYuICAgICAgICAgICAgICAgICAgICAgIAp0ABlGT1VORCA2IFBMQUNFIFNFTUlGTE9XUy4KdAABCnQAAQp0ACtBbGwgcGxhY2VzIGFyZSBjb3ZlcmVkIGJ5IHNvbWUgUC1zZW1pZmxvdy4KdAABCnQAJlRPVEFMIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAAsQ09NUFVUSU5HIFBMQUNFIEJPVU5EUyBGUk9NIFAtU0VNSUZMT1dTIC4uLgp0ACcbWzBYG1szMm0gUFJPQ0VTUyBFWElURUQgTk9STUFMTFkuG1swbQp0AKQbWzBtRVhFQzogcGVybCAtZSAnYWxhcm0gNSA7IGV4ZWMgIi91c3IvbG9jYWwvR3JlYXRTUE4vYmluL0RTUE4tVG9vbCAtbG9hZCBcIi9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy45LU1lYXN1cmVzLnNvbHV0aW9uL1BUXCIgLWxvYWQtYm5kIC1pbHAtYm5kIiAnCnQAcBtbMW0bWzRtTE9BRElORyBQRVRSSSBORVQgL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjktTWVhc3VyZXMuc29sdXRpb24vUFQgKG5ldC9kZWYpLi4uG1syMm0bWzI0bQp0AA9NQVJLSU5HIFBBUjogMAp0ABBQTEFDRVM6ICAgICAgMTYKdAAPUkFURSBQQVI6ICAgIDAKdAAQVFJBTlNJVElPTlM6IDE2CnQAD01FQVNVUkVTOiAgICAwCnQAKExPQURJTkcgVElNRTogW1VzZXIgMC4wMDBzLCBTeXMgMC4wMDBzXQp0AAEKdAABCnQAFUxPQURJTkcgQk5EIEZJTEUgLi4uCnQAJUNPTVBVVElORyBQTEFDRSBCT1VORFMgVVNJTkcgSUxQIC4uLgp0ABhBbGwgcGxhY2VzIGFyZSBib3VuZGVkLgpxAH4AJHQAeBtbMG1FWEVDOiAvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9SR01FREQzICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8zLzMuOS1NZWFzdXJlcy5zb2x1dGlvbi9QVCIgLU1FVEEgIC1jIC1DCnQAIFJhbmRvbSBzZWVkczogMTU4ODk1ODU4MSAyMDE5ODYKdABQPT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PQp0ABFHcmVhdFNQTi9NZWRkbHkuCnQAOCAgQ29weXJpZ2h0IChDKSAxOTg3LTIwMTgsIFVuaXZlcnNpdHkgb2YgVG9yaW5vLCBJdGFseS4KdAAxICBTZW5kIGZpbGVzIG5ldG5hbWUubmV0LCAuZGVmIHRvIGUtbWFpbCBhZGRyZXNzCnQAKyAgYmVjY3V0aUBkaS51bml0by5pdCBpZiB5b3UgZmluZCBhbnkgYnVnLgp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAH0Jhc2VkIG9uIE1FRERMWSB2ZXJzaW9uIDAuMTYuMAp0AEYgIENvcHlyaWdodCAoQykgMjAwOSwgSW93YSBTdGF0ZSBVbml2ZXJzaXR5IFJlc2VhcmNoIEZvdW5kYXRpb24sIEluYy4KdAApICB3ZWJzaXRlOiBodHRwOi8vbWVkZGx5LnNvdXJjZWZvcmdlLm5ldAp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAKVVzaW5nIHBlci1ldmVudCBzYXR1cmF0aW9uIChzYXQtcHJlZ2VuKS4KdAAbVXNpbmcgZmFzdCBOU0YgZ2VuZXJhdGlvbi4KdAASUHJvY2VzcyBJRDogMjUwMzcKdABLTU9ERUwgTkFNRTogL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMy8zLjktTWVhc3VyZXMuc29sdXRpb24vUFQKdAAdICAxNiBwbGFjZXMsIDE2IHRyYW5zaXRpb25zLgp0ACdVc2VkIE1lbW9yeSBmb3IgZW5jb2RpbmcgbmV0OiA0NTUxNDBLQgp0AFVPcGVuaW5nIGZpbGU6IC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzMvMy45LU1lYXN1cmVzLnNvbHV0aW9uL1BULmJuZCBPSy4KdABYT
</resource-list>
</project>