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 41.5 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
198
from cadbiom import commons as cm
LOGGER = cm.logger()

VIGNET Pierre's avatar
VIGNET Pierre committed
199
200

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

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

223
224
225
226
        :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>
227
        :type nb_sols_to_be_pruned: 10
VIGNET Pierre's avatar
VIGNET Pierre committed
228
    """
229

VIGNET Pierre's avatar
VIGNET Pierre committed
230
    def __init__(self, report):
231
232
        """The built analyser is void by default

VIGNET Pierre's avatar
VIGNET Pierre committed
233
234
        @param report: a standard reporter
        """
235
        self.unfolder = None       # computation management: unfolding; type <CLUnfolder>
VIGNET Pierre's avatar
VIGNET Pierre committed
236
        self.reporter = report     # for generic error display
237
238
239
240
241
242
243
244
        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

245
246
247
248
249
    @property
    def dynamical_system(self):
        """Return the CLDynSys object of the current unfolder"""
        return self.unfolder.dynamical_system

250
    ## Building MCLAnalyser ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
251
252

    def build_from_chart_model(self, model):
253
        """Build an MCLAnalyser and its CLUnfolder from a chartmodel object.
254
255
256

        Every parser uses this function at the end.

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

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

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

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

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

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

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

319
    ## Solutions processing ####################################################
320

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

        ..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
332
        """
333
334
335
336
        # 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))]
337
338


339
340
341
342
343
    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`).
344

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

369
370
371
372
        # 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

373
374
        # Must return fsol even if there is no more solution (search first 10 sols)
        # Get <tuple <DimacsFrontierSol>>
375
        return self.__sq_dimacs_frontier_solutions(query, max_step, max_sol)
376
377
378


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

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

        Repeat the operation until there is only one solution.
388
389

        :type fsol: <DimacsFrontierSol>
390
391
        :type query: <MCLSimpleQuery>
        :rtype: <DimacsFrontierSol>
392

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

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

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

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

441
    ## Generic solver for simple queries #######################################
442

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

446
447
448
449
        ..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
450

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

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


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

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

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

        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:

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


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

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

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


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

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

545
546
547
548
        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
549

550
551
552
        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
553

554
        This function is a wrapper of sq_solutions().
555

VIGNET Pierre's avatar
VIGNET Pierre committed
556

557
558
559
560
        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.
561

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

566
567
568
        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.
569

570
571
        @warning: no frontier places are initialized to False

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

VIGNET Pierre's avatar
VIGNET Pierre committed
587

588
589
    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
590

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

595
        @param query: MCLSimpleQuery
596
597
598
599
600
        @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.
601
            .. note:: Unicity is based on the set of activated frontier values.
602
603
604
605
606
607
608
609
610
611
        :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
612
613


614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
    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;
641
            the horizon on which the properties must be satisfied
642
643
644
645
646
647
        :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
648
        """
649
        # list of timed minimal activation conditions on frontier (dimacs code)
VIGNET Pierre's avatar
VIGNET Pierre committed
650
        # i.e list<DimacsFrontierSol>
651
        # mac_list = [] # Not used anymore
652
        forbidden_frontier_values = []
653

654
655
656
657
658
        ## 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
659
660
        reachable = self.sq_is_satisfiable(query, max_user_step)

661
662
663
664
665
666
667
668
669
        # 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)
670

671
        while reachable:
672
673
            # Forbidden solutions: already discovered macs (see at the end of the while loop)
            # Ban all sets of activated frontiers (1 set = 1 solution)
674
675
676
            # 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 ?
677
678
679
            ## 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)
680
            ## TODO: equivaut à mettre à jour le start_prop ou __initial_property avec l'ancienne méthode ??
681
682
683
684
685
            ## 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>>
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
            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

                print("NOT FOUND - current step ?", self.unfolder.get_current_step())
                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

723

724
            # Get the solution with the less number of activated states
725
            small_fsol = self.less_activated_solution(dimacs_front_sol)
726
727
728

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

            ## TEST
732
            print("__mac_exhaustive_search:: final current step ?", self.unfolder.get_current_step())
733
734
735


            if current_mac.nb_activated_frontiers == 0:
736
                # Condition that seems to be never reached..
737
                print("NOT REACHABLE")
VIGNET Pierre's avatar
VIGNET Pierre committed
738
                reachable = False
739
740
            else:
                yield current_mac
741
                # mac_list.append(current_mac)
742
743
744
745
746
747
748

                # 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]
                )
749

750
751
752
    def next_mac(self, query, max_step):
        """Search a Minimal Access Condition for the given query.

753
754
755
756
757
758
759
        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.

        ---

760
761
        On cherche ensuite d'abord des solutions non minimales (actuellement 2) via:
        self.__sq_dimacs_frontier_solutions(query, nb_step, 2)
762

763
764
765
766
767
768
769
770
771
        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).
772

773
774
        :param max_step: Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
775
        :type query: <MCLSimpleQuery>
776
        :type max_step: <int>
777
778
        :return: A FrontierSolution which is a wrapper of a symbolic
            representation of frontier values and timings from a raw solution.
779
780
781
782
783
784
785
        :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:
786
            return
787

788
789
790
791
792
793
794
795
796
797
798
        # 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
799
800
        """Wrapper for __mac_exhaustive_search(); return a generator of
        FrontierSolution objects.
801
802

        ..note:: __mac_exhaustive_search() returns DimacsFrontierSols
803

804
        @param query: MCLSimpleQuery
805
806
        @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
807
        @return: <generator <FrontierSolution>>
VIGNET Pierre's avatar
VIGNET Pierre committed
808
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
809
810
        ## TODO convert start_property in dim_start !! => eviter la recompilation des propriétés
        # Get <generator <DimacsFrontierSol>>
811
        mac_list = self.__mac_exhaustive_search(query, max_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
812
        # Convert to a generator of FrontierSolution objects
813
814
815
816
817
        #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 ##############################################################
818

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

822
823
        ..refactor note: Unclear function

824
825
        final property becomes the invariant property
        => Ex: test if "C3 and C4" will never append if start property is "A1 and C1 and B1"
826
        Cf TestMCLAnalyser...
827
828

        @return: False if the problem is satisfiable, True otherwise
VIGNET Pierre's avatar
VIGNET Pierre committed
829
        @param act_sol: FrontierSolution with activation condition
830
        @param query: the query used for act_sol condition
VIGNET Pierre's avatar
VIGNET Pierre committed
831
        """
832
833
834
835
836
837
838
839
840
841
842
        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
843
        query_2 = MCLSimpleQuery(None, inv_prop, None)
844
845
846
        #(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
847
        query_1 = query_2.merge(query_1)
848
849
850
851
852
853
        #(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))

854

VIGNET Pierre's avatar
VIGNET Pierre committed
855
856
    def next_inhibitor(self, mac, query):
        """
857
858
        ..refactor note: Unclear function

859
        if st_prop contains negation of mac conditions,
VIGNET Pierre's avatar
VIGNET Pierre committed
860
861
862
        return a different mac if any
        same parameters as __mac_exhaustive_search
        Used for search on cluster
863

VIGNET Pierre's avatar
VIGNET Pierre committed
864
        @param mac: FrontierSolution
865
        @param query: MCLSimpleQuery
866
        @param max_step: int - number of dynamical step
VIGNET Pierre's avatar
VIGNET Pierre committed
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
        @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)
882
883
        max_step = len(inh_query.variant_prop)
        assert(max_step == len(mac.ic_sequence))
884

VIGNET Pierre's avatar
VIGNET Pierre committed
885
886
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
887
        next_inhib = self.next_mac(inh_query, max_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
888
889
        self.unfolder.set_include_aux_clauses(True)
        return next_inhib
890
891


VIGNET Pierre's avatar
VIGNET Pierre committed
892
    def mac_inhibitor_search(self, mac, query, max_sol):
893
        """Search inhibitors for a mac scenario
894

895
896
        ..refactor note: Unclear function

VIGNET Pierre's avatar
VIGNET Pierre committed
897
898
899
900
        @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
901

VIGNET Pierre's avatar
VIGNET Pierre committed
902
903
904
905
906
907
908
909
910
911
912
913
914
915
        @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)
916

917
918
        max_step = len(inh_query.variant_prop)
        assert(max_step == len(mac.ic_sequence))
VIGNET Pierre's avatar
VIGNET Pierre committed
919
920
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
921
922
#        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
923
924
925
926
        self.unfolder.set_include_aux_clauses(True)
        return lsol

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

930
931
        ..refactor note: Unclear function

VIGNET Pierre's avatar
VIGNET Pierre committed
932
933
934
        @param in_sol: FrontierSolution with activation condition and inhibition
        @param query: the property which is inhibed
        """
935
936
937
938
        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
939
940
941
942
943
944
945
946
947
        # 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)
948
        return not self.sq_is_satisfiable(query_1, max_step)
949