LTL_property_base.py 2.47 KB
Newer Older
Aravind Bk's avatar
Aravind Bk committed
1 2 3 4 5 6 7
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.

Ashish Gaurav's avatar
Ashish Gaurav committed
8 9 10
    It encapsulates the model-checking part (see check /
    check_incremental), and contains additional information. The
    subclass needs to describe specific APdict to be used.
Aravind Bk's avatar
Aravind Bk committed
11
    """
Ashish Gaurav's avatar
Ashish Gaurav committed
12

Aravind Bk's avatar
Aravind Bk committed
13 14 15 16
    #: The atomic propositions dict you must set in the subclass.
    APdict = None

    def __init__(self, LTL_str, penalty, enabled=True):
Ashish Gaurav's avatar
Ashish Gaurav committed
17 18
        """Constructor for LTLPropertyBase. Assumes property does not change,
        but property may be applied to multiple traces.
Aravind Bk's avatar
Aravind Bk committed
19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34

        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
Ashish Gaurav's avatar
Ashish Gaurav committed
35

Aravind Bk's avatar
Aravind Bk committed
36 37 38 39 40 41 42 43 44
        #: 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):
Ashish Gaurav's avatar
Ashish Gaurav committed
45 46 47 48
        """Resets existing property so that it can be applied to a new sequence
        of states.

        Assumes init_property or check were previously called.
Aravind Bk's avatar
Aravind Bk committed
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65
        """
        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
Ashish Gaurav's avatar
Ashish Gaurav committed
66

Aravind Bk's avatar
Aravind Bk committed
67 68
    def check_incremental(self, state):
        """Checks an initialised property w.r.t. the next state in a trace.
Ashish Gaurav's avatar
Ashish Gaurav committed
69 70
        Assumes init_property or check were previously called.

Aravind Bk's avatar
Aravind Bk committed
71 72
        Args:
            state: next state (an integer)
Ashish Gaurav's avatar
Ashish Gaurav committed
73

Aravind Bk's avatar
Aravind Bk committed
74 75 76
        Returns:
            incremental result, in {TRUE, FALSE, UNDECIDED}
        """
Ashish Gaurav's avatar
Ashish Gaurav committed
77

Aravind Bk's avatar
Aravind Bk committed
78
        self.result = self.parser.CheckIncremental(state)
Ashish Gaurav's avatar
Ashish Gaurav committed
79

Aravind Bk's avatar
Aravind Bk committed
80
        return self.result