parameters - z3... variables

rs/__init__.py

@@ -2,7 +2,7 @@ from rs.reaction_system import ReactionSystem
 from rs.context_automaton import ContextAutomaton
 
 from rs.reaction_system_with_concentrations import ReactionSystemWithConcentrations
-from rs.reaction_system_with_concentrations_param import ReactionSystemWithConcentrationsParam, ParameterObj
+from rs.reaction_system_with_concentrations_param import ReactionSystemWithConcentrationsParam, ParameterObj, is_param
 from rs.context_automaton_with_concentrations import ContextAutomatonWithConcentrations
 
 from rs.extended_context_automaton import ExtendedContextAutomaton

rs/reaction_system_with_concentrations_param.py

@@ -11,6 +11,9 @@ class ParameterObj(object):
     def __repr__(self):
         return "@{0}".format(self.name)
 
+def is_param(some_object):
+    if isinstance(some_object, ParameterObj):
+        return True
 
 class ReactionSystemWithConcentrationsParam(ReactionSystem):
 
@@ -251,9 +254,21 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
                         " ) Command=( " + self.get_entity_name(command) + " ) ] -- ( R={" + self.state_to_str(reactants) + "}, I={" + self.state_to_str(inhibitors) + "} )")
                 else:
                     raise RuntimeError("Unknown meta-reaction type: " + repr(r_type))
+                    
+    def show_param_reactions(self, soft=False):
+        print(C_MARK_INFO + " Parametric reactions:")
+        if soft and len(self.parametric_reactions) > 50:
+            print(" -> there are more than 50 reactions (" + str(len(self.parametric_reactions)) + ")")
+        else:
+            print(" "*4 + "{0: ^35}{1: ^25}{2: ^15}".format("reactants"," inhibitors"," products"))
+            for reactants,inhibitors,products in self.parametric_reactions:
+                print(" " + "- {0: ^35}{1: ^25}{2: ^15}".format(
+                    "{ " + self.state_to_str(reactants) + " }",
+                    " { " + self.state_to_str(inhibitors) + " }",
+                    " { " + self.state_to_str(products) + " }"))
 
     def show_max_concentrations(self):
-        print(C_MARK_INFO + " Maximal allowed concentration levels (for optimized translation to RS):")
+        print(C_MARK_INFO + " Maximal allowed concentration levels:")
         for e,max_conc in self.max_conc_per_ent.items():
             print(" - {0:^20} = {1:<6}".format(self.get_entity_name(e),max_conc))
 
@@ -265,6 +280,7 @@ class ReactionSystemWithConcentrationsParam(ReactionSystem):
     def show(self, soft=False):
         self.show_background_set()
         self.show_reactions(soft)
+        self.show_param_reactions(soft)
         self.show_permanent_entities()
         self.show_meta_reactions()
         self.show_max_concentrations()

smt/smt_checker_rsc_param.py

@@ -11,6 +11,8 @@ from colour import *
 
 from logics import rsLTL_Encoder
 
+from rs.reaction_system_with_concentrations_param import ParameterObj, is_param
+
 # def simplify(x):
 #     return x
 
@@ -157,19 +159,22 @@ class SmtCheckerRSCParam(object):
         background set.
         """
         
-        # TODO:
-        #
-        # We should be checking here if we acutally need 
-        # any variables for parameters, because there might
-        # be no parameters in RS
-        
         level = self.next_level_to_encode  
-            
+ 
-        params = []    
+        param_vars_for_cur_level = dict()
-        for entity in self.rs.background_set:
+
-            new_var = Int("L{:d}_Pm_{:s}".format(level, entity))
+        for param_name in self.rs.parameters.keys():
-            params.append(new_var)
+
-        self.v_param.append(params)
+            # we start collecting bg-related vars for the given param
+            vars_for_param = []
+
+            for entity in self.rs.background_set:
+                new_var = Int("L{:d}_Pm_{:s}".format(level, entity))
+                vars_for_param.append(new_var)
+
+            param_vars_for_cur_level[param_name] = vars_for_param
+        
+        self.v_param.append(param_vars_for_cur_level)
         
         print(self.v_param)
         
@@ -270,6 +275,21 @@ class SmtCheckerRSCParam(object):
 
         return enc_reaction
 
+    def enc_single_param_reaction(self, level, p_reaction):
+        
+        reactants, inhibitors, products = p_reaction
+        
+        if is_param(reactants):
+            print("PARAM")
+        
+        if is_param(inhibitors):
+            print("PARAM")
+            
+        if is_param(products):
+            print("PARAM")
+        
+        return True
+
     def enc_rs_trans(self, level):
         """Encodes the transition relation"""
 
@@ -293,6 +313,11 @@ class SmtCheckerRSCParam(object):
             enc_reaction = self.enc_single_reaction(level, reaction)
             enc_trans = simplify(And(enc_trans, enc_reaction))
 
+        for p_reaction in self.rs.parametric_reactions:
+            print(p_reaction)
+            enc_p_reaction = self.enc_single_param_reaction(level, p_reaction)
+            enc_trans = simplify(And(enc_trans, enc_p_reaction))
+
         # Next we encode the MAX concentration values: 
         # we collect those from the intermediate product variables