Response Property Pattern

• Description
• State-Based Pattern

Description

• Pattern in the original catalog
• Structured English Specification: [Scope], if P [has occurred], then in response S eventually holds [Time].
• Pattern Intent: To describe cause-effect relationships between a pair of states. An occurrence of the first, the cause P, must be followed by an occurrence of the second, the effect S within a time bound.

State-Based Pattern

Untimed

Globally

P --> S

In UPPAAL, --> is the leads-to or response operator; P --> S is equivalent to A[] (P imply A<> S).

Before R

with A[] not ERROR

After Q

with P_happens-->S_happens

Between Q and R

with A[] not ERROR

After Q Until R

with P_happens-->S_happens

Timed

Globally

One possible solution using an automaton is:

with A[] not ERROR

Before R

with A[] not ERROR

After Q

with P_happens-->S_happens

Between Q and R

with A[] not ERROR

After Q Until R

with P_happens-->S_happens