Wrong Edge

[PhilipLukertWork]

Hi, I have the following Situation:

• Note that there is an edge of State(A) to State(B) which should not be possible.
• Interesting is that the left side in the proof tree it claims Case Change while in the dependency graph it is actually the case of Init.
  Here is the code for it:

theory NonMatchingEdge begin

rule Init: [] --> [State('A'), X('1')]  //without the X, the bug does not appear
rule Change: [State('A')] --> [State('B')]
rule Test: [State('B')] --[TestPoint()]-> []

lemma ex: exists-trace "∃ #i. TestPoint()@i"

end

I tested this on develop commit d6355e5

Best, Philip

[PhilipLukertWork]

A hint from Cas: If I turn off graph simplifications, it looks as follows

Is this an intended feature of graph simplifications?