Promela / spin 正规化方法

强力软件

Promela / spin 是实现正规化方法进行模型检查的工具。

proctype

active proctype P() {
    printf("hello, world\n");
}

data types

• bit
• byte
• short
• int
• unsigned

Sorry, there is no such thing as float point number for promela.

control statements

selection

if
:: a < b ->
    printf("<");
:: a > b ->
    printf(">");
:: else ->
    printf("==");
fi

If multiple guards are true, spin will choose one randomly ! If none of the guards are true, then the process will be blocked.

repetition

do
:: a > b -> a = a - b
:: b > a -> b = b - a
:: a == b -> break
od

for-loops

Em, this looks more tidy than do pair.

int i;
int sum = 0;
for (i : 1 .. 5 ) {
    sum = sum + i;
}

array

You can use for-each syntax like Java.

byte a[5];
int sum = 0;
for (i in a) {
    sum = sum + a [i]
}

jumps

Here comes the famous goto.

active proctype P() {
    do
    :: i > 5 ->
        goto exitloop;
    :: else ->
        sum = sum + i;
        i++;
    od;
exitloop:
    printf ("end")
}

inline code

Promela has no methods or procedure calls. You have to use inline code.

inline foo(bar) {
    printf(bar);
}
active proctype P() {
    foo("!");
}

atomicity

atomic

Looks like Java synchronized keyword, which protects critical areas from being executed by multiple processes at the same time.

atomic {
if
:: a != 0 ->
    c = b / a
:: else ->
    c = b
fi
}

d_step

Like atomic but has strong atomicity.

d_step {
    tmp = b;
    b = tmp + 1;
}

details

anonymous variable

They are doomed to abandoned. Anonymous variable _ ignore assignments.

chan c;
c ? _;