Show LTL Counterexample Lassos in ProB2-UI

[leuschel]

Currently one cannot really inspect the counterexample lassos generated by the LTL model checker. In ProB Tcl/Tk one sees a history with the lasso using a dot visualisation.

One could show the lasso's loop either in ProB2-UI's history view or also in a dot view, or preferably both.

[leuschel]

Example to test the LTL parser:

MACHINE Mutex
// with Semaphore
SETS
  Status = {noncrit,wait,crit}
CONSTANTS n
PROPERTIES n=2
VARIABLES
  pc /*@desc "the location / program counter of each program graph" */, 
  y  /*@desc "the Semaphore" */
INVARIANT
  pc: 1..n --> Status &
  y : 0..1 &
  card({i| i|->crit : pc}) <= 1 /*@ desc "Safety"*/
INITIALISATION
  pc := (1..n)*{noncrit} || y := 1
OPERATIONS
  RequestCS(i) = PRE i:1..n & pc(i)=noncrit THEN
    pc(i) := wait
  END;
  EnterCS(i) = PRE i:1..n & pc(i)=wait & y>0 THEN
    pc(i) := crit || y:=y-1
  END;
  LeaveCS(i) = PRE i:1..n & pc(i)=crit THEN
    pc(i) := noncrit || y:=y+1
  END
DEFINITIONS
  GOAL == crit:ran(pc);
  HEURISTIC_FUNCTION == card({j|j:1..n & pc(j)=noncrit}) + y;
  ASSERT_LTL == "G ([RequestCS(1)] => F {pc(1)=crit})"; // Is not satisfied
  ASSERT_LTL1 == "GF {crit:ran(pc)}";
  ASSERT_LTL2 == "FG {not(crit:ran(pc))}";

  ASSERT_LTL100 == "GF {GOAL}"; // parse error
  RPC == ran(pc);
  ASSERT_LTL101 == "GF {crit:RPC}" // ok
END

[dgelessus]

I've implemented a basic solution in hhu-stups/prob2_ui@35c6c9241fa9344071e86af453ebd232e097813c - when showing an LTL counterexample with a loop, the current trace position is now set to the loop entry point. (For counterexamples without a loop, the trace position is set to the end of the trace, as before.) This makes it possible to see the loop at least, even though it's perhaps not very clear.

ProB Tcl/Tk already uses a dot visualisation to show LTL counterexamples. Ideally we should make the same visualisation available in ProB 2 UI as well. But I don't know if probcli has all the necessary information for that when called from ProB 2, especially the current trace.