Description
Version: Ultimate 0.1.25-d7dd348
We have found some puzzling behavior in the generation of counterexamples that seems to be triggered only in certain time scales.
I describe the problem with a few examples (I omit variable declarations for brevity):
Example 1
R1: Globally, it is always the case that if "a" holds for at least "1000" time units, then "!out" holds afterwards for at least "2000" time units.
R2: Globally, it is always the case that if "b" holds, then "out" holds after at most "500" time units.
This always gives the counterexample that we would expect and understand:
1000 a=true b=false out=false
500 a=false b=true out=false
That is, after the first interval, R1 is activated, and leads to the conflict on what to do with "out" at the end of the trace.
Example 2 (the puzzling one)
We add a new requirement (which apparently causes the issue):
R1: Globally, it is always the case that if "a" holds for at least "1000" time units, then "!out" holds afterwards for at least "2000" time units.
R2: Globally, it is always the case that if "b" holds, then "out" holds after at most "500" time units.
R3: Globally, it is always the case that if "a" holds for at least "1000" time units, then "!a" holds afterwards.
Running this multiple times gives us the same rt-inconsistency between R1 and R2 but two different counterexamples. One of them is the same as for example 1. The other one, we fail to understand:
0 a=* b=* out=*
500 a=true b=true out=false
In this counterexample R1 doesn't kick in since not enough time has passed with "a" active, so the conflict is not clear (we still haven't found an explanation).
Example 3
This is exactly like Example 2 but we divide all times by 100:
R1: Globally, it is always the case that if "a" holds for at least "10" time units, then "!out" holds afterwards for at least "20" time units.
R2: Globally, it is always the case that if "b" holds, then "out" holds after at most "5" time units.
R3: Globally, it is always the case that if "a" holds for at least "10" time units, then "!a" holds afterwards.
Surprisingly, this results in the same single counterexample (the one that we understand and equivalent to Example 1):
0 a=* b=* out=*
10 a=true b=false out=false
5 a=false b=true out=false
So at first we were looking for a plausible explanation for the conterexample in example 2, but the fact that it seems to go away when changing the time scale seems to be pointing in the direction of this being some sort of bug.