Package org.bigraphs.framework.simulation.modelchecking

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

java.lang.Object

org.bigraphs.framework.simulation.modelchecking.ModelCheckingStrategySupport<B>

org.bigraphs.framework.simulation.modelchecking.BreadthFirstStrategy<B>

org.bigraphs.framework.simulation.modelchecking.BFSFirstMatchStrategy<B>

All Implemented Interfaces:

ModelCheckingStrategy<B>

public class BFSFirstMatchStrategy<B extends Bigraph<? extends Signature<?>>>
extends BreadthFirstStrategy<B>

A breadth-first exploration strategy that selects only the first available match in "natural matcher order" for each reaction rule when checking a state. The selected successor is followed exclusively, and no sibling states are explored for that rule (i.e., if the rule produces more occurrences, only the first is selected).

This produces an execution trace consistent with BFS semantics.

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
BFSFirstMatchStrategy(BigraphModelChecker<B> modelChecker)

Method Summary

Modifier and Type	Method	Description
protected MatchIterable<BigraphMatch<B>>	getBigraphMatches(ReactionRule<B> rule, B theAgent)	Return only the first match

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

addToWorklist, createWorklist, removeNext

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

evaluatePredicates, resetOccurrenceCounter, synthesizeTransitionSystem

Methods inherited from class java.lang.Object

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

Constructor Details

BFSFirstMatchStrategy

public BFSFirstMatchStrategy(BigraphModelChecker<B> modelChecker)

Method Details

getBigraphMatches

protected MatchIterable<BigraphMatch<B>> getBigraphMatches(ReactionRule<B> rule,
 B theAgent)

Return only the first match

Overrides:

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

Parameters:

rule -

theAgent -

Returns: