repositories
/
master.git
/ blob
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
history
|
raw
|
HEAD
update
[master.git]
/
ar
/
assignments
/
4a.smv
1
MODULE main
2
VAR
3
a2 : 2..65;
4
a3 : 3..65;
5
a4 : 4..65;
6
a5 : 5..65;
7
a6 : 6..65;
8
c : 0..15;
9
INIT
10
a2 = 2 & a3 = 3 & a4 = 4 & a5 = 5 & a6 = 6 & c = 0
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 & (a2=a3 | a2=a4 | a2=a5 | a2=a6)) |
21
(a3>=50 & (a3=a4 | a3=a5 | a3=a6)) |
22
(a4>=50 & (a4=a5 | a4=a6)) |
23
(a5>=50 & (a5=a6))
24
)