Package org.bigraphs.framework.simulation.modelchecking

Class RandomAgentModelCheckingStrategy<B extends Bigraph<? extends Signature<?>>>

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

Constructor	Description
RandomAgentModelCheckingStrategy(BigraphModelChecker<B> modelChecker)

Method Summary

Modifier and Type	Method	Description
protected void	addToWorklist(Collection<B> worklist, B bigraph)
protected Collection<B>	createWorklist()
protected B	removeNext(Collection<B> worklist)
void	synthesizeTransitionSystem()	Main method for model checking.

Methods inherited from class org.bigraphs.framework.simulation.modelchecking.ModelCheckingStrategySupport

evaluatePredicates, resetOccurrenceCounter

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

RandomAgentModelCheckingStrategy

public RandomAgentModelCheckingStrategy(BigraphModelChecker<B> modelChecker)

Method Details

synthesizeTransitionSystem

public void synthesizeTransitionSystem()

Description copied from class: ModelCheckingStrategySupport

Main method for model checking. The mode of traversal can be changed by implementing the ModelCheckingStrategySupport.createWorklist() and ModelCheckingStrategySupport.removeNext(Collection) methods.

Alternatively, the #synthesizeTransitionSystem() method can be simply overridden.

Specified by:

synthesizeTransitionSystem in interface ModelCheckingStrategy<B extends Bigraph<? extends Signature<?>>>

Overrides:

synthesizeTransitionSystem in class ModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>

createWorklist

protected Collection<B> createWorklist()

Specified by:

createWorklist in class ModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>

removeNext

protected B removeNext(Collection<B> worklist)

Specified by:

removeNext in class ModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>

addToWorklist

protected void addToWorklist(Collection<B> worklist,
 B bigraph)

Specified by:

addToWorklist in class ModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>