From 7a20bdb0f30458953491c148c5d68a1ee539282d Mon Sep 17 00:00:00 2001
From: VIGNET Pierre <pierre.vignet@irisa.fr>
Date: Thu, 12 Dec 2019 19:11:12 +0100
Subject: [PATCH] [cmd][lib] switch get_current_step to a proper property
---
command_line/cadbiom_cmd/solution_search.py | 10 +++++-----
.../models/clause_constraints/mcl/CLUnfolder.py | 3 ++-
.../models/clause_constraints/mcl/MCLAnalyser.py | 8 ++++----
.../models/clause_constraints/mcl/MCLSolutions.py | 2 +-
4 files changed, 12 insertions(+), 11 deletions(-)
diff --git a/command_line/cadbiom_cmd/solution_search.py b/command_line/cadbiom_cmd/solution_search.py
index 3773cfa..5b04f20 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 47b7dd9..990c42b 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 67b8d58..a13d856 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 c32cdb1..4516e12 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):
--
GitLab