Package eu.iv4xr.framework.extensions.ltl

Class LTL<State>

java.lang.Object
eu.iv4xr.framework.extensions.ltl.SequencePredicate<State>
eu.iv4xr.framework.extensions.ltl.LTL<State>
Direct Known Subclasses:
LTL.And, LTL.Next, LTL.Not, LTL.Now, LTL.Or, LTL.Until, LTL.WeakUntil
public abstract class LTL<State> extends SequencePredicate<State>
Provides a representation LTL formulas and a DSL for constructing them. An LTL formula is a predicate over sequences of states.

Additionally methods are provided to evaluate an LTL formula over a finite sequence of states (evaluating over an infinite sequence is obviously impossible). Evaluating an LTL formula on a sequence sigma means checking whether the formula holds on sigma (whether sigma satisfies the formula). The evaluation results in either SAT, UNSAT, or UNKNOWN if neither SAT nor UNSAT can be decided.

The checking is done recursively over the structure of the LTL, essentially following the recursive 'semantics' of LTL formulas. We start by evaluating the atomic propositions in the formula over the given sequence, and then bottom-up towards the root LTL. The semantics used is mostly as usual, see e.g. Baier's Principles of Model Checking. However, we define the meaning of Xp on [s] (a sequence that contains of only one state) is always UNSAT (even for Xtrue), because the sequence has no next-state. A subtle consequence of this is the property not(X phi), when interpreted over finite sequences, is not equivalent to X(not phi) (which they are, when interpreted on infinite sequences).

For steps needed to evaluate an LTL formula on a sequence, see the documentation of SequencePredicate. This class LTL extends SequencePredicate.

Author:
Wish

  • Nested Class Summary

    Nested Classes
    Modifier and Type
    Class
    Description
    static class 
    LTL.And<State>
     
    (package private) static class 
    LTL.LTLVerdictInfo
     
    static class 
    LTL.Next<State>
     
    static class 
    LTL.Not<State>
     
    static class 
    LTL.Now<State>
     
    static class 
    LTL.Or<State>
    For representing "phi || psi".
    static class 
    LTL.Until<State>
     
    static class 
    LTL.WeakUntil<State>
    Weak-until is not primitive in LTL-sense, but we add it as a separate class so that we can structurally recognize that a formula is a weak-until formula.

  • Field Summary

    Fields
    Modifier and Type
    Field
    Description
    (package private) LinkedList<LTL.LTLVerdictInfo>
    evals
    If sigma is the sequence of states that is under evaluation.
    boolean
    fullyEvaluated
    When the true then this formula is considered to have been fully evaluated.

  • Constructor Summary

    Constructors
    Constructor
    Description
    LTL()
     

  • Method Summary

    Modifier and Type
    Method
    Description
    static <State> LTL<State>
    always​(LTL<State> phi)
    always(phi) constructs the LTL formula "G phi" (also written "[] phi").
    static <State> LTL<State>
    always​(Predicate<State> phi)
    If p is a state-predicate, always(phi) constructs the LTL formula "G now(p)" (also written "[] now(p)").
    void
    checkNext​(State state)
    Use this to check this LTL formula on a sequence of states by feeding the states one state at a time.
    void
    endChecking()
    Call this to mark that the last state of the execution under evaluation has been fed to this predicate.
    (package private) abstract void
    evalAtomSat​(State state)
    Evaluate the atoms of this LTL formula on the given current state, and add the verdict at the end of evals of those atoms.
    static <State> LTL.Until<State>
    eventually​(LTL<State> phi)
    evenatually(phi) constructs the LTL formula "F phi" (also written "diamond phi").
    static <State> LTL.Until<State>
    eventually​(Predicate<State> phi)
    if p is a state-predicate, evenatually(p) constructs the LTL formula "F noq(p)" (also written "diamond now(p)").
    LTL<State>
    implies​(LTL<State> psi)
    phi.implies(psi) constructs the LTL formula "phi --> psi".
    static <State> LTL.And<State>
    ltlAnd​(LTL<State>... phis)
    ltlAnd(phi1, ..., phin ) constructs the LTL formula "phi1 ∧ phi2 ...
    static <State> LTL.Not<State>
    ltlNot​(LTL<State> phi)
    ltlNot(phi) constructs the LTL formula "not phi".
    static <State> LTL.Or<State>
    ltlOr​(LTL<State>... phis)
    ltlOr(phi1, ..., phin ) constructs the LTL formula "phi1 || phi2 ...
    static <State> LTL.Next<State>
    next​(LTL<State> phi)
    If p is a state-predicate, next(p) constructs the LTL formula "X now(p)".
    static <State> LTL.Next<State>
    next​(Predicate<State> phi)
    next(phi) constructs the LTL formula "X phi".
    static <State> LTL.Now<State>
    now​(String name, Predicate<State> p)
     
    static <State> LTL.Now<State>
    now​(Predicate<State> p)
    If p is a state-predicate, this construct the LTL formula "now(p)".
    void
    startChecking()
    Invoke this first before start checking this LTL formula on an execution; this will rest the internal state of this formula, making it ready to check a new sequence.
    abstract LTL<State>
    treeClone()
    Make a clone of this LTL formula.
    LTL.Until<State>
    until​(LTL<State> psi)
    phi.Until(psi) constructs the LTL formula "phi U psi".
    LTL<State>
    until​(Predicate<State> psi)
     
    LTL.WeakUntil<State>
    weakUntil​(LTL<State> psi)
    phi.weakUntil(psi) constructs the LTL formula "phi W psi".
    LTL.WeakUntil<State>
    weakUntil​(Predicate<State> psi)
     

    Methods inherited from class eu.iv4xr.framework.extensions.ltl.SequencePredicate

    sat, sat

    Methods inherited from class java.lang.Object

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

  • Field Details

    • evals

      LinkedList<LTL.LTLVerdictInfo> evals
      If sigma is the sequence of states that is under evaluation. Calling sat() will check/evaluates. This evaluation is recursive over the structure of the LTL formula. To facilitate this, it is necessary to also store intermediate results. This field evals is a sequence, such that evals(i) is the value of this LTL (satisfied or not satisfied) formula, evaluated on the suffix of sigma, starting at sigma(i). (this implies that validity of this LTL on the whole sigma can be obtained by looking at the value of evals(0))

    • fullyEvaluated

      public boolean fullyEvaluated
      When the true then this formula is considered to have been fully evaluated. Invoking sat() will not trigger new-re-evaluation.

  • Constructor Details

    • LTL

      LTL()

  • Method Details

    • evalAtomSat

      abstract void evalAtomSat​(State state)
      Evaluate the atoms of this LTL formula on the given current state, and add the verdict at the end of evals of those atoms.

    • startChecking

      public void startChecking()
      Invoke this first before start checking this LTL formula on an execution; this will rest the internal state of this formula, making it ready to check a new sequence.
      Specified by:
      startChecking in class SequencePredicate<State>

    • checkNext

      public void checkNext​(State state)
      Use this to check this LTL formula 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.
      Specified by:
      checkNext in class SequencePredicate<State>

    • endChecking

      public 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.
      Specified by:
      endChecking in class SequencePredicate<State>

    • treeClone

      public abstract LTL<State> treeClone()
      Make a clone of this LTL formula. The structure will be cloned, but the under lying state predicates are not cloned.

    • until

      public LTL.Until<State> until​(LTL<State> psi)
      phi.Until(psi) constructs the LTL formula "phi U psi".

    • weakUntil

      public LTL.WeakUntil<State> weakUntil​(LTL<State> psi)
      phi.weakUntil(psi) constructs the LTL formula "phi W psi".

    • until

      public LTL<State> until​(Predicate<State> psi)

    • weakUntil

      public LTL.WeakUntil<State> weakUntil​(Predicate<State> psi)

    • implies

      public LTL<State> implies​(LTL<State> psi)
      phi.implies(psi) constructs the LTL formula "phi --> psi".

    • now

      public static <State> LTL.Now<State> now​(Predicate<State> p)
      If p is a state-predicate, this construct the LTL formula "now(p)".

    • now

      public static <State> LTL.Now<State> now​(String name, Predicate<State> p)

    • next

      public static <State> LTL.Next<State> next​(LTL<State> phi)
      If p is a state-predicate, next(p) constructs the LTL formula "X now(p)".

    • next

      public static <State> LTL.Next<State> next​(Predicate<State> phi)
      next(phi) constructs the LTL formula "X phi".

    • ltlNot

      public static <State> LTL.Not<State> ltlNot​(LTL<State> phi)
      ltlNot(phi) constructs the LTL formula "not phi".

    • ltlAnd

      public static <State> LTL.And<State> ltlAnd​(LTL<State>... phis)
      ltlAnd(phi1, ..., phin ) constructs the LTL formula "phi1 ∧ phi2 ... ∧ phin".

    • ltlOr

      public static <State> LTL.Or<State> ltlOr​(LTL<State>... phis)
      ltlOr(phi1, ..., phin ) constructs the LTL formula "phi1 || phi2 ... || phin".

    • eventually

      public static <State> LTL.Until<State> eventually​(LTL<State> phi)
      evenatually(phi) constructs the LTL formula "F phi" (also written "diamond phi").

    • eventually

      public static <State> LTL.Until<State> eventually​(Predicate<State> phi)
      if p is a state-predicate, evenatually(p) constructs the LTL formula "F noq(p)" (also written "diamond now(p)").

    • always

      public static <State> LTL<State> always​(LTL<State> phi)
      always(phi) constructs the LTL formula "G phi" (also written "[] phi").

    • always

      public static <State> LTL<State> always​(Predicate<State> phi)
      If p is a state-predicate, always(phi) constructs the LTL formula "G now(p)" (also written "[] now(p)").