Package org.bigraphs.framework.simulation.modelchecking

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

java.lang.Object
org.bigraphs.framework.simulation.modelchecking.BigraphModelChecker<B>
Type Parameters:
B - the concrete bigraph type used by the reactive system
Direct Known Subclasses:
PureBigraphModelChecker
public abstract class BigraphModelChecker<B extends Bigraph<? extends Signature<?>>> extends Object
A model checker for Bigraphical Reactive Systems (BRS) that simulates state-space evolution by repeatedly applying reaction rules. A reactive system, an exploration strategy, and model checking options must be provided.

The model checker can operate with different traversal strategies (e.g., BFS, DFS, first-match variants, random exploration), enabling exhaustive analysis or guided simulations depending on the chosen configuration.

During simulation, the model checker emits state-space events through BigraphModelChecker.ReactiveSystemListener instances (inner class of this class). Listeners notify the user when predicates are evaluated, reaction rules applied or when lifecycle events are emitted.

After execution, the reaction graph (transition system, ReactionGraph) can be retrieved for inspection or further analysis. For example, it can be exported via ReactionGraphExporter or DOTReactionGraphExporter.

See Also:

  • Field Details

  • Constructor Details

    • BigraphModelChecker

      public BigraphModelChecker(ReactiveSystem<B> reactiveSystem, ModelCheckingOptions options)
      Creates a BigraphModelChecker using Breadth-First Search (BFS) as default exploration strategy.

      BFS ensures a level-by-level expansion of the reactive system and is typically preferred for exhaustive model checking where completeness and shortest-path properties are desired.

      Parameters:
      reactiveSystem - the reactive system to be explored
      options - configuration settings controlling model checking behavior

    • BigraphModelChecker

      public BigraphModelChecker(ReactiveSystem<B> reactiveSystem, BigraphModelChecker.SimulationStrategy.Type simulationStrategyType, ModelCheckingOptions options)
      Creates a BigraphModelChecker using the specified exploration strategy.

      This constructor allows selecting between different model checking strategies, such as BFS, DFS, first-match variants, or randomized exploration. The choice of strategy influences how the state space is traversed:

      • BFS: Exhaustive, level-order traversal.
      • DFS: Deep-path exploration, useful for long execution traces.
      • BFS_FIRST_MATCH / DFS_FIRST_MATCH: Deterministic path exploration using only the first available successor in natural match order.
      • RANDOM: Stochastic exploration for sampling-based analysis.

      Parameters:
      reactiveSystem - the reactive system to be explored
      simulationStrategyType - the traversal strategy to be used
      options - configuration settings controlling model checking behavior

    • BigraphModelChecker

      public BigraphModelChecker(ReactiveSystem<B> reactiveSystem, BigraphModelChecker.SimulationStrategy.Type simulationStrategyType, ModelCheckingOptions options, BigraphModelChecker.ReactiveSystemListener<B> listener)
      Creates a BigraphModelChecker with a specified exploration strategy and an optional listener.

      The listener can be used for advanced use cases where one needs to observe state-space exploration events (e.g., rule triggered, or predicate matched).

      Parameters:
      reactiveSystem - the reactive system to be explored
      simulationStrategyType - the traversal strategy to be used
      options - configuration settings controlling model checking behavior
      listener - optional listener for reactive system events (may be null)

  • Method Details