CLUnfolder.py 42.4 KB
Newer Older
VIGNET Pierre's avatar
VIGNET Pierre committed
1 2 3
## Filename    : CLUnfolder.py
## Author(s)   : Michel Le Borgne
## Created     : 22 mars 2012
4 5
## Revision    :
## Source      :
VIGNET Pierre's avatar
VIGNET Pierre committed
6 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
##
## 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
36 37
##     35042 RENNES Cedex, FRANCE
##
VIGNET Pierre's avatar
VIGNET Pierre committed
38 39 40 41 42 43
##
## Contributor(s): Geoffroy Andrieux IRSET
##
"""
Main engine for constraint unfolding and solving
"""
VIGNET Pierre's avatar
VIGNET Pierre committed
44 45
#from pyCryptoMS import CryptoMS
from pycryptosat import Solver as CryptoMS
46 47 48
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
49
from cadbiom import commons as cm
VIGNET Pierre's avatar
VIGNET Pierre committed
50 51 52 53 54 55

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

# Standard imports
56
from logging import DEBUG
VIGNET Pierre's avatar
VIGNET Pierre committed
57
import itertools as it
58 59

LOGGER = cm.logger()
VIGNET Pierre's avatar
VIGNET Pierre committed
60 61 62 63 64 65 66 67 68

class CLUnfolder(object):
    """
    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).
    During unfolding, clauses are shifted either to the future (forward) or
    to the past (backward). The shift operator is a simple addition
69 70
    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
71
    to add variables while generating a trajectory unfolding.
72 73

    Glossary
VIGNET Pierre's avatar
VIGNET Pierre committed
74 75 76
    ========
    - ground variables/ground dimacs code: variables at time 0/their encoding.
    - solution: a solution of the logical dynamic constraint from SAT solver
77
    - state vector: list of DIMACS code of original (not shifted) variables
VIGNET Pierre's avatar
VIGNET Pierre committed
78 79 80
      corresponding to a step.
    - trajectory: list of state_vectors
    """
81

VIGNET Pierre's avatar
VIGNET Pierre committed
82 83
    def __init__(self, sys):
        self.__dyn_sys = sys # symbolic clause dynamic system
84 85

        # shift_step equal to the total number of coded variables
VIGNET Pierre's avatar
VIGNET Pierre committed
86 87 88 89 90 91
        self.__shift_step_init = sys.get_var_number() # shift step of system
        self.__shift_step = self.__shift_step_init    #  current shift/step
        self.__locked = False
        self.__current_step = 1
        self.__steps_before_check = 0
        self.__include_aux_clauses = True
92

VIGNET Pierre's avatar
VIGNET Pierre committed
93 94
        # assign a DIMACS code number to each variable (invariant)
        self.__lit_cpt = self.__shift_step +1 # counter for aux. var. coding
95
        self.__var_code_table = dict()            # name -> DIMACS code
VIGNET Pierre's avatar
VIGNET Pierre committed
96 97 98 99 100 101 102
        self.__var_list = ['##']                  # DIMACS code -> name - != 0
        cpt = 1
        for svar in sys.base_var_set:
            self.__var_list.append(svar)
            self.__var_code_table[svar] = cpt
            cpt += 1
        assert(cpt == self.__shift_step + 1)
103

VIGNET Pierre's avatar
VIGNET Pierre committed
104
        # same tools for auxiliary variables from property compilation
105
        self.__aux_code_table = dict()            # name 2 code
VIGNET Pierre's avatar
VIGNET Pierre committed
106
        self.__aux_list = []                      # code to name
107 108

        # list  no_frontier place DIMACS codes
VIGNET Pierre's avatar
VIGNET Pierre committed
109 110 111
        self.__no_frontier_init = []
        for nfp in self.__dyn_sys.no_frontier:
            self.__no_frontier_init.append([- self.__var_code_table[nfp]])
112

VIGNET Pierre's avatar
VIGNET Pierre committed
113 114 115 116 117
        # ordered list of frontier place DIMACS codes for extraction (inv)
        self.__frontier = []
        for frp in self.__dyn_sys.frontier:
            self.__frontier.append(self.__var_code_table[frp])
        self.__frontier.sort()
118

VIGNET Pierre's avatar
VIGNET Pierre committed
119 120 121 122 123
        # ordered list of input places DIMACS code for extraction (inv)
        self.__inputs = []
        for inp in self.__dyn_sys.inputs:
            self.__inputs.append(self.__var_code_table[inp])
        self.__inputs.sort()
124

VIGNET Pierre's avatar
VIGNET Pierre committed
125 126 127 128 129
        # ordered list of free clocks DIMACS code for extraction (invariant)
        self.__free_clocks = []
        for fcl in self.__dyn_sys.free_clocks:
            self.__free_clocks.append(self.__var_code_table[fcl])
        self.__free_clocks.sort()
130

VIGNET Pierre's avatar
VIGNET Pierre committed
131 132 133 134
        # properties to be checked
        self.__initial_property = None            # string
        self.__dim_initial = None                 # list of dimacs clauses
        self.__final_property = None              # idem
135
        self.__dim_final = None
VIGNET Pierre's avatar
VIGNET Pierre committed
136 137 138 139 140 141
        self.__invariant_property = None          # idem
        self.__dim_invariant = None
        self.__variant_property = None            # list<logic formulas>
        self.__dim_variant = None                 # list<list<dimacs clauses>>
        # list of variant temporal constraints in Dimacs ground code
        self.__list_variant_constraints = None    # list<list<dimacs clauses>>
142 143

        # constraints - logical constraints
VIGNET Pierre's avatar
VIGNET Pierre committed
144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165
        # result from unfolding of base constraints
        self.__dynamic_constraints = []        # DIMACS clauses: X' = f(X,H,I)
        self.__initial_constraints = []        # DIMACS clauses: C(X_0)
        self.__final_constraints   = []        # idem: C(X_n)
        self.__invariant_constraints = []      # DIMACS clauses: C(X_i))
        self.__variant_constraints = []        # variant constraints along traj.
        self.__shift_direction = None          # forward or backward

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



    def reset(self):
        """
        Reset the unfolder before a new query
        """
        self.__initial_property = None
        self.__dim_initial = None
        self.__final_property = None
166
        self.__dim_final = None
VIGNET Pierre's avatar
VIGNET Pierre committed
167 168 169 170 171 172
        self.__invariant_property = None
        self.__dim_invariant = None
        self.__variant_property = None
        self.__dim_variant = None
        self.list_variant_constraints = None
        self.__steps_before_check = 0
173
        self.__shift_direction = None
VIGNET Pierre's avatar
VIGNET Pierre committed
174
        self.__locked = False
175

VIGNET Pierre's avatar
VIGNET Pierre committed
176 177 178 179 180 181 182
    def set_stats(self):
        """
        Enable solver statistics
        """
        self.__stats = True
        self.__nb_vars = 0
        self.__nb_clauses = 0
183

VIGNET Pierre's avatar
VIGNET Pierre committed
184 185 186 187 188
    def unset_stats(self):
        """
        disable solver statistics
        """
        self.__stats = False
189

VIGNET Pierre's avatar
VIGNET Pierre committed
190 191
    def _stats(self):
        """
192
        print solver statistics
VIGNET Pierre's avatar
VIGNET Pierre committed
193 194 195
        """
        print "\n NB Variables in solver: ", self.__nb_vars
        print "NB Clauses in solver: ", self.__nb_clauses
196

VIGNET Pierre's avatar
VIGNET Pierre committed
197 198 199 200 201
    def set_minimal_steps(self, nb_steps):
        """
        For reachability optimisation. number of shift before checking
        """
        self.__steps_before_check = nb_steps
202

VIGNET Pierre's avatar
VIGNET Pierre committed
203 204 205 206 207 208 209
    def set_include_aux_clauses(self, val):
        """
        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 = val
210

VIGNET Pierre's avatar
VIGNET Pierre committed
211 212 213 214 215 216
    # internal variable access for tests
    def get_dynamic_constraints(self):
        """
        For tests: returns coded dynamic constraints
        """
        return self.__dynamic_constraints
217

VIGNET Pierre's avatar
VIGNET Pierre committed
218 219 220 221 222
    def get_initial_constraints(self):
        """
        For tests: returns coded initial constraints
        """
        return self.__initial_constraints
223

VIGNET Pierre's avatar
VIGNET Pierre committed
224 225 226 227 228
    def get_invariant_constraints(self):
        """
        For tests: returns coded invariant constraints
        """
        return self.__invariant_constraints
229

VIGNET Pierre's avatar
VIGNET Pierre committed
230 231 232 233 234
    def get_variant_constraints(self):
        """
        For tests: returns coded variant constraints
        """
        return self.__variant_constraints
235

VIGNET Pierre's avatar
VIGNET Pierre committed
236 237 238 239 240
    def get_final_constraints(self):
        """
        For tests: returns coded final constraints
        """
        self.__final_constraints
241

VIGNET Pierre's avatar
VIGNET Pierre committed
242 243 244 245 246 247
    # variables management
    def var_dimacs_code(self, var_name):
        """
        returns dimacs code of (string) var_name variable
        """
        return self.__var_code_table[var_name]
248

VIGNET Pierre's avatar
VIGNET Pierre committed
249 250 251 252 253
    def get_system_var_number(self):
        """
        number of variables in the clause constraint dynamical system
        """
        return self.__dyn_sys.get_var_number()
254

VIGNET Pierre's avatar
VIGNET Pierre committed
255 256 257 258 259
    def get_var_number(self):
        """
        number of principal variables (properties excluded) in the unfolder
        """
        return len(self.__var_list) -1
260

VIGNET Pierre's avatar
VIGNET Pierre committed
261 262 263
    def get_var_name(self, var_num):
        """
        @param var_num: DIMACS literal coding of an initial variable
264
        @return: name of the variable
VIGNET Pierre's avatar
VIGNET Pierre committed
265
        """
266
        if var_num < 0:
VIGNET Pierre's avatar
VIGNET Pierre committed
267 268 269 270 271 272 273 274
            varnum1 = -var_num
        else: varnum1 = var_num
        var_code = (varnum1 - 1) % self.__shift_step + 1
        if var_code <= self.__shift_step_init: # variable from initial system
            return self.__var_list[var_code]
        else: # auxiliary variable introduced by properties compilation
            return self.__aux_list[var_code - self.__shift_step_init -1]
            #raise MCLException("Not a DIMACS code of an initial variable")
275

VIGNET Pierre's avatar
VIGNET Pierre committed
276 277 278 279 280
    def get_var_indexed_name(self, var_num):
        """
        @param var_num: DIMACS literal coding
        @return: name of the variable with time index
        """
281
        if var_num < 0:
VIGNET Pierre's avatar
VIGNET Pierre committed
282 283 284 285 286 287 288 289 290
            varnum1 = -var_num
        else: varnum1 = var_num
        var_code = (varnum1 - 1) % self.__shift_step + 1
        var_step = (varnum1 - var_code)/self.__shift_step
        if var_code <= self.__shift_step_init:
            return self.__var_list[var_code] + '_%s'% var_step
        else:
            index = var_code - self.__shift_step_init -1
            return self.__aux_list[index] + '_%s'% var_step
291

VIGNET Pierre's avatar
VIGNET Pierre committed
292 293
    def get_frontier(self):
        """
294
        @return: the DIMACS code of the frontier variables
VIGNET Pierre's avatar
VIGNET Pierre committed
295 296
        """
        return self.__frontier
297

VIGNET Pierre's avatar
VIGNET Pierre committed
298 299 300 301 302
    def get_free_clocks(self):
        """
        @return: the DIMACS code of the free_clocks variables
        """
        return self.__free_clocks
303

VIGNET Pierre's avatar
VIGNET Pierre committed
304 305 306 307 308
    def get_inputs(self):
        """
        @return: the DIMACS code of the input variables
        """
        return self.__inputs
309

VIGNET Pierre's avatar
VIGNET Pierre committed
310 311 312 313 314
    def get_shift_direction(self):
        """
        @return: string "FORWARD" or "BACKWARD"
        """
        return self.__shift_direction
315

VIGNET Pierre's avatar
VIGNET Pierre committed
316 317 318 319 320
    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
321

VIGNET Pierre's avatar
VIGNET Pierre committed
322 323 324 325 326
    def get_shift_step_init(self):
        """
        @return: the shift step ss (if n is X_0 code, n+ss is X_1 code)
        """
        return self.__shift_step_init
327

VIGNET Pierre's avatar
VIGNET Pierre committed
328 329 330 331 332 333
    def get_current_step(self):
        """
        @return: the current number of unfolding
        """
        return self.__current_step

334 335


VIGNET Pierre's avatar
VIGNET Pierre committed
336 337 338 339 340 341 342 343 344 345
    # translation from names to num codes
    # the translation depends on the shift direction
    def __forward_code(self, clause):
        """
        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 integer coding increases in futur steps
        @param clause: a Clause object
        @return: the DIMACS coding of the forward shifted clause
        """
346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366

        # Old API
        # num_clause = []
        # for lit in clause.list_of_literals:
        #     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
        #print(forward_code(clause, self.__var_code_table, self.__shift_step))
        return forward_code(clause, self.__var_code_table, self.__shift_step)

367

VIGNET Pierre's avatar
VIGNET Pierre committed
368 369 370 371 372 373 374 375 376 377
    def __backward_code(self, clause):
        """
        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
        @param clause: a Clause object
        @return: the DIMACS coding of the backward shifted clause
        """
        num_clause = []
        for lit in clause.list_of_literals:
378 379 380 381
            if not lit.name[-1] == '`': # t 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
382
            else:  # t+1 variable
383 384 385
                num_clause.append(-self.__var_code_table[lit.name[:-1]] \
                if not lit.sign \
                else self.__var_code_table[lit.name[:-1]])
VIGNET Pierre's avatar
VIGNET Pierre committed
386
        return num_clause
387

VIGNET Pierre's avatar
VIGNET Pierre committed
388 389
    def __code_clause(self, clause):
        """
390 391 392
        numerically code a clause with the numeric code found in
        self.__var_code_table for variables in the dynamic system and
        self.__aux_code_table for other variables assume all variables
VIGNET Pierre's avatar
VIGNET Pierre committed
393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413
        are basic variables (t=0)
        @warning: MODIFIES SHIFT_STEP if auxiliary variables are present (numeric code)
        """
        num_clause = []
        for lit in clause.list_of_literals:
            name = lit.name
            if self.__var_code_table.has_key(name):
                var_cod = self.__var_code_table[name]
            elif self.__aux_code_table.has_key(name):
                var_cod = self.__aux_code_table[name]
            else: # create an auxiliary variable - modifies shift_step
                self.__shift_step += 1
                self.__aux_code_table[name] = self.__shift_step
                var_cod = self.__shift_step
                self.__aux_list.append(name)
            if lit.sign:
                lit_code = var_cod
            else:
                lit_code = - var_cod
            num_clause.append(lit_code)
        return num_clause
414

VIGNET Pierre's avatar
VIGNET Pierre committed
415 416 417 418 419
    # dynamics initialisations
    def __forward_init_dynamic(self):
        """
        set dynamic constraints for a forward one step: X1 = f(X0)
        """
420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435

        # Old API
        # self.__dynamic_constraints = []

        # num_clause_list = \
        #     [self.__forward_code(clause)
        #      for clause in self.__dyn_sys.list_clauses]
        #
        # if self.__include_aux_clauses:
        #     num_clause_list += \
        #         [self.__forward_code(clause)
        #          for clause in self.__dyn_sys.aux_list_clauses]
        #
        # self.__dynamic_constraints.append(num_clause_list)

        # New API via C++ module
436
        # TODO: take a look at __backward_init_dynamic & __backward_code
VIGNET Pierre's avatar
VIGNET Pierre committed
437
        if self.__include_aux_clauses:
438 439 440 441 442 443 444 445 446 447
            self.__dynamic_constraints = \
                forward_init_dynamic(self.__dyn_sys.list_clauses,
                                     self.__var_code_table,
                                     self.__shift_step,
                                     self.__dyn_sys.aux_list_clauses)
        else:
            self.__dynamic_constraints = \
                forward_init_dynamic(self.__dyn_sys.list_clauses,
                                     self.__var_code_table,
                                     self.__shift_step)
448

VIGNET Pierre's avatar
VIGNET Pierre committed
449 450 451 452 453
    def __backward_init_dynamic(self):
        """
        set dynamic constraints for a forward one step: X0 = f(X1)
        """
        self.__dynamic_constraints = []
454 455 456 457 458

        num_clause_list = \
            [self.__backward_code(clause)
             for clause in self.__dyn_sys.list_clauses]

VIGNET Pierre's avatar
VIGNET Pierre committed
459
        if self.__include_aux_clauses:
460 461 462 463
            num_clause_list += \
                [self.__backward_code(clause)
                 for clause in self.__dyn_sys.aux_list_clauses]

VIGNET Pierre's avatar
VIGNET Pierre committed
464
        self.__dynamic_constraints.append(num_clause_list)
465

VIGNET Pierre's avatar
VIGNET Pierre committed
466 467 468 469 470 471 472
    # shifting: implementation of the shift operator
    def __shift_clause(self, ncl):
        """
        shift a clause one step
        @param ncl: DIMACS clause
        @warning: lock the unfolder
        """
473
        self.__locked = True  # shift_step must be frozen
VIGNET Pierre's avatar
VIGNET Pierre committed
474 475 476 477 478 479 480 481 482 483

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

VIGNET Pierre's avatar
VIGNET Pierre committed
485 486 487 488
    def __m_shift_clause(self, ncl, nb_steps):
        """
        shift a clause many step
        @param ncl: DIMACS clause
489
        @param nb_steps: number of shifts
VIGNET Pierre's avatar
VIGNET Pierre committed
490 491
        @warning: lock the unfolder
        """
492 493
        self.__locked = True  # shift_step must be frozen

494 495
        return [(lit + self.__shift_step * nb_steps) if lit > 0
                else (lit - self.__shift_step * nb_steps) for lit in ncl]
496

VIGNET Pierre's avatar
VIGNET Pierre committed
497 498 499
    def __shift_dynamic(self):
        """
        Shift clauses representing the dynamics X' = f(X,I,C)
500
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
501 502 503 504 505 506 507 508 509 510 511 512 513 514

        # Old API
        # self.__dynamic_constraints.append(
        #   [self.__shift_clause(clause)
        #    for clause in self.__dynamic_constraints[-1]]
        # )

        # New API via C++ module
        self.__dynamic_constraints.append(
            shift_dynamic(
                self.__dynamic_constraints[-1],
                self.__shift_step
            )
        )
515

VIGNET Pierre's avatar
VIGNET Pierre committed
516 517 518 519
    def __shift_initial(self):
        """
        Shift initialisation condition
        """
520 521 522 523

        self.__initial_constraints = \
            [self.__shift_clause(clause)
             for clause in self.__initial_constraints]
524

VIGNET Pierre's avatar
VIGNET Pierre committed
525 526 527 528
    def __shift_final(self):
        """
        Shift final property
        """
529 530 531 532 533

        self.__final_constraints = \
            [self.__shift_clause(clause)
             for clause in self.__final_constraints]

534

VIGNET Pierre's avatar
VIGNET Pierre committed
535 536 537 538 539
    def __shift_invariant(self):
        """
        Shift invariant property
        """
        if not self.__invariant_constraints == []:
VIGNET Pierre's avatar
VIGNET Pierre committed
540 541 542 543 544 545 546 547 548 549 550 551 552 553

            # Old API
            # self.__invariant_constraints.append(
            #     [self.__shift_clause(clause)
            #      for clause in self.__invariant_constraints[-1]]
            # )

            # New API via C++ module
            self.__invariant_constraints.append(
                shift_dynamic(
                    self.__invariant_constraints[-1],
                    self.__shift_step
                )
            )
554

VIGNET Pierre's avatar
VIGNET Pierre committed
555 556 557
    def __shift_variant(self):
        """
        shift variant property - depends on unfolding direction
558
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
559 560 561 562 563 564 565 566 567 568 569 570 571 572
        if not self.__list_variant_constraints:
            return
        if self.__shift_direction == "FORWARD":
            index = self.__current_step # constraint t0 already included
            current_constraint = self.__list_variant_constraints[index]
            # shift constraint at current step and add to var_constraints
            for clause in current_constraint:
                s_clause = self.__m_shift_clause(clause, index)
                self.__variant_constraints.append(s_clause)
                return
        elif self.__shift_direction == 'BACKWARD':
            raise MCLException("Not yet implemented")
        else:
            raise MCLException("Shift incoherent data: "+self.__shift_direction)
573 574


VIGNET Pierre's avatar
VIGNET Pierre committed
575 576 577 578 579 580 581 582 583 584 585 586 587 588
    def shift(self):
        """
        assume shift direction is set - shift one step
        """
        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:
            raise MCLException("Shift incoherent data: "+self.__shift_direction)
        self.__current_step += 1
589

VIGNET Pierre's avatar
VIGNET Pierre committed
590 591 592 593 594 595 596 597 598
    # coding of properties
    def __compile_property(self, property_text):
        """
        compile a property (logical formula) into clauses
        type checking uses the symbol table of dyn_sys
        error reporting through the dyn_sys reporter
        MODIFIES __lit_cpt for numbering of auxiliary variables (not coding)
        """
        if self.__locked:
VIGNET Pierre's avatar
VIGNET Pierre committed
599 600
            raise MCLException("Trying to compile property while unfolder is locked")

VIGNET Pierre's avatar
VIGNET Pierre committed
601
        # syntax analyser and type checker
VIGNET Pierre's avatar
VIGNET Pierre committed
602 603 604 605
        # property_text, symb_t, reporter
        tree_prop = compile_cond(property_text,
                                 self.__dyn_sys.symb_tab,
                                 self.__dyn_sys.report)
606 607
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
608 609 610
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
611

VIGNET Pierre's avatar
VIGNET Pierre committed
612
        # coding of properties
613

VIGNET Pierre's avatar
VIGNET Pierre committed
614 615 616 617 618 619 620 621 622 623 624 625 626 627 628
    def __compile_event(self, property_text):
        """
        compile an event (biosignal expression) into clauses
        type checking uses the symbol table of dyn_sys
        error reporting through the dyn_sys reporter
        MODIFIES __lit_cpt for numbering of auxiliary variables (not coding)
        """
        if self.__locked:
            mess = "Trying to compile property while unfolder is locked"
            raise MCLException(mess)
        reporter = self.__dyn_sys.report
        symb_t = self.__dyn_sys.symb_tab
        # syntax analyser and type checker
        (tree_prop, ste, fcl) = compile_event(property_text, symb_t,
                                              True,  reporter)
629 630
        # avoid name collisions of aux var
        prop_visitor = CLPropertyVisitor(self.__lit_cpt)
VIGNET Pierre's avatar
VIGNET Pierre committed
631 632 633
        tree_prop.accept(prop_visitor)
        self.__lit_cpt = prop_visitor.cpt # avoid name collisions of aux var
        return prop_visitor.clauses
634

VIGNET Pierre's avatar
VIGNET Pierre committed
635 636
    def set_initial_property(self, property_text):
        """
637
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
638 639
        """
        self.__initial_property = property_text
640

VIGNET Pierre's avatar
VIGNET Pierre committed
641 642 643
    def set_dim_initial_property(self, dimacs_clause_list):
        """
        set initial property with a DIMACS representation
644
        @param dimacs_clause_list:
VIGNET Pierre's avatar
VIGNET Pierre committed
645 646
        """
        self.__dim_initial = dimacs_clause_list
647

VIGNET Pierre's avatar
VIGNET Pierre committed
648 649 650 651 652 653
    def __init_initial_constraint_0(self, no_frontier_init=True):
        """
        if initial property is set, generate constraints clauses in numeric form
        base variable form - we have to wait until all variables are num coded
        before shifting anything!!
        """
654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673
# OLD
#        self.__initial_constraints = []
#        if no_frontier_init:
#            # initialize no frontier places to False
#            for nfp in self.__no_frontier_init:
#                self.__initial_constraints.append(nfp)
#        if self.__initial_property:
#            # compile initial property
#            l_clauses = self.__compile_property(self.__initial_property)
#            # compile numeric form
#            for clause in l_clauses:
#                self.__initial_constraints.append(self.__code_clause(clause))
#        # dimacs aux initial properties
#        dim_init = self.__dim_initial
#        if dim_init:
#            self.__initial_constraints = self.__initial_constraints + dim_init

        self.__initial_constraints = list()

        # initialize no frontier places to False
VIGNET Pierre's avatar
VIGNET Pierre committed
674
        if no_frontier_init:
675 676
            self.__initial_constraints += [elem for elem in self.__no_frontier_init]

VIGNET Pierre's avatar
VIGNET Pierre committed
677 678 679
        if self.__initial_property:
            # compile initial property
            # compile numeric form
680 681
            self.__initial_constraints += [self.__code_clause(clause) for clause in self.__compile_property(self.__initial_property)]

VIGNET Pierre's avatar
VIGNET Pierre committed
682
        # dimacs aux initial properties
683 684
        if self.__dim_initial:
            self.__initial_constraints += self.__dim_initial
685

VIGNET Pierre's avatar
VIGNET Pierre committed
686 687
    def set_final_property(self, property_text):
        """
688
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
689 690
        """
        self.__final_property = property_text
691

VIGNET Pierre's avatar
VIGNET Pierre committed
692 693 694
    def set_dim_final_property(self, dimacs_clause_list):
        """
        set final property with a DIMACS representation
695 696
        @param dimacs_clause_list:
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
697
        self.__dim_final = dimacs_clause_list
698

VIGNET Pierre's avatar
VIGNET Pierre committed
699 700 701 702 703 704
    def __init_final_constraint_0(self):
        """
        if final property is set, generate constraints clauses in numeric form
        base variable used - we have to wait until all variables are num coded
        before shifting anything!!
        """
705

VIGNET Pierre's avatar
VIGNET Pierre committed
706 707 708 709 710 711 712 713 714 715
        self.__final_constraints = []
        if self.__final_property:
            # compile initial (X0) property
            l_clauses = self.__compile_property(self.__final_property)
            # compile numeric form
            for clause in l_clauses:
                self.__final_constraints.append(self.__code_clause(clause))
        dim_fin = self.__dim_final
        if dim_fin:
            self.__final_constraints = self.__final_constraints + dim_fin
716

VIGNET Pierre's avatar
VIGNET Pierre committed
717 718
    def set_current_property(self, property_text):
        """
719
        @param property_text: string - litteral boolean expression
VIGNET Pierre's avatar
VIGNET Pierre committed
720
        """
721

VIGNET Pierre's avatar
VIGNET Pierre committed
722
        self.__invariant_property = property_text
723

VIGNET Pierre's avatar
VIGNET Pierre committed
724 725 726 727 728
    def set_dim_current_property(self, dimacs_clause_list):
        """
        set final property with a DIMACS representation
        @param dimacs_clause_list:
        """
729

VIGNET Pierre's avatar
VIGNET Pierre committed
730
        self.__dim_invariant = dimacs_clause_list
731

VIGNET Pierre's avatar
VIGNET Pierre committed
732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749
    def __init_invariant_constraint_0(self):
        """
        if trajectory property is set, generate constraints clauses in numeric form
        base variable used - we have to wait until all variables are num coded
        before shifting anything!!
        """
        self.__invariant_constraints = []
        if self.__invariant_property:
            # compile initial (X0) property
            l_clauses = self.__compile_property(self.__invariant_property)
            # compile numeric form
            init_const = []
            for clause in l_clauses:
                init_const.append(self.__code_clause(clause))
            self.__invariant_constraints.append(init_const)
        d_inv = self.__dim_invariant
        if d_inv:
            self.__invariant_constraints = self.__invariant_constraints + d_inv
750

VIGNET Pierre's avatar
VIGNET Pierre committed
751 752 753 754 755 756 757
    def set_variant_property(self, var_prop):
        """
        @param var_prop: a list of logical formulas representing time varying
        constraints. Each constraint uses ground (not shifted) variables.
        The order of the list of constraints is always time increasing.
        """
        self.__variant_property = var_prop
758

VIGNET Pierre's avatar
VIGNET Pierre committed
759 760
    def set_dim_variant_property(self, dim_var_prop):
        """
761 762
        @param dim_var_prop: a list list of dimacs clauses representing time
        varying constraints. Each constraint uses ground (not shifted)
VIGNET Pierre's avatar
VIGNET Pierre committed
763 764 765
        variable codes.
        """
        self.__dim_variant = dim_var_prop
766

VIGNET Pierre's avatar
VIGNET Pierre committed
767 768
    def __init_variant_constraints_0(self):
        """
769
        if variant_property is set, compile each property into clauses and
VIGNET Pierre's avatar
VIGNET Pierre committed
770 771 772 773 774 775 776 777 778 779 780 781 782 783
        encode these clauses. Clauses already in dimacs form are added.
        The two variant constraint forms must be compatible (same length)
        """
        # coding of variant properties
        if self.__variant_property:
            self.__list_variant_constraints = []
            for prop in self.__variant_property:
                # compile initial (X0) property
                l_clauses = self.__compile_event(prop)
                # encode the clauses
                dim_cl = []
                for clause in l_clauses:
                    dim_cl.append(self.__code_clause(clause))
                self.__list_variant_constraints.append(dim_cl)
784

VIGNET Pierre's avatar
VIGNET Pierre committed
785 786
            # add variant properties in dimacs form
            if self.__dim_variant:
787
                vp_length = len(self.__variant_property)
VIGNET Pierre's avatar
VIGNET Pierre committed
788 789 790
                if vp_length != len(self.__dim_variant):
                    mess = "Incoherent variant properties"
                    raise MCLException(mess)
791

VIGNET Pierre's avatar
VIGNET Pierre committed
792 793 794
                for i in range(vp_length):
                    c_var = self.__list_variant_constraints[i]
                    c_var = c_var + self.__dim_variant[i]
795
                    self.__list_variant_constraints[i] = c_var
VIGNET Pierre's avatar
VIGNET Pierre committed
796 797 798 799 800 801 802 803 804 805 806 807
        else:
            if self.__dim_variant:
                self.__list_variant_constraints = self.__dim_variant
        # initialisation
        if self.__list_variant_constraints:
            if self.__shift_direction == "FORWARD":
                self.__variant_constraints = self.__list_variant_constraints[0]
            elif  self.__shift_direction == "BACKWARD":
                raise MCLException("Not yet implemented")
            else:
                raise MCLException("Shift incoherent data: "
                                   + self.__shift_direction)
808

VIGNET Pierre's avatar
VIGNET Pierre committed
809 810 811 812 813 814 815 816 817 818
    # whole initialisations
    def init_forward_unfolding(self):
        """
        initialisation before generating constraints - forward trajectory
        """
        self.__shift_direction = 'FORWARD'
        self.__current_step = 1
        self.__shift_step = self.__shift_step_init  # back to basic!
        self.__aux_code_table = dict()              # flush auxiliary variables
        self.__aux_list = []                        # idem
819

VIGNET Pierre's avatar
VIGNET Pierre committed
820 821 822 823 824
        # init properties to generate all variable num codes
        self.__init_initial_constraint_0()
        self.__init_final_constraint_0()
        self.__init_invariant_constraint_0()
        self.__init_variant_constraints_0()
825

VIGNET Pierre's avatar
VIGNET Pierre committed
826 827 828 829
        # now shifting is possible
        self.__forward_init_dynamic()
        self.__shift_final()
        self.__shift_invariant()
830 831


VIGNET Pierre's avatar
VIGNET Pierre committed
832 833 834 835 836 837 838 839 840
    def init_backward_unfolding(self):
        """
        initialisation before generating constraints - backward trajectory
        """
        self.__shift_direction = 'BACKWARD'
        self.__current_step = 0
        self.__shift_step = self.__shift_step_init  # back to basic!
        self.__aux_code_table = dict()              # flush auxiliary variables
        self.__aux_list = []                        # idem
841

VIGNET Pierre's avatar
VIGNET Pierre committed
842 843 844 845 846
        # init properties to generate all variable num codes
        self.__init_initial_constraint_0()
        self.__init_final_constraint_0()
        self.__init_invariant_constraint_0()
        self.__init_variant_constraints_0()
847

VIGNET Pierre's avatar
VIGNET Pierre committed
848 849 850 851
        # now shifting is possible
        self.__backward_init_dynamic()
        self.__shift_initial()
        self.__shift_invariant()
852

VIGNET Pierre's avatar
VIGNET Pierre committed
853 854 855 856 857 858 859 860 861 862 863 864 865 866 867
    # for debug
    def vars_in_clause(self, clause):
        """
        DEBUG
        """
        lvar = []
        for var in clause:
            lvar.append(self.get_var_indexed_name(var))
        return lvar


    # solver interface
    def __load_solver(self, solv):
        """
        add all the current clauses in solver solv
868
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884

        # New API via C++ module
        solv.add_clauses(self.__final_constraints)
        solv.add_clauses(it.chain(*self.__invariant_constraints))
        solv.add_clauses(self.__variant_constraints)
        solv.add_clauses(it.chain(*self.__dynamic_constraints))
        solv.add_clauses(self.__initial_constraints)

        # Less efficient alternative
        # solv.add_clauses([clause for lcl in self.__invariant_constraints
        #                   for clause in lcl])
        # solv.add_clauses([clause for lcl in self.__dynamic_constraints
        #                   for clause in lcl])

        # Old API
        # Clauses are added one by one
VIGNET Pierre's avatar
VIGNET Pierre committed
885
        # final
VIGNET Pierre's avatar
VIGNET Pierre committed
886
        #[solv.add_clause(clause) for clause in self.__final_constraints]
887

VIGNET Pierre's avatar
VIGNET Pierre committed
888
        # trajectory invariant
VIGNET Pierre's avatar
VIGNET Pierre committed
889 890
        #[solv.add_clause(clause) for lcl in self.__invariant_constraints
        # for clause in lcl]
891

VIGNET Pierre's avatar
VIGNET Pierre committed
892
        # trajectory variant
VIGNET Pierre's avatar
VIGNET Pierre committed
893
        #[solv.add_clause(clause) for clause in self.__variant_constraints]
894

VIGNET Pierre's avatar
VIGNET Pierre committed
895
        # dynamics
VIGNET Pierre's avatar
VIGNET Pierre committed
896 897
        #[solv.add_clause(clause) for lcl in self.__dynamic_constraints
        # for clause in lcl]
898

899
        # initial
VIGNET Pierre's avatar
VIGNET Pierre committed
900
        #[solv.add_clause(clause) for clause in self.__initial_constraints]
VIGNET Pierre's avatar
VIGNET Pierre committed
901

902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923
        # LOGGING
        if LOGGER.getEffectiveLevel() == DEBUG:
            # final
            LOGGER.debug("Load new solver !!")
            LOGGER.debug(">> final: " + str(len(self.__final_constraints)))
            LOGGER.debug(str(self.__final_constraints))

            # trajectory invariant
            LOGGER.debug(">> trajectory inv: " + str(len(self.__invariant_constraints)))
            LOGGER.debug(str(self.__invariant_constraints))

            # trajectory variant
            LOGGER.debug(">> trajectory var: " + str(len(self.__variant_constraints)))
            LOGGER.debug(str(self.__variant_constraints))

            # dynamics
            LOGGER.debug(">> dynamics: " + str(len(self.__dynamic_constraints)))
            LOGGER.debug(str(self.__dynamic_constraints))

            # initial
            LOGGER.debug(">> initial: " + str(len(self.__initial_constraints)))
            LOGGER.debug(str(self.__initial_constraints))
924 925


VIGNET Pierre's avatar
VIGNET Pierre committed
926 927 928 929
    def __constraints_satisfied(self):
        """
        @return: boolean
        """
930
        LOGGER.debug("__constraints_satisfied ?")
VIGNET Pierre's avatar
VIGNET Pierre committed
931
        solver = CryptoMS()
932
        # Load Solver and all clauses
VIGNET Pierre's avatar
VIGNET Pierre committed
933
        self.__load_solver(solver)
934 935
        # If stats are activated (never besides in test environment):
        # sync local data (nb vars, nb clauses with solver state)
VIGNET Pierre's avatar
VIGNET Pierre committed
936
        if self.__stats:
937
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
938 939 940
                self.__nb_vars = solver.nb_vars()
            if solver.nb_clauses() > self.__nb_clauses:
                self.__nb_clauses = solver.nb_clauses()
941
        # Is problem satisfiable ?
VIGNET Pierre's avatar
VIGNET Pierre committed
942
        return solver.is_satisfiable()
943

944

VIGNET Pierre's avatar
VIGNET Pierre committed
945 946 947 948 949 950 951 952
    def __msolve_constraints(self, max_sol, vvars):
        """
        @param max_sol: int - the max number of solution returned
        @param vvars: variables for which the solver must find different solutions(dimacs code)
        @return: a list of RawSolution
        """
        solver = CryptoMS()
        self.__load_solver(solver)
953

VIGNET Pierre's avatar
VIGNET Pierre committed
954
        if self.__stats:
955
            if solver.nb_vars() > self.__nb_vars:
VIGNET Pierre's avatar
VIGNET Pierre committed
956
                self.__nb_vars = solver.nb_vars()
957
            if solver.nb_clauses() > self.__nb_clauses:
VIGNET Pierre's avatar
VIGNET Pierre committed
958
                self.__nb_clauses = solver.nb_clauses()
959

960
        if LOGGER.getEffectiveLevel() == DEBUG:
961 962 963
            LOGGER.debug("__msolve_constraints :: vvars : " + str(vvars))
            LOGGER.debug("__msolve_constraints :: max_sol : " + str(max_sol))
            lintsol = solver.msolve_selected(max_sol, vvars)
964
            LOGGER.debug("__msolve_constraints :: lintsol : " + str(lintsol))
965
            return [RawSolution(solint, self) for solint in lintsol]
966

967 968
        return [RawSolution(solint, self)
                for solint in solver.msolve_selected(max_sol, vvars)]
VIGNET Pierre's avatar
VIGNET Pierre committed
969 970 971 972 973

    # dynamic properties
    def squery_is_satisfied(self, max_step):
        """
        Ask the SAT solver
974
        @param max_step: int - the horizon
VIGNET Pierre's avatar
VIGNET Pierre committed
975 976 977 978 979 980 981
        """
        # initialization
        self.init_forward_unfolding()
        # horizon adjustment
        if self.__list_variant_constraints:
            max_step = min(max_step, len(self.__list_variant_constraints)-1)
        # loop
982
        if self.__invariant_property and not self.__final_property :
VIGNET Pierre's avatar
VIGNET Pierre committed
983 984
            while self.__current_step <= max_step:
                self.shift()
985
            return self.__constraints_satisfied()
VIGNET Pierre's avatar
VIGNET Pierre committed
986 987 988 989 990
        else :
            while self.__current_step <= max_step:
                if self.__constraints_satisfied():
                    return True
                self.shift()
991 992 993 994
            return self.__constraints_satisfied()



VIGNET Pierre's avatar
VIGNET Pierre committed
995 996 997 998 999 1000
    def squery_solve(self, vvars, max_step, max_sol):
        """
        Assert a query is loaded (start_condition, inv_condition, final_condition)
        @param vvars: variables on which different solutions must differ
        @param max_step: bounded horizon for computations
        @param max_sol: max number of solutions to be computed
1001 1002

        @return: list of RawSolution objects
VIGNET Pierre's avatar
VIGNET Pierre committed
1003
        """
1004 1005
        if LOGGER.getEffectiveLevel() == DEBUG:
            LOGGER.debug("squery_solve :: vvars : " + str(vvars))
VIGNET Pierre's avatar
VIGNET Pierre committed
1006 1007 1008 1009 1010 1011 1012 1013 1014
        # initialization
        self.init_forward_unfolding()
        # horizon adjustment
        if self.__list_variant_constraints:
            max_step = min(max_step, len(self.__list_variant_constraints)-1)
        # loop
        if self.__invariant_property and not self.__final_property :
            while self.__current_step <= max_step:
                self.shift()
VIGNET Pierre's avatar
VIGNET Pierre committed
1015 1016 1017
            # return l_rawsol
            return self.__msolve_constraints(max_sol, vvars)

VIGNET Pierre's avatar
VIGNET Pierre committed
1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032
        else : # reachability
            l_rawsol = []
            # check and correct for incoherent data on step number
            if self.__steps_before_check > max_step:
                self.__steps_before_check = max_step - 1
            # shift without checking (optimization)
            while self.__current_step <= self.__steps_before_check:
                self.shift()
            # search for solutions at each step
            while self.__current_step <= max_step:
                lsol = self.__msolve_constraints(max_sol, vvars)
                if len(lsol)>0:
                    l_rawsol = l_rawsol + lsol
                self.shift()
            return l_rawsol
1033

VIGNET Pierre's avatar
VIGNET Pierre committed
1034 1035 1036 1037 1038 1039

###############################################################################
class CLPropertyVisitor(object):
    """
    SigExpression on states and events into a set of clauses
    Type checking must be done.
1040 1041
    """

VIGNET Pierre's avatar
VIGNET Pierre committed
1042 1043 1044 1045
    def __init__(self, aux_cpt=0):
        self.cpt = aux_cpt         # for auxiliary variable naming
        self.clauses = []          # generated clauses
        self.top = True            # root of the formula?
1046

VIGNET Pierre's avatar
VIGNET Pierre committed
1047 1048 1049 1050 1051 1052 1053 1054 1055 1056
    def visit_sig_ident(self, tnode):
        """
        ident -> literal
        """
        name = tnode.name
        new_lit = Literal(name, True)
        if self.top:
            self.clauses.append(Clause([new_lit]))
            return None
        return new_lit
1057

VIGNET Pierre's avatar
VIGNET Pierre committed
1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070
    def visit_sig_not(self, node):
        """
        translate a not
        """
        top = self.top
        self.top = False
        # compile operand to nl <=> formula
        newl = node.operand.accept(self)
        notnl = newl.lit_not()
        if top: # we are at the root
            self.clauses.append(Clause([notnl]))
            return None
        return notnl # if we are not at the root
1071

VIGNET Pierre's avatar
VIGNET Pierre committed
1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088