CLUnfolder.py 39.3 KB
Newer Older
VIGNET Pierre's avatar
VIGNET Pierre committed
1
2
3
## Filename    : CLUnfolder.py
## Author(s)   : Michel Le Borgne
## Created     : 22 mars 2012
4
5
## Revision    :
## Source      :
VIGNET Pierre's avatar
VIGNET Pierre committed
6
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
##
## 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
36
37
##     35042 RENNES Cedex, FRANCE
##
VIGNET Pierre's avatar
VIGNET Pierre committed
38
39
40
41
42
43
##
## Contributor(s): Geoffroy Andrieux IRSET
##
"""
Main engine for constraint unfolding and solving
"""
VIGNET Pierre's avatar
VIGNET Pierre committed
44
45
#from pyCryptoMS import CryptoMS
from pycryptosat import Solver as CryptoMS
46
47
48
from cadbiom.models.biosignal.translators.gt_visitors import compile_cond, compile_event
from cadbiom.models.clause_constraints.CLDynSys import Clause, Literal
from cadbiom.models.clause_constraints.mcl.MCLSolutions import RawSolution, MCLException
VIGNET Pierre's avatar
VIGNET Pierre committed
49

50
51
52
from cadbiom import commons as cm

LOGGER = cm.logger()
VIGNET Pierre's avatar
VIGNET Pierre committed
53
54
55
56
57
58
59
60
61

class CLUnfolder(object):
    """
    Dynamic constraints unfolding management
    ========================================
    Each variable is coded as an integer (in var_code_table and var_list).
    Each clause is represented as a list of signed integers (DIMACS coding).
    During unfolding, clauses are shifted either to the future (forward) or
    to the past (backward). The shift operator is a simple addition
62
63
    of self.__shift_step. The shift direction depends only on initializations.
    self.__shift_step depends on the number of variables so it is impossible
VIGNET Pierre's avatar
VIGNET Pierre committed
64
    to add variables while generating a trajectory unfolding.
65
66

    Glossary
VIGNET Pierre's avatar
VIGNET Pierre committed
67
68
69
    ========
    - ground variables/ground dimacs code: variables at time 0/their encoding.
    - solution: a solution of the logical dynamic constraint from SAT solver
70
    - state vector: list of DIMACS code of original (not shifted) variables
VIGNET Pierre's avatar
VIGNET Pierre committed
71
72
73
      corresponding to a step.
    - trajectory: list of state_vectors
    """
74

VIGNET Pierre's avatar
VIGNET Pierre committed
75
76
    def __init__(self, sys):
        self.__dyn_sys = sys # symbolic clause dynamic system
77
78

        # shift_step equal to the total number of coded variables
VIGNET Pierre's avatar
VIGNET Pierre committed
79
80
81
82
83
84
        self.__shift_step_init = sys.get_var_number() # shift step of system
        self.__shift_step = self.__shift_step_init    #  current shift/step
        self.__locked = False
        self.__current_step = 1
        self.__steps_before_check = 0
        self.__include_aux_clauses = True
85

VIGNET Pierre's avatar
VIGNET Pierre committed
86
87
        # assign a DIMACS code number to each variable (invariant)
        self.__lit_cpt = self.__shift_step +1 # counter for aux. var. coding
88
        self.__var_code_table = dict()            # name -> DIMACS code
VIGNET Pierre's avatar
VIGNET Pierre committed
89
90
91
92
93
94
95
        self.__var_list = ['##']                  # DIMACS code -> name - != 0
        cpt = 1
        for svar in sys.base_var_set:
            self.__var_list.append(svar)
            self.__var_code_table[svar] = cpt
            cpt += 1
        assert(cpt == self.__shift_step + 1)
96

VIGNET Pierre's avatar
VIGNET Pierre committed
97
        # same tools for auxiliary variables from property compilation
98
        self.__aux_code_table = dict()            # name 2 code
VIGNET Pierre's avatar
VIGNET Pierre committed
99
        self.__aux_list = []                      # code to name
100
101

        # list  no_frontier place DIMACS codes
VIGNET Pierre's avatar
VIGNET Pierre committed
102
103
104
        self.__no_frontier_init = []
        for nfp in self.__dyn_sys.no_frontier:
            self.__no_frontier_init.append([- self.__var_code_table[nfp]])
105

VIGNET Pierre's avatar
VIGNET Pierre committed
106
107
108
109
110
        # ordered list of frontier place DIMACS codes for extraction (inv)
        self.__frontier = []
        for frp in self.__dyn_sys.frontier:
            self.__frontier.append(self.__var_code_table[frp])
        self.__frontier.sort()
111

VIGNET Pierre's avatar
VIGNET Pierre committed
112
113
114
115
116
        # ordered list of input places DIMACS code for extraction (inv)
        self.__inputs = []
        for inp in self.__dyn_sys.inputs:
            self.__inputs.append(self.__var_code_table[inp])
        self.__inputs.sort()
117

VIGNET Pierre's avatar
VIGNET Pierre committed
118
119
120
121
122
        # ordered list of free clocks DIMACS code for extraction (invariant)
        self.__free_clocks = []
        for fcl in self.__dyn_sys.free_clocks:
            self.__free_clocks.append(self.__var_code_table[fcl])
        self.__free_clocks.sort()
123

VIGNET Pierre's avatar
VIGNET Pierre committed
124
125
126
127
        # properties to be checked
        self.__initial_property = None            # string
        self.__dim_initial = None                 # list of dimacs clauses
        self.__final_property = None              # idem
128
        self.__dim_final = None
VIGNET Pierre's avatar
VIGNET Pierre committed
129
130
131
132
133
134
        self.__invariant_property = None          # idem
        self.__dim_invariant = None
        self.__variant_property = None            # list<logic formulas>
        self.__dim_variant = None                 # list<list<dimacs clauses>>
        # list of variant temporal constraints in Dimacs ground code
        self.__list_variant_constraints = None    # list<list<dimacs clauses>>
135
136

        # constraints - logical constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
        # result from unfolding of base constraints
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
        self.__initial_constraints = []        # DIMACS clauses: C(X_0)
        self.__final_constraints   = []        # idem: C(X_n)
        self.__invariant_constraints = []      # DIMACS clauses: C(X_i))
        self.__variant_constraints = []        # variant constraints along traj.
        self.__shift_direction = None          # forward or backward

        # statistics on solver
        self.__stats = False
        self.__nb_vars = 0
        self.__nb_clauses = 0



    def reset(self):
        """
        Reset the unfolder before a new query
        """
        self.__initial_property = None
        self.__dim_initial = None
        self.__final_property = None
159
        self.__dim_final = None
VIGNET Pierre's avatar
VIGNET Pierre committed
160
161
162
163
164
165
        self.__invariant_property = None
        self.__dim_invariant = None
        self.__variant_property = None
        self.__dim_variant = None
        self.list_variant_constraints = None
        self.__steps_before_check = 0
166
        self.__shift_direction = None
VIGNET Pierre's avatar
VIGNET Pierre committed
167
        self.__locked = False
168

VIGNET Pierre's avatar
VIGNET Pierre committed
169
170
171
172
173
174
175
    def set_stats(self):
        """
        Enable solver statistics
        """
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
176

VIGNET Pierre's avatar
VIGNET Pierre committed
177
178
179
180
181
    def unset_stats(self):
        """
        disable solver statistics
        """
        self.__stats = False
182

VIGNET Pierre's avatar
VIGNET Pierre committed
183
184
    def _stats(self):
        """
185
        print solver statistics
VIGNET Pierre's avatar
VIGNET Pierre committed
186
187
188
        """
        print "\n NB Variables in solver: ", self.__nb_vars
        print "NB Clauses in solver: ", self.__nb_clauses
189

VIGNET Pierre's avatar
VIGNET Pierre committed
190
191
192
193
194
    def set_minimal_steps(self, nb_steps):
        """
        For reachability optimisation. number of shift before checking
        """
        self.__steps_before_check = nb_steps
195

VIGNET Pierre's avatar
VIGNET Pierre committed
196
197
198
199
200
201
202
    def set_include_aux_clauses(self, val):
        """
        Include auxiliary clause to eliminate undesirable solutions
        If A->B has clock h an aux constraint added is h included in h when A
        Must be set to False for inhibitors computations
        """
        self.__include_aux_clauses = val
203

VIGNET Pierre's avatar
VIGNET Pierre committed
204
205
206
207
208
209
    # internal variable access for tests
    def get_dynamic_constraints(self):
        """
        For tests: returns coded dynamic constraints
        """
        return self.__dynamic_constraints
210

VIGNET Pierre's avatar
VIGNET Pierre committed
211
212
213
214
215
    def get_initial_constraints(self):
        """
        For tests: returns coded initial constraints
        """
        return self.__initial_constraints
216

VIGNET Pierre's avatar
VIGNET Pierre committed
217
218
219
220
221
    def get_invariant_constraints(self):
        """
        For tests: returns coded invariant constraints
        """
        return self.__invariant_constraints
222

VIGNET Pierre's avatar
VIGNET Pierre committed
223
224
225
226
227
    def get_variant_constraints(self):
        """
        For tests: returns coded variant constraints
        """
        return self.__variant_constraints
228

VIGNET Pierre's avatar
VIGNET Pierre committed
229
230
231
232
233
    def get_final_constraints(self):
        """
        For tests: returns coded final constraints
        """
        self.__final_constraints
234

VIGNET Pierre's avatar
VIGNET Pierre committed
235
236
237
238
239
240
    # variables management
    def var_dimacs_code(self, var_name):
        """
        returns dimacs code of (string) var_name variable
        """
        return self.__var_code_table[var_name]
241

VIGNET Pierre's avatar
VIGNET Pierre committed
242
243
244
245
246
    def get_system_var_number(self):
        """
        number of variables in the clause constraint dynamical system
        """
        return self.__dyn_sys.get_var_number()
247

VIGNET Pierre's avatar
VIGNET Pierre committed
248
249
250
251
252
    def get_var_number(self):
        """
        number of principal variables (properties excluded) in the unfolder
        """
        return len(self.__var_list) -1
253

VIGNET Pierre's avatar
VIGNET Pierre committed
254
255
256
    def get_var_name(self, var_num):
        """
        @param var_num: DIMACS literal coding of an initial variable
257
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
258
        """
259
        if var_num < 0:
VIGNET Pierre's avatar
VIGNET Pierre committed
260
261
262
263
264
265
266
267
            varnum1 = -var_num
        else: varnum1 = var_num
        var_code = (varnum1 - 1) % self.__shift_step + 1
        if var_code <= self.__shift_step_init: # variable from initial system
            return self.__var_list[var_code]
        else: # auxiliary variable introduced by properties compilation
            return self.__aux_list[var_code - self.__shift_step_init -1]
            #raise MCLException("Not a DIMACS code of an initial variable")
268

VIGNET Pierre's avatar
VIGNET Pierre committed
269
270
271
272
273
    def get_var_indexed_name(self, var_num):
        """
        @param var_num: DIMACS literal coding
        @return: name of the variable with time index
        """
274
        if var_num < 0:
VIGNET Pierre's avatar
VIGNET Pierre committed
275
276
277
278
279
280
281
282
283
            varnum1 = -var_num
        else: varnum1 = var_num
        var_code = (varnum1 - 1) % self.__shift_step + 1
        var_step = (varnum1 - var_code)/self.__shift_step
        if var_code <= self.__shift_step_init:
            return self.__var_list[var_code] + '_%s'% var_step
        else:
            index = var_code - self.__shift_step_init -1
            return self.__aux_list[index] + '_%s'% var_step
284

VIGNET Pierre's avatar
VIGNET Pierre committed
285
286
    def get_frontier(self):
        """
287
        @return: the DIMACS code of the frontier variables
VIGNET Pierre's avatar
VIGNET Pierre committed
288
289
        """
        return self.__frontier
290

VIGNET Pierre's avatar
VIGNET Pierre committed
291
292
293
294
295
    def get_free_clocks(self):
        """
        @return: the DIMACS code of the free_clocks variables
        """
        return self.__free_clocks
296

VIGNET Pierre's avatar
VIGNET Pierre committed
297
298
299
300
301
    def get_inputs(self):
        """
        @return: the DIMACS code of the input variables
        """
        return self.__inputs
302

VIGNET Pierre's avatar
VIGNET Pierre committed
303
304
305
306
307
    def get_shift_direction(self):
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
308

VIGNET Pierre's avatar
VIGNET Pierre committed
309
310
311
312
313
    def get_shift_step(self):
        """
        @return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
        """
        return self.__shift_step
314

VIGNET Pierre's avatar
VIGNET Pierre committed
315
316
317
318
319
    def get_shift_step_init(self):
        """
        @return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
        """
        return self.__shift_step_init
320

VIGNET Pierre's avatar
VIGNET Pierre committed
321
322
323
324
325
326
    def get_current_step(self):
        """
        @return: the current number of unfolding
        """
        return self.__current_step

327
328


VIGNET Pierre's avatar
VIGNET Pierre committed
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
    # translation from names to num codes
    # the translation depends on the shift direction
    def __forward_code(self, clause):
        """
        numerically code a clause with the numeric code found in self.__var_code_table for
        a base variable x and numeric_code + shift_step for x'
        variable integer coding increases in futur steps
        @param clause: a Clause object
        @return: the DIMACS coding of the forward shifted clause
        """
        num_clause = []
        for lit in clause.list_of_literals:
            name = lit.name
            if name[-1] == '`': # t+1 variable
                lit_cod = self.__var_code_table[name[:-1]] + self.__shift_step
            else:
                lit_cod = self.__var_code_table[name] # t variable
            if not lit.sign:
                lit_cod = - lit_cod
            num_clause.append(lit_cod)
        return num_clause
350

VIGNET Pierre's avatar
VIGNET Pierre committed
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
    def __backward_code(self, clause):
        """
        numerically code a clause with the numeric code found in self.__var_code_table+ shift_step for
        a base variable x and numeric_code for x'
        variable integer coding increases in past steps
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
        for lit in clause.list_of_literals:
            name = lit.name
            if not name[-1] == '`': # t variable
                lit_cod = self.__var_code_table[name] + self.__shift_step
            else:  # t+1 variable
                lit_cod = self.__var_code_table[name[:-1]]
            if not lit.sign:
                lit_cod = - lit_cod
            num_clause.append(lit_cod)
        return num_clause
370

VIGNET Pierre's avatar
VIGNET Pierre committed
371
372
    def __code_clause(self, clause):
        """
373
374
375
        numerically code a clause with the numeric code found in
        self.__var_code_table for variables in the dynamic system and
        self.__aux_code_table for other variables assume all variables
VIGNET Pierre's avatar
VIGNET Pierre committed
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
        are basic variables (t=0)
        @warning: MODIFIES SHIFT_STEP if auxiliary variables are present (numeric code)
        """
        num_clause = []
        for lit in clause.list_of_literals:
            name = lit.name
            if self.__var_code_table.has_key(name):
                var_cod = self.__var_code_table[name]
            elif self.__aux_code_table.has_key(name):
                var_cod = self.__aux_code_table[name]
            else: # create an auxiliary variable - modifies shift_step
                self.__shift_step += 1
                self.__aux_code_table[name] = self.__shift_step
                var_cod = self.__shift_step
                self.__aux_list.append(name)
            if lit.sign:
                lit_code = var_cod
            else:
                lit_code = - var_cod
            num_clause.append(lit_code)
        return num_clause
397

VIGNET Pierre's avatar
VIGNET Pierre committed
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
    # dynamics initialisations
    def __forward_init_dynamic(self):
        """
        set dynamic constraints for a forward one step: X1 = f(X0)
        """
        self.__dynamic_constraints = []
        num_clause_list = []
        for clause in self.__dyn_sys.list_clauses:
            ncl = self.__forward_code(clause)
            num_clause_list.append(ncl)
        if self.__include_aux_clauses:
            for clause in self.__dyn_sys.aux_list_clauses:
                ncl = self.__forward_code(clause)
                num_clause_list.append(ncl)
        self.__dynamic_constraints.append(num_clause_list)
413

VIGNET Pierre's avatar
VIGNET Pierre committed
414
415
416
417
418
419
420
421
422
423
424
425
426
427
    def __backward_init_dynamic(self):
        """
        set dynamic constraints for a forward one step: X0 = f(X1)
        """
        self.__dynamic_constraints = []
        num_clause_list = []
        for clause in self.__dyn_sys.list_clauses:
            ncl = self.__backward_code(clause)
            num_clause_list.append(ncl)
        if self.__include_aux_clauses:
            for clause in self.__dyn_sys.aux_list_clauses:
                ncl = self.__backward_code(clause)
                num_clause_list.append(ncl)
        self.__dynamic_constraints.append(num_clause_list)
428

VIGNET Pierre's avatar
VIGNET Pierre committed
429
430
431
432
433
434
435
    # shifting: implementation of the shift operator
    def __shift_clause(self, ncl):
        """
        shift a clause one step
        @param ncl: DIMACS clause
        @warning: lock the unfolder
        """
436
        self.__locked = True  # shift_step must be frozen
VIGNET Pierre's avatar
VIGNET Pierre committed
437
438
439
440
441
442
443
444
        shift_c = []
        for lit in ncl:
            if lit > 0:
                slit = lit + self.__shift_step
            else:
                slit = lit - self.__shift_step
            shift_c.append(slit)
        return shift_c
445

VIGNET Pierre's avatar
VIGNET Pierre committed
446
447
448
449
    def __m_shift_clause(self, ncl, nb_steps):
        """
        shift a clause many step
        @param ncl: DIMACS clause
450
        @param nb_steps: number of shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
451
452
        @warning: lock the unfolder
        """
453
        self.__locked = True  # shift_step must be frozen
VIGNET Pierre's avatar
VIGNET Pierre committed
454
455
456
457
458
459
460
        shift_c = []
        for lit in ncl:
            if lit > 0:
                slit = lit + self.__shift_step * nb_steps
            else:
                slit = lit - self.__shift_step * nb_steps
            shift_c.append(slit)
461
462
463
464
        return shift_c



VIGNET Pierre's avatar
VIGNET Pierre committed
465
466
467
    def __shift_dynamic(self):
        """
        Shift clauses representing the dynamics X' = f(X,I,C)
468
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
469
470
471
472
473
474
        ldc = self.__dynamic_constraints[-1]
        nlc = []
        for clause in ldc:
            shift_c = self.__shift_clause(clause)
            nlc.append(shift_c)
        self.__dynamic_constraints.append(nlc)
475

VIGNET Pierre's avatar
VIGNET Pierre committed
476
477
478
479
480
481
482
483
484
    def __shift_initial(self):
        """
        Shift initialisation condition
        """
        nic = []
        for clause in self.__initial_constraints:
            shift_c = self.__shift_clause(clause)
            nic.append(shift_c)
        self.__initial_constraints = nic
485

VIGNET Pierre's avatar
VIGNET Pierre committed
486
487
488
489
490
491
492
493
494
    def __shift_final(self):
        """
        Shift final property
        """
        nfc = []
        for clause in self.__final_constraints:
            shift_c = self.__shift_clause(clause)
            nfc.append(shift_c)
        self.__final_constraints = nfc
495

VIGNET Pierre's avatar
VIGNET Pierre committed
496
497
498
499
500
501
502
503
504
505
506
    def __shift_invariant(self):
        """
        Shift invariant property
        """
        if not self.__invariant_constraints == []:
            nltc = []
            ltc = self.__invariant_constraints[-1]
            for clause in ltc:
                shift_c = self.__shift_clause(clause)
                nltc.append(shift_c)
            self.__invariant_constraints.append(nltc)
507

VIGNET Pierre's avatar
VIGNET Pierre committed
508
509
510
    def __shift_variant(self):
        """
        shift variant property - depends on unfolding direction
511
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
512
513
514
515
516
517
518
519
520
521
522
523
524
525
        if not self.__list_variant_constraints:
            return
        if self.__shift_direction == "FORWARD":
            index = self.__current_step # constraint t0 already included
            current_constraint = self.__list_variant_constraints[index]
            # shift constraint at current step and add to var_constraints
            for clause in current_constraint:
                s_clause = self.__m_shift_clause(clause, index)
                self.__variant_constraints.append(s_clause)
                return
        elif self.__shift_direction == 'BACKWARD':
            raise MCLException("Not yet implemented")
        else:
            raise MCLException("Shift incoherent data: "+self.__shift_direction)
526
527


VIGNET Pierre's avatar
VIGNET Pierre committed
528
529
530
531
532
533
534
535
536
537
538
539
540
541
    def shift(self):
        """
        assume shift direction is set - shift one step
        """
        self.__shift_dynamic()
        self.__shift_invariant()
        self.__shift_variant()
        if self.__shift_direction == 'FORWARD':
            self.__shift_final()
        elif self.__shift_direction == 'BACKWARD':
            self.__shift_initial()
        else:
            raise MCLException("Shift incoherent data: "+self.__shift_direction)
        self.__current_step += 1
542

VIGNET Pierre's avatar
VIGNET Pierre committed
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
    # coding of properties
    def __compile_property(self, property_text):
        """
        compile a property (logical formula) into clauses
        type checking uses the symbol table of dyn_sys
        error reporting through the dyn_sys reporter
        MODIFIES __lit_cpt for numbering of auxiliary variables (not coding)
        """
        if self.__locked:
            mess = "Trying to compile property while unfolder is locked"
            raise MCLException(mess)
        reporter = self.__dyn_sys.report
        symb_t = self.__dyn_sys.symb_tab
        # syntax analyser and type checker
        tree_prop = compile_cond(property_text, symb_t, reporter)
558
559
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
560
561
562
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
563

VIGNET Pierre's avatar
VIGNET Pierre committed
564
        # coding of properties
565

VIGNET Pierre's avatar
VIGNET Pierre committed
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
    def __compile_event(self, property_text):
        """
        compile an event (biosignal expression) into clauses
        type checking uses the symbol table of dyn_sys
        error reporting through the dyn_sys reporter
        MODIFIES __lit_cpt for numbering of auxiliary variables (not coding)
        """
        if self.__locked:
            mess = "Trying to compile property while unfolder is locked"
            raise MCLException(mess)
        reporter = self.__dyn_sys.report
        symb_t = self.__dyn_sys.symb_tab
        # syntax analyser and type checker
        (tree_prop, ste, fcl) = compile_event(property_text, symb_t,
                                              True,  reporter)
581
582
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
583
584
585
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
586

VIGNET Pierre's avatar
VIGNET Pierre committed
587
588
    def set_initial_property(self, property_text):
        """
589
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
590
591
        """
        self.__initial_property = property_text
592

VIGNET Pierre's avatar
VIGNET Pierre committed
593
594
595
    def set_dim_initial_property(self, dimacs_clause_list):
        """
        set initial property with a DIMACS representation
596
        @param dimacs_clause_list:
VIGNET Pierre's avatar
VIGNET Pierre committed
597
598
        """
        self.__dim_initial = dimacs_clause_list
599

VIGNET Pierre's avatar
VIGNET Pierre committed
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
    def __init_initial_constraint_0(self, no_frontier_init=True):
        """
        if initial property is set, generate constraints clauses in numeric form
        base variable form - we have to wait until all variables are num coded
        before shifting anything!!
        """
        self.__initial_constraints = []
        if no_frontier_init:
            # initialize no frontier places to False
            for nfp in self.__no_frontier_init:
                self.__initial_constraints.append(nfp)
        if self.__initial_property:
            # compile initial property
            l_clauses = self.__compile_property(self.__initial_property)
            # compile numeric form
            for clause in l_clauses:
                self.__initial_constraints.append(self.__code_clause(clause))
        # dimacs aux initial properties
        dim_init = self.__dim_initial
        if dim_init:
            self.__initial_constraints = self.__initial_constraints + dim_init
621

VIGNET Pierre's avatar
VIGNET Pierre committed
622
623
    def set_final_property(self, property_text):
        """
624
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
625
626
        """
        self.__final_property = property_text
627

VIGNET Pierre's avatar
VIGNET Pierre committed
628
629
630
    def set_dim_final_property(self, dimacs_clause_list):
        """
        set final property with a DIMACS representation
631
632
        @param dimacs_clause_list:
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
633
        self.__dim_final = dimacs_clause_list
634

VIGNET Pierre's avatar
VIGNET Pierre committed
635
636
637
638
639
640
    def __init_final_constraint_0(self):
        """
        if final property is set, generate constraints clauses in numeric form
        base variable used - we have to wait until all variables are num coded
        before shifting anything!!
        """
641

VIGNET Pierre's avatar
VIGNET Pierre committed
642
643
644
645
646
647
648
649
650
651
        self.__final_constraints = []
        if self.__final_property:
            # compile initial (X0) property
            l_clauses = self.__compile_property(self.__final_property)
            # compile numeric form
            for clause in l_clauses:
                self.__final_constraints.append(self.__code_clause(clause))
        dim_fin = self.__dim_final
        if dim_fin:
            self.__final_constraints = self.__final_constraints + dim_fin
652

VIGNET Pierre's avatar
VIGNET Pierre committed
653
654
    def set_current_property(self, property_text):
        """
655
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
656
        """
657

VIGNET Pierre's avatar
VIGNET Pierre committed
658
        self.__invariant_property = property_text
659

VIGNET Pierre's avatar
VIGNET Pierre committed
660
661
662
663
664
    def set_dim_current_property(self, dimacs_clause_list):
        """
        set final property with a DIMACS representation
        @param dimacs_clause_list:
        """
665

VIGNET Pierre's avatar
VIGNET Pierre committed
666
        self.__dim_invariant = dimacs_clause_list
667

VIGNET Pierre's avatar
VIGNET Pierre committed
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
    def __init_invariant_constraint_0(self):
        """
        if trajectory property is set, generate constraints clauses in numeric form
        base variable used - we have to wait until all variables are num coded
        before shifting anything!!
        """
        self.__invariant_constraints = []
        if self.__invariant_property:
            # compile initial (X0) property
            l_clauses = self.__compile_property(self.__invariant_property)
            # compile numeric form
            init_const = []
            for clause in l_clauses:
                init_const.append(self.__code_clause(clause))
            self.__invariant_constraints.append(init_const)
        d_inv = self.__dim_invariant
        if d_inv:
            self.__invariant_constraints = self.__invariant_constraints + d_inv
686

VIGNET Pierre's avatar
VIGNET Pierre committed
687
688
689
690
691
692
693
    def set_variant_property(self, var_prop):
        """
        @param var_prop: a list of logical formulas representing time varying
        constraints. Each constraint uses ground (not shifted) variables.
        The order of the list of constraints is always time increasing.
        """
        self.__variant_property = var_prop
694

VIGNET Pierre's avatar
VIGNET Pierre committed
695
696
    def set_dim_variant_property(self, dim_var_prop):
        """
697
698
        @param dim_var_prop: a list list of dimacs clauses representing time
        varying constraints. Each constraint uses ground (not shifted)
VIGNET Pierre's avatar
VIGNET Pierre committed
699
700
701
        variable codes.
        """
        self.__dim_variant = dim_var_prop
702

VIGNET Pierre's avatar
VIGNET Pierre committed
703
704
    def __init_variant_constraints_0(self):
        """
705
        if variant_property is set, compile each property into clauses and
VIGNET Pierre's avatar
VIGNET Pierre committed
706
707
708
709
710
711
712
713
714
715
716
717
718
719
        encode these clauses. Clauses already in dimacs form are added.
        The two variant constraint forms must be compatible (same length)
        """
        # coding of variant properties
        if self.__variant_property:
            self.__list_variant_constraints = []
            for prop in self.__variant_property:
                # compile initial (X0) property
                l_clauses = self.__compile_event(prop)
                # encode the clauses
                dim_cl = []
                for clause in l_clauses:
                    dim_cl.append(self.__code_clause(clause))
                self.__list_variant_constraints.append(dim_cl)
720

VIGNET Pierre's avatar
VIGNET Pierre committed
721
722
            # add variant properties in dimacs form
            if self.__dim_variant:
723
                vp_length = len(self.__variant_property)
VIGNET Pierre's avatar
VIGNET Pierre committed
724
725
726
                if vp_length != len(self.__dim_variant):
                    mess = "Incoherent variant properties"
                    raise MCLException(mess)
727

VIGNET Pierre's avatar
VIGNET Pierre committed
728
729
730
                for i in range(vp_length):
                    c_var = self.__list_variant_constraints[i]
                    c_var = c_var + self.__dim_variant[i]
731
                    self.__list_variant_constraints[i] = c_var
VIGNET Pierre's avatar
VIGNET Pierre committed
732
733
734
735
736
737
738
739
740
741
742
743
        else:
            if self.__dim_variant:
                self.__list_variant_constraints = self.__dim_variant
        # initialisation
        if self.__list_variant_constraints:
            if self.__shift_direction == "FORWARD":
                self.__variant_constraints = self.__list_variant_constraints[0]
            elif  self.__shift_direction == "BACKWARD":
                raise MCLException("Not yet implemented")
            else:
                raise MCLException("Shift incoherent data: "
                                   + self.__shift_direction)
744

VIGNET Pierre's avatar
VIGNET Pierre committed
745
746
747
748
749
750
751
752
753
754
    # whole initialisations
    def init_forward_unfolding(self):
        """
        initialisation before generating constraints - forward trajectory
        """
        self.__shift_direction = 'FORWARD'
        self.__current_step = 1
        self.__shift_step = self.__shift_step_init  # back to basic!
        self.__aux_code_table = dict()              # flush auxiliary variables
        self.__aux_list = []                        # idem
755

VIGNET Pierre's avatar
VIGNET Pierre committed
756
757
758
759
760
        # init properties to generate all variable num codes
        self.__init_initial_constraint_0()
        self.__init_final_constraint_0()
        self.__init_invariant_constraint_0()
        self.__init_variant_constraints_0()
761

VIGNET Pierre's avatar
VIGNET Pierre committed
762
763
764
765
        # now shifting is possible
        self.__forward_init_dynamic()
        self.__shift_final()
        self.__shift_invariant()
766
767


VIGNET Pierre's avatar
VIGNET Pierre committed
768
769
770
771
772
773
774
775
776
    def init_backward_unfolding(self):
        """
        initialisation before generating constraints - backward trajectory
        """
        self.__shift_direction = 'BACKWARD'
        self.__current_step = 0
        self.__shift_step = self.__shift_step_init  # back to basic!
        self.__aux_code_table = dict()              # flush auxiliary variables
        self.__aux_list = []                        # idem
777

VIGNET Pierre's avatar
VIGNET Pierre committed
778
779
780
781
782
        # init properties to generate all variable num codes
        self.__init_initial_constraint_0()
        self.__init_final_constraint_0()
        self.__init_invariant_constraint_0()
        self.__init_variant_constraints_0()
783

VIGNET Pierre's avatar
VIGNET Pierre committed
784
785
786
787
        # now shifting is possible
        self.__backward_init_dynamic()
        self.__shift_initial()
        self.__shift_invariant()
788

VIGNET Pierre's avatar
VIGNET Pierre committed
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
    # for debug
    def vars_in_clause(self, clause):
        """
        DEBUG
        """
        lvar = []
        for var in clause:
            lvar.append(self.get_var_indexed_name(var))
        return lvar



    # solver interface
    def __load_solver(self, solv):
        """
        add all the current clauses in solver solv
805
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
806
        # final
807
808
809
        LOGGER.debug("Load new solver !!")
        LOGGER.debug(">> final: " + str(len(self.__final_constraints)))
        LOGGER.debug(str(self.__final_constraints))
VIGNET Pierre's avatar
VIGNET Pierre committed
810
811
        for clause in self.__final_constraints:
            solv.add_clause(clause)
812
#            LOGGER.debug(str(clause))
VIGNET Pierre's avatar
VIGNET Pierre committed
813
        # trajectory invariant
814
815
        LOGGER.debug(">> trajectory inv: " + str(len(self.__invariant_constraints)))
        LOGGER.debug(str(self.__invariant_constraints))
VIGNET Pierre's avatar
VIGNET Pierre committed
816
817
818
        for lcl in self.__invariant_constraints:
            for clause in lcl:
                solv.add_clause(clause)
819
#                LOGGER.debug(str(clause))
820

VIGNET Pierre's avatar
VIGNET Pierre committed
821
        # trajectory variant
822
823
        LOGGER.debug(">> trajectory var: " + str(len(self.__variant_constraints)))
        LOGGER.debug(str(self.__variant_constraints))
VIGNET Pierre's avatar
VIGNET Pierre committed
824
825
        for clause in self.__variant_constraints:
            solv.add_clause(clause)
826
#            LOGGER.debug(str(clause))
827

VIGNET Pierre's avatar
VIGNET Pierre committed
828
        # dynamics
829
830
        LOGGER.debug(">> dynamics: " + str(len(self.__dynamic_constraints)))
        LOGGER.debug(str(self.__dynamic_constraints))
VIGNET Pierre's avatar
VIGNET Pierre committed
831
832
833
834
835
        lvars = []
        for lcl in self.__dynamic_constraints:
            for clause in lcl:
                solv.add_clause(clause)
                lvars.append(self.vars_in_clause(clause))
836
#                LOGGER.debug(str(clause))
837
        # initial
838
839
        LOGGER.debug(">> initial: " + str(len(self.__initial_constraints)))
        LOGGER.debug(str(self.__initial_constraints))
VIGNET Pierre's avatar
VIGNET Pierre committed
840
841
        for clause in self.__initial_constraints:
            solv.add_clause(clause)
842
#            LOGGER.debug(str(clause))
VIGNET Pierre's avatar
VIGNET Pierre committed
843

844
845


VIGNET Pierre's avatar
VIGNET Pierre committed
846
847
848
849
    def __constraints_satisfied(self):
        """
        @return: boolean
        """
850
        LOGGER.debug("__constraints_satisfied ?")
VIGNET Pierre's avatar
VIGNET Pierre committed
851
        solver = CryptoMS()
852
        # Load Solver and all clauses
VIGNET Pierre's avatar
VIGNET Pierre committed
853
        self.__load_solver(solver)
854
855
        # If stats are activated (never besides in test environment):
        # sync local data (nb vars, nb clauses with solver state)
VIGNET Pierre's avatar
VIGNET Pierre committed
856
        if self.__stats:
857
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
858
859
860
                self.__nb_vars = solver.nb_vars()
            if solver.nb_clauses() > self.__nb_clauses:
                self.__nb_clauses = solver.nb_clauses()
861
        # Is problem satisfiable ?
VIGNET Pierre's avatar
VIGNET Pierre committed
862
        return solver.is_satisfiable()
863

VIGNET Pierre's avatar
VIGNET Pierre committed
864
865
866
867
868
869
870
871
    def __msolve_constraints(self, max_sol, vvars):
        """
        @param max_sol: int - the max number of solution returned
        @param vvars: variables for which the solver must find different solutions(dimacs code)
        @return: a list of RawSolution
        """
        solver = CryptoMS()
        self.__load_solver(solver)
872
873
        LOGGER.debug("__msolve_constraints :: vvars : " + str(vvars))
        LOGGER.debug("__msolve_constraints :: max_sol : " + str(max_sol))
VIGNET Pierre's avatar
VIGNET Pierre committed
874
        if self.__stats:
875
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
876
                self.__nb_vars = solver.nb_vars()
877
            if solver.nb_clauses() > self.__nb_clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
878
879
                self.__nb_clauses = solver.nb_clauses()
        lintsol = solver.msolve_selected(max_sol, vvars)
880
        LOGGER.debug("__msolve_constraints :: lintsol : " + str(lintsol))
VIGNET Pierre's avatar
VIGNET Pierre committed
881
882
883
884
885
        lsol = []
        for solint in lintsol:
            sol = RawSolution(solint, self)
            lsol.append(sol)
        return lsol
886

VIGNET Pierre's avatar
VIGNET Pierre committed
887
888
889
890
891

    # dynamic properties
    def squery_is_satisfied(self, max_step):
        """
        Ask the SAT solver
892
        @param max_step: int - the horizon
VIGNET Pierre's avatar
VIGNET Pierre committed
893
894
895
896
897
898
899
        """
        # initialization
        self.init_forward_unfolding()
        # horizon adjustment
        if self.__list_variant_constraints:
            max_step = min(max_step, len(self.__list_variant_constraints)-1)
        # loop
900
        if self.__invariant_property and not self.__final_property :
VIGNET Pierre's avatar
VIGNET Pierre committed
901
902
            while self.__current_step <= max_step:
                self.shift()
903
            return self.__constraints_satisfied()
VIGNET Pierre's avatar
VIGNET Pierre committed
904
905
906
907
908
        else :
            while self.__current_step <= max_step:
                if self.__constraints_satisfied():
                    return True
                self.shift()
909
910
911
912
            return self.__constraints_satisfied()



VIGNET Pierre's avatar
VIGNET Pierre committed
913
914
915
916
917
918
    def squery_solve(self, vvars, max_step, max_sol):
        """
        Assert a query is loaded (start_condition, inv_condition, final_condition)
        @param vvars: variables on which different solutions must differ
        @param max_step: bounded horizon for computations
        @param max_sol: max number of solutions to be computed
919
920

        @return: list of RawSolution objects
VIGNET Pierre's avatar
VIGNET Pierre committed
921
        """
922
        LOGGER.debug("squery_solve :: vvars : " + str(vvars))
VIGNET Pierre's avatar
VIGNET Pierre committed
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
        # initialization
        self.init_forward_unfolding()
        # horizon adjustment
        if self.__list_variant_constraints:
            max_step = min(max_step, len(self.__list_variant_constraints)-1)
        # loop
        if self.__invariant_property and not self.__final_property :
            while self.__current_step <= max_step:
                self.shift()
            l_rawsol = self.__msolve_constraints(max_sol, vvars)
            return l_rawsol
        else : # reachability
            l_rawsol = []
            # check and correct for incoherent data on step number
            if self.__steps_before_check > max_step:
                self.__steps_before_check = max_step - 1
            # shift without checking (optimization)
            while self.__current_step <= self.__steps_before_check:
                self.shift()
            # search for solutions at each step
            while self.__current_step <= max_step:
                lsol = self.__msolve_constraints(max_sol, vvars)
                if len(lsol)>0:
                    l_rawsol = l_rawsol + lsol
                self.shift()
            return l_rawsol
949

VIGNET Pierre's avatar
VIGNET Pierre committed
950
951
952
953
954
955

###############################################################################
class CLPropertyVisitor(object):
    """
    SigExpression on states and events into a set of clauses
    Type checking must be done.
956
957
    """

VIGNET Pierre's avatar
VIGNET Pierre committed
958
959
960
961
    def __init__(self, aux_cpt=0):
        self.cpt = aux_cpt         # for auxiliary variable naming
        self.clauses = []          # generated clauses
        self.top = True            # root of the formula?
962

VIGNET Pierre's avatar
VIGNET Pierre committed
963
964
965
966
967
968
969
970
971
972
    def visit_sig_ident(self, tnode):
        """
        ident -> literal
        """
        name = tnode.name
        new_lit = Literal(name, True)
        if self.top:
            self.clauses.append(Clause([new_lit]))
            return None
        return new_lit
973

VIGNET Pierre's avatar
VIGNET Pierre committed
974
975
976
977
978
979
980
981
982
983
984
985
986
    def visit_sig_not(self, node):
        """
        translate a not
        """
        top = self.top
        self.top = False
        # compile operand to nl <=> formula
        newl = node.operand.accept(self)
        notnl = newl.lit_not()
        if top: # we are at the root
            self.clauses.append(Clause([notnl]))
            return None
        return notnl # if we are not at the root
987

VIGNET Pierre's avatar
VIGNET Pierre committed
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
    def visit_sig_sync(self, binnode):
        """
        translate a binary (or/and) expression
        """
        top = self.top
        self.top = False
        # the internal nodes will be affected with the name '_lit'
        name = '_lit'+str(self.cpt)
        self.cpt += 1
        newl = Literal(name, True)
        notnl = Literal(name, False)
        # recursive visits
        operator = binnode.operator
        nl1 = binnode.left_h.accept(self)
        notnl1 = nl1.lit_not()
        nl2 = binnode.right_h.accept(self)
        notnl2 = nl2.lit_not()
        # clauses generation
        if operator == 'and':   # x = lh and rh
            cl1 = Clause([nl1, notnl])           # not x or not lh
            cl2 = Clause([nl2, notnl])           # not x or not rh
            cl3 = Clause([notnl1, notnl2, newl]) # x or not lh or not rh

        if operator == 'or':    # x = lh or rh
            cl1 = Clause([notnl1, newl])        # x or not lh
            cl2 = Clause([notnl2, newl])        # x or not rh
            cl3 = Clause([nl1, nl2, notnl])     # not x or not lh or not rh

        self.clauses.append(cl1)
        self.clauses.append(cl2)
        self.clauses.append(cl3)
        if top:
            self.clauses.append(Clause([newl]))
            return None
        return newl
1023

VIGNET Pierre's avatar
VIGNET Pierre committed
1024
1025
1026
1027
1028
1029
1030
1031
1032
    def visit_sig_const(self, exp):
        """
        translate a constant expression
        """
        top = self.top
        if top:
            if exp.is_const_false():
                raise TypeError("No constant False property allowed")
            else: # always present or satisfied
1033
                return None
VIGNET Pierre's avatar
VIGNET Pierre committed
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
        # the internal nodes will be affected with the name '_lit'
        name = '_lit'+str(self.cpt)
        self.cpt += 1
        newl = Literal(name, True)

        # clause generation
        if exp.value:
            clause = newl  # x = True
        else:
            clause = newl.lit_not()
        self.clauses.append(Clause([clause]))
        return newl

    # time operators
    def visit_sig_default(self, exp):
        """
        default translation
        """
        top = self.top
        self.top = False
        # the internal nodes will be affected the name '_lit'
        name = '_lit'+str(self.cpt)
        self.cpt += 1
        newl = Literal(name, True)
        notnl = Literal(name, False)
        # recursive visits
        nl1 = exp.left_h.accept(self)
        notnl1 = nl1.lit_not()
        nl2 = exp.right_h.accept(self)
        notnl2 = nl2.lit_not()
        # clause generation: x = lh or rh
        cl1 = Clause([notnl1, newl])        # x or not lh
        cl2 = Clause([notnl2, newl])        # x or not rh
        cl3 = Clause([nl1, nl2, notnl])     # not x or not lh or not rh
1068

VIGNET Pierre's avatar
VIGNET Pierre committed
1069
1070
1071
1072
1073
1074
1075
        self.clauses.append(cl1)
        self.clauses.append(cl2)
        self.clauses.append(cl3)
        if top:
            self.clauses.append(Clause([newl]))
            return None
        return newl
1076

VIGNET Pierre's avatar
VIGNET Pierre committed
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
    def visit_sig_when(self, exp):
        """
        when translation
        """
        top = self.top
        self.top = False
        # the internal nodes will be affected the name '_lit'
        name = '_lit'+str(self.cpt)
        self.cpt += 1
        newl = Literal(name, True)
        notnl = Literal(name, False)
        # recursive visits
        nl1 = exp.left_h.accept(self)
        notnl1 = nl1.lit_not()
        nl2 = exp.right_h.accept(self)
        notnl2 = nl2.lit_not()
        # clause generation: x = lh and rh
        cl1 = Clause([nl1, notnl])           # not x or not lh
        cl2 = Clause([nl2, notnl])           # not x or not rh
        cl3 = Clause([notnl1, notnl2, newl]) # x or not lh or not rh

        self.clauses.append(cl1)
        self.clauses.append(cl2)
        self.clauses.append(cl3)
        if top:
            self.clauses.append(Clause([newl]))
            return None
        return newl
1105