diff --git a/in/scripts/gen_asm.py b/in/scripts/gen_asm.py new file mode 100755 index 0000000..56dc0f6 --- /dev/null +++ b/in/scripts/gen_asm.py @@ -0,0 +1,89 @@ +#!/usr/bin/env python + +from sys import argv,exit + +OPTIONS_STR = """ +options { use-context-automaton; make-progressive; } +""" + +PROC_STR = """ + proc{:d} {{ + {{{{a}}, {{s}} -> {{y}}}}; + {{{{y}}, {{s}} -> {{y}}}}; + {{{{a}}, {{s}} -> {{b}}}}; + {{{{b}}, {{s}} -> {{c}}}}; + {{{{c}}, {{s}} -> {{d}}}}; + {{{{d,y}}, {{s}} -> {{dy}}}}; + }}; +""" + +FINAL_PROC = """ + procFinal { + {{done}, {s} -> {done}}; + }; +""" + +CA_STR = """ +context-automaton {{ + states {{ init, act }} + init-state {{ init }} + transitions {{ +{:s} + }} +}} +""" + +PROPERTY_STR = """ +rsctlk-property {{ {:s} : {:s} }} +""" + + +################################################################# + +if len(argv) < 1: + print("Usage: {:s} ".format(argv[0])) + exit(100) + +n = int(argv[1]) + +assert n > 1, "number of proc must be > 1" + +out = "" + +out += OPTIONS_STR +out += "reactions {\n" +for i in range(1, n+1): + out += PROC_STR.format(i) + +out += FINAL_PROC +out += "}\n" + +transitions = "" + +init_trans = 8*" " + "{ proc1={a} }: init -> act;\n" +transitions += init_trans + +for i in range(1, n+1): + transitions += "{:s}{{ proc{:d}={{}} }}: act -> act;\n".format(8*" ", i, i) + +for i in range(2, n+1): + transitions += "{:s}{{ proc{:d}={{a}} }}: act -> act : proc{:d}.dy;\n".format(8*" ", i, i-1) + +final_cond = "proc1.dy" +for i in range(1, n+1): + final_cond += " AND proc{:d}.dy".format(i) + +transitions += "{:s}{{ procFinal={{done}} }}: act -> act : {:s};\n".format(8*" ", final_cond) + +out += CA_STR.format(transitions) + +# f1 +formula = "EF( procFinal.done )" +out += PROPERTY_STR.format("f1",formula) + +# f2 +formula = "EF( ~procFinal.done )" +out += PROPERTY_STR.format("f2",formula) + +print(out) +