diff --git a/logics/__init__.py b/logics/__init__.py index 848d5c1..fcb859c 100644 --- a/logics/__init__.py +++ b/logics/__init__.py @@ -1,3 +1,3 @@ from logics.rsltl import Formula_rsLTL -from logics.rsltl import BagDescription -from logics.rsltl import Encoder_rsLTL \ No newline at end of file +from logics.bags import BagDescription +from logics.rsltl_encoder import rsLTL_Encoder diff --git a/logics/bags.py b/logics/bags.py new file mode 100644 index 0000000..d80135c --- /dev/null +++ b/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 diff --git a/logics/rsltl.py b/logics/rsltl.py index 2de24ec..98960f5 100644 --- a/logics/rsltl.py +++ b/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): - """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 +# EOF \ No newline at end of file diff --git a/logics/rsltl_encoder.py b/logics/rsltl_encoder.py new file mode 100644 index 0000000..b9f6d00 --- /dev/null +++ b/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") + diff --git a/rs_testing.py b/rs_testing.py index e45f556..129a67c 100644 --- a/rs_testing.py +++ b/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(): diff --git a/smt/smt_checker_rsc.py b/smt/smt_checker_rsc.py index 932aba3..1ca4d07 100644 --- a/smt/smt_checker_rsc.py +++ b/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 @@ -420,13 +379,15 @@ class SmtCheckerRSC(object): current_level = 0 self.prepare_all_variables() - + 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)) - + print("\n{:-^70}".format("[ Working at level=" + str(current_level) + " ]")) stdout.flush() @@ -434,8 +395,8 @@ 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: print("[" + colour_str(C_BOLD, "+") + "] " + colour_str(C_GREEN, "SAT at level=" + str(current_level))) @@ -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