-
Notifications
You must be signed in to change notification settings - Fork 0
Response Chain Property Pattern 1 Stimulus N Responses
Marc Carwehl edited this page Dec 16, 2021
·
4 revisions
- Pattern in the original catalog
- Structured English Specification:
Scope, if P [has occurred], then in response [within Time(0)] S eventually holds [<Chain>].
Chain:= [T]
ONE --> TWO
A[] not ERROR
ONE --> TWO
A[] not ERROR
ONE --> TWO
ONE --> TWO
A[] not ERROR
ONE --> TWO
A[] not ERROR
ONE --> TWO
Specification Pattern Catalogue for UPPAAL
Evaluation