This page describes mappings for property patterns in regular
alternation-free mu-calculus (RAFMC). For other information about
the patterns click on the pattern links.
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.
Pattern Mappings
The patterns written in RAFMC are adequate for action-based systems (the
symbols P, Q, R, etc. denote action predicates). For simplicity, we assume
there is no clash between action predicates, i.e., every action of the system
satisfies at most one predicate P, Q, R, etc. This restriction can be removed
by changing the pattern mappings appropriately.
P is false:
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
P occurs:
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
In these mappings we illustrate one instance of the bounded existence
pattern, where the bound is at most 2 designated actions. Other bounds
can be specified by variations on this mapping.
P occurs at most
2 times:
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
P is true:
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
S precedes
P:
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
S responds to
P:
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
This is the 2 cause-1 effect mapping.
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
This is the 2 stimulus-1 response mapping.
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
This is the 1-2 response chain constrained with a single event.
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.