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