Commit 7a20bdb0 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[cmd][lib] switch get_current_step to a proper property

parent 1d2b9ec5
......@@ -357,7 +357,7 @@ def find_macs(mcla,
frontier_sol.save(file, only_macs=True)
# Save min steps
# min_step = mcla.unfolder.get_current_step() - 1 # Magic number !
# min_step = mcla.unfolder.current_step - 1 # Magic number !
# LOGGER.debug("%s:: Save minimal steps: %s", final_prop, min_step)
# with open(mac_step_file, 'a') as file:
# file.write(str(min_step)+'\n')
......@@ -402,7 +402,7 @@ def find_mac(mcla,
# Is the property reacheable ?
reacheable = mcla.sq_is_satisfiable(query, steps)
# If yes, in how many steps ?
min_step = mcla.unfolder.get_current_step()
min_step = mcla.unfolder.current_step
if reacheable and (min_step <= steps):
LOGGER.info("%s:: Property %s is reacheable in %s steps",
......@@ -429,7 +429,7 @@ def find_mac(mcla,
frontier_sol.save(file, only_macs=True)
# Save min steps
min_step = mcla.unfolder.get_current_step() - 1 # Magic number !
min_step = mcla.unfolder.current_step - 1 # Magic number !
# LOGGER.debug("%s:: Save minimal steps: %s", final_prop, min_step)
# with open(mac_step_file, 'a') as file:
# file.write(str(min_step)+'\n')
......@@ -536,7 +536,7 @@ def detect_model_type(mclanalyser, filepath):
#
# reacheable = mcla.sq_is_satisfiable(query, steps) #important step
# print("reacheable:", reacheable)
# min_step = mcla.unfolder.get_current_step()
# min_step = mcla.unfolder.current_step
# print("min_step:", min_step)
# # Set max step authorized
# query.steps_before_check = min_step - 1
......@@ -556,7 +556,7 @@ def detect_model_type(mclanalyser, filepath):
# write_list(next_mac, mac_file)
#
# # SAVE STEP
# min_step = mcla.unfolder.get_current_step()
# min_step = mcla.unfolder.current_step
# print("save min step:", min_step)
# with open(mac_step_file, 'a') as file:
# file.write(str(min_step)+'\n')
......
......@@ -588,7 +588,8 @@ class CLUnfolder(object):
"""
return self.__shift_step
def get_current_step(self):
@property
def current_step(self):
"""
@return: the current number of unfolding
"""
......
......@@ -691,7 +691,7 @@ class MCLAnalyser(object):
reachable = self.sq_is_satisfiable(query, max_user_step)
# Get the minimum number of steps for reachability
min_step = self.unfolder.get_current_step()
min_step = self.unfolder.current_step
# Adjust the number of useless shifts needed before finding a solution
# (i.e. testing final prop).
# __steps_before_check can't be >= max_user_step
......@@ -721,8 +721,8 @@ class MCLAnalyser(object):
# break
LOGGER.info("MCLA: NOT FOUND -> satis test; current step %s",
self.unfolder.get_current_step())
if self.unfolder.get_current_step() + 1 > max_user_step:
self.unfolder.current_step)
if self.unfolder.current_step + 1 > max_user_step:
# Cosmetic break, avoid to do useless test
break
......@@ -747,7 +747,7 @@ class MCLAnalyser(object):
break
# __steps_before_check can't be >= min_step
# (see squery_is_satisfied() and squery_solve())
min_step = self.unfolder.get_current_step()
min_step = self.unfolder.current_step
query.steps_before_check = min_step - 1
print("testing AUTO CORRECT max step:", min_step)
......
......@@ -134,7 +134,7 @@ class RawSolution(object):
self.solution = solution
self.unfolder = unfolder
self.shift_step = unfolder.get_shift_step()
self.current_step = unfolder.get_current_step()
self.current_step = unfolder.current_step
self.shift_direction = unfolder.get_shift_direction()
def get_unshift_code(self, var_num):
......
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