CLUnfolder.py 69.8 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
162
163
164
165

# C++ API
from _cadbiom import shift_clause, shift_dynamic, forward_code, \
                     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

VIGNET Pierre's avatar
VIGNET Pierre committed
585
586
587
588
589
    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
590

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

597

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

632

VIGNET Pierre's avatar
VIGNET Pierre committed
633
    def __backward_code(self, clause):
634
635
636
637
638
639
        """(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
640
641
642
643
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
644
645
646
647
648
649
650
651
652
653
654
655
656
        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
657
        return num_clause
658

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

667
668
669
670
        @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.
671
672
673
674
675
676

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
707
        Numerically code clauses with the numeric codes found in
708
709
        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
710
711
712
713
714
        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.
715

716
717
        .. seealso:: __forward_code()

718
        .. note:: Called by init_forward_unfolding()
719

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

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

739
740
741
742
        # __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
743
    def __backward_init_dynamic(self):
744
745
        """Dynamics initialisations. (never used, backward is partially implemented)
        Set dynamic constraints for a forward one step: X0 = f(X1)
746

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

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

758
        self.__dynamic_constraints = [num_clause_list]
759

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

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

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

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

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

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

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

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

795
796
797
798
799
800
801
802
        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:
803
804
805
806
807
        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.

808
809
        Called by: __shift_variant()

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

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

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

826
827
        .. note:: Called by shift()
        """
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848

        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(
                "__shift_dynamic:: OPTI-DO NOT SHIFT; "
                "Reload dynamic constraints; step: %s",
                self.__current_step
            )
            return

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

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

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

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

868
869
        Shift + replace __initial_constraints

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

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

883
884
        Shift + replace __final_constraints

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

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

898
899
        Shift + append of the last element of __invariant_constraints

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

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

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

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


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

        self.__current_step is incremented here!

957
        Modified attributes:
958
            - __dynamic_constraints[-1] (last element)
959
                Shift + append of the last element of __dynamic_constraints
960
            - __invariant_constraints[-1] (last element)
961
962
963
964
                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.
965
966
            - __final_constraints if __shift_direction is "FORWARD"
            - __initial_constraints if __shift_direction is "BACKWARD"
967

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

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

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

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

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

1009
1010
        # Syntax analyser and type checker
        # Compile a condition expression to a tree representation
VIGNET Pierre's avatar
VIGNET Pierre committed
1011
        tree_prop = compile_cond(
1012