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 Summary
Constructors Constructor Description Trace(ConcreteState initialConcreteState)
Trace(ConcreteState initialConcreteState, SymbolicState initialSymbolicState)
Trace(SymbolicState initialSymbolicState)
-
Method Summary
All Methods Instance Methods Concrete Methods Modifier and Type Method Description void
append(SystemEdgeSelect[] transitionEdges, SymbolicState symbolicState)
void
append(BigDecimal delay, SystemEdgeSelect[] transitionEdges, ConcreteState concreteState)
void
append(BigDecimal delay, SystemEdgeSelect[] transitionEdges, ConcreteState concreteState, SymbolicState symbolicState)
void
clearAfterState(int i)
ConcreteState
getConcreteState(int i)
BigDecimal
getDelay(int i)
BigDecimal
getEntryTime(int i)
SymbolicState
getSymbolicState(int i)
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.SystemEdgeSelect[]
getTransitionEdges(int i)
void
reset(ConcreteState initialConcreteState, SymbolicState initialSymbolicState)
Resets the trace with the given parameters.int
size()
-
-
-
Constructor Detail
-
Trace
public Trace(SymbolicState initialSymbolicState)
-
Trace
public Trace(ConcreteState initialConcreteState)
-
Trace
public Trace(ConcreteState initialConcreteState, SymbolicState initialSymbolicState)
-
-
Method Detail
-
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()
-
-