reset & initialise methods for SMT Checker; fixed some typos for rsLTL

logics/rsltl.py

@@ -50,7 +50,7 @@ class Formula_rsLTL(object):
 
     @classmethod
     def f_X(cls, sub, arg):
-        return cls(rsLTL_form_type.next, L_oper = arg, sub_oper = sub)
+        return cls(rsLTL_form_type.t_next, L_oper = arg, sub_oper = sub)
 
     @classmethod
     def f_G(cls, sub, arg):

logics/rsltl_encoder.py

@@ -24,7 +24,7 @@ class rsLTL_Encoder(object):
             
         if bag_formula.f_type == BagDesc_oper.l_and:
             return And(self.encode_bag(bag_formula.left_operand, level, context), 
-                self.encode_bag(bag_formula.left_.right_operand, level, context))
+                self.encode_bag(bag_formula.right_operand, level, context))
             
         if bag_formula.f_type == BagDesc_oper.l_or:
             return Or(self.encode_bag(bag_formula.left_operand, level, context), 

rs_testing.py

@@ -71,16 +71,28 @@ def heat_shock_response(print_system=True):
     
     # prop_req = [("hsp:hsf",1),("hse",1),("prot",1)]
     # prop_block = [("temp",stress_temp)]
-    prop_req   = [ ("mfp",1) ]
-    prop_block = [ ]
-    prop       = (prop_req,prop_block)
-    rs_prop    = (state_translate_rsc2rs(prop_req),state_translate_rsc2rs(prop_block))
-    
-    f_reach_mfp = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("mfp") > 0) )
+    # prop_req   = [ ("mfp",1) ]
+    # prop_block = [ ]
+    # prop       = (prop_req,prop_block)
+    # rs_prop    = (state_translate_rsc2rs(prop_req),state_translate_rsc2rs(prop_block))
+    #
+    # f_reach_mfp = Formula_rsLTL.f_F(BagDescription.f_TRUE(), (BagDescription.f_entity("mfp") > 0) )
     
     smt_rsc = SmtCheckerRSC(rc)
+    
+    # (1) if we keep increasing the temperature the protein will eventually misfold
+    # f_mfp_when_heating = Formula_rsLTL.f_X(BagDescription.f_TRUE(),
+    #         Formula_rsLTL.f_F(BagDescription.f_entity("heat") > 0, (BagDescription.f_entity("mfp") > 0) )
+    #     )
+    # smt_rsc.check_rsltl(formula=f_mfp_when_heating)
+    
+    # (2) when heating, we finally exceed the stress_temp
+    f_2 = Formula_rsLTL.f_X(BagDescription.f_TRUE(),
+            Formula_rsLTL.f_F(BagDescription.f_entity("heat") > 0, (BagDescription.f_entity("temp") > stress_temp))
+        )
+    smt_rsc.check_rsltl(formula=f_2)
+    
     # smt_rsc.check_reachability(prop,max_level=40)
-    smt_rsc.check_rsltl(formula=f_reach_mfp)
 
 def state_translate_rsc2rs(p):
     return [e[0] + "#" + str(e[1]) for e in p]    

smt/smt_checker_rsc.py

@@ -26,6 +26,11 @@ class SmtCheckerRSC(object):
         self.rs = rsca.rs
         self.ca = rsca.ca
 
+        self.initialise()
+    
+    def initialise(self):
+        """Initialises all the variables used by the checker"""
+        
         self.v = []
         self.v_ctx = []
         self.ca_state = []
@@ -37,6 +42,11 @@ class SmtCheckerRSC(object):
         
         self.verification_time = None        
 
+    def reset(self):
+        """Reinitialises the state of the checker"""
+        
+        self.initialise()
+        
     def prepare_all_variables(self):
         """Encodes all the variables"""
 
@@ -370,6 +380,8 @@ class SmtCheckerRSC(object):
     def check_rsltl(self, formula, print_witness=True, print_time=True, print_mem=True, max_level=None):
         """Bounded Model Checking for rsLTL properties"""
         
+        self.reset()
+        
         print("[" + colour_str(C_BOLD, "i") + "] Running rsLTL bounded model checking")
         
         if print_time:
@@ -475,6 +487,8 @@ class SmtCheckerRSC(object):
             print_time=True, print_mem=True, max_level=1000):
         """Main testing function"""
 
+        self.reset()
+
         if print_time:
             # start = time()
             start = resource.getrusage(resource.RUSAGE_SELF).ru_utime
@@ -537,6 +551,8 @@ class SmtCheckerRSC(object):
             print_time=False, print_mem=False, max_level=100):
         """Encoding debug function"""
 
+        self.reset()
+
         self.prepare_all_variables()
         init_s = self.enc_init_state(0)
         print(init_s)