RALib can generate non-deterministic RAs

[pfg666]

Added a test case which showcases that ('src/test/java/de/learnlib/ralib/learning/LearnBoundedListTest.java' in bug-non-deterministic-ra branch). Therein, we learn a list with methods push (adds element to start of list), pop (removes element from start) and insert (inserts second argument before the first element equal to the first argument, or at the end of a list if the first argument is not contained).

The result after processing a few counterexamples is:

INFO: l0 (+) (initial):
  (l0 (+), ?pop[int], TRUE, [], l1 (-))
  (l0 (+), ?insert[int, int], TRUE && TRUE, [r1:=p2,], l2 (+))
  (l0 (+), ?push[int], TRUE, [r1:=p1,], l2 (+))

l1 (-):
  (l1 (-), ?insert[int, int], TRUE && TRUE, [], l1 (-))
  (l1 (-), ?push[int], TRUE, [], l1 (-))
  (l1 (-), ?pop[int], TRUE, [], l1 (-))

l2 (+):
  (l2 (+), ?pop[int], TRUE, [], l1 (-))
  (l2 (+), ?insert[int, int], (r1==p1) && TRUE, [r1:=r1,r2:=p2,], l3 (+))
  (l2 (+), ?insert[int, int], (r1!=p1) && TRUE, [r1:=p2,r2:=r1,], l3 (+))
  (l2 (+), ?push[int], TRUE, [r1:=r1,r2:=p1,], l3 (+))

l3 (+):
  (l3 (+), ?pop[int], (r2!=p1), [], l1 (-))
  (l3 (+), ?pop[int], (r2==p1), [r1:=r1,], l2 (+))
  (l3 (+), ?insert[int, int], (r1==p1) && TRUE, [r1:=p2,r2:=r2,r3:=r1,], l4 (+))
  (l3 (+), ?insert[int, int], (r2==p1) && TRUE, [r1:=r2,r2:=p2,r3:=r1,], l4 (+))
  (l3 (+), ?insert[int, int], (r2!=p1) && TRUE, [r1:=r1,r2:=r2,r3:=p2,], l4 (+))
  (l3 (+), ?push[int], TRUE, [r1:=r2,r2:=p1,r3:=r1,], l4 (+))

l4 (+):
  (l4 (+), ?pop[int], (r2!=p1), [], l1 (-))
  (l4 (+), ?pop[int], (r2==p1), [r1:=r3,r2:=r1,], l3 (+))
  (l4 (+), ?insert[int, int], TRUE && TRUE, [r1:=r1,r2:=r2,r3:=r3,], l4 (+))
  (l4 (+), ?push[int], TRUE, [r1:=r1,r2:=r2,r3:=r3,], l4 (+))

Init:[]

Pushing two equal elements will prompt the RA to transition to l3, with r1 and r2 taking the same value. In l3, two transitions (with guards r1==p1 and r2==p1) may be fired on receiving an insert whose first argument is the value stored in the two registers. Depending on which transition is chosen first, we may or may not get the counterexample. If we do, learning cannot handle it and will fail.

I think the issue lies in the algorithm, rather than in the implementation.

[pfg666]

Looking at the hypothesis, it is quite easy to notice another problem. The third transition on insert should be (r1!=p1 && r2!=p1) instead of just (r1!=p1).