#!/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