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 20.9 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
from antlr3 import ANTLRFileStream, CommonTokenStream
VIGNET Pierre's avatar
VIGNET Pierre committed
46

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

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

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
from cadbiom.models.clause_constraints.mcl.MCLSolutions import \
VIGNET Pierre's avatar
VIGNET Pierre committed
57
        extract_dimacs_init_frontier, MCLException
58
59
60
61
62
63
64

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
from cadbiom.models.clause_constraints.mcl.MCLSolutions import FrontierSolution
from cadbiom.models.clause_constraints.mcl.MCLQuery import MCLSimpleQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
65
66
67
68
69
70
71
72
73
74

#import random
import sys
TRACEFILE = sys.stdout

class MCLAnalyser(object):
    """
    query a UCL dynamical system and analyses solutions
    """
    NB_SOL = 10  # for mac search - to be optimized??
75

VIGNET Pierre's avatar
VIGNET Pierre committed
76
77
78
79
80
81
82
83
    def __init__(self, report):
        """
        Constructor - the built analyser is void
        @param report: a standard reporter
        """
        self.cl_dyn_sys = None     # dynamical system in clause constraint form
        self.unfolder = None       # computation management: unfolding
        self.reporter = report     # for generic error display
84
        self.opti = True           # turn on optimizations for translation
VIGNET Pierre's avatar
VIGNET Pierre committed
85
86
87
88
89
90
91
92
93
94
95

    # building
    def build_from_chart_model(self, model):
        """
        Build an MCLAnalyser from a chartmodel object
        @param model: object - ChartModel
        """
        # reloading a MCLAnalyser is forbidden - create a new one
        if self.unfolder:
            raise MCLException("This MCLAnalyser is already initialized")
        # building CLsys
96
        vtab = TableVisitor(self.reporter)
VIGNET Pierre's avatar
VIGNET Pierre committed
97
98
99
100
101
102
103
104
105
106
107
        model.accept(vtab)
        if self.reporter.error:
            return
        clds = CLDynSys( vtab.tab_symb, self.reporter)
        if self.reporter.error:
            return
        comp_visitor = GT2Clauses(clds, self.reporter, self.opti)
        model.accept(comp_visitor)
        if self.reporter.error:
            return
        self.cl_dyn_sys = clds
108

VIGNET Pierre's avatar
VIGNET Pierre committed
109
110
111
112
113
114
115
116
117
118
119
120
121
        # build unfolder
        self.unfolder = CLUnfolder(clds)

    def build_from_chart_file(self, file_name):
        """
        Build an MCLAnalyser from a .bcx file
        @param file_name: str - path of the .bcx file
        """
        parsing = MakeModelFromXmlFile(file_name)
        # chart model
        cmodel = parsing.get_model()
        self.build_from_chart_model(cmodel)

122
    def build_from_pid_file(self,
VIGNET Pierre's avatar
VIGNET Pierre committed
123
124
125
126
127
                            file_name, has_clock=True, ai_interpretation=0):
        """
        Build an MCLAnalyser from a .xml file of PID database
        @param file_name: str - path of .xml file
        """
128
        parsing = MakeModelFromPidFile(file_name,
VIGNET Pierre's avatar
VIGNET Pierre committed
129
130
131
132
                                    self.reporter, has_clock, ai_interpretation)
        # chart model
        cmodel = parsing.get_model()
        self.build_from_chart_model(cmodel)
133

VIGNET Pierre's avatar
VIGNET Pierre committed
134
135
136
137
138
139
140
    def build_from_cadlang(self, file_name):
        """
        Build an MCLAnalyser from a .cal file of PID database
        @param file_name: str - path of .cal file
        """
        creporter = self.reporter
        fstream = ANTLRFileStream(file_name)
141
        lexer = cadlangLexer(fstream)
VIGNET Pierre's avatar
VIGNET Pierre committed
142
143
144
145
146
147
148
149
150
        lexer.set_error_reporter(creporter)
        parser = cadlangParser(CommonTokenStream(lexer))
        parser.set_error_reporter(creporter)
        model = ChartModel(file_name)
        parser.cad_model(model)
        # chart model
        cmodel = parser.model
        self.build_from_chart_model(cmodel)

151
152


VIGNET Pierre's avatar
VIGNET Pierre committed
153
154
155
156
    # solution processing
    def less_activated_solution(self, dimacs_solution_list):
        """
        return the solution with the less activated  states
157
        @param dimacs_solution_list: either a DimacsFrontierSol or DimacsActFrontSol list
VIGNET Pierre's avatar
VIGNET Pierre committed
158
159
160
161
162
163
164
165
166
        @return: a solution object of the type in the list
        """
        if not dimacs_solution_list:
            self.reporter.display(
                    "Trying to find a smallest solution without solution list")
            return None

        smallest_sol = dimacs_solution_list[0]
        la_number = smallest_sol.nb_activated()
167

VIGNET Pierre's avatar
VIGNET Pierre committed
168
169
170
171
172
        for sol in dimacs_solution_list[1:]:
            if sol.nb_activated() < la_number:
                smallest_sol = sol
                la_number = sol.nb_activated()
        return smallest_sol
173

VIGNET Pierre's avatar
VIGNET Pierre committed
174
175
    def __prune_frontier_solution(self, fsol, query, max_step):
        """
176
        take a frontier condition  which induces property prop and reduce the
VIGNET Pierre's avatar
VIGNET Pierre committed
177
178
179
180
        number of activated variables from this solution while inducing prop,
        @param fsol: a DimacsFrontierSol
        @param query: MCLQuery
        @return: a DimacsfrontierSol
181

VIGNET Pierre's avatar
VIGNET Pierre committed
182
183
        ASSERT: fsol is a frontier condition implying sq satisfiability
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
184

VIGNET Pierre's avatar
VIGNET Pierre committed
185
186
187
188
189
190
191
192
193
#        # for debug - too expansive to be activated anytime
#        start = []
#        for s in fsol.frontier_values:
#            start.append([s])
#        assert(self.sq_is_satisfiable(query, max_step))
        to_prune = fsol
        current_len = fsol.nb_activated() # number of act. places in solution
        next_len = 0
        is_pruned = True
194

VIGNET Pierre's avatar
VIGNET Pierre committed
195
        while is_pruned:
196
            # find at most 10 ic frontier solutions with same no activated
VIGNET Pierre's avatar
VIGNET Pierre committed
197
            # frontier place - return current_small if no more sol
198
199
200
            dimacs_solutions = self.__solve_with_inact_fsolution(
                                                                 to_prune,
                                                                 query,
VIGNET Pierre's avatar
VIGNET Pierre committed
201
202
203
204
205
206
207
208
209
210
211
212
                                                                 max_step)
            if len(dimacs_solutions) == 1:
                return dimacs_solutions[0]  # found no new solutions
            # seach for less activated solutions
            next_small = self.less_activated_solution(dimacs_solutions)
            next_len = next_small.nb_activated()
            is_pruned = current_len > next_len
            if is_pruned:
                to_prune = next_small
                current_len = next_len
        # never reach this point
        raise MCLException("_prune_frontier_solution: what happened??")
213

VIGNET Pierre's avatar
VIGNET Pierre committed
214
215
216
217
218
219
    # for unit test
    def test_prune_frontier_solution(self, fsol, query, max_step):
        """
        For tests only
        """
        return self.__prune_frontier_solution(fsol, query, max_step)
220
221
222


    # generic solver for simple queries
VIGNET Pierre's avatar
VIGNET Pierre committed
223
224
    def sq_is_satisfiable(self, query, max_step):
        """
225
        @param query: MCLQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
226
227
228
        @param max_step: int - length of unfolding

        @return: boolean
229

VIGNET Pierre's avatar
VIGNET Pierre committed
230
231
232
233
234
235
236
237
238
239
240
241
        @warning: no_frontier places are initialized to False in simple queries
        """
        # setting parameters
        self.unfolder.reset()
        self.unfolder.set_initial_property(query.start_prop)
        self.unfolder.set_dim_initial_property(query.dim_start)
        self.unfolder.set_current_property(query.inv_prop)
        self.unfolder.set_dim_current_property(query.dim_inv)
        self.unfolder.set_final_property(query.final_prop)
        self.unfolder.set_dim_final_property(query.dim_final)
        self.unfolder.set_variant_property(query.variant_prop)
        self.unfolder.set_dim_variant_property(query.dim_variant_prop)
242

VIGNET Pierre's avatar
VIGNET Pierre committed
243
244
245
        self.unfolder.set_minimal_steps(query.steps_before_reach)
        # go
        return self.unfolder.squery_is_satisfied(max_step)
246
247


VIGNET Pierre's avatar
VIGNET Pierre committed
248
249
    def sq_solutions(self, query, max_step, max_sol, vvars):
        """
250
        @param query: MCLQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
251
        @param max_step: int - length of unfolding
252
253
        @param vvars: variables for which solutions must differ:
                    list<int> Dimacs code
VIGNET Pierre's avatar
VIGNET Pierre committed
254
        @return: a list of RawSolution objects
255
256

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

VIGNET Pierre's avatar
VIGNET Pierre committed
259
260
261
262
263
264
265
266
267
268
269
270
271
        @warning: if the query includes variant constraints, the horizon (max_step) is
            automatically adjusted to min(max_step, len(variant_constraints)).
        """
        # setting parameters
        self.unfolder.reset()
        self.unfolder.set_initial_property(query.start_prop)
        self.unfolder.set_dim_initial_property(query.dim_start)
        self.unfolder.set_current_property(query.inv_prop)
        self.unfolder.set_dim_current_property(query.dim_inv)
        self.unfolder.set_final_property(query.final_prop)
        self.unfolder.set_dim_final_property(query.dim_final)
        self.unfolder.set_variant_property(query.variant_prop)
        self.unfolder.set_dim_variant_property(query.dim_variant_prop)
272

VIGNET Pierre's avatar
VIGNET Pierre committed
273
274
275
        self.unfolder.set_minimal_steps(query.steps_before_reach)
        # go
        return self.unfolder.squery_solve(vvars, max_step, max_sol)
276
277


VIGNET Pierre's avatar
VIGNET Pierre committed
278
279
280
    def sq_frontier_solutions(self, query, max_step, max_sol):
        """
        Compute active frontier places and timing
281
        @param query: MCLQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
282
        @param max_step: int - length of unfolding
283
284
        @param max_sol: max number of solutions
        @return:  list<FrontierSolution>  set of frontier place names which
VIGNET Pierre's avatar
VIGNET Pierre committed
285
                                      must be activated for implying query satisfaction
286
287
        @warning:  no_frontier places are initialized to False

VIGNET Pierre's avatar
VIGNET Pierre committed
288
289
290
291
292
293
294
295
        """
        vvars = self.unfolder.get_frontier()
        l_sol = self.sq_solutions(query, max_step, max_sol, vvars)
        out = []
        for sol in l_sol:
            fsol = FrontierSolution.from_raw(sol)
            out.append(fsol)
        return out
296

VIGNET Pierre's avatar
VIGNET Pierre committed
297
298
    def __sq_dimacs_frontier_solutions(self, query, max_step, max_sol):
        """
299
        @param query: MCLQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
300
        @param max_step: int - length of unfolding
301
        @param max_sol:int - max number of solutions for each solve
VIGNET Pierre's avatar
VIGNET Pierre committed
302
        @return:  list<DimacsFrontierSol>
303

VIGNET Pierre's avatar
VIGNET Pierre committed
304
305
306
307
308
        """
        frontier = self.unfolder.get_frontier()
        lsol = self.sq_solutions(query, max_step, max_sol, frontier)
        return extract_dimacs_init_frontier(lsol)

309

VIGNET Pierre's avatar
VIGNET Pierre committed
310
311
312
313
314
    # only for unit test
    def test_dimacs_frontier_sol(self, query, max_step, max_sol):
        """ for test only """
        return self.__sq_dimacs_frontier_solutions(query, max_step, max_sol)

315
316


VIGNET Pierre's avatar
VIGNET Pierre committed
317
318
319
320
321
322
323
    def __solve_with_inact_fsolution(self, fsolution, query, max_step):
        """
        frontier states not activated in  fsolution (frontier solution) forced
        to be False at start solve and return frontier solution list with this constraint
        @param fsolution: list<DimacsFrontierSol> -  one solution to obtain the property in dimacs
        @param query: current query
        @param max_step: int - horizon
324

VIGNET Pierre's avatar
VIGNET Pierre committed
325
326
        @precondition: fsolution is a frontier solution for the query
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
327
328
329
330

        # collect inactivated places
        final_dsol = \
            [[var] for var in fsolution.frontier_values if var < 0]
VIGNET Pierre's avatar
VIGNET Pierre committed
331
332
333
334
335
        if query.dim_start:
            query.set_dim_start(final_dsol + query.dim_start)
        else:
            query.set_dim_start(final_dsol)
        # must return fsol if no more solution
336
        return self.__sq_dimacs_frontier_solutions(query, max_step,
VIGNET Pierre's avatar
VIGNET Pierre committed
337
338
                                                   MCLAnalyser.NB_SOL)

339

VIGNET Pierre's avatar
VIGNET Pierre committed
340
341
342
343
344
345
    # only for unit test
    def test_solve_with_inact_fsolution(self, fsolution, query, max_step):
        """
        unit test accessible
        """
        self.__solve_with_inact_fsolution(fsolution, query, max_step)
346
347
348



VIGNET Pierre's avatar
VIGNET Pierre committed
349
350
    def __mac_exhaustive_search(self, query, nb_step):
        """
351
        @param query: MCLQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
352
        @param nb_step: int - number of dynamical step
353
        @return tuple<DimacsFrontierSol>
VIGNET Pierre's avatar
VIGNET Pierre committed
354
        """
355
        # list of timed minimal activation conditions on frontier (dimacs code)
VIGNET Pierre's avatar
VIGNET Pierre committed
356
        # i.e list<DimacsFrontierSol>
357
358
        mac_list = []

VIGNET Pierre's avatar
VIGNET Pierre committed
359
360
361
362
        reachable = self.sq_is_satisfiable(query, nb_step)
        # get the minimum number of steps for reachability
        min_step = self.unfolder.get_current_step() - 1
        query.set_steps_before_reach(min_step)
363

VIGNET Pierre's avatar
VIGNET Pierre committed
364
365
366
367
368
369
370
371
372
        while reachable :
            # compute forbidden solutions: already discovered macs
            forbidden_sol = []
            for dsol in mac_list:
                dimacs_clause = []
                for var in dsol.frontier_values:
                    if var > 0:
                        dimacs_clause.append(-var)       # OR( not var)
                forbidden_sol.append(dimacs_clause)
373
374

            # reachable - solutions differ on frontier: 2 different solutions
VIGNET Pierre's avatar
VIGNET Pierre committed
375
            # to avoid a all activated solution - lfsol:list<DimacsFrontierSol>
376
            query.set_dim_start(forbidden_sol)
VIGNET Pierre's avatar
VIGNET Pierre committed
377
378
            lfsol = self.__sq_dimacs_frontier_solutions(query, nb_step, 2)
            if len(lfsol)>0:
379
                small_sol = self.less_activated_solution(lfsol)
VIGNET Pierre's avatar
VIGNET Pierre committed
380
381
382
383
384
385
386
                start = []
                for ssol in small_sol.frontier_values:
                    start.append([ssol])
                #assert(self.sq_is_satisfiable(query, nb_step))
            else:
                reachable = False
                break
387
388

            current_mac = self.__prune_frontier_solution(small_sol,
VIGNET Pierre's avatar
VIGNET Pierre committed
389
390
391
                                                         query, nb_step)
            if current_mac.nb_activated() == 0:
                reachable = False
392
            else :
VIGNET Pierre's avatar
VIGNET Pierre committed
393
                mac_list.append(current_mac)
394
        return tuple(mac_list)
395
396
397



VIGNET Pierre's avatar
VIGNET Pierre committed
398
399
    def next_mac(self, query, nb_step):
        """
400
        if st_prop contains negation of mac conditions,
VIGNET Pierre's avatar
VIGNET Pierre committed
401
402
403
        return a different mac if any
        same parameters as __mac_exhaustive_search
        Used for search on cluster
404
405

        @param query: MCLQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
406
407
408
409
410
        @param nb_step: int - number of dynamical step
        @return: a list of variables (list<string>)
        """
        lfsol = self.__sq_dimacs_frontier_solutions(query, nb_step, 2)
        if len(lfsol)>0:
411
            small_fsol = self.less_activated_solution(lfsol)
VIGNET Pierre's avatar
VIGNET Pierre committed
412
413
        else:
            return None
414
415

        current_mac = self.__prune_frontier_solution(small_fsol,
VIGNET Pierre's avatar
VIGNET Pierre committed
416
417
418
419
                                                     query,
                                                     nb_step)
        vmac = FrontierSolution.from_dimacs_front_sol(current_mac)
        return vmac
420

VIGNET Pierre's avatar
VIGNET Pierre committed
421
422
    def mac_search(self, query, nb_step):
        """
423
        @param query: MCLQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
424
        @param nb_step: int - number of dynamical step
425
        @return: list<FrontierSolution>
VIGNET Pierre's avatar
VIGNET Pierre committed
426
427
428
        """
        mac_list = self.__mac_exhaustive_search(query, nb_step)
        # convert to FrontierSolution list
429
        return tuple(FrontierSolution.from_dimacs_front_sol(mac) for mac in mac_list)
430

VIGNET Pierre's avatar
VIGNET Pierre committed
431
432
433
434
    def is_strong_activator(self, act_sol, query):
        """
        test if an activation condition is a strong one (independent of timing)
        @param act_sol: FrontierSolution with activation condition
435
        @param query: the query used for act_sol condition
VIGNET Pierre's avatar
VIGNET Pierre committed
436
437
        """
        nb_step = len(act_sol.ic_sequence) - 1
438
        query_1 = MCLSimpleQuery.from_frontier_sol_same_timing(act_sol,
439
                                                               self.unfolder)
VIGNET Pierre's avatar
VIGNET Pierre committed
440
441
442
443
        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))
444

VIGNET Pierre's avatar
VIGNET Pierre committed
445
446
    def next_inhibitor(self, mac, query):
        """
447
        if st_prop contains negation of mac conditions,
VIGNET Pierre's avatar
VIGNET Pierre committed
448
449
450
        return a different mac if any
        same parameters as __mac_exhaustive_search
        Used for search on cluster
451

VIGNET Pierre's avatar
VIGNET Pierre committed
452
        @param mac: FrontierSolution
453
        @param query: MCLQuery
VIGNET Pierre's avatar
VIGNET Pierre committed
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
        @param nb_step: int - number of dynamical step
        @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)
        nb_step = len(inh_query.variant_prop)
        assert(nb_step == len(mac.ic_sequence))
472

VIGNET Pierre's avatar
VIGNET Pierre committed
473
474
475
476
477
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
        next_inhib = self.next_mac(inh_query, nb_step)
        self.unfolder.set_include_aux_clauses(True)
        return next_inhib
478
479


VIGNET Pierre's avatar
VIGNET Pierre committed
480
481
482
    def mac_inhibitor_search(self, mac, query, max_sol):
        """
        Search inhibitors for a mac scenario
483

VIGNET Pierre's avatar
VIGNET Pierre committed
484
485
486
487
        @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
488

VIGNET Pierre's avatar
VIGNET Pierre committed
489
490
491
492
493
494
495
496
497
498
499
500
501
502
        @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)
503

VIGNET Pierre's avatar
VIGNET Pierre committed
504
505
506
507
508
509
510
511
512
513
514
        nb_step = len(inh_query.variant_prop)
        assert(nb_step == len(mac.ic_sequence))
        # search solutions - diseable aux clauses
        self.unfolder.set_include_aux_clauses(False)
#        lsol = self.sq_frontier_solutions(inh_query, nb_step, max_sol)
        lsol = self.mac_search(inh_query, nb_step)
        self.unfolder.set_include_aux_clauses(True)
        return lsol

    def is_strong_inhibitor(self, in_sol, query):
        """
515
        test if an activation condition inhibitor is a trong one
VIGNET Pierre's avatar
VIGNET Pierre committed
516
517
518
519
520
        (i.e independent of timing)
        @param in_sol: FrontierSolution with activation condition and inhibition
        @param query: the property which is inhibed
        """
        nb_step = len(in_sol.ic_sequence) - 1
521
        query_1 = MCLSimpleQuery.from_frontier_sol_new_timing(in_sol,
VIGNET Pierre's avatar
VIGNET Pierre committed
522
523
524
525
526
527
528
529
530
531
                                                              self.unfolder)
        # 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)
532
533
534
535
        return not self.sq_is_satisfiable(query_1, nb_step)


# helper functions
VIGNET Pierre's avatar
VIGNET Pierre committed
536
def only_in_l1(ll1, ll2):
VIGNET Pierre's avatar
VIGNET Pierre committed
537
    """(not used)
VIGNET Pierre's avatar
VIGNET Pierre committed
538
539
540
541
542
543
544
545
546
547
    @param ll1: list<any> - list of element
    @param ll2: list<any> - list of element
    @return: only_l1 list<any> - list of element that are only in the first list (l1\l2)
    """
    only_l1 = []
    for el1 in ll1:
        if el1 not in ll2:
            only_l1.append(el1)
    only_l1.sort()
    return only_l1