From 06a28f9e5447b419a44241a8662c7e5a4fce2d75 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 29 Apr 2018 18:54:19 +0100
Subject: [PATCH] Mutext DRS generator

---
 formrsctlk.cc       |  2 +-
 in/gen_drs_mutex.py | 82 +++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 83 insertions(+), 1 deletion(-)
 create mode 100755 in/gen_drs_mutex.py

diff --git a/formrsctlk.cc b/formrsctlk.cc
index 334fa0d..044cc38 100644
--- a/formrsctlk.cc
+++ b/formrsctlk.cc
@@ -155,7 +155,7 @@ std::string FormRSCTLK::toStr(void) const
     return "NK[" + getSingleAgent() + "](" + arg[0]->toStr() + ")";
   }
   else if (oper == RSCTLK_UK) {
-    return "UK[" + getSingleAgent() + "](" + arg[0]->toStr() + ")";
+    return "K[" + getSingleAgent() + "](" + arg[0]->toStr() + ")";
   }
 
   else {
diff --git a/in/gen_drs_mutex.py b/in/gen_drs_mutex.py
new file mode 100755
index 0000000..9a3e4b1
--- /dev/null
+++ b/in/gen_drs_mutex.py
@@ -0,0 +1,82 @@
+#!/usr/bin/env python
+
+from sys import argv,exit
+
+OPTIONS_STR = """
+options { use-context-automaton; }
+"""
+CONTROLLER_STR = """
+    ct {
+        {{lock},{release} -> {lock}};
+        {{req},{} -> {lock}};
+    };
+"""
+
+PROC_STR = """
+    proc{:d} {{
+        {{{{out, busy}}, {{}} -> {{req}}}};
+        {{{{out}}, {{}} -> {{req}}}};
+        {{{{req}}, {{lock}} -> {{in}}}};
+        {{{{in}}, {{busy}} -> {{out, release}}}};
+        {{{{in, busy}}, {{}} -> {{in}}}};
+        {{{{in, lock}}, {{}} -> {{req}}}};
+    }};
+"""
+
+CA_STR = """
+context-automaton {{
+    states {{ s0, s1 }}
+    init-state {{ s0 }}
+    transitions {{
+{:s}
+    }}
+}}
+"""
+
+PROPERTY_STR = """
+rsctlk-property { AG(proc0.in IMPLIES K[proc0](~proc1.in) ) }
+"""
+
+
+#################################################################
+
+if len(argv) < 2:
+    print("Usage: {:s} <number of modules>".format(argv[0]))
+    exit(100)
+
+n = int(argv[1])
+
+out = ""
+
+out += OPTIONS_STR
+out += "reactions {\n"
+out += CONTROLLER_STR
+for i in range(n):
+    out += PROC_STR.format(i)
+out += "}\n"
+
+transitions = ""
+
+init_trans = 8*" " + "{ ct={} "
+for i in range(n):
+    init_trans += "proc{:d}={{out}} ".format(i)
+
+init_trans += "}: s0 -> s1;\n"
+
+transitions += init_trans
+
+for i in range(n):
+    transitions += "{:s}{{ ct={{}} proc{:d}={{}} }}: s1 -> s1;\n".format(8*" ", i)    
+
+out += CA_STR.format(transitions)
+
+out += PROPERTY_STR
+
+print(out)
+
+        # { ct={} proc1={out} }: s0 -> s1;
+        # { ct={} proc2={out} }: s0 -> s1;
+        
+        # { ct={} proc1={} }: s1 -> s1;
+        # { ct={} proc2={} }: s1 -> s1;
+