Instantly share code, notes, and snippets.

# hwayne/queue_template.py

Created November 2, 2020 02:47
Show Gist options
• 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.

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