Universality Property Pattern

• Description
• State-Based Pattern

Description

• Pattern in the original catalog
• Structured English Specification: [Scope], it is always the case that P [holds] [Time].
• Universality of a state can be viewed as absence of its negation.
• Pattern Intent: This pattern describes a portion of a system's execution which contains only states that have a desired property [within a given timebound]. Thus, P is a state or a state formula. The latter refers to conditions of global system variables (e.g., x > 5). Here, we consider the case that P is a state.

State-Based Pattern

Untimed

Globally

A[] P

Before R

with A[] not ERROR

After Q

A[] Q_held_once == 1 imply P

Alternative using the observer technique

A[] INIT imply not Q
A[] SCOPEOPEN imply P
A[] not ERROR

We may skip the ERROR state:

A[] INIT imply not Q
A[] SCOPEOPEN imply P

Between Q and R

A[] INIT imply not Q //as warning
A[] not ERROR

After Q until R

with

A[] INIT imply not Q //as warning
A[] not ERROR

Alternative

with

A[] INIT imply not Q //as warning
A[] SCOPEOPEN imply (P and not R)
A[] not ERROR

Timed

Globally

A[] ((gc >= t1 and gc <= t2) imply P)

where gc is a global clock, t1 is the lower and t2 the upper time bound. Thus, when the time constrained is satisfied, P must hold.

Before R

with A[] not ERROR

Comments:

• The observer assures that P must hold at the beginning of the time window, that is, at t1.
• We consider the case when R is reached before t1 as an error.

After Q

with

A[] INIT imply not Q (as warning)
A[] (SCOPEOPEN and c == t1) imply P
A[] not ERROR

Alternative skipping the ERROR state:

with

A[] INIT imply not Q //as warning
A[] (SCOPEOPEN and c>=t1 and c<=t2) imply P

Between Q and R

with

A[] INIT imply not Q //as warning
A[] SCOPEOPEN imply not R // needed or already covered by the observer
A[] not ERROR

After Q until R

with

A[] INIT imply not Q
A[] (SCOPEOPEN and c == t1) imply P
A[] not ERROR

Alternative encoding the time interval in the observer

A[] INIT imply not Q
A[] INTERVALOPEN imply P