Skip to content

Instantly share code, notes, and snippets.

@hwayne
Created November 2, 2020 02:47
Show Gist options
  • Save hwayne/00ec2cef54a3031ec304ccb44eeaa42a to your computer and use it in GitHub Desktop.
Save hwayne/00ec2cef54a3031ec304ccb44eeaa42a to your computer and use it in GitHub Desktop.
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