diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py index d168c5924f730e946d0247db9aa4c1fa2a1e90ad..9218924fc3fdf3576b275686b8a5d82b6a1b39a6 100644 --- a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py +++ b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py @@ -378,7 +378,7 @@ class MCLAnalyser(object): reduce the number of activated frontier variables from this solution while inducing "prop". - Find at most nb_sols_to_be_pruned frontier solutions inducing + Find at most `nb_sols_to_be_pruned` frontier solutions inducing the same final property but with all inactivated frontier places forced to be initially False. @@ -470,11 +470,10 @@ class MCLAnalyser(object): def sq_solutions(self, query, max_step, max_sol, vvars): """Return a list of RawSolution objects - Parameters are the same as in sq_is_satisfiable() except for vvars - parameter which deserves some explanations. - This function is the lowest level function exploiting the solver results. + Parameters are the same as in sq_is_satisfiable() except for vvars + parameter which deserves some explanations. The solver doesn’t provide all solutions of the set of logical constraints encoding the temporal property. It gives only a sample of these solutions @@ -677,6 +676,13 @@ class MCLAnalyser(object): def next_mac(self, query, max_step): """Search a Minimal Access Condition for the given query. + This is a function very similar to __mac_exhaustive_search(), but it + returns only 1 solution. + Satisfiability tests and the banishment of previous solutions must be + done before the call. + + --- + On cherche ensuite d'abord des solutions non minimales (actuellement 2) via: self.__sq_dimacs_frontier_solutions(query, nb_step, 2)