CLUnfolder.py 67.7 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
275
        # Include auxiliary clause to eliminate undesirable solutions
        # If A->B has clock h, an aux constraint added is h included in h when A
        # Must be set to False for inhibitors computations
        self.__include_aux_clauses = True
        self.__lit_cpt = self.__shift_step + 1    # counter for aux. var. coding
276

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

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

287
        # ordered list of DIMACS codes of the frontier variables/places
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
        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)
309
310
311
312
        self.frontiers_pos_and_neg = \
            self.frontiers_negative_values | frozenset(self.frontier_values)

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

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

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

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

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

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

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

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


    def reset(self):
356
357
        """Reset the unfolder before a new query

358
359
360
        Reset only properties and dimacs clauses from the current query;
        AND __list_variant_constraints.

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

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

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

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

390
391
392
    def init_with_query(self, query):
        """Initialise the unfolder with the given query

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

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

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

411
412
        self.__final_property = query.final_prop # logical formula in text
        self.__dimacs_final = query.dim_final
413

414
415
        self.__invariant_property = query.inv_prop # logical formula in text
        self.__dimacs_invariant = query.dim_inv
416
417

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

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
440
441
442
    def set_include_aux_clauses(self, val):
        """
        Include auxiliary clause to eliminate undesirable solutions
443
        If A->B has clock h, an aux constraint added is h included in h when A
VIGNET Pierre's avatar
VIGNET Pierre committed
444
445
446
        Must be set to False for inhibitors computations
        """
        self.__include_aux_clauses = val
447

448
    ## Internal variable access for tests (never used) #########################
449
450
    @property
    def dynamic_constraints(self):
451
        """For tests: returns coded dynamic constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
452
        return self.__dynamic_constraints
453

454
455
    @property
    def initial_constraints(self):
456
        """For tests: returns coded initial constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
457
        return self.__initial_constraints
458

459
460
    @property
    def invariant_constraints(self):
461
        """For tests: returns coded invariant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
462
        return self.__invariant_constraints
463

464
465
    @property
    def variant_constraints(self):
466
        """For tests: returns coded variant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
467
        return self.__variant_constraints
468

469
470
    @property
    def final_constraints(self):
471
        """For tests: returns coded final constraints"""
472
        return self.__final_constraints
473

474
    ## Variables management ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
475
476
    def var_names_in_clause(self, clause):
        """Return the names of the variables from values in the given numeric clause
477
478
479
480
        (DEBUG never used)
        """
        return [self.get_var_indexed_name(var) for var in clause]

VIGNET Pierre's avatar
VIGNET Pierre committed
481
    def var_dimacs_code(self, var_name):
482
        """Returns DIMACS code of var_name (string) variable (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
483
        return self.__var_code_table[var_name]
484

VIGNET Pierre's avatar
VIGNET Pierre committed
485
    def get_system_var_number(self):
486
487
        """Get number of variables in the clause constraint dynamical system
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
488
489
490

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

VIGNET Pierre's avatar
VIGNET Pierre committed
494
    def get_var_number(self):
495
496
        """Get number of principal variables (properties excluded) in the unfolder
        (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_system_var_number()
VIGNET Pierre's avatar
VIGNET Pierre committed
500
        """
501
502
        # Remove the blacklisted first item (##) for variables naming
        return len(self.__var_list) - 1
503

VIGNET Pierre's avatar
VIGNET Pierre committed
504
    def get_var_name(self, var_num):
505
506
507
508
        """Get name of the variable

        .. seealso:: Explanations on get_var_indexed_name()

VIGNET Pierre's avatar
VIGNET Pierre committed
509
        @param var_num: DIMACS literal coding of an initial variable
510
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
511
        """
512
        # Get the original var_code without shifts
513
        var_code = (abs(var_num) - 1) % self.__shift_step + 1
514
        if var_code <= self.shift_step_init:
515
516
            # 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
517
            return self.__var_list[var_code]
518
519
520
        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
521
            #raise MCLException("Not a DIMACS code of an initial variable")
522

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

VIGNET Pierre's avatar
VIGNET Pierre committed
562
    def get_free_clocks(self):
563
        """Get the DIMACS codes of the free_clocks variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
564
        return self.__free_clocks
565

VIGNET Pierre's avatar
VIGNET Pierre committed
566
    def get_inputs(self):
567
        """Get the DIMACS codes of the input variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
568
        return self.__inputs
569

VIGNET Pierre's avatar
VIGNET Pierre committed
570
571
572
573
574
    def get_shift_direction(self):
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
575

VIGNET Pierre's avatar
VIGNET Pierre committed
576
577
578
579
580
    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
581

VIGNET Pierre's avatar
VIGNET Pierre committed
582
583
584
585
586
587
    def get_current_step(self):
        """
        @return: the current number of unfolding
        """
        return self.__current_step

588

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

623

VIGNET Pierre's avatar
VIGNET Pierre committed
624
    def __backward_code(self, clause):
625
626
627
628
629
630
        """(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
631
632
633
634
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
635
636
637
638
639
640
641
642
643
644
645
646
647
        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
648
        return num_clause
649

VIGNET Pierre's avatar
VIGNET Pierre committed
650
    def __code_clause(self, clause):
651
652
653
654
655
        """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;
656
        assume all variables are basic variables (t=0) (not shifted).
657

658
659
660
661
        @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.
662
663
664
665
666
667

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

693
    ## Dynamic initialisations #################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
694
    def __forward_init_dynamic(self):
695
696
        """Dynamics initialisations.
        Set dynamic constraints for a forward one step: X1 = f(X0)
697

VIGNET Pierre's avatar
VIGNET Pierre committed
698
        Numerically code clauses with the numeric codes found in
699
700
        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
701
702
703
704
705
        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.
706

707
708
        .. seealso:: __forward_code()

709
        .. note:: Called by init_forward_unfolding()
710

711
712
713
714
        .. note:: Future variables x' are noted "name`" in Literal names.

        .. note:: Values of variables increases of __shift_step in future steps.
        """
715
        # New API via C++ module
716
        # TODO: take a look at __backward_init_dynamic & __backward_code
VIGNET Pierre's avatar
VIGNET Pierre committed
717
        if self.__include_aux_clauses:
718
            # Auxiliary clauses are supported (default)
719
            self.__dynamic_constraints = \
720
                forward_init_dynamic(self.dynamic_system.list_clauses,
721
722
                                     self.__var_code_table,
                                     self.__shift_step,
723
                                     self.dynamic_system.aux_list_clauses)
724
725
        else:
            self.__dynamic_constraints = \
726
                forward_init_dynamic(self.dynamic_system.list_clauses,
727
728
                                     self.__var_code_table,
                                     self.__shift_step)
729

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

734
735
        .. note:: Called by init_backward_unfolding()
        """
736
737
        num_clause_list = \
            [self.__backward_code(clause)
738
             for clause in self.dynamic_system.list_clauses]
739

VIGNET Pierre's avatar
VIGNET Pierre committed
740
        if self.__include_aux_clauses:
741
742
            num_clause_list += \
                [self.__backward_code(clause)
743
                 for clause in self.dynamic_system.aux_list_clauses]
744

745
        self.__dynamic_constraints = [num_clause_list]
746

747
    ## Shifting variables: implementation of the shift operator ################
748
    def __shift_clause(self, numeric_clause):
749
750
        """Shift a clause for the current __shift_step

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

753
754
755
        Basically, `shift_step` is added to positive variables and subtracted
        from negative variables in `numeric_clause`.

756
        About unfolder lock and shift_step:
757
758
759
760
761
        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.

762
        @param numeric_clause: DIMACS clause
VIGNET Pierre's avatar
VIGNET Pierre committed
763
764
        @warning: lock the unfolder
        """
765
766
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
VIGNET Pierre's avatar
VIGNET Pierre committed
767
768
769

        # Old API
        # Less efficient with abs()
770
771
        # return [(abs(lit) + self.__shift_step) * (-1 if lit < 0 else 1)
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
772
773
        # More efficient with ternary assignment
        # return [(lit + self.__shift_step) if lit > 0 else (lit - self.__shift_step)
774
        #         for lit in numeric_clause]
VIGNET Pierre's avatar
VIGNET Pierre committed
775
776

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

779
    def __m_shift_clause(self, numeric_clause, nb_steps):
780
781
        """Shift a clause for the given step number

782
783
784
785
786
787
788
789
        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:
790
791
792
793
794
        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.

795
796
        Called by: __shift_variant()

797
        @param numeric_clause: DIMACS clause
798
        @param nb_steps: number of shifts asked
VIGNET Pierre's avatar
VIGNET Pierre committed
799
800
        @warning: lock the unfolder
        """
801
802
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
803

804
        return [(lit + self.__shift_step * nb_steps) if lit > 0
805
                else (lit - self.__shift_step * nb_steps) for lit in numeric_clause]
806

VIGNET Pierre's avatar
VIGNET Pierre committed
807
    def __shift_dynamic(self):
808
809
810
811
        """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
812

813
814
        .. note:: Called by shift()
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
815
816
817
818
819
820
821
        # Old API
        # self.__dynamic_constraints.append(
        #   [self.__shift_clause(clause)
        #    for clause in self.__dynamic_constraints[-1]]
        # )

        # New API via C++ module
822
823
        # __dynamic_constraints:
        # List of lists of DIMACS encoded clauses (lists of ints)
VIGNET Pierre's avatar
VIGNET Pierre committed
824
825
        self.__dynamic_constraints.append(
            shift_dynamic(
826
                self.__dynamic_constraints[-1], # <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
827
828
829
                self.__shift_step
            )
        )
830

VIGNET Pierre's avatar
VIGNET Pierre committed
831
    def __shift_initial(self):
832
        """Shift initialisation condition
833

834
835
        Shift + replace __initial_constraints

836
837
838
839
        .. note:: Called by:
            - shift()
            - init_backward_unfolding()
        """
840
        self.__initial_constraints = \
841
842
843
844
            shift_dynamic(
                self.__initial_constraints,
                self.__shift_step
            )
845

VIGNET Pierre's avatar
VIGNET Pierre committed
846
    def __shift_final(self):
847
        """Shift final property
848

849
850
        Shift + replace __final_constraints

851
852
853
854
        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
        """
855
        self.__final_constraints = \
856
857
858
859
            shift_dynamic(
                self.__final_constraints,
                self.__shift_step
            )
860

VIGNET Pierre's avatar
VIGNET Pierre committed
861
    def __shift_invariant(self):
862
863
        """Shift invariant property

864
865
        Shift + append of the last element of __invariant_constraints

866
867
868
869
        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
            - init_backward_unfolding()
VIGNET Pierre's avatar
VIGNET Pierre committed
870
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
871
        if self.__invariant_constraints:
VIGNET Pierre's avatar
VIGNET Pierre committed
872
873
874
875
876
877
878
            # New API via C++ module
            self.__invariant_constraints.append(
                shift_dynamic(
                    self.__invariant_constraints[-1],
                    self.__shift_step
                )
            )
879

VIGNET Pierre's avatar
VIGNET Pierre committed
880
    def __shift_variant(self):
881
882
        """Shift variant property - depends on unfolding direction

883
884
        Shift clauses of the current step in __list_variant_constraints, and
        append them to __variant_constraints.
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900

        .. 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()
901
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
902
903
904
        if not self.__list_variant_constraints:
            return
        if self.__shift_direction == "FORWARD":
905
906
            # Constraint t0 already included from the query during initialisation
            current_constraint = self.__list_variant_constraints[self.__current_step]
907
            # Shift constraints at current step and append them to __variant_constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
908
            for clause in current_constraint:
909
                s_clause = self.__m_shift_clause(clause, self.__current_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
910
                self.__variant_constraints.append(s_clause)
911
912
                return # ?????
        elif self.__shift_direction == "BACKWARD":
VIGNET Pierre's avatar
VIGNET Pierre committed
913
914
            raise MCLException("Not yet implemented")
        else:
915
            raise MCLException("Shift incoherent data: " + self.__shift_direction)
916
917


VIGNET Pierre's avatar
VIGNET Pierre committed
918
    def shift(self):
919
        """Shift all clauses of the system to prepare it for the next step.
920
921
922

        self.__current_step is incremented here!

923
        Modified attributes:
924
            - __dynamic_constraints[-1] (last element)
925
                Shift + append of the last element of __dynamic_constraints
926
            - __invariant_constraints[-1] (last element)
927
928
929
930
                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.
931
932
            - __final_constraints if __shift_direction is "FORWARD"
            - __initial_constraints if __shift_direction is "BACKWARD"
933

934
935
936
            PS: __initial_constraints are left as this for now
            (shifted only with BACKWARD shift direction)

937
938
939
        Called at each step by:
            - squery_solve()
            - squery_is_satisfied()
VIGNET Pierre's avatar
VIGNET Pierre committed
940
        """
941
942
943
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True

VIGNET Pierre's avatar
VIGNET Pierre committed
944
945
946
947
948
949
950
951
        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:
952
            # Shift direction must be set
953
            raise MCLException("Shift incoherent data: " + self.__shift_direction)
954
955

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

958
    ## Coding of properties ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
959
    def __compile_property(self, property_text):
960
961
962
963
964
965
966
967
968
969
970
        """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
971
972
        """
        if self.__locked:
VIGNET Pierre's avatar
VIGNET Pierre committed
973
974
            raise MCLException("Trying to compile property while unfolder is locked")

975
976
        # Syntax analyser and type checker
        # Compile a condition expression to a tree representation
VIGNET Pierre's avatar
VIGNET Pierre committed
977
        tree_prop = compile_cond(
978
979
980
981
982
            property_text,
            self.dynamic_system.symb_tab,
            self.dynamic_system.report
        )
        # Avoid name collisions of aux var
983
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
984
985
986
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
987

VIGNET Pierre's avatar
VIGNET Pierre committed
988
    def __compile_event(self, property_text):
989
990
991
992
993
994
995
996
997
        """Compile an event (biosignal expression) into clauses

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

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

        .. note:: Called by:
            - __init_variant_constraints_0()
VIGNET Pierre's avatar
VIGNET Pierre committed
998
999
        """
        if self.__locked:
1000
1001
1002
            raise MCLException("Trying to compile property while unfolder is locked")

        # Syntax analyser and type checker
1003
1004
1005
1006
        # Compile an event expression to a tree representation
        # tree_prop is the event expression,
        # ste the state events (s#> ..) used and
        # fcl is the free clocks used in the event expression.
1007
1008
        tr