ar/assignments/marble.smv

   1 MODULE main
   2 VAR
   3 a : 0..100;
   4 c : 0..20;
   5 INIT
   6 a = 1 & c = 0
   7 TRANS
   8 case
   9         c<20 : next(c) = c+1;
  10         TRUE : next(c) = c;
  11 esac & (
  12 case
  13         a<100 : next(a) = a+1;
  14         TRUE : next(a)=a;
  15 esac |
  16 case
  17         a<=50 : next(a) = 2*a;
  18         TRUE : next(a)=a;
  19 esac)
  20 LTLSPEC G !(a = 100 & c = 8)