Commit b7a9379c authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] CLUnfolder: fix typos

parent aba61e84
......@@ -959,11 +959,11 @@ class CLUnfolder(object):
# System has not been shifted for this step until now
LOGGER.info(
"shift_dynamic:: SHIFT; "
"Set dynamic constraints; step: %s; dyn consts len: %s",
self.__current_step,
len(self.__dynamic_constraints)
)
"shift_dynamic:: SHIFT; "
"Set dynamic constraints; step: %s; constraints nb: %s",
self.__current_step,
len(self.__dynamic_constraints)
)
# Old API
# self.__dynamic_constraints.append(
......@@ -1065,7 +1065,7 @@ class CLUnfolder(object):
elif self.__shift_direction == "BACKWARD":
raise MCLException("Shift direction 'BACKWARD' is not yet implemented")
else:
raise MCLException("Shift incoherent data: " + self.__shift_direction)
raise MCLException("Shift unsupported direction: " + self.__shift_direction)
def shift(self):
......@@ -1103,11 +1103,13 @@ class CLUnfolder(object):
self.__shift_initial()
else:
# Shift direction must be set
raise MCLException("Shift incoherent data: " + self.__shift_direction)
raise MCLException("Shift unsupported direction: " + self.__shift_direction)
# Increment the current step
self.__current_step += 1
LOGGER.info("shift:: done; new current_step: %s", self.__current_step)
## Coding of properties ####################################################
def __compile_property(self, property_text):
"""Compile a property (logical formula) into clauses
......@@ -1220,7 +1222,7 @@ class CLUnfolder(object):
in self.__compile_property(self.__initial_property)]
if self.__dimacs_initial:
# Add DIMACS aux clauses initial properties
# Add DIMACS clauses
self.__initial_constraints += self.__dimacs_initial
def __init_final_constraint_0(self):
......@@ -1249,7 +1251,7 @@ class CLUnfolder(object):
in self.__compile_property(self.__final_property)]
if self.__dimacs_final:
# Add DIMACS aux clauses initial properties
# Add DIMACS clauses
self.__final_constraints += self.__dimacs_final
def __init_invariant_constraint_0(self):
......@@ -1292,7 +1294,7 @@ class CLUnfolder(object):
)
if self.__dimacs_invariant:
# Add DIMACS aux clauses initial properties
# Add DIMACS clauses
if self.__invariant_constraints:
# Merge initial state
self.__invariant_constraints[0].append(self.__dimacs_invariant[0])
......@@ -1337,7 +1339,7 @@ class CLUnfolder(object):
)
if self.__dimacs_variant:
# Add DIMACS aux clauses initial properties
# Add DIMACS clauses
# Check if the number of steps is equal
if len(self.__variant_property) != len(self.__dimacs_variant):
raise MCLException(
......@@ -1368,7 +1370,7 @@ class CLUnfolder(object):
# Other steps are taken during shift() calls
self.__variant_constraints = self.__precomputed_variant_constraints[0]
elif self.__shift_direction == "BACKWARD":
raise MCLException("shift 'BACKWARD' is not yet implemented")
raise MCLException("Shift direction 'BACKWARD' is not yet implemented")
else:
raise MCLException("Shift incoherent data: " + self.__shift_direction)
......@@ -1654,8 +1656,12 @@ class CLUnfolder(object):
# Auto shift loop: Shift without checking (optimization)
# Do not search solutions before the specified limit
LOGGER.info(
"Satis test:: OPTI AUTO SHIFT from current_step: %s "
"to __steps_before_check: %s; max_step: %s",
self.__current_step, self.__steps_before_check, max_step
)
while self.__current_step < self.__steps_before_check:
LOGGER.info("Satis test:: OPTI AUTO SHIFT")
self.shift()
satisfiability_test = False
......@@ -1727,9 +1733,12 @@ class CLUnfolder(object):
# Auto shift loop: Shift without checking (optimization)
# Do not search solutions before the specified limit
print("squery_solve: begining; current_step:", self.__current_step, "max_step:", max_step)
LOGGER.info(
"Solve:: OPTI AUTO SHIFT from current_step: %s "
"to __steps_before_check: %s; max_step: %s",
self.__current_step, self.__steps_before_check, max_step
)
while self.__current_step < self.__steps_before_check:
LOGGER.info("Solve: OPTI AUTO SHIFT")
self.shift()
# Search for solutions for each remaining step
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment