{{ message }}

Instantly share code, notes, and snippets.

# hwayne/queue_template.py

Created Nov 2, 2020
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