CLUnfolder.py 64 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
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
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
"""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

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
    system.


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


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()
            ...


VIGNET Pierre's avatar
VIGNET Pierre committed
114
"""
115
116
from __future__ import print_function

VIGNET Pierre's avatar
VIGNET Pierre committed
117
118
#from pyCryptoMS import CryptoMS
from pycryptosat import Solver as CryptoMS
119
120
121
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
122
from cadbiom import commons as cm
VIGNET Pierre's avatar
VIGNET Pierre committed
123
124
125
126
127
128

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

# Standard imports
129
from logging import DEBUG
VIGNET Pierre's avatar
VIGNET Pierre committed
130
import itertools as it
131
132

LOGGER = cm.logger()
VIGNET Pierre's avatar
VIGNET Pierre committed
133
134
135

class CLUnfolder(object):
    """
136
137
138
139
140
141
142
143
144
    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
145
146
147
148
    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
149

VIGNET Pierre's avatar
VIGNET Pierre committed
150
151
    During unfolding, clauses are shifted either to the future (forward) or
    to the past (backward). The shift operator is a simple addition
152
153
    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
154
    to add variables while generating a trajectory unfolding.
155
156

    Glossary
VIGNET Pierre's avatar
VIGNET Pierre committed
157
158
159
    ========
    - ground variables/ground dimacs code: variables at time 0/their encoding.
    - solution: a solution of the logical dynamic constraint from SAT solver
160
    - state vector: list of DIMACS code of original (not shifted) variables
VIGNET Pierre's avatar
VIGNET Pierre committed
161
162
163
      corresponding to a step.
    - trajectory: list of state_vectors
    """
164

165
166
167
168
169
    def __init__(self, dynamic_system):
        """
        :param dynamic_system: Describe a dynamic system in clause form.
        :type dynamic_system: <CLDynSys>
        """
170
        self.dynamic_system = dynamic_system # symbolic clause dynamic system
171

172
173
        # shift_step equals to the total number of coded variables
        # (including inputs, entities, clocks/events, auxiliary variables)
174
        # shift_step_init: the shift step ss (if n is X_0 code, n+ss is X_1 code)
175
176
177
178
179
180
181
182
        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
183
        self.__locked = False
184
185
186
        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
187
        self.__steps_before_check = 0
188

VIGNET Pierre's avatar
VIGNET Pierre committed
189
        # assign a DIMACS code number to each variable (invariant)
190
191
        # 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
192
        # (including inputs, entities, clocks/events, auxiliary variables).
193
194
        self.__var_code_table = dict()     # Mapping: name -> DIMACS code (!= 0)
        self.__var_list = ['##']           # Mapping: DIMACS code (!= 0) -> name
195
196

        # Fix order of variables names with a list:
197
198
        # - indexes of __var_list are the values of the variables at these indexes
        # - values begin from 1 (0 is a blacklisted value)
199
200
        base_var_set = list(dynamic_system.base_var_set)
        self.__var_list += base_var_set
201
        # keys: are the names of the variables, values: their values
202
203
204
205
206
207
208
209
210
211
212
213
214
        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)
215

216
        assert len(self.__var_code_table) == 2 * self.__shift_step
217

218
219
220
221
222
        # 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
223

224
225
226
227
        # 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
228
        self.__aux_list = []                      # code to name
229

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

234
        # ordered list of DIMACS codes of the frontier variables/places
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
        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)
256
257
258
259
        self.frontiers_pos_and_neg = \
            self.frontiers_negative_values | frozenset(self.frontier_values)

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

262
        # DIMACS codes of the free_clocks variables/places for extraction (invariant)
263
        self.__free_clocks = frozenset(self.__var_code_table[fcl] for fcl in self.dynamic_system.free_clocks)
264
265

        # Binding for a merged version of __inputs and __free_clocks
266
        # Convenient attribute for RawSolution.extract_act_input_clock_seq()
267
268
        # DIMACS codes of the input and free_clocks variables
        self.inputs_and_free_clocks = self.__inputs | self.__free_clocks
269

270
271
        # Properties to be checked
        self.reset()
272

273
        # Logical constraints:
274
        # Result from unfolding of base constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
275
276
277
278
279
        # 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
280
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
VIGNET Pierre's avatar
VIGNET Pierre committed
281

282
        # Simple temporal properties:
VIGNET Pierre's avatar
VIGNET Pierre committed
283
284
        # SP(X0): Initial property/start property; Never change at each step.
        # IP(X): Invariant property
285
        # VP(X): Variant property
VIGNET Pierre's avatar
VIGNET Pierre committed
286
        #   List of logical formulas of properties forced at each step
287
        #   It's the trajectory of events of a solution.
VIGNET Pierre's avatar
VIGNET Pierre committed
288
289
        # FP(X): Final property

290
        self.__initial_constraints = []        # DIMACS clauses: C(X_0) <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
291
292
        self.__final_constraints   = []        # idem: C(X_n)
        self.__invariant_constraints = []      # DIMACS clauses: C(X_i))
293
        self.__variant_constraints = []        # variant constraints along trajectory
294
        self.__shift_direction = None          # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
295
296
297
298
299
300
301
302

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


    def reset(self):
303
304
        """Reset the unfolder before a new query

305
306
307
        Reset only properties and dimacs clauses from the current query;
        AND __list_variant_constraints.

308
        This function is called from the constructor and during
309
310
        MCLAnalyser.sq_is_satisfiable() and MCLAnalyser.sq_solutions()
        following the call of init_with_query().
VIGNET Pierre's avatar
VIGNET Pierre committed
311
        """
312
        # Properties to be checked
313
        self.__initial_property = None            # logical formula - literal boolean expression
314
        self.__dimacs_initial = None              # list of DIMACS clauses
315
        self.__final_property = None              # logical formula
316
        self.__dimacs_final = None                # list of DIMACS clauses
317
        self.__invariant_property = None          # logical formula
318
        self.__dimacs_invariant = None            # list of DIMACS clauses
319
        self.__variant_property = None            # list<logic formulas>
320
        self.__dimacs_variant = None              # list<list<DIMACS clauses>>
321
        # list of variant temporal constraints in Dimacs ground code
322
        self.__list_variant_constraints = None    # list<list<DIMACS clauses>>
323

324
325
        # If this function is called from the constructor,
        # the following variables are just redefined here.
326
327
328

        # For reachability optimisation. Number of shifts before checking
        # the final property
VIGNET Pierre's avatar
VIGNET Pierre committed
329
        self.__steps_before_check = 0
330
        self.__shift_direction = None             # FORWARD or BACKWARD
VIGNET Pierre's avatar
VIGNET Pierre committed
331
        self.__locked = False
332

333
334
335
    def init_with_query(self, query):
        """Initialise the unfolder with the given query

336
        Following attributes are used from the query:
337
            start_prop, dim_start, inv_prop, dim_inv, final_prop, dim_final,
338
            variant_prop, dim_variant_prop, steps_before_check
339
340

        Textual properties of query are compiled into numeric clauses in
341
342
        init_forward_unfolding(), just at the beginning of squery_is_satisfied()
        and squery_solve().
343
        This compilation step is costly due to ANTLR performances...
344
345
346

        .. warning:: ALL textual properties are susceptible to add new auxiliary
            variables in the system (increase shift_step).
347
348
349
        """
        # Reset the unfolder before a new query
        self.reset()
350
        # Init with query properties and clauses
351
352
        self.__initial_property = query.start_prop # logical formula in text
        self.__dimacs_initial = query.dim_start
353

354
355
        self.__final_property = query.final_prop # logical formula in text
        self.__dimacs_final = query.dim_final
356

357
358
        self.__invariant_property = query.inv_prop # logical formula in text
        self.__dimacs_invariant = query.dim_inv
359
360

        # It's the trajectory of events of a solution.
361
362
        self.__variant_property = query.variant_prop # logical formula in text
        self.__dimacs_variant = query.dim_variant_prop
363

364
365
366
        # For reachability optimisation. Number of shifts before checking
        # the final property (default 0)
        self.__steps_before_check = query.steps_before_check
367

VIGNET Pierre's avatar
VIGNET Pierre committed
368
    def set_stats(self):
369
        """Enable solver statistics (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
370
371
372
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
373

VIGNET Pierre's avatar
VIGNET Pierre committed
374
    def unset_stats(self):
375
        """Disable solver statistics (never used)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
376
        self.__stats = False
377

VIGNET Pierre's avatar
VIGNET Pierre committed
378
    def _stats(self):
379
380
381
        """Display solver statistics"""
        print("\n NB Variables in solver:", self.__nb_vars)
        print("NB Clauses in solver:", self.__nb_clauses)
382

VIGNET Pierre's avatar
VIGNET Pierre committed
383
384
385
    def set_include_aux_clauses(self, val):
        """
        Include auxiliary clause to eliminate undesirable solutions
386
        If A->B has clock h, an aux constraint added is h included in h when A
VIGNET Pierre's avatar
VIGNET Pierre committed
387
388
389
        Must be set to False for inhibitors computations
        """
        self.__include_aux_clauses = val
390

391
    ## Internal variable access for tests (never used) #########################
392
393
    @property
    def dynamic_constraints(self):
394
        """For tests: returns coded dynamic constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
395
        return self.__dynamic_constraints
396

397
398
    @property
    def initial_constraints(self):
399
        """For tests: returns coded initial constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
400
        return self.__initial_constraints
401

402
403
    @property
    def invariant_constraints(self):
404
        """For tests: returns coded invariant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
405
        return self.__invariant_constraints
406

407
408
    @property
    def variant_constraints(self):
409
        """For tests: returns coded variant constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
410
        return self.__variant_constraints
411

412
413
    @property
    def final_constraints(self):
414
        """For tests: returns coded final constraints"""
VIGNET Pierre's avatar
VIGNET Pierre committed
415
        self.__final_constraints
416

417
    ## Variables management ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
418
419
    def var_names_in_clause(self, clause):
        """Return the names of the variables from values in the given numeric clause
420
421
422
423
        (DEBUG never used)
        """
        return [self.get_var_indexed_name(var) for var in clause]

VIGNET Pierre's avatar
VIGNET Pierre committed
424
    def var_dimacs_code(self, var_name):
425
        """Returns DIMACS code of var_name (string) variable (for tests)"""
VIGNET Pierre's avatar
VIGNET Pierre committed
426
        return self.__var_code_table[var_name]
427

VIGNET Pierre's avatar
VIGNET Pierre committed
428
    def get_system_var_number(self):
429
430
        """Get number of variables in the clause constraint dynamical system
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
431
432
433

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

VIGNET Pierre's avatar
VIGNET Pierre committed
437
    def get_var_number(self):
438
439
        """Get number of principal variables (properties excluded) in the unfolder
        (including inputs, entities, clocks/events, auxiliary variables) (for tests)
440
441
442

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

VIGNET Pierre's avatar
VIGNET Pierre committed
447
    def get_var_name(self, var_num):
448
449
450
451
        """Get name of the variable

        .. seealso:: Explanations on get_var_indexed_name()

VIGNET Pierre's avatar
VIGNET Pierre committed
452
        @param var_num: DIMACS literal coding of an initial variable
453
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
454
        """
455
        # Get the original var_code without shifts
456
        var_code = (abs(var_num) - 1) % self.__shift_step + 1
457
        if var_code <= self.shift_step_init:
458
459
            # 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
460
            return self.__var_list[var_code]
461
462
463
        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
464
            #raise MCLException("Not a DIMACS code of an initial variable")
465

VIGNET Pierre's avatar
VIGNET Pierre committed
466
    def get_var_indexed_name(self, var_num):
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
        """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
489
        @param var_num: DIMACS literal coding
490
        @return: name of the variable with the time index appended
VIGNET Pierre's avatar
VIGNET Pierre committed
491
        """
492
        varnum1 = abs(var_num)
493
        # Get the original var_code without shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
494
        var_code = (varnum1 - 1) % self.__shift_step + 1
495
        var_step = (varnum1 - var_code) / self.__shift_step
496
        if var_code <= self.shift_step_init:
497
498
            # 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
499
500
            return self.__var_list[var_code] + '_%s'% var_step
        else:
501
502
            # Auxiliary variable introduced by properties compilation
            index = var_code - self.shift_step_init - 1
VIGNET Pierre's avatar
VIGNET Pierre committed
503
            return self.__aux_list[index] + '_%s'% var_step
504

VIGNET Pierre's avatar
VIGNET Pierre committed
505
    def get_free_clocks(self):
506
        """Get the DIMACS codes of the free_clocks variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
507
        return self.__free_clocks
508

VIGNET Pierre's avatar
VIGNET Pierre committed
509
    def get_inputs(self):
510
        """Get the DIMACS codes of the input variables"""
VIGNET Pierre's avatar
VIGNET Pierre committed
511
        return self.__inputs
512

VIGNET Pierre's avatar
VIGNET Pierre committed
513
514
515
516
517
    def get_shift_direction(self):
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
518

VIGNET Pierre's avatar
VIGNET Pierre committed
519
520
521
522
523
    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
524

VIGNET Pierre's avatar
VIGNET Pierre committed
525
526
527
528
529
530
    def get_current_step(self):
        """
        @return: the current number of unfolding
        """
        return self.__current_step

531

532
    ## Translation from names to num codes #####################################
VIGNET Pierre's avatar
VIGNET Pierre committed
533
    ## The translation depends on the shift direction
VIGNET Pierre's avatar
VIGNET Pierre committed
534
    def __forward_code(self, clause):
535
536
537
538
539
540
541
542
543
        """(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
544
545
546
        @param clause: a Clause object
        @return: the DIMACS coding of the forward shifted clause
        """
547
548
        # Old API
        # num_clause = []
549
        # for lit in clause.literals:
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
        #     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)

566

VIGNET Pierre's avatar
VIGNET Pierre committed
567
    def __backward_code(self, clause):
568
569
570
571
572
573
        """(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
574
575
576
577
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
578
579
580
581
582
583
584
585
586
587
588
589
590
        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
591
        return num_clause
592

VIGNET Pierre's avatar
VIGNET Pierre committed
593
    def __code_clause(self, clause):
594
595
596
597
598
599
600
        """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
601
        @warning: MODIFIES SHIFT_STEP if auxiliary variables are present (numeric code)
602
603
604
605
606
607
608
            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
609
610
        """
        num_clause = []
611
        for lit in clause.literals:
612
            # Get variable value with the given name
VIGNET Pierre's avatar
VIGNET Pierre committed
613
            name = lit.name
614
            if name in self.__var_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
615
                var_cod = self.__var_code_table[name]
616
            elif name in self.__aux_code_table:
VIGNET Pierre's avatar
VIGNET Pierre committed
617
                var_cod = self.__aux_code_table[name]
618
619
            else:
                # Create an auxiliary variable - modifies shift_step (nb of variables)
VIGNET Pierre's avatar
VIGNET Pierre committed
620
                self.__shift_step += 1
621
                # Mapping name to value code
VIGNET Pierre's avatar
VIGNET Pierre committed
622
                self.__aux_code_table[name] = self.__shift_step
623
                # Mapping value code to name
VIGNET Pierre's avatar
VIGNET Pierre committed
624
                self.__aux_list.append(name)
625
626
627
628
629
                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
630
631
            num_clause.append(lit_code)
        return num_clause
632

633
    ## Dynamic initialisations #################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
634
    def __forward_init_dynamic(self):
635
636
        """Dynamics initialisations.
        Set dynamic constraints for a forward one step: X1 = f(X0)
637

VIGNET Pierre's avatar
VIGNET Pierre committed
638
        Numerically code clauses with the numeric codes found in
639
640
        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
641
642
643
644
645
        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.
646
647

        .. note:: Called by init_forward_unfolding()
648

649
650
651
652
        .. note:: Future variables x' are noted "name`" in Literal names.

        .. note:: Values of variables increases of __shift_step in future steps.
        """
653
        # New API via C++ module
654
        # TODO: take a look at __backward_init_dynamic & __backward_code
VIGNET Pierre's avatar
VIGNET Pierre committed
655
        if self.__include_aux_clauses:
656
            # Auxiliary clauses are supported (default)
657
            self.__dynamic_constraints = \
658
                forward_init_dynamic(self.dynamic_system.list_clauses,
659
660
                                     self.__var_code_table,
                                     self.__shift_step,
661
                                     self.dynamic_system.aux_list_clauses)
662
663
        else:
            self.__dynamic_constraints = \
664
                forward_init_dynamic(self.dynamic_system.list_clauses,
665
666
                                     self.__var_code_table,
                                     self.__shift_step)
667

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

672
673
        .. note:: Called by init_backward_unfolding()
        """
674
675
        num_clause_list = \
            [self.__backward_code(clause)
676
             for clause in self.dynamic_system.list_clauses]
677

VIGNET Pierre's avatar
VIGNET Pierre committed
678
        if self.__include_aux_clauses:
679
680
            num_clause_list += \
                [self.__backward_code(clause)
681
                 for clause in self.dynamic_system.aux_list_clauses]
682

683
        self.__dynamic_constraints = [num_clause_list]
684

685
    ## Shifting variables: implementation of the shift operator ################
VIGNET Pierre's avatar
VIGNET Pierre committed
686
    def __shift_clause(self, ncl):
687
688
        """Shift a clause for the current __shift_step

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

691
692
693
        Basically, `shift_step` is added to positive variables and subtracted
        from negative variables in `numeric_clause`.

694
695
696
697
698
699
        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
700
701
        @warning: lock the unfolder
        """
702
703
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
VIGNET Pierre's avatar
VIGNET Pierre committed
704
705
706
707
708
709
710
711
712
713

        # 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)
714

VIGNET Pierre's avatar
VIGNET Pierre committed
715
    def __m_shift_clause(self, ncl, nb_steps):
716
717
718
719
720
721
722
        """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.

723
724
725
        Called by: __shift_variant()


VIGNET Pierre's avatar
VIGNET Pierre committed
726
        @param ncl: DIMACS clause
727
        @param nb_steps: number of shifts asked
VIGNET Pierre's avatar
VIGNET Pierre committed
728
729
        @warning: lock the unfolder
        """
730
731
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True
732

733
734
        return [(lit + self.__shift_step * nb_steps) if lit > 0
                else (lit - self.__shift_step * nb_steps) for lit in ncl]
735

VIGNET Pierre's avatar
VIGNET Pierre committed
736
    def __shift_dynamic(self):
737
738
739
740
        """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
741

742
743
        .. note:: Called by shift()
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
744
745
746
747
748
749
750
        # Old API
        # self.__dynamic_constraints.append(
        #   [self.__shift_clause(clause)
        #    for clause in self.__dynamic_constraints[-1]]
        # )

        # New API via C++ module
751
752
        # __dynamic_constraints:
        # List of lists of DIMACS encoded clauses (lists of ints)
VIGNET Pierre's avatar
VIGNET Pierre committed
753
754
        self.__dynamic_constraints.append(
            shift_dynamic(
755
                self.__dynamic_constraints[-1], # <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
756
757
758
                self.__shift_step
            )
        )
759

VIGNET Pierre's avatar
VIGNET Pierre committed
760
    def __shift_initial(self):
761
        """Shift initialisation condition
762

763
764
        Shift + replace __initial_constraints

765
766
767
768
        .. note:: Called by:
            - shift()
            - init_backward_unfolding()
        """
769
        self.__initial_constraints = \
770
771
772
773
            shift_dynamic(
                self.__initial_constraints,
                self.__shift_step
            )
774

VIGNET Pierre's avatar
VIGNET Pierre committed
775
    def __shift_final(self):
776
        """Shift final property
777

778
779
        Shift + replace __final_constraints

780
781
782
783
        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
        """
784
        self.__final_constraints = \
785
786
787
788
            shift_dynamic(
                self.__final_constraints,
                self.__shift_step
            )
789

VIGNET Pierre's avatar
VIGNET Pierre committed
790
    def __shift_invariant(self):
791
792
        """Shift invariant property

793
794
        Shift + append of the last element of __invariant_constraints

795
796
797
798
        .. note:: Called by:
            - shift()
            - init_forward_unfolding()
            - init_backward_unfolding()
VIGNET Pierre's avatar
VIGNET Pierre committed
799
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
800
        if self.__invariant_constraints:
VIGNET Pierre's avatar
VIGNET Pierre committed
801
802
803
804
805
806
807
            # New API via C++ module
            self.__invariant_constraints.append(
                shift_dynamic(
                    self.__invariant_constraints[-1],
                    self.__shift_step
                )
            )
808

VIGNET Pierre's avatar
VIGNET Pierre committed
809
    def __shift_variant(self):
810
811
        """Shift variant property - depends on unfolding direction

812
813
        Shift clauses of the current step in __list_variant_constraints, and
        append them to __variant_constraints.
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829

        .. 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()
830
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
831
832
833
        if not self.__list_variant_constraints:
            return
        if self.__shift_direction == "FORWARD":
834
835
            # Constraint t0 already included from the query during initialisation
            current_constraint = self.__list_variant_constraints[self.__current_step]
836
            # Shift constraints at current step and append them to __variant_constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
837
            for clause in current_constraint:
838
                s_clause = self.__m_shift_clause(clause, self.__current_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
839
                self.__variant_constraints.append(s_clause)
840
841
                return # ?????
        elif self.__shift_direction == "BACKWARD":
VIGNET Pierre's avatar
VIGNET Pierre committed
842
843
            raise MCLException("Not yet implemented")
        else:
844
            raise MCLException("Shift incoherent data: " + self.__shift_direction)
845
846


VIGNET Pierre's avatar
VIGNET Pierre committed
847
    def shift(self):
848
        """Shift all clauses of the system to prepare it for the next step.
849
850
851

        self.__current_step is incremented here!

852
        Modified attributes:
853
            - __dynamic_constraints[-1] (last element)
854
                Shift + append of the last element of __dynamic_constraints
855
            - __invariant_constraints[-1] (last element)
856
857
858
859
                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.
860
861
            - __final_constraints if __shift_direction is "FORWARD"
            - __initial_constraints if __shift_direction is "BACKWARD"
862
863
864
865

        Called at each step by:
            - squery_solve()
            - squery_is_satisfied()
VIGNET Pierre's avatar
VIGNET Pierre committed
866
        """
867
868
869
        # Froze unfolder to avoid modifications of shift_step
        self.__locked = True

VIGNET Pierre's avatar
VIGNET Pierre committed
870
871
872
873
874
875
876
877
        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:
878
            # Shift direction must be set
879
            raise MCLException("Shift incoherent data: " + self.__shift_direction)
880
881

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

884
    ## Coding of properties ####################################################
VIGNET Pierre's avatar
VIGNET Pierre committed
885
    def __compile_property(self, property_text):
886
887
888
889
890
891
892
893
894
895
896
        """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
897
898
        """
        if self.__locked:
VIGNET Pierre's avatar
VIGNET Pierre committed
899
900
            raise MCLException("Trying to compile property while unfolder is locked")

901
902
        # Syntax analyser and type checker
        # Compile a condition expression to a tree representation
VIGNET Pierre's avatar
VIGNET Pierre committed
903
        tree_prop = compile_cond(
904
905
906
907
908
            property_text,
            self.dynamic_system.symb_tab,
            self.dynamic_system.report
        )
        # Avoid name collisions of aux var
909
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
910
911
912
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
913

VIGNET Pierre's avatar
VIGNET Pierre committed
914
    def __compile_event(self, property_text):
915
916
917
918
919
920
921
922
923
        """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
924
925
        """
        if self.__locked:
926
927
928
            raise MCLException("Trying to compile property while unfolder is locked")

        # Syntax analyser and type checker
929
930
931
932
        # 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.
933
934
        tree_prop, ste, fcl = compile_event(
            property_text,
935
            self.dynamic_system.symb_tab,
936
            True, # Collect free clocks (events)
937
            self.dynamic_system.report
938
939
        )
        # Avoid name collisions of aux var
940
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
941
942
943
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
944

VIGNET Pierre's avatar
VIGNET Pierre committed
945
    def __init_initial_constraint_0(self, no_frontier_init=True):
946
947
948
949
950
951
952
953
        """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).
954

955
956
957
        self.__initial_constraints is filled with the current query data AND
        with a clause with ALL places that are not frontiers (negative values).

958
959
960
961
962
963
        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
964
965
            places/entities that are not frontiers to be disabled before each
            search.
966
967
968
            default: True
        :type no_frontier_init: <boolean>
        """
969
970
        self.__initial_constraints = list()

VIGNET Pierre's avatar
VIGNET Pierre committed
971
        if no_frontier_init:
972
973
            # Disable all variables of places (entities) in the model (except frontiers)
            self.__initial_constraints += self.__no_frontier_init
974

VIGNET Pierre's avatar
VIGNET Pierre committed
975
        if self.__initial_property:
976
977
978
979
980
981
            # 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)]
982

983
984
985
        if self.__dimacs_initial:
            # Add DIMACS aux clauses initial properties
            self.__initial_constraints += self.__dimacs_initial
986

VIGNET Pierre's avatar
VIGNET Pierre committed
987
    def __init_final_constraint_0(self):
988
989
990
991
992
993
994
995
996
997
998
999
1000
        """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
1001
        """
1002
        self.__final_constraints = list()
1003

VIGNET Pierre's avatar
VIGNET Pierre committed
1004
        if self.__final_property:
1005
1006
1007
1008
1009
1010
1011
1012
1013
            # 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
1014

VIGNET Pierre's avatar
VIGNET Pierre committed
1015
    def __init_invariant_constraint_0(self):