diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py index 15b20759f6b92ff564f620193b5f16341475b53d..07123a62b047385ae555ef1d14a389482b2c0ebe 100644 --- a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py +++ b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py @@ -398,11 +398,20 @@ class MCLAnalyser(object): Repeat the operation until there is only one solution. + :param fsol: A DimacsFrontierSol for which we assume/assert that the + system is satisfiable. :type fsol: <DimacsFrontierSol> :type query: <MCLSimpleQuery> :rtype: <DimacsFrontierSol> - ASSERT: fsol is a frontier condition implying sq satisfiability + .. todo:: + - regarder si les solutions dimacs_solutions sont si différentes. + il est possible que le solveur soit relativement optimisé pour qu'on + puisse en demander moins ou qu'on puisse éliminer les solutions les + moins diversifiées (détection d'un ensemble commun de places dont on + forcerait l'inactivation pas l'intermédiaire d'une clause de l'état + initial). + - ajuster automatiquement nb_sols_to_be_pruned (10 actuellement) """ # for debug - too expansive to be activated anytime # assert(self.sq_is_satisfiable(query, max_step)) @@ -436,9 +445,6 @@ class MCLAnalyser(object): i, len(dimacs_solutions) ) - ####TODO: regarder si ces solutions sont si différentes et ce qu'on en fait au final... - ### en fin de compte il est possible que le solveur ne soit pas si bete... - ##TODO: ajuster automatiquement nb_sols_to_be_pruned # PS: dimacs_solutions should never be None or empty if len(dimacs_solutions) == 1: @@ -701,20 +707,18 @@ class MCLAnalyser(object): # (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) + LOGGER.info("Solution reachable in min_step: %s", min_step) + + # Forbidden solutions: already discovered macs + # (see at the end of the current loop). # Ban all sets of activated frontiers (1 set = 1 solution) - # 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 ? - ## TODO: keep previous dim_start à la première itération (mettre le contenu dans forbidden values) + # Equivalent of wrapping each previous solution with a logical AND: + # AND(not(frontier places)) 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() + + #### redondance partielle avec next_mac() # Solutions differ on frontiers: Search only 2 different solutions # to avoid all activated solutions # Get <tuple <DimacsFrontierSol>> @@ -725,7 +729,7 @@ class MCLAnalyser(object): LOGGER.info("MCLA: NOT FOUND -> satis test; current step %s", self.unfolder.current_step) - if self.unfolder.current_step + 1 > max_user_step: + if self.unfolder.current_step == max_user_step: # Cosmetic break, avoid to do useless test break @@ -745,7 +749,7 @@ class MCLAnalyser(object): 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 + # The problem is definitively not satisfiable in the given # number of steps break # __steps_before_check can't be >= min_step @@ -837,7 +841,7 @@ class MCLAnalyser(object): the horizon on which the properties must be satisfied @return: <generator <FrontierSolution>> """ - ## TODO convert start_property in dim_start !! => eviter la recompilation des propriétés + ## TODO: convert start_property in dim_start !! => eviter la recompilation des propriétés # Get <generator <DimacsFrontierSol>> mac_list = self.__mac_exhaustive_search(query, max_step) # Convert to a generator of FrontierSolution objects