UniTO/anno3/vpc/consegne/2/gspn/Es2B.PNPRO

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="Es2B" version="121">
  <gspn name="PT" show-color-cmd="false" show-fluid-cmd="false" show-timed-cmd="false" view-rates="false">
    <nodes>
      <place marking="r1" name="S0" x="17.0" y="6.0"/>
      <transition label-x="-5.0" label-y="0.0" name="Inizio_Servizio_s" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="17.55" y="11.0"/>
      <place label-x="2.5" label-y="0.0" name="S1_a" x="11.0" y="15.0"/>
      <place label-x="-2.0" label-y="0.0" name="S1_b" x="23.0" y="15.0"/>
      <transition label-x="4.0" name="azione_locale_sa" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="11.55" y="19.0"/>
      <transition label-x="-4.0" label-y="1.5" name="azione_locale_sb" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="23.55" y="19.0"/>
      <place label-x="2.5" label-y="0.0" name="S2_a" x="11.0" y="23.0"/>
      <place label-x="-2.5" label-y="0.0" name="S2_b" x="23.0" y="23.0"/>
      <transition label-x="-4.0" label-y="0.0" name="Fine_Servizio_s" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="17.55" y="28.0"/>
      <transition name="Reset_S" nservers-x="0.5" type="EXP" x="8.55" y="32.0"/>
      <place name="S3" x="17.0" y="32.0"/>
      <place marking="r2" name="R0" x="38.0" y="6.0"/>
      <place name="R1" x="38.0" y="15.0"/>
      <place name="R2" x="38.0" y="23.0"/>
      <place name="R3" x="38.0" y="32.0"/>
      <transition label-x="4.5" label-y="1.0" name="Inizio_Servizio_R" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="38.55" y="11.0"/>
      <transition label-x="3.5" label-y="1.5" name="Azione_locale_R" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="38.55" y="19.0"/>
      <transition label-x="3.5" label-y="1.5" name="Fine_Servizio_R" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="38.55" y="28.0"/>
      <transition name="Reset_R" nservers-x="0.5" rotation="6.283185307179586" type="EXP" x="31.55" y="32.0"/>
      <place label-x="-2.0" label-y="-1.0" marking="n" name="M0" x="71.0" y="6.0"/>
      <place name="M1" x="71.0" y="14.0"/>
      <transition label-y="-2.0" name="azione_locale_m" nservers-x="0.5" type="EXP" x="71.55" y="10.0"/>
      <transition name="Richiesta_Servizio" nservers-x="0.5" type="EXP" x="66.55" y="14.0"/>
      <transition label-x="-5.0" name="Attesa_Elaborazione" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="71.55" y="25.0"/>
      <place label-y="-1.5" name="M2" x="71.0" y="19.0"/>
      <place label-x="-1.5" name="M3" x="71.0" y="28.0"/>
      <transition name="Reset_M" nservers-x="0.5" rotation="4.71238898038469" type="EXP" x="77.55" y="19.0"/>
      <place name="Freechoice" x="57.0" y="14.0"/>
      <transition name="Scelta_1" nservers-x="0.5" type="EXP" x="49.55" y="3.0"/>
      <transition name="Scelta_2" nservers-x="0.5" type="EXP" x="49.55" y="9.0"/>
      <place name="P0" x="46.0" y="9.0"/>
      <place name="P1" x="46.0" y="3.0"/>
      <place label-x="-3.0" label-y="0.0" name="Risultato" x="57.0" y="25.0"/>
      <template last-binding="2" name="n" type="INTEGER" x="67.0" y="38.0"/>
      <template last-binding="1" name="r1" type="INTEGER" x="72.0" y="38.0"/>
      <template last-binding="1" name="r2" type="INTEGER" x="76.0" y="38.0"/>
    </nodes>
    <edges>
      <arc head="Inizio_Servizio_s" kind="INPUT" tail="S0"/>
      <arc head="S1_a" kind="OUTPUT" tail="Inizio_Servizio_s"/>
      <arc head="S1_b" kind="OUTPUT" tail="Inizio_Servizio_s"/>
      <arc head="azione_locale_sb" kind="INPUT" tail="S1_b"/>
      <arc head="azione_locale_sa" kind="INPUT" tail="S1_a"/>
      <arc head="S2_a" kind="OUTPUT" tail="azione_locale_sa"/>
      <arc head="S2_b" kind="OUTPUT" tail="azione_locale_sb"/>
      <arc head="Fine_Servizio_s" kind="INPUT" tail="S2_a"/>
      <arc head="Fine_Servizio_s" kind="INPUT" tail="S2_b"/>
      <arc head="S3" kind="OUTPUT" tail="Fine_Servizio_s"/>
      <arc head="Reset_S" kind="INPUT" tail="S3"/>
      <arc head="S0" kind="OUTPUT" tail="Reset_S">
        <point x="9.0" y="29.0"/>
        <point x="9.0" y="7.0"/>
      </arc>
      <arc head="R0" kind="OUTPUT" tail="Reset_R">
        <point x="32.0" y="7.0"/>
      </arc>
      <arc head="Reset_R" kind="INPUT" tail="R3"/>
      <arc head="R3" kind="OUTPUT" tail="Fine_Servizio_R"/>
      <arc head="Fine_Servizio_R" kind="INPUT" tail="R2"/>
      <arc head="R2" kind="OUTPUT" tail="Azione_locale_R"/>
      <arc head="Azione_locale_R" kind="INPUT" tail="R1"/>
      <arc head="R1" kind="OUTPUT" tail="Inizio_Servizio_R"/>
      <arc head="Inizio_Servizio_R" kind="INPUT" tail="R0"/>
      <arc head="azione_locale_m" kind="INPUT" tail="M0">
        <point x="68.5" y="7.0"/>
        <point x="68.5" y="11.0"/>
      </arc>
      <arc head="M1" kind="OUTPUT" tail="azione_locale_m">
        <point x="75.5" y="11.0"/>
        <point x="75.5" y="15.0"/>
      </arc>
      <arc head="Richiesta_Servizio" kind="INPUT" tail="M1"/>
      <arc head="M2" kind="OUTPUT" tail="Richiesta_Servizio">
        <point x="67.0" y="20.0"/>
      </arc>
      <arc head="Attesa_Elaborazione" kind="INPUT" tail="M2"/>
      <arc head="M3" kind="OUTPUT" tail="Attesa_Elaborazione"/>
      <arc head="M0" kind="OUTPUT" tail="Reset_M">
        <point x="78.0" y="7.0"/>
      </arc>
      <arc head="Reset_M" kind="INPUT" tail="M3">
        <point x="78.0" y="29.0"/>
      </arc>
      <arc head="Freechoice" kind="OUTPUT" tail="Richiesta_Servizio"/>
      <arc head="Scelta_1" kind="INPUT" tail="Freechoice">
        <point x="58.0" y="4.0"/>
      </arc>
      <arc head="Scelta_2" kind="INPUT" tail="Freechoice">
        <point x="58.0" y="10.0"/>
      </arc>
      <arc head="P0" kind="OUTPUT" tail="Scelta_2"/>
      <arc head="Inizio_Servizio_R" kind="INPUT" tail="P0">
        <point x="42.5" y="10.0"/>
        <point x="42.5" y="12.0"/>
      </arc>
      <arc head="P1" kind="OUTPUT" tail="Scelta_1"/>
      <arc head="Inizio_Servizio_s" kind="INPUT" tail="P1">
        <point x="23.5" y="4.0"/>
        <point x="23.5" y="12.0"/>
      </arc>
      <arc head="Risultato" kind="OUTPUT" tail="Fine_Servizio_s">
        <point x="25.0" y="29.0"/>
        <point x="25.0" y="38.0"/>
        <point x="57.5" y="38.0"/>
        <point x="58.0" y="38.0"/>
      </arc>
      <arc head="Risultato" kind="OUTPUT" tail="Fine_Servizio_R">
        <point x="48.0" y="29.0"/>
        <point x="48.0" y="38.0"/>
        <point x="58.0" y="38.0"/>
      </arc>
      <arc head="Attesa_Elaborazione" kind="INPUT" tail="Risultato"/>
    </edges>
  </gspn>
  <measures gspn-name="PT" name="Measures" simplified-UI="false">
    <assignments>
      <assignment bind-model="SINGLE_VALUE" single-val="" type="INTEGER" varname="n"/>
      <assignment bind-model="SINGLE_VALUE" single-val="" type="INTEGER" varname="r1"/>
      <assignment bind-model="SINGLE_VALUE" single-val="" type="INTEGER" varname="r2"/>
    </assignments>
    <rgmedd2/>
    <formulas>
      <formula comment="Basic statistics of the toolchain execution." language="STAT"/>
    </formulas>
  </measures>
  <measures gspn-name="PT" log-uuid="0d144336-f757-401b-bc1b-b6adf679f0ee" name="CTL model checking of PT" rapid-type="CTL_MODEL_CHECKING" simplified-UI="true">
    <assignments>
      <assignment bind-model="SINGLE_VALUE" single-val="2" type="INTEGER" varname="n"/>
      <assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="r1"/>
      <assignment bind-model="SINGLE_VALUE" single-val="1" type="INTEGER" varname="r2"/>
    </assignments>
    <rgmedd2/>
    <formulas>
      <formula language="STAT"/>
      <formula comment="CTL formula" expr="AF(#S1_a == 1)" language="CTL">
        <result-table>
          <mc-result name="MEASURE0" value="false">
            <bindings>
              <binding name="r2" value="1"/>
              <binding name="n" value="2"/>
              <binding name="r1" value="1"/>
            </bindings>
          </mc-result>
        </result-table>
      </formula>
    </formulas>
  </measures>
  <resource-list>
    <document-log uuid="0d144336-f757-401b-bc1b-b6adf679f0ee">rO0ABXNyABRqYXZhLnV0aWwuTGlua2VkTGlzdAwpU11KYIgiAwAAeHB3BAAAAKZ0AMkbWzBtRVhFQzogL3Vzci9sb2NhbC9HcmVhdFNQTi9iaW4vRFNQTi1Ub29sIC1sb2FkICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8yL2dzcG4vRXMyQi1DVEwgbW9kZWwgY2hlY2tpbmcgb2YgUFQuc29sdXRpb24vUFQiIC1tcGFyIG4gMiAtbXBhciByMSAxIC1tcGFyIHIyIDEgLXBiYXNpcyAtZGV0ZWN0LWV4cCAtcHNmbCAtYm5kIAp0AIYbWzFtG1s0bUxPQURJTkcgUEVUUkkgTkVUIC9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzIvZ3Nwbi9FczJCLUNUTCBtb2RlbCBjaGVja2luZyBvZiBQVC5zb2x1dGlvbi9QVCAobmV0L2RlZikuLi4bWzIybRtbMjRtCnQAD01BUktJTkcgUEFSOiAzCnQAEFBMQUNFUzogICAgICAxOAp0AA9SQVRFIFBBUjogICAgMAp0ABBUUkFOU0lUSU9OUzogMTUKdAAPTUVBU1VSRVM6ICAgIDAKdAAoTE9BRElORyBUSU1FOiBbVXNlciAwLjAwMHMsIFN5cyAwLjAwMHNdCnQAAQp0AAEKdAAfTUFSS0lORyBQQVJBTUVURVIgIm4iIFNFVCBUTyAyCnQAIE1BUktJTkcgUEFSQU1FVEVSICJyMSIgU0VUIFRPIDEKdAAgTUFSS0lORyBQQVJBTUVURVIgInIyIiBTRVQgVE8gMQp0AB5DT01QVVRJTkcgUExBQ0UgRkxPVyBCQVNJUy4uLgp0ABJNPTE1LCBOPTE4LCBOMD0xOAp0ADlDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBzdGVwIDEvMTUsIHxLfD0xNiwgcHJvZHVjdHM9MQp0AFMbWzFBICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgCnQAUxtbMUFDb21wdXRhdGlvbiBvZiBGbG93IGJhc2lzOiBjb21wbGV0ZWQgaW4gMTMgc3RlcHMsIHxLfD01LiAgICAgICAgICAgICAgICAgICAgICAKdABARk9VTkQgNSBWRUNUT1JTIElOIFRIRSBQTEFDRSBGTE9XIEJBU0lTICg0IHNlbWlmbG93cywgMSBmbG93cykuCnQAAQp0AAEKdAAnQWxsIHBsYWNlcyBhcmUgY292ZXJlZCBieSBzb21lIFAtZmxvdy4KdAABCnQAJlRPVEFMIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAAnQVZPSUQgRVhQT05FTlRJQUwgR1JPV1RIIE9GIFNFTUlGTE9XUy4KdAAdQ09NUFVUSU5HIFBMQUNFIFNFTUlGTE9XUy4uLgp0ABJNPTE1LCBOPTE4LCBOMD0xOAp0ACtHZW5lcmF0aW9uIG9mIFNlbWlmbG93czogc3RlcCAxLzE1LCB8S3w9MTYKdABTG1sxQSAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIAp0AFEbWzFBR2VuZXJhdGlvbiBvZiBTZW1pZmxvd3M6IGNvbXBsZXRlZCBpbiAxMyBzdGVwcywgfEt8PTYuICAgICAgICAgICAgICAgICAgICAgIAp0ABlGT1VORCA2IFBMQUNFIFNFTUlGTE9XUy4KdAABCnQAAQp0ACtBbGwgcGxhY2VzIGFyZSBjb3ZlcmVkIGJ5IHNvbWUgUC1zZW1pZmxvdy4KdAABCnQAJlRPVEFMIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAAsQ09NUFVUSU5HIFBMQUNFIEJPVU5EUyBGUk9NIFAtU0VNSUZMT1dTIC4uLgp0ACcbWzBYG1szMm0gUFJPQ0VTUyBFWElURUQgTk9STUFMTFkuG1swbQp0ANobWzBtRVhFQzogcGVybCAtZSAnYWxhcm0gNSA7IGV4ZWMgIi91c3IvbG9jYWwvR3JlYXRTUE4vYmluL0RTUE4tVG9vbCAtbG9hZCBcIi9ob21lL3VzZXIvVU5JVE8vYW5ubzMvdnBjL2NvbnNlZ25lLzIvZ3Nwbi9FczJCLUNUTCBtb2RlbCBjaGVja2luZyBvZiBQVC5zb2x1dGlvbi9QVFwiIC1tcGFyIG4gMiAtbXBhciByMSAxIC1tcGFyIHIyIDEgLWxvYWQtYm5kIC1pbHAtYm5kIiAnCnQAhhtbMW0bWzRtTE9BRElORyBQRVRSSSBORVQgL2hvbWUvdXNlci9VTklUTy9hbm5vMy92cGMvY29uc2VnbmUvMi9nc3BuL0VzMkItQ1RMIG1vZGVsIGNoZWNraW5nIG9mIFBULnNvbHV0aW9uL1BUIChuZXQvZGVmKS4uLhtbMjJtG1syNG0KdAAPTUFSS0lORyBQQVI6IDMKdAAQUExBQ0VTOiAgICAgIDE4CnQAD1JBVEUgUEFSOiAgICAwCnQAEFRSQU5TSVRJT05TOiAxNQp0AA9NRUFTVVJFUzogICAgMAp0AChMT0FESU5HIFRJTUU6IFtVc2VyIDAuMDAwcywgU3lzIDAuMDAwc10KdAABCnQAAQp0AB9NQVJLSU5HIFBBUkFNRVRFUiAibiIgU0VUIFRPIDIKdAAgTUFSS0lORyBQQVJBTUVURVIgInIxIiBTRVQgVE8gMQp0ACBNQVJLSU5HIFBBUkFNRVRFUiAicjIiIFNFVCBUTyAxCnQAFUxPQURJTkcgQk5EIEZJTEUgLi4uCnQAJUNPTVBVVElORyBQTEFDRSBCT1VORFMgVVNJTkcgSUxQIC4uLgp0ABhBbGwgcGxhY2VzIGFyZSBib3VuZGVkLgpxAH4AJ3QAqxtbMG1FWEVDOiAvdXNyL2xvY2FsL0dyZWF0U1BOL2Jpbi9SR01FREQzICIvaG9tZS91c2VyL1VOSVRPL2Fubm8zL3ZwYy9jb25zZWduZS8yL2dzcG4vRXMyQi1DVEwgbW9kZWwgY2hlY2tpbmcgb2YgUFQuc29sdXRpb24vUFQiIC1NRVRBICAtbXBhciBuIDIgLW1wYXIgcjEgMSAtbXBhciByMiAxIC1DCnQAK092ZXJyaWRpbmcgbWFya2luZyBwYXJhbWV0ZXIgbiB0byB2YWx1ZSAyLgp0ACxPdmVycmlkaW5nIG1hcmtpbmcgcGFyYW1ldGVyIHIxIHRvIHZhbHVlIDEuCnQALE92ZXJyaWRpbmcgbWFya2luZyBwYXJhbWV0ZXIgcjIgdG8gdmFsdWUgMS4KdAAgUmFuZG9tIHNlZWRzOiAxNTkwMDY5NDQ0IDM5MzgwMgp0AFA9PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09CnQAEUdyZWF0U1BOL01lZGRseS4KdAA4ICBDb3B5cmlnaHQgKEMpIDE5ODctMjAxOCwgVW5pdmVyc2l0eSBvZiBUb3Jpbm8sIEl0YWx5Lgp0ADEgIFNlbmQgZmlsZXMgbmV0bmFtZS5uZXQsIC5kZWYgdG8gZS1tYWlsIGFkZHJlc3MKdAArICBiZWNjdXRpQGRpLnVuaXRvLml0IGlmIHlvdSBmaW5kIGFueSBidWcuCnQAUD09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT09PT0KdAAfQmFzZWQgb24gTUVERExZIHZlc
  </resource-list>
</project>