The graph computed or output by covreach algorithm is not correct

[fredher]

The covreach algorithm on an asynchronous model of Fischer's protocol (fischer_2.txt
) outputs the following graph:

digraph fischer_async_2_10 {
node [shape="box",style="rounded"];
n1 [label="<A,A,l,l> id1=0,id2=0 (0<=x1 & 0<=x2 & x1=x2)"]
n1 -> n2 [color=black]
n1 -> n3 [color=black]
n2 [label="<A,req,l,l> id1=0,id2=0 (0<=x1 & 0<=x2<=10 & 0<=x1-x2)"]
n2 -> n4 [color=black]
n3 [label="<req,A,l,l> id1=0,id2=0 (0<=x1<=10 & 0<=x2 & x1-x2<=0)"]
n3 -> n4 [color=black]
n4 [label="<req,req,l,l> id1=0,id2=0 (0<=x1<=10 & 0<=x2<=10 & 0<=x1-x2<=10)"]
}

command: tchecker covreach -l foo -m zg:elapsed:NOextra -f dot fischer_2.txt

whereas the explore algorithm outputs:

digraph fischer_async_2_10 {
node [shape="box",style="rounded"];
n0 [label="<A,A,l,l> id1=0,id2=0 (0<=x1 & 0<=x2 & x1=x2)"]
n1 [label="<req,A,l,l> id1=0,id2=0 (0<=x1<=10 & 0<=x2 & x1-x2<=0)"]
n0 -> n1
n2 [label="<A,req,l,l> id1=0,id2=0 (0<=x1 & 0<=x2<=10 & 0<=x1-x2)"]
n0 -> n2
n3 [label="<req,req,l,l> id1=0,id2=0 (0<=x1<=10 & 0<=x2<=10 & 0<=x1-x2<=10)"]
n1 -> n3
n4 [label="<req,req,l,l> id1=0,id2=0 (0<=x1<=10 & 0<=x2<=10 & -10<=x1-x2<=0)"]
n2 -> n4
}

command: tchecker explore -s bfs -m zg:elapsed:NOextra -f dot fischer_2.txt

The nodes n2 and n3 in the output produced by covreach algorithm should not have the same successor n4 as demonstrated by the output produced by explore algorithm. They have two distinct successors, and there is no subsumption between these two nodes (n3 and n4 in the output of algorithm explore).