Interface ModelCheckingStrategy<B extends Bigraph<? extends Signature<?>>>

All Known Implementing Classes:
BreadthFirstSimulationStrategy, BreadthFirstStrategy, ModelCheckingStrategySupport, RandomAgentModelCheckingStrategy

public interface ModelCheckingStrategy<B extends Bigraph<? extends Signature<?>>>
Strategy pattern for implementing new model checking algorithms.

Current implementations:

  • Breadth-first search (with cycle detection)
  • Simulation (BFS without cycle checking)
  • Random
Author:
Dominik Grzelak
  • Method Summary

    Modifier and Type
    Method
    Description
    void
    Entry point of the model checking strategy to implement.
  • Method Details

    • synthesizeTransitionSystem

      void synthesizeTransitionSystem()
      Entry point of the model checking strategy to implement.

      The reaction graph (i.e., transition system) can be acquired and stored via the model checker object.