Existence Property Pattern

• Description
• State-Based Pattern

Description

• Pattern in the original catalog
• Structured English Specification: [Scope], P eventually [holds] [Time].
• Pattern Intent: This pattern aims at describing a portion of a system's execution bounded by a time interval that contains an instance of certain states.

State-Based Pattern

Untimed

Globally

A<> P

Before R

with A[] not ERROR

After Q

A[] not Q
A<> (Q_held_once == 1 and P)

Either one of the formulas has to be satisfied. The first one connotes that Q may never hold, which is fine. However, if Q does hold, P has to hold sometime later as well.

Between Q and R

with

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

After Q Until R

with

A[] INIT imply not Q // warning
SCOPEOPEN --> FULFILLED

Timed

Globally

A<>(gc >= t1 and gc <= t2 and P)

where gc is a global clock, t1 the lower time bound, and t2 the upper time bound.

Before R

with

A[] INIT imply not R // warning
A[] not ERROR

P occurring before t1 or after t2 is not considered as an error.

After Q

with

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

Between Q and R

with

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

After Q Until R

with

A[] INIT imply not R // warning
SCOPEOPEN --> P_happens