MODULE main
VAR
-a1 : 0..100;
-a2 : 0..100;
-a3 : 0..100;
-a4 : 0..100;
-a5 : 0..100;
-a6 : 0..100;
-a7 : 0..100;
+a2 : 2..100;
+a3 : 3..100;
+a4 : 4..100;
+a5 : 5..100;
+a6 : 6..100;
c : 0..25;
INIT
-a1 = 1 &
-a2 = 2 &
-a3 = 3 &
-a4 = 4 &
-a5 = 5 &
-a6 = 6 &
-a7 = 7 &
-c = 0
+a2 = 2 & a3 = 3 & a4 = 4 & a5 = 5 & a6 = 6 & c=1
TRANS
-next(c) = c + 1 & (
- next(a2) = a1+a3 |
- next(a3) = a2+a4 |
- next(a4) = a3+a5 |
- next(a5) = a4+a6 |
- next(a6) = a5+a7
+next(c)=c+1 & (
+ next(a2)=1+a3 |
+ next(a3)=a2+a4 |
+ next(a4)=a3+a5 |
+ next(a5)=a4+a6 |
+ next(a6)=a5+7
)
LTLSPEC G !(
- c < 10 &
- a2>50 & (
- a2=a3 |
- a2=a4 |
- a2=a5 |
- a2=a6
- ) |
- a3>50 & (
- a3=a4 |
- a3=a5 |
- a3=a6
- ) |
- a4>50 & (
- a4=a5 |
- a4=a6
- ) |
- a5>50 & (
- a5=a6
- )
+ (a2>=50) |
+ (a3>=50) |
+ (a4>=50) |
+ (a5>=50)
)