java.lang.Object
org.bigraphs.framework.simulation.modelchecking.ModelCheckingStrategySupport<B>
org.bigraphs.framework.simulation.modelchecking.BreadthFirstStrategy<B>
- All Implemented Interfaces:
ModelCheckingStrategy<B>
public class BreadthFirstStrategy<B extends Bigraph<? extends Signature<?>>>
extends ModelCheckingStrategySupport<B>
The algorithm implemented here to synthesize the "reaction graph" is adopted from [1].
It is a breadth-first simulation, which also checks some given predicates.
It also detects cycles.
This algorithm can be used to conduct reachability analysis.
- Author:
- Dominik Grzelak
- See Also:
-
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 void
addToWorklist
(Collection<B> worklist, B bigraph) protected Collection
<B> protected B
removeNext
(Collection<B> worklist) Methods inherited from class org.bigraphs.framework.simulation.modelchecking.ModelCheckingStrategySupport
evaluatePredicates, resetOccurrenceCounter, synthesizeTransitionSystem
-
Constructor Details
-
BreadthFirstStrategy
-
-
Method Details
-
createWorklist
- Specified by:
createWorklist
in classModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>
-
removeNext
- Specified by:
removeNext
in classModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>
-
addToWorklist
- Specified by:
addToWorklist
in classModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>
-