diff --git a/command_line/cadbiom_cmd/solution_search.py b/command_line/cadbiom_cmd/solution_search.py index 3773cfa30d1e663ad1089cdc14f50b2954059b89..5b04f20b59286827cf4d3d3fbe8fb25fdf1fd0a1 100644 --- a/command_line/cadbiom_cmd/solution_search.py +++ b/command_line/cadbiom_cmd/solution_search.py @@ -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') diff --git a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py index 47b7dd9bdad4d2737d93488c6d567f32af8f3c64..990c42b219b6fabe0845ec3223aecbe554a657ad 100644 --- a/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py +++ b/library/cadbiom/models/clause_constraints/mcl/CLUnfolder.py @@ -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 """ diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py index 67b8d58e2137ac9011a54703dc40b81a515b100b..a13d856933466dfd9320cdd4dca95d47a7fd1b2e 100644 --- a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py +++ b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py @@ -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) diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLSolutions.py b/library/cadbiom/models/clause_constraints/mcl/MCLSolutions.py index c32cdb160f7a775490b9b004055a31d00429405c..4516e1200bdd611536018829ae2c0838502f4055 100644 --- a/library/cadbiom/models/clause_constraints/mcl/MCLSolutions.py +++ b/library/cadbiom/models/clause_constraints/mcl/MCLSolutions.py @@ -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):