Commit 887f0bdf authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] MCLAnalyser: Doc and fix typos

parent 05f970f8
......@@ -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)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment