These pattern mappings can be used with the EVALUATOR 3.5 model-checker of CADP.
Information about the entire pattern system is available at the Specification Patterns Home Page.
Globally | [true*. P] false |
Before R | [(not R)*. P. (not R)*. R] false |
After Q | [(not Q)*. Q. true*. P] false |
Between Q and R | [true*. Q. (not R)*. P. (not R)*. R] false |
After Q until R | [true*. Q. (not R)*. P] false |
Globally | mu X. (<P> true or <not P> X) and [not P] X |
Before R | [(not P)*. R] false |
After Q | [(not Q)*. Q] mu X. (<P> true or <not P> X) and [not P] X |
Between Q and R | [true*. Q. (not (P or R))*. R] false |
After Q until R | [true*. Q] mu X. (<P> true or <not P> X) and [R] false and [not P] X |
Globally | [(not P)*. P. (not P)*. P. (not P)*. P] false |
Before R | [(not R)*. P. (not R)*. P. (not R)*. P. (not R)*. R] false |
After Q | [(not Q)*. Q. (not P)*. P. (not P)*. P. (not P)*. P] false |
Between Q and R | [true*. Q. (not R)*. P. (not R)*. P. (not R)*. P. (not R)*. R] false |
After Q until R | [true*. Q. (not R)*. P. (not R)*. P. (not R)*. P] false |
Globally | [true*. not P] false |
Before R | [(not R)*. not (P or R). (not R)*. R] false |
After Q | [(not Q)*. Q. true*. not P] false |
Between Q and R | [true*. Q. (not R)*. not (P or R). (not R)*. R] false |
After Q until R | [true*. Q. (not R)*. not (P or R)] false |
Globally | [(not S)*. P] false |
Before R | [(not (S or R))*. P. (not R)*. R] false |
After Q | [(not Q)*. Q. (not S)*. P] false |
Between Q and R | [true*. Q. (not (S or R))*. P. (not R)*. R] false |
After Q until R | [true*. Q. (not (S or R))*. P] false |
Globally | [true*. P] mu X. (<S> true or <not S> X) and [not S] X |
Before R | [(not R)*. P. (not (S or R))*. R] false |
After Q | [(not Q)*. Q. true*. P] mu X. (<S> true or <not S> X) and [not S] X |
Between Q and R | [true*. Q. (not R)*. P. (not (S or R))*. R] false |
After Q until R | [true*. Q. (not R)*. P] mu X. (<S> true or <not S> X) and [R] false and [not S] X |
S, T precede P:
Globally | [(not S)*. (nil | (S. (not T)*)). P] false |
Before R | [(not (S or R))*. (nil | (S. (not (T or R))*)). P. (not R)*. R] false |
After Q | [(not Q)*. Q. (not S)*. (nil | (S. (not T)*)). P] false |
Between Q and R |
[true*. Q. (not (S or R))*. (nil | (S. (not (T or R))*)). P.
(not R)*. R] false |
After Q until R | [true*. Q. (not (S or R))*. (nil | (S. (not (T or R))*)). P] false |
This is the 1 cause-2 effect mapping.
P precedes S, T:
Globally | [(not P)*. S. (not T)*. T] false |
Before R | [(not (P or R))*. S. (not (T or R))*. T. (not R)*. R] false |
After Q | [(not Q)*. Q. (not P)*. S. (not T)*. T] false |
Between Q and R | [true*. Q. (not (P or R))*. S. (not (T or R))*. T. (not R)*. R] false |
After Q until R | [true*. Q. (not (P or R))*. S. (not (T or R))*. T] false |
P responds to S, T:
Globally | [true*. S. (not T)*. T] mu X. (<P> true or <not P> X) and [not P] X |
Before R | [true*. S. (not T)*. T. (not P)*. R] false |
After Q | [(not Q)*. Q. true*. S. (not T)*. T] mu X. (<P> true or <not P> X) and [not P] X |
Between Q and R |
[true*. Q. (not (S or R))*. S. (not (T or R))*. T.
(not (P or R))*. R] false |
After Q until R |
[true*. Q. (not (S or R))*. S. (not (T or R))*. T]
mu X. (<P> true or <not P> X) and [R] false and [not P] X |
This is the 1 stimulus-2 response mapping.
S, T respond to P:
Globally |
[true*. P] mu X. (<S> true or <not S> X) and
[S] mu Y. ((<T> true or <not T> Y) and [not T] Y) and [not S] X |
Before R | [(not R)*. P. (not (S or R))*. (nil | (S. (not (T or R))*)). R] false |
After Q |
[(not Q)*. Q. true*. P] mu X. (<S> true or <not S> X) and
[S] mu Y. ((<T> true or <not T> Y) and [not T] Y) and [not S] X |
Between Q and R |
[true*. Q. (not R)*. P. (not (S or R))*.
(nil | (S. (not (T or R))*)). R] false |
After Q until R |
[true*. Q. (not R)*. P] mu X. (<S> true or <not S> X) and [R] false and
[S] mu Y. ((<T> true or <not T> Y) and [R] false and [not T] Y) and [not S] X |
S, T without Z respond to P:
Globally |
[true*. P] mu X . (<S> true or <not S> X) and
[S] mu Y. ((<T> true or <not T> Y) and [Z] false and [not T] Y) and [not S] X |
Before R |
[(not R)*. P. (not (S or R))*.
(nil | (S. (nil | ((not (T or R))*. Z)). (not (T or R))*)). R] false |
After Q |
[(not Q)*. Q. true*. P] mu X. (<S> true or <not S> X) and
[S] mu Y. ((<T> true or <not T> Y) and [Z] false and [not T] Y) and [not S] X |
Between Q and R |
[true*. Q. (not R)*. P. (not (S or R))*.
(nil | (S. (nil | ((not (T or R))*. Z)). (not (T or R))*)). R] false |
After Q until R |
[true*. Q. (not R)*. P] mu X. (<S> true or <not S> X) and [R] false and
[S] mu Y. ((<T> true or <not T> Y) and [Z or R] false and [not T] Y) and [not S] X |
Author: Radu Mateescu (INRIA/VASY team). Last updated 2019/01/14 13:11:22.