Skip to content

Constrained Response Property Pattern

Jump to bottom
Marc Carwehl edited this page Dec 16, 2021 · 4 revisions

Description

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

State-Based Pattern

Untimed

Globally

P_happens --> S_happens
A [] P_happens imply (not ZS_holds)

Constrained Response Globally untimed observer

Before R

A[] not ERROR

Constrained Response before R untimed observer

After Q

P_happens --> S_happens
A [] P_happens imply (not ZS_holds)

Constrained Response after Q untimed observer

Between Q and R

A[] not ERROR

Constrained Response between Q and R untimed observer

After Q Until R

P_happens --> S_happens
A [] P_happens imply (not ZS_holds)

Constrained Response after Q until R untimed observer

Timed

Globally

P_happens --> S_happens
A [] P_happens imply ((not ZS_holds) OR c > t2)

Constrained Response Globally untimed observer

Before R

A[] not ERROR

Response before R timed observer

After Q

P_happens --> S_happens
A [] P_happens imply (not ZS)

Response after Q timed observer

Between Q and R

A[] not ERROR

Response between Q and R timed observer

After Q Until R

P_happens --> S_happens
A [] P_happens imply (not ZS)

Response after Q until R timed observer

Home

Specification Pattern Catalogue for UPPAAL

Evaluation

Clone this wiki locally