Uses of Interface
dev.civl.mc.semantics.IF.Transition
Packages that use Transition
Package
Description
Module kripke provides the definition of various
transitions and the enabler and state manager of CIVL.
Module semantics implements the semantics of CIVL-C.
-
Uses of Transition in dev.civl.mc.kripke.IF
Methods in dev.civl.mc.kripke.IF that return TransitionModifier and TypeMethodDescriptionAtomicStep.getTransition()Returns the transition associated to this atomic step.Methods in dev.civl.mc.kripke.IF that return types with arguments of type TransitionModifier and TypeMethodDescriptionLibraryEnabler.enabledTransitions(State state, CallOrSpawnStatement call, dev.civl.sarl.IF.expr.BooleanExpression pathCondition, int pid) Computes the enabled transitions of a given function call.static dev.civl.gmc.dpor.DependencyAnalyzer<State, Transition> Kripkes.newDependencyAnalyzer(dev.civl.gmc.seq.StateManager<State, Transition> manager, StateFactory stateFactory, dev.civl.mc.kripke.common.SimpleEnabler enabler) Method parameters in dev.civl.mc.kripke.IF with type arguments of type TransitionModifier and TypeMethodDescriptionstatic dev.civl.gmc.dpor.DependencyAnalyzer<State, Transition> Kripkes.newDependencyAnalyzer(dev.civl.gmc.seq.StateManager<State, Transition> manager, StateFactory stateFactory, dev.civl.mc.kripke.common.SimpleEnabler enabler) -
Uses of Transition in dev.civl.mc.semantics.IF
Methods in dev.civl.mc.semantics.IF that return TransitionModifier and TypeMethodDescriptionstatic TransitionSemantics.newTransition(int pid, dev.civl.sarl.IF.expr.BooleanExpression clause, Statement statement) Creates a new regularTransitionwhose statement will be executed by executor.static TransitionSemantics.newTransition(int pid, dev.civl.sarl.IF.expr.BooleanExpression clause, Statement statement, boolean simplifyState) Creates a new regularTransitionwhose statement will be executed by executor.Methods in dev.civl.mc.semantics.IF with parameters of type TransitionModifier and TypeMethodDescriptionExecutor.execute(State state, int pid, Transition transition) Returns the state that results from executing the statement, or null if path condition becomes unsatisfiable.