Package eu.iv4xr.framework.extensions.ltl

Class SequencePredicate<State>

java.lang.Object
eu.iv4xr.framework.extensions.ltl.SequencePredicate<State>
Direct Known Subclasses:
BoundedLTL, LTL
public abstract class SequencePredicate<State> extends Object
An abstract class representing a predicate over finite sequences, defining a minimum interface needed to evaluate such a predicate on a given sequence. The class itself does not provide an implementation for the predicate.

Since we typically use such a sequence to represent an execution of some system through a series of states, elements of the sequence will be called 'states'. These states can be thought as representing the series of states passed by some execution of a system. Note this class does not in itself restrict what a 'state' is. For example, if we need to express a predicate over pairs of (transition,state), then we can use a sequence of such pairs as our 'path'.

Two modes for checking/evaluating a sequence predicate on a sequence are supported:

  • (1) Invoke sat(List), giving the sequence to it.
  • (2) However, giving a sequence of states is not always possible. Assuming we can still give the states one at a time, we can do the checking incrementally like this:
    1. (a) invoke startChecking()
    2. (b) feed the state one at a time using checkNext(Object)
    3. (c) when there is no more state to check (so, we are at the end of the sequence), invoke endChecking()
    4. (d) invoke sat() to get the result.
Author:
Wish

  • Constructor Summary

    Constructors
    Constructor
    Description
    SequencePredicate()
     

  • Method Summary

    Modifier and Type
    Method
    Description
    abstract void
    checkNext​(State state)
    Use this to check this predicate on a sequence of states by feeding the states one state at a time.
    abstract void
    endChecking()
    Call this to mark that the last state of the execution under evaluation has been fed to this predicate.
    abstract SATVerdict
    sat()
    Return the result of the checking whether this predicate holds on the last sequence given to it.
    SATVerdict
    sat​(List<State> sequenceOfStates)
    Check is the given sequence of states (representing some execution) satisfies this LTL formula.
    abstract void
    startChecking()
    Invoke this first before start checking this predicate on a sequence.

    Methods inherited from class java.lang.Object

    clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

  • Constructor Details

    • SequencePredicate

      public SequencePredicate()

  • Method Details

    • startChecking

      public abstract void startChecking()
      Invoke this first before start checking this predicate on a sequence.

    • checkNext

      public abstract void checkNext​(State state)
      Use this to check this predicate on a sequence of states by feeding the states one state at a time. The typical setup is if the execution under evaluation does not allow states to be serialized or cloned. This means that we cannot collect those states in some collection and therefore the execution has to be checked incrementally by feeding this predicate one state (the current state) at a time.

    • endChecking

      public abstract void endChecking()
      Call this to mark that the last state of the execution under evaluation has been fed to this predicate. So, we can now call sat() to inspect whether this predicate holds on the execution or not.

    • sat

      public abstract SATVerdict sat()
      Return the result of the checking whether this predicate holds on the last sequence given to it. The the sequence was given one state at a time using checkNext(), sat() should be called after endChecking() was called.
      • The method returns SAT if this predicate holds on the sequence (it is satisfied by the sequence):
      • UNSAT if the sequence does not satisfy this predicate.
      • UNKNOWN if neither SAT nor UNSAT can be decided.

    • sat

      public SATVerdict sat​(List<State> sequenceOfStates)
      Check is the given sequence of states (representing some execution) satisfies this LTL formula. This method will implicitly call startChecking() and endChecking(). A verdict is returned, saying whether this predicate holds on the given sequence.
      • The method returns SAT if this predicate holds on the sequence (it is satisfied by the sequence).
      • UNSAT if the sequence does not satisfy this predicate.
      • UNKNOWN if neither SAT nor UNSAT can be decided.
      Note that the states in the sequence typically represent the states of some system at different points in time, and as such they should not contain shared sub-objects, or else the evaluation a sequence predicate may give an unsound result.