Bounded Existence Property Pattern

• Description
• State-Based Pattern

Description

• Pattern in the original catalog
• Structured English Specification: [Scope], P [holds] at most n times.
• Pattern Intent: This pattern describes a portion of a system's execution that contains at most a specified number of instances of a designated state transition.
• A time-constrained extension for the bounded existence is not applicable. Indeed, we could not find any use case, in published papers and other available documents we searched, justifying the need of such a pattern.

State-Based Pattern

In the observers, the threshold n is named n_.

Untimed

Globally

with A[] not ERROR

Before R

with

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

After Q

with

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

Between Q and R

with

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

After Q Until R

with

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

Timed

A time-constrained extension for the bounded existence is not applicable.