CLUnfolder.py 37.9 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
53
54
55
56
57
58


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
59
60
    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
61
    to add variables while generating a trajectory unfolding.
62
63

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

VIGNET Pierre's avatar
VIGNET Pierre committed
72
73
    def __init__(self, sys):
        self.__dyn_sys = sys # symbolic clause dynamic system
74
75

        # shift_step equal to the total number of coded variables
VIGNET Pierre's avatar
VIGNET Pierre committed
76
77
78
79
80
81
        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
82

VIGNET Pierre's avatar
VIGNET Pierre committed
83
84
        # assign a DIMACS code number to each variable (invariant)
        self.__lit_cpt = self.__shift_step +1 # counter for aux. var. coding
85
        self.__var_code_table = dict()            # name -> DIMACS code
VIGNET Pierre's avatar
VIGNET Pierre committed
86
87
88
89
90
91
92
        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)
93

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
103
104
105
106
107
        # 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()
108

VIGNET Pierre's avatar
VIGNET Pierre committed
109
110
111
112
113
        # 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()
114

VIGNET Pierre's avatar
VIGNET Pierre committed
115
116
117
118
119
        # 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()
120

VIGNET Pierre's avatar
VIGNET Pierre committed
121
122
123
124
        # properties to be checked
        self.__initial_property = None            # string
        self.__dim_initial = None                 # list of dimacs clauses
        self.__final_property = None              # idem
125
        self.__dim_final = None
VIGNET Pierre's avatar
VIGNET Pierre committed
126
127
128
129
130
131
        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>>
132
133

        # constraints - logical constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
        # 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
156
        self.__dim_final = None
VIGNET Pierre's avatar
VIGNET Pierre committed
157
158
159
160
161
162
        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
163
        self.__shift_direction = None
VIGNET Pierre's avatar
VIGNET Pierre committed
164
        self.__locked = False
165

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

VIGNET Pierre's avatar
VIGNET Pierre committed
174
175
176
177
178
    def unset_stats(self):
        """
        disable solver statistics
        """
        self.__stats = False
179

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
193
194
195
196
197
198
199
    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
200

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

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

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

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

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
251
252
253
    def get_var_name(self, var_num):
        """
        @param var_num: DIMACS literal coding of an initial variable
254
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
255
        """
256
        if var_num < 0:
VIGNET Pierre's avatar
VIGNET Pierre committed
257
258
259
260
261
262
263
264
            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")
265

VIGNET Pierre's avatar
VIGNET Pierre committed
266
267
268
269
270
    def get_var_indexed_name(self, var_num):
        """
        @param var_num: DIMACS literal coding
        @return: name of the variable with time index
        """
271
        if var_num < 0:
VIGNET Pierre's avatar
VIGNET Pierre committed
272
273
274
275
276
277
278
279
280
            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
281

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
306
307
308
309
310
    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
311

VIGNET Pierre's avatar
VIGNET Pierre committed
312
313
314
315
316
    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
317

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

324
325


VIGNET Pierre's avatar
VIGNET Pierre committed
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
    # 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
347

VIGNET Pierre's avatar
VIGNET Pierre committed
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
    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
367

VIGNET Pierre's avatar
VIGNET Pierre committed
368
369
    def __code_clause(self, clause):
        """
370
371
372
        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
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
        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
394

VIGNET Pierre's avatar
VIGNET Pierre committed
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
    # 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)
410

VIGNET Pierre's avatar
VIGNET Pierre committed
411
412
413
414
415
416
417
418
419
420
421
422
423
424
    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)
425

VIGNET Pierre's avatar
VIGNET Pierre committed
426
427
428
429
430
431
432
    # shifting: implementation of the shift operator
    def __shift_clause(self, ncl):
        """
        shift a clause one step
        @param ncl: DIMACS clause
        @warning: lock the unfolder
        """
433
        self.__locked = True  # shift_step must be frozen
VIGNET Pierre's avatar
VIGNET Pierre committed
434
435
436
437
438
439
440
441
        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
442

VIGNET Pierre's avatar
VIGNET Pierre committed
443
444
445
446
    def __m_shift_clause(self, ncl, nb_steps):
        """
        shift a clause many step
        @param ncl: DIMACS clause
447
        @param nb_steps: number of shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
448
449
        @warning: lock the unfolder
        """
450
        self.__locked = True  # shift_step must be frozen
VIGNET Pierre's avatar
VIGNET Pierre committed
451
452
453
454
455
456
457
        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)
458
459
460
461
        return shift_c



VIGNET Pierre's avatar
VIGNET Pierre committed
462
463
464
    def __shift_dynamic(self):
        """
        Shift clauses representing the dynamics X' = f(X,I,C)
465
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
466
467
468
469
470
471
        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)
472

VIGNET Pierre's avatar
VIGNET Pierre committed
473
474
475
476
477
478
479
480
481
    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
482

VIGNET Pierre's avatar
VIGNET Pierre committed
483
484
485
486
487
488
489
490
491
    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
492

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

VIGNET Pierre's avatar
VIGNET Pierre committed
505
506
507
    def __shift_variant(self):
        """
        shift variant property - depends on unfolding direction
508
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
509
510
511
512
513
514
515
516
517
518
519
520
521
522
        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)
523
524


VIGNET Pierre's avatar
VIGNET Pierre committed
525
526
527
528
529
530
531
532
533
534
535
536
537
538
    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
539

VIGNET Pierre's avatar
VIGNET Pierre committed
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
    # 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)
555
556
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
557
558
559
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
560

VIGNET Pierre's avatar
VIGNET Pierre committed
561
        # coding of properties
562

VIGNET Pierre's avatar
VIGNET Pierre committed
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
    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)
578
579
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
580
581
582
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
583

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
    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
618

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
632
633
634
635
636
637
    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!!
        """
638

VIGNET Pierre's avatar
VIGNET Pierre committed
639
640
641
642
643
644
645
646
647
648
        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
649

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

VIGNET Pierre's avatar
VIGNET Pierre committed
655
        self.__invariant_property = property_text
656

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

VIGNET Pierre's avatar
VIGNET Pierre committed
663
        self.__dim_invariant = dimacs_clause_list
664

VIGNET Pierre's avatar
VIGNET Pierre committed
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
    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
683

VIGNET Pierre's avatar
VIGNET Pierre committed
684
685
686
687
688
689
690
    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
691

VIGNET Pierre's avatar
VIGNET Pierre committed
692
693
    def set_dim_variant_property(self, dim_var_prop):
        """
694
695
        @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
696
697
698
        variable codes.
        """
        self.__dim_variant = dim_var_prop
699

VIGNET Pierre's avatar
VIGNET Pierre committed
700
701
    def __init_variant_constraints_0(self):
        """
702
        if variant_property is set, compile each property into clauses and
VIGNET Pierre's avatar
VIGNET Pierre committed
703
704
705
706
707
708
709
710
711
712
713
714
715
716
        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)
717

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

VIGNET Pierre's avatar
VIGNET Pierre committed
725
726
727
                for i in range(vp_length):
                    c_var = self.__list_variant_constraints[i]
                    c_var = c_var + self.__dim_variant[i]
728
                    self.__list_variant_constraints[i] = c_var
VIGNET Pierre's avatar
VIGNET Pierre committed
729
730
731
732
733
734
735
736
737
738
739
740
        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)
741

VIGNET Pierre's avatar
VIGNET Pierre committed
742
743
744
745
746
747
748
749
750
751
    # 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
752

VIGNET Pierre's avatar
VIGNET Pierre committed
753
754
755
756
757
        # 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()
758

VIGNET Pierre's avatar
VIGNET Pierre committed
759
760
761
762
        # now shifting is possible
        self.__forward_init_dynamic()
        self.__shift_final()
        self.__shift_invariant()
763
764


VIGNET Pierre's avatar
VIGNET Pierre committed
765
766
767
768
769
770
771
772
773
    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
774

VIGNET Pierre's avatar
VIGNET Pierre committed
775
776
777
778
779
        # 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()
780

VIGNET Pierre's avatar
VIGNET Pierre committed
781
782
783
784
        # now shifting is possible
        self.__backward_init_dynamic()
        self.__shift_initial()
        self.__shift_invariant()
785

VIGNET Pierre's avatar
VIGNET Pierre committed
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
    # 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
802
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
803
804
805
806
807
808
809
        # final
        for clause in self.__final_constraints:
            solv.add_clause(clause)
        # trajectory invariant
        for lcl in self.__invariant_constraints:
            for clause in lcl:
                solv.add_clause(clause)
810

VIGNET Pierre's avatar
VIGNET Pierre committed
811
812
813
        # trajectory variant
        for clause in self.__variant_constraints:
            solv.add_clause(clause)
814

VIGNET Pierre's avatar
VIGNET Pierre committed
815
816
817
818
819
820
        # dynamics
        lvars = []
        for lcl in self.__dynamic_constraints:
            for clause in lcl:
                solv.add_clause(clause)
                lvars.append(self.vars_in_clause(clause))
821
        # initial
VIGNET Pierre's avatar
VIGNET Pierre committed
822
823
824
        for clause in self.__initial_constraints:
            solv.add_clause(clause)

825
826


VIGNET Pierre's avatar
VIGNET Pierre committed
827
828
829
830
831
832
833
    def __constraints_satisfied(self):
        """
        @return: boolean
        """
        solver = CryptoMS()
        self.__load_solver(solver)
        if self.__stats:
834
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
835
836
837
838
                self.__nb_vars = solver.nb_vars()
            if solver.nb_clauses() > self.__nb_clauses:
                self.__nb_clauses = solver.nb_clauses()
        return solver.is_satisfiable()
839

VIGNET Pierre's avatar
VIGNET Pierre committed
840
841
842
843
844
845
846
847
848
    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)
        if self.__stats:
849
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
850
                self.__nb_vars = solver.nb_vars()
851
            if solver.nb_clauses() > self.__nb_clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
852
853
854
855
856
857
858
                self.__nb_clauses = solver.nb_clauses()
        lintsol = solver.msolve_selected(max_sol, vvars)
        lsol = []
        for solint in lintsol:
            sol = RawSolution(solint, self)
            lsol.append(sol)
        return lsol
859

VIGNET Pierre's avatar
VIGNET Pierre committed
860
861
862
863
864

    # dynamic properties
    def squery_is_satisfied(self, max_step):
        """
        Ask the SAT solver
865
        @param max_step: int - the horizon
VIGNET Pierre's avatar
VIGNET Pierre committed
866
867
868
869
870
871
872
        """
        # initialization
        self.init_forward_unfolding()
        # horizon adjustment
        if self.__list_variant_constraints:
            max_step = min(max_step, len(self.__list_variant_constraints)-1)
        # loop
873
        if self.__invariant_property and not self.__final_property :
VIGNET Pierre's avatar
VIGNET Pierre committed
874
875
            while self.__current_step <= max_step:
                self.shift()
876
            return self.__constraints_satisfied()
VIGNET Pierre's avatar
VIGNET Pierre committed
877
878
879
880
881
        else :
            while self.__current_step <= max_step:
                if self.__constraints_satisfied():
                    return True
                self.shift()
882
883
884
885
            return self.__constraints_satisfied()



VIGNET Pierre's avatar
VIGNET Pierre committed
886
887
888
889
890
891
    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
892
893

        @return: list of RawSolution objects
VIGNET Pierre's avatar
VIGNET Pierre committed
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
        """
        # 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
921

VIGNET Pierre's avatar
VIGNET Pierre committed
922
923
924
925
926
927

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

VIGNET Pierre's avatar
VIGNET Pierre committed
930
931
932
933
    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?
934

VIGNET Pierre's avatar
VIGNET Pierre committed
935
936
937
938
939
940
941
942
943
944
    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
945

VIGNET Pierre's avatar
VIGNET Pierre committed
946
947
948
949
950
951
952
953
954
955
956
957
958
    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
959

VIGNET Pierre's avatar
VIGNET Pierre committed
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
    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
995

VIGNET Pierre's avatar
VIGNET Pierre committed
996
997
998
999
1000
1001
1002
1003
1004
    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
1005
                return None
VIGNET Pierre's avatar
VIGNET Pierre committed
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
        # 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
1040

VIGNET Pierre's avatar
VIGNET Pierre committed
1041
1042
1043
1044
1045
1046
1047
        self.clauses.append(cl1)
        self.clauses.append(cl2)
        self.clauses.append(cl3)
        if top:
            self.clauses.append(Clause([newl]))
            return None
        return newl
1048

VIGNET Pierre's avatar
VIGNET Pierre committed
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
    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
1077