Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

MCLAnalyser.py 37 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
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

## 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
173
"""
174
175
from __future__ import print_function

176
from antlr3 import ANTLRFileStream, CommonTokenStream
VIGNET Pierre's avatar
VIGNET Pierre committed
177

178
from cadbiom.models.guard_transitions.translators.chart_xml import \
VIGNET Pierre's avatar
VIGNET Pierre committed
179
        MakeModelFromXmlFile
180
181

from cadbiom.models.guard_transitions.translators.chart_xml_pid import \
VIGNET Pierre's avatar
VIGNET Pierre committed
182
        MakeModelFromPidFile
183
184
185
186

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
187
from cadbiom.models.clause_constraints.mcl.MCLSolutions import MCLException
188
189
190
191
192

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
193
from cadbiom.models.clause_constraints.mcl.MCLSolutions import FrontierSolution, DimacsFrontierSol
194
from cadbiom.models.clause_constraints.mcl.MCLQuery import MCLSimpleQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
195
196
197


class MCLAnalyser(object):
198
199
200
201
202
203
204
205
206
207
208
209
210
    """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:

211
        :param dynamical_system: dynamical system in clause constraint form
212
213
214
215
216
217
218
219
        :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.

220
221
222
223
        :type dynamical_system: None before loading a model / <CLDynSys>
        :type unfolder: None before loading a model / <CLUnfolder>
        :type reporter: <ErrorRep>
        :type translator_opti: True / <boolean>
224
        :type nb_sols_to_be_pruned: 10
VIGNET Pierre's avatar
VIGNET Pierre committed
225
    """
226

VIGNET Pierre's avatar
VIGNET Pierre committed
227
    def __init__(self, report):
228
229
        """The built analyser is void by default

VIGNET Pierre's avatar
VIGNET Pierre committed
230
231
        @param report: a standard reporter
        """
232
        self.unfolder = None       # computation management: unfolding; type <CLUnfolder>
VIGNET Pierre's avatar
VIGNET Pierre committed
233
        self.reporter = report     # for generic error display
234
235
236
237
238
239
240
241
        self.translator_opti = True# turn on optimizations for ANTLR translation (subexpression elimination)

        # 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

242
243
244
245
246
    @property
    def dynamical_system(self):
        """Return the CLDynSys object of the current unfolder"""
        return self.unfolder.dynamical_system

247
    ## Building MCLAnalyser ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
248
249

    def build_from_chart_model(self, model):
250
        """Build an MCLAnalyser and its CLUnfolder from a chartmodel object.
251
252
253

        Every parser uses this function at the end.

254
        @param model: <ChartModel>
VIGNET Pierre's avatar
VIGNET Pierre committed
255
        """
256
        # Reloading a MCLAnalyser is forbidden - create a new one is mandatory
VIGNET Pierre's avatar
VIGNET Pierre committed
257
258
        if self.unfolder:
            raise MCLException("This MCLAnalyser is already initialized")
259
260

        # Build CLDynSys (dynamical system in clause constraint form)
261
        # Parse the model data
262
        vtab = TableVisitor(self.reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
263
264
265
        model.accept(vtab)
        if self.reporter.error:
            return
266
267
268
        # PS:
        # Here, all keys of vtab.tab_symb = no_frontiers + frontiers + model name
        # (probably a bug for this last one)
269
        dynamic_system = CLDynSys(vtab.tab_symb, self.reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
270
271
        if self.reporter.error:
            return
272
        # Build clauses and auxiliary variables from events and places in the model
273
        comp_visitor = GT2Clauses(dynamic_system, self.reporter, self.translator_opti)
VIGNET Pierre's avatar
VIGNET Pierre committed
274
275
276
        model.accept(comp_visitor)
        if self.reporter.error:
            return
277
278
        # Build unfolder
        self.unfolder = CLUnfolder(dynamic_system)
VIGNET Pierre's avatar
VIGNET Pierre committed
279
280

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

VIGNET Pierre's avatar
VIGNET Pierre committed
283
284
285
286
        @param file_name: str - path of the .bcx file
        """
        parsing = MakeModelFromXmlFile(file_name)
        # chart model
287
288
289
290
        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
291
292
293

        @param file_name: str - path of .xml file
        """
294
295
296
        parsing = MakeModelFromPidFile(
            file_name, self.reporter, has_clock, ai_interpretation
        )
VIGNET Pierre's avatar
VIGNET Pierre committed
297
        # chart model
298
        self.build_from_chart_model(parsing.get_model())
299

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

VIGNET Pierre's avatar
VIGNET Pierre committed
303
304
305
306
        @param file_name: str - path of .cal file
        """
        creporter = self.reporter
        fstream = ANTLRFileStream(file_name)
307
        lexer = cadlangLexer(fstream)
VIGNET Pierre's avatar
VIGNET Pierre committed
308
309
310
311
312
313
        lexer.set_error_reporter(creporter)
        parser = cadlangParser(CommonTokenStream(lexer))
        parser.set_error_reporter(creporter)
        model = ChartModel(file_name)
        parser.cad_model(model)
        # chart model
314
        self.build_from_chart_model(parser.model)
VIGNET Pierre's avatar
VIGNET Pierre committed
315

316
    ## Solutions processing ####################################################
317

VIGNET Pierre's avatar
VIGNET Pierre committed
318
    def less_activated_solution(self, dimacs_solution_list):
319
320
        """Get the solution with the less number of activated frontier places
        among the given solutions.
321
322
323
324
325
326
327
328

        ..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
329
        """
330
331
332
333
        # Count the number of activated places in each solution
        nb_activated = [sol.nb_activated_frontiers for sol in dimacs_solution_list]
        print("nb_activated per dimacs fronts sols", nb_activated)
        return dimacs_solution_list[nb_activated.index(min(nb_activated))]
334
335


336
337
338
339
340
    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`).
341

342
343
344
        :param dimacs_front_sol: A solution to obtain the property.
        :param query: Current query
        :param max_step: Number of steps allowed in the unfolding;
345
            the horizon on which the properties must be satisfied
346
347
348
349
350
351
352
353
354
        :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
355
        """
356
        # Collect inactivated frontier places
357
        # OLD:
358
359
        # inactive_frontier_values = \
        #     [[var] for var in dimacs_front_sol.frontier_values if var < 0]
360
361
        # Intersection between pre-computed negative values for all frontiers
        # and all frontiers (negative and positive) in the given solution
362
        inactive_frontier_values = \
363
            [[var] for var in
364
             self.unfolder.frontiers_negative_values & dimacs_front_sol.frontier_values]
365

366
367
        # Prepend inactivated frontier places as a start property in DIMACS form
        if query.dim_start:
368
            query.dim_start = inactive_frontier_values + query.dim_start
369
        else:
370
            query.dim_start = inactive_frontier_values
371
372
        # Must return fsol even if there is no more solution (search first 10 sols)
        # Get <tuple <DimacsFrontierSol>>
373
        return self.__sq_dimacs_frontier_solutions(query, max_step, max_sol)
374
375
376


    def __prune_frontier_solution(self, fsol, query, max_step):
377
378
379
380
        """"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".

381
        Find at most `nb_sols_to_be_pruned` frontier solutions inducing
382
383
384
385
        the same final property but with all inactivated frontier places
        forced to be initially False.

        Repeat the operation until there is only one solution.
386
387

        :type fsol: <DimacsFrontierSol>
388
389
        :type query: <MCLSimpleQuery>
        :rtype: <DimacsFrontierSol>
390

VIGNET Pierre's avatar
VIGNET Pierre committed
391
392
        ASSERT: fsol is a frontier condition implying sq satisfiability
        """
393
394
395
396
397
398
        # 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
399
400
        next_len = 0
        is_pruned = True
401

402
        i = 0
VIGNET Pierre's avatar
VIGNET Pierre committed
403
        while is_pruned:
404
            i += 1
405
406
407
            # 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.
408
409
410
411
412
413
414
415
416
417
418
419
420
421
            # 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
                )
            print("iteration", i, "nb pruned inact solutions", len(dimacs_solutions))
            ####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
422
            if len(dimacs_solutions) == 1:
423
424
                # No new solution has been found,
                # the current solution is the best (sol_to_prune)
425
                return dimacs_solutions[0] # it's sol_to_prune variable
426
427
428
429
430

            # 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
431
432
            is_pruned = current_len > next_len
            if is_pruned:
433
                sol_to_prune = next_sol
VIGNET Pierre's avatar
VIGNET Pierre committed
434
                current_len = next_len
435

VIGNET Pierre's avatar
VIGNET Pierre committed
436
        # never reach this point
437
        raise MCLException("MCLAnalyser:__prune_frontier_solution:: what happened??")
438

439
    ## Generic solver for simple queries #######################################
440

VIGNET Pierre's avatar
VIGNET Pierre committed
441
    def sq_is_satisfiable(self, query, max_step):
442
443
        """Check if the query is satisfiable.

444
445
446
447
        ..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
448

449
450
            **These variables of interest are not checked here!**
                It is just a satisfiability test!
451

452
453
454
455
456
        ..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
457
        :type query: <MCLSimpleQuery>
458
459
        :type max_step: <int>
        :rtype: <boolean>
VIGNET Pierre's avatar
VIGNET Pierre committed
460
        """
461
462
463
        # 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,
464
        #    variant_prop, dim_variant_prop, steps_before_check
465
        self.unfolder.init_with_query(query)
VIGNET Pierre's avatar
VIGNET Pierre committed
466
467
        # go
        return self.unfolder.squery_is_satisfied(max_step)
468
469


VIGNET Pierre's avatar
VIGNET Pierre committed
470
    def sq_solutions(self, query, max_step, max_sol, vvars):
471
472
473
474
        """Return a list of RawSolution objects

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

475
476
        Parameters are the same as in sq_is_satisfiable() except for vvars
        parameter which deserves some explanations.
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495

        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:

496
            - frontier_pos_and_neg_values:
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
                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.


512
        @param query: MCLSimpleQuery
513
514
        @param max_step: int - Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
515
516
517
518
        :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>>
519
520
        :return: a list of RawSolutions from the solver
        :rtype: <list <RawSolution>>
521
522

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

VIGNET Pierre's avatar
VIGNET Pierre committed
525
526
527
        @warning: if the query includes variant constraints, the horizon (max_step) is
            automatically adjusted to min(max_step, len(variant_constraints)).
        """
528
529
530
        # 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,
531
        #    variant_prop, dim_variant_prop, steps_before_check
532
        self.unfolder.init_with_query(query)
VIGNET Pierre's avatar
VIGNET Pierre committed
533
534
        # go
        return self.unfolder.squery_solve(vvars, max_step, max_sol)
535
536


VIGNET Pierre's avatar
VIGNET Pierre committed
537
    def sq_frontier_solutions(self, query, max_step, max_sol):
538
        """Compute active frontier places and timings
539

540
541
        Compute the set of frontier place names which must be activated for
        implying query satisfaction and returned it as a list of FrontierSolution.
542

543
544
545
546
        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
547

548
549
550
        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
551

552
        This function is a wrapper of sq_solutions().
553

VIGNET Pierre's avatar
VIGNET Pierre committed
554

555
556
557
558
        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.
559

560
561
562
            - The second important attribute is ic_sequence, a list of strings
            which describes the successive activated inputs and free events in
            the solution.
563

564
565
566
        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.
567

568
569
        @warning: no frontier places are initialized to False

570
        @param query: MCLSimpleQuery
571
572
573
574
575
576
577
        @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
578
        """
579
580
581
582
583
        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
584

VIGNET Pierre's avatar
VIGNET Pierre committed
585

586
587
    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
588

589
590
        DimacsFrontierSol objects provides some interesting attributes like:
        activated_frontier_values (raw values of literals).
591
        Note: FrontierSolution are of higher level without such attributes.
592

593
        @param query: MCLSimpleQuery
594
595
596
597
598
        @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.
599
            .. note:: Unicity is based on the set of activated frontier values.
600
601
602
603
604
605
606
607
608
609
        :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)
        print("Taille dimacsfrontsol", [len(sol) for sol in dimacfrontsol])
        print("Nombre demande:", max_sol, "steps", max_step, "obtenu", len(dimacfrontsol))
        return dimacfrontsol
610
611


612
    def __mac_exhaustive_search(self, query, max_step):
VIGNET Pierre's avatar
VIGNET Pierre committed
613
        """
614
        @param query: MCLQuery
615
616
        @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
617
        @return: <generator <FrontierSolution>>
VIGNET Pierre's avatar
VIGNET Pierre committed
618
        """
619
        # list of timed minimal activation conditions on frontier (dimacs code)
VIGNET Pierre's avatar
VIGNET Pierre committed
620
        # i.e list<DimacsFrontierSol>
621
        mac_list = []
622
        forbidden_frontier_values = []
623

VIGNET Pierre's avatar
VIGNET Pierre committed
624
625
        reachable = self.sq_is_satisfiable(query, max_user_step)

VIGNET Pierre's avatar
VIGNET Pierre committed
626
        # get the minimum number of steps for reachability
627
        # set number of shifts before testing final prop
VIGNET Pierre's avatar
VIGNET Pierre committed
628
629
        min_step = self.unfolder.get_current_step() - 1
        query.set_steps_before_reach(min_step)
630

631
        while reachable:
632
633
            # Forbidden solutions: already discovered macs (see at the end of the while loop)
            # Ban all sets of activated frontiers (1 set = 1 solution)
634
635
636
            # 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 ?
637
            print("forbidden_frontier_values", forbidden_frontier_values)
638

639
640
            query.dim_start = forbidden_frontier_values
            ## TODO: equivaut à mettre à jour le start_prop ou __initial_property avec l'ancienne méthode ??
641
642
643
644
645
646
647
            ## 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>>
            lfsol = self.__sq_dimacs_frontier_solutions(query, max_step, 2)
            if not lfsol:
VIGNET Pierre's avatar
VIGNET Pierre committed
648
                break
649

650
651
652
653
654
655
656
657
658
659
660
661
662
            # 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)

            ## TEST
            print("final current step ?", self.unfolder.get_current_step())


            if current_mac.nb_activated_frontiers == 0:
                print("NOT REACHABLE")
VIGNET Pierre's avatar
VIGNET Pierre committed
663
                reachable = False
664
665
            else:
                yield current_mac
VIGNET Pierre's avatar
VIGNET Pierre committed
666
                mac_list.append(current_mac)
667
668
669
670
671
672
673

                # 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]
                )
674
675


676
677
678
    def next_mac(self, query, max_step):
        """Search a Minimal Access Condition for the given query.

679
680
681
682
683
684
685
        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.

        ---

686
687
        On cherche ensuite d'abord des solutions non minimales (actuellement 2) via:
        self.__sq_dimacs_frontier_solutions(query, nb_step, 2)
688

689
690
691
692
693
694
695
696
697
        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).
698

699
700
        :param max_step: Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
701
        :type query: <MCLSimpleQuery>
702
        :type max_step: <int>
703
704
        :return: A FrontierSolution which is a wrapper of a symbolic
            representation of frontier values and timings from a raw solution.
705
706
707
708
709
710
711
        :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:
712
            return
713

714
715
716
717
718
719
720
721
722
723
724
        # 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
725
726
        """Wrapper for __mac_exhaustive_search(); return a generator of
        FrontierSolution objects.
727
728

        ..note:: __mac_exhaustive_search() returns DimacsFrontierSols
729

730
        @param query: MCLSimpleQuery
731
732
        @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
733
        @return: <generator <FrontierSolution>>
VIGNET Pierre's avatar
VIGNET Pierre committed
734
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
735
736
        ## TODO convert start_property in dim_start !! => eviter la recompilation des propriétés
        # Get <generator <DimacsFrontierSol>>
737
        mac_list = self.__mac_exhaustive_search(query, max_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
738
        # Convert to a generator of FrontierSolution objects
739
740
741
742
743
        #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 ##############################################################
744

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

748
749
        ..refactor note: Unclear function

750
751
752
753
        final property becomes the invariant property
        => Ex: test if "C3 and C4" will never append if start property is "A1 and C1 and B1"

        @return: False if the problem is satisfiable, True otherwise
VIGNET Pierre's avatar
VIGNET Pierre committed
754
        @param act_sol: FrontierSolution with activation condition
755
        @param query: the query used for act_sol condition
VIGNET Pierre's avatar
VIGNET Pierre committed
756
757
        """
        nb_step = len(act_sol.ic_sequence) - 1
758
        query_1 = MCLSimpleQuery.from_frontier_sol_same_timing(act_sol,
759
                                                               self.unfolder)
VIGNET Pierre's avatar
VIGNET Pierre committed
760
761
762
763
        inv_prop = 'not('+query.final_prop+')'
        query_2 = MCLSimpleQuery(None, inv_prop, None)
        query_1 = query_2.merge(query_1)
        return not(self.sq_is_satisfiable(query_1, nb_step))
764

VIGNET Pierre's avatar
VIGNET Pierre committed
765
766
    def next_inhibitor(self, mac, query):
        """
767
768
        ..refactor note: Unclear function

769
        if st_prop contains negation of mac conditions,
VIGNET Pierre's avatar
VIGNET Pierre committed
770
771
772
        return a different mac if any
        same parameters as __mac_exhaustive_search
        Used for search on cluster
773

VIGNET Pierre's avatar
VIGNET Pierre committed
774
        @param mac: FrontierSolution
775
        @param query: MCLSimpleQuery
776
        @param max_step: int - number of dynamical step
VIGNET Pierre's avatar
VIGNET Pierre committed
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
        @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)
792
793
        max_step = len(inh_query.variant_prop)
        assert(max_step == len(mac.ic_sequence))
794

VIGNET Pierre's avatar
VIGNET Pierre committed
795
796
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
797
        next_inhib = self.next_mac(inh_query, max_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
798
799
        self.unfolder.set_include_aux_clauses(True)
        return next_inhib
800
801


VIGNET Pierre's avatar
VIGNET Pierre committed
802
    def mac_inhibitor_search(self, mac, query, max_sol):
803
        """Search inhibitors for a mac scenario
804

805
806
        ..refactor note: Unclear function

VIGNET Pierre's avatar
VIGNET Pierre committed
807
808
809
810
        @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
811

VIGNET Pierre's avatar
VIGNET Pierre committed
812
813
814
815
816
817
818
819
820
821
822
823
824
825
        @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)
826

827
828
        max_step = len(inh_query.variant_prop)
        assert(max_step == len(mac.ic_sequence))
VIGNET Pierre's avatar
VIGNET Pierre committed
829
830
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
831
832
#        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
833
834
835
836
        self.unfolder.set_include_aux_clauses(True)
        return lsol

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

840
841
        ..refactor note: Unclear function

VIGNET Pierre's avatar
VIGNET Pierre committed
842
843
844
        @param in_sol: FrontierSolution with activation condition and inhibition
        @param query: the property which is inhibed
        """
845
846
847
848
        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
849
850
851
852
853
854
855
856
857
        # 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)
858
        return not self.sq_is_satisfiable(query_1, max_step)
859