Attention une mise à jour du service Gitlab va être effectuée le mardi 18 janvier (et non lundi 17 comme annoncé précédemment) entre 18h00 et 18h30. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes.

CLUnfolder.py 69.9 KB
Newer Older
VIGNET Pierre's avatar
VIGNET Pierre committed
1
# -*- coding: utf-8 -*-
VIGNET Pierre's avatar
VIGNET Pierre committed
2
3
4
## Filename    : 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
##
## Contributor(s): Geoffroy Andrieux IRSET
##
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
"""Main engine for constraints unfolding and solving.

Process from the intialization with a query to the finding of a solution.


MCLSimpleQuery (reminder):
    Object containing 2 main types of attributes describing properties:

        - Attributes in text format: These are logical formulas that are humanly
        readable.
            Ex: start_prop, inv_prop, final_prop, variant_prop
        - Attributes in DIMACS format: These are logical formulas encoded in
        the form of clauses containing numerical values.
            Ex: dim_start, dim_inv, dim_final, dim_variant_prop

57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
---

About shifting clauses and variables:

    Initialization of the dynamic system by __forward_init_dynamic() iterates on
    all literals of the system.
    If a literal is a t+1 literal, its value is shifted to the right or to the
    left depending on whether its value is positive or negative
    (addition vs soustraction of shift_step value which is the number of
    variables in the system).

    Otherwise, the literal is a t literal and its value stays untouched.

    t+1 and t literals are generated by CLDynSys object directly from the current
    model.

    Shift a clause consists to iterates on all its literals and shift their values
    to the right or to the left depending on whether their values are positive
    or negative.

---

79
80
81
82
83
84
85
86
init_with_query(query):
    Copy of the query attributes to temporary attributes internal to the CLUnfolder.

    Textual properties of query are compiled into numeric clauses in
    init_forward_unfolding(), just at the beginning of squery_is_satisfied()
    and squery_solve().

    ALL textual properties are susceptible to add new auxiliary variables in the
87
88
    system (increase shift_step). This is why any shift must be made after the
    initialization.
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117


init_forward_unfolding():
    Organization of the initialization of the system (its clauses) for
    the current request and first variables shift.

    Initialized attributes:
        - __initial_constraints:
            Query data + negative values of all places that are not frontiers.
        - __final_constraints:
            Query data
        - __invariant_constraints:
            List of Query data
        - __list_variant_constraints:
            Query data (automatic merge of textual and DIMACS forms)
        - __variant_constraints:
            Initilized with the first item of __list_variant_constraints

    Shifted attributes with __shift_step (nb of variables in the system):
        - __forward_init_dynamic(): __dynamic_constraints:
            Shift dynamic_system.list_clauses + dynamic_system.aux_list_clauses + init
        - __shift_final(): __final_constraints:
            Shift + replace __final_constraints
        - __shift_invariant(): _invariant_constraints:
            Shift + append of the last element of __invariant_constraints

        PS: __variant_constraints si already initialized for the first step


118
119
120
121
    The following functions decompile textual properties or events and code them
    into DIMACS clauses constraints via __code_clause().
    __code_clause() is susceptible to add new auxiliary numerical variables
    during this process if a variable is not found in __var_code_table and in
122
123
124
125
126
127
128
129
    __aux_code_table.

    - __init_initial_constraint_0, __init_final_constraint_0, __init_invariant_constraint_0
        __code_clause + __compile_property
    - __init_variant_constraints_0
        __code_clause + __compile_event


130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
shift():
    Shift all clauses of the system to prepare it for the next step.

    Called at each step by:
        - squery_solve()
        - squery_is_satisfied()

    Modified attributes:
        - __shift_dynamic(): __dynamic_constraints:
            Shift + append of the last element of __dynamic_constraints
        - __shift_variant(): __variant_constraints:
            Shift clauses of the current step in __list_variant_constraints, and
            append them to __variant_constraints.
        - __shift_invariant()
            ...
        - __shift_final()
            ...

148
149
        PS: __initial_constraints are left as this for now
        (shifted only with BACKWARD shift direction).
150

VIGNET Pierre's avatar
VIGNET Pierre committed
151
"""
152
153
from __future__ import print_function

VIGNET Pierre's avatar
VIGNET Pierre committed
154
155
#from pyCryptoMS import CryptoMS
from pycryptosat import Solver as CryptoMS
156
157
158
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
159
from cadbiom import commons as cm
VIGNET Pierre's avatar
VIGNET Pierre committed
160
161

# C++ API
162
from _cadbiom import shift_clause, shift_dimacs_clauses, forward_code, \
VIGNET Pierre's avatar
VIGNET Pierre committed
163
164
165
                     forward_init_dynamic

# Standard imports
166
from logging import DEBUG
VIGNET Pierre's avatar
VIGNET Pierre committed
167
import itertools as it
168
169

LOGGER = cm.logger()
VIGNET Pierre's avatar
VIGNET Pierre committed
170
171
172

class CLUnfolder(object):
    """
173
174
175
176
177
178
179
180
181
    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
182
183
184
185
    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
186

VIGNET Pierre's avatar
VIGNET Pierre committed
187
188
    During unfolding, clauses are shifted either to the future (forward) or
    to the past (backward). The shift operator is a simple addition
189
190
    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
191
    to add variables while generating a trajectory unfolding.
192
193

    Glossary
VIGNET Pierre's avatar
VIGNET Pierre committed
194
195
196
    ========
    - ground variables/ground dimacs code: variables at time 0/their encoding.
    - solution: a solution of the logical dynamic constraint from SAT solver
197
    - state vector: list of DIMACS code of original (not shifted) variables
VIGNET Pierre's avatar
VIGNET Pierre committed
198
199
      corresponding to a step.
    - trajectory: list of state_vectors
200
201
202
203
204
205
206
207
208
209
210


    Some attributes (Please read the constructor comments for much more information):

        __*_property: Logical formulas in text format from the current query.
        __dimacs_*: Clauses in DIMACS format from the current query.
        __*_constraints: CLUnfolder attributes for unfolding and shift initialised
            from the query attributes.

        :param dynamical_system: dynamical system in clause constraint form
        :type dynamical_system: <CLDynSys>
VIGNET Pierre's avatar
VIGNET Pierre committed
211
    """
212

213
    def __init__(self, dynamic_system, debug=False):
214
215
216
217
        """
        :param dynamic_system: Describe a dynamic system in clause form.
        :type dynamic_system: <CLDynSys>
        """
218
        self.dynamic_system = dynamic_system # symbolic clause dynamic system
219

VIGNET Pierre's avatar
VIGNET Pierre committed
220
        # shift_step equals to the total number of coded variables of the system
221
        # (including inputs, entities, clocks/events, auxiliary variables)
VIGNET Pierre's avatar
VIGNET Pierre committed
222

223
        # shift_step_init: the shift step ss (if n is X_0 code, n+ss is X_1 code)
VIGNET Pierre's avatar
VIGNET Pierre committed
224
        self.shift_step_init = dynamic_system.get_var_number()
225
226
        self.__shift_step = self.shift_step_init  # current shift/step

227
        # About unfolder lock and shift_step:
228
229
230
231
232
        # 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
233
        self.__locked = False
234
235
236
        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
237
        self.__steps_before_check = 0
238

VIGNET Pierre's avatar
VIGNET Pierre committed
239
        # assign a DIMACS code number to each variable (invariant)
240
241
        # 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
242
        # (including inputs, entities, clocks/events, auxiliary variables).
243
244
        self.__var_code_table = dict()     # Mapping: name -> DIMACS code (!= 0)
        self.__var_list = ['##']           # Mapping: DIMACS code (!= 0) -> name
245
246

        # Fix order of variables names with a list:
247
248
        # - indexes of __var_list are the values of the variables at these indexes
        # - values begin from 1 (0 is a blacklisted value)
249
250
251
252
        if debug:
            base_var_set = sorted(list(dynamic_system.base_var_set))
        else:
            base_var_set = list(dynamic_system.base_var_set)
253
        self.__var_list += base_var_set
254
        # keys: are the names of the variables, values: their values
255
256
257
258
259
260
261
262
263
264
265
266
267
        self.__var_code_table = \
            {var_name: var_num for var_num, var_name in enumerate(base_var_set, 1)}
        # Optimization: for forward_init_dynamic() and forward_code() (mostly
        # implemented in C.
        # Precompute __var_code_table with the literal names in "future" format;
        # i.e with a last char '`' at the end.
        # Thus it is easy to search them directly in the dict (in O(1)),
        # instead of slicing them.
        # Note: "future" literals are already in self.dynamic_system.list_clauses
        # and maybe in self.dynamic_system.aux_list_clauses
        temp_var_code_table = \
            {var_name + "`": var_num for var_name, var_num in self.__var_code_table.iteritems()}
        self.__var_code_table.update(temp_var_code_table)
268

269
        assert len(self.__var_code_table) == 2 * self.__shift_step
270

271
272
273
274
        # 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
275
        self.__include_aux_clauses_changed = False
276
        self.__lit_cpt = self.__shift_step + 1    # counter for aux. var. coding
277

278
279
280
281
        # 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
282
        self.__aux_list = []                      # code to name
283

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

288
        # ordered list of DIMACS codes of the frontier variables/places
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
        self.frontier_values = [self.__var_code_table[frp] for frp in self.dynamic_system.frontiers]
        self.frontier_values.sort()
        ## TODO: sort utile ici ???? si non passer en frozenset et supprimer les casts partout ailleurs
        ## Cf RawSolution.frontier_pos_and_neg_values BACKWARD, encore utilisé avec index
        ## Cf TestCLUnfolder.test_frontier indexable mais peut etre contourné

        # Precompute convenient attributes for:
        # frontiers_pos_and_neg:
        #     - RawSolution.frontier_pos_and_neg_values
        #     (set operation with solution variables)
        # frontiers_negative_values:
        #     - MCLQuery.from_frontier_sol_new_timing
        #     - MCLQuery.frontiers_negative_values
        #     - MCLAnalyser.__solve_with_inact_fsolution
        #     - TestCLUnfolder.test_prune
        #
        # Set of frontier positive and negative values
        # (all frontiers and their opposite version).
        # => operations with sets are much faster
        self.frontiers_negative_values = \
            frozenset(-frontier for frontier in self.frontier_values)
310
311
312
313
        self.frontiers_pos_and_neg = \
            self.frontiers_negative_values | frozenset(self.frontier_values)

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

316
        # DIMACS codes of the free_clocks variables/places for extraction (invariant)
317
        self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.dynamic_system.free_clocks)
318
319

        # Binding for a merged version of __inputs and __free_clocks
320
        # Convenient attribute for RawSolution.extract_act_input_clock_seq()
321
322
        # DIMACS codes of the input and free_clocks variables
        self.inputs_and_free_clocks = self.__inputs | self.__free_clocks
323

324
325
        # Properties to be checked
        self.reset()
326

327
        # Logical constraints:
328
        # Result from unfolding of base constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
329
330
331
332
333
        # 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
334
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
335
        self.__precomputed_dynamic_constraints = []
VIGNET Pierre's avatar
VIGNET Pierre committed
336

337
        # Simple temporal properties:
VIGNET Pierre's avatar
VIGNET Pierre committed
338
339
        # SP(X0): Initial property/start property; Never change at each step.
        # IP(X): Invariant property
340
        # VP(X): Variant property
VIGNET Pierre's avatar
VIGNET Pierre committed
341
        #   List of logical formulas of properties forced at each step
342
        #   It's the trajectory of events of a solution.
VIGNET Pierre's avatar
VIGNET Pierre committed
343
344
        # FP(X): Final property

345
        self.__initial_constraints = []        # DIMACS clauses: C(X_0) <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
346
347
        self.__final_constraints   = []        # idem: C(X_n)
        self.__invariant_constraints = []      # DIMACS clauses: C(X_i))
348
        self.__variant_constraints = []        # variant constraints along trajectory
349
        self.__shift_direction = None          # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
350
351
352
353
354
355
356
357

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


    def reset(self):
358
359
        """Reset the unfolder before a new query

360
361
362
        Reset only properties and dimacs clauses from the current query;
        AND __list_variant_constraints.

363
364
365
366
        => __initial_constraints, __final_constraints, __invariant_constraints,
        __variant_constraints and __dynamic_constraints ARE NOT reset here
        (see init_forward_unfolding())

367
        This function is called from the constructor and during
368
369
        MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_solutions()
        following the call of init_with_query().
VIGNET Pierre's avatar
VIGNET Pierre committed
370
        """
371
        # Properties to be checked
372
        self.__initial_property = None            # logical formula - literal boolean expression
373
        self.__dimacs_initial = None              # list of DIMACS clauses
374
        self.__final_property = None              # logical formula
375
        self.__dimacs_final = None                # list of DIMACS clauses
376
        self.__invariant_property = None          # logical formula
377
        self.__dimacs_invariant = None            # list of DIMACS clauses
378
        self.__variant_property = None            # list<logic formulas>
379
        self.__dimacs_variant = None              # list<list<DIMACS clauses>>
380
        # list of variant temporal constraints in Dimacs ground code
381
        self.__list_variant_constraints = None    # list<list<DIMACS clauses>>
382

383
384
        # If this function is called from the constructor,
        # the following variables are just redefined here.
385
386
387

        # For reachability optimisation. Number of shifts before checking
        # the final property
VIGNET Pierre's avatar
VIGNET Pierre committed
388
        self.__steps_before_check = 0
389
        self.__shift_direction = None             # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
390
        self.__locked = False
391

392
393
394
    def init_with_query(self, query):
        """Initialise the unfolder with the given query

395
        Following attributes are used from the query:
396
            start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
397
            variant_prop, dim_variant_prop, steps_before_check
398
399

        Textual properties of query are compiled into numeric clauses in
400
401
        init_forward_unfolding(), just at the beginning of squery_is_satisfied()
        and squery_solve().
402
        This compilation step is costly due to ANTLR performances...
403
404
405

        .. warning:: ALL textual properties are susceptible to add new auxiliary
            variables in the system (increase shift_step).
406
407
408
        """
        # Reset the unfolder before a new query
        self.reset()
409
        # Init with query properties and clauses
410
411
        self.__initial_property = query.start_prop # logical formula in text
        self.__dimacs_initial = query.dim_start
412

413
414
        self.__final_property = query.final_prop # logical formula in text
        self.__dimacs_final = query.dim_final
415

416
417
        self.__invariant_property = query.inv_prop # logical formula in text
        self.__dimacs_invariant = query.dim_inv
418
419

        # It's the trajectory of events of a solution.
420
421
        self.__variant_property = query.variant_prop # logical formula in text
        self.__dimacs_variant = query.dim_variant_prop
422

423
424
425
        # For reachability optimisation. Number of shifts before checking
        # the final property (default 0)
        self.__steps_before_check = query.steps_before_check
426

VIGNET Pierre's avatar
VIGNET Pierre committed
427
    def set_stats(self):
428
        """Enable solver statistics (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
429
430
431
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
432

VIGNET Pierre's avatar
VIGNET Pierre committed
433
    def unset_stats(self):
434
        """Disable solver statistics (never used)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
435
        self.__stats = False
436

VIGNET Pierre's avatar
VIGNET Pierre committed
437
    def _stats(self):
438
439
440
        """Display solver statistics"""
        print("\n NB Variables in solver:", self.__nb_vars)
        print("NB Clauses in solver:", self.__nb_clauses)
441

VIGNET Pierre's avatar
VIGNET Pierre committed
442
    def set_include_aux_clauses(self, val):
443
444
        """Flag to include auxiliary clause to eliminate undesirable solutions.

445
        If A->B has clock h, an aux constraint added is h included in h when A
446
447
448
449
450
451
452
        Must be set to False for inhibitors computations.

        .. warning:: This function impacts the shift_step number.

        Tested in by:
            - __forward_init_dynamic
            - __backward_init_dynamic
VIGNET Pierre's avatar
VIGNET Pierre committed
453
454
        """
        self.__include_aux_clauses = val
455
        self.__include_aux_clauses_changed = True
456

457
    ## Internal variable access for tests (never used) #########################
458
459
    @property
    def dynamic_constraints(self):
460
        """For tests: returns coded dynamic constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
461
        return self.__dynamic_constraints
462

463
464
    @property
    def initial_constraints(self):
465
        """For tests: returns coded initial constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
466
        return self.__initial_constraints
467

468
469
    @property
    def invariant_constraints(self):
470
        """For tests: returns coded invariant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
471
        return self.__invariant_constraints
472

473
474
    @property
    def variant_constraints(self):
475
        """For tests: returns coded variant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
476
        return self.__variant_constraints
477

478
479
    @property
    def final_constraints(self):
480
        """For tests: returns coded final constraints"""
481
        return self.__final_constraints
482

483
    ## Variables management ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
484
485
    def var_names_in_clause(self, clause):
        """Return the names of the variables from values in the given numeric clause
486
487
488
489
        (DEBUG never used)
        """
        return [self.get_var_indexed_name(var) for var in clause]

VIGNET Pierre's avatar
VIGNET Pierre committed
490
    def var_dimacs_code(self, var_name):
491
        """Returns DIMACS code of var_name (string) variable (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
492
        return self.__var_code_table[var_name]
493

VIGNET Pierre's avatar
VIGNET Pierre committed
494
    def get_system_var_number(self):
495
496
        """Get number of variables in the clause constraint dynamical system
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
497
498
499

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

VIGNET Pierre's avatar
VIGNET Pierre committed
503
    def get_var_number(self):
504
505
        """Get number of principal variables (properties excluded) in the unfolder
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
506
507
508

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

VIGNET Pierre's avatar
VIGNET Pierre committed
513
    def get_var_name(self, var_num):
514
515
516
517
        """Get name of the variable

        .. seealso:: Explanations on get_var_indexed_name()

VIGNET Pierre's avatar
VIGNET Pierre committed
518
        @param var_num: DIMACS literal coding of an initial variable
519
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
520
        """
521
        # Get the original var_code without shifts
522
        var_code = (abs(var_num) - 1) % self.__shift_step + 1
523
        if var_code <= self.shift_step_init:
524
525
            # 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
526
            return self.__var_list[var_code]
527
528
529
        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
530
            #raise MCLException("Not a DIMACS code of an initial variable")
531

VIGNET Pierre's avatar
VIGNET Pierre committed
532
    def get_var_indexed_name(self, var_num):
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
        """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
555
        @param var_num: DIMACS literal coding
556
        @return: name of the variable with the time index appended
VIGNET Pierre's avatar
VIGNET Pierre committed
557
        """
558
        varnum1 = abs(var_num)
559
        # Get the original var_code without shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
560
        var_code = (varnum1 - 1) % self.__shift_step + 1
561
        var_step = (varnum1 - var_code) / self.__shift_step
562
        if var_code <= self.shift_step_init:
563
564
            # 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
565
566
            return self.__var_list[var_code] + '_%s'% var_step
        else:
567
568
            # Auxiliary variable introduced by properties compilation
            index = var_code - self.shift_step_init - 1
VIGNET Pierre's avatar
VIGNET Pierre committed
569
            return self.__aux_list[index] + '_%s'% var_step
570

VIGNET Pierre's avatar
VIGNET Pierre committed
571
    def get_free_clocks(self):
572
        """Get the DIMACS codes of the free_clocks variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
573
        return self.__free_clocks
574

VIGNET Pierre's avatar
VIGNET Pierre committed
575
    def get_inputs(self):
576
        """Get the DIMACS codes of the input variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
577
        return self.__inputs
578

VIGNET Pierre's avatar
VIGNET Pierre committed
579
580
581
582
583
    def get_shift_direction(self):
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
584

585
586
    @property
    def shift_step(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
587
588
589
590
        """
        @return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
        """
        return self.__shift_step
591

592
593
    @property
    def current_step(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
594
595
596
597
598
        """
        @return: the current number of unfolding
        """
        return self.__current_step

599

600
    ## Translation from names to num codes #####################################
VIGNET Pierre's avatar
VIGNET Pierre committed
601
    ## The translation depends on the shift direction
VIGNET Pierre's avatar
VIGNET Pierre committed
602
    def __forward_code(self, clause):
603
604
605
606
607
608
609
610
611
        """(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
612
613
614
        @param clause: a Clause object
        @return: the DIMACS coding of the forward shifted clause
        """
615
616
        # Old API
        # num_clause = []
617
        # for lit in clause.literals:
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
        #     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)

634

VIGNET Pierre's avatar
VIGNET Pierre committed
635
    def __backward_code(self, clause):
636
637
638
639
640
641
        """(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
642
643
644
645
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
646
647
648
649
650
651
652
653
654
655
656
657
658
        for lit in clause.literals:
            if lit.name[-1] == '`': # t+1 variable
                num_clause.append(
                    -self.__var_code_table[lit.name[:-1]] \
                    if not lit.sign \
                    else self.__var_code_table[lit.name[:-1]]
                )
            else: # t variable, base 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
659
        return num_clause
660

VIGNET Pierre's avatar
VIGNET Pierre committed
661
    def __code_clause(self, clause):
662
663
664
665
666
        """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;
667
        assume all variables are basic variables (t=0) (not shifted).
668

669
670
671
672
        @warning: This function MODIFIES SHIFT_STEP because we add a variable
            in the system if a variable is not found in __var_code_table or in
            __aux_code_table.
            A new auxiliary variable will be created in __aux_code_table.
673
674
675
676
677
678

        :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
679
680
        """
        num_clause = []
681
        for lit in clause.literals:
682
            # Get variable value with the given name
VIGNET Pierre's avatar
VIGNET Pierre committed
683
            name = lit.name
684
            if name in self.__var_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
685
                var_cod = self.__var_code_table[name]
686
            elif name in self.__aux_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
687
                var_cod = self.__aux_code_table[name]
688
689
            else:
                # Create an auxiliary variable - modifies shift_step (nb of variables)
VIGNET Pierre's avatar
VIGNET Pierre committed
690
                self.__shift_step += 1
691
                # Mapping name to value code
VIGNET Pierre's avatar
VIGNET Pierre committed
692
                self.__aux_code_table[name] = self.__shift_step
693
                # Mapping value code to name
VIGNET Pierre's avatar
VIGNET Pierre committed
694
                self.__aux_list.append(name)
695
                # Define var_cod
696
697
698
699
700
                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
701
702
            num_clause.append(lit_code)
        return num_clause
703

704
    ## Dynamic initialisations #################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
705
    def __forward_init_dynamic(self):
706
707
        """Dynamics initialisations.
        Set dynamic constraints for a forward one step: X1 = f(X0)
708

VIGNET Pierre's avatar
VIGNET Pierre committed
709
        Numerically code clauses with the numeric codes found in
710
711
        self.__var_code_table for a base variable x,
        and numeric_code + shift_step for x' variable integer coding increases
VIGNET Pierre's avatar
VIGNET Pierre committed
712
713
714
715
716
        in future steps.

        __dynamic_constraints is a list of lists of numeric clauses (lists of ints)
        Each sublist of __dynamic_constraints corresponds to a step in the unfolder;
        the last step is the last element.
717

718
719
        .. seealso:: __forward_code()

720
        .. note:: Called by init_forward_unfolding()
721

722
723
724
725
        .. note:: Future variables x' are noted "name`" in Literal names.

        .. note:: Values of variables increases of __shift_step in future steps.
        """
726
        # New API via C++ module
727
        # TODO: take a look at __backward_init_dynamic & __backward_code
VIGNET Pierre's avatar
VIGNET Pierre committed
728
        if self.__include_aux_clauses:
729
            # Auxiliary clauses are supported (default)
730
            self.__dynamic_constraints = \
731
                forward_init_dynamic(self.dynamic_system.list_clauses,
732
733
                                     self.__var_code_table,
                                     self.__shift_step,
734
                                     self.dynamic_system.aux_list_clauses)
735
736
        else:
            self.__dynamic_constraints = \
737
                forward_init_dynamic(self.dynamic_system.list_clauses,
738
739
                                     self.__var_code_table,
                                     self.__shift_step)
740

741
742
743
744
        # __dynamic_constraints is initialized and
        # has now taken into account the auxiliary clauses flag
        self.__include_aux_clauses_changed = False

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

749
750
        .. note:: Called by init_backward_unfolding()
        """
751
752
        num_clause_list = \
            [self.__backward_code(clause)
753
             for clause in self.dynamic_system.list_clauses]
754

VIGNET Pierre's avatar
VIGNET Pierre committed
755
        if self.__include_aux_clauses:
756
757
            num_clause_list += \
                [self.__backward_code(clause)
758
                 for clause in self.dynamic_system.aux_list_clauses]
759

760
        self.__dynamic_constraints = [num_clause_list]
761

762
    ## Shifting variables: implementation of the shift operator ################
763
    def __shift_clause(self, numeric_clause):
764
765
        """Shift a clause for the current __shift_step

VIGNET Pierre's avatar
VIGNET Pierre committed
766
767
        (no used anymore, replaced by direct use of C++ code)

768
769
770
        Basically, `shift_step` is added to positive variables and subtracted
        from negative variables in `numeric_clause`.

771
        About unfolder lock and shift_step:
772
773
774
775
776
        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.

777
        @param numeric_clause: DIMACS clause
VIGNET Pierre's avatar
VIGNET Pierre committed
778
779
        @warning: lock the unfolder
        """
780
781
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
VIGNET Pierre's avatar
VIGNET Pierre committed
782
783
784

        # Old API
        # Less efficient with abs()
785
786
        # return [(abs(lit) + self.__shift_step) * (-1 if lit < 0 else 1)
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
787
788
        # More efficient with ternary assignment
        # return [(lit + self.__shift_step) if lit > 0 else (lit - self.__shift_step)
789
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
790
791

        # New API via C++ module
792
        return shift_clause(numeric_clause, self.__shift_step)
793

794
    def __m_shift_clause(self, numeric_clause, nb_steps):
795
796
        """Shift a clause for the given step number

797
798
799
800
801
802
803
804
        Each literal will be shifted by (nb_steps * __shift_step).

        Why ?
        Such function is used for clauses that are not already shifted during
        previous steps. It is the case of variant_constraints which come from a
        reloaded/forced trajectory.

        About unfolder lock and shift_step:
805
806
807
808
809
        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.

810
811
        Called by: __shift_variant()

812
        @param numeric_clause: DIMACS clause
813
        @param nb_steps: number of shifts asked
VIGNET Pierre's avatar
VIGNET Pierre committed
814
815
        @warning: lock the unfolder
        """
816
817
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
818

819
        return [(lit + self.__shift_step * nb_steps) if lit > 0
820
                else (lit - self.__shift_step * nb_steps) for lit in numeric_clause]
821

VIGNET Pierre's avatar
VIGNET Pierre committed
822
    def __shift_dynamic(self):
823
824
825
826
        """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
827

828
829
        .. note:: Called by shift()
        """
830
831
832
833
834
835
836

        if len(self.__precomputed_dynamic_constraints) > self.__current_step:
            # Recall the saved state of the system for the next step
            self.__dynamic_constraints.append(
                self.__precomputed_dynamic_constraints[self.__current_step]
            )
            LOGGER.info(
837
                "shift_dynamic:: OPTI DO NOT SHIFT; "
838
839
840
841
842
843
844
                "Reload dynamic constraints; step: %s",
                self.__current_step
            )
            return

        # System has not been shifted for this step until now
        LOGGER.info(
845
                "shift_dynamic:: SHIFT; "
846
847
848
849
850
                "Set dynamic constraints; step: %s; dyn consts len: %s",
                self.__current_step,
                len(self.__dynamic_constraints)
            )

VIGNET Pierre's avatar
VIGNET Pierre committed
851
852
853
854
855
856
857
        # Old API
        # self.__dynamic_constraints.append(
        #   [self.__shift_clause(clause)
        #    for clause in self.__dynamic_constraints[-1]]
        # )

        # New API via C++ module
858
859
        # __dynamic_constraints:
        # List of lists of DIMACS encoded clauses (lists of ints)
VIGNET Pierre's avatar
VIGNET Pierre committed
860
        self.__dynamic_constraints.append(
861
            shift_dimacs_clauses(
862
                self.__dynamic_constraints[-1], # <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
863
864
865
                self.__shift_step
            )
        )
866

VIGNET Pierre's avatar
VIGNET Pierre committed
867
    def __shift_initial(self):
868
        """Shift initialisation condition
869

870
871
        Shift + replace __initial_constraints

872
873
874
875
        .. note:: Called by:
            - shift()
            - init_backward_unfolding()
        """
876
        self.__initial_constraints = \
877
            shift_dimacs_clauses(
878
879
880
                self.__initial_constraints,
                self.__shift_step
            )
881

VIGNET Pierre's avatar
VIGNET Pierre committed
882
    def __shift_final(self):
883
        """Shift final property
884

885
886
        Shift + replace __final_constraints

887
888
889
890
        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
        """
891
        self.__final_constraints = \
892
            shift_dimacs_clauses(
893
894
895
                self.__final_constraints,
                self.__shift_step
            )
896

VIGNET Pierre's avatar
VIGNET Pierre committed
897
    def __shift_invariant(self):
898
899
        """Shift invariant property

900
901
        Shift + append of the last element of __invariant_constraints

902
903
904
905
        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
            - init_backward_unfolding()
VIGNET Pierre's avatar
VIGNET Pierre committed
906
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
907
        if self.__invariant_constraints:
VIGNET Pierre's avatar
VIGNET Pierre committed
908
909
            # New API via C++ module
            self.__invariant_constraints.append(
910
                shift_dimacs_clauses(
VIGNET Pierre's avatar
VIGNET Pierre committed
911
912
913
914
                    self.__invariant_constraints[-1],
                    self.__shift_step
                )
            )
915

VIGNET Pierre's avatar
VIGNET Pierre committed
916
    def __shift_variant(self):
917
918
        """Shift variant property - depends on unfolding direction

919
920
        Shift clauses of the current step in __list_variant_constraints, and
        append them to __variant_constraints.
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936

        .. warning:: Refactor note: unclear function. No apparent reason for
            only the first clause to be shifted...

        Process:
            - Take the clauses (constraint) of the current step
            - Shift the first clause
            - Append it to __variant_constraints
            - Stop ????

            Example:
            current_step: 2 (shift for step 3)
            [[], [[4], [4]], [[6], [7]], []]
            => Only [6] is shifted...

        .. note:: Called by shift()
937
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
938
939
940
        if not self.__list_variant_constraints:
            return
        if self.__shift_direction == "FORWARD":
941
942
            # Constraint t0 already included from the query during initialisation
            current_constraint = self.__list_variant_constraints[self.__current_step]
943
            # Shift constraints at current step and append them to __variant_constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
944
            for clause in current_constraint:
945
                s_clause = self.__m_shift_clause(clause, self.__current_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
946
                self.__variant_constraints.append(s_clause)
947
948
                return # ?????
        elif self.__shift_direction == "BACKWARD":
VIGNET Pierre's avatar
VIGNET Pierre committed
949
950
            raise MCLException("Not yet implemented")
        else:
951
            raise MCLException("Shift incoherent data: " + self.__shift_direction)
952
953


VIGNET Pierre's avatar
VIGNET Pierre committed
954
    def shift(self):
955
        """Shift all clauses of the system to prepare it for the next step.
956
957
958

        self.__current_step is incremented here!

959
        Modified attributes:
960
            - __dynamic_constraints[-1] (last element)
961
                Shift + append of the last element of __dynamic_constraints
962
            - __invariant_constraints[-1] (last element)
963
964
965
966
                Shift + append of the last element of __invariant_constraints
            - __list_variant_constraints[current_step]
                Shift clauses of the current step in __list_variant_constraints,
                and append them to __variant_constraints.
967
968
            - __final_constraints if __shift_direction is "FORWARD"
            - __initial_constraints if __shift_direction is "BACKWARD"
969

970
971
972
            PS: __initial_constraints are left as this for now
            (shifted only with BACKWARD shift direction)

973
974
975
        Called at each step by:
            - squery_solve()
            - squery_is_satisfied()
VIGNET Pierre's avatar
VIGNET Pierre committed
976
        """
977
978
979
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True

VIGNET Pierre's avatar
VIGNET Pierre committed
980
981
982
983
984
985
986
987
        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:
988
            # Shift direction must be set
989
            raise MCLException("Shift incoherent data: " + self.__shift_direction)
990
991

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

994
    ## Coding of properties ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
995
    def __compile_property(self, property_text):
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
        """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
1007
1008
        """
        if self.__locked:
VIGNET Pierre's avatar
VIGNET Pierre committed
1009
1010
            raise MCLException("Trying to compile property while unfolder is locked")

1011
1012
        # Syntax analyser and type checker
        # Compile a condition expression to a tree representation
VIGNET Pierre's avatar
VIGNET Pierre committed
1013
        tree_prop = compile_cond(
1014
1015
1016
1017
1018
            property_text,
            self.dynamic_system.symb_tab,
            self.dynamic_system.report
        )
        # Avoid name collisions of aux var
1019
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
1020
1021
1022
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses