Instantly share code, notes, and snippets.

# hwayne/queue_template.py

Created November 2, 2020 02:47
Code for PRISM essay

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

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