Change line 20 of the python script to change the number of workers. Pipe output to a .prism
file.
Code for PRISM essay
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