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, SimulatedAnnealingFrontierStrategy

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 boolean	isRunning
protected org.slf4j.Logger	logger
protected BigraphModelChecker<B>	modelChecker
protected int	occurrenceCounter
protected PredicateChecker<B>	predicateChecker
protected ReactionRuleFilter<B>	reactionRuleFilter
protected BigraphFilter<B>	worklistFilter

Constructor Summary

Constructors

Constructor	Description
ModelCheckingStrategySupport()
ModelCheckingStrategySupport(BigraphModelChecker<B> modelChecker)

Method Summary

Modifier and Type	Method	Description
abstract void	addToWorklist(Collection<B> worklist, B bigraph)
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.
ReactionRuleFilter<B>	getReactionRuleFilter()	Returns the currently configured reaction rule filter.
BigraphFilter<B>	getWorklistFilter()
abstract B	removeNext(Collection<B> worklist)
protected void	resetOccurrenceCounter()
void	setReactionRuleFilter(ReactionRuleFilter<B> filter)	Sets the reaction rule filter used during rule exploration.
void	setWorklistFilter(BigraphFilter<B> filter)	Defaults to BigraphFilter.noop() unless a subclass overrides this to add logic.
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

worklistFilter

protected BigraphFilter<B extends Bigraph<? extends Signature<?>>> worklistFilter

reactionRuleFilter

protected ReactionRuleFilter<B extends Bigraph<? extends Signature<?>>> reactionRuleFilter

isRunning

protected boolean isRunning

Constructor Details

ModelCheckingStrategySupport

public ModelCheckingStrategySupport()

ModelCheckingStrategySupport

public ModelCheckingStrategySupport(BigraphModelChecker<B> modelChecker)

Method Details

createWorklist

public abstract Collection<B> createWorklist()

removeNext

public abstract B removeNext(Collection<B> worklist)

addToWorklist

public 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.

setWorklistFilter

public void setWorklistFilter(BigraphFilter<B> filter)

Defaults to BigraphFilter.noop() unless a subclass overrides this to add logic.

Specified by:

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

Parameters:

filter - the filter to apply, if null, the default noop is used.

getWorklistFilter

public BigraphFilter<B> getWorklistFilter()

Specified by:

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

setReactionRuleFilter

public void setReactionRuleFilter(ReactionRuleFilter<B> filter)

Sets the reaction rule filter used during rule exploration. The filter decides whether a reaction rule should be considered for a given agent before computing matches.

If null is provided, ReactionRuleFilter.alwaysAccept() will be used.

Specified by:

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

Parameters:

filter - the reaction rule filter

getReactionRuleFilter

public ReactionRuleFilter<B> getReactionRuleFilter()

Returns the currently configured reaction rule filter.

Specified by:

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

Returns:

the reaction rule filter

evaluatePredicates

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