Until Property Pattern

• Description
• State-Based Pattern

Description

• Pattern in the original catalog
• As the formulae in the original catalogue do not distinguish between the Between Q and R and the After Q and Until R scopes, the formulae for the Between Q and R scope are worked out by ourselves, they DO NOT match to the formulae!
• Structured English Specification: Scope, P [holds] without interruption until S [holds].

State-Based Pattern

Untimed

Globally

A[] INIT imply P /as precondition/
A[] INIT imply S /as exit condition/
INIT --> O1

Before R

A[] not R /as exit condition, property is satisfied if true/
A[] INIT imply P /as precondition/
A[] INIT imply R /as exit condition/
A[] INIT imply S /as exit condition/
INIT --> O1

After Q

A[] INIT imply P /as precondition/
A[] INIT imply S /as exit condition/
INIT --> O1

Between Q and R

observer does not match the original formula

Our revised version of the formula: AG ( (Q /\ not(R) /\ AF(R)) -> ( (P U S) U R) )

A[] not Q /as exit condition/
A[] not R /as exit condition/
A[] INIT imply Q /as exit condition/
A[] O2 imply R /as exit condition/
A[] O2 imply S /as exit condition/
A[] not ERROR

After Q until R

A[] not ERROR
O1 --> O2

Timed

Globally

A[] INIT imply P /as precondition/
INIT --> O1

Before R

A[] INIT imply R /as exit condition/
A[] INIT imply S /as exit condition/
A[] not ERROR

After Q

A[] INIT imply P /as precondition/
INIT --> O1

Between Q and R

observer does not match the original formula

Our revised version of the formula: AG ( (Q /\ AF(R) /\ AG[0,t1]( not(R) )) -> ( (P U[t1,t2] S) U R) )

A[] not ERROR

After Q until R

A[] not ERROR