Commit aa72badd authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] MCLAnalyser Refactor documentation and variable naming

parent 7bc2a944
......@@ -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>)
"""
......
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