Generators: cleanup

examples/bdd/generators/old_syntax/gen_bc.py

@@ -0,0 +1,88 @@
+#!/usr/bin/env python3
+"""
+Generator for the Binary Counter (BC) benchmark.
+
+Produces a reaction system modelling an N-bit binary counter
+with increment and decrement operations controlled via context
+entities. Generates one of four RSCTL properties.
+
+NOTE: generates old-syntax input (context-entities, initial-contexts,
+rsctl-property) which is not compatible with the current parser.
+"""
+
+import argparse
+
+K = 8  # constant used by property 3
+
+
+def generate(n, prop):
+    out = "reactions {\n"
+
+    # (1) no dec, no inc: bits persist
+    out += "\t# (1) no decrement, no increment\n"
+    for j in range(n):
+        out += "\t{{{{p{j}}},{{dec,inc}} -> {{p{j}}}}};\n".format(j=j)
+
+    # (2) increment operation
+    out += "\n\t# (2) increment operation\n"
+    out += "\t{{inc},{dec,p0} -> {p0}};\n"
+    for j in range(1, n):
+        bits = ",".join("p" + str(k) for k in range(j))
+        out += "\t{{{{inc,{bits}}},{{dec,p{j}}} -> {{p{j}}}}};\n".format(bits=bits, j=j)
+
+    out += "\n\t# the more significant bits remain (inc)\n"
+    for j in range(n):
+        for k in range(j + 1, n):
+            out += "\t{{{{inc,p{k}}},{{dec,p{j}}} -> {{p{k}}}}};\n".format(j=j, k=k)
+
+    # (3) decrement operation
+    out += "\n\t# (3) decrement operation\n"
+    for j in range(n):
+        bits = ",".join("p" + str(k) for k in range(j + 1))
+        out += "\t{{{{dec}},{{inc,{bits}}} -> {{p{j}}}}};\n".format(bits=bits, j=j)
+
+    out += "\n\t# the more significant bits remain (dec)\n"
+    for j in range(n):
+        for k in range(j + 1, n):
+            out += "\t{{{{dec,p{j},p{k}}},{{inc}} -> {{p{k}}}}};\n".format(j=j, k=k)
+
+    out += "}\n\n"
+    out += "context-entities { inc,dec }\n"
+    out += "initial-contexts { {} }\n"
+
+    if prop == 1:
+        all_neg = " AND ".join("~p" + str(i) for i in range(n))
+        all_pos = " AND ".join("p" + str(i) for i in range(n))
+        out += "rsctl-property {{ AG(({}) IMPLIES E[{{inc}},{{dec}}]F({})) }}\n".format(
+            all_neg, all_pos)
+    elif prop == 2:
+        all_pos = " AND ".join("p" + str(i) for i in range(n))
+        all_neg = " AND ".join("~p" + str(i) for i in range(n))
+        out += "rsctl-property {{ AG(({}) IMPLIES A[{{inc}}]X({})) }}\n".format(
+            all_pos, all_neg)
+    elif prop == 3:
+        parts = ["p" + str(i) for i in range(n - K)]
+        parts += ["~p" + str(i) for i in range(n - K, n)]
+        out += "rsctl-property {{ E[{{inc}}]F({}) }}\n".format(" AND ".join(parts))
+    elif prop == 4:
+        out += "rsctl-property {{ AG( p{} IMPLIES EF ~p{} ) }}\n".format(n - 1, n - 1)
+
+    return out
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__,
+        formatter_class=argparse.RawDescriptionHelpFormatter)
+    parser.add_argument("n", type=int, help="number of bits")
+    parser.add_argument("property", type=int, choices=[1, 2, 3, 4],
+        help="property to generate (1-4)")
+    args = parser.parse_args()
+
+    if args.property == 3 and args.n < K + 1:
+        parser.error("n must be >= {} for property 3".format(K + 1))
+
+    print(generate(args.n, args.property))
+
+
+if __name__ == "__main__":
+    main()