Package org.bigraphs.framework.simulation.modelchecking

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

java.lang.Object

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

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

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

All Implemented Interfaces:

ModelCheckingStrategy<B>

public class DFSFirstMatchStrategy<B extends Bigraph<? extends Signature<?>>>
extends DepthFirstStrategy<B>

A depth-first exploration strategy that selects only the first available match in "natural matcher order" for each reaction rule when checking a state. The strategy descends along this single successor path 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 DFS 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
DFSFirstMatchStrategy(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.DepthFirstStrategy

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

DFSFirstMatchStrategy

public DFSFirstMatchStrategy(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: