From 1f5938ba96c9b235cba95097688b4ee1a033b0a2 Mon Sep 17 00:00:00 2001
From: Artur Meski <artur.meski@gmail.com>
Date: Fri, 19 Feb 2016 18:19:50 +0100
Subject: [PATCH] Translation RSC -> RS. CA translation - to be done.

---
 rctsys.py        | 56 ++++++++++++++++++++++++++++++++++++++++--------
 rssmt.py         | 18 ++++++++++------
 smtcheckerrsc.py |  5 -----
 3 files changed, 59 insertions(+), 20 deletions(-)

diff --git a/rctsys.py b/rctsys.py
index b548b4a..1445f65 100755
--- a/rctsys.py
+++ b/rctsys.py
@@ -172,19 +172,23 @@ class ReactionSystem(object):
 
         self.reactions = []
         self.background_set = []
+
+        #self.reactions_by_agents = [] # each element is 'reactions_by_prod'
+        self.reactions_by_prod = None
+
+        ## legacy:
         self.init_contexts = []
         self.context_entities = []
 
-        self.reactions_by_agents = [] # each element is 'reactions_by_prod'
-
-        self.reactions_by_prod = None
-
     def add_bg_set_entity(self, name):
         if not self.is_in_background_set(name):
             self.background_set.append(name)
         else:
-            print("The entity", name, "is already on the list")
-            raise
+            raise RuntimeError("The entity " + name + " is already on the list")
+    
+    def ensure_bg_set_entity(self, name):
+        if not self.is_in_background_set(name):
+            self.background_set.append(name)
 
     def add_bg_set_entities(self, names):
         for name in names:
@@ -345,12 +349,12 @@ class ReactionSystemWithConcentrations(ReactionSystem):
 
         self.reactions = []
         self.background_set = []
+
         self.context_entities = []
-
-        self.reactions_by_agents = [] # each element is 'reactions_by_prod'
-
         self.reactions_by_prod = None
 
+        self.max_concentration = 0
+
     def is_valid_entity_with_concentration(self, e):
         """Sanity check for entities with concentration"""
         
@@ -389,6 +393,8 @@ class ReactionSystemWithConcentrations(ReactionSystem):
             self.has_non_zero_concentration(r)
             entity,level = r
             reactants.append((self.get_entity_id(entity),level))
+            if self.max_concentration < level:
+                self.max_concentration = level
             
         inhibitors = []
         for i in I:
@@ -396,6 +402,8 @@ class ReactionSystemWithConcentrations(ReactionSystem):
             self.has_non_zero_concentration(i)
             entity,level = i
             inhibitors.append((self.get_entity_id(entity),level))
+            if self.max_concentration < level:
+                self.max_concentration = level
 
         products = []
         for p in P:
@@ -466,6 +474,36 @@ class ReactionSystemWithConcentrations(ReactionSystem):
 
         return reactions_by_prod
 
+    def get_reaction_system(self):
+        
+        rs = ReactionSystem()
+                
+        for reactants,inhibitors,products in self.reactions:
+
+            new_reactants = []
+            new_inhibitors = []
+            new_products = []
+
+            for ent,conc in reactants:
+                n = self.get_entity_name(ent) + "_" + str(conc)
+                rs.ensure_bg_set_entity(n)
+                new_reactants.append(n)
+                
+            for ent,conc in inhibitors:
+                n = self.get_entity_name(ent) + "_" + str(conc)
+                rs.ensure_bg_set_entity(n)
+                new_inhibitors.append(n)
+
+            for ent,conc in products:
+                for i in range(1,conc+1):
+                    n = self.get_entity_name(ent) + "_" + str(i)
+                    rs.ensure_bg_set_entity(n)
+                    new_products.append(n)
+                            
+            rs.add_reaction(new_reactants,new_inhibitors,new_products)
+        
+        return rs
+    
 
 class ReactionSystemWithAutomaton(object):
     
diff --git a/rssmt.py b/rssmt.py
index 3b83dfc..d4cb3cf 100755
--- a/rssmt.py
+++ b/rssmt.py
@@ -69,21 +69,27 @@ def main():
     r.add_bg_set_entities(["a","b","c","d"])
 
     r.add_reaction([("c",1)],[("b",2)],[("c",1),("b",1)])
+    r.add_reaction([("b",2)],[("c",1)],[("c",5),("b",1)])
     r.show()
     
+    print("================================================")
+    
+    ordinary_rs = r.get_reaction_system()
+    ordinary_rs.show()
+    
     # print(r.get_reactions_by_product())
     
     c = ContextAutomatonWithConcentrations(r)
     c.add_init_state("1")
     c.add_transition("1", [("c",1)], "1")
     c.add_transition("1", [("d",2)], "1")
-    c.show()
+    # c.show()
 
-    rc = ReactionSystemWithAutomaton(r,c)
-
-    smt = SmtCheckerRSC(rc)
-
-    smt.check_reachability([('c',1)],print_time=True,max_level=20)
+    # rc = ReactionSystemWithAutomaton(r,c)
+    #
+    # smt = SmtCheckerRSC(rc)
+    #
+    # smt.check_reachability([('c',1)],print_time=True,max_level=20)
 
 if __name__ == "__main__":
     try:
diff --git a/smtcheckerrsc.py b/smtcheckerrsc.py
index ad8ae87..86c7429 100644
--- a/smtcheckerrsc.py
+++ b/smtcheckerrsc.py
@@ -230,14 +230,9 @@ class SmtCheckerRSC(object):
         self.prepare_all_variables()
         self.solver.add(self.enc_init_state(0))
         current_level = 0
-        
-        # print(self.enc_exact_state(current_level,state))
-        #
-        # print(self.enc_produced_concentration(current_level, 1))
 
         self.prepare_all_variables()
         print(And(self.enc_transition_relation(current_level), self.enc_init_state(0)))
-
         
         while True:
             self.prepare_all_variables()