diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
index eac3fb33015c7d96153be33fa2c3a80584009ddc..b82ec0a5c947d7ce60906ddc41118eda4c997845 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
+++ b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
@@ -193,6 +193,9 @@ from cadbiom.models.guard_transitions.chart_model import ChartModel
from cadbiom.models.clause_constraints.mcl.MCLSolutions import FrontierSolution, DimacsFrontierSol
from cadbiom.models.clause_constraints.mcl.MCLQuery import MCLSimpleQuery
+from cadbiom import commons as cm
+LOGGER = cm.logger()
+
class MCLAnalyser(object):
"""Query a UCL dynamical system and analyse solutions
@@ -608,24 +611,62 @@ class MCLAnalyser(object):
return dimacfrontsol
- def __mac_exhaustive_search(self, query, max_step):
- """
- @param query: MCLQuery
- @param max_step: int - Number of steps allowed in the unfolding;
+ def __mac_exhaustive_search(self, query, max_user_step):
+ """Return a generator of FrontierSolution objects.
+
+ This is a function very similar to next_mac(), but it returns
+ many solutions.
+ The satisfiability tests and the banishment of the previous solutions
+ are done internally in an optimal way.
+ There is also a self adjustment of the number of minimum steps during
+ which to find solutions until reaching the maximum number set by the user.
+
+ ---
+
+ On cherche ensuite d'abord des solutions non minimales (actuellement 2) via:
+ self.__sq_dimacs_frontier_solutions(query, nb_step, 2)
+
+ Pour ensuite les élaguer en supprimant les places non essentielles à la
+ satisfiabilité de la propriété via:
+ small_fsol = self.less_activated_solution(lfsol)
+ current_mac = self.__prune_frontier_solution(small_sol, query, nb_step)
+
+ Ce processus itératif est le plus "time-consuming" car nous n'avons pas
+ le controle sur les solutions fournies par SAT et les solutions non minimales
+ sont en général très éloignées de la solution minimale, c.-à -d. contiennent
+ beaucoup plus de places (ces places excédentaires sont dispensables).
+
+ :param query: Current query.
+ :param max_user_step: Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
- @return: <generator <FrontierSolution>>
+ :type query: <MCLSimpleQuery>
+ :type max_user_step: <int>
+ :return: A generator of FrontierSolution objects which are a wrapper of
+ a symbolic representation of frontier values and timings from
+ a raw solution.
+ :rtype: <generator <FrontierSolution>>
"""
# list of timed minimal activation conditions on frontier (dimacs code)
# i.e list<DimacsFrontierSol>
- mac_list = []
+ # mac_list = [] # Not used anymore
forbidden_frontier_values = []
+ ## TODO: parser les properties au format DIMACS une bonne fois pour toutes
+ ## et les ajouter dans forbidden_frontier_values
+ ## Lors du rechargement des places précédentes, le problème du parsing va réapparaitre
+
+ # Satisfiability test
reachable = self.sq_is_satisfiable(query, max_user_step)
- # get the minimum number of steps for reachability
- # set number of shifts before testing final prop
- min_step = self.unfolder.get_current_step() - 1
- query.set_steps_before_reach(min_step)
+ # Get the minimum number of steps for reachability
+ min_step = self.unfolder.get_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
+ # (see squery_is_satisfied() and squery_solve())
+ query.steps_before_check = min_step - 1
+
+ LOGGER.info("Solution reachable in min_step: %s", min_step)
while reachable:
# Forbidden solutions: already discovered macs (see at the end of the while loop)
@@ -633,36 +674,71 @@ class MCLAnalyser(object):
# Equivalent of wrapping each previous solution with a logical OR:
# OR( not (frontier places))
## TODO: check in unfolder: dim_start elements joined by OR or AND operator ?
- print("forbidden_frontier_values", forbidden_frontier_values)
-
- query.dim_start = forbidden_frontier_values
+ ## TODO: keep previous dim_start à la première itération (mettre le contenu dans forbidden values)
+ query.dim_start = list(forbidden_frontier_values)
+ print("query variant prop", query.variant_prop)
## TODO: equivaut à mettre à jour le start_prop ou __initial_property avec l'ancienne méthode ??
## si non, faudrait ptetre éviter de recompiler ça à chaque fois dans __init_initial_constraint_0
#### redondance code next_mac()
# Solutions differ on frontiers: Search only 2 different solutions
# to avoid all activated solutions
# Get <tuple <DimacsFrontierSol>>
- lfsol = self.__sq_dimacs_frontier_solutions(query, max_step, 2)
- if not lfsol:
- break
+ dimacs_front_sol = self.__sq_dimacs_frontier_solutions(query, min_step, 2)
+ if not dimacs_front_sol:
+ # If we do not want to self-adjust steps, just break the loop
+ # break
+
+ print("NOT FOUND - current step ?", self.unfolder.get_current_step())
+ if self.unfolder.get_current_step() + 1 > max_user_step:
+ # Cosmetic break, avoid to do useless test
+ break
+
+ ## TEST
+ ## Make autoadjustment... of max_steps during the solving
+ ## Juste appeler squery_solve avec les memes parametres mais
+ ## min_step augmenté de 1
+ ## en restant inférieur au nb d'étapes demandées à l'origine
+ ## => on bénéficie des shifts précédents et on évite de reconstruire le problème...
+
+ # Hack: reuse the current Unfolder (without init with query)
+ # => do not do this at home!
+ self.unfolder._CLUnfolder__locked = False
+ # Avoid a new test of satisfiability on the same current_step
+ # (we already know that there is no more solution for it)
+ # => increment __steps_before_check
+ self.unfolder._CLUnfolder__steps_before_check += 1
+ ret = self.unfolder.squery_is_satisfied(max_user_step)
+ if not ret:
+ # The problem is definitly not satisfiable in the given
+ # number of steps
+ break
+ # __steps_before_check can't be >= min_step
+ # (see squery_is_satisfied() and squery_solve())
+ min_step = self.unfolder.get_current_step()
+ query.steps_before_check = min_step - 1
+
+ print("testing AUTO CORRECT max step:", min_step)
+ continue
+
# Get the solution with the less number of activated states
- small_fsol = self.less_activated_solution(lfsol)
+ small_fsol = self.less_activated_solution(dimacs_front_sol)
# Prune non essential places for the satisfiability of the property
# => reduce the number of activated variables
- current_mac = self.__prune_frontier_solution(small_fsol, query, max_step)
+ current_mac = self.__prune_frontier_solution(small_fsol, query, min_step)
## TEST
- print("final current step ?", self.unfolder.get_current_step())
+ print("__mac_exhaustive_search:: final current step ?", self.unfolder.get_current_step())
if current_mac.nb_activated_frontiers == 0:
+ # Condition that seems to be never reached..
print("NOT REACHABLE")
reachable = False
else:
yield current_mac
- mac_list.append(current_mac)
+ # mac_list.append(current_mac)
# Keep a list of frontier values to be banned in the next search
# - Get all activated frontiers on the current DimacsFrontierSol
@@ -671,7 +747,6 @@ class MCLAnalyser(object):
[-var for var in current_mac.activated_frontier_values]
)
-
def next_mac(self, query, max_step):
"""Search a Minimal Access Condition for the given query.