Skip to main content

Cheat Sheet

Author @wadhah101

conditions​

if no instruction is executable "if" blocks else if only one is it's options will gets excuted else if multiple insctructions are valid, one will be randomly chosen

proctype A(){
    if
        ::instr1 -> options1
        ::instrN -> optionsN
    fi;
}

While loop​

the instruction to execute is chosen randomly

do
    :: count = count - 1
    :: (count == 0) -> break;
od;

Functions​

    proctype A() {
        work();
    }

Main​

<!-- note:  every functions runs in parllel with no particular order -->
init {
    run A(2); run B(2,3);
}

<!-- or use active before function definition -->
active proctype A() {
    work();
}

Atomic instruction​

java​

class Main {

  synchronized void work() {}
}

promela​

proctype A(){
    atomic
    {
        work();
    }
}

Channels ( ~ Arrays )​

definition​

chan gname = [20] of {short}
chan gnameObject = [10] of {short, byte}

send​

proctype A(chan q) {
    q!28 ;
}

receive​

proctype A(chan q) {
    int x ;
    q?x ;
}

Finite state machines modeling​

we have 4 place s1 , s2 , s3 , s4

proctype A(){
    s1: if
        :: x ? a -> goto s2
        :: x ? b -> goto s3
        :: else -> skip
    s2 : ..

    s3 :
        goto s4 ;
}