Skip to content

Constrained Response Chain Property Pattern 1 Stimulus N Responses

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

Description

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

State-Based Pattern

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

Untimed

Globally

Nothing further to do for adding elements to the chain.

P --> (END and Z_Flag = 0)
A[] END imply Z_Flag = 0

ConstrainedResponse globally untimed observer

Before R

To add an element to the chain, do the following:
Update the transition to EVALUATE.
A[] EVALUATE imply Z_Flag = 0
A[] not ERROR

ConstrainedResponse before R untimed observer

After Q

Nothing further to do for adding elelemts to the chain.

(Q_held_once == 1 and P) --> (END and Z_Flag = 0)
A[] END imply Z_Flag = 0

ConstrainedResponse after Q untimed observer

Between Q and R

To add an element to the chain, do the following:
Update the transitions to EVALUATE and ERROR.
A[] EVALUATE imply Z_Flag = 0
A[] not ERROR

ConstrainedResponse between Q and R 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 and Z_Flag = 0)
A[] END imply Z_Flag = 0

ConstrainedResponse after Q until R untimed observer

Timed

Globally

Nothing forther to do for adding elelemts to the chain.

P --> (END and Z_Flag = 0)
A[] END imply Z_Flag = 0

ConstrainedResponse globally timed observer

Before R

To add an element to the chain, do the following:
Update the transitions to EVALUATE and ERROR.
A[] EVALUATE imply Z_Flag = 0
A[] not ERROR

ConstrainedResponse before R timed observer

After Q

Nothing forther to do for adding elelemts to the chain.

(Q_held_once == 1 and P) --> (END and Z_Flag = 0)
A[] END imply Z_Flag = 0

ConstrainedResponse after Q timed observer

Between Q and R

To add an element to the chain, do the following:
Update the transitions to EVALUATE and ERROR.
A[] EVALUATE imply Z_Flag = 0
A[] not ERROR

ConstrainedResponse between Q and R timed observer

After Q Until R

To add an element to the chain, do the following:
Update the transition to EVALUATE.
P --> (END and Z_Flag = 0)
A[] END imply Z_Flag = 0

ConstrainedResponse after Q until R timed observer

Clone this wiki locally