Open
Description
As mentioned in #543, this would apply to 6d31cd0, as more recent versions don't show these inconsistencies.
Example:
Input count_1 is int
R11: Globally, it is always the case that "count_1 == prev(count_1) + 1" holds at least every "1" time units.
R12: Globally, it is never the case that "count_1 < prev(count_1)" holds.
R13: Globally, it is never the case that "count_1 < 0" holds.
R14: Globally, it is always the case that if "count_1 == 0" holds, then "count_1 >= 10" holds after at most "10" time units.
Result:
- ReqCheckRtInconsistentResult [Line: -1]: Requirements R14, R11 are rt-inconsistent
Requirements R14, R11 are rt-inconsistent
We found a FailurePath:
INITIAL |'count_1|=0 count_1=0
[0;17/2] |'count_1|=0 count_1=1
[17/2;17] |'count_1|=1 count_1=1
Without going too much into other specifics of the example, in this issue I want to address the following:
- Initial value for
count_1
is 0. Thus, via R14,count_1 >= 10
will have to happen before time 10. - During [0;17/2] (i.e. 0-8.5),
count_1 = 1
andprev(count_1) = 0
, satisfying R11. - And the last segment [8.5;17] is the one that I can't make heads and tails of:
count_1 == prev(count_1)
for 8.5 units, which seems to violate R11.- The time point 10 has been crossed and
count_1 == 1
so R14 is also being violated in this example.