java.lang.Object
org.bigraphs.framework.simulation.modelchecking.ModelCheckingStrategySupport<B>
org.bigraphs.framework.simulation.modelchecking.RandomAgentModelCheckingStrategy<B>
- All Implemented Interfaces:
ModelCheckingStrategy<B>
public class RandomAgentModelCheckingStrategy<B extends Bigraph<? extends Signature<?>>>
extends ModelCheckingStrategySupport<B>
Random state-space traversal without cycle-checking and predicate evaluation.
- Author:
- Dominik Grzelak
-
Nested Class Summary
Nested classes/interfaces inherited from class org.bigraphs.framework.simulation.modelchecking.ModelCheckingStrategySupport
ModelCheckingStrategySupport.MatchResult<B extends Bigraph<? extends Signature<?>>> -
Field Summary
Fields inherited from class org.bigraphs.framework.simulation.modelchecking.ModelCheckingStrategySupport
decoder, encoder, logger, modelChecker, occurrenceCounter, predicateChecker -
Constructor Summary
Constructors -
Method Summary
Modifier and TypeMethodDescriptionprotected voidaddToWorklist(Collection<B> worklist, B bigraph) protected Collection<B> protected BremoveNext(Collection<B> worklist) voidMain method for model checking.Methods inherited from class org.bigraphs.framework.simulation.modelchecking.ModelCheckingStrategySupport
evaluatePredicates, resetOccurrenceCounter
-
Constructor Details
-
RandomAgentModelCheckingStrategy
-
-
Method Details
-
synthesizeTransitionSystem
public void synthesizeTransitionSystem()Description copied from class:ModelCheckingStrategySupportMain method for model checking. The mode of traversal can be changed by implementing theModelCheckingStrategySupport.createWorklist()andModelCheckingStrategySupport.removeNext(Collection)methods.Alternatively, the #synthesizeTransitionSystem() method can be simply overridden.
- Specified by:
synthesizeTransitionSystemin interfaceModelCheckingStrategy<B extends Bigraph<? extends Signature<?>>>- Overrides:
synthesizeTransitionSystemin classModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>
-
createWorklist
- Specified by:
createWorklistin classModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>
-
removeNext
- Specified by:
removeNextin classModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>
-
addToWorklist
- Specified by:
addToWorklistin classModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>
-