Skip to content

rt-inconsistency between one requirement and invariants are not reported / reported in the wrong part #533

Open
@danieldietsch

Description

@danieldietsch

see #465

Ex. 3 is still broken.

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 or at least just one.

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions