Add PRISM backend to probably

[linusheck]

This PR adds a PRISM backend to probably. It can convert pCGL programs to PRISM!

For an example, I slightly modified the example.pctl because the loop would never execute (because by default the model checker wouldn't do the probabilities for all values of f, only initialises f to false if not specified).
From this program, you can get a PRISM file:

> cat example.pgcl

bool f;
nat c;
while (c < 10) {
     {c := c+1} [0.8] {f:=true}
}

> poetry run probably example.pgcl --prism > example.prism
> cat example.prism

dtmc
module program
f : bool;
c : int;
ppc : int init 0;
ter : bool init false;
[] (ter=false & ppc=0) -> (ter'=true);
[] (ter=true & ppc=0 & (c) < (10)) -> (ter'=false)&(ppc'=1);
[] (ter=true & ppc=0 & !((c) < (10))) -> (ter'=false)&(ppc'=-1);
[] (ter=false & ppc=1) -> (ter'=true);
[] (ter=true & ppc=1) -> 4/5 : (ppc'=2)&(ter'=false) + 1-(4/5) : (ppc'=3)&(ter'=false);
[] (ter=false & ppc=2) -> (ter'=true)&(c'=(c) + (1));
[] (ter=true & ppc=2) -> (ter'=false)&(ppc'=0);
[] (ter=false & ppc=3) -> (ter'=true)&(f'=true);
[] (ter=true & ppc=3) -> (ter'=false)&(ppc'=0);
endmodule

You can plug that into your favourite model checker:

storm --prism example.prism -prop "P=? [F f]" --exact # what is the probability that at some point, f is true?
Model checking property "1": P=? [F (f)] ...
Result (for initial states): 8717049/9765625 (approx. 0.8926258176)
Time for model checking: 0.001s.

The tests currently only check whether the PRISM translation doesn't crash, I'm not sure how to verify the correctness of the output without implementing a PRISM parser or something :D

What would be nice:

• build a couple of pCGL examples that are meant for plugging into a model checker
• somehow add labels, make it a bit more integrated with the model checker

[linusheck]

I built the Herman self-stabilising protocol. The PRISM is actually more elegant for this one, but just as a proof-of-concept! There is some code duplication for computing the number of tokens.

The bounds of the variables are optional, but required if you want to use Storm in symbolic mode.

const p := 0.5;

# Number of participants in the herman protocol
const n := 11;

# Holds state, ith bit is the bit of the ith process
nat state [0, 2^n];
nat statetmp [0, 2^n];

nat i [0, n];
nat j [0, n];
nat numtokenstmp [0, n];
nat numtokens [0, n];
nat out [0, 1];

bool step;

# Randomly initialize state
i := 0;
while (i < n) {
    {statetmp := statetmp + 2^i} [1/2] {};
    i := i + 1;
}
state := statetmp;

# Compute initial number of tokens
numtokenstmp := 0;
i := 0;
while (i < n) {
    # i == this process
    # j == next process
    j := i + 1;
    if (j = n) {
        j := 0;
    } else {}
    if ((state / 2^i) % 2 = (state / 2^j) % 2) {
        numtokenstmp := numtokenstmp + 1;
    } else {}
    i := i + 1;
}
numtokens := numtokenstmp;

while (not (numtokens = 1)) {
    # Do step of the algorithm
    i := 0;
    statetmp := 0;
    while (i < n) {
        # i == this process
        # j == next process
        j := i + 1;
        if (j = n) {
            j := 0;
        } else {}

        # actual herman's algorithm
        if ((state / 2^i) % 2 = (state / 2^j) % 2) {
            {out := 0} [1/2] {out := 1};
        } else {
            out := (state / 2^j) % 2;
        }

        # set the out bit in state       
        statetmp := statetmp + 2^i * out;

        i := i + 1;
    }

    state := statetmp;
    
    # register a step
    step := true;
    step := false;
    
    # Compute number of tokens
    numtokenstmp := 0;
    i := 0;
    while (i < n) {
        # i == this process
        # j == next process
        j := i + 1;
        if (j = n) {
            j := 0;
        } else {}
        if ((state / 2^i) % 2 = (state / 2^j) % 2) {
            numtokenstmp := numtokenstmp + 1;
        } else {}
        i := i + 1;
    }
    numtokens := numtokenstmp;
}

../storm/build/bin/storm --prism herman.prism -prop "P=? [F numtokens=1]"
Model checking property "1": P=? [F (numtokens = 1)] ...
Result (for initial states): 1
Time for model checking: 1.713s.

To use the step variable, for now I manually added a reward to the prism file:

rewards "steps"
	step : 1;
endrewards

and then we can check the number of steps until the protocol stabilises:

../storm/build/bin/storm --prism herman.prism -prop "R=? [F numtokens=1]"
Model checking property "1": R[exp]=? [F (numtokens = 1)] ...
Result (for initial states): 24.41195636
Time for model checking: 4.657s.