from model_checker.scanner import Scanner
from model_checker.parser import Parser, Errors


class LTLPropertyBase(object):
    """This is a base class that contains information of an LTL property.

    It encapsulates the model-checking part (see check /
    check_incremental), and contains additional information. The
    subclass needs to describe specific APdict to be used.
    """

    #: The atomic propositions dict you must set in the subclass.
    APdict = None

    def __init__(self, LTL_str, penalty, enabled=True):
        """Constructor for LTLPropertyBase. Assumes property does not change,
        but property may be applied to multiple traces.

        Args:
            LTL_str: the human readable string representation of the LTL property
            penalty: the penalty given when the LTL property is violated
        """

        #: This property's checker virtual machine
        self.parser = Parser()

        self.str = LTL_str
        self.penalty = penalty
        self.enabled = enabled

        #: the result of the model checking (TRUE, UNDECIDED, or FALSE) --
        #  see 'check' method below.
        self.result = Parser.UNDECIDED

        #: initialise the Errors class to give meaningful messages when calling parser.SetProperty
        Errors.Init(self.str, "", False, self.parser.getParsingPos,
                    self.parser.errorMessages)

        self.parser.APdict = self.APdict
        self.parser.SetProperty(Scanner(self.str))
        self.result = Parser.UNDECIDED

    def reset_property(self):
        """Resets existing property so that it can be applied to a new sequence
        of states.

        Assumes init_property or check were previously called.
        """
        self.parser.ResetProperty()
        self.result = Parser.UNDECIDED

    def check(self, trace):
        """Checks the LTL property w.r.t. the given trace.

        Args:
            trace: a sequence of states

        Returns:
            result w.r.t. entire trace, in {TRUE, FALSE, UNDECIDED}
        """

        self.result = self.parser.Check(trace)

        return self.result

    def check_incremental(self, state):
        """Checks an initialised property w.r.t. the next state in a trace.
        Assumes init_property or check were previously called.

        Args:
            state: next state (an integer)

        Returns:
            incremental result, in {TRUE, FALSE, UNDECIDED}
        """

        self.result = self.parser.CheckIncremental(state)

        return self.result