ProB: are invariants checked for random animation?

[Denis Efremov]

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]

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]

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

[-//--//-]

Since I posted a snippet for finding violated invariants, here is the snippet to find first violated guard condition:

https://github.com/evdenis/animate/blob/edd7d21e350aa53738453cea50c656f9342b2419/src/main/java/animate/Animate.java#L92

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]

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