Package org.bigraphs.framework.simulation.modelchecking

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

java.lang.Object

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

All Implemented Interfaces:

ModelCheckingStrategy<B>

Direct Known Subclasses:

BreadthFirstStrategy, DepthFirstStrategy, RandomAgentModelCheckingStrategy

public abstract class ModelCheckingStrategySupport<B extends Bigraph<? extends Signature<?>>>
extends Object
implements ModelCheckingStrategy<B>

Base class for supporting model checking strategy implementations. Provides some useful method to keep subclasses simple.

Author:

Dominik Grzelak

See Also:

• BreadthFirstStrategy
• DepthFirstStrategy
• RandomAgentModelCheckingStrategy
• BFSFirstMatchStrategy
• DFSFirstMatchStrategy

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static class	ModelCheckingStrategySupport.MatchResult<B extends Bigraph<? extends Signature<?>>>

Field Summary

Fields

Modifier and Type	Field	Description
protected JLibBigBigraphDecoder	decoder
protected JLibBigBigraphEncoder	encoder
protected org.slf4j.Logger	logger
protected BigraphModelChecker<B>	modelChecker
protected int	occurrenceCounter
protected PredicateChecker<B>	predicateChecker

Constructor Summary

Constructors

Constructor	Description
ModelCheckingStrategySupport(BigraphModelChecker<B> modelChecker)

Method Summary

Modifier and Type	Method	Description
protected abstract void	addToWorklist(Collection<B> worklist, B bigraph)
protected abstract Collection<B>	createWorklist()
protected void	evaluatePredicates(B agent, String canonical, String root)
protected MatchIterable<BigraphMatch<B>>	getBigraphMatches(ReactionRule<B> rule, B theAgent)	Retrieves all matches of the given reaction rule for the provided agent bigraph.
protected abstract B	removeNext(Collection<B> worklist)
protected void	resetOccurrenceCounter()
void	synthesizeTransitionSystem()	Main method for model checking.

Methods inherited from class java.lang.Object

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

Field Details

logger

protected org.slf4j.Logger logger

modelChecker

protected BigraphModelChecker<B extends Bigraph<? extends Signature<?>>> modelChecker

predicateChecker

protected PredicateChecker<B extends Bigraph<? extends Signature<?>>> predicateChecker

occurrenceCounter

protected int occurrenceCounter

decoder

protected JLibBigBigraphDecoder decoder

encoder

protected JLibBigBigraphEncoder encoder

Constructor Details

ModelCheckingStrategySupport

public ModelCheckingStrategySupport(BigraphModelChecker<B> modelChecker)

Method Details

createWorklist

protected abstract Collection<B> createWorklist()

removeNext

protected abstract B removeNext(Collection<B> worklist)

addToWorklist

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

resetOccurrenceCounter

protected void resetOccurrenceCounter()

synthesizeTransitionSystem

public void synthesizeTransitionSystem()

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

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

Specified by:

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

getBigraphMatches

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

Retrieves all matches of the given reaction rule for the provided agent bigraph.

Subclasses may override this method to introduce additional filtering, pruning strategies, or domain-specific constraints on the match set (e.g., restricting matches by attributes, spatial bounds, or metadata).

By default, this method delegates to the underlying AbstractBigraphMatcher.

Parameters:

rule - the reaction rule whose redex will be matched against the agent

theAgent - the agent (host) bigraph in which matches should be searched

Returns:

an iterable collection of all matches found for the given rule on the agent; never null, but may be empty if no matches exist. Depends on AbstractBigraphMatcher.

evaluatePredicates

protected void evaluatePredicates(B agent,
 String canonical,
 String root)