Constrained Precedence Chain Property Pattern N Causes 1 Effect

• Description
• State-Based Pattern

Description

• Pattern in the original catalog
• Structured English Specification: Scope, if P [holds] then it must have been the case that S and afterwards [<Chain>] [have occurred] before P [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 && P) && (Z_Flag == 1)) /should evaluate to false/
A[] P imply END /should evaluate to true/

Before R

(R && SCOPE_CLOSED == 0) --> (P && END && Z_Flag == 0)
A[] (P && R_Flag == 1) imply (END && Z_Flag == 0)

After Q

E<> ((END && P) && (Z_Flag == 1)) /should evaluate to false/
A[] P imply END /should evaluate to true/

Between Q and R

A[] (R_Flag == 1 && P) imply (END && Z_Flag == 0 && Z0_Flag == 0)
A[] (EVALUATE && P_Flag == 1) imply (Z_Flag == 0 && Z0_Flag == 0)

After Q Until R

A[] (P && not EVALUATE) imply CLOSED
A[] (P && not CLOSED) imply EVALUATE
E<> (EVALUATE && (Z_Flag == 1)) /should evaluate to false/
E<> (EVALUATE && (Z0_Flag == 1)) /should evaluate to false/

Timed

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