Maximum Duration

• Description
• State-Based Pattern

Description

• Pattern in the original catalog
• Structured English Specification: [Scope], once P [becomes satisfied] it remains so for less than u time units.
• Note that this pattern is very similar to the Minimum-Duration Pattern.

State-Based Pattern

Untimed

The untimed version of this pattern does not make any sense.

Timed

Globally

A[] (State AND c >= t1) imply not P

Before R

A[] not ERROR

After Q

A[] Scope imply c < t1

Between Q and R

A[] not ERROR

After Q until R

A[] (State AND c >= t1) imply not P