Bigraphical Predicates
This section explains how to create predicates for model checking.
Important generic abstract class: org.bigraphs.framework.core.reactivesystem.ReactiveSystemPredicate<B extends Bigraph<? extends Signature<?>>>.
Adding Predicates​
Any sub-class of AbstractSimpleReactiveSystem<B extends Bigraph<? extends Signature<?>>> provides the following method for adding predicates:
AbstractSimpleReactiveSystem#addPredicate(ReactiveSystemPredicates<B> predicate)
Safety and Liveness Properties​
As long as the transition system is being built from a BRS specification, the provided predicates of the user are checked simultaneously for each new computed state in the course of a BRS simulation.
note
A user can listen to these events. Therefore, the interface ReactiveSystemListener<B extends Bigraph<? extends Signature<?>>> must be implemented and added to the model checker instance.
These predicates come in two forms: as safety properties or as liveness properties. The former represents a state in the system that should not occur, whereas the later denote a system state that eventually occurs. By this we can test if a program never reaches a "bad state" (safety), or correctly terminates (reaching a desirable state), possibly producing a result (liveness).
Some further safety properties are: partial correctness, absence of deadlocks, and mutual exclusion (see [1]).
tip
Fairness properties are important for reactive systems. Safety is easier to check than liveness.
Listening to Predicate Evaluation​
If predicates are added to a reactive system instance, one can add additional logic when these predicates gets evaluated.
Therefore, one must add a listener the bigraph model checker instance by calling BigraphModelChecker<B>#setReactiveSystemListener(BigraphModelChecker.ReactiveSystemListener<B> reactiveSystemListener)
or by passing the object as argument in one of its constructors.
The listener BigraphModelChecker.ReactiveSystemListener<B> contains several methods for getting the evaluation result of a predicate match.
onAllPredicateMatched(...)​
This method is called if all available predicates of a reactive system evaluated to true in one state.
In this case, the method ReactiveSystemListener#onPredicateMatched(Bigraph, ReactiveSystemPredicates) is not called.
It has the following arguments:
B currentAgent: the agent
onPredicateMatched(...)​
This method is called if a predicate evaluated to {@code true} after a transition.
It is only called if not all predicates yielded true.
It has the following arguments:
B currentAgent: the agentReactiveSystemPredicates<B> predicate: the predicate
onPredicateViolated(...)​
Reports a violation of a predicate and supplies a counterexample trace from the initial state to the violating state. It has the following arguments:
B currentAgent: the agentReactiveSystemPredicates<B> predicate: the predicateGraphPath<ReactionGraph.LabeledNode, ReactionGraph.LabeledEdge> counterExampleTrace: the trace representing a counterexample