CLUnfolder.py 54.4 KB
Newer Older
VIGNET Pierre's avatar
VIGNET Pierre committed
1
# -*- coding: utf-8 -*-
VIGNET Pierre's avatar
VIGNET Pierre committed
2
3
4
## Filename    : CLUnfolder.py
## Author(s)   : Michel Le Borgne
## Created     : 22 mars 2012
5
6
## Revision    :
## Source      :
VIGNET Pierre's avatar
VIGNET Pierre committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
##
## Copyright 2012 : IRISA/IRSET
##
## This library is free software; you can redistribute it and/or modify it
## under the terms of the GNU General Public License as published
## by the Free Software Foundation; either version 2.1 of the License, or
## any later version.
##
## This library is distributed in the hope that it will be useful, but
## WITHOUT ANY WARRANTY, WITHOUT EVEN THE IMPLIED WARRANTY OF
## MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE.  The software and
## documentation provided here under is on an "as is" basis, and IRISA has
## no obligations to provide maintenance, support, updates, enhancements
## or modifications.
## In no event shall IRISA be liable to any party for direct, indirect,
## special, incidental or consequential damages, including lost profits,
## arising out of the use of this software and its documentation, even if
## IRISA have been advised of the possibility of such damage.  See
## the GNU General Public License for more details.
##
## You should have received a copy of the GNU General Public License
## along with this library; if not, write to the Free Software Foundation,
## Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
##
## The original code contained here was initially developed by:
##
##     Michel Le Borgne.
##     IRISA
##     Symbiose team
##     IRISA  Campus de Beaulieu
37
38
##     35042 RENNES Cedex, FRANCE
##
VIGNET Pierre's avatar
VIGNET Pierre committed
39
40
41
42
43
44
##
## Contributor(s): Geoffroy Andrieux IRSET
##
"""
Main engine for constraint unfolding and solving
"""
45
46
from __future__ import print_function

VIGNET Pierre's avatar
VIGNET Pierre committed
47
48
#from pyCryptoMS import CryptoMS
from pycryptosat import Solver as CryptoMS
49
50
51
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
52
from cadbiom import commons as cm
VIGNET Pierre's avatar
VIGNET Pierre committed
53
54
55
56
57
58

# C++ API
from _cadbiom import shift_clause, shift_dynamic, forward_code, \
                     forward_init_dynamic

# Standard imports
59
from logging import DEBUG
VIGNET Pierre's avatar
VIGNET Pierre committed
60
import itertools as it
61
62

LOGGER = cm.logger()
VIGNET Pierre's avatar
VIGNET Pierre committed
63
64
65

class CLUnfolder(object):
    """
66
67
68
69
70
71
72
73
74
    When loading a model in a MCLAnalyser object, a CLUnfolder is generated which
    implies the compilation of the dynamical system into a clause constraint
    dynamical system and the DIMACS coding of all the variables.
    This coding cannot be changed later.
    The unfolding of constraints is performed efficiently on the numeric form
    of the clause constraints. The CLUnfolder provide various method to convert
    variable names to DIMACS code and back, to extract the frontier of a model
    and to extract informations from raw solutions.

VIGNET Pierre's avatar
VIGNET Pierre committed
75
76
77
78
    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).
VIGNET Pierre's avatar
VIGNET Pierre committed
79

VIGNET Pierre's avatar
VIGNET Pierre committed
80
81
    During unfolding, clauses are shifted either to the future (forward) or
    to the past (backward). The shift operator is a simple addition
82
83
    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
84
    to add variables while generating a trajectory unfolding.
85
86

    Glossary
VIGNET Pierre's avatar
VIGNET Pierre committed
87
88
89
    ========
    - ground variables/ground dimacs code: variables at time 0/their encoding.
    - solution: a solution of the logical dynamic constraint from SAT solver
90
    - state vector: list of DIMACS code of original (not shifted) variables
VIGNET Pierre's avatar
VIGNET Pierre committed
91
92
93
      corresponding to a step.
    - trajectory: list of state_vectors
    """
94

95
96
97
98
99
    def __init__(self, dynamic_system):
        """
        :param dynamic_system: Describe a dynamic system in clause form.
        :type dynamic_system: <CLDynSys>
        """
100
        self.dynamic_system = dynamic_system # symbolic clause dynamic system
101

102
103
        # shift_step equals to the total number of coded variables
        # (including inputs, entities, clocks/events, auxiliary variables)
104
        # shift_step_init: the shift step ss (if n is X_0 code, n+ss is X_1 code)
105
106
107
108
109
110
111
112
        self.shift_step_init = dynamic_system.get_var_number() # shift step of system (number of variables of the system)
        self.__shift_step = self.shift_step_init  # current shift/step

        # self.shift_step must be frozen in order to avoid problems during the
        # unflatten() step of RawSolutions.
        # => Each step MUST have the same number of variables.
        # Thus, we lock the Unfolder by turning self.__locked to True.
        # See __shift_clause() and __m_shift_clause()
VIGNET Pierre's avatar
VIGNET Pierre committed
113
        self.__locked = False
114
115
116
        self.__current_step = 1                   # current number of unfolding
        # For reachability optimisation. Number of shifts before checking
        # the final property
VIGNET Pierre's avatar
VIGNET Pierre committed
117
        self.__steps_before_check = 0
118

VIGNET Pierre's avatar
VIGNET Pierre committed
119
        # assign a DIMACS code number to each variable (invariant)
120
121
        # Create mappings between names and values of the variables of the system
        # dynamic_system.base_var_set : Set of ALL variables of the dynamic system
122
        # (including inputs, entities, clocks/events, auxiliary variables).
123
124
        self.__var_code_table = dict()     # Mapping: name -> DIMACS code (!= 0)
        self.__var_list = ['##']           # Mapping: DIMACS code (!= 0) -> name
125
126

        # Fix order of variables names with a list:
127
128
        # - indexes of __var_list are the values of the variables at these indexes
        # - values begin from 1 (0 is a blacklisted value)
129
130
        base_var_set = list(dynamic_system.base_var_set)
        self.__var_list += base_var_set
131
        # keys: are the names of the variables, values: their values
132
133
134
135
        self.__var_code_table = {var_name: var_num for var_num, var_name in enumerate(base_var_set, 1)}

        assert len(self.__var_code_table) == self.__shift_step

136
137
138
139
140
        # 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 = True
        self.__lit_cpt = self.__shift_step + 1    # counter for aux. var. coding
141

142
143
144
145
        # Same mapping tools for auxiliary variables introduced by properties
        # compilation
        # Cf __code_clause()
        self.__aux_code_table = dict()            # name to code
VIGNET Pierre's avatar
VIGNET Pierre committed
146
        self.__aux_list = []                      # code to name
147

148
149
        # ordered list of DIMACS codes of the simple variables/places
        # Disable all variables of places (entities) in the model (except frontiers)
150
        self.__no_frontier_init = [[-self.__var_code_table[nfp]] for nfp in self.dynamic_system.no_frontiers]
151

152
153
        # ordered list of DIMACS codes of the frontier variables/places
        self.frontier_values = [self.__var_code_table[frp] for frp in self.__dyn_sys.frontiers]
154
        self.frontier_values.sort() ## TODO: sort utile ici ???? si non passer en frozenset et supprimer les casts partout ailleurs
155
156
        # Convenient attribute for RawSolution.extract_frontier_values()
        # all frontiers and their opposite version
157
        # Set of frontier positive and negative values.
158
        # operations with sets are much faster
159
160
        ## plus forcément nécessaire... ou passer avec une @property et un lrucache dessus
        ## ou mieux juste un attr avec les frontières négatives,
161
        ## utilisé dans RawSolution.frontier_pos_and_neg_values pour faire l'intersection avec les variables d'une solution
162
163
164
165
166
167
        ## utilisé dans MCLAnalyser.__solve_with_inact_fsolution directement en utilisant l'objet unfolder
        self.frontiers_negative_values = frozenset(-frontier for frontier in self.frontier_values)
        self.frontiers_pos_and_neg = \
            self.frontiers_negative_values | frozenset(self.frontier_values)

        # DIMACS codes of the input variables/places for extraction (inv)
168
        self.__inputs = frozenset(self.__var_code_table[inp] for inp in self.dynamic_system.inputs)
169

170
        # DIMACS codes of the free_clocks variables/places for extraction (invariant)
171
        self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.dynamic_system.free_clocks)
172
173

        # Binding for a merged version of __inputs and __free_clocks
174
        # Convenient attribute for RawSolution.extract_act_input_clock_seq()
175
176
        # DIMACS codes of the input and free_clocks variables
        self.inputs_and_free_clocks = self.__inputs | self.__free_clocks
177

178
179
        # Properties to be checked
        self.reset()
180

181
        # Logical constraints:
VIGNET Pierre's avatar
VIGNET Pierre committed
182
        # result from unfolding of base constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
183
184
185
186
187
        # Boolean vectors signification:
        # X: Current state of places (activated/unactivated)
        # X': Future state of places
        # H: Current 'free' events (present/not present) => ?
        # I: Current inputs => ?
VIGNET Pierre's avatar
VIGNET Pierre committed
188
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
VIGNET Pierre's avatar
VIGNET Pierre committed
189

190
        # Simple temporal properties:
VIGNET Pierre's avatar
VIGNET Pierre committed
191
192
        # SP(X0): Initial property/start property; Never change at each step.
        # IP(X): Invariant property
193
        # VP(X): Variant property
VIGNET Pierre's avatar
VIGNET Pierre committed
194
        #   List of logical formulas of properties forced at each step
195
        #   It's the trajectory of events of a solution.
VIGNET Pierre's avatar
VIGNET Pierre committed
196
197
        # FP(X): Final property

VIGNET Pierre's avatar
VIGNET Pierre committed
198
199
200
        self.__initial_constraints = []        # DIMACS clauses: C(X_0)
        self.__final_constraints   = []        # idem: C(X_n)
        self.__invariant_constraints = []      # DIMACS clauses: C(X_i))
201
        self.__variant_constraints = []        # variant constraints along trajectory
202
        self.__shift_direction = None          # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
203
204
205
206
207
208
209
210

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


    def reset(self):
211
212
213
        """Reset the unfolder before a new query

        This function is called from the constructor and during
214
215
        MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_solutions()
        following the call of init_with_query().
VIGNET Pierre's avatar
VIGNET Pierre committed
216
        """
217
        # Properties to be checked
218
219
220
221
222
223
        self.__initial_property = None            # logical formula - literal boolean expression
        self.__dim_initial = None                 # list of DIMACS clauses
        self.__final_property = None              # logical formula
        self.__dim_final = None                   # list of DIMACS clauses
        self.__invariant_property = None          # logical formula
        self.__dim_invariant = None               # list of DIMACS clauses
224
        self.__variant_property = None            # list<logic formulas>
225
        self.__dim_variant = None                 # list<list<DIMACS clauses>>
226
        # list of variant temporal constraints in Dimacs ground code
227
        self.__list_variant_constraints = None    # list<list<DIMACS clauses>>
228
229

        # If called from the constructor, for now these variables are just redefined here
230
231
232

        # For reachability optimisation. Number of shifts before checking
        # the final property
VIGNET Pierre's avatar
VIGNET Pierre committed
233
        self.__steps_before_check = 0
234
        self.__shift_direction = None             # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
235
        self.__locked = False
236

237
238
239
    def init_with_query(self, query):
        """Initialise the unfolder with the given query

240
        Following attributes are used from the query:
241
            start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
242
            variant_prop, dim_variant_prop, steps_before_check
243
244
245
        """
        # Reset the unfolder before a new query
        self.reset()
246
247
248
        # Init with query properties and clauses
        self.__initial_property = query.start_prop
        self.__dim_initial = query.dim_start
249

250
251
252
253
254
255
256
257
258
259
        self.__final_property = query.final_prop
        self.__dim_final = query.dim_final

        self.__invariant_property = query.inv_prop
        self.__dim_invariant = query.dim_inv

        # It's the trajectory of events of a solution.
        self.__variant_property = query.variant_prop
        self.__dim_variant = query.dim_variant_prop

260
261
262
        # For reachability optimisation. Number of shifts before checking
        # the final property (default 0)
        self.__steps_before_check = query.steps_before_check
263

VIGNET Pierre's avatar
VIGNET Pierre committed
264
    def set_stats(self):
265
        """Enable solver statistics (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
266
267
268
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
269

VIGNET Pierre's avatar
VIGNET Pierre committed
270
    def unset_stats(self):
271
        """Disable solver statistics (never used)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
272
        self.__stats = False
273

VIGNET Pierre's avatar
VIGNET Pierre committed
274
    def _stats(self):
275
276
277
        """Display solver statistics"""
        print("\n NB Variables in solver:", self.__nb_vars)
        print("NB Clauses in solver:", self.__nb_clauses)
278

VIGNET Pierre's avatar
VIGNET Pierre committed
279
280
281
    def set_include_aux_clauses(self, val):
        """
        Include auxiliary clause to eliminate undesirable solutions
282
        If A->B has clock h, an aux constraint added is h included in h when A
VIGNET Pierre's avatar
VIGNET Pierre committed
283
284
285
        Must be set to False for inhibitors computations
        """
        self.__include_aux_clauses = val
286

287
    ## Internal variable access for tests (never used) #########################
288
289
    @property
    def dynamic_constraints(self):
290
        """For tests: returns coded dynamic constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
291
        return self.__dynamic_constraints
292

293
294
    @property
    def initial_constraints(self):
295
        """For tests: returns coded initial constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
296
        return self.__initial_constraints
297

298
299
    @property
    def invariant_constraints(self):
300
        """For tests: returns coded invariant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
301
        return self.__invariant_constraints
302

303
304
    @property
    def variant_constraints(self):
305
        """For tests: returns coded variant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
306
        return self.__variant_constraints
307

308
309
    @property
    def final_constraints(self):
310
        """For tests: returns coded final constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
311
        self.__final_constraints
312

313
    ## Variables management ####################################################
314
315
316
317
318
319
    def vars_in_clause(self, clause):
        """Return variables names from values in the given clause
        (DEBUG never used)
        """
        return [self.get_var_indexed_name(var) for var in clause]

VIGNET Pierre's avatar
VIGNET Pierre committed
320
    def var_dimacs_code(self, var_name):
321
        """Returns DIMACS code of var_name (string) variable (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
322
        return self.__var_code_table[var_name]
323

VIGNET Pierre's avatar
VIGNET Pierre committed
324
    def get_system_var_number(self):
325
326
        """Get number of variables in the clause constraint dynamical system
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
327
328
329

        .. note:: This number should be equal to the number of variables
            in self.get_var_number()
VIGNET Pierre's avatar
VIGNET Pierre committed
330
        """
331
        return self.dynamic_system.get_var_number()
332

VIGNET Pierre's avatar
VIGNET Pierre committed
333
    def get_var_number(self):
334
335
        """Get number of principal variables (properties excluded) in the unfolder
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
336
337
338

        .. note:: This number should be equal to the number of variables
            in self.get_system_var_number()
VIGNET Pierre's avatar
VIGNET Pierre committed
339
        """
340
341
        # Remove the blacklisted first item (##) for variables naming
        return len(self.__var_list) - 1
342

VIGNET Pierre's avatar
VIGNET Pierre committed
343
    def get_var_name(self, var_num):
344
345
346
347
        """Get name of the variable

        .. seealso:: Explanations on get_var_indexed_name()

VIGNET Pierre's avatar
VIGNET Pierre committed
348
        @param var_num: DIMACS literal coding of an initial variable
349
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
350
        """
351
        # Get the original var_code without shifts
352
        var_code = (abs(var_num) - 1) % self.__shift_step + 1
353
        if var_code <= self.shift_step_init:
354
355
            # Variable num is less than the number of the variables in the system
            # => variable from the initial system
VIGNET Pierre's avatar
VIGNET Pierre committed
356
            return self.__var_list[var_code]
357
358
359
        else:
            # auxiliary variable introduced by properties compilation
            return self.__aux_list[var_code - self.shift_step_init -1]
VIGNET Pierre's avatar
VIGNET Pierre committed
360
            #raise MCLException("Not a DIMACS code of an initial variable")
361

VIGNET Pierre's avatar
VIGNET Pierre committed
362
    def get_var_indexed_name(self, var_num):
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
        """Get name of the variable with the time index appended

        .. note:: time index is the number of steps since the begining of the
            simulation.

            :Example:
                __shift_step = 2 (current step of the unfolding)
                shift_step_init = 2 (number of variables in the system)
                __var_list = ["##", "n1", "n2"]

                Virtual list of indexes in the state vector of a solution:
                [0, 1, 2, 3, 4, 5, 6, 7, 8, ...]
                 #|n1,n2|n1,n2|n1,n2|n1,n2|
                   ti=0  ti=1  ti=2  ti=3

                Given var_num = 7:
                index of var_name in __var_list: ((7-1) % 2) + 1 = 1
                var_name = "n1"
                time index: (7 - 1) / 2 = 3

                => return: "n1_3"

VIGNET Pierre's avatar
VIGNET Pierre committed
385
        @param var_num: DIMACS literal coding
386
        @return: name of the variable with the time index appended
VIGNET Pierre's avatar
VIGNET Pierre committed
387
        """
388
        varnum1 = abs(var_num)
389
        # Get the original var_code without shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
390
        var_code = (varnum1 - 1) % self.__shift_step + 1
391
        var_step = (varnum1 - var_code) / self.__shift_step
392
        if var_code <= self.shift_step_init:
393
394
            # Variable num is less than the number of the variables in the system
            # => variable from the initial system
VIGNET Pierre's avatar
VIGNET Pierre committed
395
396
            return self.__var_list[var_code] + '_%s'% var_step
        else:
397
398
            # Auxiliary variable introduced by properties compilation
            index = var_code - self.shift_step_init - 1
VIGNET Pierre's avatar
VIGNET Pierre committed
399
            return self.__aux_list[index] + '_%s'% var_step
400

VIGNET Pierre's avatar
VIGNET Pierre committed
401
    def get_free_clocks(self):
402
        """Get the DIMACS codes of the free_clocks variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
403
        return self.__free_clocks
404

VIGNET Pierre's avatar
VIGNET Pierre committed
405
    def get_inputs(self):
406
        """Get the DIMACS codes of the input variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
407
        return self.__inputs
408

VIGNET Pierre's avatar
VIGNET Pierre committed
409
410
411
412
413
    def get_shift_direction(self):
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
414

VIGNET Pierre's avatar
VIGNET Pierre committed
415
416
417
418
419
    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
420

VIGNET Pierre's avatar
VIGNET Pierre committed
421
422
423
424
425
426
    def get_current_step(self):
        """
        @return: the current number of unfolding
        """
        return self.__current_step

427

428
    ## Translation from names to num codes #####################################
VIGNET Pierre's avatar
VIGNET Pierre committed
429
430
    # the translation depends on the shift direction
    def __forward_code(self, clause):
431
432
433
434
435
436
437
438
439
        """(deprecated, directly included in C++ module: forward_init_dynamic())

        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

        ..note:: Future variables x' are noted "name`" in Literal names.
            Values of variables increases of __shift_step in future steps.

VIGNET Pierre's avatar
VIGNET Pierre committed
440
441
442
        @param clause: a Clause object
        @return: the DIMACS coding of the forward shifted clause
        """
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
        # Old API
        # num_clause = []
        # for lit in clause.list_of_literals:
        #     if lit.name[-1] == '`': # t+1 variable
        #         num_clause.append(
        #             -(self.__var_code_table[lit.name[:-1]] + self.__shift_step) \
        #             if not lit.sign \
        #             else (self.__var_code_table[lit.name[:-1]] + self.__shift_step)
        #         )
        #     else: # t variable
        #         num_clause.append(
        #             -self.__var_code_table[lit.name] \
        #             if not lit.sign else self.__var_code_table[lit.name]
        #         )
        # return num_clause

        # New API via C++ module
        return forward_code(clause, self.__var_code_table, self.__shift_step)

462

VIGNET Pierre's avatar
VIGNET Pierre committed
463
    def __backward_code(self, clause):
464
465
466
467
468
469
        """(never used, backward is partially implemented)

        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

VIGNET Pierre's avatar
VIGNET Pierre committed
470
471
472
473
474
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
        for lit in clause.list_of_literals:
475
476
477
478
            if not lit.name[-1] == '`': # t variable
                num_clause.append(-(self.__var_code_table[lit.name] + self.__shift_step) \
                if not lit.sign \
                else (self.__var_code_table[lit.name] + self.__shift_step))
VIGNET Pierre's avatar
VIGNET Pierre committed
479
            else:  # t+1 variable
480
481
482
                num_clause.append(-self.__var_code_table[lit.name[:-1]] \
                if not lit.sign \
                else self.__var_code_table[lit.name[:-1]])
VIGNET Pierre's avatar
VIGNET Pierre committed
483
        return num_clause
484

VIGNET Pierre's avatar
VIGNET Pierre committed
485
    def __code_clause(self, clause):
486
487
488
489
490
491
492
        """Numerically code a clause

        The numerical values are found in
        self.__var_code_table for variables in the dynamic system,
        or in self.__aux_code_table for other auxiliary variables;
        assume all variables are basic variables (t=0)

VIGNET Pierre's avatar
VIGNET Pierre committed
493
        @warning: MODIFIES SHIFT_STEP if auxiliary variables are present (numeric code)
494
495
496
497
498
499
500
            Because we add a variable in the system...

        :param clause:
        :return: List of numerical values corresponding to the literals
            in the given clause.
        :type clause: <Clause>
        :rtype: <list <int>>
VIGNET Pierre's avatar
VIGNET Pierre committed
501
502
503
        """
        num_clause = []
        for lit in clause.list_of_literals:
504
            # Get variable value with the given name
VIGNET Pierre's avatar
VIGNET Pierre committed
505
            name = lit.name
506
            if name in self.__var_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
507
                var_cod = self.__var_code_table[name]
508
            elif name in self.__aux_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
509
                var_cod = self.__aux_code_table[name]
510
511
            else:
                # Create an auxiliary variable - modifies shift_step (nb of variables)
VIGNET Pierre's avatar
VIGNET Pierre committed
512
                self.__shift_step += 1
513
                # Mapping name to value code
VIGNET Pierre's avatar
VIGNET Pierre committed
514
                self.__aux_code_table[name] = self.__shift_step
515
                # Mapping value code to name
VIGNET Pierre's avatar
VIGNET Pierre committed
516
                self.__aux_list.append(name)
517
518
519
520
521
                var_cod = self.__shift_step

            # Add the sign to the value
            lit_code = var_cod if lit.sign else -var_cod

VIGNET Pierre's avatar
VIGNET Pierre committed
522
523
            num_clause.append(lit_code)
        return num_clause
524

525
    ## Dynamic initialisations #################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
526
    def __forward_init_dynamic(self):
527
528
        """Dynamics initialisations.
        Set dynamic constraints for a forward one step: X1 = f(X0)
529

530
531
532
533
534
535
        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

        .. note:: Called by init_forward_unfolding()
536

537
538
539
540
        .. note:: Future variables x' are noted "name`" in Literal names.

        .. note:: Values of variables increases of __shift_step in future steps.
        """
541
        # New API via C++ module
542
        # TODO: take a look at __backward_init_dynamic & __backward_code
VIGNET Pierre's avatar
VIGNET Pierre committed
543
        if self.__include_aux_clauses:
544
            # Auxiliary clauses are supported (default)
545
            self.__dynamic_constraints = \
546
                forward_init_dynamic(self.dynamic_system.list_clauses,
547
548
                                     self.__var_code_table,
                                     self.__shift_step,
549
                                     self.dynamic_system.aux_list_clauses)
550
551
        else:
            self.__dynamic_constraints = \
552
                forward_init_dynamic(self.dynamic_system.list_clauses,
553
554
                                     self.__var_code_table,
                                     self.__shift_step)
555

VIGNET Pierre's avatar
VIGNET Pierre committed
556
    def __backward_init_dynamic(self):
557
558
        """Dynamics initialisations. (never used, backward is partially implemented)
        Set dynamic constraints for a forward one step: X0 = f(X1)
559

560
561
        .. note:: Called by init_backward_unfolding()
        """
562
563
        num_clause_list = \
            [self.__backward_code(clause)
564
             for clause in self.dynamic_system.list_clauses]
565

VIGNET Pierre's avatar
VIGNET Pierre committed
566
        if self.__include_aux_clauses:
567
568
            num_clause_list += \
                [self.__backward_code(clause)
569
                 for clause in self.dynamic_system.aux_list_clauses]
570

571
        self.__dynamic_constraints = [num_clause_list]
572

573
    ## Shifting variables: implementation of the shift operator ################
VIGNET Pierre's avatar
VIGNET Pierre committed
574
    def __shift_clause(self, ncl):
575
576
577
578
579
580
581
582
        """Shift a clause for the current __shift_step

        self.shift_step must be frozen in order to avoid problems during the
        unflatten() step of RawSolutions.
        => Each step MUST have the same number of variables.
        Thus, we lock the Unfolder by turning self.__locked to True.

        @param ncl: DIMACS clause ## TODO rename
VIGNET Pierre's avatar
VIGNET Pierre committed
583
584
        @warning: lock the unfolder
        """
585
586
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
VIGNET Pierre's avatar
VIGNET Pierre committed
587
588
589
590
591
592
593
594
595
596

        # Old API
        # Less efficient with abs()
        # return [(abs(lit) + self.__shift_step) * (-1 if lit < 0 else 1) for lit in ncl]
        # More efficient with ternary assignment
        # return [(lit + self.__shift_step) if lit > 0 else (lit - self.__shift_step)
        #         for lit in ncl]

        # New API via C++ module
        return shift_clause(ncl, self.__shift_step)
597

VIGNET Pierre's avatar
VIGNET Pierre committed
598
    def __m_shift_clause(self, ncl, nb_steps):
599
600
601
602
603
604
605
        """Shift a clause for the given step number

        self.shift_step must be frozen in order to avoid problems during the
        unflatten() step of RawSolutions.
        => Each step MUST have the same number of variables.
        Thus, we lock the Unfolder by turning self.__locked to True.

VIGNET Pierre's avatar
VIGNET Pierre committed
606
        @param ncl: DIMACS clause
607
        @param nb_steps: number of shifts asked
VIGNET Pierre's avatar
VIGNET Pierre committed
608
609
        @warning: lock the unfolder
        """
610
611
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
612

613
614
        return [(lit + self.__shift_step * nb_steps) if lit > 0
                else (lit - self.__shift_step * nb_steps) for lit in ncl]
615

VIGNET Pierre's avatar
VIGNET Pierre committed
616
    def __shift_dynamic(self):
617
618
619
620
        """Shift clauses representing the dynamics X' = f(X,I,C)

        Shift the last item of self.__dynamic_constraints and append the result
        to self.__dynamic_constraints.
VIGNET Pierre's avatar
VIGNET Pierre committed
621

622
623
        .. note:: Called by shift()
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
624
625
626
627
628
629
630
        # Old API
        # self.__dynamic_constraints.append(
        #   [self.__shift_clause(clause)
        #    for clause in self.__dynamic_constraints[-1]]
        # )

        # New API via C++ module
631
632
        # __dynamic_constraints:
        # List of lists of DIMACS encoded clauses (lists of ints)
VIGNET Pierre's avatar
VIGNET Pierre committed
633
634
        self.__dynamic_constraints.append(
            shift_dynamic(
635
                self.__dynamic_constraints[-1], # <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
636
637
638
                self.__shift_step
            )
        )
639

VIGNET Pierre's avatar
VIGNET Pierre committed
640
    def __shift_initial(self):
641
        """Shift initialisation condition
642

643
644
645
646
        .. note:: Called by:
            - shift()
            - init_backward_unfolding()
        """
647
        self.__initial_constraints = \
648
649
650
651
            shift_dynamic(
                self.__initial_constraints,
                self.__shift_step
            )
652

VIGNET Pierre's avatar
VIGNET Pierre committed
653
    def __shift_final(self):
654
        """Shift final property
655

656
657
658
659
        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
        """
660
        self.__final_constraints = \
661
662
663
664
            shift_dynamic(
                self.__final_constraints,
                self.__shift_step
            )
665

VIGNET Pierre's avatar
VIGNET Pierre committed
666
    def __shift_invariant(self):
667
668
669
670
671
672
        """Shift invariant property

        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
            - init_backward_unfolding()
VIGNET Pierre's avatar
VIGNET Pierre committed
673
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
674
        if self.__invariant_constraints:
VIGNET Pierre's avatar
VIGNET Pierre committed
675
676
677
678
679
680
681
682
683
684
685
686
687
            # Old API
            # self.__invariant_constraints.append(
            #     [self.__shift_clause(clause)
            #      for clause in self.__invariant_constraints[-1]]
            # )

            # New API via C++ module
            self.__invariant_constraints.append(
                shift_dynamic(
                    self.__invariant_constraints[-1],
                    self.__shift_step
                )
            )
688

VIGNET Pierre's avatar
VIGNET Pierre committed
689
690
691
    def __shift_variant(self):
        """
        shift variant property - depends on unfolding direction
692
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
693
694
695
696
697
698
699
700
701
702
703
704
705
706
        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)
707
708


VIGNET Pierre's avatar
VIGNET Pierre committed
709
    def shift(self):
710
711
712
713
714
715
716
717
718
719
        """Shift all clauses of one step

        self.__current_step is incremented here!

        Clauses shifted:
            - __dynamic_constraints[-1] (last element)
            - __invariant_constraints[-1] (last element)
            - __list_variant_constraints => TODO: audit...
            - __final_constraints if __shift_direction is "FORWARD"
            - __initial_constraints if __shift_direction is "BACKWARD"
VIGNET Pierre's avatar
VIGNET Pierre committed
720
        """
721
722
723
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True

VIGNET Pierre's avatar
VIGNET Pierre committed
724
725
726
727
728
729
730
731
        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:
732
            # Shift direction must be set
VIGNET Pierre's avatar
VIGNET Pierre committed
733
            raise MCLException("Shift incoherent data: "+self.__shift_direction)
734
735

        # Increment the current step
VIGNET Pierre's avatar
VIGNET Pierre committed
736
        self.__current_step += 1
737

738
    ## Coding of properties ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
739
    def __compile_property(self, property_text):
740
741
742
743
744
745
746
747
748
749
750
        """Compile a property (logical formula) into clauses

        Type checking uses the symbol table of dyn_sys
        Error reporting is made through the dyn_sys reporter

        .. warning:: MODIFIES __lit_cpt for numbering of auxiliary variables (not coding)

        .. note:: Called by:
            - __init_initial_constraint_0()
            - __init_final_constraint_0()
            - __init_invariant_constraint_0()
VIGNET Pierre's avatar
VIGNET Pierre committed
751
752
        """
        if self.__locked:
VIGNET Pierre's avatar
VIGNET Pierre committed
753
754
            raise MCLException("Trying to compile property while unfolder is locked")

VIGNET Pierre's avatar
VIGNET Pierre committed
755
        # syntax analyser and type checker
VIGNET Pierre's avatar
VIGNET Pierre committed
756
757
758
759
        # property_text, symb_t, reporter
        tree_prop = compile_cond(property_text,
                                 self.__dyn_sys.symb_tab,
                                 self.__dyn_sys.report)
760
761
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
762
763
764
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
765

VIGNET Pierre's avatar
VIGNET Pierre committed
766
    def __compile_event(self, property_text):
767
768
769
770
771
772
773
774
775
        """Compile an event (biosignal expression) into clauses

        Type checking uses the symbol table of dyn_sys
        Error reporting is made through the dyn_sys reporter

        .. warning:: MODIFIES __lit_cpt for numbering of auxiliary variables (not coding)

        .. note:: Called by:
            - __init_variant_constraints_0()
VIGNET Pierre's avatar
VIGNET Pierre committed
776
777
        """
        if self.__locked:
778
779
780
781
782
            raise MCLException("Trying to compile property while unfolder is locked")

        # Syntax analyser and type checker
        tree_prop, ste, fcl = compile_event(
            property_text,
783
            self.dynamic_system.symb_tab,
784
            True,
785
            self.dynamic_system.report
786
787
        )
        # Avoid name collisions of aux var
788
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
789
790
791
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
792

VIGNET Pierre's avatar
VIGNET Pierre committed
793
794
795
796
797
798
    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!!
        """
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
# OLD
#        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

        self.__initial_constraints = list()

        # initialize no frontier places to False
VIGNET Pierre's avatar
VIGNET Pierre committed
819
        if no_frontier_init:
820
821
            self.__initial_constraints += [elem for elem in self.__no_frontier_init]

VIGNET Pierre's avatar
VIGNET Pierre committed
822
823
824
        if self.__initial_property:
            # compile initial property
            # compile numeric form
825
826
            self.__initial_constraints += [self.__code_clause(clause) for clause in self.__compile_property(self.__initial_property)]

VIGNET Pierre's avatar
VIGNET Pierre committed
827
        # dimacs aux initial properties
828
829
        if self.__dim_initial:
            self.__initial_constraints += self.__dim_initial
830

VIGNET Pierre's avatar
VIGNET Pierre committed
831
832
833
834
835
836
    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!!
        """
837

VIGNET Pierre's avatar
VIGNET Pierre committed
838
839
840
        self.__final_constraints = []
        if self.__final_property:
            # compile initial (X0) property
VIGNET Pierre's avatar
VIGNET Pierre committed
841
            # ex: Px => [$Px$]
VIGNET Pierre's avatar
VIGNET Pierre committed
842
843
            l_clauses = self.__compile_property(self.__final_property)
            # compile numeric form
VIGNET Pierre's avatar
VIGNET Pierre committed
844
            # ex: [$Px$] => self.__final_constraints = [[7]]
VIGNET Pierre's avatar
VIGNET Pierre committed
845
846
847
848
849
            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
850

VIGNET Pierre's avatar
VIGNET Pierre committed
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
    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
869

VIGNET Pierre's avatar
VIGNET Pierre committed
870
871
    def __init_variant_constraints_0(self):
        """
872
        if variant_property is set, compile each property into clauses and
VIGNET Pierre's avatar
VIGNET Pierre committed
873
874
875
876
877
878
879
880
881
882
883
884
885
886
        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)
887

VIGNET Pierre's avatar
VIGNET Pierre committed
888
889
            # add variant properties in dimacs form
            if self.__dim_variant:
890
                vp_length = len(self.__variant_property)
VIGNET Pierre's avatar
VIGNET Pierre committed
891
892
893
                if vp_length != len(self.__dim_variant):
                    mess = "Incoherent variant properties"
                    raise MCLException(mess)
894

VIGNET Pierre's avatar
VIGNET Pierre committed
895
896
897
                for i in range(vp_length):
                    c_var = self.__list_variant_constraints[i]
                    c_var = c_var + self.__dim_variant[i]
898
                    self.__list_variant_constraints[i] = c_var
VIGNET Pierre's avatar
VIGNET Pierre committed
899
900
901
902
903
904
905
906
907
908
909
910
        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)
911

912
    ## Whole initialisations ###################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
913
914
915
    def init_forward_unfolding(self):
        """
        initialisation before generating constraints - forward trajectory
916
917

        Called at the begining of squery_is_satisfied and squery_solve
VIGNET Pierre's avatar
VIGNET Pierre committed
918
919
920
        """
        self.__shift_direction = 'FORWARD'
        self.__current_step = 1
921
922
923
        self.__shift_step = self.shift_step_init  # back to basic!
        self.__aux_code_table = dict()            # flush auxiliary variables
        self.__aux_list = []                      # idem
924

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

VIGNET Pierre's avatar
VIGNET Pierre committed
931
932
933
934
        # now shifting is possible
        self.__forward_init_dynamic()
        self.__shift_final()
        self.__shift_invariant()
935
936


VIGNET Pierre's avatar
VIGNET Pierre committed
937
    def init_backward_unfolding(self):
938
        """Never used (and backward not implemented in __init_variant_constraints_0)
VIGNET Pierre's avatar
VIGNET Pierre committed
939
940
941
942
        initialisation before generating constraints - backward trajectory
        """
        self.__shift_direction = 'BACKWARD'
        self.__current_step = 0
943
944
945
        self.__shift_step = self.shift_step_init  # back to basic!
        self.__aux_code_table = dict()            # flush auxiliary variables
        self.__aux_list = []                      # idem
946

VIGNET Pierre's avatar
VIGNET Pierre committed
947
948
949
950
951
        # 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()
952

VIGNET Pierre's avatar
VIGNET Pierre committed
953
954
955
956
        # now shifting is possible
        self.__backward_init_dynamic()
        self.__shift_initial()
        self.__shift_invariant()
957

958
    ## Solver interface ########################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
959
    def __load_solver(self, solv):
960
        """Add all the current clauses in the solver
VIGNET Pierre's avatar
VIGNET Pierre committed
961

962
963
964
965
        .. note:: Called by:
            - __constraints_satisfied()
            - __msolve_constraints()
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
966
967
968
969
970
971
972
        # New API via C++ module
        solv.add_clauses(self.__final_constraints)
        solv.add_clauses(it.chain(*self.__invariant_constraints))
        solv.add_clauses(self.__variant_constraints)
        solv.add_clauses(it.chain(*self.__dynamic_constraints))
        solv.add_clauses(self.__initial_constraints)

973
974
975
976
        # LOGGING
        if LOGGER.getEffectiveLevel() == DEBUG:
            # final
            LOGGER.debug("Load new solver !!")
VIGNET Pierre's avatar
VIGNET Pierre committed
977
            LOGGER.debug(">> final constraints: %s", len(self.__final_constraints))
978
979
980
            LOGGER.debug(str(self.__final_constraints))

            # trajectory invariant
VIGNET Pierre's avatar
VIGNET Pierre committed
981
            LOGGER.debug(">> trajectory invariant constraints: %s", len(self.__invariant_constraints))
982
983
984
            LOGGER.debug(str(self.__invariant_constraints))

            # trajectory variant
VIGNET Pierre's avatar
VIGNET Pierre committed
985
            LOGGER.debug(">> trajectory variant constraints: %s", len(self.__variant_constraints))
986
987
988
            LOGGER.debug(str(self.__variant_constraints))

            # dynamics
VIGNET Pierre's avatar
VIGNET Pierre committed
989
            LOGGER.debug(">> dynamic constraints: %s", len(self.__dynamic_constraints))
990
991
992
            LOGGER.debug(str(self.__dynamic_constraints))

            # initial
VIGNET Pierre's avatar
VIGNET Pierre committed
993
            LOGGER.debug(">> initial constraints: %s", len(self.__initial_constraints))
994
            LOGGER.debug(str(self.__initial_constraints))
995
996


VIGNET Pierre's avatar
VIGNET Pierre committed
997
    def __constraints_satisfied(self):
998
999
1000
        """Test if the system loaded in the solver is satisfiable
        :return: True if the problem is satisfiable, False otherwise.
        :rtype: <boolean>
VIGNET Pierre's avatar
VIGNET Pierre committed
1001
1002
        """
        solver = CryptoMS()
1003
        # Load all clauses into the solver
VIGNET Pierre's avatar
VIGNET Pierre committed
1004
        self.__load_solver(solver)
1005

VIGNET Pierre's avatar
VIGNET Pierre committed
1006
        if self.__stats:
1007