mirela / scp

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

Upload new file

Inline Side-by-side
Showing 1 changed file with 185 additions and 0 deletions
pta
formula fk1Ca = (sU=1);
formula fk2Ca = (sCa=3);
formula fk1I = (sF=1);
formula fk2I = (sI=3);
formula fk1F = (sL=1);
formula fk2F = (sF=4);
formula fk1U = (sL=1);
formula fk2U = (sU=9);
formula fk1L = (sF=1);
formula fk2L = (sL=9);
formula flock1 = (sU=4) | (sL=4) | (sG=1);
formula flock2 = (sM=1);
formula funlock1 = (sU=7) | (sL=7) | (sG=4);
formula funlock2 = (sM=3);
module mCa
xCa : clock;
sCa : [0..3] init 0;
invariant
(sCa=0 => xCa <= 0) &
(sCa=1 => xCa <= 0) &
(sCa=2 => xCa <= 0)
endinvariant
[] sCa=0 & xCa >= 0 -> (sCa'=1) & (xCa'=0);
[] sCa=1 & xCa >= 0 -> (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 mI
xI : clock;
sI : [0..3] init 0;
invariant
(sI=0 => xI <= 0) &
(sI=1 => xI <= 0) &
(sI=2 => xI <= 0)
endinvariant
[] sI=0 & xI >= 0 -> (sI'=1) & (xI'=0);
[] sI=1 & xI >= 0 -> (sI'=2) & (xI'=0);
[k1I] sI=2 -> (sI'=1) & (xI'=0);
[] sI=2 & !fk1I -> (sI'=3);
[k2I] sI=3 -> (sI'=1) & (xI'=0);
endmodule
module mU
xU : clock;
sU : [0..9] init 0;
invariant
(sU=0 => xU<=0) &
(sU=2 => xU<=0) &
(sU=3 => xU<=0) &
(sU=5 => xU<=0) &
(sU=6 => xU<=0) &
(sU=8 => xU<=0)
endinvariant
[k2Ca] sU=0 -> (sU'=2) & (xU'=0);
[] sU=0 & !fk2Ca -> (sU'=1);
[k1Ca] sU=1 -> (sU'=2) & (xU'=0);
[] sU=2 & xU >= 0 -> (sU'=3) & (xU'=0);
[] sU=3 & !flock2 -> (sU'=4);
[lock2U] sU=3 -> (sU'=5) & (xU'=0);
[lock1U] sU=4 -> (sU'=5) & (xU'=0);
[] sU=5 & xU >= 0 -> (sU'=6) & (xU'=0);
[] sU=6 & !funlock2 -> (sU'=7);
[unlock2U] sU=6 -> (sU'=8) & (xU'=0);
[unlock1U] sU=7 -> (sU'=8) & (xU'=0);
[k2U] sU=8 -> (sU'=0) & (xU'=0);
[] sU=8 & !fk2U -> (sU'=9);
[k1U] sU=9 -> (sU'=0) & (xU'=8);
endmodule
module mF
xF : clock;
sF : [0..4] init 0;
invariant
(sF=0 => xF<=0) &
(sF=2 => xF<=0) &
(sF=3 => xF<=0)
endinvariant
[k2I] sF=0 -> (sF'=2) & (xF'=0);
[k2L] sF=0 -> (sF'=2) & (xF'=0);
[] sF=0 & !fk2I & !fk2L -> (sF'=1);
[k1I] sF=1 -> (sF'=2) & (xF'=0);
[k1L] sF=1 -> (sF'=2) & (xF'=0);
[] sF=2 & xF >= 0 -> (sF'=3) & (xF'=0);
[] sF=3 & !fk1F -> (sF'=4);
[k1F] sF=3 -> (sF'=0) & (xF'=0);
[k2F] sF=4 -> (sF'=0) & (xF'=0);
endmodule
module mL
xL : clock;
sL : [0..9] init 0;
invariant
(sL=0 => xL<=0) &
(sL=2 => xL<=0) &
(sL=3 => xL<=0) &
(sL=5 => xL<=0) &
(sL=6 => xL<=0) &
(sL=8 => xL<=0)
endinvariant
[k2U] sL=0 -> (sL'=2) & (xL'=0);
[k2F] sL=0 -> (sL'=2) & (xL'=0);
[] sL=0 & !fk2U & !fk2F -> (sL'=1);
[k1U] sL=1 -> (sL'=2) & (xL'=0);
[k1F] sL=1 -> (sL'=2) & (xL'=0);
[] sL=2 & xL >= 0 -> (sL'=3) & (xL'=0);
[] sL=3 & !flock2 -> (sL'=4);
[lock2L] sL=3 -> (sL'=5) & (xL'=0);
[lock1L] sL=4 -> (sL'=5) & (xL'=0);
[] sL=5 & xL >= 0 -> (sL'=6) & (xL'=0);
[] sL=6 & !funlock2 -> (sL'=7);
[unlock2L] sL=6 -> (sL'=8) & (xL'=0);
[unlock1L] sL=7 -> (sL'=8) & (xL'=0);
[k2L] sL=8 -> (sL'=0) & (xL'=0);
[] sL=8 & !fk2L -> (sL'=9);
[k1L] sL=9 -> (sL'=0) & (xL'=8);
endmodule
module mM
xM : clock;
sM : [0..3] init 1;
invariant
(sM=0 => xM<=0) &
(sM=2 => xM<=0)
endinvariant
[] sM=0 & !flock1-> (sM'=1);
[lock1L] sM=0 -> (sM'=2) & (xM'=0);
[lock1U] sM=0 -> (sM'=2) & (xM'=0);
[lock1G] sM=0 -> (sM'=2) & (xM'=0);
[lock2L] sM=1 -> (sM'=2) & (xM'=0);
[lock2U] sM=1 -> (sM'=2) & (xM'=0);
[lock2G] sM=1 -> (sM'=2) & (xM'=0);
[] sM=2 & !funlock1 -> (sM'=3);
[unlock1L] sM=2 -> (sM'=0) & (xM'=0);
[unlock1U] sM=2 -> (sM'=0) & (xM'=0);
[unlock1G] sM=2 -> (sM'=0) & (xM'=0);
[unlock2L] sM=3 -> (sM'=0) & (xM'=0);
[unlock2U] sM=3 -> (sM'=0) & (xM'=0);
[unlock2G] sM=3 -> (sM'=0) & (xM'=0);
endmodule
module mG
xG : clock;
sG : [0..5] init 0;
invariant
(sG=0 => xG<=0) &
(sG=2 => xG<=0) &
(sG=3 => xG<=0) &
(sG=5 => xG<=0)
endinvariant
[lock2G] sG=0 -> (sG'=2) & (xG'=0);
[] sG=0 & !flock2 -> (sG'=1);
[lock1G] sG=1 -> (sG'=2) & (xG'=0);
[] sG=2 & xG >= 0 -> (sG'=3) & (xG'=0);
[unlock2G] sG=3 -> (sG'=5) & (xG'=0);
[] sG=3 & !funlock2 -> (sG'=4);
[unlock1G] sG=4 -> (sG'=5) & (xG'=0);
[] sG=5 & xG >= 0 -> (sG'=0) & (xG'=0);
endmodule