ProB: are invariants checked for random animation?

22 views
Skip to first unread message

Denis Efremov

unread,
Jul 3, 2020, 3:54:35 AM7/3/20
to ProB Users
Hi,

are invariants checked in this loop by default (no proof obligations in model) or do I need to uncomment the condition and check violation explicitly:

try {
for (int i = 0; i < steps; i++) {
trace = trace.anyEvent(null);
System.out.println(trace.getCurrent().getTransition().evaluate().getPrettyRep());
//if (!trace.getCurrentState().isInvariantOk()) {
// throw new Exception("Invariants violation");
//}
}
} catch (Exception e) {
System.out.println("Error: " + e.getMessage());
}

How can I get info about a "broken" invariant in this case?

Thanks,
Denis

Denis Efremov

unread,
Jul 3, 2020, 10:44:42 AM7/3/20
to ProB Users


How can I get info about a "broken" invariant in this case?


The only way I found to do it is to eval all invariants as predicates on current state:

List<IEvalElement> invariants = new ArrayList<>();
EventBMachine machine = (EventBMachine) stateSpace.getMainComponent();
for (Invariant i : machine.getAllInvariants()) {
invariants.add(i.getPredicate());
}
List<AbstractEvalResult> results = trace.getCurrentState().eval(invariants);

List<String> violated_invariants = new ArrayList<>();
for (int i = 0; i < results.size(); ++i) {
EvalResult r = (EvalResult) results.get(i);
if (r != EvalResult.TRUE) {
violated_invariants.add(invariants.get(i).toString());
}
}

if (!violated_invariants.isEmpty()) {
System.out.println("Violated invariants:\n\t - " + String.join("\n\t - ", violated_invariants));
}
 
But I hope there is a better way and someone could point me to it.

Thanks,
Denis

yefremo...@gmail.com

unread,
Jul 4, 2020, 9:49:53 AM7/4/20
to ProB Users
I found that internally ProB check invariants during "trace.anyEvent(null);" call, because ComputeCoverageCommand(); command shows stats for "violated_invariants" if there are ones.
However, one needs to call "trace.getCurrentState().isInvariantOk()" after every animation step to get this "knowledge" from ProB internals.

BTW, it's not obvious what is "invariants_not_checked" property about in coverage ComputeCoverageCommand.getNodes().

Regards,
Denis

-//--//-

unread,
Jul 4, 2020, 10:30:04 AM7/4/20
to ProB Users
Since I posted a snippet for finding violated invariants, here is the snippet to find first violated guard condition:
ProB Plugin for Rodin can highlight invariants/guards evaluation status and I found no better way with Java API than just to evaluate guards against current state one-by-one. Logic expression for each next guard consists from all previous guards and parameter values. Is there a special API to get this info from ProB internals? Maybe it's correct to evaluate guards independently from all previous ones? I mean, no need to conjunct predicates for grd1 & grd2 & grd3 to evaluate grd3. 

Again, this code doesn't look like a proper way to do it and I hope there is some internal command to fetch guards evaluation status from ProB internals.

Regards,
Denis
пятница, 3 июля 2020 г. в 17:44:42 UTC+3, yefremo...@gmail.com:

Fabian Vu

unread,
Jul 17, 2020, 6:00:40 AM7/17/20
to ProB Users
Hello Denis,

the invariant is evaluated as a single predicate in the internal implementation of ProB. You can check whether the invariant is violated in the current state using the function isInvariantOk() in State (https://github.com/hhu-stups/prob2_kernel/blob/develop/de.prob2.kernel/src/main/java/de/prob/statespace/State.java).

However, there is no function in the ProB2 Java API to detect which parts (conjuncts) of the invariant are violated. To achieve this, it is required to evaluate each conjunct as a predicate on the current state as you have done it in your implementation.

Yours sincerely,

Fabian
Reply all
Reply to author
Forward
0 new messages