Change line 20 of the python script to change the number of workers. Pipe output to a .prism
file.
Code for PRISM essay
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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))) | |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
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