repositories
/
master.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
67d257bb289c275712452b04b8c47ba9db9b3e7c
[master.git]
/
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
)