Package eu.iv4xr.framework.extensions.ltl

Class BoundedLTL.WitnessTrace

java.lang.Object
eu.iv4xr.framework.extensions.ltl.BoundedLTL.WitnessTrace
Enclosing class:
BoundedLTL
public static class BoundedLTL.WitnessTrace extends Object
Represent a 'trace' of an execution. An execution is a sequence of steps and the states that result from each state. A 'trace' is not literally a sequence of these states, as it might be expensive or not possible to 'remember' states passed during the execution. But rather it only keeps some string 'description' or 'summary' of the states. To be more precise, a witness-trace is a sequence of pairs (tr,s) where tr is the id of a step/transition, and s is a string description of the state after tr.

  • Field Details

    • trace

      List<Pair<String,​String>> trace
      A list of "transition". Every transition is represented by a pair (tr,s) where tr is the id of a transition, and s is a string-dec of the resulting state. The transition tr might be null, if it is not known, or if s represents an initial state (so, it has no transition that precedes it).

  • Constructor Details

    • WitnessTrace

      public WitnessTrace()

  • Method Details

    • register

      public void register​(ITransition transitionLabel, IState resultingState)

    • reset

      public void reset()

    • getState

      public String getState​(int k)

    • getTransitionLabel

      public String getTransitionLabel​(int k)

    • toString

      public String toString()
      Overrides:
      toString in class Object