Conversion from PARTY LTS into the SPOT automaton

lts_to_spot.py

from itertools import chain
from typing import Union

import spot
import buddy

from interfaces.automata import Label
from interfaces.lts import LTS
from synthesis.funcs_args_types_names import ARG_MODEL_STATE


def lts_to_spot_automaton(lts:LTS, bdict:spot.bdd_dict) -> Union[spot.twa_graph, spot.twa]:
    """ We shift LTS outputs into edge labels
        and treat it as an automaton. """

    # prefix sp_ denotes spot's structure

    sp_atm = spot.make_twa_graph(bdict)  # type: spot.twa_graph
    bdd_by_sig = dict()
    sig_by_bdd = dict()
    for sig in chain(lts.input_signals, lts.output_models.keys()):
        bdd_by_sig[sig] = buddy.bdd_ithvar(sp_atm.register_ap(str(sig)))
        sig_by_bdd[bdd_by_sig[sig]] = sig

    spState_by_ltsState = dict((s, sp_atm.new_state()) for s in lts.states)

    sp_atm.set_init_state(spState_by_ltsState[list(lts.init_states)[0]])

    for lbl, dst in lts.tau_model.items():
        src = lbl[ARG_MODEL_STATE]
        if src not in lts.states:  # unreachable state
            continue

        # (1) (2) creating spot label for the edge from ours inputs and outputs
        sp_lbl = buddy.bddtrue
        # (1) converting inputs
        inputsVal = dict(filter(lambda k_v: k_v[0] != ARG_MODEL_STATE,
                                lbl.items()))
        for sig, val in inputsVal.items():
            sp_lbl &= bdd_by_sig[sig] if val else -bdd_by_sig[sig]
        # (2) converting outputs
        for sig, sig_model in lts.model_by_signal.items():
            val = sig_model[Label({ARG_MODEL_STATE:src})]
            sp_lbl &= bdd_by_sig[sig] if val else -bdd_by_sig[sig]

        sp_atm.new_edge(spState_by_ltsState[src],
                        spState_by_ltsState[dst],
                        sp_lbl)
    sp_atm.merge_edges()  # simplify the edges
    # end of for lts.tau_model.items()
    return sp_atm