ar/assignments/4.smv

   1 MODULE main
   2 VAR
   3 a1 : 0..100;
   4 a2 : 0..100;
   5 a3 : 0..100;
   6 a4 : 0..100;
   7 a5 : 0..100;
   8 a6 : 0..100;
   9 a7 : 0..100;
  10 c : 0..25;
  11 INIT
  12 a1 = 1 &
  13 a2 = 2 &
  14 a3 = 3 &
  15 a4 = 4 &
  16 a5 = 5 &
  17 a6 = 6 &
  18 a7 = 7 &
  19 c = 0
  20 TRANS
  21 next(c) = c + 1 & (
  22         next(a2) = a1+a3 |
  23         next(a3) = a2+a4 |
  24         next(a4) = a3+a5 |
  25         next(a5) = a4+a6 |
  26         next(a6) = a5+a7
  27 )
  28 LTLSPEC G !(
  29         c < 10 &
  30         a2>50 & (
  31                 a2=a3 |
  32                 a2=a4 |
  33                 a2=a5 |
  34                 a2=a6
  35         ) |
  36         a3>50 & (
  37                 a3=a4 |
  38                 a3=a5 |
  39                 a3=a6
  40         ) |
  41         a4>50 & (
  42                 a4=a5 |
  43                 a4=a6
  44         ) |
  45         a5>50 & (
  46                 a5=a6
  47         )
  48 )