-
Notifications
You must be signed in to change notification settings - Fork 0
Recurrence Property Pattern
Marc Carwehl edited this page Dec 16, 2021
·
4 revisions
- Pattern in the original catalog
- Structured English Specification:
[Scope], P [holds] repeatedly every t timeunits.
- Pattern Intent: This pattern describes a portion of a system's execution that contains an unspecified number of instances of a designated state, which must not be absent longer than the timebound.
- In the observers below,
t
is the time bound.
START --> GOAL
START --> GOAL
START --> GOAL
This scope is hardly applicable.
VALIDATION --> (P_ or INIT)
VALIDATE --> (P or R)
The following observer reaches an ERROR
state when P
is not true repeatedly in time. Whenever P is left, the clock is reset.
A[] not ERROR
The following observer reaches an ERROR
state when P
is not true repeatedly in time and afterwards it observes an R
. Whenever P is left, the clock is reset. The ERROR
state is unreachable once R
happened.
A[] not ERROR
After observing Q
, the following observer reaches an ERROR
state when P
is not true repeatedly in time. Whenever P is left, the clock is reset.
A[] not ERROR
A[] not ERROR
A[] not ERROR
Specification Pattern Catalogue for UPPAAL
Evaluation