Wrong specification in rtinconsistency_test5

[hauff]

Expected: // #TestSpec: rt-inconsistent:; vacuous:; inconsistent:; results:-1 Actual: // #TestSpec: rt-inconsistent:req1+req2; vacuous:; inconsistent:; results:-1

CONST MAX_TIME is 50.0
CONST time_at_least is 30.0

req1: Globally It is always the case that once "var4" becomes satisfied, it holds for at least "time_at_least" time units
req2: Globally It is always the case that If "var3" holds, then "!var4" holds after at most "MAX_TIME" time units for at least "time_at_least" time units

[hauff]

Obsolete (MinDurationPattern was refactored) New issue #500.

[danieldietsch]

Back to this decision ;)

[Langenfeld]

Actual is correct, test must be fixed.

[henkele]

• Jenkins: history
• Hanfor: req1, req2

Result

• Expected: rt-inconsistent:req1+req2; vacuous:; inconsistent:;
• Actual: rt-inconsistent:; vacuous:; inconsistent:;

Test (.req file)

CONST MAX_TIME is 50.0
CONST time_at_least is 30.0

req1: Globally It is always the case that once "var4" becomes satisfied, it holds for at least "time_at_least" time units
req2: Globally It is always the case that If "var3" holds, then "!var4" holds after at most "MAX_TIME" time units for at least "time_at_least" time units

Comments

Actual should be correct.

The example that we used earlier to argue for rt-inconsistency is broken. We assumed to have a prefix satisfying both requirements but req2 is actually violated at t=32. As "MAX_TIME" is larger than "time_at_least", rt-inconsistency should not be possible.