MCLAnalyser.py 42.2 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
171
172
173
174
175
176
177
178
179
## 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>>
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
192
193

from cadbiom.models.guard_transitions.analyser.ana_visitors import TableVisitor
from cadbiom.models.clause_constraints.mcl.MCLTranslators import  GT2Clauses
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
200
from cadbiom.models.clause_constraints.mcl.MCLSolutions import FrontierSolution, DimacsFrontierSol
201
from cadbiom.models.clause_constraints.mcl.MCLQuery import MCLSimpleQuery
202
from cadbiom import commons as cm
203
204
205
206

# Standard imports
from logging import DEBUG, INFO

207
208
LOGGER = cm.logger()

VIGNET Pierre's avatar
VIGNET Pierre committed
209
210

class MCLAnalyser(object):
211
212
213
214
215
216
217
218
219
220
221
222
223
    """Query a UCL dynamical system and analyse solutions

    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:

224
        :param dynamical_system: dynamical system in clause constraint form
225
226
227
228
229
230
231
        :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.
232
        :key debug: (optional) Used to activate debug mode in the Unfolder
233

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

242
    def __init__(self, report, debug=False):
243
244
        """The built analyser is void by default

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

        # 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

258
259
260
261
262
    @property
    def dynamical_system(self):
        """Return the CLDynSys object of the current unfolder"""
        return self.unfolder.dynamical_system

263
    ## Building MCLAnalyser ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
264
265

    def build_from_chart_model(self, model):
266
        """Build an MCLAnalyser and its CLUnfolder from a chartmodel object.
267
268
269

        Every parser uses this function at the end.

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

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

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

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

    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
307
308
309

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

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

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

332
    ## Solutions processing ####################################################
333

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

        ..note:: There is not constraint on the complexity of the trajectories;
            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
345
        """
346
        # Count the number of activated places in each solution
VIGNET Pierre's avatar
VIGNET Pierre committed
347
348
        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))]
349
350


351
352
353
354
355
    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`).
356

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

381
382
383
384
        # 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

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


    def __prune_frontier_solution(self, fsol, query, max_step):
391
392
393
394
        """"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".

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

        Repeat the operation until there is only one solution.
400
401

        :type fsol: <DimacsFrontierSol>
402
403
        :type query: <MCLSimpleQuery>
        :rtype: <DimacsFrontierSol>
404

VIGNET Pierre's avatar
VIGNET Pierre committed
405
406
        ASSERT: fsol is a frontier condition implying sq satisfiability
        """
407
408
409
410
411
412
        # 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
413
414
        next_len = 0
        is_pruned = True
415

416
        i = 0
VIGNET Pierre's avatar
VIGNET Pierre committed
417
        while is_pruned:
418
            i += 1
419
420
421
            # 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.
422
423
424
425
426
427
428
429
430
431
432
            # 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.
            dimacs_solutions = \
                self.__solve_with_inact_fsolution(
                    sol_to_prune,
                    query,
                    max_step,
                    self.nb_sols_to_be_pruned
                )
433
434
435
436
437
438

            LOGGER.info(
                "MCLA::Prune: Iteration %s, nb pruned inact solutions: %s",
                i,
                len(dimacs_solutions)
            )
439
440
            ####TODO: regarder si ces solutions sont si différentes et ce qu'on en fait au final...
            ### en fin de compte il est possible que le solveur ne soit pas si bete...
VIGNET Pierre's avatar
VIGNET Pierre committed
441
442
443
            ##TODO:  ajuster automatiquement nb_sols_to_be_pruned

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

            # 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
453
            is_pruned = current_len > next_len
454
455
456
457
458
459

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

VIGNET Pierre's avatar
VIGNET Pierre committed
460
            if is_pruned:
461
                sol_to_prune = next_sol
VIGNET Pierre's avatar
VIGNET Pierre committed
462
                current_len = next_len
463

VIGNET Pierre's avatar
VIGNET Pierre committed
464
        # never reach this point
465
        raise MCLException("MCLAnalyser:__prune_frontier_solution:: what happened?")
466

467
    ## Generic solver for simple queries #######################################
468

VIGNET Pierre's avatar
VIGNET Pierre committed
469
    def sq_is_satisfiable(self, query, max_step):
470
471
        """Check if the query is satisfiable.

472
473
474
475
        ..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.
VIGNET Pierre's avatar
VIGNET Pierre committed
476

477
478
            **These variables of interest are not checked here!**
                It is just a satisfiability test!
479

480
481
482
483
484
        ..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
485
        :type query: <MCLSimpleQuery>
486
487
        :type max_step: <int>
        :rtype: <boolean>
VIGNET Pierre's avatar
VIGNET Pierre committed
488
        """
489
490
491
        # 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,
492
        #    variant_prop, dim_variant_prop, steps_before_check
493
        self.unfolder.init_with_query(query)
VIGNET Pierre's avatar
VIGNET Pierre committed
494
495
        # go
        return self.unfolder.squery_is_satisfied(max_step)
496
497


VIGNET Pierre's avatar
VIGNET Pierre committed
498
    def sq_solutions(self, query, max_step, max_sol, vvars):
499
500
501
502
        """Return a list of RawSolution objects

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

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

        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:

524
            - frontier_pos_and_neg_values:
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
                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.


540
        @param query: MCLSimpleQuery
541
542
        @param max_step: int - Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
543
544
545
546
        :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.
        :type vvars: <list <int>>
547
548
        :return: a list of RawSolutions from the solver
        :rtype: <list <RawSolution>>
549
550

        @warning:  no_frontier places are initialized to False in simple queries
VIGNET Pierre's avatar
VIGNET Pierre committed
551
            except if initial condition.
552

VIGNET Pierre's avatar
VIGNET Pierre committed
553
554
555
        @warning: if the query includes variant constraints, the horizon (max_step) is
            automatically adjusted to min(max_step, len(variant_constraints)).
        """
556
557
558
        # 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,
559
        #    variant_prop, dim_variant_prop, steps_before_check
560
        self.unfolder.init_with_query(query)
VIGNET Pierre's avatar
VIGNET Pierre committed
561
562
        # go
        return self.unfolder.squery_solve(vvars, max_step, max_sol)
563
564


VIGNET Pierre's avatar
VIGNET Pierre committed
565
    def sq_frontier_solutions(self, query, max_step, max_sol):
566
        """Compute active frontier places and timings
567

568
569
        Compute the set of frontier place names which must be activated for
        implying query satisfaction and returned it as a list of FrontierSolution.
570

571
572
573
574
        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
575

576
577
578
        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
579

580
        This function is a wrapper of sq_solutions().
581

VIGNET Pierre's avatar
VIGNET Pierre committed
582

583
584
585
586
        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.
587

588
589
590
            - The second important attribute is ic_sequence, a list of strings
            which describes the successive activated inputs and free events in
            the solution.
591

592
593
594
        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.
595

596
597
        @warning: no frontier places are initialized to False

598
        @param query: MCLSimpleQuery
599
600
601
602
603
604
605
        @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
606
        """
607
608
609
610
611
        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
612

VIGNET Pierre's avatar
VIGNET Pierre committed
613

614
615
    def __sq_dimacs_frontier_solutions(self, query, max_step, max_sol):
        """Search set of minimal solutions for the given query, with a maximum of steps
616

617
618
        DimacsFrontierSol objects provides some interesting attributes like:
        activated_frontier_values (raw values of literals).
619
        Note: FrontierSolution are of higher level without such attributes.
620

621
        @param query: MCLSimpleQuery
622
623
624
625
626
        @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.
627
            .. note:: Unicity is based on the set of activated frontier values.
628
629
630
631
632
633
634
        :rtype: <tuple <DimacsFrontierSol>>
        """
        vvars = self.unfolder.frontier_values
        # sq_solutions() returns <list <RawSolution>>
        raw_sols = self.sq_solutions(query, max_step, max_sol, vvars)
        # Get unique DimacsFrontierSol objects from RawSolution objects
        dimacfrontsol = DimacsFrontierSol.get_unique_dimacs_front_sols_from_raw_sols(raw_sols)
635
636
637
638
639
640
641
642
643
644

        if LOGGER.getEffectiveLevel() == INFO:
            LOGGER.info(
                "MCLA: Nb queried: %s, steps: %s\n"
                "\tget: %s, unique: %s\n"
                "\tactivated fronts per dimacfrontsol: %s",
                max_sol, max_step,
                len(raw_sols), len(dimacfrontsol),
                [len(sol) for sol in dimacfrontsol]
            )
645
        return dimacfrontsol
646
647


648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
    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.
        :param max_user_step: Number of steps allowed in the unfolding;
675
            the horizon on which the properties must be satisfied
676
677
678
679
680
681
        :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
682
        """
683
        # list of timed minimal activation conditions on frontier (dimacs code)
VIGNET Pierre's avatar
VIGNET Pierre committed
684
        # i.e list<DimacsFrontierSol>
685
        # mac_list = [] # Not used anymore
686
        forbidden_frontier_values = []
687

688
689
690
691
692
        ## TODO: parser les properties au format DIMACS une bonne fois pour toutes
        ## et les ajouter dans forbidden_frontier_values
        ## Lors du rechargement des places précédentes, le problème du parsing va réapparaitre

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

695
696
697
698
699
700
701
702
703
        # Get the minimum number of steps for reachability
        min_step = self.unfolder.get_current_step()
        # 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

        LOGGER.info("Solution reachable in min_step: %s", min_step)
704

705
        while reachable:
706
707
            # Forbidden solutions: already discovered macs (see at the end of the while loop)
            # Ban all sets of activated frontiers (1 set = 1 solution)
708
709
710
            # Equivalent of wrapping each previous solution with a logical OR:
            # OR( not (frontier places))
            ## TODO: check in unfolder: dim_start elements joined by OR or AND operator ?
711
712
713
            ## TODO: keep previous dim_start à la première itération (mettre le contenu dans forbidden values)
            query.dim_start = list(forbidden_frontier_values)
            print("query variant prop", query.variant_prop)
714
            ## TODO: equivaut à mettre à jour le start_prop ou __initial_property avec l'ancienne méthode ??
715
716
717
718
719
            ## si non, faudrait ptetre éviter de recompiler ça à chaque fois dans __init_initial_constraint_0
            #### redondance code next_mac()
            # Solutions differ on frontiers: Search only 2 different solutions
            # to avoid all activated solutions
            # Get <tuple <DimacsFrontierSol>>
720
721
722
723
724
            dimacs_front_sol = self.__sq_dimacs_frontier_solutions(query, min_step, 2)
            if not dimacs_front_sol:
                # If we do not want to self-adjust steps, just break the loop
                # break

725
726
                LOGGER.info("MCLA: NOT FOUND -> satis test; current step %s",
                            self.unfolder.get_current_step())
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
                if self.unfolder.get_current_step() + 1 > max_user_step:
                    # Cosmetic break, avoid to do useless test
                    break

                ## TEST
                ## Make autoadjustment... of max_steps during the solving
                ## Juste appeler squery_solve avec les memes parametres mais
                ## min_step augmenté de 1
                ## en restant inférieur au nb d'étapes demandées à l'origine
                ## => on bénéficie des shifts précédents et on évite de reconstruire le problème...

                # Hack: reuse the current Unfolder (without init with query)
                # => do not do this at home!
                self.unfolder._CLUnfolder__locked = False
                # Avoid a new test of satisfiability on the same current_step
                # (we already know that there is no more solution for it)
                # => increment __steps_before_check
                self.unfolder._CLUnfolder__steps_before_check += 1
                ret = self.unfolder.squery_is_satisfied(max_user_step)
                if not ret:
                    # The problem is definitly not satisfiable in the given
                    # number of steps
                    break
                # __steps_before_check can't be >= min_step
                # (see squery_is_satisfied() and squery_solve())
                min_step = self.unfolder.get_current_step()
                query.steps_before_check = min_step - 1

                print("testing AUTO CORRECT max step:", min_step)
                continue

758

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

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

766
767
768
769
770
771
772
773
774
            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]
            )
775
776
777
778
            LOGGER.debug(
                "MCLA::mac_exhaustive_search: forbidden frontiers: %s",
                forbidden_frontier_values
            )
779

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

783
784
785
786
787
788
789
        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.

        ---

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

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

803
804
        :param max_step: Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
805
        :type query: <MCLSimpleQuery>
806
        :type max_step: <int>
807
808
        :return: A FrontierSolution which is a wrapper of a symbolic
            representation of frontier values and timings from a raw solution.
809
810
811
812
813
814
815
        :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:
816
            return
817

818
819
820
821
822
823
824
825
826
827
828
        # 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
829
830
        """Wrapper for __mac_exhaustive_search(); return a generator of
        FrontierSolution objects.
831
832

        ..note:: __mac_exhaustive_search() returns DimacsFrontierSols
833

834
        @param query: MCLSimpleQuery
835
836
        @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
837
        @return: <generator <FrontierSolution>>
VIGNET Pierre's avatar
VIGNET Pierre committed
838
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
839
840
        ## TODO convert start_property in dim_start !! => eviter la recompilation des propriétés
        # Get <generator <DimacsFrontierSol>>
841
        mac_list = self.__mac_exhaustive_search(query, max_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
842
        # Convert to a generator of FrontierSolution objects
843
844
845
846
847
        #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 ##############################################################
848

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

852
853
        ..refactor note: Unclear function

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

        @return: False if the problem is satisfiable, True otherwise
VIGNET Pierre's avatar
VIGNET Pierre committed
859
        @param act_sol: FrontierSolution with activation condition
860
        @param query: the query used for act_sol condition
VIGNET Pierre's avatar
VIGNET Pierre committed
861
        """
862
863
864
865
866
867
868
869
870
871
872
        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
873
        query_2 = MCLSimpleQuery(None, inv_prop, None)
874
875
876
        #(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
877
        query_1 = query_2.merge(query_1)
878
879
880
881
882
883
        #(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))

884

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
894
        @param mac: FrontierSolution
895
        @param query: MCLSimpleQuery
896
        @param max_step: int - number of dynamical step
VIGNET Pierre's avatar
VIGNET Pierre committed
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
        @return: a list of variables (list<string>)
        """
        # query with mac init frontier places and  timing
        inh_query1 = MCLSimpleQuery.from_frontier_sol_same_timing(mac,
                                                                  self.unfolder)
        # 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:
            inv_prop = query.inv_prop + "and (not (" + query.final_prop +"))"
        inh_query2 = MCLSimpleQuery(None, inv_prop, None)
        # init + timing + final property not reachable
        inh_query = inh_query1.merge(inh_query2)
912
913
        max_step = len(inh_query.variant_prop)
        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
921


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

925
926
        ..refactor note: Unclear function

VIGNET Pierre's avatar
VIGNET Pierre committed
927
928
929
930
        @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
931

VIGNET Pierre's avatar
VIGNET Pierre committed
932
933
934
935
936
937
938
939
940
941
942
943
944
945
        @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:
            inv_prop = query.inv_prop + "and (not (" + query.final_prop +"))"
        inh_query2 = MCLSimpleQuery(None, inv_prop, None)
        # init + timing + final property not reachable
        inh_query = inh_query1.merge(inh_query2)
946

947
948
        max_step = len(inh_query.variant_prop)
        assert(max_step == len(mac.ic_sequence))
VIGNET Pierre's avatar
VIGNET Pierre committed
949
950
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
951
952
#        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
953
954
955
956
        self.unfolder.set_include_aux_clauses(True)
        return lsol

    def is_strong_inhibitor(self, in_sol, query):
957
        """Test if an activation condition inhibitor is a strong one
VIGNET Pierre's avatar
VIGNET Pierre committed
958
        (i.e independent of timing)
959

960
961
        ..refactor note: Unclear function

VIGNET Pierre's avatar
VIGNET Pierre committed
962
963
964
        @param in_sol: FrontierSolution with activation condition and inhibition
        @param query: the property which is inhibed
        """
965
966
967
968
        max_step = len(in_sol.ic_sequence) - 1

        # New timings, force inactivated frontiers
        query_1 = MCLSimpleQuery.from_frontier_sol_new_timing(in_sol, self.unfolder)
VIGNET Pierre's avatar
VIGNET Pierre committed
969
970
971
972
973
974
975
976
977
        # negation of the query
        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:
            inv_prop = query.inv_prop + "and (not (" + query.final_prop +"))"
        inh_query = MCLSimpleQuery(None, inv_prop, None)
        query_1 = inh_query.merge(query_1)
978
        return not self.sq_is_satisfiable(query_1, max_step)
979