MODEL = """
------------------------------------------------------------------------
-- Generated using Kripkomat
------------------------------------------------------------------------
MODULE {name}
VAR
state : {{ {states} }};
ASSIGN
    init(state) := {initial};
    next(state) :=
        case
{transitions}
        esac;
DEFINE
{properties}
"""

TRAN = "            state = {n} : {{{ms}}};"
PROP = """    -- Property "{prop}"
    {alias} := {logic};
"""
PROP_LOGIC = "state = {state}"

LTL_FORM = """LTLSPEC
    {ltl};
"""

class ModelBuilder:
    def __init__(self, states, initial, transitions, properties, ltls=[], name="main"):
        self._name = name
        self._states = states
        self._initial = initial
        self._tran = transitions
        self._props = properties
        self._ltls = ltls

    def generate(self):
        # build model
        states_decl = ",".join(self._states)
        transitions = []

        for n,ms in self._tran.items():
            transition = TRAN.format(n=n, ms=",".join(ms))
            transitions.append(transition)

        properties = []
        for alias,(states,prop) in self._props.items():
            logic = " | ".join([PROP_LOGIC.format(state=x) for x in states])
            prop_str = PROP.format(prop=prop, alias=alias, logic=logic)
            properties.append(prop_str)

        out = MODEL.format(name=self._name,
                            states=states_decl,
                            initial=self._initial,
                            transitions="\n".join(transitions),
                            properties="\n".join(properties))

        # add LTL formulas
        for ltl in self._ltls:
            out += LTL_FORM.format(ltl=ltl)
        return out