% ------------ train missions ------------ % T0 = < 1, 9,10,13,15,20,23> % T1 = < 3, 9,10,13,15,20,24> % T2 = < 5,27,11,13,16,20,25> % T3 = < 7,27,11,13,16,20,26> % T4 = <23,22,17,18,11, 9, 2> % T5 = <24,22,17,18,11, 9, 4> % T6 = <25,22,17,18,12,27, 6> % T7 = <26,22,17,18,12,27, 8> % 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; 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; map Steps: Nat; eqn Steps=6; % ----- region A: train constraints ------ % [0, 0, 0, 1, 0,-1, 0] -- A0 % [0, 0, 0, 1, 0,-1, 0] -- A1 % [0, 0, 1,-1, 0, 1, 0] -- A2 % [0, 0, 1,-1, 0, 0, 0] -- A3 % [0, 1, 0, 0, 0,-1, 0] -- A4 % [0, 1, 0, 0, 0,-1, 0] -- A5 % [1, 0, 0, 0,-1, 0, 0] -- A6 % [0, 1, 0, 0,-1, 0, 0] -- A7 % ---------------------------------------- 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)=0; A4(5)=-1; A4(6)=0; map A5: Nat -> Int; eqn A5(0)=0; A5(1)=1; A5(2)=0; A5(3)=0; A5(4)=0; A5(5)=-1; A5(6)=0; map A6: Nat -> Int; eqn A6(0)=1; A6(1)=0; A6(2)=0; A6(3)=0; A6(4)=-1; A6(5)=0; A6(6)=0; map A7: Nat -> Int; eqn A7(0)=0; A7(1)=1; A7(2)=0; A7(3)=0; A7(4)=-1; A7(5)=0; A7(6)=0; % ----- region B: train constraints ------ % [0, 0, 0, 1, 0,-1, 0] -- B0 % [0, 0, 0, 1, 0,-1, 0] -- B1 % [0, 0, 1,-1, 0, 0, 0] -- B2 % [0, 0, 1,-1, 0, 1, 0] -- B3 % [0, 1, 0, 0, 0,-1, 0] -- B4 % [0, 1, 0, 0, 0,-1, 0] -- B5 % [0, 1, 0, 0,-1, 0, 0] -- B6 % [1, 0, 0, 0,-1, 0, 0] -- B7 % ---------------------------------------- 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)=0; B4(5)=-1; B4(6)=0; map B5: Nat -> Int; eqn B5(0)=0; B5(1)=1; B5(2)=0; B5(3)=0; B5(4)=0; B5(5)=-1; B5(6)=0; map B6: Nat -> Int; eqn B6(0)=0; B6(1)=1; B6(2)=0; B6(3)=0; B6(4)=-1; B6(5)=0; B6(6)=0; map B7: Nat -> Int; eqn B7(0)=1; B7(1)=0; B7(2)=0; B7(3)=0; B7(4)=-1; B7(5)=0; B7(6)=0; act senter,penter,tenter,enter,raenter,rbenter: Nat # Nat # Int # Int; sexit,pexit,texit,exit: Nat # Nat # Int # Int; move,smove: Nat # Nat # Int # Int; ok; arrived; proc E(id:Nat) = sum from:Nat. sum ra:Int. sum rb:Int. penter(from,id,ra,rb).EB(id); proc EB(id:Nat) = sum to:Nat. sum ra:Int. sum rb:Int. pexit(id,to,ra,rb).E(id); proc Train0(Progress:Nat) = (Progress < Steps) -> move(T0(Progress),T0(Progress+1),A0(Progress+1),B0(Progress+1)).Train0(Progress+1) <> ok.Train0(Progress); proc Train1(Progress:Nat) = (Progress < Steps) -> move(T1(Progress),T1(Progress+1),A1(Progress+1),B1(Progress+1)).Train1(Progress+1) <> ok.Train1(Progress); proc Train2(Progress:Nat) = (Progress < Steps) -> move(T2(Progress),T2(Progress+1),A2(Progress+1),B2(Progress+1)).Train2(Progress+1) <> ok.Train2(Progress); proc Train3(Progress:Nat) = (Progress < Steps) -> move(T3(Progress),T3(Progress+1),A3(Progress+1),B3(Progress+1)).Train3(Progress+1) <> ok.Train3(Progress); proc Train4(Progress:Nat) = (Progress < Steps) -> move(T4(Progress),T4(Progress+1),A4(Progress+1),B4(Progress+1)).Train4(Progress+1) <> ok.Train4(Progress); proc Train5(Progress:Nat) = (Progress < Steps) -> move(T5(Progress),T5(Progress+1),A5(Progress+1),B5(Progress+1)).Train5(Progress+1) <> ok.Train5(Progress); proc Train6(Progress:Nat) = (Progress < Steps) -> move(T6(Progress),T6(Progress+1),A6(Progress+1),B6(Progress+1)).Train6(Progress+1) <> ok.Train6(Progress); proc Train7(Progress:Nat) = (Progress < Steps) -> move(T7(Progress),T7(Progress+1),A7(Progress+1),B7(Progress+1)).Train7(Progress+1) <> ok.Train7(Progress); proc Ra(Count:Int) = (Count <= LA) -> sum p1:Nat. sum p2:Nat. sum rb:Int.raenter(p1,p2,0,rb).Ra(Count) + (Count < LA) -> sum p1:Nat. sum p2:Nat. sum rb:Int. raenter(p1,p2,1,rb).Ra(Count+1) + (Count >0) -> sum p1:Nat. sum p2:Nat. sum rb:Int. raenter(p1,p2,-1,rb).Ra(Count-1); proc Rb(Count:Int) = (Count <= LA) -> sum p1:Nat. sum p2:Nat. sum ra:Int. rbenter(p1,p2,ra,0).Rb(Count) + (Count < LA) -> sum p1:Nat. sum p2:Nat. sum ra:Int. rbenter(p1,p2,ra,1).Rb(Count+1) + (Count >0) -> sum p1:Nat. sum p2:Nat. sum ra:Int. rbenter(p1,p2,ra,-1).Rb(Count-1); % % proc Trains = % allow({move,arrived}, % comm({ok|ok|ok|ok -> arrived}, % Train0(0) || Train1(0) || % Train4(0) || Train5(0) % ) % ); proc Trains = allow({move,arrived}, comm({ok|ok|ok| ok|ok|ok|ok -> arrived}, Train0(0) || Train1(0) || Train2(0) || Train3(0) || Train4(0) || Train5(0) || Train6(0) || Train7(0) ) ); Sys = allow( {smove,arrived}, comm({penter|pexit|move|raenter|rbenter -> smove}, Trains || EB(1) || E(2) || EB(3) || E(4) || EB(5) || E(6) || EB(7) || E(8) || E(9) || E(10) || E(11) || E(12) || E(13) || E(14) || E(15) || E(16) || E(17) || E(18) || E(19) || E(20) || E(21) || E(22) || EB(23) || EB(24) || EB(25) || EB(26) || E(27) || Ra(1) || Rb(1) )); init Sys; %% %% formula.mcf= "mu X.(([!arrived] X) && ( true))" %% % /Applications/mCRL2/Applications/mcrl22lps nfm8t-parallelRR-flatflatB-mcrl2.txt temp.lps % /Applications/mCRL2/Applications/lps2pbes -f formula.mcf temp.lps temp.pbes % % time /Applications/mCRL2/Applications/pbes2bool -s2 -vrjittyc temp.pbes % % %%%%%%%%%%%%%%%%%% 4 TRAINS %%%%%%%%%%%%%%%%%%%%% % (-vrjittyc ) % real 0m17.838s % user 0m17.648s % sys 0m0.159s % %%%%%%%%%%%%%%%%%% 8 TRAINS %%%%%%%%%%%%%%%%%%%%% % (-vrjittyc ) % real 431m9.970s % user 430m22.416s % sys 0m25.573s % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% %%%%%%%%%%%% % DEADLOCK DETECTION and TRACE VISUALIZATION % % /Applications/mCRL2/Applications/lps2lts -D -t temp.lps % /Applications/mCRL2/Applications/tracepp temp.lps_dlk_0.trc %%%%%%%%%%%% %%%%%%%%%%%% % --approximate-false % % If set, variables that are removed from the todo buffer are set to true. % This means that the result false is reliable, and the result true can still mean % that the formula is false. % Without this flag true is appromated, meaning that true is the reliable answer, and false is not. % %%%%%%%%%%%