Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Code for PRISM essay

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

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)))
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.