Package com.uppaal.model.system

Class Trace

java.lang.Object
com.uppaal.model.system.Trace
public class Trace
extends Object
This class can be used for a combinated symbolic and concrete trace, or just one of them.

  • Constructor Details

  • Method Details

    • reset

      public void reset​(ConcreteState initialConcreteState, SymbolicState initialSymbolicState)
      Resets the trace with the given parameters. Set both parameters to initialize a combined symbolic and concrete trace. If both parameters are null the trace will be useless, and the append methods will throw IllegalStateExceptions.
      Parameters:
      initialConcreteState - the initial concrete state. If null this trace will not be concrete.
      initialSymbolicState - the initial symbolic state. If null this trace will not be symbolic.

    • clearAfterState

      public void clearAfterState​(int i)

    • append

      public void append​(BigDecimal delay, SystemEdgeSelect[] transitionEdges, ConcreteState concreteState, SymbolicState symbolicState)

    • append

      public void append​(BigDecimal delay, SystemEdgeSelect[] transitionEdges, ConcreteState concreteState)

    • append

      public void append​(SystemEdgeSelect[] transitionEdges, SymbolicState symbolicState)

    • getEntryTime

      public BigDecimal getEntryTime​(int i)

    • getDelay

      public BigDecimal getDelay​(int i)
      Returns:
      The i'th delay. Null if the i'th delay is undefined.

    • getTransitionEdges

      public SystemEdgeSelect[] getTransitionEdges​(int i)

    • getSymbolicTransition

      public SymbolicTransition getSymbolicTransition​(int i)
      Warning: In this representation of the trace, all transitions have a source and a destination, meaning that compared with the old symbolic trace representation, the initial transition is missing. The initial transition was a (null,null,initialState) transition and was a hack necessary only in the old symbolic trace representation. Therefore it will not be reflected by this new trace representation. This warning can be removed when all of the old symbolic trace is gone.
      Returns:
      The i'th symbolic transition. Null if the i'th symbolic transition is undefined.

    • getConcreteState

      public ConcreteState getConcreteState​(int i)

    • getSymbolicState

      public SymbolicState getSymbolicState​(int i)

    • size

      public int size()