Skip to content

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] [ Interval(S) ] before S [holds].
  • Chain := [T1, T2, T3]

State-Based Pattern

To add an element T4 to the chain, do the following:

1. Turn state END into committed state
2. Add a new states: 0, 1.
3. Add transition from END to 0 with guard T4_holds == 1.
4. Add transition from END to 1 with guard T4_holds == 0.
5. Add transition from 1 to 0 with sync T4_reached?.
6. Add missing transitions for individual scope.
7. Delete name END.
8. Rename 0 to END.

Untimed

Globally

A[] END imply P_Flag == 1

Nothing more to do for adding objects to the chain.

Precedence Chain globally untimed

Before R

A[] EVALUATE imply P_Flag
A[] R_Flag == 0
For adding objects to the chain:
Delete transition from END to EVALUATE.
Add transistion with sync R_reached? from 0 to EVALUATE.
Add state 2 as committed state.
Add transition from 1 to 2 with sync R_reached? and update R_Flag = 1.
Add transition from 2 to 1.

Precedence Chain before untimed

After Q

A[] END imply P_Flag == 1

Nothing more to do for adding objects to the chain.

Precedence Chain after untimed

Between Q and R

A[] R_Flag == 0
A[] END imply P_Flag == 1
For adding objects to the chain:
Same procedure as in scope Before R

Precedence Chain between untimed

After Q and until R

A[] R_Flag == 0
A[] EVALUATE imply P_Flag == 1
For adding objects to the chain:
Same procedure as in scope Before R

Precedence Chain until untimed

Timed

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