Package org.bigraphs.framework.simulation.modelchecking

Interface BigraphModelChecker.ReactiveSystemListener<B extends Bigraph<? extends Signature<?>>>

Enclosing class:
BigraphModelChecker<B extends Bigraph<? extends Signature<?>>>
public static interface BigraphModelChecker.ReactiveSystemListener<B extends Bigraph<? extends Signature<?>>>

  • Method Details

    • onReactiveSystemStarted

      default void onReactiveSystemStarted()

    • onReactiveSystemFinished

      default void onReactiveSystemFinished()

    • onCheckingReactionRule

      default void onCheckingReactionRule(ReactionRule<B> reactionRule)

    • onUpdateReactionRuleApplies

      default void onUpdateReactionRuleApplies(B agent, ReactionRule<B> reactionRule, BigraphMatch<B> matchResult)
      This method is called within a running simulation (i.e., model checking operation), when the redex of a reaction rule could be matched within the host bigraph (i.e., the last active agent of the reactive system).
      Parameters:
      agent - the agent where the redex pattern was found
      reactionRule - the respective reaction rule
      matchResult - the result of the matching

    • onReactionIsNull

      default void onReactionIsNull()

    • onAllPredicateMatched

      default void onAllPredicateMatched(B currentAgent, String label)
      This method is called if all available predicates of a reactive system evaluated to true for some state. In this case, the method onPredicateMatched(Bigraph, ReactiveSystemPredicate) is not called.
      Parameters:
      currentAgent - the agent
      label -

    • onPredicateMatched

      default void onPredicateMatched(B currentAgent, ReactiveSystemPredicate<B> predicate)
      This method is called if a predicate evaluated to true for some state. It is only called if not all predicates yielded true.
      Parameters:
      currentAgent - the agent
      predicate - the predicate

    • onSubPredicateMatched

      default void onSubPredicateMatched(B currentAgent, ReactiveSystemPredicate<B> predicate, B context, B subBigraph, B redexOnly, B paramsOnly)
      This method is called if a sub-bigraph-predicate evaluated to true for some state. It is only called if not all predicates yielded true.
      Parameters:
      currentAgent - the agent
      predicate - the predicate
      subBigraph - the sub-bigraph as matched by the predicate in currentAgent

    • onPredicateViolated

      default void onPredicateViolated(B currentAgent, ReactiveSystemPredicate<B> predicate, org.jgrapht.GraphPath<ReactionGraph.LabeledNode,ReactionGraph.LabeledEdge> counterExampleTrace)
      Reports a violation of a predicate and supplies a counterexample trace from the initial state to the violating state.
      Parameters:
      currentAgent - the agent
      predicate - the predicate
      counterExampleTrace - the trace representing a counterexample

    • onError

      default void onError(Exception e)