blob: 5337219a858199791b2a1c8e322787bce5c75339 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
|
#!/usr/bin/env python
# Usage for 4b (where 100 is the maximum value for the values):
# $0 100 | nusmv /dev/stdin
import sys
n = 8
maxValue = int(sys.argv[1])
is_b = len(sys.argv) >= 3 and sys.argv[2] == 'b'
def fillin(cases, template_vars):
if type(cases) == str:
return cases.format(**template_vars)
return [template.format(**template_vars) for template in cases]
variables = ["a%d" % i for i in range(1, n+1)]
# vars: a_1 .. a_n
varDefs = " ".join("%s : 0..%d;" % (x, maxValue) for x in variables)
# initial values: a_i = i
initVals = ""
initVals += " & ".join("%s = %d" % (var, i + 1) for i, var in enumerate(variables))
# Transitions:
# - any of the alternatives: sum one, keep others.
trans = "next(a1) = a1 & next(a{n}) = a{n} & (\n".format(n=n)
# The first and last one cannot be changed. In a step, one can choose to
# change a_i for any i, leaving all other j (i != j) intact.
altpreds = []
for i in range(2, n):
prev = i - 1
next = i + 1
# Require a'_i = a_{i-1} + a_{i+1}
statepreds = fillin([
"next(a{i}) = a{prev} + a{next}"
], vars())
# Require a'_j = a_j for i != j
for j in range(2, n):
if i == j:
continue
statepreds += fillin([
"next(a{j}) = a{j}"
], vars())
altpreds += [
"(%s)" % " & ".join(statepreds)
]
trans += "|\n".join(altpreds)
trans += ")"
# Desired condition
if not is_b:
spec = "! (a3 = a7)"
else:
spec = "! (a3 = a5 & a5 = a7)"
# Begin generator
s = """MODULE main
VAR
{varDefs}
INIT
{initVals}
TRANS
{trans}
LTLSPEC G {spec}
""".format(**vars())
try:
import sys
print(s)
# Hack to avoid printing a ugly error in case stdin of next pipe is closed.
sys.stdout.flush()
sys.stdout.close()
except BrokenPipeError:
pass
|
