mirela / scp

Go to a project
Toggle navigation Toggle navigation pinning
Johan ARCILE
0ee2e2e4 1 parent e0e02f82

Upload new file

Inline Side-by-side
Showing 1 changed file with 281 additions and 0 deletions
pta
formula fk1Ca = (sPr=1) | (sPr=3);
formula fk2Ca = (sCa=3);
formula fk1O = (sPr=1);
formula fk2O = (sO=2);
formula fk3O = (sF=1);
formula fk4O = (sO=4);
formula fk1P = (sF=1);
formula fk2P = (sP=3);
formula flock1M1 = (sPr=6) | (sG=1);
formula flock2M1 = (sM1=1);
formula funlock1M1 = (sPr=9) | (sG=4);
formula funlock2M1 = (sM1=3);
formula flock1M2 = (sF=4) | (sH=1);
formula flock2M2 = (sM2=1);
formula funlock1M2 = (sF=7) | (sH=4);
formula funlock2M2 = (sM2=3);
formula flock1M3 = (sF=9) | (sM=1);
formula flock2M3 = (sM3=1);
formula funlock1M3 = (sF=12) | (sM=4);
formula funlock2M3 = (sM3=3);
module mCa
xCa : clock;
sCa : [0..3] init 0;
invariant
(sCa=0 => xCa <= 3000) &
(sCa=1 => xCa <= 4500) &
(sCa=2 => xCa <= 0)
endinvariant
[] sCa=0 & xCa >= 2000 -> (sCa'=1) & (xCa'=0);
[] sCa=1 & xCa >= 3500 -> (sCa'=2) & (xCa'=0);
[k1Ca] sCa=2 -> (sCa'=1) & (xCa'=0);
[] sCa=2 & !fk1Ca -> (sCa'=3);
[k2Ca] sCa=3 -> (sCa'=1) & (xCa'=0);
endmodule
module mO
xO : clock;
sO : [0..4] init 0;
invariant
(sO=1 => xO <= 0) &
(sO=3 => xO <= 0)
endinvariant
[] sO=0 & xO >= 50 -> (sO'=1) & (xO'=0);
[k1O] sO=1 -> (sO'=3) & (xO'=0);
[] sO=1 & !fk1O -> (sO'=2);
[k2O] sO=2 -> (sO'=3) & (xO'=0);
[k3O] sO=3 -> (sO'=0) & (xO'=0);
[] sO=3 & !fk3O -> (sO'=4);
[k4O] sO=4 -> (sO'=0) & (xO'=0);
endmodule
module mP
xP : clock;
sP : [0..3] init 0;
invariant
(sP=0 => xP <= 3600) &
(sP=1 => xP <= 3600) &
(sP=2 => xP <= 0)
endinvariant
[] sP=0 & xP >= 2600 -> (sP'=1) & (xP'=0);
[] sP=1 & xP >= 2600 -> (sP'=2) & (xP'=0);
[k1P] sP=2 -> (sP'=1) & (xP'=0);
[] sP=2 & !fk1P -> (sP'=3);
[k2P] sP=3 -> (sP'=1) & (xP'=0);
endmodule
module mF
xF : clock;
sF : [0..12] init 0;
invariant
(sF=0 => xF<=0) &
(sF=2 => xF<=75) &
(sF=3 => xF<=0) &
(sF=5 => xF<=30) &
(sF=6 => xF<=0) &
(sF=8 => xF<=0) &
(sF=10 => xF<=20) &
(sF=11 => xF<=0)
endinvariant
[k2P] sF=0 -> (sF'=2) & (xF'=0);
[k4O] sF=0 -> (sF'=2) & (xF'=0);
[] sF=0 & !fk2P & !fk4O -> (sF'=1);
[k1P] sF=1 -> (sF'=2) & (xF'=0);
[k3O] sF=1 -> (sF'=2) & (xF'=0);
[] sF=2 & xF >= 50 -> (sF'=3) & (xF'=0);
[] sF=3 & !flock2M2 -> (sF'=4);
[lock2F] sF=3 -> (sF'=5) & (xF'=0);
[lock1F] sF=4 -> (sF'=5) & (xF'=0);
[] sF=5 & xF >= 20 -> (sF'=6) & (xF'=0);
[] sF=6 & !funlock2M2 -> (sF'=7);
[unlock2F] sF=6 -> (sF'=8) & (xF'=0);
[unlock1F] sF=7 -> (sF'=8) & (xF'=0);
[] sF=8 & !flock2M3 -> (sF'=9);
[lock4F] sF=8 -> (sF'=10) & (xF'=0);
[lock3F] sF=9 -> (sF'=10) & (xF'=0);
[] sF=10 & xF >= 10 -> (sF'=11) & (xF'=0);
[] sF=11 & !funlock2M3 -> (sF'=12);
[unlock4F] sF=11 -> (sF'=0) & (xF'=0);
[unlock3F] sF=12 -> (sF'=0) & (xF'=0);
endmodule
module mPr
xPr : clock;
sPr : [0..9] init 0;
invariant
(sPr=0 => xPr<=0) &
(sPr=2 => xPr<=0) &
(sPr=4 => xPr<=3000) &
(sPr=5 => xPr<=0) &
(sPr=7 => xPr<=300) &
(sPr=8 => xPr<=0)
endinvariant
[k2O] sPr=0 -> (sPr'=2) & (xPr'=0);
[k2Ca] sPr=0 -> (sPr'=4) & (xPr'=0);
[] sPr=0 & !fk2O & !fk2Ca -> (sPr'=1);
[k1O] sPr=1 -> (sPr'=2) & (xPr'=0);
[k1Ca] sPr=1 -> (sPr'=4) & (xPr'=0);
[k2Ca] sPr=2 -> (sPr'=4) & (xPr'=0);
[] sPr=2 & !fk2Ca -> (sPr'=3);
[k1Ca] sPr=3 -> (sPr'=4) & (xPr'=0);
[] sPr=4 & xPr >= 2000 -> (sPr'=5) & (xPr'=0);
[] sPr=5 & !flock2M1 -> (sPr'=6);
[lock2Pr] sPr=5 -> (sPr'=7) & (xPr'=0);
[lock1Pr] sPr=6 -> (sPr'=7) & (xPr'=0);
[] sPr=7 & xPr >= 200 -> (sPr'=8) & (xPr'=0);
[] sPr=8 & !funlock2M1 -> (sPr'=9);
[unlock2Pr] sPr=8 -> (sPr'=0) & (xPr'=0);
[unlock1Pr] sPr=9 -> (sPr'=0) & (xPr'=0);
endmodule
module mM1
xM1 : clock;
sM1 : [0..3] init 1;
invariant
(sM1=0 => xM1<=0) &
(sM1=2 => xM1<=0)
endinvariant
[] sM1=0 & !flock1M1-> (sM1'=1);
[lock1G] sM1=0 -> (sM1'=2) & (xM1'=0);
[lock1Pr] sM1=0 -> (sM1'=2) & (xM1'=0);
[lock2G] sM1=1 -> (sM1'=2) & (xM1'=0);
[lock2Pr] sM1=1 -> (sM1'=2) & (xM1'=0);
[] sM1=2 & !funlock1M1 -> (sM1'=3);
[unlock1G] sM1=2 -> (sM1'=0) & (xM1'=0);
[unlock1Pr] sM1=2 -> (sM1'=0) & (xM1'=0);
[unlock2G] sM1=3 -> (sM1'=0) & (xM1'=0);
[unlock2Pr] sM1=3 -> (sM1'=0) & (xM1'=0);
endmodule
module mM2
xM2 : clock;
sM2 : [0..3] init 1;
invariant
(sM2=0 => xM2<=0) &
(sM2=2 => xM2<=0)
endinvariant
[] sM2=0 & !flock1M2-> (sM2'=1);
[lock1H] sM2=0 -> (sM2'=2) & (xM2'=0);
[lock1F] sM2=0 -> (sM2'=2) & (xM2'=0);
[lock2H] sM2=1 -> (sM2'=2) & (xM2'=0);
[lock2F] sM2=1 -> (sM2'=2) & (xM2'=0);
[] sM2=2 & !funlock1M2 -> (sM2'=3);
[unlock1H] sM2=2 -> (sM2'=0) & (xM2'=0);
[unlock1F] sM2=2 -> (sM2'=0) & (xM2'=0);
[unlock2H] sM2=3 -> (sM2'=0) & (xM2'=0);
[unlock2F] sM2=3 -> (sM2'=0) & (xM2'=0);
endmodule
module mM3
xM3 : clock;
sM3 : [0..3] init 1;
invariant
(sM3=0 => xM3<=0) &
(sM3=2 => xM3<=0)
endinvariant
[] sM3=0 & !flock1M3-> (sM3'=1);
[lock1M] sM3=0 -> (sM3'=2) & (xM3'=0);
[lock3F] sM3=0 -> (sM3'=2) & (xM3'=0);
[lock2M] sM3=1 -> (sM3'=2) & (xM3'=0);
[lock4F] sM3=1 -> (sM3'=2) & (xM3'=0);
[] sM3=2 & !funlock1M3 -> (sM3'=3);
[unlock1M] sM3=2 -> (sM3'=0) & (xM3'=0);
[unlock3F] sM3=2 -> (sM3'=0) & (xM3'=0);
[unlock2M] sM3=3 -> (sM3'=0) & (xM3'=0);
[unlock4F] sM3=3 -> (sM3'=0) & (xM3'=0);
endmodule
module mG
xG : clock;
sG : [0..5] init 0;
invariant
(sG=0 => xG<=0) &
(sG=2 => xG<=310) &
(sG=3 => xG<=0) &
(sG=5 => xG<=500)
endinvariant
[lock2G] sG=0 -> (sG'=2) & (xG'=0);
[] sG=0 & !flock2M1 -> (sG'=1);
[lock1G] sG=1 -> (sG'=2) & (xG'=0);
[] sG=2 & xG >= 210 -> (sG'=3) & (xG'=0);
[unlock2G] sG=3 -> (sG'=5) & (xG'=0);
[] sG=3 & !funlock2M1 -> (sG'=4);
[unlock1G] sG=4 -> (sG'=5) & (xG'=0);
[] sG=5 & xG >= 400 -> (sG'=0) & (xG'=0);
endmodule
module mH
xH : clock;
sH : [0..5] init 0;
invariant
(sH=0 => xH<=0) &
(sH=2 => xH<=30) &
(sH=3 => xH<=0) &
(sH=5 => xH<=20)
endinvariant
[lock2H] sH=0 -> (sH'=2) & (xH'=0);
[] sH=0 & !flock2M2 -> (sH'=1);
[lock1H] sH=1 -> (sH'=2) & (xH'=0);
[] sH=2 & xH >= 20 -> (sH'=3) & (xH'=0);
[unlock2H] sH=3 -> (sH'=5) & (xH'=0);
[] sH=3 & !funlock2M2 -> (sH'=4);
[unlock1H] sH=4 -> (sH'=5) & (xH'=0);
[] sH=5 & xH >= 10 -> (sH'=0) & (xH'=0);
endmodule
module mM
xM : clock;
sM : [0..5] init 0;
invariant
(sM=0 => xM<=0) &
(sM=2 => xM<=20) &
(sM=3 => xM<=0) &
(sM=5 => xM<=20)
endinvariant
[lock2M] sM=0 -> (sM'=2) & (xM'=0);
[] sM=0 & !flock2M3 -> (sM'=1);
[lock1M] sM=1 -> (sM'=2) & (xM'=0);
[] sM=2 & xM >= 10 -> (sM'=3) & (xM'=0);
[unlock2M] sM=3 -> (sM'=5) & (xM'=0);
[] sM=3 & !funlock2M3 -> (sM'=4);
[unlock1M] sM=4 -> (sM'=5) & (xM'=0);
[] sM=5 & xM >= 10 -> (sM'=0) & (xM'=0);
endmodule