CLUnfolder.py 39.6 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
from cadbiom import commons as cm
51
from logging import DEBUG
52
53

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

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
63
64
    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
65
    to add variables while generating a trajectory unfolding.
66
67

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

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

        # shift_step equal to the total number of coded variables
VIGNET Pierre's avatar
VIGNET Pierre committed
80
81
82
83
84
85
        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
86

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

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
119
120
121
122
123
        # 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()
124

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

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

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
197
198
199
200
201
202
203
    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
204

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
316
317
318
319
320
    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
321

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

328
329


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

VIGNET Pierre's avatar
VIGNET Pierre committed
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
    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
371

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

VIGNET Pierre's avatar
VIGNET Pierre committed
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
    # 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)
414

VIGNET Pierre's avatar
VIGNET Pierre committed
415
416
417
418
419
420
421
422
423
424
425
426
427
428
    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)
429

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

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



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

VIGNET Pierre's avatar
VIGNET Pierre committed
477
478
479
480
481
482
483
484
485
    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
486

VIGNET Pierre's avatar
VIGNET Pierre committed
487
488
489
490
491
492
493
494
495
    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
496

VIGNET Pierre's avatar
VIGNET Pierre committed
497
498
499
500
501
502
503
504
505
506
507
    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)
508

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


VIGNET Pierre's avatar
VIGNET Pierre committed
529
530
531
532
533
534
535
536
537
538
539
540
541
542
    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
543

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

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

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

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

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
636
637
638
639
640
641
    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!!
        """
642

VIGNET Pierre's avatar
VIGNET Pierre committed
643
644
645
646
647
648
649
650
651
652
        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
653

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
    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
687

VIGNET Pierre's avatar
VIGNET Pierre committed
688
689
690
691
692
693
694
    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
695

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
746
747
748
749
750
751
752
753
754
755
    # 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
756

VIGNET Pierre's avatar
VIGNET Pierre committed
757
758
759
760
761
        # 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()
762

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


VIGNET Pierre's avatar
VIGNET Pierre committed
769
770
771
772
773
774
775
776
777
    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
778

VIGNET Pierre's avatar
VIGNET Pierre committed
779
780
781
782
783
        # 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()
784

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

VIGNET Pierre's avatar
VIGNET Pierre committed
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
        [solv.add_clause(clause) for clause in self.__final_constraints]

VIGNET Pierre's avatar
VIGNET Pierre committed
809
        # trajectory invariant
810
811
        [solv.add_clause(clause) for lcl in self.__invariant_constraints
         for clause in lcl]
812

VIGNET Pierre's avatar
VIGNET Pierre committed
813
        # trajectory variant
814
        [solv.add_clause(clause) for clause in self.__variant_constraints]
815

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

826
        # initial
827
        [solv.add_clause(clause) for clause in self.__initial_constraints]
VIGNET Pierre's avatar
VIGNET Pierre committed
828

829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
        # LOGGING
        if LOGGER.getEffectiveLevel() == DEBUG:
            # final
            LOGGER.debug("Load new solver !!")
            LOGGER.debug(">> final: " + str(len(self.__final_constraints)))
            LOGGER.debug(str(self.__final_constraints))

            # trajectory invariant
            LOGGER.debug(">> trajectory inv: " + str(len(self.__invariant_constraints)))
            LOGGER.debug(str(self.__invariant_constraints))

            # trajectory variant
            LOGGER.debug(">> trajectory var: " + str(len(self.__variant_constraints)))
            LOGGER.debug(str(self.__variant_constraints))

            # dynamics
            LOGGER.debug(">> dynamics: " + str(len(self.__dynamic_constraints)))
            LOGGER.debug(str(self.__dynamic_constraints))

            # initial
            LOGGER.debug(">> initial: " + str(len(self.__initial_constraints)))
            LOGGER.debug(str(self.__initial_constraints))
851
852


VIGNET Pierre's avatar
VIGNET Pierre committed
853
854
855
856
    def __constraints_satisfied(self):
        """
        @return: boolean
        """
857
        LOGGER.debug("__constraints_satisfied ?")
VIGNET Pierre's avatar
VIGNET Pierre committed
858
        solver = CryptoMS()
859
        # Load Solver and all clauses
VIGNET Pierre's avatar
VIGNET Pierre committed
860
        self.__load_solver(solver)
861
862
        # 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
863
        if self.__stats:
864
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
865
866
867
                self.__nb_vars = solver.nb_vars()
            if solver.nb_clauses() > self.__nb_clauses:
                self.__nb_clauses = solver.nb_clauses()
868
        # Is problem satisfiable ?
VIGNET Pierre's avatar
VIGNET Pierre committed
869
        return solver.is_satisfiable()
870

871

VIGNET Pierre's avatar
VIGNET Pierre committed
872
873
874
875
876
877
878
879
    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)
880
881
882
        if LOGGER.getEffectiveLevel() == DEBUG:
            LOGGER.debug("__msolve_constraints :: vvars : " + str(vvars))
            LOGGER.debug("__msolve_constraints :: max_sol : " + str(max_sol))
VIGNET Pierre's avatar
VIGNET Pierre committed
883
        if self.__stats:
884
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
885
                self.__nb_vars = solver.nb_vars()
886
            if solver.nb_clauses() > self.__nb_clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
887
888
                self.__nb_clauses = solver.nb_clauses()
        lintsol = solver.msolve_selected(max_sol, vvars)
889
890
        if LOGGER.getEffectiveLevel() == DEBUG:
            LOGGER.debug("__msolve_constraints :: lintsol : " + str(lintsol))
VIGNET Pierre's avatar
VIGNET Pierre committed
891
892
893
894
895
        lsol = []
        for solint in lintsol:
            sol = RawSolution(solint, self)
            lsol.append(sol)
        return lsol
896

VIGNET Pierre's avatar
VIGNET Pierre committed
897
898
899
900
901

    # dynamic properties
    def squery_is_satisfied(self, max_step):
        """
        Ask the SAT solver
902
        @param max_step: int - the horizon
VIGNET Pierre's avatar
VIGNET Pierre committed
903
904
905
906
907
908
909
        """
        # initialization
        self.init_forward_unfolding()
        # horizon adjustment
        if self.__list_variant_constraints:
            max_step = min(max_step, len(self.__list_variant_constraints)-1)
        # loop
910
        if self.__invariant_property and not self.__final_property :
VIGNET Pierre's avatar
VIGNET Pierre committed
911
912
            while self.__current_step <= max_step:
                self.shift()
913
            return self.__constraints_satisfied()
VIGNET Pierre's avatar
VIGNET Pierre committed
914
915
916
917
918
        else :
            while self.__current_step <= max_step:
                if self.__constraints_satisfied():
                    return True
                self.shift()
919
920
921
922
            return self.__constraints_satisfied()



VIGNET Pierre's avatar
VIGNET Pierre committed
923
924
925
926
927
928
    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
929
930

        @return: list of RawSolution objects
VIGNET Pierre's avatar
VIGNET Pierre committed
931
        """
932
933
        if LOGGER.getEffectiveLevel() == DEBUG:
            LOGGER.debug("squery_solve :: vvars : " + str(vvars))
VIGNET Pierre's avatar
VIGNET Pierre committed
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
        # 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
960

VIGNET Pierre's avatar
VIGNET Pierre committed
961
962
963
964
965
966

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

VIGNET Pierre's avatar
VIGNET Pierre committed
969
970
971
972
    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?
973

VIGNET Pierre's avatar
VIGNET Pierre committed
974
975
976
977
978
979
980
981
982
983
    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
984

VIGNET Pierre's avatar
VIGNET Pierre committed
985
986
987
988
989
990
991
992
993
994
995
996
997
    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
998

VIGNET Pierre's avatar
VIGNET Pierre committed
999
1000
1001
1002
1003
1004
1005
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
    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
1034

VIGNET Pierre's avatar
VIGNET Pierre committed
1035
1036
1037
1038
1039
1040
1041
1042
1043
    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
1044
                return None
VIGNET Pierre's avatar
VIGNET Pierre committed
1045
1046
1047
1048
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
1077
1078
        # 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
1079

VIGNET Pierre's avatar
VIGNET Pierre committed
1080
1081
1082
1083
1084
1085
1086
        self.clauses.append(cl1)
        self.clauses.append(cl2)
        self.clauses.append(cl3)
        if top:
            self.clauses.append(Clause([newl]))
            return None
        return newl
1087

VIGNET Pierre's avatar
VIGNET Pierre committed
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
    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
1116