-
Notifications
You must be signed in to change notification settings - Fork 0
Precedence Chain Property Pattern N Causes 1 Effect
Marc Carwehl edited this page Dec 16, 2021
·
4 revisions
- Pattern in the original catalog
- Structured English Specification:
Scope, if P [holds] then it must have been the case that S and afterwards [<Chain>] [have occurred] [Interval(P)] before P [holds]
Chain := [T]
- To add elements to the chain, add states to the observer after states that checked whether
T_holds
.
A[] not ERROR
A[] not ERROR
A[] not ERROR
A[] not ERROR
A[] not ERROR
A time-constrained extension for the precedence is not applicable.
Specification Pattern Catalogue for UPPAAL
Evaluation