diff --git a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
index 5e3a49d66a754af2c64c56b93b2a480b29a0f95a..e1238f986d6e9dac45ed5e7a9aa7a21585b9c658 100644
--- a/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
+++ b/library/cadbiom/models/clause_constraints/mcl/MCLAnalyser.py
@@ -187,8 +187,8 @@ class MCLAnalyser(object):
## Solutions processing ####################################################
def less_activated_solution(self, dimacs_solution_list):
- """Get the solution with the less number of activated
- states among the given solutions.
+ """Get the solution with the less number of activated frontier places
+ among the given solutions.
..note:: There is not constraint on the complexity of the trajectories;
only on the number of activated frontier places.
@@ -204,47 +204,60 @@ class MCLAnalyser(object):
return dimacs_solution_list[nb_activated.index(min(nb_activated))]
- def __solve_with_inact_fsolution(self, dimacs_front_sol, query, max_step, max_sols):
- """Frontier states not activated in dimacs_front_sol (frontier solution)
- are **forced to be False at start**; solve this and return first frontier
- solutions list with this constraint (this number is defined in the
- argument: max_sols).
+ def __solve_with_inact_fsolution(self, dimacs_front_sol, query, max_step, max_sol):
+ """Frontier states not activated in dimacs_front_sol (DimacsFrontierSol)
+ are **forced to be False at start**; solve this and return DimacsFrontierSol
+ objects matching this constraint (their number is defined with the
+ argument `max_sol`).
- @param dimacs_front_sol: list<DimacsFrontierSol>
- one solution to obtain the property in dimacs format
- @param query: current query
- @param max_step: int - Number of steps allowed in the unfolding;
+ :param dimacs_front_sol: A solution to obtain the property.
+ :param query: Current query
+ :param max_step: Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
- @return: <tuple <DimacsFrontierSol>>
-
- @precondition: dimacs_front_sol is a frontier solution for the query
+ :param max_sol: Number of wanted solutions.
+ :return: DimacsFrontierSol objects matching the constraint of
+ useless inactivated frontier places.
+ :type dimacs_front_sol: <DimacsFrontierSol>
+ :type query: <MCLSimpleQuery>
+ :type max_step: <int>
+ :type max_sol: <int>
+ :return: <tuple <DimacsFrontierSol>>
+ :precondition: dimacs_front_sol is a frontier solution for the query
"""
# Collect inactivated frontier places
# OLD:
- # final_dsol = [[var] for var in dimacs_front_sol.frontier_values if var < 0]
+ # inactive_frontier_values = \
+ # [[var] for var in dimacs_front_sol.frontier_values if var < 0]
# Intersection between pre-computed negative values for all frontiers
# and all frontiers (negative and positive) in the given solution
- final_dsol = \
+ inactive_frontier_values = \
[[var] for var in
- self.unfolder.frontiers_negative_values & dimacs_front_sol.frontier_values] ## TODO: utilisation dimacs frontier_values
+ self.unfolder.frontiers_negative_values & dimacs_front_sol.frontier_values]
# Prepend inactivated frontier places as a start property in DIMACS form
if query.dim_start:
- query.dim_start = final_dsol + query.dim_start
+ query.dim_start = inactive_frontier_values + query.dim_start
else:
- query.dim_start = final_dsol
+ query.dim_start = inactive_frontier_values
# Must return fsol even if there is no more solution (search first 10 sols)
# Get <tuple <DimacsFrontierSol>>
- return self.__sq_dimacs_frontier_solutions(query, max_step, max_sols)
+ return self.__sq_dimacs_frontier_solutions(query, max_step, max_sol)
def __prune_frontier_solution(self, fsol, query, max_step):
- """"Take a frontier condition which induces a property prop and reduce the
- number of activated variables from this solution while inducing prop.
+ """"Take a frontier condition which induces a property "prop" and try to
+ reduce the number of activated frontier variables from this solution while
+ inducing "prop".
+
+ 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.
+
+ Repeat the operation until there is only one solution.
:type fsol: <DimacsFrontierSol>
- :type query: <MCLQuery>
- :rtype: <DimacsfrontierSol>
+ :type query: <MCLSimpleQuery>
+ :rtype: <DimacsFrontierSol>
ASSERT: fsol is a frontier condition implying sq satisfiability
"""
@@ -260,9 +273,9 @@ class MCLAnalyser(object):
i = 0
while is_pruned:
i += 1
- # find at most 10 ic frontier solutions with the same number of
- # activated frontier places and with all inactivated frontier places
- # forced to be False
+ # 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.
# return sol_to_prune if no more solution
# PS: We need to index the result in less_activated_solution
@@ -299,19 +312,20 @@ class MCLAnalyser(object):
def sq_is_satisfiable(self, query, max_step):
"""Check if the query is satisfiable.
- Many logical variables are auxiliary variables with no interest other
- than technical, we want different solutions to differ by their values on
- some set of significant variables.
+ ..warning::
+ Many logical variables are auxiliary variables with no interest other
+ than technical, we want different solutions to differ by their values
+ on some set of significant variables.
- ..warning:: **These variables of interest are not checked here!**
- It is just a satisfiability test!
+ **These variables of interest are not checked here!**
+ It is just a satisfiability test!
..warning:: No frontier place is initialized to False in simple queries.
:param query:
:param max_step: Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
- :type query: <MCLQuery>
+ :type query: <MCLSimpleQuery>
:type max_step: <int>
:rtype: <boolean>
"""
@@ -367,7 +381,7 @@ class MCLAnalyser(object):
because it returns FrontierSolutions.
- @param query: MCLQuery
+ @param query: MCLSimpleQuery
@param max_step: int - Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
:param vvars: Variables for which solutions must differ.
@@ -425,7 +439,7 @@ class MCLAnalyser(object):
@warning: no frontier places are initialized to False
- @param query: MCLQuery
+ @param query: MCLSimpleQuery
@param max_step: int - Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
@param max_sol: max number of wanted solutions.
@@ -446,14 +460,15 @@ class MCLAnalyser(object):
DimacsFrontierSol objects provides some interesting attributes like:
activated_frontier_values (raw values of literals).
- FrontierSolution are of higher level without such attributes.
+ Note: FrontierSolution are of higher level without such attributes.
- @param query: MCLQuery
+ @param query: MCLSimpleQuery
@param max_step: int - Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
@param max_sol: int - max number of solutions for each solve
:return: Tuple of unique DimacsFrontierSol objects built from RawSolutions
from the solver.
+ .. note:: Unicity is based on the set of activated frontier values.
:rtype: <tuple <DimacsFrontierSol>>
"""
vvars = self.unfolder.frontier_values
@@ -533,25 +548,25 @@ class MCLAnalyser(object):
def next_mac(self, query, max_step):
"""Search a Minimal Access Condition for the given query.
- on cherche d´abord des solutions non minimales
- pour ensuite les élaguer en supprimant les places non essentielles à la
- satisfiabilité de la propriété.
- Ce processus récursif 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,
- cad contiennent beaucoup plus de places.
+ On cherche ensuite d'abord des solutions non minimales (actuellement 2) via:
+ self.__sq_dimacs_frontier_solutions(query, nb_step, 2)
- if st_prop contains negation of mac conditions,
- return a different mac if any
- same parameters as __mac_exhaustive_search
- Used for search on cluster
+ 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 max_step: Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
- :type query: <MCLQuery> or <MCLSimpleQuery>
+ :type query: <MCLSimpleQuery>
:type max_step: <int>
- :return: a list of variables: FrontierSolution is a wrapping of a symbolic
- representation of frontier values and timing from a raw solution.
+ :return: A FrontierSolution which is a wrapper of a symbolic
+ representation of frontier values and timings from a raw solution.
:rtype: <FrontierSolution> - <list <str>>
"""
# Solutions differ on frontiers: Search only 2 different solutions
@@ -577,7 +592,7 @@ class MCLAnalyser(object):
..note:: __mac_exhaustive_search() returns DimacsFrontierSols
- @param query: MCLQuery
+ @param query: MCLSimpleQuery
@param max_step: int - Number of steps allowed in the unfolding;
the horizon on which the properties must be satisfied
@return: <generator <FrontierSolution>>
@@ -622,7 +637,7 @@ class MCLAnalyser(object):
Used for search on cluster
@param mac: FrontierSolution
- @param query: MCLQuery
+ @param query: MCLSimpleQuery
@param max_step: int - number of dynamical step
@return: a list of variables (list<string>)
"""