Parameter constraints

logics/__init__.py

@@ -2,3 +2,4 @@ from logics.rsltl import Formula_rsLTL
 from logics.bags import BagDescription
 from logics.param_constr import ParamConstraint
 from logics.rsltl_encoder import rsLTL_Encoder
+from logics.param_constr_encoder import ParamConstr_Encoder

logics/param_constr.py

@@ -49,7 +49,7 @@ class ParamConstraint(object):
 
     @classmethod
     def f_param_ent(cls, param, entity_name):
-        return cls(ParamConstraint_oper.entity, param=param, entity=entity_name)
+        return cls(ParamConstraint_oper.param_entity, param=param, entity=entity_name)
 
     @classmethod
     def f_TRUE(cls):

logics/param_constr_encoder.py

@@ -0,0 +1,59 @@
+from logics.param_constr import *
+from z3 import And, Not, Or
+
+class ParamConstr_Encoder(object):
+    """Class for encoding parameter constraints"""
+        
+    def __init__(self, smt_checker):
+        self.smt_checker = smt_checker
+        self.rs = smt_checker.rs
+
+        # self.v = None
+        # self.v_ctx = None
+        # self.loop_position = None
+        
+    def load_variables(self, var_rs, var_ctx, var_loop_pos):
+        
+        self.v = var_rs
+        self.v_ctx = var_ctx
+        self.loop_position = var_loop_pos
+        
+    def encode(self, param_constr):
+        
+        if not param_constr:
+            raise RuntimeError("param_constr is None")
+
+        if param_constr.f_type == ParamConstraint_oper.param_entity:
+            return self.smt_checker.get_enc_param(param_constr.param.name, param_constr.entity)
+            
+        if param_constr.f_type == ParamConstraint_oper.true:
+            return True
+            
+        if param_constr.f_type == ParamConstraint_oper.l_and:
+            return And(self.encode(param_constr.left_operand), 
+                self.encode(param_constr.right_operand))
+            
+        if param_constr.f_type == ParamConstraint_oper.l_or:
+            return Or(self.encode(param_constr.left_operand), 
+                self.encode(param_constr.right_operand))
+            
+        if param_constr.f_type == ParamConstraint_oper.l_not:
+            return Not(self.encode(param_constr.left_operand))
+            
+        if param_constr.f_type == ParamConstraint_oper.lt:
+            return self.encode(param_constr.left_operand) < int(param_constr.right_operand)
+            
+        if param_constr.f_type == ParamConstraint_oper.le:
+            return self.encode(param_constr.left_operand) <= int(param_constr.right_operand)
+            
+        if param_constr.f_type == ParamConstraint_oper.eq:
+            return self.encode(param_constr.left_operand) == int(param_constr.right_operand)
+            
+        if param_constr.f_type == ParamConstraint_oper.ge:
+            return self.encode(param_constr.left_operand) >= int(param_constr.right_operand)
+            
+        if param_constr.f_type == ParamConstraint_oper.gt:
+            return self.encode(param_constr.left_operand) > int(param_constr.right_operand)
+            
+        assert False, "Unsupported case {:s}".format(param_constr.f_type)
+    

logics/rsltl_encoder.py

@@ -1,7 +1,7 @@
 from logics.rsltl import *
 
 def simplify(x):
-    return x
+   return x
 
 class rsLTL_Encoder(object):
     """Class for encoding rsLTL formulae for a given smt_checker instance"""

rs/reaction_system.py

@@ -23,6 +23,10 @@ class ReactionSystem(object):
     def set_of_bgset_ids(self):
         return set(range(self.background_set_size))
 
+    @property
+    def ordered_list_of_bgset_ids(self):
+        return list(range(self.background_set_size))
+
     def assume_not_in_bgset(self, name):
         if self.is_in_background_set(name):
             raise RuntimeError("The entity " + name + " is already on the list")

rs_testing.py

@@ -26,13 +26,23 @@ def gene_expression(cmd_args):
     """
     r = ReactionSystemWithConcentrationsParam()
 
+    r.add_bg_set_entity(("x", 1))
+    r.add_bg_set_entity(("xp", 1))
+    r.add_bg_set_entity(("X", 1))    
     r.add_bg_set_entity(("y", 1))
     r.add_bg_set_entity(("yp", 1))
     r.add_bg_set_entity(("Y", 1))
     r.add_bg_set_entity(("h", 1))
+    r.add_bg_set_entity(("Q", 1))
 
     all_entities = set(r.background_set)
 
+    r.add_reaction([("x",1)],[("h",1)],[("x",1)])
+    r.add_reaction([("x",1)],[("h",1)],[("xp",1)])
+    r.add_reaction([("x",1),("xp",1)],[("h",1)],[("X",1)])
+
+    r.add_reaction([("X",1),("Y",1)],[("h",1)],[("Q",1)])
+
     ## y
     # r.add_reaction([("y",1)],[("h",1)],[("y",1)])
     # r.add_reaction([("y",1)],[("Q",1)],[("yp",1)])
@@ -50,10 +60,11 @@ def gene_expression(cmd_args):
     c.add_state("1")
     
     # the experiments starts with adding x and y:
-    c.add_transition("0", [("y", 1)], "1")
+    c.add_transition("0", [("y", 1),("x",1)], "1")
     
     # for all the remaining steps we have empty context sequences
     c.add_transition("1", [], "1")
+    c.add_transition("1", [("h", 1)], "1")
 
     rc = ReactionSystemWithAutomaton(r, c)
     rc.show()
@@ -65,32 +76,42 @@ def gene_expression(cmd_args):
     #     exact_state(["x", "xp"], all_entities),
     #     ltl_X(bag_Not("h"), exact_state("X", all_entities))))
 
-    reach_yp = ltl_F(True, "yp")
+    # reachability
-    reach_Y = ltl_F(True, "Y")
+    reach_y = ltl_F(bag_entity("h") == 0, "y")
-    reach_y = ltl_F(True, "y")
+    reach_yp = ltl_F(bag_entity("h") == 0, "yp")
+    reach_Y = ltl_F(bag_entity("h") == 0, "Y")
+    #
+    phi_r = ltl_And(reach_y, reach_yp, reach_Y)
 
-    f_y1 = ltl_G(bag_entity("h") == 0, ltl_Implies(
+    # rules
+    phi_c1 = ltl_G(bag_entity("h") == 0, ltl_Implies(
         bag_entity("y") > 0,
         ltl_X(True, bag_And(bag_entity("y") > 0, bag_entity("yp") > 0))))
 
-    f_y2 = ltl_G(bag_entity("h") == 0, ltl_Implies(
+    phi_c2 = ltl_G(bag_entity("h") == 0, ltl_Implies(
         bag_And(bag_entity("y") > 0, bag_entity("yp") > 0),
         ltl_F(True, bag_entity("Y") > 0)))
 
     # delayed_Y = ltl_X(True, ltl_And(bag_entity("Y") == 0, ltl_X(True, bag_entity("Y") == 0)))
-    delayed_Y = ltl_X(True, bag_entity("Y") == 0)
 
-    obs_1 = ltl_And(f_y1, reach_y, delayed_Y)
+    # delayed_Y = ltl_X(True, bag_entity("Y") == 0)  
-    obs_2 = ltl_And(f_y2, reach_y, reach_Y, delayed_Y)
+    
+    delayed_Q = ltl_And(bag_entity("Q") == 0, ltl_X(True, ltl_And(bag_entity("Q") == 0, ltl_X(True, ltl_And(bag_entity("Q") == 0, ltl_F(True, bag_entity("Q") > 0))))))
+
+    obs_1 = ltl_And(phi_r, phi_c1, phi_c2, delayed_Q)
+    
+    # obs_2 = ltl_And(f_y2, reach_y, reach_Y, delayed_Y, delayed_Q)
 
     # f_x2 = ltl_G(True, ltl_Implies(
     #     exact_state(["x", "xp"], all_entities),
     #     ltl_X(bag_Not("h"), exact_state("X", all_entities))))
     #
     
+    param_constr = param_And(param_entity(lda3, "Y") > 0, param_entity(lda2, "Q") == 0, param_entity(lda1, "yp") == 0, param_entity(lda1, "Y") == 0)
+        
     smt_rsc = SmtCheckerRSCParam(rc, optimise=cmd_args.optimise)
     #
-    smt_rsc.check_rsltl(formulae_list=[obs_1, obs_2], max_level=4, cont_if_sat=True)
+    smt_rsc.check_rsltl(formulae_list=[obs_1], param_constr=param_constr) #, max_level=4, cont_if_sat=True)
 
     # smt_rsc.check_rsltl(formula=f_x1, print_witness=True)
 

rsltl_shortcuts.py

@@ -61,6 +61,11 @@ def ltl_X(ctx_arg, a0):
     a0 = get_bag_if_str(a0)
     return Formula_rsLTL.f_X(ctx_arg, a0)
 
+def ltl_U(ctx_arg, a0, a1):
+    a0 = get_bag_if_str(a0)
+    a1 = get_bag_if_str(a1)
+    return Formula_rsLTL.f_U(ctx_arg, a0, a1)
+
 def ltl_And(*args):
     assert len(args) > 1
     last = get_bag_if_str(args[0])
@@ -77,3 +82,13 @@ def ltl_Implies(a0, a1):
     a1 = get_bag_if_str(a1)
     return Formula_rsLTL.f_Implies(a0, a1)
 
+def param_entity(param, entity_name):
+    return ParamConstraint.f_param_ent(param, entity_name)
+
+def param_And(*args):
+    assert len(args) > 1
+    last = args[0]
+    for arg in args[1:]:
+        last = ParamConstraint.f_And(last, arg)
+    return last
+

smt/smt_checker_rsc_param.py

@@ -10,6 +10,7 @@ import resource
 from colour import *
 
 from logics import rsLTL_Encoder
+from logics import ParamConstr_Encoder
 
 from rs.reaction_system_with_concentrations_param import ParameterObj, is_param
 
@@ -224,12 +225,19 @@ class SmtCheckerRSCParam(object):
             # we start collecting bg-related vars for the given param
             vars_for_param = []
 
-            for entity in self.rs.set_of_bgset_ids:
+            for entity in self.rs.ordered_list_of_bgset_ids:
                 new_var = Int("Pm{:s}_{:s}".format(param_name, self.rs.get_entity_name(entity)))
                 vars_for_param.append(new_var)
 
             self.v_param[param_name] = vars_for_param
 
+    def get_enc_param(self, param_name, entity_name):
+        """
+        Returns encoded param[entity_name]
+        """
+        entity_id = self.rs.get_entity_id(entity_name)
+        return self.v_param[param_name][entity_id]
+        
     def load_varset_for_path(self, path_idx):
         """
         Loads the the variables for the path with path_idx
@@ -682,7 +690,8 @@ class SmtCheckerRSCParam(object):
             self, formulae_list, 
             print_witness=True, 
             print_time=True, print_mem=True,
-            max_level=None, cont_if_sat=False):
+            max_level=None, cont_if_sat=False,
+            param_constr=None):
         """
         Bounded Model Checking for rsLTL properties
             
@@ -694,11 +703,15 @@ class SmtCheckerRSCParam(object):
             * cont_if_sat     -- if True, then the method
                                  continues up until max_level is
                                  reached (even if sat found)
+            * param_constr    -- constraints on parameters
         """
             
         if not isinstance(formulae_list, (list, tuple)):
             print_error("Expected a list of formulae")
         
+        print_info("Parameter constraint: {:s}".format(str(param_constr)))
+
+
         self.reset()
 
         num_of_paths = len(formulae_list)
@@ -735,6 +748,11 @@ class SmtCheckerRSCParam(object):
 
         encoder = rsLTL_Encoder(self)
         
+        if param_constr:
+            param_contr_encoder = ParamConstr_Encoder(self)
+            enc_param_constr = param_contr_encoder.encode(param_constr)
+            self.solver_add(enc_param_constr)
+
         if self.optimise:
             self.assert_param_optimisation()