working on the new encoding

logics/__init__.py

@@ -1,3 +1,3 @@
 from logics.rsltl import Formula_rsLTL
-from logics.rsltl import BagDescription
+from logics.bags import BagDescription
-from logics.rsltl import Encoder_rsLTL
+from logics.rsltl_encoder import rsLTL_Encoder

logics/bags.py

@@ -0,0 +1,72 @@
+from enum import Enum
+BagDesc_oper = Enum('BagDesc_oper', 'entity true l_and l_or l_not lt le eq ge gt')
+
+class BagDescription(object):
+    def __init__(self, f_type, L_oper = None, R_oper = None, entity = ""):
+        self.f_type = f_type
+        self.left_operand = L_oper
+        self.right_operand = R_oper
+        self.entity = entity
+        
+    def __repr__(self):
+        if self.f_type == BagDesc_oper.entity:
+            return self.entity
+        if self.f_type == BagDesc_oper.true:
+            return "TRUE"
+        if self.f_type == BagDesc_oper.l_and:
+            return "( " + repr(self.left_operand) + " & " + repr(self.right_operand) + " )"
+        if self.f_type == BagDesc_oper.l_or:
+            return "( " + repr(self.left_operand) + " | " + repr(self.right_operand) + " )"
+        if self.f_type == BagDesc_oper.l_not:
+            return "~" + repr(self.left_operand)
+        if self.f_type == BagDesc_oper.lt:
+            return repr(self.left_operand) + " < " + repr(self.right_operand)
+        if self.f_type == BagDesc_oper.le:
+            return repr(self.left_operand) + " <= " + repr(self.right_operand)
+        if self.f_type == BagDesc_oper.eq:
+            return repr(self.left_operand) + " == " + repr(self.right_operand)
+        if self.f_type == BagDesc_oper.ge:
+            return repr(self.left_operand) + " >= " + repr(self.right_operand)
+        if self.f_type == BagDesc_oper.gt:
+            return repr(self.left_operand) + " > " + repr(self.right_operand)
+            
+    def sanity_check(self):
+        """Checks if the right operands for the relations are integers"""
+        
+        # TODO
+        
+        pass
+
+    @classmethod
+    def f_entity(cls, entity_name):
+        return cls(BagDesc_oper.entity, entity = entity_name)
+        
+    @classmethod
+    def f_TRUE(cls):
+        return cls(BagDesc_oper.true)
+        
+    def __lt__(self, other):
+        return BagDescription(BagDesc_oper.lt, L_oper = self, R_oper = other)
+        
+    def __le__(self, other):
+        return BagDescription(BagDesc_oper.le, L_oper = self, R_oper = other)
+        
+    def __eq__(self, other):
+        return BagDescription(BagDesc_oper.eq, L_oper = self, R_oper = other)
+    
+    def __ge__(self, other):
+        return BagDescription(BagDesc_oper.ge, L_oper = self, R_oper = other)
+    
+    def __gt__(self, other):
+        return BagDescription(BagDesc_oper.gt, L_oper = self, R_oper = other)
+        
+    def __and__(self, other):
+        return BagDescription(BagDesc_oper.l_and, L_oper = self, R_oper = other)
+    
+    def __or__(self, other):
+        return BagDescription(BagDesc_oper.l_or, L_oper = self, R_oper = other)
+    
+    def __invert__(self):
+        return BagDescription(BagDesc_oper.l_not, L_oper = self)
+        
+# EOF

logics/rsltl.py

@@ -1,76 +1,10 @@
 from z3 import *
 from enum import Enum
 
+from logics.bags import *
+
 rsLTL_form_type = Enum('rsLTL_form_type', 'bag l_and l_or l_not t_globally t_finally t_next t_until t_release')
-BagDesc_oper = Enum('BagDesc_oper', 'entity true l_and l_or l_not lt le eq ge gt')
 
-class BagDescription(object):
-    def __init__(self, f_type, L_oper = None, R_oper = None, entity = ""):
-        self.f_type = f_type
-        self.left_operand = L_oper
-        self.right_operand = R_oper
-        self.entity = entity
-        
-    def __repr__(self):
-        if self.f_type == BagDesc_oper.entity:
-            return self.entity
-        if self.f_type == BagDesc_oper.true:
-            return "TRUE"
-        if self.f_type == BagDesc_oper.l_and:
-            return "( " + repr(self.left_operand) + " & " + repr(self.right_operand) + " )"
-        if self.f_type == BagDesc_oper.l_or:
-            return "( " + repr(self.left_operand) + " | " + repr(self.right_operand) + " )"
-        if self.f_type == BagDesc_oper.l_not:
-            return "~" + repr(self.left_operand)
-        if self.f_type == BagDesc_oper.lt:
-            return repr(self.left_operand) + " < " + repr(self.right_operand)
-        if self.f_type == BagDesc_oper.le:
-            return repr(self.left_operand) + " <= " + repr(self.right_operand)
-        if self.f_type == BagDesc_oper.eq:
-            return repr(self.left_operand) + " == " + repr(self.right_operand)
-        if self.f_type == BagDesc_oper.ge:
-            return repr(self.left_operand) + " >= " + repr(self.right_operand)
-        if self.f_type == BagDesc_oper.gt:
-            return repr(self.left_operand) + " > " + repr(self.right_operand)
-            
-    def sanity_check(self):
-        """Checks if the right operands for the relations are integers"""
-        
-        # TODO
-        
-        pass
-
-    @classmethod
-    def f_entity(cls, entity_name):
-        return cls(BagDesc_oper.entity, entity = entity_name)
-        
-    @classmethod
-    def f_TRUE(cls):
-        return cls(BagDesc_oper.true)
-        
-    def __lt__(self, other):
-        return BagDescription(BagDesc_oper.lt, L_oper = self, R_oper = other)
-        
-    def __le__(self, other):
-        return BagDescription(BagDesc_oper.le, L_oper = self, R_oper = other)
-        
-    def __eq__(self, other):
-        return BagDescription(BagDesc_oper.eq, L_oper = self, R_oper = other)
-    
-    def __ge__(self, other):
-        return BagDescription(BagDesc_oper.ge, L_oper = self, R_oper = other)
-    
-    def __gt__(self, other):
-        return BagDescription(BagDesc_oper.gt, L_oper = self, R_oper = other)
-        
-    def __and__(self, other):
-        return BagDescription(BagDesc_oper.l_and, L_oper = self, R_oper = other)
-    
-    def __or__(self, other):
-        return BagDescription(BagDesc_oper.l_or, L_oper = self, R_oper = other)
-    
-    def __invert__(self):
-        return BagDescription(BagDesc_oper.l_not, L_oper = self)
 
 class Formula_rsLTL(object):
     
@@ -144,148 +78,4 @@ class Formula_rsLTL(object):
         return Formula_rsLTL(rsLTL_form_type.l_not, L_oper = self)
 
 
-class Encoder_rsLTL(object):
+# EOF
-    """Class for encoding rsLTL formulae for a given smt_checker instance"""
-        
-    def __init__(self, smt_checker):
-        self.smt_checker = smt_checker
-        self.v = smt_checker.v
-        self.v_ctx = smt_checker.v_ctx
-        self.rs = smt_checker.rs
-        
-    def encode_bag(self, bag_formula, level, context=False):
-                
-        if bag_formula.f_type == BagDesc_oper.entity:
-            entity_id = self.rs.get_entity_id(bag_formula.entity)
-            if context:
-                return self.v_ctx[level][entity_id]
-            else:
-                return self.v[level][entity_id]
-            
-        if bag_formula.f_type == BagDesc_oper.true:
-            return True
-            
-        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))
-            
-        if bag_formula.f_type == BagDesc_oper.l_or:
-            return Or(self.encode_bag(bag_formula.left_operand, level, context), 
-                self.encode_bag(bag_formula.right_operand, level, context))
-            
-        if bag_formula.f_type == BagDesc_oper.l_not:
-            return Not(self.encode_bag(bag_formula.left_operand, level, context))
-            
-        if bag_formula.f_type == BagDesc_oper.lt:
-            return self.encode_bag(bag_formula.left_operand, level, context) < int(bag_formula.right_operand)
-            
-        if bag_formula.f_type == BagDesc_oper.le:
-            return self.encode_bag(bag_formula.left_operand, level, context) <= int(bag_formula.right_operand)
-            
-        if bag_formula.f_type == BagDesc_oper.eq:
-            return self.encode_bag(bag_formula.left_operand, level, context) == int(bag_formula.right_operand)
-            
-        if bag_formula.f_type == BagDesc_oper.ge:
-            return self.encode_bag(bag_formula.left_operand, level, context) >= int(bag_formula.right_operand)
-            
-        if bag_formula.f_type == BagDesc_oper.gt:
-            return self.encode_bag(bag_formula.left_operand, level, context) > int(bag_formula.right_operand)
-    
-    def encode_bag_state(self, bag_formula, level):
-        return self.encode_bag(bag_formula, level)
-        
-    def encode_bag_ctx(self, bag_formula, level):
-        return self.encode_bag(bag_formula, level, context=True)
-      
-    def encode(self, formula, level, bound, loop_level=None):
-        
-        if loop_level != None and level == bound:
-            next_level = loop_level
-        else:
-            next_level = level + 1
-                    
-        if not isinstance(formula, Formula_rsLTL):
-            raise NotImplementedError("Unsupported formula type: " + str(type(formula)))
-        
-        if level > bound:
-            return False
-    
-        if formula.f_type == rsLTL_form_type.bag:
-            return self.encode_bag_state(formula.bag_descr, level)
-
-        elif formula.f_type == rsLTL_form_type.l_not:
-            subform = formula.left_operand
-            if subform.is_bag:
-                return Not(self.encode_bag_state(subform, level))
-            else:
-                raise RuntimeError("Negation can be applied to bags only")
-        
-        elif formula.f_type == rsLTL_form_type.l_and:
-            return And(
-                    self.encode(formula.left_operand, level, bound, loop_level), 
-                    self.encode(formula.right_operand, level, bound, loop_level)
-                )
-
-        elif formula.f_type == rsLTL_form_type.l_or:
-            return Or(
-                    self.encode(formula.left_operand, level, bound, loop_level), 
-                    self.encode(formula.right_operand, level, bound, loop_level)
-                )
-
-        elif formula.f_type == rsLTL_form_type.t_next:
-            enc = And(
-                    self.encode(formula.left_operand, next_level, bound, loop_level), 
-                    self.encode_bag_ctx(formula.sub_operand, level)
-                )
-            return enc 
-
-        elif formula.f_type == rsLTL_form_type.t_globally:
-            enc = And(
-                    self.encode(formula.left_operand, level, bound, loop_level),
-                    self.encode_bag_ctx(formula.sub_operand, level),
-                    self.encode(formula, next_level, bound, loop_level)
-                )
-            # enc = True
-            # for i in range(level, bound+1):
-                
-            return enc
-            
-        elif formula.f_type == rsLTL_form_type.t_finally:
-            enc = Or(
-                    self.encode(formula.left_operand, level, bound, loop_level),
-                    And(
-                        self.encode(formula, next_level, bound, loop_level), 
-                        self.encode_bag_ctx(formula.sub_operand, level)
-                    )
-                )
-            return enc
-
-        elif formula.f_type == rsLTL_form_type.t_until:
-            enc = Or(
-                    self.encode(formula.right_operand, level, bound, loop_level), 
-                    And(
-                        self.encode(formula.left_operand, level, bound, loop_level),
-                        self.encode(formula, next_level, bound, loop_level),
-                        self.encode_bag_ctx(formula.sub_operand, level)
-                    )
-                )
-            return enc
-            
-        elif formula.f_type == rsLTL_form_type.t_release:
-            enc = And(
-                    self.encode(formula.right_operand, level, bound, loop_level), 
-                    Or(
-                        self.encode(formula.left_operand, level, bound, loop_level),
-                        And(
-                            self.encode(formula, next_level, bound, loop_level),
-                            self.encode_bag_ctx(formula.sub_operand, level)
-                        )
-                    )
-                )
-            return enc
-        
-        else:
-            raise NotImplementedError("Unsupported operator")
-
-    def encode_loop(self, formula, level, bound):
-        pass

logics/rsltl_encoder.py

@@ -0,0 +1,243 @@
+from logics.rsltl import *
+
+class rsLTL_Encoder(object):
+    """Class for encoding rsLTL formulae for a given smt_checker instance"""
+        
+    def __init__(self, smt_checker):
+        self.smt_checker = smt_checker
+        self.v = smt_checker.v
+        self.v_ctx = smt_checker.v_ctx
+        self.rs = smt_checker.rs
+        self.loop_position = smt_checker.loop_position
+        
+    def encode_bag(self, bag_formula, level, context=False):
+                
+        if bag_formula.f_type == BagDesc_oper.entity:
+            entity_id = self.rs.get_entity_id(bag_formula.entity)
+            if context:
+                return self.v_ctx[level][entity_id]
+            else:
+                return self.v[level][entity_id]
+            
+        if bag_formula.f_type == BagDesc_oper.true:
+            return True
+            
+        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))
+            
+        if bag_formula.f_type == BagDesc_oper.l_or:
+            return Or(self.encode_bag(bag_formula.left_operand, level, context), 
+                self.encode_bag(bag_formula.right_operand, level, context))
+            
+        if bag_formula.f_type == BagDesc_oper.l_not:
+            return Not(self.encode_bag(bag_formula.left_operand, level, context))
+            
+        if bag_formula.f_type == BagDesc_oper.lt:
+            return self.encode_bag(bag_formula.left_operand, level, context) < int(bag_formula.right_operand)
+            
+        if bag_formula.f_type == BagDesc_oper.le:
+            return self.encode_bag(bag_formula.left_operand, level, context) <= int(bag_formula.right_operand)
+            
+        if bag_formula.f_type == BagDesc_oper.eq:
+            return self.encode_bag(bag_formula.left_operand, level, context) == int(bag_formula.right_operand)
+            
+        if bag_formula.f_type == BagDesc_oper.ge:
+            return self.encode_bag(bag_formula.left_operand, level, context) >= int(bag_formula.right_operand)
+            
+        if bag_formula.f_type == BagDesc_oper.gt:
+            return self.encode_bag(bag_formula.left_operand, level, context) > int(bag_formula.right_operand)
+    
+    def encode_bag_state(self, bag_formula, level):
+        return self.encode_bag(bag_formula, level)
+        
+    def encode_bag_ctx(self, bag_formula, level):
+        return self.encode_bag(bag_formula, level, context=True)
+      
+    def encode(self, formula, level, bound):
+        
+        if not isinstance(formula, Formula_rsLTL):
+            raise NotImplementedError("Unsupported formula type: " + str(type(formula)))
+        
+        if level > bound:
+            raise RuntimeError("level > bound. Unexpected behaviour. The encoding does not support levels higher than a bound.")
+    
+        if formula.f_type == rsLTL_form_type.bag:
+            return self.encode_bag_state(formula.bag_descr, level)
+
+        elif formula.f_type == rsLTL_form_type.l_not:
+            subform = formula.left_operand
+            if subform.is_bag:
+                return Not(self.encode_bag_state(subform, level))
+            else:
+                raise RuntimeError("Negation can be applied to bags only")
+        
+        elif formula.f_type == rsLTL_form_type.l_and:
+            return And(
+                    self.encode(formula.left_operand, level, bound), 
+                    self.encode(formula.right_operand, level, bound)
+                )
+
+        elif formula.f_type == rsLTL_form_type.l_or:
+            return Or(
+                    self.encode(formula.left_operand, level, bound), 
+                    self.encode(formula.right_operand, level, bound)
+                )
+
+        elif formula.f_type == rsLTL_form_type.t_next:
+            if level < bound:
+                enc = And(
+                        self.encode(formula.left_operand, level + 1, bound), 
+                        self.encode_bag_ctx(formula.sub_operand, level)
+                    )
+            else: 
+                # level == bound
+                enc = False
+                for loop_level in range(1, bound):
+                    enc = Or(enc, And(self.loop_position == loop_level, 
+                        self.encode(formula.left_operand, loop_level, bound)))
+                enc = And(enc, self.encode_bag_ctx(formula.sub_operand, level))
+                enc = simplify(enc)
+                
+            return enc 
+
+        elif formula.f_type == rsLTL_form_type.t_globally:
+            if level < bound:
+                enc = And(
+                        self.encode(formula.left_operand, level, bound),
+                        self.encode_bag_ctx(formula.sub_operand, level),
+                        self.encode(formula, level + 1, bound)
+                    )
+            else:
+                # level == bound
+                enc = False
+                for loop_level in range(1, bound):
+                    enc = Or(enc, And(self.loop_position == loop_level),
+                        self.encode_approx(formula, loop_level, bound),
+                        )
+                enc = And(enc, self.encode_bag_ctx(formula.sub_operand, level))
+                enc = simplify(enc)   
+
+            return enc
+
+        elif formula.f_type == rsLTL_form_type.t_finally:
+            if level < bound:
+                enc = Or(
+                        self.encode(formula.left_operand, level, bound),
+                        And(
+                            self.encode_bag_ctx(formula.sub_operand, level),
+                            self.encode(formula, level + 1, bound)
+                        )
+                    )
+            else:
+                # level == bound
+                enc = False
+                for loop_level in range(1, bound):
+                    enc = Or(enc, 
+                            And(
+                                self.loop_position == loop_level),
+                                self.encode_approx(formula, loop_level, bound),
+                        )
+                enc = And(enc, self.encode_bag_ctx(formula.sub_operand, level))
+                enc = simplify(enc)
+
+            return enc
+
+        elif formula.f_type == rsLTL_form_type.t_until:
+            if level < bound:
+                inner_enc = self.encode(formula, level + 1, bound)
+            else: 
+                # level == bound
+                inner_enc = False
+                for loop_level in range(1, bound):
+                    inner_enc = Or(inner_enc, 
+                            And(
+                                self.loop_position == loop_level, 
+                                self.encode_approx(formula, loop_level, bound)
+                            )
+                        )
+
+            enc = Or(
+                    self.encode(formula.right_operand, level, bound), 
+                    And(
+                        self.encode(formula.left_operand, level, bound),
+                        inner_enc,
+                        self.encode_bag_ctx(formula.sub_operand, level)
+                    )
+                )
+                                
+            return enc
+            
+        elif formula.f_type == rsLTL_form_type.t_release:
+            if level < bound:
+                inner_enc = self.encode(formula, level + 1, bound)
+            else: 
+                # level == bound
+                inner_enc = False
+                for loop_level in range(1, bound):
+                    inner_enc = Or(inner_enc, 
+                            And(
+                                self.loop_position == loop_level, 
+                                self.encode_approx(formula, loop_level, bound)
+                            )
+                        )
+                
+            enc = And(
+                    self.encode(formula.right_operand, level, bound), 
+                    Or(
+                        self.encode(formula.left_operand, level, bound),
+                        And(
+                            inner_enc,
+                            self.encode_bag_ctx(formula.sub_operand, level)
+                        )
+                    )
+                )
+
+                
+            return enc
+        
+        else:
+            raise NotImplementedError("Unsupported operator")
+
+    def encode_approx(self, formula, level, bound):
+        """Provides the approximation-encoding
+        
+        Used by encode()
+        """
+        if formula.f_type == rsLTL_form_type.t_until:
+            if level < bound:
+                enc = Or(
+                        self.encode(formula.right_operand, level, bound), 
+                        And(
+                            self.encode(formula.left_operand, level, bound),
+                            self.encode_approx(formula, level + 1, bound),
+                            self.encode_bag_ctx(formula.sub_operand, level)
+                        )
+                    )
+            else: 
+                # level == bound
+                enc = self.encode(formula.right_operand, bound, bound)
+        
+            return enc
+    
+        elif formula.f_type == rsLTL_form_type.t_release:
+            if level < bound:
+                enc = And(
+                        self.encode(formula.right_operand, level, bound), 
+                        Or(
+                            self.encode(formula.left_operand, level, bound),
+                            And(
+                                self.encode_approx(formula, level + 1, bound),
+                                self.encode_bag_ctx(formula.sub_operand, level)
+                            )
+                        )
+                    )
+            else: 
+                # level == bound
+                enc = self.encode(formula.right_operand, bound, bound)
+        
+            return enc
+
+        else:
+            raise NotImplementedError("Unsupported operator in approximation encoding")
+

rs_testing.py

@@ -31,11 +31,12 @@ def test_rsLTL():
     
     rc = ReactionSystemWithAutomaton(r,c)
     checker = SmtCheckerRSC(rc)
-    checker.dummy_unroll(10)
-    #e = Encoder_rsLTL(checker)
     
-    print(checker.get_loop_encodings())
+    checker.check_rsltl(formula=x)
     
+    # checker.dummy_unroll(10)
+    # e = rsLTL_Encoder(checker)
+    # print(checker.get_loop_encodings())
     # print(e.encode(x, 0, 10))
 
 def test_extended_automaton():

smt/smt_checker_rsc.py

@@ -9,7 +9,7 @@ from itertools import chain
 import resource
 from colour import *
 
-import logics
+from logics import rsLTL_Encoder
 
 # def simplify(x):
 #     return x
@@ -367,50 +367,9 @@ class SmtCheckerRSC(object):
                         print(" " + self.rs.get_entity_name(var_id) + "=" + var_rep, end="")
                 print(" }")
                 
-    def check_rsltl(self, formula, print_witness=True):
+    def check_rsltl(self, formula, print_witness=True, print_time=True, print_mem=True, max_level=None):
         """Bounded Model Checking for rsLTL properties"""
         
-    def dummy_unroll(self, levels):
-        """Unrolls the variables for testing purposes"""
-
-        self.current_level = 0     
-        for i in range(levels+1):
-            self.prepare_all_variables()
-            self.current_level += 1
-
-        print(C_MARK_INFO + " Dummy Unrolling done.")
-    
-    def state_equality(self, level_A, level_B):
-        """Encodes equality of two states at two different levels"""
-        
-        eq_enc = True
-        
-        print(level_A, level_B, self.current_level)
-        print(len(self.v), self.v)
-        
-        for e_i in range(len(self.rs.background_set)):
-            e_i_equality = self.v[level_A][e_i] == self.v[level_B][e_i]
-            eq_enc = simplify(And(eq_enc, e_i_equality))
-            
-        return eq_enc
-    
-    def get_loop_encodings(self):
-        
-        k = self.current_level-1 # TODO: cos jest pokichane z tymi indeksami. sprawdzic. zasypiam.
-        loop_var = self.loop_position
-        
-        loop_k = True
-        for i in range(1,k+1):
-            loop_k = simplify(And(loop_k, Implies( loop_var == i, self.state_equality(i-1, k) )))
-        
-        loop_enc = loop_k
-        
-        return loop_enc
-        
-    def check_reachability(self, state, print_witness=True, 
-            print_time=True, print_mem=True, max_level=1000):
-        """Main testing function"""
-
         if print_time:
             # start = time()
             start = resource.getrusage(resource.RUSAGE_SELF).ru_utime
@@ -423,6 +382,8 @@ class SmtCheckerRSC(object):
     
         self.solver.add(self.enc_concentration_levels_assertion(0))
     
+        encoder = rsLTL_Encoder(self)
+    
         while True:
             self.prepare_all_variables()
             self.solver.add(self.enc_concentration_levels_assertion(current_level+1))
@@ -434,7 +395,7 @@ class SmtCheckerRSC(object):
             print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...")       
             self.solver.push()
 
-            self.solver.add(self.enc_state_with_blocking(current_level,state))
+            self.solver.add(encoder.encode(formula, 0, current_level))
             
             result = self.solver.check()
             if result == sat:
@@ -452,7 +413,105 @@ class SmtCheckerRSC(object):
             print("{:->70}".format("[ level=" + str(current_level) + " done ]"))
             current_level += 1
 
-            if current_level > max_level:
+            if not max_level is None and current_level > max_level:
+                print("Stopping at level=" + str(max_level))
+                break
+
+        if print_time:
+            # stop = time()
+            stop = resource.getrusage(resource.RUSAGE_SELF).ru_utime
+            self.verification_time = stop-start
+            print()
+            print("\n[i] {: >60}".format(" Time: " + repr(self.verification_time) + " s"))
+        
+        if print_mem:
+            print("[i] {: >60}".format(" Memory: " + repr(resource.getrusage(resource.RUSAGE_SELF).ru_maxrss/(1024*1024)) + " MB"))
+        
+    def dummy_unroll(self, levels):
+        """Unrolls the variables for testing purposes"""
+
+        self.current_level = -1     
+        for i in range(levels+1):
+            self.prepare_all_variables()
+            self.current_level += 1
+
+        print(C_MARK_INFO + " Dummy Unrolling done.")
+    
+    def state_equality(self, level_A, level_B):
+        """Encodes equality of two states at two different levels"""
+        
+        eq_enc = True
+        
+        for e_i in range(len(self.rs.background_set)):
+            e_i_equality = self.v[level_A][e_i] == self.v[level_B][e_i]
+            eq_enc = simplify(And(eq_enc, e_i_equality))
+
+        return eq_enc
+    
+    def get_loop_encodings(self):
+        
+        k = self.current_level
+        loop_var = self.loop_position
+        
+        loop_enc = True
+        
+        """
+        (loop_var == i) means that there is a loop taking back to the state (i-1)
+        
+        Therefore, the encoding starts at 1, not at 0.
+        """
+        
+        for i in range(1,k+1):
+            loop_enc = simplify(And(loop_enc, Implies( loop_var == i, self.state_equality(i-1, k) )))
+        
+        return loop_enc
+        
+    def check_reachability(self, state, print_witness=True, 
+            print_time=True, print_mem=True, max_level=1000):
+        """Main testing function"""
+
+        if print_time:
+            # start = time()
+            start = resource.getrusage(resource.RUSAGE_SELF).ru_utime
+
+        self.prepare_all_variables()
+        self.solver.add(self.enc_init_state(0))
+        self.current_level = 0
+
+        self.prepare_all_variables()
+        
+        self.solver.add(self.enc_concentration_levels_assertion(0))
+        
+        while True:
+            self.prepare_all_variables()
+            self.solver.add(self.enc_concentration_levels_assertion(self.current_level+1))
+            
+            print("\n{:-^70}".format("[ Working at level=" + str(self.current_level) + " ]"))
+            stdout.flush()
+
+            # reachability test:
+            print("[" + colour_str(C_BOLD, "i") + "] Adding the reachability test...")       
+            self.solver.push()
+
+            self.solver.add(self.enc_state_with_blocking(self.current_level,state))
+                
+            result = self.solver.check()
+            if result == sat:
+                print("[" + colour_str(C_BOLD, "+") + "] " + colour_str(C_GREEN, "SAT at level=" + str(self.current_level)))
+                if print_witness:
+                    print("\n{:=^70}".format("[ WITNESS ]"))
+                    self.decode_witness(self.current_level)
+                break
+            else:
+                self.solver.pop()
+
+            print("[" + colour_str(C_BOLD, "i") + "] Unrolling the transition relation")
+            self.solver.add(self.enc_transition_relation(self.current_level))
+
+            print("{:->70}".format("[ level=" + str(self.current_level) + " done ]"))
+            self.current_level += 1
+
+            if self.current_level > max_level:
                 print("Stopping at level=" + str(max_level))
                 break