ERRORs generated while extracting certificate

[mukherjee-sayan]

Hi,

We are trying to generate (concrete) certificates for reachability by calling tck-reach -a covreach -C concrete -l .... We sometimes are getting the following two kinds of errors (for both the errors we have REACHABLE true)

• ERROR: *** compute_finite_path(symbolic): sequence is not feasible from given initial locations
• ERROR: clock valuation does not belong to the zone

Could you please explain what is the meaning of these errors and when they may occur?

Best regards, Sayan

[fredher]

Dear Sayan, This is hard to tell what happens exactly here: it seems that TChecker has computed a symbolic counter example which is not feasible from the initial locations. This should not occur. Could you please attach the model, and give the full command-line to let me reproduce the bug? Best regards, Frédéric

[mukherjee-sayan]

Dear Frédéric,

Below is a small automaton where we are getting the first error.

---

system:my_sys

event:a

clock:1:x

process:P0 location:P0:l0{initial:} location:P0:l1{} location:P0:l2{labels: accepting}

edge:P0:l0:l1:a{provided:x>0&&x<1} edge:P0:l0:l1:a{provided:x>=1} edge:P0:l1:l2:a{provided:x<1&&x>0 : do:x=0}

---

We are using the following on the command line: tck-reach -a covreach -C concrete -l accepting <filename.txt> This shows that REACHABLE true but produces the error ERROR: *** compute_finite_path(symbolic): sequence is not feasible from given initial locations

We will try to find a small example where the second error was occurring.

Best regards, Sayan

[fredher]

Dear Sayan,

The bug has been fixed in commit a6579ad

The zone graph in your example is as follows:

(l0, 0<=x) -a-> (l1, 0<x) -a-> (l2, 0<=x)
     |--------a-> (l1, 1<=x)

Since (l1, 1<=x) is subsummed by (l1, 0<x), we only keep the later in the zone graph, and add a special edge, called a subsumption edge from (l0, 0<=x) to (l1, 0<x) corresponding to the edge with guard (x>=1).

So, we end up with two paths to accepting node l2. One of them is the actual path to (l2, 0<=x), which takes the first and last transitions in your model. The other path is spurious: it takes the subsumption edge corresponding to the second edge in your model, then the last edge in your model. Obviously, counter-examples should only be built from actual edges (and not from subsumption edges), since, as your example shows, path with subsumption edges may not be feasible. Subsumption edges lead to over-approximation of the actual paths in the zone graphs, but reachability is preserved.

There was a bug in TChecker where subsumption edges may appear in counter-examples. This has been easily fixed by restricting counter-examples generation to only take actual edges.

Thanks for pointing out the problem!

Best regards, Frédéric

[mukherjee-sayan]

Thanks Frédéric for the quick fix. We are not facing that error anymore :)

Best regards, Sayan