Package eu.iv4xr.framework.extensions.ltl

Class BoundedLTL

java.lang.Object
eu.iv4xr.framework.extensions.ltl.SequencePredicate<Pair<ITransition,​IState>>
eu.iv4xr.framework.extensions.ltl.BoundedLTL
public class BoundedLTL extends SequencePredicate<Pair<ITransition,​IState>>
Bounded LTL is a variation of LTL. So, a BLTL formula is also a sequence predicate. In this particular implementation, the sequence consists of pairs (tr,s) where s represents a state, and tr represents the transition that was done out in the system under evaluation, that results in the state s. A BLTL formula F can be thought a tuple (phi,p,q,n), where phi is an LTL formula, p,q are state-predicates, and n (if provided) is a natural number. To construct F we do: var F = new BoundedLTL() .thereIs(phi) .when(p) .until(q) .withMaxLength(n) ; F is interpreted over a (finite) sequence. Let sigma be a finite sequence. The predicates p and q induce a set of disjoint segments of sigma, such every segment Z: (1) starts with a state satisfying p, (2) Z ends with a state satisfying q (this can coincide with the starting state), (3) the end-state of Z is the only state satisfying q, (3b) if n is given, then additionally Z length should be at most n. (4) Z is maximal in length while maintaining properties 1..3 above. Note that conditions above imply that the segments cannot overlap. Also note that p can holds multiple times within Z, but Z ends at with a q. If p occurs multiple times, Z is maximal in the sense that it starts with the first p before q holds. F holds on the sequence (F is satisfied by the sequence) if the sequence contains such a pq-segment Z such that this Z satisfies ltl. The segment Z can be seen as the witness of this satisfaction. Note that the interpretation of F is indeed existensial (it is satisfied if there is a pq-segment in the sequence that satisfies F's ltl). But we can also check a universal interpretation. To checks whether ALL pq-segment satisfies an ltl-formula phi, we instead check the BLTL (p,q, ltlNot(phi),n)). If this results in UNSAT, the all pq-segments in the target sequence satisfies phi (and else, there is one segment that does not satisfy phi).
Author:
Wish

  • Field Details

  • Constructor Details

    • BoundedLTL

      public BoundedLTL()

  • Method Details

    • thereIs

      public BoundedLTL thereIs​(LTL<IState> F)

    • when

      public BoundedLTL when​(Predicate<IState> p)

    • until

      public BoundedLTL until​(Predicate<IState> q)

    • withMaxLength

      public BoundedLTL withMaxLength​(int n)

    • startChecking

      public void startChecking()
      Invoke this first before start checking this predicate on a sequence; this will reset the state of this bounded LTL checker to its initial internal state.
      Specified by:
      startChecking in class SequencePredicate<Pair<ITransition,​IState>>

    • checkNext

      public void checkNext​(Pair<ITransition,​IState> step)
      Use this to check this BLTL predicate on a sequence of pairs transition-state by feeding it one item 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 item (the current transition-state pair) at a time.
      Specified by:
      checkNext in class SequencePredicate<Pair<ITransition,​IState>>

    • 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<Pair<ITransition,​IState>>

    • sat

      public SATVerdict sat​(List<Pair<ITransition,​IState>> sequence)
      This checks this BLTL formula on the given execution (list of pairs transition-state). The execution is assumed to be complete (that is, we don't wait for more states to extend it). If the execution satisfy this BLTL, this method will return SAT, and the witnessing trace can be obtained. Otherwise it returns UNSAT. The witness is a trace that satisfies this BLTL's interval/segment specification, and on which (on this interval/segment) the LTL part of this BLTL holds. The witness can be obtained through the method getWitness().
      Overrides:
      sat in class SequencePredicate<Pair<ITransition,​IState>>

    • sat

      public SATVerdict sat()
      Return the verdict of the last sat-checking. If it was SAT, then this method returns SAT as well. Else, it returns UNSAT (even if the previous SAT-check returned UNKNOWN; so essentially this method assumes that the last state of the execution under evaluation has been seen).
      Specified by:
      sat in class SequencePredicate<Pair<ITransition,​IState>>

    • getWitness

      public BoundedLTL.WitnessTrace getWitness()
      Return the witnessing trace, if the last sat-checking results in a SAT. Else it returns null.