MCLAnalyser.py 30 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
44
##
## Contributor(s): Geoffroy Andrieux - IRISA/IRSET
##
"""
Main class to perform dynamic analysis of Cadbiom chart models.
"""
45
46
from __future__ import print_function

47
from antlr3 import ANTLRFileStream, CommonTokenStream
VIGNET Pierre's avatar
VIGNET Pierre committed
48

49
from cadbiom.models.guard_transitions.translators.chart_xml import \
VIGNET Pierre's avatar
VIGNET Pierre committed
50
        MakeModelFromXmlFile
51
52

from cadbiom.models.guard_transitions.translators.chart_xml_pid import \
VIGNET Pierre's avatar
VIGNET Pierre committed
53
        MakeModelFromPidFile
54
55
56
57

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
58
from cadbiom.models.clause_constraints.mcl.MCLSolutions import MCLException
59
60
61
62
63

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
64
from cadbiom.models.clause_constraints.mcl.MCLSolutions import FrontierSolution, DimacsFrontierSol
65
from cadbiom.models.clause_constraints.mcl.MCLQuery import MCLSimpleQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
66
67
68


class MCLAnalyser(object):
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
    """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:

        :param cl_dyn_sys: dynamical system in clause constraint form
        :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.

        :type cl_dyn_sys: None / <CLDynSys>
        :type unfolder: None / <CLUnfolder>
        :type reporter: no default value / <ErrorRep>
        :type opti: True / <boolean>
        :type nb_sols_to_be_pruned: 10
VIGNET Pierre's avatar
VIGNET Pierre committed
96
    """
97

VIGNET Pierre's avatar
VIGNET Pierre committed
98
    def __init__(self, report):
99
100
        """The built analyser is void by default

VIGNET Pierre's avatar
VIGNET Pierre committed
101
102
103
        @param report: a standard reporter
        """
        self.cl_dyn_sys = None     # dynamical system in clause constraint form
104
        self.unfolder = None       # computation management: unfolding; type <CLUnfolder>
VIGNET Pierre's avatar
VIGNET Pierre committed
105
        self.reporter = report     # for generic error display
106
107
108
109
110
111
112
113
114
        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

    ## Building MCLAnalyser ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
115
116

    def build_from_chart_model(self, model):
117
118
119
120
121
        """Build an MCLAnalyser from a chartmodel object.

        Every parser uses this function at the end.

        @param model: ChartModel
VIGNET Pierre's avatar
VIGNET Pierre committed
122
        """
123
        # Reloading a MCLAnalyser is forbidden - create a new one is mandatory
VIGNET Pierre's avatar
VIGNET Pierre committed
124
125
        if self.unfolder:
            raise MCLException("This MCLAnalyser is already initialized")
126
127

        # Build CLDynSys (dynamical system in clause constraint form)
128
        vtab = TableVisitor(self.reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
129
130
131
        model.accept(vtab)
        if self.reporter.error:
            return
132
        dynamic_system = CLDynSys(vtab.tab_symb, self.reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
133
134
        if self.reporter.error:
            return
135
        comp_visitor = GT2Clauses(dynamic_system, self.reporter, self.translator_opti)
VIGNET Pierre's avatar
VIGNET Pierre committed
136
137
138
        model.accept(comp_visitor)
        if self.reporter.error:
            return
139
        self.cl_dyn_sys = dynamic_system
140

141
142
        # Build unfolder
        self.unfolder = CLUnfolder(dynamic_system)
VIGNET Pierre's avatar
VIGNET Pierre committed
143
144

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

VIGNET Pierre's avatar
VIGNET Pierre committed
147
148
149
150
        @param file_name: str - path of the .bcx file
        """
        parsing = MakeModelFromXmlFile(file_name)
        # chart model
151
152
153
154
        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
155
156
157

        @param file_name: str - path of .xml file
        """
158
159
160
        parsing = MakeModelFromPidFile(
            file_name, self.reporter, has_clock, ai_interpretation
        )
VIGNET Pierre's avatar
VIGNET Pierre committed
161
        # chart model
162
        self.build_from_chart_model(parsing.get_model())
163

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

VIGNET Pierre's avatar
VIGNET Pierre committed
167
168
169
170
        @param file_name: str - path of .cal file
        """
        creporter = self.reporter
        fstream = ANTLRFileStream(file_name)
171
        lexer = cadlangLexer(fstream)
VIGNET Pierre's avatar
VIGNET Pierre committed
172
173
174
175
176
177
        lexer.set_error_reporter(creporter)
        parser = cadlangParser(CommonTokenStream(lexer))
        parser.set_error_reporter(creporter)
        model = ChartModel(file_name)
        parser.cad_model(model)
        # chart model
178
        self.build_from_chart_model(parser.model)
VIGNET Pierre's avatar
VIGNET Pierre committed
179

180
    ## Solutions processing ####################################################
181

VIGNET Pierre's avatar
VIGNET Pierre committed
182
    def less_activated_solution(self, dimacs_solution_list):
183
184
185
186
187
188
189
190
191
192
        """Get the solution with the less number of activated
        states among the given solutions.

        ..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
193
194
195
        """
        if not dimacs_solution_list:
            self.reporter.display(
196
197
                "Trying to find a smallest solution without solution list"
            )
VIGNET Pierre's avatar
VIGNET Pierre committed
198
199
            return None

200
201
202
203
        # 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))]
204
205


206
207
208
209
210
211
212
213
214
215
216
217
218
219
    def __solve_with_inact_fsolution(self, fsolution, query, max_step, max_sols):
        """Frontier states not activated in fsolution (frontier solution)
        are **forced to be False at start**; solve this and return first frontier
        solutions list with this constraint (this number is defined in the
        argument: max_sols).

        @param fsolution: list<DimacsFrontierSol>
            one solution to obtain the property in dimacs format
        @param query: current query
        @param max_step: int - Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
        @return: <tuple <DimacsFrontierSol>>

        @precondition: fsolution is a frontier solution for the query
VIGNET Pierre's avatar
VIGNET Pierre committed
220
        """
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
        # Collect inactivated frontier places
        ### TODO: avoir un attribut non pas pour toutes les frontieres mais juste celles inactives
        final_dsol = \
            [[var] for var in fsolution.frontier_values if var < 0]
        # Prepend inactivated frontier places as a start property in DIMACS form
        if query.dim_start:
            query.dim_start = final_dsol + query.dim_start
        else:
            query.dim_start = final_dsol
        # Must return fsol even if there is no more solution (search first 10 sols)
        # Get <tuple <DimacsFrontierSol>>
        return self.__sq_dimacs_frontier_solutions(query, max_step, max_sols)


    def __prune_frontier_solution(self, fsol, query, max_step):
        """"Take a frontier condition which induces a property prop and reduce the
        number of activated variables from this solution while inducing prop.

        :type fsol: <DimacsFrontierSol>
        :type query: <MCLQuery>
        :rtype: <DimacsfrontierSol>
242

VIGNET Pierre's avatar
VIGNET Pierre committed
243
244
        ASSERT: fsol is a frontier condition implying sq satisfiability
        """
245
246
247
248
249
250
        # 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
251
252
        next_len = 0
        is_pruned = True
253

254
        i = 0
VIGNET Pierre's avatar
VIGNET Pierre committed
255
        while is_pruned:
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
            i += 1
            # find at most 10 ic frontier solutions with the same number of
            # activated frontier places and with all inactivated frontier places
            # forced to be False
            # 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
274
            if len(dimacs_solutions) == 1:
275
276
277
278
279
280
281
282
                # No new solution has been found,
                # the current solution is the best (sol_to_prune)
                return dimacs_solutions[0] # it's sol_to_prune

            # 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
283
284
            is_pruned = current_len > next_len
            if is_pruned:
285
                sol_to_prune = next_sol
VIGNET Pierre's avatar
VIGNET Pierre committed
286
287
                current_len = next_len
        # never reach this point
288
        raise MCLException("MCLAnalyser:__prune_frontier_solution:: what happened??")
289

290
    ## Generic solver for simple queries #######################################
291

VIGNET Pierre's avatar
VIGNET Pierre committed
292
    def sq_is_satisfiable(self, query, max_step):
293
294
295
296
297
        """Check if the query is satisfiable.

        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
298

299
300
        ..warning:: **These variables of interest are not checked here!**
            It is just a satisfiability test!
301

302
303
304
305
306
307
308
309
        ..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
        :type query: <MCLQuery>
        :type max_step: <int>
        :rtype: <boolean>
VIGNET Pierre's avatar
VIGNET Pierre committed
310
        """
311
312
313
314
315
        # 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,
        #    variant_prop, dim_variant_prop, steps_before_reach
        self.unfolder.init_with_query(query)
VIGNET Pierre's avatar
VIGNET Pierre committed
316
317
        # go
        return self.unfolder.squery_is_satisfied(max_step)
318
319


VIGNET Pierre's avatar
VIGNET Pierre committed
320
    def sq_solutions(self, query, max_step, max_sol, vvars):
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
        """Return a list of RawSolution objects

        Parameters are the same as in sq_is_satisfiable() except for vvars
        parameter which deserves some explanations.

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


        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:

            - extract_frontier_values():
                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.


363
        @param query: MCLQuery
364
365
        @param max_step: int - Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
366
367
        @param vvars: variables for which solutions must differ:
                    list<int> Dimacs code
368
369
        :return: a list of RawSolutions from the solver
        :rtype: <list <RawSolution>>
370
371

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

VIGNET Pierre's avatar
VIGNET Pierre committed
374
375
376
        @warning: if the query includes variant constraints, the horizon (max_step) is
            automatically adjusted to min(max_step, len(variant_constraints)).
        """
377
378
379
380
381
        # 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,
        #    variant_prop, dim_variant_prop, steps_before_reach
        self.unfolder.init_with_query(query)
VIGNET Pierre's avatar
VIGNET Pierre committed
382
383
        # go
        return self.unfolder.squery_solve(vvars, max_step, max_sol)
384
385


VIGNET Pierre's avatar
VIGNET Pierre committed
386
    def sq_frontier_solutions(self, query, max_step, max_sol):
387
        """Compute active frontier places and timings
388

389
390
        Compute the set of frontier place names which must be activated for
        implying query satisfaction and returned it as a list of FrontierSolution.
391

392
393
394
395
        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
396

397
398
399
        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
400

401
        This function is a wrapper of sq_solutions().
402

VIGNET Pierre's avatar
VIGNET Pierre committed
403

404
405
406
407
        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.
408

409
410
411
            - The second important attribute is ic_sequence, a list of strings
            which describes the successive activated inputs and free events in
            the solution.
412

413
414
415
        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.
416

417
418
419
420
421
422
423
424
425
426
        @warning: no frontier places are initialized to False

        @param query: MCLQuery
        @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
427
        """
428
429
430
431
432
        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
433

VIGNET Pierre's avatar
VIGNET Pierre committed
434

435
436
    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
437

438
439
440
        DimacsFrontierSol objects provides some interesting attributes like:
        activated_frontier_values (raw values of literals).
        FrontierSolution are of higher level without such attributes.
441

442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
        @param query: MCLQuery
        @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.
        :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
458
459


460
    def __mac_exhaustive_search(self, query, max_step):
VIGNET Pierre's avatar
VIGNET Pierre committed
461
        """
462
        @param query: MCLQuery
463
464
465
        @param max_step: int - Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
        @return <tuple <DimacsFrontierSol>>
VIGNET Pierre's avatar
VIGNET Pierre committed
466
        """
467
        # list of timed minimal activation conditions on frontier (dimacs code)
VIGNET Pierre's avatar
VIGNET Pierre committed
468
        # i.e list<DimacsFrontierSol>
469
470
        mac_list = []

471
472
        reachable = self.sq_is_satisfiable(query, max_step)
        print("reachable ?", reachable)
VIGNET Pierre's avatar
VIGNET Pierre committed
473
        # get the minimum number of steps for reachability
474
        # set number of shifts before testing final prop
VIGNET Pierre's avatar
VIGNET Pierre committed
475
476
        min_step = self.unfolder.get_current_step() - 1
        query.set_steps_before_reach(min_step)
477

478
        while reachable:
VIGNET Pierre's avatar
VIGNET Pierre committed
479
            # compute forbidden solutions: already discovered macs
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
            # Ban all sets of activated frontiers (1 set = 1 sol)
            # 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 ?

            ####TODO: optimiser pr éviter de refaire la négation de toutes les macs à chaque fois
            ### garder en mémoire le résultat précédent
            ####Yield le résultat à chaque fois
            forbidden_sol = \
                [
                    # Get all activated frontiers in each DimacsFrontierSol
                    [-var for var in dimacs_front_sol.activated_frontier_values]
                    for dimacs_front_sol in mac_list
                ]
            print("forbidden sol", forbidden_sol)
            query.dim_start = forbidden_sol
            ## equivaut à mettre à jour le start_prop ou __initial_property avec l'ancienne méthode ??
            ## 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
504
                break
505

506
507
508
509
510
511
512
513
514
515
516
517
518
            # 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
519
                reachable = False
520
521
            else:
                yield current_mac
VIGNET Pierre's avatar
VIGNET Pierre committed
522
                mac_list.append(current_mac)
523
524
        # Return all macs found
        #return tuple(mac_list)
525
526


527
528
529
530
531
532
533
534
535
536
    def next_mac(self, query, max_step):
        """Search a Minimal Access Condition for the given query.

        on cherche d´abord des solutions non minimales
        pour ensuite les élaguer en supprimant les places non essentielles à la
        satisfiabilité de la propriété.
        Ce processus récursif 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,
        cad contiennent beaucoup plus de places.
537
538

        if st_prop contains negation of mac conditions,
VIGNET Pierre's avatar
VIGNET Pierre committed
539
540
541
        return a different mac if any
        same parameters as __mac_exhaustive_search
        Used for search on cluster
542

543
544
545
546
547
548
549
550
551
552
553
554
555
        :param max_step: Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
        :type query: <MCLQuery> or <MCLSimpleQuery>
        :type max_step: <int>
        :return: a list of variables: FrontierSolution is a wrapping of a symbolic
            representation of frontier values and timing from a raw solution.
        :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:
VIGNET Pierre's avatar
VIGNET Pierre committed
556
            return None
557

558
559
560
561
562
563
564
565
566
567
568
569
570
571
        # 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):
        """Wrapper for __mac_exhaustive_search(); return FrontierSolutions

        ..note:: __mac_exhaustive_search() returns DimacsFrontierSols
572
573

        @param query: MCLQuery
574
575
576
        @param max_step: int - Number of steps allowed in the unfolding;
            the horizon on which the properties must be satisfied
        @return: <tuple <FrontierSolution>>
VIGNET Pierre's avatar
VIGNET Pierre committed
577
        """
578
579
580
581
582
583
584
585
        # Get <tuple <DimacsFrontierSol>>
        mac_list = self.__mac_exhaustive_search(query, max_step)
        # Convert to a tuple of FrontierSolution
        #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 ##############################################################
586

VIGNET Pierre's avatar
VIGNET Pierre committed
587
    def is_strong_activator(self, act_sol, query):
588
589
590
591
592
593
        """Test if an activation condition is a strong one (independent of timing)

        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
594
        @param act_sol: FrontierSolution with activation condition
595
        @param query: the query used for act_sol condition
VIGNET Pierre's avatar
VIGNET Pierre committed
596
597
        """
        nb_step = len(act_sol.ic_sequence) - 1
598
        query_1 = MCLSimpleQuery.from_frontier_sol_same_timing(act_sol,
599
                                                               self.unfolder)
VIGNET Pierre's avatar
VIGNET Pierre committed
600
601
602
603
        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))
604

VIGNET Pierre's avatar
VIGNET Pierre committed
605
606
    def next_inhibitor(self, mac, query):
        """
607
        if st_prop contains negation of mac conditions,
VIGNET Pierre's avatar
VIGNET Pierre committed
608
609
610
        return a different mac if any
        same parameters as __mac_exhaustive_search
        Used for search on cluster
611

VIGNET Pierre's avatar
VIGNET Pierre committed
612
        @param mac: FrontierSolution
613
        @param query: MCLQuery
614
        @param max_step: int - number of dynamical step
VIGNET Pierre's avatar
VIGNET Pierre committed
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
        @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)
630
631
        max_step = len(inh_query.variant_prop)
        assert(max_step == len(mac.ic_sequence))
632

VIGNET Pierre's avatar
VIGNET Pierre committed
633
634
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
635
        next_inhib = self.next_mac(inh_query, max_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
636
637
        self.unfolder.set_include_aux_clauses(True)
        return next_inhib
638
639


VIGNET Pierre's avatar
VIGNET Pierre committed
640
    def mac_inhibitor_search(self, mac, query, max_sol):
641
        """Search inhibitors for a mac scenario
642

VIGNET Pierre's avatar
VIGNET Pierre committed
643
644
645
646
        @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
647

VIGNET Pierre's avatar
VIGNET Pierre committed
648
649
650
651
652
653
654
655
656
657
658
659
660
661
        @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)
662

663
664
        max_step = len(inh_query.variant_prop)
        assert(max_step == len(mac.ic_sequence))
VIGNET Pierre's avatar
VIGNET Pierre committed
665
666
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
667
668
#        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
669
670
671
672
        self.unfolder.set_include_aux_clauses(True)
        return lsol

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

VIGNET Pierre's avatar
VIGNET Pierre committed
676
677
678
        @param in_sol: FrontierSolution with activation condition and inhibition
        @param query: the property which is inhibed
        """
679
680
681
682
        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
683
684
685
686
687
688
689
690
691
        # 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)
692
        return not self.sq_is_satisfiable(query_1, max_step)
693