From b7c4cd69064b7def01163c3876411fc64d242041 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Sun, 29 Apr 2018 19:58:17 +0100
Subject: [PATCH] Scalable formula

---
 in/gen_drs_mutex.py | 17 ++++++++++++-----
 symrs.cc            |  6 +++++-
 2 files changed, 17 insertions(+), 6 deletions(-)

diff --git a/in/gen_drs_mutex.py b/in/gen_drs_mutex.py
index 852488d..acb8adb 100755
--- a/in/gen_drs_mutex.py
+++ b/in/gen_drs_mutex.py
@@ -34,17 +34,20 @@ context-automaton {{
 """
 
 PROPERTY_STR = """
-rsctlk-property { AG(proc0.in IMPLIES K[proc0](~proc1.in) ) }
+rsctlk-property {{ {:s} }}
 """
 
 
 #################################################################
 
 if len(argv) < 2:
-    print("Usage: {:s} <number of modules>".format(argv[0]))
+    print("Usage: {:s} <number of processes> <property number>".format(argv[0]))
     exit(100)
 
 n = int(argv[1])
+f = int(argv[2])
+
+assert n > 1, "number of proc must be > 1"
 
 out = ""
 
@@ -70,9 +73,13 @@ for i in range(n):
 
 out += CA_STR.format(transitions)
 
-out += PROPERTY_STR
+if f == 1:
+    subf = "~proc1.in"
+    for i in range(2, n):
+        subf += " AND ~proc{:d}.in".format(i)
+    formula = "AG( proc0.in IMPLIES K[proc0]({:s}) )".format(subf)
+
+out += PROPERTY_STR.format(formula)
 
 print(out)
 
-
-
diff --git a/symrs.cc b/symrs.cc
index 7c35081..75c6a3e 100644
--- a/symrs.cc
+++ b/symrs.cc
@@ -596,7 +596,6 @@ BDD SymRS::encEnabledness(Process prod_proc_id, Entity entity_id)
 
   auto production_conditions = prod_conds[prod_proc_id][entity_id];
 
-
   VERB_LN(5, "| Produce " << rs->getEntityName(entity_id) << " in " << rs->getProcessName(prod_proc_id) << ":");
 
   for (const auto &cond : production_conditions) {
@@ -639,6 +638,11 @@ BDD SymRS::encEnabledness(Process prod_proc_id, Entity entity_id)
 
   } // END FOR: cond
 
+  if (opts->reorder_trans) {
+    VERB_L2("Reordering");
+    Cudd_ReduceHeap(cuddMgr->getManager(), CUDD_REORDER_SIFT, 10000);
+  }
+
   return enab;
 }