<?xml version="1.0" encoding="UTF-8" ?>
<romeo version="Romeo v3.10.2">
<TPN name="/Users/dalzilio/Documents/Now/2025_EcoleSED_ModelChecking/Romeo/trains2b.xml">
  <place id="1" identifier="Far" label="Far" initialMarking="1" eft="0" lft="inf"> 
      <graphics color="0"> 
         <position x="121.0" y="76.0"/> 
         <deltaLabel deltax="13.0" deltay="-24.0"/> 
      </graphics> 
      <scheduling gamma="0" omega="0"/> 
  </place> 

  <place id="2" identifier="Close" label="Close" initialMarking="0" eft="0" lft="inf"> 
      <graphics color="0"> 
         <position x="121.0" y="196.0"/> 
         <deltaLabel deltax="25.77777777777777" deltay="-7.111111111111114"/> 
      </graphics> 
      <scheduling gamma="0" omega="0"/> 
  </place> 

  <place id="3" identifier="On" label="On" initialMarking="0" eft="0" lft="inf"> 
      <graphics color="0"> 
         <position x="121.0" y="316.0"/> 
         <deltaLabel deltax="10" deltay="10"/> 
      </graphics> 
      <scheduling gamma="0" omega="0"/> 
  </place> 

  <place id="4" identifier="Far2" label="Far2" initialMarking="1" eft="0" lft="inf"> 
      <graphics color="0"> 
         <position x="541.0" y="76.0"/> 
         <deltaLabel deltax="13.0" deltay="-24.0"/> 
      </graphics> 
      <scheduling gamma="0" omega="0"/> 
  </place> 

  <place id="5" identifier="Open" label="Open" initialMarking="1" eft="0" lft="inf"> 
      <graphics color="0"> 
         <position x="286.0" y="211.0"/> 
         <deltaLabel deltax="-2.0" deltay="15.0"/> 
      </graphics> 
      <scheduling gamma="0" omega="0"/> 
  </place> 

  <place id="6" identifier="Closed" label="Closed" initialMarking="0" eft="0" lft="inf"> 
      <graphics color="0"> 
         <position x="406.0" y="211.0"/> 
         <deltaLabel deltax="10" deltay="10"/> 
      </graphics> 
      <scheduling gamma="0" omega="0"/> 
  </place> 

  <place id="7" identifier="Close2" label="Close2" initialMarking="0" eft="0" lft="inf"> 
      <graphics color="0"> 
         <position x="541.0" y="196.0"/> 
         <deltaLabel deltax="29.555555555555543" deltay="-8.111111111111114"/> 
      </graphics> 
      <scheduling gamma="0" omega="0"/> 
  </place> 

  <place id="8" identifier="On2" label="On2" initialMarking="0" eft="0" lft="inf"> 
      <graphics color="0"> 
         <position x="541.0" y="316.0"/> 
         <deltaLabel deltax="24.0" deltay="-6.7777777777777715"/> 
      </graphics> 
      <scheduling gamma="0" omega="0"/> 
  </place> 

  <transition id="1" identifier="app" label="app"  eft="1" lft="inf" eft_param="1" speed="1" priority="0" cost="0" unctrl="0" obs="1"  guard=""> 
     <graphics color="0"> 
        <position x="121.0" y="136.0"/> 
        <deltaLabel deltax="33.0" deltay="-23.0"/> 
        <deltaGuard deltax="20" deltay="-20"/> 
        <deltaUpdate deltax="34.0" deltay="11.0"/> 
        <deltaSpeed deltax="-20" deltay="5"/> 
        <deltaCost deltax="-20" deltay="5"/> 
     </graphics> 
     <update><![CDATA[nbTrain++;]]></update> 
  </transition> 

  <transition id="2" identifier="in" label="in"  eft="4" lft="5" eft_param="c" lft_param="5" speed="1" priority="0" cost="0" unctrl="0" obs="1"  guard=""> 
     <graphics color="0"> 
        <position x="121.0" y="256.0"/> 
        <deltaLabel deltax="36.33333333333334" deltay="-0.11111111111114269"/> 
        <deltaGuard deltax="20" deltay="-20"/> 
        <deltaUpdate deltax="42.77777777777777" deltay="-18.22222222222223"/> 
        <deltaSpeed deltax="-20" deltay="5"/> 
        <deltaCost deltax="-20" deltay="5"/> 
     </graphics> 
     <update><![CDATA[CptOn++;]]></update> 
  </transition> 

  <transition id="3" identifier="exit" label="exit"  eft="2" lft="4" eft_param="2" lft_param="4" speed="1" priority="0" cost="0" unctrl="0" obs="1"  guard=""> 
     <graphics color="0"> 
        <position x="121.0" y="391.0"/> 
        <deltaLabel deltax="38.333333333333314" deltay="-18.66666666666663"/> 
        <deltaGuard deltax="20" deltay="-20"/> 
        <deltaUpdate deltax="6.0" deltay="12.0"/> 
        <deltaSpeed deltax="-20" deltay="5"/> 
        <deltaCost deltax="-20" deltay="5"/> 
     </graphics> 
     <update><![CDATA[nbTrain--;
CptOn--;]]></update> 
  </transition> 

  <transition id="4" identifier="down" label="down"  eft="1" lft="2" eft_param="a" lft_param="b" speed="1" priority="0" cost="0" unctrl="0" obs="1"  guard="nbTrain#greater0"> 
     <graphics color="0"> 
        <position x="346.0" y="151.0"/> 
        <deltaLabel deltax="36.0" deltay="-16.0"/> 
        <deltaGuard deltax="-8.0" deltay="-27.0"/> 
        <deltaUpdate deltax="20" deltay="10"/> 
        <deltaSpeed deltax="-20" deltay="5"/> 
        <deltaCost deltax="-20" deltay="5"/> 
     </graphics> 
     <update><![CDATA[]]></update> 
  </transition> 

  <transition id="5" identifier="up" label="up"  eft="1" lft="2" eft_param="1" lft_param="2" speed="1" priority="0" cost="0" unctrl="0" obs="1"  guard="nbTrain#eqeq0 "> 
     <graphics color="0"> 
        <position x="346.0" y="271.0"/> 
        <deltaLabel deltax="14.0" deltay="11.0"/> 
        <deltaGuard deltax="50.0" deltay="-8.0"/> 
        <deltaUpdate deltax="20" deltay="10"/> 
        <deltaSpeed deltax="-20" deltay="5"/> 
        <deltaCost deltax="-20" deltay="5"/> 
     </graphics> 
     <update><![CDATA[]]></update> 
  </transition> 

  <transition id="6" identifier="app2" label="app2"  eft="1" lft="inf" eft_param="1" speed="1" priority="0" cost="0" unctrl="0" obs="1"  guard=""> 
     <graphics color="0"> 
        <position x="541.0" y="136.0"/> 
        <deltaLabel deltax="33.0" deltay="-23.0"/> 
        <deltaGuard deltax="20" deltay="-20"/> 
        <deltaUpdate deltax="34.0" deltay="11.0"/> 
        <deltaSpeed deltax="-20" deltay="5"/> 
        <deltaCost deltax="-20" deltay="5"/> 
     </graphics> 
     <update><![CDATA[nbTrain++;]]></update> 
  </transition> 

  <transition id="7" identifier="in2" label="in2"  eft="4" lft="5" eft_param="c" lft_param="5" speed="1" priority="0" cost="0" unctrl="0" obs="1"  guard=""> 
     <graphics color="0"> 
        <position x="541.0" y="256.0"/> 
        <deltaLabel deltax="33.0" deltay="3.0"/> 
        <deltaGuard deltax="20" deltay="-20"/> 
        <deltaUpdate deltax="41.0" deltay="-12.0"/> 
        <deltaSpeed deltax="-20" deltay="5"/> 
        <deltaCost deltax="-20" deltay="5"/> 
     </graphics> 
     <update><![CDATA[CptOn++;]]></update> 
  </transition> 

  <transition id="8" identifier="exit2" label="exit2"  eft="2" lft="4" eft_param="2" lft_param="4" speed="1" priority="0" cost="0" unctrl="0" obs="1"  guard=""> 
     <graphics color="0"> 
        <position x="541.0" y="391.0"/> 
        <deltaLabel deltax="38.333333333333314" deltay="-18.66666666666663"/> 
        <deltaGuard deltax="20" deltay="-20"/> 
        <deltaUpdate deltax="6.0" deltay="12.0"/> 
        <deltaSpeed deltax="-20" deltay="5"/> 
        <deltaCost deltax="-20" deltay="5"/> 
     </graphics> 
     <update><![CDATA[nbTrain--;
CptOn--;]]></update> 
  </transition> 

  <arc place="1" transition="1" type="PlaceTransition" weight="1" tokenColor="-1"  inhibitingCondition=""> 
    <nail xnail="0" ynail="0"/> 
    <graphics  color="0"> 
     </graphics> 
  </arc> 
 

  <arc place="2" transition="1" type="TransitionPlace" weight="1" tokenColor="-1"> 
     <nail xnail="0" ynail="0"/> 
     <graphics  color="0"> 
     </graphics> 
  </arc> 

  <arc place="2" transition="2" type="PlaceTransition" weight="1" tokenColor="-1"  inhibitingCondition=""> 
    <nail xnail="0" ynail="0"/> 
    <graphics  color="0"> 
     </graphics> 
  </arc> 
 

  <arc place="3" transition="2" type="TransitionPlace" weight="1" tokenColor="-1"> 
     <nail xnail="0" ynail="0"/> 
     <graphics  color="0"> 
     </graphics> 
  </arc> 

  <arc place="3" transition="3" type="PlaceTransition" weight="1" tokenColor="-1"  inhibitingCondition=""> 
    <nail xnail="0" ynail="0"/> 
    <graphics  color="0"> 
     </graphics> 
  </arc> 
 

  <arc place="1" transition="3" type="TransitionPlace" weight="1" tokenColor="-1"> 
     <nail xnail="30.0" ynail="228.33333333333337"/> 
     <graphics  color="0"> 
     </graphics> 
  </arc> 

  <arc place="5" transition="4" type="PlaceTransition" weight="1" tokenColor="-1"  inhibitingCondition=""> 
    <nail xnail="0" ynail="0"/> 
    <graphics  color="0"> 
     </graphics> 
  </arc> 
 

  <arc place="6" transition="4" type="TransitionPlace" weight="1" tokenColor="-1"> 
     <nail xnail="0" ynail="0"/> 
     <graphics  color="0"> 
     </graphics> 
  </arc> 

  <arc place="6" transition="5" type="PlaceTransition" weight="1" tokenColor="-1"  inhibitingCondition=""> 
    <nail xnail="0" ynail="0"/> 
    <graphics  color="0"> 
     </graphics> 
  </arc> 
 

  <arc place="5" transition="5" type="TransitionPlace" weight="1" tokenColor="-1"> 
     <nail xnail="0" ynail="0"/> 
     <graphics  color="0"> 
     </graphics> 
  </arc> 

  <arc place="4" transition="6" type="PlaceTransition" weight="1" tokenColor="-1"  inhibitingCondition=""> 
    <nail xnail="0" ynail="0"/> 
    <graphics  color="0"> 
     </graphics> 
  </arc> 
 

  <arc place="7" transition="6" type="TransitionPlace" weight="1" tokenColor="-1"> 
     <nail xnail="0" ynail="0"/> 
     <graphics  color="0"> 
     </graphics> 
  </arc> 

  <arc place="7" transition="7" type="PlaceTransition" weight="1" tokenColor="-1"  inhibitingCondition=""> 
    <nail xnail="0" ynail="0"/> 
    <graphics  color="0"> 
     </graphics> 
  </arc> 
 

  <arc place="8" transition="7" type="TransitionPlace" weight="1" tokenColor="-1"> 
     <nail xnail="0" ynail="0"/> 
     <graphics  color="0"> 
     </graphics> 
  </arc> 

  <arc place="8" transition="8" type="PlaceTransition" weight="1" tokenColor="-1"  inhibitingCondition=""> 
    <nail xnail="0" ynail="0"/> 
    <graphics  color="0"> 
     </graphics> 
  </arc> 
 

  <arc place="4" transition="8" type="TransitionPlace" weight="1" tokenColor="-1"> 
     <nail xnail="671.0" ynail="215.0"/> 
     <graphics  color="0"> 
     </graphics> 
  </arc> 

  <timedCost></timedCost>

  <nbTokenColor>0</nbTokenColor>

  <declaration><![CDATA[// insert here your type definitions using C-like syntax

// insert here your function definitions 
// using C-like syntax

initially {
int nbTrain=0;
int CptOn=0;

// insert here the state variables declarations 
// and possibly some code to initialize them 
// using C-like syntax
 
 }







]]></declaration>

  <project nbinput="0" openinput="0" nbinclude="0" >
 </project>

  <preferences> 
      <colorPlace  c0="SkyBlue2"  c1="gray"  c2="cyan"  c3="green"  c4="yellow"  c5="brown" /> 
 
      <colorTransition  c0="yellow"  c1="gray"  c2="cyan"  c3="green"  c4="SkyBlue2"  c5="brown" /> 
 
      <colorArc  c0="black"  c1="gray"  c2="blue"  c3="#beb760"  c4="#be5c7e"  c5="#46be90" /> 
 
  </preferences> 
 </TPN> 

  </romeo>
