Skip to content

Precedence Property Pattern

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

Description

  • Pattern in the original catalog
  • Structured English Specification: [Scope], if P [becomes satisfied] then it must be that case that S [has been satisfied] before P [becomes satisfied].

State-Based Pattern

Untimed

Globally

The observer checks if S is reached before P: Once S is reached the Path does not interest us anymore, since the specification will be true. However if P is reached before S has ever occurred in a Path, the observer goes into an ERROR state, since the specification is not fulfilled in this case.

A[] not ERROR

Precedence globally untimed observer

Before R

A[] not ERROR

Precedence before Q untimed observer

After Q

A[] not ERROR

Precedence after R untimed observer

Between Q and R

A[] not ERROR

Precedence between Q and R untimed observer

After Q Until R

A[] not ERROR

Precedence after Q until R untimed observer

Timed

  • The timed version of the Precedence pattern, including its variance with Chains, is not applicable in UPPAAL. Any instance of S would have to be taken into consideration when evaluating an instance of P. UPPAAL, however, cannot handle arbitrary many variables, states, or arrays with arbitrary length.