Package org.bigraphs.framework.simulation.modelchecking

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

java.lang.Object

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

Direct Known Subclasses:

PureBigraphModelChecker

public abstract class BigraphModelChecker<B extends Bigraph<? extends Signature<?>>>
extends Object

A bigraph model checker that allows to simulate a BRS by reaction rules. A reactive system, the strategy and options must be provided.

The model checker allows to react on live predicate matches in the course of the simulation by listeners. They can also be evaluated later by getting the reaction graph/system.

Author:

Dominik Grzelak

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static interface	BigraphModelChecker.ReactiveSystemListener<B extends Bigraph<? extends Signature<?>>>
static class	BigraphModelChecker.SimulationStrategy	Enum-like class that holds all kind of simulations.

Field Summary

Fields

Modifier and Type	Field	Description
protected BigraphCanonicalForm	canonicalForm
protected ModelCheckingStrategy<B>	modelCheckingStrategy
protected ModelCheckingOptions	options
protected PredicateChecker<B>	predicateChecker
protected BigraphModelChecker.ReactiveSystemListener<B>	reactiveSystemListener
protected BigraphModelChecker.SimulationStrategy.Type	simulationStrategyType

Constructor Summary

Constructors

Constructor	Description
BigraphModelChecker(ReactiveSystem<B> reactiveSystem, BigraphModelChecker.SimulationStrategy.Type simulationStrategyType, ModelCheckingOptions options)
BigraphModelChecker(ReactiveSystem<B> reactiveSystem, BigraphModelChecker.SimulationStrategy.Type simulationStrategyType, ModelCheckingOptions options, BigraphModelChecker.ReactiveSystemListener<B> listener)
BigraphModelChecker(ReactiveSystem<B> reactiveSystem, ModelCheckingOptions options)

Method Summary

Modifier and Type	Method	Description
BigraphCanonicalForm	acquireCanonicalForm()
protected void	assertReactionSystemValid()	Performs some checks if the reactive system is valid.
void	execute()	Perform the simulation based on the provided reactive system and options.
Future<ReactionGraph<B>>	executeAsync()	Asynchronously start the simulation based on the provided reactive system and options.
void	exportReactionGraph(ReactionGraph<B> reactionGraph)
protected String	exportState(B bigraph, String canonicalForm, String suffix)
AbstractBigraphMatcher<B>	getMatcher()
List<ReactiveSystemPredicate<B>>	getPredicates()
ReactionGraph<B>	getReactionGraph()
ReactiveSystem<B>	getReactiveSystem()
BigraphModelChecker<B>	setReactiveSystemListener(BigraphModelChecker.ReactiveSystemListener<B> reactiveSystemListener)
<A> A	watch(Supplier<A> function)

Methods inherited from class java.lang.Object

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

Field Details

modelCheckingStrategy

protected ModelCheckingStrategy<B extends Bigraph<? extends Signature<?>>> modelCheckingStrategy

simulationStrategyType

protected BigraphModelChecker.SimulationStrategy.Type simulationStrategyType

reactiveSystemListener

protected BigraphModelChecker.ReactiveSystemListener<B extends Bigraph<? extends Signature<?>>> reactiveSystemListener

canonicalForm

protected BigraphCanonicalForm canonicalForm

predicateChecker

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

options

protected ModelCheckingOptions options

Constructor Details

BigraphModelChecker

public BigraphModelChecker(ReactiveSystem<B> reactiveSystem,
 ModelCheckingOptions options)

BigraphModelChecker

public BigraphModelChecker(ReactiveSystem<B> reactiveSystem,
 BigraphModelChecker.SimulationStrategy.Type simulationStrategyType,
 ModelCheckingOptions options)

BigraphModelChecker

public BigraphModelChecker(ReactiveSystem<B> reactiveSystem,
 BigraphModelChecker.SimulationStrategy.Type simulationStrategyType,
 ModelCheckingOptions options,
 BigraphModelChecker.ReactiveSystemListener<B> listener)

Method Details

acquireCanonicalForm

public BigraphCanonicalForm acquireCanonicalForm()

execute

public void execute()
             throws BigraphSimulationException,
ReactiveSystemException

Perform the simulation based on the provided reactive system and options.

Throws:

BigraphSimulationException - if agent is null or the simulation strategy was not selected

ReactiveSystemException

executeAsync

public Future<ReactionGraph<B>> executeAsync()
                                      throws BigraphSimulationException,
ReactiveSystemException

Asynchronously start the simulation based on the provided reactive system and options.

Throws:

BigraphSimulationException - if agent is null or the simulation strategy was not selected

ReactiveSystemException

assertReactionSystemValid

protected void assertReactionSystemValid()
                                  throws ReactiveSystemException

Performs some checks if the reactive system is valid.

Throws:

BigraphSimulationException - if the system is not valid

ReactiveSystemException

getReactiveSystem

public ReactiveSystem<B> getReactiveSystem()

getPredicates

public List<ReactiveSystemPredicate<B>> getPredicates()

getMatcher

public AbstractBigraphMatcher<B> getMatcher()

getReactionGraph

public ReactionGraph<B> getReactionGraph()

watch

public <A> A watch(Supplier<A> function)

exportState

protected String exportState(B bigraph,
 String canonicalForm,
 String suffix)

exportReactionGraph

public void exportReactionGraph(ReactionGraph<B> reactionGraph)
                         throws IOException

Throws:

IOException

setReactiveSystemListener

public BigraphModelChecker<B> setReactiveSystemListener(BigraphModelChecker.ReactiveSystemListener<B> reactiveSystemListener)