MCLAnalyser.py 41.7 KB
Newer Older
VIGNET Pierre's avatar
VIGNET Pierre committed
1
# -*- coding: utf-8 -*-
VIGNET Pierre's avatar
VIGNET Pierre committed
2 3 4
## Filename    : MCLAnalyser.py
## Author(s)   : Michel Le Borgne
## Created     : 03/2012
5 6
## Revision    :
## Source      :
VIGNET Pierre's avatar
VIGNET Pierre committed
7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36
##
## Copyright 2012 : IRISA/IRSET
##
## This library is free software; you can redistribute it and/or modify it
## under the terms of the GNU General Public License as published
## by the Free Software Foundation; either version 2.1 of the License, or
## any later version.
##
## This library is distributed in the hope that it will be useful, but
## WITHOUT ANY WARRANTY, WITHOUT EVEN THE IMPLIED WARRANTY OF
## MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE.  The software and
## documentation provided here under is on an "as is" basis, and IRISA has
## no obligations to provide maintenance, support, updates, enhancements
## or modifications.
## In no event shall IRISA be liable to any party for direct, indirect,
## special, incidental or consequential damages, including lost profits,
## arising out of the use of this software and its documentation, even if
## IRISA have been advised of the possibility of such damage.  See
## the GNU General Public License for more details.
##
## You should have received a copy of the GNU General Public License
## along with this library; if not, write to the Free Software Foundation,
## Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
##
## The original code contained here was initially developed by:
##
##     Michel Le Borgne.
##     IRISA
##     Symbiose team
##     IRISA  Campus de Beaulieu
37 38
##     35042 RENNES Cedex, FRANCE
##
VIGNET Pierre's avatar
VIGNET Pierre committed
39 40 41 42 43
##
## Contributor(s): Geoffroy Andrieux - IRISA/IRSET
##
"""
Main class to perform dynamic analysis of Cadbiom chart models.
44

45 46 47 48 49 50 51
Discrete event system simulation is a standard simulation scheme which consists
in the repetition of the following actions until some halting condition
is satisfied:
- Find the current events and inputs (including free events)
- Find the state variables subject to change
- Perform the state evolution

52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170
## 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:
171
        self.unfolder.init_with_query(query, check_query=False)
172 173 174 175 176 177 178 179
        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>>
VIGNET Pierre's avatar
VIGNET Pierre committed
180
"""
181 182
from __future__ import print_function

183
from antlr3 import ANTLRFileStream, CommonTokenStream
VIGNET Pierre's avatar
VIGNET Pierre committed
184

185
from cadbiom.models.guard_transitions.translators.chart_xml import \
VIGNET Pierre's avatar
VIGNET Pierre committed
186
        MakeModelFromXmlFile
187 188

from cadbiom.models.guard_transitions.translators.chart_xml_pid import \
VIGNET Pierre's avatar
VIGNET Pierre committed
189
        MakeModelFromPidFile
190 191

from cadbiom.models.guard_transitions.analyser.ana_visitors import TableVisitor
VIGNET Pierre's avatar
VIGNET Pierre committed
192
from cadbiom.models.clause_constraints.mcl.MCLTranslators import GT2Clauses
193
from cadbiom.models.clause_constraints.mcl.CLUnfolder import CLUnfolder
194
from cadbiom.models.clause_constraints.mcl.MCLSolutions import MCLException
195 196 197 198 199

from cadbiom.models.clause_constraints.CLDynSys import CLDynSys
from cadbiom.models.guard_transitions.translators.cadlangLexer import cadlangLexer
from cadbiom.models.guard_transitions.translators.cadlangParser import cadlangParser
from cadbiom.models.guard_transitions.chart_model import ChartModel
VIGNET Pierre's avatar
VIGNET Pierre committed
200 201 202 203
from cadbiom.models.clause_constraints.mcl.MCLSolutions import (
    FrontierSolution,
    DimacsFrontierSol,
)
204
from cadbiom.models.clause_constraints.mcl.MCLQuery import MCLSimpleQuery
205
from cadbiom import commons as cm
206 207 208 209

# Standard imports
from logging import DEBUG, INFO

210 211
LOGGER = cm.logger()

VIGNET Pierre's avatar
VIGNET Pierre committed
212 213

class MCLAnalyser(object):
VIGNET Pierre's avatar
VIGNET Pierre committed
214
    """Query a dynamical system and analyse the solutions
215 216 217 218 219 220 221 222 223 224 225 226

    When loading a model in a MCLAnalyser object, a CLUnfolder is generated which
    implies the compilation of the dynamical system into a clause constraint
    dynamical system and the DIMACS coding of all the variables.
    This coding cannot be changed later.
    The unfolding of constraints is performed efficiently on the numeric form
    of the clause constraints. The CLUnfolder provide various method to convert
    variable names to DIMACS code and back, to extract the frontier of a model
    and to extract informations from raw solutions.

    Attributes and default values:

227
        :param dynamic_system: dynamical system in clause constraint form
228 229 230 231 232 233 234
        :param unfolder: computation management: unfolding
        :param reporter: reporter for generic error display
        :param translator_opti: turn on optimizations for ANTLR translation
            (subexpression elimination)
        :param nb_sols_to_be_pruned: For mac search: We search a number of
            solutions that will be pruned later, in order to find the most
            optimized MAC with a reduced the number of activated frontiers.
235
        :key debug: (optional) Used to activate debug mode in the Unfolder
236

237
        :type dynamic_system: None before loading a model / <CLDynSys>
238
        :type unfolder: None before loading a model / <CLUnfolder>
239
        :type debug: False / <boolean>
240 241
        :type reporter: <ErrorRep>
        :type translator_opti: True / <boolean>
242
        :type nb_sols_to_be_pruned: 10
VIGNET Pierre's avatar
VIGNET Pierre committed
243
    """
244

245
    def __init__(self, report, debug=False):
246 247
        """The built analyser is void by default

VIGNET Pierre's avatar
VIGNET Pierre committed
248 249
        @param report: a standard reporter
        """
250 251 252 253
        self.debug = debug
        self.unfolder = None
        self.reporter = report
        self.translator_opti = True
254 255 256 257 258 259 260

        # For mac search: We search a number of solutions that will be pruned
        # in order to find the most optimized MAC with a reduced the number of
        # activated frontiers.
        ## TODO: ajuster ce paramètre dynamiquement
        self.nb_sols_to_be_pruned = 10

261
    @property
262
    def dynamic_system(self):
263
        """Return the CLDynSys object of the current unfolder"""
264
        return self.unfolder.dynamic_system
265

266
    ## Building MCLAnalyser ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
267 268

    def build_from_chart_model(self, model):
269
        """Build an MCLAnalyser and its CLUnfolder from a chartmodel object.
270 271 272

        Every parser uses this function at the end.

273
        @param model: <ChartModel>
VIGNET Pierre's avatar
VIGNET Pierre committed
274
        """
275
        # Reloading a MCLAnalyser is forbidden - create a new one is mandatory
VIGNET Pierre's avatar
VIGNET Pierre committed
276 277
        if self.unfolder:
            raise MCLException("This MCLAnalyser is already initialized")
278 279

        # Build CLDynSys (dynamical system in clause constraint form)
280
        # Parse the model data
281
        vtab = TableVisitor(self.reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
282 283 284
        model.accept(vtab)
        if self.reporter.error:
            return
285 286 287
        # PS:
        # Here, all keys of vtab.tab_symb = no_frontiers + frontiers + model name
        # (probably a bug for this last one)
288
        dynamic_system = CLDynSys(vtab.tab_symb, self.reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
289 290
        if self.reporter.error:
            return
291
        # Build clauses and auxiliary variables from events and places in the model
292
        comp_visitor = GT2Clauses(dynamic_system, self.reporter, self.translator_opti)
VIGNET Pierre's avatar
VIGNET Pierre committed
293 294 295
        model.accept(comp_visitor)
        if self.reporter.error:
            return
296
        # Build unfolder
297
        self.unfolder = CLUnfolder(dynamic_system, debug=self.debug)
VIGNET Pierre's avatar
VIGNET Pierre committed
298 299

    def build_from_chart_file(self, file_name):
300 301
        """Build an MCLAnalyser from a .bcx file

VIGNET Pierre's avatar
VIGNET Pierre committed
302 303 304 305
        @param file_name: str - path of the .bcx file
        """
        parsing = MakeModelFromXmlFile(file_name)
        # chart model
306
        self.build_from_chart_model(parsing.model)
307 308 309

    def build_from_pid_file(self, file_name, has_clock=True, ai_interpretation=0):
        """Build an MCLAnalyser from a .xml file of PID database
VIGNET Pierre's avatar
VIGNET Pierre committed
310 311 312

        @param file_name: str - path of .xml file
        """
313 314 315
        parsing = MakeModelFromPidFile(
            file_name, self.reporter, has_clock, ai_interpretation
        )
VIGNET Pierre's avatar
VIGNET Pierre committed
316
        # chart model
317
        self.build_from_chart_model(parsing.model)
318

VIGNET Pierre's avatar
VIGNET Pierre committed
319
    def build_from_cadlang(self, file_name):
320 321
        """Build an MCLAnalyser from a .cal, Cadlang file

VIGNET Pierre's avatar
VIGNET Pierre committed
322 323 324 325
        @param file_name: str - path of .cal file
        """
        creporter = self.reporter
        fstream = ANTLRFileStream(file_name)
326
        lexer = cadlangLexer(fstream)
VIGNET Pierre's avatar
VIGNET Pierre committed
327 328 329 330 331 332
        lexer.set_error_reporter(creporter)
        parser = cadlangParser(CommonTokenStream(lexer))
        parser.set_error_reporter(creporter)
        model = ChartModel(file_name)
        parser.cad_model(model)
        # chart model
333
        self.build_from_chart_model(parser.model)
VIGNET Pierre's avatar
VIGNET Pierre committed
334

335
    ## Solutions processing ####################################################
336

VIGNET Pierre's avatar
VIGNET Pierre committed
337
    def less_activated_solution(self, dimacs_solution_list):
338 339
        """Get the solution with the less number of activated frontier places
        among the given solutions.
340

VIGNET Pierre's avatar
VIGNET Pierre committed
341
        .. note:: There is not constraint on the complexity of the trajectories;
342 343 344 345 346 347
            only on the number of activated frontier places.

        :param dimacs_solution_list: list of DimacsFrontierSol objects
        :return: 1 DimacsFrontierSol with the less number of activated states.
        :type dimacs_solution_list: <tuple <DimacsFrontierSol>>
        :rtype: <DimacsFrontierSol>
VIGNET Pierre's avatar
VIGNET Pierre committed
348
        """
349
        # Count the number of activated places in each solution
VIGNET Pierre's avatar
VIGNET Pierre committed
350 351
        activated_per_sol = [sol.nb_activated_frontiers for sol in dimacs_solution_list]
        return dimacs_solution_list[activated_per_sol.index(min(activated_per_sol))]
352

353 354 355 356 357
    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`).
358

359 360 361
        :param dimacs_front_sol: A solution to obtain the property.
        :param query: Current query
        :param max_step: Number of steps allowed in the unfolding;
362
            the horizon on which the properties must be satisfied
363 364 365 366 367 368 369 370 371
        :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
VIGNET Pierre's avatar
VIGNET Pierre committed
372
        """
373
        # Collect inactivated frontier places
374
        # OLD:
375 376
        # inactive_frontier_values = \
        #     [[var] for var in dimacs_front_sol.frontier_values if var < 0]
377
        # Intersection between pre-computed negative values for all frontiers
VIGNET Pierre's avatar
VIGNET Pierre committed
378
        # (negative and positive) in the given solution, and all frontiers.
VIGNET Pierre's avatar
VIGNET Pierre committed
379 380 381 382 383
        inactive_frontier_values = [
            [var]
            for var in self.unfolder.frontiers_negative_values
            & dimacs_front_sol.frontier_values
        ]
384

385 386 387 388
        # Append inactivated frontier places as a start property in DIMACS form
        # PS: do not test dim_start: In the worse case, it's an empty list.
        query.dim_start += inactive_frontier_values

389 390
        # Must return fsol even if there is no more solution (search first 10 sols)
        # Get <tuple <DimacsFrontierSol>>
391
        return self.__sq_dimacs_frontier_solutions(query, max_step, max_sol)
392 393

    def __prune_frontier_solution(self, fsol, query, max_step):
394 395 396 397
        """"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".

398
        Find at most `nb_sols_to_be_pruned` frontier solutions inducing
399 400 401 402
        the same final property but with all inactivated frontier places
        forced to be initially False.

        Repeat the operation until there is only one solution.
403

VIGNET Pierre's avatar
VIGNET Pierre committed
404 405
        :param fsol: A DimacsFrontierSol for which we assume/assert that the
            system is satisfiable.
406
        :type fsol: <DimacsFrontierSol>
407 408
        :type query: <MCLSimpleQuery>
        :rtype: <DimacsFrontierSol>
409

VIGNET Pierre's avatar
VIGNET Pierre committed
410 411 412 413 414 415 416 417
        .. todo::
            - regarder si les solutions dimacs_solutions sont si différentes.
            il est possible que le solveur soit relativement optimisé pour qu'on
            puisse en demander moins ou qu'on puisse éliminer les solutions les
            moins diversifiées (détection d'un ensemble commun de places dont on
            forcerait l'inactivation pas l'intermédiaire d'une clause de l'état
            initial).
            - ajuster automatiquement nb_sols_to_be_pruned (10 actuellement)
VIGNET Pierre's avatar
VIGNET Pierre committed
418
        """
419 420 421 422 423 424
        # for debug - too expansive to be activated anytime
        # assert(self.sq_is_satisfiable(query, max_step))
        sol_to_prune = fsol
        # Number of activated places in solution
        # We are trying to reduce this number
        current_len = fsol.nb_activated_frontiers
VIGNET Pierre's avatar
VIGNET Pierre committed
425 426
        next_len = 0
        is_pruned = True
427

428
        i = 0
VIGNET Pierre's avatar
VIGNET Pierre committed
429
        while is_pruned:
430
            i += 1
431 432 433
            # 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.
434 435 436 437
            # return sol_to_prune if no more solution

            # PS: We need to index the result in less_activated_solution
            # thus, this why __solve_with_inact_fsolution() returns a tuple.
VIGNET Pierre's avatar
VIGNET Pierre committed
438 439 440
            dimacs_solutions = self.__solve_with_inact_fsolution(
                sol_to_prune, query, max_step, self.nb_sols_to_be_pruned
            )
441 442 443 444

            LOGGER.info(
                "MCLA::Prune: Iteration %s, nb pruned inact solutions: %s",
                i,
VIGNET Pierre's avatar
VIGNET Pierre committed
445
                len(dimacs_solutions),
446
            )
VIGNET Pierre's avatar
VIGNET Pierre committed
447 448

            # PS: dimacs_solutions should never be None or empty
VIGNET Pierre's avatar
VIGNET Pierre committed
449
            if len(dimacs_solutions) == 1:
450 451
                # No new solution has been found,
                # the current solution is the best (sol_to_prune)
VIGNET Pierre's avatar
VIGNET Pierre committed
452
                return dimacs_solutions[0]  # it's sol_to_prune variable
453 454 455 456 457

            # Seach for less activated solution
            # Get the solution with the less number of activated states
            next_sol = self.less_activated_solution(dimacs_solutions)
            next_len = next_sol.nb_activated_frontiers
VIGNET Pierre's avatar
VIGNET Pierre committed
458
            is_pruned = current_len > next_len
459 460 461 462 463 464

            LOGGER.info(
                "MCLA::Prune: Current solution activated length:%s next:%s",
                current_len, next_len
            )

VIGNET Pierre's avatar
VIGNET Pierre committed
465
            if is_pruned:
466
                sol_to_prune = next_sol
VIGNET Pierre's avatar
VIGNET Pierre committed
467
                current_len = next_len
468

VIGNET Pierre's avatar
VIGNET Pierre committed
469
        # never reach this point
470
        raise MCLException("MCLAnalyser:__prune_frontier_solution:: what happened?")
471

472
    ## Generic solver for simple queries #######################################
473

VIGNET Pierre's avatar
VIGNET Pierre committed
474
    def sq_is_satisfiable(self, query, max_step):
475 476
        """Check if the query is satisfiable.

VIGNET Pierre's avatar
VIGNET Pierre committed
477
        .. warning::
478 479 480
            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.
VIGNET Pierre's avatar
VIGNET Pierre committed
481

482 483
            **These variables of interest are not checked here!**
                It is just a satisfiability test!
484

VIGNET Pierre's avatar
VIGNET Pierre committed
485
        .. warning:: No frontier place is initialized to False in simple queries.
486 487 488 489

        :param query:
        :param max_step: Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
490
        :type query: <MCLSimpleQuery>
491 492
        :type max_step: <int>
        :rtype: <boolean>
VIGNET Pierre's avatar
VIGNET Pierre committed
493
        """
494 495 496
        # Initialise the unfolder with the given query
        # Following properties are used from the query:
        #    start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
497
        #    variant_prop, dim_variant, steps_before_check
498
        self.unfolder.init_with_query(query, check_query=False)
VIGNET Pierre's avatar
VIGNET Pierre committed
499 500
        # go
        return self.unfolder.squery_is_satisfied(max_step)
501

502
    def sq_solutions(self, query, max_step, max_sol, vvars, max_user_step=None):
503 504 505 506
        """Return a list of RawSolution objects

        This function is the lowest level function exploiting the solver results.

507 508
        Parameters are the same as in sq_is_satisfiable() except for vvars
        parameter which deserves some explanations.
509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527

        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
        limited in number by the max_sol parameter. **Since 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. That is the meaning of the vvars parameter.**

        Remark that the variables of interest must be specified in DIMACS code.
        Most of the time, this method is used internally, so DIMACS code is
        transparent to the user.

        The class RawSolution provides a representation of solutions which are
        raw results from the SAT solver with all variable parameters from the
        unfolder, and consequently not easily readable.
        In addition to the solution in DIMACS form (including values for auxiliary
        variables), a RawSolution object registers data which permit information
        extraction from these raw solutions. The most important methods are:

528
            - frontier_pos_and_neg_values:
529 530 531 532 533 534 535 536 537 538 539 540 541 542 543
                Which extracts the frontier values from the solution.
                These values are in DIMACS code.

            - extract_activated_frontier_values():
                Extracts frontier variables which are active in solution.

            - extract_act_input_clock_seq():
                Extract the sequence of activated inputs and events in the solution.


        In models of signal propagation, we are more interested in frontier solutions.
        The following method is then well adapted: sq_frontier_solutions(),
        because it returns FrontierSolutions.


VIGNET Pierre's avatar
VIGNET Pierre committed
544 545
        :param query: Query.
        :param max_step: Number of steps allowed in the unfolding;
546
            the horizon on which the properties must be satisfied
547 548 549
        :param vvars: Variables for which solutions must differ.
            In practice, it is a list with the values (Dimacs code)
            of all frontier places of the system.
550
        :key max_user_step: (Optional) See :meth:`__mac_exhaustive_search`.
VIGNET Pierre's avatar
VIGNET Pierre committed
551 552
        :type query: <MCLSimpleQuery>
        :type max_step: <int>
553
        :type vvars: <list <int>>
554
        :type max_user_step: <int>
555 556
        :return: a list of RawSolutions from the solver
        :rtype: <list <RawSolution>>
557

VIGNET Pierre's avatar
VIGNET Pierre committed
558
        .. warning:: no_frontier places are initialized to False in simple queries
VIGNET Pierre's avatar
VIGNET Pierre committed
559
            except if initial condition.
560

VIGNET Pierre's avatar
VIGNET Pierre committed
561 562 563
        .. warning:: if the query includes variant constraints,
            the horizon (max_step) is automatically adjusted to
            min(max_step, len(variant_constraints)).
VIGNET Pierre's avatar
VIGNET Pierre committed
564
        """
565 566 567
        # Initialise the unfolder with the given query
        # Following properties are used from the query:
        #    start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
568
        #    variant_prop, dim_variant, steps_before_check
569
        self.unfolder.init_with_query(query, check_query=False)
VIGNET Pierre's avatar
VIGNET Pierre committed
570
        # go
VIGNET Pierre's avatar
VIGNET Pierre committed
571 572 573
        return self.unfolder.squery_solve(
            vvars, max_step, max_sol, max_user_step=max_user_step
        )
574

VIGNET Pierre's avatar
VIGNET Pierre committed
575
    def sq_frontier_solutions(self, query, max_step, max_sol):
576
        """Compute active frontier places and timings
577

578 579
        Compute the set of frontier place names which must be activated for
        implying query satisfaction and returned it as a list of FrontierSolution.
580

581 582 583 584
        Quiet deprecated but referenced by:
            gt_gui/chart_checker/chart_checker_controler
            cadbiom_cmd/solution_search.py very old code for debug purpose
            self.mac_inhibitor_search
585

586 587 588
        In models of signal propagation, we are more interested in frontier solutions.
        So the current method is better adapted: sq_frontier_solutions()
        than sq_solutions() which returns RawSolutions.
VIGNET Pierre's avatar
VIGNET Pierre committed
589

590
        This function is a wrapper of sq_solutions().
591

VIGNET Pierre's avatar
VIGNET Pierre committed
592

593 594 595 596
        The class FrontierSolution provides objects wrapping a symbolic
        representation of frontier values and timing from a raw solution.
            - The main attributes are activated_frontier which is a set of
            (string) names of frontier places which are activated in the solution.
597

598 599 600
            - The second important attribute is ic_sequence, a list of strings
            which describes the successive activated inputs and free events in
            the solution.
601

602 603 604
        If events h2, h5 and input in3 are activated at step k in the solution,
        then the kth element of the list is “% h2 h5 in3”.
        This format is understood by the Cadbiom simulator.
605

606 607
        @warning: no frontier places are initialized to False

608
        @param query: MCLSimpleQuery
609 610 611 612 613 614 615
        @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.
        @return: List of FrontierSolutions built from RawSolutions from the solver.
            So, lists of lists of frontier place names which must be activated
            for implying query satisfaction
        :rtype: <list <FrontierSolution>>
VIGNET Pierre's avatar
VIGNET Pierre committed
616
        """
617 618 619 620 621
        vvars = self.unfolder.frontier_values
        # sq_solutions() returns <list <RawSolution>>
        # We transtype them to FrontierSolution
        return [FrontierSolution.from_raw(sol) for sol
                in self.sq_solutions(query, max_step, max_sol, vvars)]
VIGNET Pierre's avatar
VIGNET Pierre committed
622

VIGNET Pierre's avatar
VIGNET Pierre committed
623

624
    def __sq_dimacs_frontier_solutions(self, query, max_step, max_sol, max_user_step=None):
625
        """Search set of minimal solutions for the given query, with a maximum of steps
626

627 628
        DimacsFrontierSol objects provides some interesting attributes like:
        activated_frontier_values (raw values of literals).
629
        Note: FrontierSolution are of higher level without such attributes.
630

631 632
        :param query: Query
        :param max_step: Number of steps allowed in the unfolding;
633
            the horizon on which the properties must be satisfied
634 635 636 637 638 639
        :param max_sol: Max number of solutions for each solve
        :key max_user_step: (Optional) See :meth:`__mac_exhaustive_search`
        :type query: <MCLSimpleQuery>
        :type max_step: <int>
        :type max_sol: <int>
        :type max_user_step: <int>
640 641
        :return: Tuple of unique DimacsFrontierSol objects built from RawSolutions
            from the solver.
642
            .. note:: Unicity is based on the set of activated frontier values.
643 644 645 646
        :rtype: <tuple <DimacsFrontierSol>>
        """
        vvars = self.unfolder.frontier_values
        # sq_solutions() returns <list <RawSolution>>
VIGNET Pierre's avatar
VIGNET Pierre committed
647 648 649
        raw_sols = self.sq_solutions(
            query, max_step, max_sol, vvars, max_user_step=max_user_step
        )
650 651
        # Get unique DimacsFrontierSol objects from RawSolution objects
        dimacfrontsol = DimacsFrontierSol.get_unique_dimacs_front_sols_from_raw_sols(raw_sols)
652 653 654 655 656 657

        if LOGGER.getEffectiveLevel() == INFO:
            LOGGER.info(
                "MCLA: Nb queried: %s, steps: %s\n"
                "\tget: %s, unique: %s\n"
                "\tactivated fronts per dimacfrontsol: %s",
658
                max_sol, self.unfolder.current_step,
659 660 661
                len(raw_sols), len(dimacfrontsol),
                [len(sol) for sol in dimacfrontsol]
            )
662
        return dimacfrontsol
663

664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689
    def __mac_exhaustive_search(self, query, max_user_step):
        """Return a generator of FrontierSolution objects.

        This is a function very similar to next_mac(), but it returns
        many solutions.
        The satisfiability tests and the banishment of the previous solutions
        are done internally in an optimal way.
        There is also a self adjustment of the number of minimum steps during
        which to find solutions until reaching the maximum number set by the user.

        ---

        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).

        :param query: Current query.
690 691 692 693 694
        :param max_user_step: Number of steps allowed by the user in the unfolding;
            the horizon on which the properties must be satisfied.
            This argument is also used to auto-adjust max_step for an extra step
            in CLUnfolder.
            .. seealso:: :meth:`cadbiom.models.clause_constraints.mcl.CLUnfolder.squery_solve`
695 696 697 698 699 700
        :type query: <MCLSimpleQuery>
        :type max_user_step: <int>
        :return: A generator of FrontierSolution objects which are a wrapper of
            a symbolic representation of frontier values and timings from
            a raw solution.
        :rtype: <generator <FrontierSolution>>
VIGNET Pierre's avatar
VIGNET Pierre committed
701
        """
702
        # list of timed minimal activation conditions on frontier (dimacs code)
VIGNET Pierre's avatar
VIGNET Pierre committed
703
        # i.e list<DimacsFrontierSol>
704
        # mac_list = [] # Not used anymore
705

VIGNET Pierre's avatar
VIGNET Pierre committed
706
        # Keep a list of frontier values to be banned in the next search
707
        forbidden_frontier_values = query.dim_start
708 709

        # Satisfiability test
VIGNET Pierre's avatar
VIGNET Pierre committed
710 711
        reachable = self.sq_is_satisfiable(query, max_user_step)

712
        # Get the minimum number of steps for reachability
713
        min_step = self.unfolder.current_step
714 715 716 717 718 719
        # Adjust the number of useless shifts needed before finding a solution
        # (i.e. testing final prop).
        # __steps_before_check can't be >= max_user_step
        # (see squery_is_satisfied() and squery_solve())
        query.steps_before_check = min_step - 1

720
        while reachable:
VIGNET Pierre's avatar
VIGNET Pierre committed
721 722 723 724
            LOGGER.info("Solution reachable in min_step: %s", min_step)

            # Forbidden solutions: already discovered macs
            # (see at the end of the current loop).
725
            # Ban all sets of activated frontiers (1 set = 1 solution)
VIGNET Pierre's avatar
VIGNET Pierre committed
726 727
            # Equivalent of wrapping each previous solution with a logical AND:
            # AND(not(frontier places))
728
            query.dim_start = list(forbidden_frontier_values)
VIGNET Pierre's avatar
VIGNET Pierre committed
729 730

            #### redondance partielle avec next_mac()
731 732 733
            # Solutions differ on frontiers: Search only 2 different solutions
            # to avoid all activated solutions
            # Get <tuple <DimacsFrontierSol>>
734
            dimacs_front_sol = self.__sq_dimacs_frontier_solutions(
VIGNET Pierre's avatar
VIGNET Pierre committed
735
                query, min_step, 2, max_user_step=max_user_step
736 737 738 739 740 741 742 743 744 745 746
            )

            # Self-adjustment of min_step/max_step may have taken place;
            # resynchronization of values:
            # __steps_before_check can't be >= min_step
            # (see squery_is_satisfied() and squery_solve())
            # __steps_before_check should be min_step - 1 to avoid a maximum of
            # useless checks from (min_step to current_step).
            min_step = self.unfolder.current_step
            query.steps_before_check = min_step - 1

747
            if not dimacs_front_sol:
748 749 750 751 752 753
                # No more solution
                # Note that self-adjust steps is made via max_user_step
                # argument of CLUnfolder.squery_solve

                LOGGER.info(
                    "MCLA:__mac_exhaustive_search: No more solution; current step %s",
VIGNET Pierre's avatar
VIGNET Pierre committed
754
                    self.unfolder.current_step,
755 756
                )

VIGNET Pierre's avatar
VIGNET Pierre committed
757
                assert self.unfolder.current_step == max_user_step
758 759
                # just break the loop
                break
760

761
            # Get the solution with the less number of activated states
762
            small_fsol = self.less_activated_solution(dimacs_front_sol)
763 764 765

            # Prune non essential places for the satisfiability of the property
            # => reduce the number of activated variables
766
            current_mac = self.__prune_frontier_solution(small_fsol, query, min_step)
767

768 769 770 771 772 773 774 775 776
            yield current_mac
            # mac_list.append(current_mac)

            # Keep a list of frontier values to be banned in the next search
            # - Get all activated frontiers on the current DimacsFrontierSol
            # - Build a list of their opposite values
            forbidden_frontier_values.append(
                [-var for var in current_mac.activated_frontier_values]
            )
777 778
            LOGGER.debug(
                "MCLA::mac_exhaustive_search: forbidden frontiers: %s",
VIGNET Pierre's avatar
VIGNET Pierre committed
779
                forbidden_frontier_values,
780
            )
781

782 783 784
    def next_mac(self, query, max_step):
        """Search a Minimal Access Condition for the given query.

785 786 787 788 789 790 791
        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.

        ---

792 793
        On cherche ensuite d'abord des solutions non minimales (actuellement 2) via:
        self.__sq_dimacs_frontier_solutions(query, nb_step, 2)
794

795 796 797 798 799 800 801 802 803
        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).
804

805 806
        :param max_step: Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
807
        :type query: <MCLSimpleQuery>
808
        :type max_step: <int>
809 810
        :return: A FrontierSolution which is a wrapper of a symbolic
            representation of frontier values and timings from a raw solution.
811 812 813 814 815 816 817
        :rtype: <FrontierSolution> - <list <str>>
        """
        # Solutions differ on frontiers: Search only 2 different solutions
        # to avoid all activated solutions
        # Get <tuple <DimacsFrontierSol>>
        lfsol = self.__sq_dimacs_frontier_solutions(query, max_step, 2)
        if not lfsol:
818
            return
819

820 821 822 823 824 825 826 827 828 829
        # Get the solution with the less number of activated states
        small_fsol = self.less_activated_solution(lfsol)

        # Prune non essential places for the satisfiability of the property
        # => reduce the number of activated variables
        current_mac = self.__prune_frontier_solution(small_fsol, query, max_step)

        return FrontierSolution.from_dimacs_front_sol(current_mac)

    def mac_search(self, query, max_step):
VIGNET Pierre's avatar
VIGNET Pierre committed
830 831
        """Wrapper for __mac_exhaustive_search(); return a generator of
        FrontierSolution objects.
832

VIGNET Pierre's avatar
VIGNET Pierre committed
833
        .. note:: __mac_exhaustive_search() returns DimacsFrontierSols
834

835
        @param query: MCLSimpleQuery
836 837
        @param max_step: int - Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
VIGNET Pierre's avatar
VIGNET Pierre committed
838
        @return: <generator <FrontierSolution>>
VIGNET Pierre's avatar
VIGNET Pierre committed
839
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
840
        ## TODO: convert start_property in dim_start !! => eviter la recompilation des propriétés
VIGNET Pierre's avatar
VIGNET Pierre committed
841
        # Get <generator <DimacsFrontierSol>>
842
        mac_list = self.__mac_exhaustive_search(query, max_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
843
        # Convert to a generator of FrontierSolution objects
844 845 846 847 848
        #return tuple(FrontierSolution.from_dimacs_front_sol(mac) for mac in mac_list)
        for mac in mac_list:
            yield FrontierSolution.from_dimacs_front_sol(mac)

    ## Inhibitors ##############################################################
849

VIGNET Pierre's avatar
VIGNET Pierre committed
850
    def is_strong_activator(self, act_sol, query):
851 852
        """Test if an activation condition is a strong one (independent of timing)

VIGNET Pierre's avatar
VIGNET Pierre committed
853
        .. refactor note: Unclear function
854

855 856
        final property becomes the invariant property
        => Ex: test if "C3 and C4" will never append if start property is "A1 and C1 and B1"
857
        Cf TestMCLAnalyser...
858 859

        @return: False if the problem is satisfiable, True otherwise
VIGNET Pierre's avatar
VIGNET Pierre committed
860
        @param act_sol: FrontierSolution with activation condition
861
        @param query: the query used for act_sol condition
VIGNET Pierre's avatar
VIGNET Pierre committed
862
        """
863 864 865 866 867 868 869 870 871 872 873
        max_step = len(act_sol.ic_sequence) - 1
        print("max steps:", max_step)

        # Same timings, force inactivated frontiers
        query_1 = MCLSimpleQuery.from_frontier_sol_same_timing(act_sol, self.unfolder)

        inv_prop = 'not(' + query.final_prop + ')'
        #(None, None, 'A1 and C1 and B1', ['', 'h2', '', ''])
        print("naive query1:", query_1.final_prop, query_1.inv_prop,
              query_1.start_prop, query_1.variant_prop)

VIGNET Pierre's avatar
VIGNET Pierre committed
874
        query_2 = MCLSimpleQuery(None, inv_prop, None)
875 876 877
        #(None, 'not(C3 and C4)', None, [])
        print("query 2:", query_2.final_prop, query_2.inv_prop,
              query_2.start_prop, query_2.variant_prop)
VIGNET Pierre's avatar
VIGNET Pierre committed
878
        query_1 = query_2.merge(query_1)
879 880 881 882 883 884
        #(None, 'not(C3 and C4)', 'A1 and C1 and B1', ['', 'h2', '', '']
        print("merged query1:", query_1.final_prop, query_1.inv_prop,
              query_1.start_prop, query_1.variant_prop)

        return not(self.sq_is_satisfiable(query_1, max_step))

885

VIGNET Pierre's avatar
VIGNET Pierre committed
886 887
    def next_inhibitor(self, mac, query):
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
888
        .. refactor note: Unclear function
889

890
        if st_prop contains negation of mac conditions,
VIGNET Pierre's avatar
VIGNET Pierre committed
891 892 893
        return a different mac if any
        same parameters as __mac_exhaustive_search
        Used for search on cluster
894

VIGNET Pierre's avatar
VIGNET Pierre committed
895
        @param mac: FrontierSolution
896
        @param query: MCLSimpleQuery
897
        @param max_step: int - number of dynamical step
VIGNET Pierre's avatar
VIGNET Pierre committed
898 899 900
        @return: a list of variables (list<string>)
        """
        # query with mac init frontier places and  timing
VIGNET Pierre's avatar
VIGNET Pierre committed
901
        inh_query1 = MCLSimpleQuery.from_frontier_sol_same_timing(mac, self.unfolder)
VIGNET Pierre's avatar
VIGNET Pierre committed
902 903 904 905 906 907
        # query with negation of final prop as invariant property
        if not query.final_prop:
            raise MCLException("Query must have a final property")
        if not query.inv_prop:
            inv_prop = "not (" + query.final_prop + ")"
        else:
VIGNET Pierre's avatar
VIGNET Pierre committed
908
            inv_prop = query.inv_prop + "and (not (" + query.final_prop + "))"
VIGNET Pierre's avatar
VIGNET Pierre committed
909 910 911
        inh_query2 = MCLSimpleQuery(None, inv_prop, None)
        # init + timing + final property not reachable
        inh_query = inh_query1.merge(inh_query2)
912
        max_step = len(inh_query.variant_prop)
VIGNET Pierre's avatar
VIGNET Pierre committed
913
        assert max_step == len(mac.ic_sequence)
914

VIGNET Pierre's avatar
VIGNET Pierre committed
915 916
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
917
        next_inhib = self.next_mac(inh_query, max_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
918 919
        self.unfolder.set_include_aux_clauses(True)
        return next_inhib
920

VIGNET Pierre's avatar
VIGNET Pierre committed
921
    def mac_inhibitor_search(self, mac, query, max_sol):
922
        """Search inhibitors for a mac scenario
923

VIGNET Pierre's avatar
VIGNET Pierre committed
924
        .. refactor note: Unclear function
925

VIGNET Pierre's avatar
VIGNET Pierre committed
926 927 928 929
        @param mac: the mac
        @param query: the property enforced by the mac
        @param max_sol: limit on the number of solutions
        @param max_sol: maximum number of solutions
930

VIGNET Pierre's avatar
VIGNET Pierre committed
931 932 933 934 935 936 937 938 939 940
        @return: a list of frontier solution
        """
        # query with mac init frontier places and  timing
        inh_query1 = MCLSimpleQuery.from_frontier_sol(mac)
        # query with negation of final prop as invariant property
        if not query.final_prop:
            raise MCLException("Query must have a final property")
        if not query.inv_prop:
            inv_prop = "not (" + query.final_prop + ")"
        else:
VIGNET Pierre's avatar
VIGNET Pierre committed
941
            inv_prop = query.inv_prop + "and (not (" + query.final_prop + "))"
VIGNET Pierre's avatar
VIGNET Pierre committed
942 943 944
        inh_query2 = MCLSimpleQuery(None, inv_prop, None)
        # init + timing + final property not reachable
        inh_query = inh_query1.merge(inh_query2)
945

946
        max_step = len(inh_query.variant_prop)
VIGNET Pierre's avatar
VIGNET Pierre committed
947
        assert max_step == len(mac.ic_sequence)
VIGNET Pierre's avatar
VIGNET Pierre committed
948 949
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
950 951
#        lsol = self.sq_frontier_solutions(inh_query, max_step, max_sol)
        lsol = tuple(self.mac_search(inh_query, max_step))
VIGNET Pierre's avatar
VIGNET Pierre committed
952 953 954 955
        self.unfolder.set_include_aux_clauses(True)
        return lsol

    def is_strong_inhibitor(self, in_sol, query):