Skip to content

Response Chain Property Pattern N Stimuli 1 Response

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

Description

  • Pattern in the original catalog
  • Structured English Specification: Scope, if S[<Chain>] [has occurred], then in response [within Time(0)] P eventually holds.
  • Chain:= [T1, T2, T3]

State-Based Pattern

How to add an element t4 to the chain:
1. Make END a committed state.
2. Add states 1, 2.
3. Add transition from END to 1, one with guard T4_holds == 0.
4. Add transition from END to 2 with guard T4_holds == 1.
5. Add transition from 1 to 2 with sync T4_reached?.
6. Rename END.
7. Rename 2 to END.
8. If the observer is timed, update timeguards on added transitions and states.
9. Follow scope-specific instructions.

Untimed

Globally

Nothing further to do for adding elelemts to the chain.

P --> END

Response Chain Globally untimed observer

Before R

To add an element to the chain, do the following:
Update the transition to EVALUATE.

A[] not ERROR

Response Chain Before untimed observer

After Q

Nothing further to do for adding elelemts to the chain.

(Q_held_once == 1 and P) --> END

Response Chain After untimed observer

Between Q and R

To add an element to the chain, do the following:
Update the transitions to EVALUATE and ERROR.

A[] not ERROR

Response Chain Between untimed observer

After Q Until R

To add an element to the chain, do the following:
Update the transitions to EVALUATE and ERROR.

P --> END

Response Chain Until untimed observer

Timed

Globally

Nothing further to do for adding elelemts to the chain.

P --> END

Response Chain Globally timed observer

Before R

To add an element to the chain, do the following:
Update the transitions to EVALUATE and ERROR.

A[] not ERROR

Response Chain Before timed observer

After Q

Nothing further to do for adding elelemts to the chain.

(Q_held_once == 1 and P) --> END

Response Chain After timed observer

Between Q and R

To add an element to the chain, do the following:
Update the transitions to EVALUATE and ERROR.

A[] not ERROR

Response Chain Between timed observer

After Q Until R

To add an element to the chain, do the following:
Update the transition to EVALUATE.

P --> END

Response Chain Until timed observer

Clone this wiki locally