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

All Known Implementing Classes:
BFSFirstMatchStrategy, BreadthFirstStrategy, DepthFirstStrategy, DFSFirstMatchStrategy, ModelCheckingStrategySupport, RandomAgentModelCheckingStrategy, SimulatedAnnealingFrontierStrategy

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

    • setWorklistFilter

      void setWorklistFilter(BigraphFilter<B> filter)
    • getWorklistFilter

      BigraphFilter<B> getWorklistFilter()
    • setReactionRuleFilter

      void setReactionRuleFilter(ReactionRuleFilter<B> filter)
    • getReactionRuleFilter

      ReactionRuleFilter<B> getReactionRuleFilter()