Code for PRISM essay

readme.md

Change line 20 of the python script to change the number of workers. Pipe output to a .prism file.

queue_template.py

from math import comb
from string import Template


guard = "[worker] (left >= {n} & ((queue >= {n} & K = {n}) | (queue = {n} & K > {n}))) ->"

# For n = 3, this should be
# p^3 + 3p^2(1-p) + 3p(1-p)^2 + (1-p)^3
def actions_for(n):
    base = "{prob}: (left' = left - {x}) & (queue' = queue - {x})"
    out = [] # For formatting
    for i in range(0, n+1): # Inclusive of n
        prob = f"{comb(n, i)}*pow(P_worker, {i})*pow(1-P_worker,{n-i})" #f"{comb(n,i)*pow(P_worker,{i})
        out.append(base.format(prob=prob, x=i))
    outstr = "  " + "\n\t+ ".join(out) + ";"
    return outstr


worker = []
for k in range(1, 5):
    tmp = []
    tmp.append(guard.format(n=k,k=k))
    tmp.append(actions_for(k))
    worker.append("\n\t".join(tmp))

with open("worker_template.txt") as f:
    spec = Template(f.read())


print(spec.substitute(worker="\n\n".join(worker)))

worker_template.txt

dtmc

const int N; // Max Tasks
const double P_request; // in [0, 1]
const double P_worker; // in [0, 1]
const int K; // [1, ]

module queues
  left : [0..N] init N;
  queue: [0..N] init 0;


$worker


  [] (left = 0) -> true;

  [inbound] (queue < left & left <= N) ->
	P_request: (queue' = queue + 1)
	+ (1 - P_request): true;
endmodule

rewards "wait_time"
  [worker] queue > K: queue - K;
endrewards

rewards "total_time"
  [worker] left > 0: 1;
endrewards