java.lang.Object
org.bigraphs.framework.simulation.modelchecking.BigraphModelChecker<B>
- Direct Known Subclasses:
PureBigraphModelChecker
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 ClassesModifier and TypeClassDescriptionstatic interface
BigraphModelChecker.ReactiveSystemListener<B extends Bigraph<? extends Signature<?>>>
static class
Enum-like class that holds all kind of simulations. -
Field Summary
FieldsModifier and TypeFieldDescriptionprotected BigraphCanonicalForm
protected ModelCheckingStrategy<B>
protected ModelCheckingOptions
protected PredicateChecker<B>
protected BigraphModelChecker.ReactiveSystemListener<B>
-
Constructor Summary
ConstructorsConstructorDescriptionBigraphModelChecker
(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 TypeMethodDescriptionprotected void
Performs some checks if the reactive system is valid.void
execute()
Perform the simulation based on the provided reactive system and options.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) Exports a bigraph to the filesystem using the export options setting from the member variableoptions
.setReactiveSystemListener
(BigraphModelChecker.ReactiveSystemListener<B> reactiveSystemListener) <A> A
-
Field Details
-
modelCheckingStrategy
-
simulationStrategyType
-
reactiveSystemListener
protected BigraphModelChecker.ReactiveSystemListener<B extends Bigraph<? extends Signature<?>>> reactiveSystemListener -
canonicalForm
-
predicateChecker
-
options
-
-
Constructor Details
-
BigraphModelChecker
-
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
-
execute
Perform the simulation based on the provided reactive system and options.- Throws:
BigraphSimulationException
- if agent isnull
or the simulation strategy was not selectedReactiveSystemException
-
executeAsync
public Future<ReactionGraph<B>> executeAsync() throws BigraphSimulationException, ReactiveSystemExceptionAsynchronously start the simulation based on the provided reactive system and options.- Throws:
BigraphSimulationException
- if agent isnull
or the simulation strategy was not selectedReactiveSystemException
-
assertReactionSystemValid
Performs some checks if the reactive system is valid.- Throws:
BigraphSimulationException
- if the system is not validReactiveSystemException
-
getReactiveSystem
-
getPredicates
-
getMatcher
-
getReactionGraph
-
watch
-
exportState
Exports a bigraph to the filesystem using the export options setting from the member variableoptions
.- Parameters:
bigraph
- the bigraph to be exportedcanonicalForm
- its canonical formsuffix
- a suffix for the filename- Returns:
- the exported state label, or
null
-
exportReactionGraph
- Throws:
IOException
-
setReactiveSystemListener
public BigraphModelChecker<B> setReactiveSystemListener(BigraphModelChecker.ReactiveSystemListener<B> reactiveSystemListener)
-