time_bound := 10; vmax := 83.4; l := 200; sd := 400; amin := -1.4; amax := 0.7; bon := -0.7; boff := -0.3; // -------------------------------------------------------- // System Definition // -------------------------------------------------------- automaton train synclabs : tau; state_var : v,a,s,auth,sl,vl,al,c,m,clock; loc FRxFRxI: while 0 <= v & v <= vmax & amin <= a & a <= amax & v*vmax <= 2*bon*(s-auth) & 0 <= vl & vl <= vmax & amin <= al & al <= amax & c<=8 & clock <= time_bound wait { v' == a & s' == v & vl' == al & sl' == vl & c' == 1 & m' == 0 & auth' == 0 & clock' == 1 } when s>=sl-l sync tau do {v'==0 & a'==0 & s'==0 & auth'==0 & sl'==0 & vl'==0 & al'==0 & c'==0 & m'==0 & clock'==0} goto Crash; when v*vmax >= 2*bon*(s-auth) sync tau goto ABxFRxI; when c>=8 sync tau palt { 99379033: do {v'==v & a'==a & s'==s & auth'==auth & sl'==sl & vl'==vl & al'==al & c'==c & m'<=sl+51 & clock'==clock} goto FRxFRxS, // safe 620967: do {v'==v & a'==a & s'==s & auth'==auth & sl'==sl & vl'==vl & al'==al & c'==c & m'>=sl+49 & clock'==clock} goto FRxFRxS }; loc ABxFRxI: while 0 <= v & v <= vmax & a == amin & v*vmax >= 2*boff*(s-auth) & 0 <= vl & vl <= vmax & amin <= al & al <= amax & c<=8 & clock <= time_bound wait { v' == a & s' == v & vl' == al & sl' == vl & c' == 1 & m' == 0 & auth' == 0 & clock' == 1 } when s>=sl-l sync tau do {v'==0 & a'==0 & s'==0 & auth'==0 & sl'==0 & vl'==0 & al'==0 & c'==0 & m'==0 & clock'==0} goto Crash; when v*vmax <= 2*boff*(s-auth) sync tau goto FRxFRxI; when c>=8 sync tau palt { 99379033: do {v'==v & a'==a & s'==s & auth'==auth & sl'==sl & vl'==vl & al'==al & c'==c & m'<=sl+51 & clock'==clock} goto ABxFRxS, // safe 620967: do {v'==v & a'==a & s'==s & auth'==auth & sl'==sl & vl'==vl & al'==al & c'==c & m'>=sl+49 & clock'==clock} goto ABxFRxS }; loc FRxFRxS: while 0 <= v & v <= vmax & amin <= a & a <= amax & v*vmax <= 2*bon*(s-auth) & 0 <= vl & vl <= vmax & amin <= al & al <= amax & c<=8 & clock <= time_bound wait { v' == a & s' == v & vl' == al & sl' == vl & c' == 1 & m' == 0 & auth' == 0 & clock' == 1 } when s>=sl-l sync tau do {v'==0 & a'==0 & s'==0 & auth'==0 & sl'==0 & vl'==0 & al'==0 & c'==0 & m'==0 & clock'==0} goto Crash; when v*vmax >= 2*bon*(s-auth) sync tau goto ABxFRxS; when c>=8 sync tau palt {9: do {v'==v & a'==a & s'==s & auth'==m-l-sd & sl'==sl & vl'==vl & al'==al & c'==0 & m'==0 & clock'==clock} goto FRxFRxI, 1: do {v'==v & a'==a & s'==s & auth'==auth & sl'==sl & vl'==vl & al'==al & c'==0 & m'==0 & clock'==clock} goto FRxFRxI}; loc ABxFRxS: while 0 <= v & v <= vmax & a == amin & v*vmax >= 2*boff*(s-auth) & 0 <= vl & vl <= vmax & amin <= al & al <= amax & c<=8 & clock <= time_bound wait { v' == a & s' == v & vl' == al & sl' == vl & c' == 1 & m' == 0 & auth' == 0 & clock' == 1 } when s>=sl-l sync tau do {v'==0 & a'==0 & s'==0 & auth'==0 & sl'==0 & vl'==0 & al'==0 & c'==0 & m'==0 & clock'==0} goto Crash; when v*vmax <= 2*boff*(s-auth) sync tau goto FRxFRxS; when c>=8 sync tau palt {9: do {v'==v & a'==a & s'==s & auth'==m-l-sd & sl'==sl & vl'==vl & al'==al & c'==0 & m'==0 & clock'==clock} goto ABxFRxI, 1: do {v'==v & a'==a & s'==s & auth'==auth & sl'==sl & vl'==vl & al'==al & c'==0 & m'==0 & clock'==clock} goto ABxFRxI}; loc Crash: while True wait {v'==0 & a'==0 & s'==0 & vl'==0 & sl'==0 & c'==0 & m'==0 & auth'==0 & al'==0 & clock'==0} initially FRxFRxI & s==200 & v==0 & sl==1400 & vl==0 & auth==800 & clock==0 & c==0 & m==0; end -- train forbidden=train.{Crash & True}; train.reach_graph("ts.graph", forbidden);