Skip to content
Snippets Groups Projects

Breach stuff

Merged Benoit Barbot requested to merge breach_stuff into master
7 files
+ 207
5
Compare changes
  • Side-by-side
  • Inline
Files
7
+ 26
0
pta
module controller
s : [0..6] init 0;
x: clock;
x1 : clock;
x2 : clock;
x3 : clock;
x4 : clock;
invariant
(x<=4) & (x1<=12) & (x2<=12) & (x3<=12) & (x4<=12)
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>=8) -> (s'=4) & (x'=0) & (x4'=0) ;
[b] (s=4) & (x1>=8) -> (s'=5) & (x'=0) & (x1'=0) ;
[c] (s=5) & (x2>=8) -> (s'=6) & (x'=0) & (x2'=0) ;
[d] (s=6) & (x3>=8) -> (s'=3) & (x'=0) & (x3'=0) ;
endmodule
Loading