a2/src/4.smv

   1 MODULE main
   2 VAR
   3 p1: boolean;
   4 p2: boolean;
   5 INIT
   6 p1=TRUE & p2=TRUE & p3=TRUE &
   7 p4=TRUE & p5=TRUE & p6=TRUE &
   8
   9 p7=TRUE & p8=TRUE &
  10         p9=TRUE & p10=TRUE & p11=TRUE &
  11         p12=TRUE & p13=TRUE &
  12 p14=TRUE & p15=TRUE &
  13         p16=TRUE & p17=TRUE & p18=TRUE &
  14         p19=TRUE & p20=TRUE &
  15 p21=TRUE & p22=TRUE & p23=TRUE &
  16         p24=TRUE & p25=TRUE & p26=TRUE &
  17         p27=TRUE & p28=TRUE &
  18
  19 p29=TRUE & p30=TRUE & p31=TRUE &
  20 p32=TRUE & p33=TRUE & p34=TRUE
  21 TRANS
  22 next(p1)=TRUE &
  23 next(p2)=TRUE
  24 LTLSPEC G !(p1=FALSE)