New property: continuous consistency

[danieldietsch]

Like rt-inconsistency, but without projecting changes.

[danieldietsch]

Next step: Better example

[alopez-developair]

I did a few simple tests to try to understand the unexpected results we get. The results are indeed a bit puzzling: Ex. 1:

req1: Globally, it is always the case that if "c" holds, then "a" holds after at most "50" time units
req2: Globally, it is always the case that if "c" holds, then "b" holds after at most "50" time units

Results in no errors (as expected).

Ex. 2:

req1: Globally, it is always the case that if "c" holds, then "a" holds after at most "50" time units
req3: Globally, it is never the case that "a" holds.

Also results in no errors, despite the apparent conflict.

Ex. 3:

req1: Globally, it is always the case that if "c" holds, then "a" holds after at most "50" time units
req2: Globally, it is always the case that if "c" holds, then "b" holds after at most "50" time units
req3: Globally, it is never the case that "a" holds.

Gives rt-inconsistency between req1 and req2; yet the conflict should be between req1 and req3.

[Langenfeld]

please update ultimate to the newest (nightly) build: Ex.2: rt-incosnistency found Ex.3: is still wrong, and needs some investigation