init {
printf("it works\n")
}
proctype you_run(byte x)
{
printf("my x is: %d\n", x)
}
init {
run you_run(1);
run you_run(2)
}
active proctype main() {
run you_run(1);
run you_run(2)
}
active [4] proctype try_me() {
printf("hi, i am process %d\n", _pid)
}
while (a != b) /* not valid Promela syntax */
skip; /* wait for a==b */
...
(a == b);
...
(a == b) -> ...
/*
* Peterson's algorithm for enforcing
* mutual exclusion between two processes
* competing for access to a critical section
*/
bool turn, want[2];
active [2] proctype user()
{
again:
want[_pid] = 1; turn = _pid;
/* wait until this condition holds: */
(want[1 - _pid] == 0 || turn == 1 - _pid);
/* enter */
critical: skip;
/* leave */
want[_pid] = 0;
goto again
}
type name = expression;
type name[constant] = expression
byte a, b[3], c = 4
typedef Field {
short f = 3;
byte g
};
typedef Msg {
byte a[3];
int fld1;
Field fld2;
chan p[3];
bit b
};
Msg foo;
foo.a[2] = foo.fld2.f + 12
proctype me(Msg z) {
z.a[2] = 12
}
init {
Msg foo;
run me(foo)
}
typedef Array {
byte el[4]
};
Array a[4];
c = c + 1; c = c - 1
c++; c--
b = c++
(expr1 -> expr2 : expr3)
variable = expression
chan qname = [16] of { short, byte }
qname!expr1,expr2
qname?var1,var2
qname!expr1(expr2,expr3)
qname?var1(var2,var3)
Some or all of the arguments of the receive operation can be given as constants instead of as variables:
qname?cons1,var2,cons2
proctype A(chan q1)
{ chan q2;
q1?q2;
q2!123
}
proctype B(chan qforb)
{ int x;
qforb?x;
printf("x = %d\n", x)
}
init {
chan qname = [1] of { chan };
chan qforb = [1] of { int };
run A(qname);
run B(qforb);
qname!qforb
}
(qname?var == 0)
(a > b && qname!123)
atomic { (a > b && !full(qname)) -> qname!123 }
empty(qname)
atomic { qname?[0] -> qname?var }
qname?0
!full(qname) -> qname!msgtype
qname?[msgtype] -> qname?msgtype
qname!!msg
qname??msg
chan qname = [N] of { byte }
chan port = [0] of { byte }
#define msgtype 33
chan name = [0] of { byte, byte };
active proctype A()
{ name!msgtype(124);
name!msgtype(121)
}
active proctype B()
{ byte state;
name?msgtype(state)
}
mtype = { ack, msg, error, data };
atomic { /* swap the values of a and b */
tmp = b;
b = a;
a = tmp
}
init {
atomic {
run A(1,2);
run B(2,3);
run C(3,1)
}
}
d_step { /* swap the values of a and b */
tmp = b;
b = a;
a = tmp
}
if
:: (a != b) -> option1
:: (a == b) -> option2
fi
mtype = { a, b };
chan ch = [1] of { byte };
active proctype A()
{ ch!a
}
active proctype B()
{ ch!b
}
active proctype C()
{ if
:: ch?a
:: ch?b
fi
}
byte count;
active proctype counter()
{
if
:: count++
:: count--
fi
}
byte count;
active proctype counter()
{
do
:: count++
:: count--
:: (count == 0) -> break
od
}
active proctype counter()
{
do
:: (count != 0) ->
if
:: count++
:: count--
fi
:: (count == 0) -> break
od
}
active proctype counter()
{
do
:: (count != 0) ->
if
:: count++
:: count--
:: else
fi
:: else -> break
od
}
proctype Euclid(int x, y)
{
do
:: (x > y) -> x = x - y
:: (x < y) -> y = y - x
:: (x == y) -> goto done
od;
done:
skip
}
init { run Euclid(36, 12) }
#define p 0
#define v 1
chan sema = [0] of { bit };
active proctype Dijkstra()
{ byte count = 1;
do
:: (count == 1) ->
sema!p; count = 0
:: (count == 0) ->
sema?v; count = 1
od
}
active [3] proctype user()
{ do
:: sema?p;
/* critical section */
sema!v;
/* non-critical section */
od
}
proctype fact(int n; chan p)
{ chan child = [1] of { int };
int result;
if
:: (n <= 1) -> p!1
:: (n >= 2) ->
run fact(n-1, child);
child?result;
p!n*result
fi
}
init
{ chan child = [1] of { int };
int result;
run fact(7, child);
child?result;
printf("result: %d\n", result)
}
{ P } unless { E }
A;
do
:: b1 -> B1
:: b2 -> B2
...
od
unless { c -> C };
D
A;
do
:: b1 -> B1
:: b2 -> B2
...
:: c -> break
od;
C; D
assert(expression)
proctype Dijkstra()
{ byte count = 1;
end: do
:: (count == 1) ->
sema!p; count = 0
:: (count == 0) ->
sema?v; count = 1
od
}
proctype Dijkstra()
{ byte count = 1;
end: do
:: (count == 1) ->
progress: sema!p; count = 0
:: (count == 0) ->
sema?v; count = 1
od
}
active proctype monitor()
{
progress:
do
:: P -> Q
od
}
active proctype monitor()
{
progress:
do
:: P -> assert(P || Q)
od
}
s0;s1;s2;...
pUq = q || (p && O (pUq))
¤ p = !º !p = !(true U !p)
¤ (P => º Q)
P => Q means !P || (P && Q)
never {
...
}
accept: do :: skip od
do :: skip od
never { /* []p */
do
:: skip /* after an arbitrarily long prefix */
:: p -> break /* p becomes true */
od;
accept: do
:: p /* and remains true forever after */
od
}
never { /* ![]p = <>!p*/
do
:: skip
:: !p -> break
od
}
never { /* ![]p = <>!p*/
do
:: p
:: !p -> break
od
}
never { do :: assert(p) od }
never {
do
:: skip
:: p && !q -> break
od;
accept:
do
:: !q
od
}
never {
do
:: skip /* to match any occurrence */
:: p && q && !r -> break
:: p && !q && !r -> goto error
od;
do
:: q && !r
:: !q && !r -> break
od;
error: skip
}
never {
/* it is not possible for the process with pid=1
* to execute precisely every other step forever
*/
accept:
do
:: _last != 1 -> _last == 1
od
}
never {
/* Whimsical use: claim that it is impossible
* for process 1 to remain in the same control
* state as process 2, or one with smaller value.
*/
accept: do
:: pc_value(1) <= pc_value(2)
od
}
never {
/* it is not possible for the process with pid=1
* to remain enabled without ever executing
*/
accept:
do
:: _last != 1 && enabled(1)
od
}
spin -p spec
spin -p -l -g -r -s -n1 spec
spin -i -p spec
#define Printf(x) skip
spin -a spec
pcc -o pan pan.c # standard exhaustive search
pcc -DREDUCE -o pan pan.c # use partial order reduction
pcc '-DMEMCNT=23' -DREDUCE -o pan pan.c
pcc -DBITSTATE -DREDUCE -o pan pan.c
pan -w23
pan -m100000
pan -m40
pan -l # search for non-progress cycles
pan -a # search for acceptance cycles
pan -f -l # search for fair non-progress cycles
pan -f -a # search for fair acceptance cycles
pan -n -f -a
pan --
spin -t -p spec
spin -t -r -s -l -g spec
pan -c3
pan -c0
pan -d # print state machines
xr q1;
xs q2;