Skip to content

Constrained Precedence Chain Property Pattern 1 Cause N Effects

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

Description

  • Pattern in the original catalog
  • Structured English Specification: Scope, if S [has occurred] and afterwards [<Chain>] [hold] then it must have been the case that P [has occurred] before S [holds] without Z0 holding between S and the chain and without Z1,Z2,..,Zn holding between the elements of the chain

State-Based Pattern

Untimed

Globally

E<> (END && (Z_Flag == 1)) /should evaluate to false/
E<> (END && (P_Flag == 0)) /should evaluate to false/

Precedence Chain Constrained globally untimed observer

Before R

A[] R_Flag == 0 /should evaluate to true/

E<> (END && (Z_Flag == 1)) /should evaluate to false/
E<> (END && (P_Flag == 0)) /should evaluate to false/

Precedence Chain Constrained before R untimed observer

After Q

E<> (END && (Z_Flag == 1)) /should evaluate to false/
E<> (END && (P_Flag == 0)) /should evaluate to false/

Precedence Chain Constrained after Q untimed observer

Between Q and R

A[] R_Flag == 0 /should evaluate to true/

E<> (EVALUATE && (Z_Flag == 1)) /should evaluate to false/
E<> (EVALUATE && (P_Flag == 0)) /should evaluate to false/

Precedence Chain Constrained between Q and R untimed observer

After Q Until R

A[] R_Flag == 0 /should evaluate to true/

E<> (EVALUATE && (Z_Flag == 1)) /should evaluate to false/
E<> (EVALUATE && (P_Flag == 0)) /should evaluate to false/

Precedence Chain Constrained after Q until R untimed observer

Timed

A time-constrained extension for the precedence is not applicable.