Commit 2a28638a authored by Benoit Barbot's avatar Benoit Barbot
Browse files

prog

parent 32b9e98a
Pipeline #2141 passed with stages
in 2 minutes and 34 seconds
pta
module m
s : [0..6] init 0;
x: clock;
x1 : clock;
x2 : clock;
x3 : clock;
x4 : clock;
invariant
(x<2) & (x1<6) & (x2<6) & (x3<6) & (x4<6)
endinvariant
[b] (s=0) -> (s'=1) & (x'=0) & (x1'=0) ;
[c] (s=1) -> (s'=2) & (x'=0) & (x2'=0) ;
[d] (s=2) -> (s'=3) & (x'=0) & (x3'=0) ;
[a] (s=3) & (x4>1) -> (s'=4) & (x'=0) & (x4'=0) ;
[b] (s=4) & (x1>1) -> (s'=5) & (x'=0) & (x1'=0) ;
[c] (s=5) & (x2>1) -> (s'=6) & (x'=0) & (x2'=0) ;
[d] (s=6) & (x3>1) -> (s'=3) & (x'=0) & (x3'=0) ;
endmodule
label "accepting" = (s!=6)&(s!=4);
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment