CLUnfolder.py 58.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
42
43
44
##
## Contributor(s): Geoffroy Andrieux IRSET
##
"""
Main engine for constraint unfolding and solving
"""
45
46
from __future__ import print_function

VIGNET Pierre's avatar
VIGNET Pierre committed
47
48
#from pyCryptoMS import CryptoMS
from pycryptosat import Solver as CryptoMS
49
50
51
from cadbiom.models.biosignal.translators.gt_visitors import compile_cond, compile_event
from cadbiom.models.clause_constraints.CLDynSys import Clause, Literal
from cadbiom.models.clause_constraints.mcl.MCLSolutions import RawSolution, MCLException
52
from cadbiom import commons as cm
VIGNET Pierre's avatar
VIGNET Pierre committed
53
54
55
56
57
58

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

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

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
75
76
77
78
    Dynamic constraints unfolding management
    ========================================
    Each variable is coded as an integer (in var_code_table and var_list).
    Each clause is represented as a list of signed integers (DIMACS coding).
VIGNET Pierre's avatar
VIGNET Pierre committed
79

VIGNET Pierre's avatar
VIGNET Pierre committed
80
81
    During unfolding, clauses are shifted either to the future (forward) or
    to the past (backward). The shift operator is a simple addition
82
83
    of self.__shift_step. The shift direction depends only on initializations.
    self.__shift_step depends on the number of variables so it is impossible
VIGNET Pierre's avatar
VIGNET Pierre committed
84
    to add variables while generating a trajectory unfolding.
85
86

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

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

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

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

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

        # Fix order of variables names with a list:
127
128
        # - indexes of __var_list are the values of the variables at these indexes
        # - values begin from 1 (0 is a blacklisted value)
129
130
        base_var_set = list(dynamic_system.base_var_set)
        self.__var_list += base_var_set
131
        # keys: are the names of the variables, values: their values
132
133
134
135
136
137
138
139
140
141
142
143
144
        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)
145

146
        assert len(self.__var_code_table) == 2 * self.__shift_step
147

148
149
150
151
152
        # 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
153

154
155
156
157
        # 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
158
        self.__aux_list = []                      # code to name
159

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

164
        # ordered list of DIMACS codes of the frontier variables/places
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
        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)
186
187
188
189
        self.frontiers_pos_and_neg = \
            self.frontiers_negative_values | frozenset(self.frontier_values)

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

192
        # DIMACS codes of the free_clocks variables/places for extraction (invariant)
193
        self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.dynamic_system.free_clocks)
194
195

        # Binding for a merged version of __inputs and __free_clocks
196
        # Convenient attribute for RawSolution.extract_act_input_clock_seq()
197
198
        # DIMACS codes of the input and free_clocks variables
        self.inputs_and_free_clocks = self.__inputs | self.__free_clocks
199

200
201
        # Properties to be checked
        self.reset()
202

203
        # Logical constraints:
204
        # Result from unfolding of base constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
205
206
207
208
209
        # 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
210
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
VIGNET Pierre's avatar
VIGNET Pierre committed
211

212
        # Simple temporal properties:
VIGNET Pierre's avatar
VIGNET Pierre committed
213
214
        # SP(X0): Initial property/start property; Never change at each step.
        # IP(X): Invariant property
215
        # VP(X): Variant property
VIGNET Pierre's avatar
VIGNET Pierre committed
216
        #   List of logical formulas of properties forced at each step
217
        #   It's the trajectory of events of a solution.
VIGNET Pierre's avatar
VIGNET Pierre committed
218
219
        # FP(X): Final property

220
        self.__initial_constraints = []        # DIMACS clauses: C(X_0) <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
221
222
        self.__final_constraints   = []        # idem: C(X_n)
        self.__invariant_constraints = []      # DIMACS clauses: C(X_i))
223
        self.__variant_constraints = []        # variant constraints along trajectory
224
        self.__shift_direction = None          # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
225
226
227
228
229
230
231
232

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


    def reset(self):
233
234
        """Reset the unfolder before a new query

235
236
237
        Reset only properties and dimacs clauses from the current query;
        AND __list_variant_constraints.

238
        This function is called from the constructor and during
239
240
        MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_solutions()
        following the call of init_with_query().
VIGNET Pierre's avatar
VIGNET Pierre committed
241
        """
242
        # Properties to be checked
243
        self.__initial_property = None            # logical formula - literal boolean expression
244
        self.__dimacs_initial = None              # list of DIMACS clauses
245
        self.__final_property = None              # logical formula
246
        self.__dimacs_final = None                # list of DIMACS clauses
247
        self.__invariant_property = None          # logical formula
248
        self.__dimacs_invariant = None            # list of DIMACS clauses
249
        self.__variant_property = None            # list<logic formulas>
250
        self.__dimacs_variant = None              # list<list<DIMACS clauses>>
251
        # list of variant temporal constraints in Dimacs ground code
252
        self.__list_variant_constraints = None    # list<list<DIMACS clauses>>
253

254
255
        # If this function is called from the constructor,
        # the following variables are just redefined here.
256
257
258

        # For reachability optimisation. Number of shifts before checking
        # the final property
VIGNET Pierre's avatar
VIGNET Pierre committed
259
        self.__steps_before_check = 0
260
        self.__shift_direction = None             # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
261
        self.__locked = False
262

263
264
265
    def init_with_query(self, query):
        """Initialise the unfolder with the given query

266
        Following attributes are used from the query:
267
            start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
268
            variant_prop, dim_variant_prop, steps_before_check
269
270
271
272
273

        Textual properties of query are compiled into numeric clauses in
        init_forward_unfolding(), just before squery_is_satisfied() and
        squery_solve().
        This compilation step is costly due to ANTLR performances...
274
275
276
        """
        # Reset the unfolder before a new query
        self.reset()
277
        # Init with query properties and clauses
278
279
        self.__initial_property = query.start_prop # logical formula in text
        self.__dimacs_initial = query.dim_start
280

281
282
        self.__final_property = query.final_prop # logical formula in text
        self.__dimacs_final = query.dim_final
283

284
285
        self.__invariant_property = query.inv_prop # logical formula in text
        self.__dimacs_invariant = query.dim_inv
286
287

        # It's the trajectory of events of a solution.
288
289
        self.__variant_property = query.variant_prop # logical formula in text
        self.__dimacs_variant = query.dim_variant_prop
290

291
292
293
        # For reachability optimisation. Number of shifts before checking
        # the final property (default 0)
        self.__steps_before_check = query.steps_before_check
294

VIGNET Pierre's avatar
VIGNET Pierre committed
295
    def set_stats(self):
296
        """Enable solver statistics (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
297
298
299
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
300

VIGNET Pierre's avatar
VIGNET Pierre committed
301
    def unset_stats(self):
302
        """Disable solver statistics (never used)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
303
        self.__stats = False
304

VIGNET Pierre's avatar
VIGNET Pierre committed
305
    def _stats(self):
306
307
308
        """Display solver statistics"""
        print("\n NB Variables in solver:", self.__nb_vars)
        print("NB Clauses in solver:", self.__nb_clauses)
309

VIGNET Pierre's avatar
VIGNET Pierre committed
310
311
312
    def set_include_aux_clauses(self, val):
        """
        Include auxiliary clause to eliminate undesirable solutions
313
        If A->B has clock h, an aux constraint added is h included in h when A
VIGNET Pierre's avatar
VIGNET Pierre committed
314
315
316
        Must be set to False for inhibitors computations
        """
        self.__include_aux_clauses = val
317

318
    ## Internal variable access for tests (never used) #########################
319
320
    @property
    def dynamic_constraints(self):
321
        """For tests: returns coded dynamic constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
322
        return self.__dynamic_constraints
323

324
325
    @property
    def initial_constraints(self):
326
        """For tests: returns coded initial constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
327
        return self.__initial_constraints
328

329
330
    @property
    def invariant_constraints(self):
331
        """For tests: returns coded invariant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
332
        return self.__invariant_constraints
333

334
335
    @property
    def variant_constraints(self):
336
        """For tests: returns coded variant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
337
        return self.__variant_constraints
338

339
340
    @property
    def final_constraints(self):
341
        """For tests: returns coded final constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
342
        self.__final_constraints
343

344
    ## Variables management ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
345
346
    def var_names_in_clause(self, clause):
        """Return the names of the variables from values in the given numeric clause
347
348
349
350
        (DEBUG never used)
        """
        return [self.get_var_indexed_name(var) for var in clause]

VIGNET Pierre's avatar
VIGNET Pierre committed
351
    def var_dimacs_code(self, var_name):
352
        """Returns DIMACS code of var_name (string) variable (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
353
        return self.__var_code_table[var_name]
354

VIGNET Pierre's avatar
VIGNET Pierre committed
355
    def get_system_var_number(self):
356
357
        """Get number of variables in the clause constraint dynamical system
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
358
359
360

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

VIGNET Pierre's avatar
VIGNET Pierre committed
364
    def get_var_number(self):
365
366
        """Get number of principal variables (properties excluded) in the unfolder
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
367
368
369

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

VIGNET Pierre's avatar
VIGNET Pierre committed
374
    def get_var_name(self, var_num):
375
376
377
378
        """Get name of the variable

        .. seealso:: Explanations on get_var_indexed_name()

VIGNET Pierre's avatar
VIGNET Pierre committed
379
        @param var_num: DIMACS literal coding of an initial variable
380
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
381
        """
382
        # Get the original var_code without shifts
383
        var_code = (abs(var_num) - 1) % self.__shift_step + 1
384
        if var_code <= self.shift_step_init:
385
386
            # 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
387
            return self.__var_list[var_code]
388
389
390
        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
391
            #raise MCLException("Not a DIMACS code of an initial variable")
392

VIGNET Pierre's avatar
VIGNET Pierre committed
393
    def get_var_indexed_name(self, var_num):
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
        """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
416
        @param var_num: DIMACS literal coding
417
        @return: name of the variable with the time index appended
VIGNET Pierre's avatar
VIGNET Pierre committed
418
        """
419
        varnum1 = abs(var_num)
420
        # Get the original var_code without shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
421
        var_code = (varnum1 - 1) % self.__shift_step + 1
422
        var_step = (varnum1 - var_code) / self.__shift_step
423
        if var_code <= self.shift_step_init:
424
425
            # 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
426
427
            return self.__var_list[var_code] + '_%s'% var_step
        else:
428
429
            # Auxiliary variable introduced by properties compilation
            index = var_code - self.shift_step_init - 1
VIGNET Pierre's avatar
VIGNET Pierre committed
430
            return self.__aux_list[index] + '_%s'% var_step
431

VIGNET Pierre's avatar
VIGNET Pierre committed
432
    def get_free_clocks(self):
433
        """Get the DIMACS codes of the free_clocks variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
434
        return self.__free_clocks
435

VIGNET Pierre's avatar
VIGNET Pierre committed
436
    def get_inputs(self):
437
        """Get the DIMACS codes of the input variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
438
        return self.__inputs
439

VIGNET Pierre's avatar
VIGNET Pierre committed
440
441
442
443
444
    def get_shift_direction(self):
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
445

VIGNET Pierre's avatar
VIGNET Pierre committed
446
447
448
449
450
    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
451

VIGNET Pierre's avatar
VIGNET Pierre committed
452
453
454
455
456
457
    def get_current_step(self):
        """
        @return: the current number of unfolding
        """
        return self.__current_step

458

459
    ## Translation from names to num codes #####################################
VIGNET Pierre's avatar
VIGNET Pierre committed
460
    ## The translation depends on the shift direction
VIGNET Pierre's avatar
VIGNET Pierre committed
461
    def __forward_code(self, clause):
462
463
464
465
466
467
468
469
470
        """(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
471
472
473
        @param clause: a Clause object
        @return: the DIMACS coding of the forward shifted clause
        """
474
475
        # Old API
        # num_clause = []
476
        # for lit in clause.literals:
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
        #     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)

493

VIGNET Pierre's avatar
VIGNET Pierre committed
494
    def __backward_code(self, clause):
495
496
497
498
499
500
        """(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
501
502
503
504
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
505
506
507
508
509
510
511
512
513
514
515
516
517
        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
518
        return num_clause
519

VIGNET Pierre's avatar
VIGNET Pierre committed
520
    def __code_clause(self, clause):
521
522
523
524
525
526
527
        """Numerically code a clause

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

VIGNET Pierre's avatar
VIGNET Pierre committed
528
        @warning: MODIFIES SHIFT_STEP if auxiliary variables are present (numeric code)
529
530
531
532
533
534
535
            Because we add a variable in the system...

        :param clause:
        :return: List of numerical values corresponding to the literals
            in the given clause.
        :type clause: <Clause>
        :rtype: <list <int>>
VIGNET Pierre's avatar
VIGNET Pierre committed
536
537
        """
        num_clause = []
538
        for lit in clause.literals:
539
            # Get variable value with the given name
VIGNET Pierre's avatar
VIGNET Pierre committed
540
            name = lit.name
541
            if name in self.__var_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
542
                var_cod = self.__var_code_table[name]
543
            elif name in self.__aux_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
544
                var_cod = self.__aux_code_table[name]
545
546
            else:
                # Create an auxiliary variable - modifies shift_step (nb of variables)
VIGNET Pierre's avatar
VIGNET Pierre committed
547
                self.__shift_step += 1
548
                # Mapping name to value code
VIGNET Pierre's avatar
VIGNET Pierre committed
549
                self.__aux_code_table[name] = self.__shift_step
550
                # Mapping value code to name
VIGNET Pierre's avatar
VIGNET Pierre committed
551
                self.__aux_list.append(name)
552
553
554
555
556
                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
557
558
            num_clause.append(lit_code)
        return num_clause
559

560
    ## Dynamic initialisations #################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
561
    def __forward_init_dynamic(self):
562
563
        """Dynamics initialisations.
        Set dynamic constraints for a forward one step: X1 = f(X0)
564

VIGNET Pierre's avatar
VIGNET Pierre committed
565
        Numerically code clauses with the numeric codes found in
566
567
        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
568
569
570
571
572
        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.
573
574

        .. note:: Called by init_forward_unfolding()
575

576
577
578
579
        .. note:: Future variables x' are noted "name`" in Literal names.

        .. note:: Values of variables increases of __shift_step in future steps.
        """
580
        # New API via C++ module
581
        # TODO: take a look at __backward_init_dynamic & __backward_code
VIGNET Pierre's avatar
VIGNET Pierre committed
582
        if self.__include_aux_clauses:
583
            # Auxiliary clauses are supported (default)
584
            self.__dynamic_constraints = \
585
                forward_init_dynamic(self.dynamic_system.list_clauses,
586
587
                                     self.__var_code_table,
                                     self.__shift_step,
588
                                     self.dynamic_system.aux_list_clauses)
589
590
        else:
            self.__dynamic_constraints = \
591
                forward_init_dynamic(self.dynamic_system.list_clauses,
592
593
                                     self.__var_code_table,
                                     self.__shift_step)
594

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

599
600
        .. note:: Called by init_backward_unfolding()
        """
601
602
        num_clause_list = \
            [self.__backward_code(clause)
603
             for clause in self.dynamic_system.list_clauses]
604

VIGNET Pierre's avatar
VIGNET Pierre committed
605
        if self.__include_aux_clauses:
606
607
            num_clause_list += \
                [self.__backward_code(clause)
608
                 for clause in self.dynamic_system.aux_list_clauses]
609

610
        self.__dynamic_constraints = [num_clause_list]
611

612
    ## Shifting variables: implementation of the shift operator ################
VIGNET Pierre's avatar
VIGNET Pierre committed
613
    def __shift_clause(self, ncl):
614
615
        """Shift a clause for the current __shift_step

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

618
619
620
        Basically, `shift_step` is added to positive variables and subtracted
        from negative variables in `numeric_clause`.

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

        @param ncl: DIMACS clause ## TODO rename
VIGNET Pierre's avatar
VIGNET Pierre committed
627
628
        @warning: lock the unfolder
        """
629
630
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
VIGNET Pierre's avatar
VIGNET Pierre committed
631
632
633
634
635
636
637
638
639
640

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

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

VIGNET Pierre's avatar
VIGNET Pierre committed
642
    def __m_shift_clause(self, ncl, nb_steps):
643
644
645
646
647
648
649
        """Shift a clause for the given step number

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

650
651
652
        Called by: __shift_variant()


VIGNET Pierre's avatar
VIGNET Pierre committed
653
        @param ncl: DIMACS clause
654
        @param nb_steps: number of shifts asked
VIGNET Pierre's avatar
VIGNET Pierre committed
655
656
        @warning: lock the unfolder
        """
657
658
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
659

660
661
        return [(lit + self.__shift_step * nb_steps) if lit > 0
                else (lit - self.__shift_step * nb_steps) for lit in ncl]
662

VIGNET Pierre's avatar
VIGNET Pierre committed
663
    def __shift_dynamic(self):
664
665
666
667
        """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
668

669
670
        .. note:: Called by shift()
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
671
672
673
674
675
676
677
        # Old API
        # self.__dynamic_constraints.append(
        #   [self.__shift_clause(clause)
        #    for clause in self.__dynamic_constraints[-1]]
        # )

        # New API via C++ module
678
679
        # __dynamic_constraints:
        # List of lists of DIMACS encoded clauses (lists of ints)
VIGNET Pierre's avatar
VIGNET Pierre committed
680
681
        self.__dynamic_constraints.append(
            shift_dynamic(
682
                self.__dynamic_constraints[-1], # <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
683
684
685
                self.__shift_step
            )
        )
686

VIGNET Pierre's avatar
VIGNET Pierre committed
687
    def __shift_initial(self):
688
        """Shift initialisation condition
689

690
691
692
693
        .. note:: Called by:
            - shift()
            - init_backward_unfolding()
        """
694
        self.__initial_constraints = \
695
696
697
698
            shift_dynamic(
                self.__initial_constraints,
                self.__shift_step
            )
699

VIGNET Pierre's avatar
VIGNET Pierre committed
700
    def __shift_final(self):
701
        """Shift final property
702

703
704
705
706
        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
        """
707
        self.__final_constraints = \
708
709
710
711
            shift_dynamic(
                self.__final_constraints,
                self.__shift_step
            )
712

VIGNET Pierre's avatar
VIGNET Pierre committed
713
    def __shift_invariant(self):
714
715
716
717
718
719
        """Shift invariant property

        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
            - init_backward_unfolding()
VIGNET Pierre's avatar
VIGNET Pierre committed
720
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
721
        if self.__invariant_constraints:
VIGNET Pierre's avatar
VIGNET Pierre committed
722
723
724
725
726
727
728
            # New API via C++ module
            self.__invariant_constraints.append(
                shift_dynamic(
                    self.__invariant_constraints[-1],
                    self.__shift_step
                )
            )
729

VIGNET Pierre's avatar
VIGNET Pierre committed
730
    def __shift_variant(self):
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
        """Shift variant property - depends on unfolding direction

        ## TODO audit...

        .. 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()
750
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
751
752
753
        if not self.__list_variant_constraints:
            return
        if self.__shift_direction == "FORWARD":
754
755
            # Constraint t0 already included from the query during initialisation
            current_constraint = self.__list_variant_constraints[self.__current_step]
VIGNET Pierre's avatar
VIGNET Pierre committed
756
757
            # shift constraint at current step and add to var_constraints
            for clause in current_constraint:
758
                s_clause = self.__m_shift_clause(clause, self.__current_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
759
                self.__variant_constraints.append(s_clause)
760
761
                return # ?????
        elif self.__shift_direction == "BACKWARD":
VIGNET Pierre's avatar
VIGNET Pierre committed
762
763
            raise MCLException("Not yet implemented")
        else:
764
            raise MCLException("Shift incoherent data: " + self.__shift_direction)
765
766


VIGNET Pierre's avatar
VIGNET Pierre committed
767
    def shift(self):
768
769
770
771
772
773
774
775
776
777
        """Shift all clauses of one step

        self.__current_step is incremented here!

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

VIGNET Pierre's avatar
VIGNET Pierre committed
782
783
784
785
786
787
788
789
        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:
790
            # Shift direction must be set
791
            raise MCLException("Shift incoherent data: " + self.__shift_direction)
792
793

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

796
    ## Coding of properties ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
797
    def __compile_property(self, property_text):
798
799
800
801
802
803
804
805
806
807
808
        """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
809
810
        """
        if self.__locked:
VIGNET Pierre's avatar
VIGNET Pierre committed
811
812
            raise MCLException("Trying to compile property while unfolder is locked")

813
814
        # Syntax analyser and type checker
        # Compile a condition expression to a tree representation
VIGNET Pierre's avatar
VIGNET Pierre committed
815
        tree_prop = compile_cond(
816
817
818
819
820
            property_text,
            self.dynamic_system.symb_tab,
            self.dynamic_system.report
        )
        # Avoid name collisions of aux var
821
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
822
823
824
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
825

VIGNET Pierre's avatar
VIGNET Pierre committed
826
    def __compile_event(self, property_text):
827
828
829
830
831
832
833
834
835
        """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
836
837
        """
        if self.__locked:
838
839
840
            raise MCLException("Trying to compile property while unfolder is locked")

        # Syntax analyser and type checker
841
842
843
844
        # 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.
845
846
        tree_prop, ste, fcl = compile_event(
            property_text,
847
            self.dynamic_system.symb_tab,
848
            True, # Collect free clocks (events)
849
            self.dynamic_system.report
850
851
        )
        # Avoid name collisions of aux var
852
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
853
854
855
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
856

VIGNET Pierre's avatar
VIGNET Pierre committed
857
    def __init_initial_constraint_0(self, no_frontier_init=True):
858
859
860
861
862
863
864
865
        """Code initial constraints in a numerical clause.

        If initial property is set (in text format of logical formulas, or
        in dimacs format of numerical values), this function generates
        constraints clauses in numerical form.

        Initialisation of self.__initial_constraints:
        List of DIMACS clauses (lists of values).
866

867
868
869
870
871
872
873
874
875
876
        We have to wait until all variables are num coded before shifting anything!

        .. note:: Compilation of properties in text format (logical formulas)
            to numeric format is expensive when they must be parsed at each query.

        :key no_frontier_init: (optional) boolean to force all variables of
            places/entities to be disabled before each search.
            default: True
        :type no_frontier_init: <boolean>
        """
877
878
        self.__initial_constraints = list()

VIGNET Pierre's avatar
VIGNET Pierre committed
879
        if no_frontier_init:
880
881
            # Disable all variables of places (entities) in the model (except frontiers)
            self.__initial_constraints += self.__no_frontier_init
882

VIGNET Pierre's avatar
VIGNET Pierre committed
883
        if self.__initial_property:
884
885
886
887
888
889
            # Compile initial property from text logical formulas to numeric form
            # __initial_property: is taken from the current query
            # Costly...
            self.__initial_constraints += \
                [self.__code_clause(clause) for clause
                 in self.__compile_property(self.__initial_property)]
890

891
892
893
        if self.__dimacs_initial:
            # Add DIMACS aux clauses initial properties
            self.__initial_constraints += self.__dimacs_initial
894

VIGNET Pierre's avatar
VIGNET Pierre committed
895
    def __init_final_constraint_0(self):
896
897
898
899
900
901
902
903
904
905
906
907
908
        """Code final constraints in a numerical clause.

        If final property is set (in text format of logical formulas, or
        in dimacs format of numerical values), this function generates
        constraints clauses in numerical form.

        Initialisation of self.__final_constraints:
        List of DIMACS clauses (lists of values).

        We have to wait until all variables are num coded before shifting anything!

        .. note:: Compilation of properties in text format (logical formulas)
            to numeric format is expensive when they must be parsed at each query.
VIGNET Pierre's avatar
VIGNET Pierre committed
909
        """
910
        self.__final_constraints = list()
911

VIGNET Pierre's avatar
VIGNET Pierre committed
912
        if self.__final_property:
913
914
915
916
917
918
919
920
921
            # compile initial (X0) property into numeric form
            # Ex: [$Px$] => self.__final_constraints = [[7]]
            self.__final_constraints += \
                [self.__code_clause(clause) for clause
                 in self.__compile_property(self.__final_property)]

        if self.__dimacs_final:
            # Add DIMACS aux clauses initial properties
            self.__final_constraints += self.__dimacs_final
922

VIGNET Pierre's avatar
VIGNET Pierre committed
923
    def __init_invariant_constraint_0(self):
924
925
926
927
928
929
930
931
932
933
934
935
936
        """Code final constraints in a numerical clause.

        If trajectory property is set (in text format of logical formulas, or
        in dimacs format of numerical values), this function generates
        constraints clauses in numerical form.

        Initialisation of self.__invariant_constraints:
        List of lists of DIMACS clauses (lists of values).

        We have to wait until all variables are num coded before shifting anything!

        .. note:: Compilation of properties in text format (logical formulas)
            to numeric format is expensive when they must be parsed at each query.
VIGNET Pierre's avatar
VIGNET Pierre committed
937
        """
938
939
        self.__invariant_constraints = list()

VIGNET Pierre's avatar
VIGNET Pierre committed
940
        if self.__invariant_property:
941
942
943
944
945
946
947
948
949
950
            # compile initial (X0) property into numeric form
            self.__invariant_constraints.append(
                [self.__code_clause(clause) for clause
                 in self.__compile_property(self.__invariant_property)]
            )

        if self.__dimacs_invariant:
            # Add DIMACS aux clauses initial properties
            ## TODO: pas de append ? tester avec... => aucun changement, pas de test unitaire ici...
            self.__invariant_constraints += self.__dimacs_invariant
951

VIGNET Pierre's avatar
VIGNET Pierre committed
952
    def __init_variant_constraints_0(self):
953
954
955
956
957
958
        """Code variant constraints in a numerical clause.

        variant_property list d'étapes, chaque étape a une formule logique impliquant les évènements (et les places? pas sur.;)
        => ensemble de place/propriétés devant ^etre valides à chaque étape

        If variant_property is set, compile each property into clauses and
VIGNET Pierre's avatar
VIGNET Pierre committed
959
960
        encode these clauses. Clauses already in dimacs form are added.
        The two variant constraint forms must be compatible (same length)
961
962
963

        self.__list_variant_constraints is built here and is used later to shift
        given variant properties in __shift_variant().
VIGNET Pierre's avatar
VIGNET Pierre committed
964
965
        """
        # coding of variant properties
966
        # Take __variant_property in priority on __dimacs_variant
VIGNET Pierre's avatar
VIGNET Pierre committed
967
        if self.__variant_property:
968
969
            self.__list_variant_constraints = list()

VIGNET Pierre's avatar
VIGNET Pierre committed
970
            for prop in self.__variant_property:
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
                # compile initial (X0) property into numeric form
                # For each property in step of __variant_property
                self.__list_variant_constraints.append(
                    [self.__code_clause(clause)
                     for clause in self.__compile_event(prop)]
                )
                print(self.__list_variant_constraints)

            if self.__dimacs_variant:
                # Add DIMACS aux clauses initial properties
                # Check if the number of steps is equal
                if len(self.__variant_property) != len(self.__dimacs_variant):
                    raise MCLException(
                        "Incoherent variant properties; sizes of "
                        "__variant_property and __dimacs_variant differ"
                    )

                # Merge together all steps content
                # Ex:
                # __list_variant_constraints due to __variant_property convertion:
                # [[], [[4]], [], []]
                # __dimacs_variant:
                # [[], [[4]], [[6], [7]], []]
                # Result:
                # [[], [[4], [4]], [[6], [7]], []]
                self.__list_variant_constraints = \
                    [list(it.chain(*cpl)) for cpl
                     in zip(self.__dimacs_variant, self.__list_variant_constraints)]

        elif self.__dimacs_variant:
            # No __variant_property, keep only __dimacs_variant
            self.__list_variant_constraints = self.__dimacs_variant

        # Initialisation
VIGNET Pierre's avatar
VIGNET Pierre committed
1005
1006
        if self.__list_variant_constraints:
            if self.__shift_direction == "FORWARD":
1007
1008
                # For now, keep only the events of the first step (t0)
                # Other steps are taken during shift() calls
VIGNET Pierre's avatar
VIGNET Pierre committed
1009
1010
1011
1012
                self.__variant_constraints = self.__list_variant_constraints[0]
            elif  self.__shift_direction == "BACKWARD":
                raise MCLException("Not yet implemented")
            else:
1013
                raise MCLException("Shift incoherent data: " + self.__shift_direction)
1014