Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 05f970f8 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] MCLAnalyser: Module documentation

parent aa72badd
......@@ -41,6 +41,135 @@
##
"""
Main class to perform dynamic analysis of Cadbiom chart models.
## Here you will find a global view of the process of dynamic analysis
mac_search:
Wrapper for __mac_exhaustive_search()
Return a generator of FrontierSolution objects.
__mac_exhaustive_search:
Return a generator of FrontierSolution objects.
Test if the given query is satisfiable according the given maximum number of steps.
Get the minimum of steps that are mandatory to reach the final property in the query.
This task is made with: `sq_is_satisfiable(query, max_user_step)`
Which call internal functions of the unfolder (this is beyond the scope of this doc)
- Initialisation: `self.unfolder.init_with_query(query)`
- Ultimate test: `self.unfolder.squery_is_satisfied(max_step)`
Adjust the attribute `steps_before_check` of the query, this is the number of
useless shifts that are needed by the unfolder before finding a solution.
Reload in the query a list of frontiers values that constitute each solution
previously found.
These values are in DIMACS format (i.e, numerical values). Since we doesn't
want further similar solutions, each value has a negative sign
(which which means that a value is prohibited).
On banni les solutions précédemment trouvées. Une solution est apparentée à
un ensemble de places frontières;
Notons qu'il n'y a pas de contraintes sur les trajectoires ayant permis
d'obtenir un ensemble de places frontières.
Pour bannir les solutions 2 choix se présentent:
- Soit les joindre par des "and" logiques et contraindre chaque solution
par un "non".
Ex: Pour 2 solutions [(A, B), (B, C)]:
not((A and B) or (B and C))
- Soit conserver les valeurs de chaque ensemble de places frontière sous
forme de clauses constituées de valeurs numériques.
Ex: Pour 2 solutions [(A, B), (B, C)]:
[[-1, -2], [-2, -3]]
La deuxième solution est nettement plus performante car elle permet de
s'affranchir du travail de parsing réalisé par l'intervention d'une grammaire,
des propriétés de plus en plus complexes au fur et à mesure des solutions
trouvées.
Ainsi, chaque nouvelle requête se voit recevoir dans son attribut dim_start,
l'ensemble des solutions précédentes, bannies, au format DIMACS.
On cherche ensuite d'abord des solutions non minimales (actuellement 2) via:
`self.__sq_dimacs_frontier_solutions(query, nb_step, 2)`
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).
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.
---
## Back on the few mentioned functions and their call dependencies:
less_activated_solution(self, dimacs_solution_list):
Get the solution with the less number of activated frontier places among the given solutions.
__prune_frontier_solution(self, fsol, query, max_step):
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.
Return <DimacsFrontierSol>
This functions calls __solve_with_inact_fsolution().
__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_sols`)
Return <tuple <DimacsFrontierSol>>
This function calls __sq_dimacs_frontier_solutions().
__sq_dimacs_frontier_solutions(self, query, max_step, max_sol)
Search set of minimal solutions for the given query, with a maximum of steps
Tuple of unique DimacsFrontierSol objects built from RawSolutions
from the solver.
Return <tuple <DimacsFrontierSol>>
This function calls sq_solutions().
sq_solutions(query, max_step, max_sol, vvars)
This function is the lowest level function exploiting the solver results.
Return <list <RawSolution>>
This function calls:
self.unfolder.init_with_query(query)
self.unfolder.squery_solve(vvars, max_step, max_sol)
## Quiet deprecated but still used in the GUI:
sq_frontier_solutions(self, query, max_step, max_sol):
This function is a wrapper of sq_solutions().
Return <list <FrontierSolution>>
"""
from __future__ import print_function
......
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