%-------------------------------------------------------------- % T0 := [ 1, 9,10,13,15,20,23,22]; -- G1 % T1 := [ 3, 9,10,13,15,20,24,22]; -- R1 % T2 := [ 5,27,11,13,16,20,25,22]; -- Y1 % T3 := [ 7,27,11,13,16,20,26,22]; -- B1 % T4 := [23,22,17,18,11, 9, 2, 1]; -- G2 % T5 := [24,22,17,18,11, 9, 4, 3]; -- R2 % T6 := [25,22,17,18,12,27, 6, 5]; -- Y2 % T7 := [26,22,17,18,12,27, 8, 7]; -- B2 %-------------------------------------------------------------- map T0: Nat -> Nat; eqn T0(0)= 1; T0(1)= 9; T0(2)=10; T0( 3)=13; T0( 4)=15; T0( 5)=20; T0( 6)=23; map T1: Nat -> Nat; eqn T1(0)= 3; T1(1)=9; T1(2)=10; T1( 3)=13; T1( 4)=15; T1( 5)=20; T1( 6)=24; map T2: Nat -> Nat; eqn T2(0)= 5; T2(1)=27; T2(2)=11; T2( 3)=13; T2( 4)=16; T2( 5)=20; T2( 6)=25; map T3: Nat -> Nat; eqn T3(0)= 7; T3(1)=27; T3(2)=11; T3( 3)=13; T3( 4)=16; T3( 5)=20; T3( 6)=26; map T4: Nat -> Nat; eqn T4(0)=23; T4(1)=22; T4(2)=17; T4( 3)=18; T4( 4)=11; T4( 5)= 9; T4( 6)= 2; map T5: Nat -> Nat; eqn T5(0)=24; T5(1)=22; T5(2)=17; T5( 3)=18; T5( 4)=11; T5( 5)=9; T5( 6)= 4; map T6: Nat -> Nat; eqn T6(0)=25; T6(1)=22; T6(2)=17; T6(3)=18; T6(4)=12; T6(5)=27; T6(6)=6; T6(7)= 5; T6(8)=27; T6(9)=11; T6(10)=13; T6(11)=16; T6(12)=20; T6(13)=25; map T7: Nat -> Nat; eqn T7(0)=26; T7(1)=22; T7(2)=17; T7( 3)=18; T7( 4)=12; T7( 5)=27; T7( 6)= 8; % ------ region A: train constraints ------ % 0 1 2 3 4 5 6 7 8 9 10 11 12 13 % A0 := [ 0, 0, 0, 1, 0,-1, 0, 1, 0, 0,-1, 0, 0, 0]; -- G1 % A1 := [ 0, 0, 0, 1, 0,-1, 0, 1, 0, 0,-1, 0, 0, 0]; -- R1 % A2 := [ 0, 0, 1,-1, 0, 1, 0, 0, 0,-1, 0, 0, 0, 0]; -- Y1 % A3 := [ 0, 0, 1,-1, 0, 0, 0, 1, 0,-1, 0, 0, 0, 0]; -- B1 % A4 := [ 0, 1, 0, 0,-1, 0, 0, 0, 0, 0, 1, 0,-1, 0]; -- G2 % A5 := [ 0, 1, 0, 0,-1, 0, 0, 0, 0, 0, 1, 0,-1, 0]; -- R2 % A6 := [ 0, 0, 0,-1, 0, 0, 0, 0, 0, 1,-1, 0, 1, 0]; -- Y2 % A7 := [ 0, 1, 0,-1, 0, 0, 0, 0, 0, 1,-1, 0, 0, 0]; -- B2 % ------------------------------------------ map LA: Nat; % limit for region A eqn LA = 7; map A0: Nat -> Int; eqn A0(0)=0; A0(1)=0; A0(2)=0; A0( 3)= 1; A0( 4)=0; A0( 5)=-1; A0( 6)=0; map A1: Nat -> Int; eqn A1(0)=0; A1(1)=0; A1(2)=0; A1( 3)= 1; A1( 4)=0; A1( 5)=-1; A1( 6)=0; map A2: Nat -> Int; eqn A2(0)=0; A2(1)=0; A2(2)= 1; A2( 3)=-1; A2( 4)=0; A2( 5)= 1; A2( 6)=0; map A3: Nat -> Int; eqn A3(0)=0; A3(1)=0; A3(2)= 1; A3( 3)=-1; A3( 4)=0; A3( 5)= 0; A3( 6)=0; map A4: Nat -> Int; eqn A4(0)=0; A4(1)=1; A4(2)=0; A4( 3)=0; A4( 4)=-1; A4( 5)= 0; A4( 6)=0; map A5: Nat -> Int; eqn A5(0)=0; A5(1)=1; A5(2)=0; A5( 3)=0; A5( 4)=-1; A5( 5)= 0; A5( 6)=0; map A6: Nat -> Int; eqn A6(0)=0; A6(1)=0; A6(2)=0; A6( 3)=-1; A6( 4)=0; A6( 5)= 0; A6( 6)=0; map A7: Nat -> Int; eqn A7(0)=0; A7(1)=1; A7(2)=0; A7( 3)=-1; A7( 4)=0; A7( 5)= 0; A7( 6)=0; % ------- region B: train constraints ------ % 0 1 2 3 4 5 6 7 8 9 10 11 12 13 % B0 := [ 0, 0, 0, 1, 0,-1, 0, 1, 0, 0,-1, 0, 0, 0]; -- G1 % B1 := [ 0, 0, 0, 1, 0,-1, 0, 1, 0, 0,-1, 0, 0, 0]; -- R1 % B2 := [ 0, 0, 1,-1, 0, 0, 0, 1, 0,-1, 0, 0, 0, 0]; -- Y1 % B3 := [ 0, 0, 1,-1, 0, 1, 0, 0, 0,-1, 0, 0, 0, 0]; -- B1 % B4 := [ 0, 1, 0, 0,-1, 0, 0, 0, 0, 0, 1, 0,-1, 0]; -- G2 % B5 := [ 0, 1, 0, 0,-1, 0, 0, 0, 0, 0, 1, 0,-1, 0]; -- R2 % B6 := [ 0, 1, 0,-1, 0, 0, 0, 0, 0, 1,-1, 0, 0, 0]; -- Y2 % B7 := [ 0, 0, 0,-1, 0, 0, 0, 0, 0, 1,-1, 0, 1, 0]; -- B2 % ------------------------------------------ map LB: Nat; % limit for region B eqn LB = 7; map B0: Nat -> Int; eqn B0(0)=0; B0(1)=0; B0(2)=0; B0( 3)= 1; B0( 4)=0; B0( 5)=-1; B0( 6)=0; map B1: Nat -> Int; eqn B1(0)=0; B1(1)=0; B1(2)=0; B1( 3)= 1; B1( 4)=0; B1( 5)=-1; B1( 6)=0; map B2: Nat -> Int; eqn B2(0)=0; B2(1)=0; B2(2)= 1; B2( 3)=-1; B2( 4)=0; B2( 5)= 0; B2( 6)=0; map B3: Nat -> Int; eqn B3(0)=0; B3(1)=0; B3(2)= 1; B3( 3)=-1; B3( 4)=0; B3( 5)= 1; B3( 6)=0; map B4: Nat -> Int; eqn B4(0)=0; B4(1)=1; B4(2)=0; B4( 3)=-0; B4( 4)=-1; B4( 5)= 0; B4( 6)=0; map B5: Nat -> Int; eqn B5(0)=0; B5(1)=1; B5(2)=0; B5( 3)=0; B5( 4)=-1; B5( 5)= 0; B5( 6)=0; map B6: Nat -> Int; eqn B6(0)=0; B6(1)=1; B6(2)=0; B6( 3)=-1; B6( 4)=0; B6( 5)= 0; B6( 6)=0; map B7: Nat -> Int; eqn B7(0)=0; B7(1)=0; B7(2)=0; B7( 3)=-1; B7( 4)=0; B7( 5)= 0; B7( 6)=0; act arrived; move: Nat; proc AllTrains(P0:Nat, P1:Nat, P2:Nat, P3:Nat, P4:Nat, P5:Nat, P6:Nat, P7:Nat, RA: Int, RB: Int) = (P0 < 6 && % train0 has not yet reached all the steps of its mission T0(P0+1) != T1(P1) && % next place of train0 not occupied by train1 T0(P0+1) != T2(P2) && % next place of train0 not occupied by train2 T0(P0+1) != T3(P3) && T0(P0+1) != T4(P4) && T0(P0+1) != T5(P5) && T0(P0+1) != T6(P6) && T0(P0+1) != T7(P7) && % next place of train0 not occupied by train7 RA + A0(P0+1) <= LA && % progress of train0 does not saturate RA RB + B0(P0+1) <= LB % progress of train0 does not saturate RB ) -> move(0). AllTrains(P0+1,P1,P2,P3,P4,P5,P6,P7,RA+A0(P0+1),RB+B0(P0+1)) + (P1 < 6 && T1(P1+1) != T0(P0) && T1(P1+1) != T2(P2) && T1(P1+1) != T3(P3) && T1(P1+1) != T4(P4) && T1(P1+1) != T5(P5) && T1(P1+1) != T6(P6) && T1(P1+1) != T7(P7) && RA + A1(P1+1) <= LA && RB + B1(P1+1) <= LB ) -> move(1). AllTrains(P0,P1+1,P2,P3,P4,P5,P6,P7,RA+A1(P1+1),RB+B1(P1+1)) + (P2 < 6 && T2(P2+1) != T0(P0) && T2(P2+1) != T1(P1) && T2(P2+1) != T3(P3) && T2(P2+1) != T4(P4) && T2(P2+1) != T5(P5) && T2(P2+1) != T6(P6) && T2(P2+1) != T7(P7) && RA + A2(P2+1) <= LA && RB + B2(P2+1) <= LB ) -> move(2). AllTrains(P0,P1,P2+1,P3,P4,P5,P6,P7,RA+A2(P2+1),RB+B2(P2+1)) + (P3 < 6 && T3(P3+1) != T0(P0) && T3(P3+1) != T1(P1) && T3(P3+1) != T2(P2) && T3(P3+1) != T4(P4) && T3(P3+1) != T5(P5) && T3(P3+1) != T6(P6) && T3(P3+1) != T7(P7) && RA + A3(P3+1) <= LA && RB + B3(P3+1) <= LB ) -> move(3). AllTrains(P0,P1,P2,P3+1,P4,P5,P6,P7,RA+A3(P3+1),RB+B3(P3+1)) + (P4 < 6 && T4(P4+1) != T0(P0) && T4(P4+1) != T1(P1) && T4(P4+1) != T2(P2) && T4(P4+1) != T3(P3) && T4(P4+1) != T5(P5) && T4(P4+1) != T6(P6) && T4(P4+1) != T7(P7) && RA + A4(P4+1) <= LA && RB + B4(P4+1) <= LB ) -> move(4). AllTrains(P0,P1,P2,P3,P4+1,P5,P6,P7,RA+A4(P4+1),RB+B4(P4+1)) + (P5 < 6 && T5(P5+1) != T0(P0) && T5(P5+1) != T1(P1) && T5(P5+1) != T2(P2) && T5(P5+1) != T3(P3) && T5(P5+1) != T4(P4) && T5(P5+1) != T6(P6) && T5(P5+1) != T7(P7) && RA + A5(P5+1) <= LA && RB + B5(P5+1) <= LB ) -> move(5). AllTrains(P0,P1,P2,P3,P4,P5+1,P6,P7,RA+A5(P5+1),RB+B5(P5+1)) + (P6 < 6 && T6(P6+1) != T0(P0) && T6(P6+1) != T1(P1) && T6(P6+1) != T2(P2) && T6(P6+1) != T3(P3) && T6(P6+1) != T4(P4) && T6(P6+1) != T5(P5) && T6(P6+1) != T7(P7) && RA + A6(P6+1) <= LA && RB + B6(P6+1) <= LB ) -> move(6). AllTrains(P0,P1,P2,P3,P4,P5,P6+1,P7,RA+A6(P6+1),RB+B6(P6+1)) + (P7 < 6 && T7(P7+1) != T0(P0) && T7(P7+1) != T1(P1) && T7(P7+1) != T2(P2) && T7(P7+1) != T3(P3) && T7(P7+1) != T4(P4) && T7(P7+1) != T5(P5) && T7(P7+1) != T6(P6) && RA + A7(P7+1) <= LA && RB + B7(P7+1) <= LB ) -> move(7). AllTrains(P0,P1,P2,P3,P4,P5,P6,P7+1,RA+A7(P7+1),RB+B7(P7+1)) + ((P0 ==6) && (P1 ==6) && (P2 ==6) && (P3 ==6) && (P4 ==6) && (P5 ==6) && (P6 ==6) && (P7 ==6)) -> arrived . AllTrains(P0,P1,P2,P3,P4,P5,P6,P7,RA,RB); init AllTrains(0,0,0,0,0,0,0,0, 1,1); %%%%%%%%%%% verfication process : %%%%%%%%%%%%%%%%% % % mcrl22lps mcrl2_oneway8small.txt temp.lps % lps2pbes -fformula.mcf temp.lps temp.pbes % formula.mcf= "mu X.(([!arrived]X) && ( true))" == AF {arrived} % time pbes2bool -s2 -vrjittyc temp.pbes % > real 1m53.996s % > user 1m52.243s % > sys 0m1.583s % > USED VIRTUAL MEMORY 1.06 GB % % time pbes2bool -s2 temp.pbes % > real 19m47.753s % % lps2lts -rjittyc --verbose temp.lps temp.lts % ltsinfo temp.lts % > done with state space generation (49 levels, 1_636_545 states and 7_134_233 transitions) % > % > % % formula.mcf= "mu X.(([!arrived]X) && ( true))" == AF {arrived} % formula.mcf= "[ true* ] < true* . ARRIVED > true" == AG EF {arrived} % pbes2bool -c print evidence on validity of formula, nedded by lpsxsim for % % lps2lts --verbose –rjittyc –cached -D -F temp.lps temp.lts % ( -sdepth -sBreadth --suppress --todo=maxnum --no-info % % the generation of counter-examples % pbes2bool -zb breadth-first % pbes2bool -zd depth-first % pbes2bool --todo -strategy %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%