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

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 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<?>>>

evaluatePredicates

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