Method Summary
All Methods Instance Methods Default Methods
default void
This method is called if all available predicates of a reactive system evaluated to true for some state.
default void
default void
default void
This method is called if a predicate evaluated to true
for some state.
default void
Reports a violation of a predicate and supplies a counterexample trace from the initial state to the
violating state.
default void
default void
default void
default void
This method is called if a sub-bigraph-predicate evaluated to true
for some state.
default void
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).
Method Details
onReactiveSystemStarted
default void onReactiveSystemStarted ()
onReactiveSystemFinished
default void onReactiveSystemFinished ()
onCheckingReactionRule
default void onCheckingReactionRule (ReactionRule <B > reactionRule)
onUpdateReactionRuleApplies
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)
Parameters:
currentAgent
- the agent
label
-
onPredicateMatched
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
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
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
Copyright © 2021-present. Dominik Grzelak, Software Technology Group, Technische Universität Dresden. All rights reserved.