Uses of Interface
dev.civl.gmc.TraceStepIF
Packages that use TraceStepIF
Package
Description
The root package of generic model checking is used to construct model
checking applications, either sequential or concurrent.
This package provides sequential generic model checking functionality.
A simple implementation of General Model Checker (GMC) is used by a set of
code coverage test cases.
-
Uses of TraceStepIF in dev.civl.gmc
Methods in dev.civl.gmc that return TraceStepIFModifier and TypeMethodDescriptionTrace.traceStep(int i) Returns the i'th trace step of this trace.Methods in dev.civl.gmc that return types with arguments of type TraceStepIFModifier and TypeMethodDescriptionTrace.traceSteps()Returns the list of trace steps contained in this trace.Methods in dev.civl.gmc with parameters of type TraceStepIFModifier and TypeMethodDescriptionvoidTrace.addTraceStep(TraceStepIF<STATE> traceStep) Adds a new trace step to this trace. -
Uses of TraceStepIF in dev.civl.gmc.dpor
Methods in dev.civl.gmc.dpor that return TraceStepIFMethods in dev.civl.gmc.dpor with parameters of type TraceStepIFModifier and TypeMethodDescriptionvoidDporNode.cacheTraceStep(TRANSITION transition, TraceStepIF<STATE> traceStep) Accepts a transition and the trace step that it entails and caches this association.DporNodeFactory.getNode(TraceStepIF<STATE> traceStep) Implements the fly-weight pattern and normalize a state. -
Uses of TraceStepIF in dev.civl.gmc.seq
Methods in dev.civl.gmc.seq that return TraceStepIFModifier and TypeMethodDescriptionabstract TraceStepIF<STATE> StateManager.nextState(STATE state, TRANSITION transition) Given a state and a transition, returns the trace step after executing the transition at the given state.abstract TraceStepIF<STATE> StateManager.tryNextState(STATE state, TRANSITION transition) Same asStateManager.nextState(STATE,TRANSITION)except if an error is encountered then it is not reported and null is returnedMethods in dev.civl.gmc.seq with parameters of type TraceStepIFModifier and TypeMethodDescriptionSequentialNodeFactory.getNode(TraceStepIF<STATE> traceStep) Implements the fly-weight pattern and normalize a state.abstract voidStateManager.normalize(TraceStepIF<STATE> traceStep) Normalize/simplify a state.abstract voidStateManager.printTraceStep(STATE sourceState, TraceStepIF<STATE> traceStep) This method should print the source state id and transitions within this traceStep. -
Uses of TraceStepIF in dev.civl.gmc.smc
Classes in dev.civl.gmc.smc that implement TraceStepIFModifier and TypeClassDescriptionclassThe implementation of the interfaceTraceStepIFused by SMC.Methods in dev.civl.gmc.smc that return TraceStepIFModifier and TypeMethodDescriptionSimpleStateManager.tryNextState(Integer state, String transition) Methods in dev.civl.gmc.smc with parameters of type TraceStepIFModifier and TypeMethodDescriptionvoidSimpleStateManager.normalize(TraceStepIF<Integer> traceStep) voidSimpleStateManager.printTraceStep(Integer sourceState, TraceStepIF<Integer> traceStep)