ar/assignments/4.smv

   1 MODULE main
   2 VAR
   3 a2 : 2..100;
   4 a3 : 3..100;
   5 a4 : 4..100;
   6 a5 : 5..100;
   7 a6 : 6..100;
   8 c : 0..30;
   9 INIT
  10 a2 = 2 & a3 = 3 & a4 = 4 & a5 = 5 & a6 = 6 & c=1
  11 TRANS
  12 next(c)=c+1 & (
  13         next(a2)=1+a3 |
  14         next(a3)=a2+a4 |
  15         next(a4)=a3+a5 |
  16         next(a5)=a4+a6 |
  17         next(a6)=a5+7
  18 )
  19 LTLSPEC G !(
  20         (a2>=50) |
  21         (a3>=50) |
  22         (a4>=50) |
  23         (a5>=50)
  24 )