MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

MCLSolutions.py 31 KB
Newer Older
1
# -*- coding: utf-8 -*-
VIGNET Pierre's avatar
VIGNET Pierre committed
2
3
4
## Filename    : MCLSolutions.py
## Author(s)   : Michel Le Borgne
## Created     : 03/9/2012
VIGNET Pierre's avatar
VIGNET Pierre committed
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
VIGNET Pierre's avatar
VIGNET Pierre committed
37
38
##     35042 RENNES Cedex, FRANCE
##
VIGNET Pierre's avatar
VIGNET Pierre committed
39
40
41
##
## Contributor(s): Geoffroy Andrieux - IRISA/IRSET
##
42
43
44
45
46
47
48
49
50
51
52
53
54
"""Classes used to store solver answers.

RawSolution:
    Contain a solution got from SAT solver with all variable parameters
    from the unfolder.

DimacsFrontierSol:
    A numerical representation of *frontier values and timings* from a raw solution.

FrontierSolution:
    Provides is a wrapper for a symbolic
    representation (human readable) of activated frontiers defined in
    RawSolution and DimacsFrontierSol objects.
VIGNET Pierre's avatar
VIGNET Pierre committed
55
"""
56
57
58
# Standard imports
from __future__ import print_function
import itertools as it
59
60
#from functools import cached_property
from cached_property import cached_property
61
62

from cadbiom import commons as cm
VIGNET Pierre's avatar
VIGNET Pierre committed
63

VIGNET Pierre's avatar
VIGNET Pierre committed
64
65
66
# C++ API
from _cadbiom import get_unshift_code, unflatten

67
68
69
LOGGER = cm.logger()


VIGNET Pierre's avatar
VIGNET Pierre committed
70
class MCLException(Exception):
VIGNET Pierre's avatar
VIGNET Pierre committed
71
    """Exception for MCLAnalyser"""
VIGNET Pierre's avatar
VIGNET Pierre committed
72
73
    def __init__(self, mess):
        self.message = mess
VIGNET Pierre's avatar
VIGNET Pierre committed
74

VIGNET Pierre's avatar
VIGNET Pierre committed
75
76
77
    def __str__(self):
        return self.message

78
79
################################################################################

VIGNET Pierre's avatar
VIGNET Pierre committed
80
class RawSolution(object):
81
82
83
84
85
86
87
88
89
    """RawSolution objects contain a solution got from SAT solver with all
    variable parameters from the unfolder.

    The class RawSolution provides a representation of solutions which are
    raw results from the SAT solver with all variable parameters from the
    unfolder, and consequently not easily readable.

    In addition to the solution in DIMACS form (including values for auxiliary
    variables), a RawSolution object registers data which permit information
90
    extraction from these raw solutions. The most important methods/attributes are:
91

92
        - frontier_pos_and_neg_values:
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
            Extracts the frontier values from the solution.
            These values are in DIMACS code.

        - extract_activated_frontier_values():
            Extracts frontier variables which are active in solution.

        - extract_act_input_clock_seq():
            Extract the sequence of activated inputs and events in the solution.

    ..warning:: IMPORTANT: the solution MUST correspond to the properties registered
        for its computation. Any change in these properties will give incorrect
        results (current_step, etc.).

    Attributes:
        :param shift_direction: Unfolding direction
        :param shift_step: The shift step ss (if n is X_0 code, n+ss is X_1 code) (?)
            Dependant on the run.
        :param solution: DIMACS encoding of **a solution** from the solver
            A solution is list of state vectors (tuple of literals).
            Each literal is a variable.
            ..note:: The solver returns list of solutions.
        :param unfolder: Get the current unfolder for the solution
            (unfolder is used for invariant constants)
        :param current_step: Get current step of the unfolder
            (Thus the current number of steps related to the current solution and
            by extension the maximum of steps until now)
        :type shift_direction: "FORWARD" or "BACKWARD"
        :type shift_step: <int>
        :type solution: <tuple <int>>
        :type unfolder: <CLUnfolder>
        :type current_step: <int>
VIGNET Pierre's avatar
VIGNET Pierre committed
124
    """
125
    def __init__(self, solution, unfolder):
VIGNET Pierre's avatar
VIGNET Pierre committed
126
        """
127
128
129
130
131
132
        :param solution: DIMACS encoding of **a solution** from the solver
            (tuple of literals)
        :param unfolder: Current unfolder for the solution
            (unfolder is used for invariant constants)
        :type solution: <tuple <int>>
        :type unfolder: <CLUnfolder>
VIGNET Pierre's avatar
VIGNET Pierre committed
133
        """
134
135
136
137
138
        self.solution = solution
        self.unfolder = unfolder
        self.shift_step = unfolder.get_shift_step()
        self.current_step = unfolder.get_current_step()
        self.shift_direction = unfolder.get_shift_direction()
VIGNET Pierre's avatar
VIGNET Pierre committed
139

VIGNET Pierre's avatar
VIGNET Pierre committed
140
    def get_unshift_code(self, var_num):
141
142
143
144
        """Get the real value of the given variable in the system (remove the shift)

        ..warning:: DEPRECATED Used internally by self.unflatten()

VIGNET Pierre's avatar
VIGNET Pierre committed
145
146
        @param var_num: DIMACS literal coding of a shifted variable x_i
        @return: DIMACS literal coding of  x_0 with same value
147
        :return: <int>
VIGNET Pierre's avatar
VIGNET Pierre committed
148
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
149
        # Old API
150
        # var_code = (abs(var_num) - 1) % self.shift_step + 1
VIGNET Pierre's avatar
VIGNET Pierre committed
151
        #
152
        # if var_code <= self.shift_step:
VIGNET Pierre's avatar
VIGNET Pierre committed
153
        #     return var_code * (-1 if var_num < 0 else 1)
154
155
        #
        # raise MCLException("Not a DIMACS code of an initial variable")
156

VIGNET Pierre's avatar
VIGNET Pierre committed
157
        # New API via C++ module
158
        get_unshift_code(var_num, self.shift_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
159

VIGNET Pierre's avatar
VIGNET Pierre committed
160
    def get_var_name(self, var_num):
161
162
        """For translation to symbolic representation
        Return the name of a variable with its value.
VIGNET Pierre's avatar
VIGNET Pierre committed
163
        """
164
        return self.unfolder.get_var_name(var_num)
VIGNET Pierre's avatar
VIGNET Pierre committed
165

166
167
    def unflatten(self):
        """Extract trajectories from the current solution
VIGNET Pierre's avatar
VIGNET Pierre committed
168

169
170
171
172
        Transform a flat DIMACS representation of a trajectory into a
        <list <list <int>>>.
        Each sublist represents a state vector (the state of all variables of
        the system for 1 step in the trajectory).
VIGNET Pierre's avatar
VIGNET Pierre committed
173

174
175
176
        ..note:: This assertion seems to be not true:
            Auxiliary variables introduced by properties compiling are ignored.
            => there are lots of variables on the format "_name"...
VIGNET Pierre's avatar
VIGNET Pierre committed
177

178
        ..note:: Debug with:
VIGNET Pierre's avatar
VIGNET Pierre committed
179

180
181
182
183
184
185
186
187
            >>> raw_sol = RawSolution()
            >>> print(raw_sol)

        ..note:: The list returns all variables of the system including
            inputs, clocks, auxiliary variables.

        :return: A list of state vectors (<list <int>>) in DIMACS format
        :rtype: <list <list <int>>>
VIGNET Pierre's avatar
VIGNET Pierre committed
188
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
189
190
191
192
193

        # Old API
        # lv_traj = []
        # step = 0
        # dec = 0
194
        # shift_step_init = self.unfolder.shift_step_init
VIGNET Pierre's avatar
VIGNET Pierre committed
195
        # # n steps means h0, ..., h(n-1) in constraints for clocks and inputs
196
197
        # while dec + self.shift_step < len(self.solution):
        #     #assert [self.get_unshift_code(self.solution[i+dec]) for i in range(shift_step_init)] == [get_unshift_code(self.solution[i+dec], self.shift_step) for i in range(shift_step_init)]
VIGNET Pierre's avatar
VIGNET Pierre committed
198
        #     lv_traj.append(
199
200
        #         [get_unshift_code(self.solution[i+dec], self.shift_step)
        #          for i in range(shift_step_init)]
VIGNET Pierre's avatar
VIGNET Pierre committed
201
202
        #     )
        #     step += 1
203
        #     dec = step * self.shift_step # first index of time step
VIGNET Pierre's avatar
VIGNET Pierre committed
204
205
206
207
        # return lv_traj # list of lists

        # New API via C++ module
        return unflatten(
208
209
210
            self.solution,
            self.unfolder.shift_step_init,
            self.shift_step
VIGNET Pierre's avatar
VIGNET Pierre committed
211
212
        )

213
    def extract_activated_frontier_values(self):
214
215
216
217
218
        """Extracts frontier variables which are active in solution.

        :return: Set of activated frontier values.
        :rtype: <set>
        """
219
        if self.shift_direction == 'FORWARD':
220
221
            # frontier_values: Set of frontier positive values only.
            return frozenset(self.unfolder.frontier_values) & self.frontier_pos_and_neg_values
222
223
        else:
            NotImplementedError("BACKWARD shift direction is not yet implemented")
VIGNET Pierre's avatar
VIGNET Pierre committed
224

225
226
    @cached_property
    def frontier_pos_and_neg_values(self):
227
228
229
        """Extracts the frontier values from the solution.
        These values are in DIMACS code.

230
231
        .. warning:: This function returns values of active AND inactive frontiers.

VIGNET Pierre's avatar
VIGNET Pierre committed
232
        .. warning:: Assert: solution is sorted by variable code for BACKWARD
233

234
235
236
237
238
239
        .. note:: This function makes set operations between all values of
            frontiers and the current solution.
            This last one is a list of hundreds of thousands items
            (ex: ~500000 for a solution with 10 steps).
            Thus, the operation is costly and we use a decorator @cached_property
            to put the result in cache.
VIGNET Pierre's avatar
VIGNET Pierre committed
240

VIGNET Pierre's avatar
VIGNET Pierre committed
241
242
243
244
        .. note:: Used by:
            - self.extract_activated_frontier_values()
            - DimacsFrontierSol.__init__()

245
246
247
248
249
        .. note::
            frontiers (fixed size): 3824
            solution (increasing size): 171231, 228314, 285405, 285453, 400091 etc.

        @param sol: a dimacs solution
VIGNET Pierre's avatar
VIGNET Pierre committed
250
251
        @return: a dimacs code list of the activation state on the frontier for sol
        """
252
        # Old API
253
        # jmax = len(self.unfolder.frontier_values)
254
255
        # fsol = []
        # j = 0
256
257
        # dec = self.shift_step * self.current_step
        # sol = self.solution
258
259
        # for i in range(len(sol)):
        #     # the variable is frontier var:
260
261
        #     if abs(sol[i]) == self.unfolder.frontier_values[j]:
        #         if self.shift_direction == "FORWARD":
262
263
264
265
266
267
268
269
        #             fsol.append(sol[i])
        #         else:
        #             fsol.append(sol[i+dec])     # look for initial values
        #         j += 1
        #         if j == jmax:
        #             return fsol
        # return fsol # never reach this point

270
        # Old API v2
271
        # frontiers = self.unfolder.frontier_values
272
273
274
        # jmax = len(frontiers)
        # fsol = list()
        # j = 0
275
276
        # dec = self.shift_step * self.current_step
        # for i, sol in enumerate(self.solution):
277
278
        #    # the variable is frontier var:
        #    if abs(sol) == frontiers[j]:
279
        #        if self.shift_direction == "FORWARD":
280
281
        #            fsol.append(sol)
        #        else:
282
        #            fsol.append(self.solution[i+dec])# look for initial values
283
284
285
286
287
        #        j += 1
        #        if j == jmax:
        #            return fsol
        #return fsol # never reach this point

288
        if self.shift_direction == 'FORWARD':
289
            # frontiers_pos_and_neg:
290
291
292
            # All frontiers and their opposite version Union
            # Set of frontier positive and negative values.
            return self.unfolder.frontiers_pos_and_neg & frozenset(self.solution)
293
        else:
294
295
            # NEVER USED (BACKWARD is partially implemented)
            frontiers = self.unfolder.frontier_values
296
297
298
            jmax = len(frontiers)
            fsol = list()
            j = 0
299
            dec = self.shift_step * self.current_step
300
            frontier = frontiers[0]
VIGNET Pierre's avatar
VIGNET Pierre committed
301
302
303
            for i, var in enumerate(self.solution):
                # the variable is frontier var:
                if abs(var) == frontier:
304
                    fsol.append(self.solution[i+dec])# look for initial values
305
306
                    j += 1
                    if j == jmax:
VIGNET Pierre's avatar
VIGNET Pierre committed
307
                        # all frontiers are found
308
309
                        return fsol
                    frontier = frontiers[j]
VIGNET Pierre's avatar
VIGNET Pierre committed
310
        return fsol # never reach this point
VIGNET Pierre's avatar
VIGNET Pierre committed
311

312
    # Useless proposition
313
    # ps: jmax allows to stop the search when the iteration is made on solution
314
315
    # which is increasing over time.
    # without jmax, this proposition is not efficient
316
317
318
319
    #        frontiers = frozenset(self.unfolder.frontier_values)
    #        dec = self.shift_step * self.current_step
    #        if self.shift_direction == 'FORWARD':
    #            fsol = [sol for sol in self.solution if abs(sol) in frontiers]
320
    #        else:
321
    #            fsol = [self.solution[i+dec] for i, sol in enumerate(self.solution) if abs(sol) in frontiers]
322
323
324
325
    #
    #        assert len(fsol) == len(frontiers)
    #        return fsol

326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
    def extract_act_inputs_clocks(self, state_vector):
        """Extract active *inputs* and *free_clocks* from a state vector.

        Return the intersection of all inputs and free clocks of the system
        with the given state vector.

        PS: unfolder.inputs_and_free_clocks contains only positive values
            so the intersection with state_vector allows to get only activated
            variables.

        Used only by extract_act_input_clock_seq().

        :param state_vector: A state vector. A list of literals.
        :return: Tuple of activated inputs and free_clocks in the given state vector.
        :type state_vector: <list <int>>
        :rtype: <tuple>
VIGNET Pierre's avatar
VIGNET Pierre committed
342
        """
343
        # Old API
344
        # return [s_varcode for s_varcode in state_vector
345
        #        if s_varcode > 0
346
        #        and s_varcode in self.unfolder.inputs_and_free_clocks]
VIGNET Pierre's avatar
VIGNET Pierre committed
347
        return tuple(self.unfolder.inputs_and_free_clocks & frozenset(state_vector))
348

VIGNET Pierre's avatar
VIGNET Pierre committed
349
350

    def extract_act_input_clock_seq(self):
351
352
        """Extract the sequence of activated *inputs* and *events/free clocks*
        in the current solution.
353

354
        .. note::
355
356
357
358
            - Each tuple is the state of literals in a step of the solution.
            - Each literal in the tuple is an activated variable in a step.
            - Variables are inputs or events (free clocks) ONLY!

359
360
361
362
363
        .. note:: A solution is list of state vectors (list of literals).

        .. note:: This function is called by:
            - FrontierSolution.from_raw()
            - DimacsFrontierSol.ic_sequence
364
365
366
367
368
369
370

        :return: list of input vector
            (may be empty if data-flow model is without input)
        :rtype: <tuple <tuple <int>>>
        """
        # unflatten() returns a list of state vectors in DIMACS format
        # State vectors are (<list <int>>)
371
        return tuple() \
372
373
374
375
376
377
378
379
380
381
382
            if not self.unfolder.inputs_and_free_clocks \
            else tuple(
                self.extract_act_inputs_clocks(activated_inputs_and_clocks)
                for activated_inputs_and_clocks in self.unflatten() # list of lists
            )

    def __len__(self):
        """Length of solution (number of tuples of literals)
        @return: int
        """
        return len(self.solution)
383

VIGNET Pierre's avatar
VIGNET Pierre committed
384
    def __str__(self):
385
386
        """For debug: display all variables
        (including inactivated and auxiliary ones)
VIGNET Pierre's avatar
VIGNET Pierre committed
387
388
389
390
391
392
393
394
395
396
397
        """
        unfl = self.unflatten()
        stn = []
        for vect in unfl:
            vect_n = []
            for dcod in vect:
                if dcod > 0:
                    vect_n.append(self.get_var_name(dcod))
                else:
                    vect_n.append("-"+self.get_var_name(dcod))
            stn.append(vect_n)
398
        return str(stn)
VIGNET Pierre's avatar
VIGNET Pierre committed
399
400

    def display_activ_sol(self):
401
402
        """For debug: display only activated variables
        (auxiliary variables are pruned)
VIGNET Pierre's avatar
VIGNET Pierre committed
403
404
405
406
407
408
409
410
411
        """
        unfl = self.unflatten()
        stn = []
        for vect in unfl:
            vect_n = []
            for dcod in vect:
                if dcod > 0:
                    v_name = self.get_var_name(dcod)
                    if not v_name[0] == "_":
412
                        # Not auxiliary variable
VIGNET Pierre's avatar
VIGNET Pierre committed
413
414
415
                        vect_n.append(v_name)
            vect_n.sort()
            stn.append(vect_n)
416
        print(stn)
VIGNET Pierre's avatar
VIGNET Pierre committed
417
418
419


class FrontierSolution(object):
420
    """Class for symbolic (human readable) frontiers and timings representation
421

422
423
424
    The class FrontierSolution provides is a wrapper for a symbolic
    representation (human readable) of activated frontiers defined in
    RawSolution and DimacsFrontierSol objects.
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444

    Attributes:
        - The main attributes are activated_frontier which is a set of
        (string) names of frontier places which are activated in the solution.

        - The second important attribute is ic_sequence, a list of strings
        which describes the successive activated inputs and free events in
        the solution.

        - current_step is the number of steps used during the unfolding that made
        the solution.

    If events h2, h5 and input in3 are activated at step k in the solution,
    then the kth element of the list is “% h2 h5 in3”.
    This format is understood by the Cadbiom simulator.

    :type activated_frontier: <frozenset <str>>
    :type ic_sequence: <list <str>>
    :type current_step: <int>

445
446
    ..TODO::
        - Faire une super classe dont héritent RawSolution et DimacsFrontierSol
447
448
        pour éviter la duplication de code et le stockage d'attributs qu'on
        connait déjà dans les types de plus bas niveaux...
449
450
        - ... Ou détecter le type d'objet dans le constructeur => ducktyping
        - renommer l'attr activated_frontier en activated_frontiers
VIGNET Pierre's avatar
VIGNET Pierre committed
451
    """
VIGNET Pierre's avatar
VIGNET Pierre committed
452

453
454
    def __init__(self, activated_frontiers, ic_sequence, current_step):
        """Build a symbolic representation of frontier values and timing from
VIGNET Pierre's avatar
VIGNET Pierre committed
455
        a raw solution
VIGNET Pierre's avatar
VIGNET Pierre committed
456

457
458
459
460
461
462
463
464
465
466
467
468
469
470
        :param activated_frontiers: A list of (string) names of frontier places
            which are activated in the solution.
        :param ic_sequence: A list of strings which describes the successive
            activated inputs and free events in the solution.
            (format: % h1 h2)
        :param current_step: Number of steps in the sequence.
            ..note:: This attribute should be deducted with the length of ic_sequence.
        :type activated_frontiers: <frozenset <str>>
        :type ic_sequence: <list <str>>
        :type current_step: <int>
        """
        self.activated_frontier = frozenset(activated_frontiers)
        self.ic_sequence = ic_sequence
        self.current_step = current_step
VIGNET Pierre's avatar
VIGNET Pierre committed
471

VIGNET Pierre's avatar
VIGNET Pierre committed
472
    @classmethod
473
474
475
476
477
478
479
480
481
482
483
484
485
    def build_input_clock_sequence(cls, get_var_name, ic_sequence):
        """Get strings representing timings of each step in the solution.

        :param get_var_name: Method to call for a conversion of values to names.
            (binding of the method get_var_name() of an unfolder).
        :param ic_sequence:
            - Each tuple is the state of literals in a step of the solution.
            - Each literal in the tuple is an activated variable in a step.
            - Variables are inputs or events (free clocks) ONLY!
        :type get_var_name: <function>
        :type ic_sequence: <tuple <tuple <int>>
        :return: List of strings representing timings of each step in ic_sequence.
        :rtype: <list <str>>
VIGNET Pierre's avatar
VIGNET Pierre committed
486
        """
487
488
489
490
491
492
        # Strip used to remove trailing space on empty steps : "% "
        return [
            str("% " + " ".join(get_var_name(value)
            for value in step_literals)).rstrip(" ")
            for step_literals in ic_sequence
        ]
VIGNET Pierre's avatar
VIGNET Pierre committed
493

VIGNET Pierre's avatar
VIGNET Pierre committed
494
    @classmethod
495
496
497
498
499
500
501
502
503
    def from_raw(cls, raw_sol):
        """Build FrontierSolution object, a symbolic representation of frontier
        values and timings from a RawSolution solution.

        - Extract activated frontiers values (literals)
        - Convert activated frontiers values to places names (strings)
        - Extract inputs and clocks sequence (steps of the whole solution)

        :type raw_sol: <RawSolution>
VIGNET Pierre's avatar
VIGNET Pierre committed
504
        """
505
506
507
508
509
510
511
512
513
        # Get names of activated frontier places
        # RawSolution has not activated_frontiers attr we must compute them
        activated_frontier_values = raw_sol.extract_activated_frontier_values()

        activated_frontiers = \
            {raw_sol.get_var_name(var_num) for var_num in activated_frontier_values}

        # Get raw activated inputs and free clocks (values)
        # and format them so that they are understandable by humans
514
515
516
517
        ic_sequence = FrontierSolution.build_input_clock_sequence(
            raw_sol.get_var_name,
            raw_sol.extract_act_input_clock_seq()
        )
518
        # LOGGER.debug("FrontierSolution:from_raw:: ic_sequence %s", ic_sequence)
519
520
521
522

        return cls(activated_frontiers, ic_sequence, raw_sol.current_step)

    @classmethod
523
    def from_dimacs_front_sol(cls, dimacs_front_sol):
524
525
526
527
528
529
        """Build FrontierSolution object, a symbolic representation of frontier
        values and timings from a DimacsFrontierSolution solution.

        - Convert activated frontiers values to places names (strings)
        - Extract inputs and clocks sequence (steps of the whole solution)

530
        :type dimacs_front_sol: <DimacsFrontierSol>
VIGNET Pierre's avatar
VIGNET Pierre committed
531
        """
532
533
534
        # Get names of activated frontier places
        # DimacsFrontierSol already has activated_frontiers attr
        activated_frontiers = \
535
536
            {dimacs_front_sol.get_var_name(var_num)
             for var_num in dimacs_front_sol.activated_frontier_values}
537
538
539

        # Get raw activated inputs and free clocks (values)
        # and format them so that they are understandable by humans
540
541
542
543
        ic_sequence = FrontierSolution.build_input_clock_sequence(
            dimacs_front_sol.get_var_name,
            dimacs_front_sol.ic_sequence
        )
544
        # LOGGER.debug("FrontierSolution:from_dimacs_front_sol:: ic_sequence %s", ic_sequence)
545

546
        return cls(activated_frontiers, ic_sequence, dimacs_front_sol.current_step)
VIGNET Pierre's avatar
VIGNET Pierre committed
547

VIGNET Pierre's avatar
VIGNET Pierre committed
548
    @classmethod
VIGNET Pierre's avatar
VIGNET Pierre committed
549
    def from_file(cls, file_name):
550
        """Build a symbolic representation of frontier values and timing from
VIGNET Pierre's avatar
VIGNET Pierre committed
551
        a DimacsFrontierSolution solution
VIGNET Pierre's avatar
VIGNET Pierre committed
552

553
        ..warning:: This method can only be used if the file contains 1 solution...
554

555
        Note: use cadbiom_cmd/tools/solutions.py functions to reload frontiers
VIGNET Pierre's avatar
VIGNET Pierre committed
556
        """
557
558
559
560
561
562
563
564
565
566
567
        with open(file_name, "r") as f_d:
            # Get first line: frontiers
            act_front = f_d.readline().split()
            # Get steps
            ic_seq = []
            step = f_d.readline()
            current_step = 0
            while step:
                current_step += 1
                ic_seq.append(step[:-1])
                step = f_d.readline()
568

569
570
        LOGGER.debug("FrontierSolution:from_file:: ic_seq: %s; maxsteps: %s",
                     ic_seq, current_step)
571
572
573
574
575
576
577
578
579
580
581
582
        return cls(act_front, ic_seq, current_step)

    def save(self, outfile, only_macs=False):
        """Save a symbolic solution in a file
        The format is readable by the simulator and all Cadbiom tools.

        .. note:: Frontiers are sorted in (lower case) alphabetical order.

        :param outfile: Writable file handler
        :param only_macs: Write only frontiers, and skip timings.
        :type outfile: <open file>
        :type only_macs: <boolean>
583
        """
584
        outfile.write(' '.join(sorted(self.activated_frontier, key=lambda s: s.lower())) + '\n')
585
586
        if not only_macs:
            outfile.write('\n'.join(self.ic_sequence) + '\n')
VIGNET Pierre's avatar
VIGNET Pierre committed
587
        outfile.flush()
VIGNET Pierre's avatar
VIGNET Pierre committed
588

589
590
591
    def __eq__(self, other):
        """Check if two FrontierSolution have same activated frontiers
        Used with __hash__
VIGNET Pierre's avatar
VIGNET Pierre committed
592

593
594
595
596
597
        ..warning:: We do not test other attributes than activated_frontier.
            ic_sequence might be necessary.

        :type other: <DimacsFrontierSol>
        :rtype: <boolean>
VIGNET Pierre's avatar
VIGNET Pierre committed
598
        """
599
600
        return self.activated_frontier == other.activated_frontier

601
    def __ne__(self, other):
VIGNET Pierre's avatar
VIGNET Pierre committed
602
        """Python 2 requires this in conjunction to __eq__..."""
603
604
        return self.__eq__(other)

605
606
607
608
609
610
    def __hash__(self):
        """Used to test unicity of FrontierSolution in sets;
        Used with __eq__

        ..warning:: We do not test other attributes than activated_frontier.
            ic_sequence might be necessary.
VIGNET Pierre's avatar
VIGNET Pierre committed
611
        """
612
        return hash(self.activated_frontier)
VIGNET Pierre's avatar
VIGNET Pierre committed
613

614
615
616
617
618
619
620
    def __str__(self):
        """String representation of a FrontierSolution"""
        stro = "<FrontierSolution - Activated frontiers: "
        stro += str(self.activated_frontier)
        stro += "\nTimings:\n   "
        stro += "\n   ".join(self.ic_sequence) + ">"
        return stro
VIGNET Pierre's avatar
VIGNET Pierre committed
621
622


623
624
625
class DimacsFrontierSol(object):
    """Class for solution frontier and timings representation

626
    DimacsFrontierSol is a numerical representation of *frontier values and timings*
627
628
629
630
631
632
633
634
635
    from a raw solution.

    Attributes:

        :param frontier_values: Frontier values from the solution.
            These values are in DIMACS code.
            This attribute is **immutable**.
            Based on the initial RawSolution.
        :param ic_sequence: Sequence of activated inputs and events in the solution.
636
637
638
            Only used in FrontierSolution.from_dimacs_front_sol()
            (at the end of the search process for the cast into FrontierSolution)
            and for tests.
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
            Based on the initial RawSolution.
        :param current_step: The number of steps allowed in the unfolding;
            the current_step on which the properties must be satisfied (never used)
            Based on the initial RawSolution.
        :param nb_activated_frontiers: Number of activated places in the current
            Dimacs solution.
            This attribute is precomputed because it is used intensively and
            multiple times for each object in:
                MCLAnalyser.less_activated_solution
                MCLAnalyser.__prune_frontier_solution
                MCLAnalyser.__mac_exhaustive_search
        :param activated_frontier_values: Values of activated frontier places
            in the current Dimacs solution.
            Convenient attribute used:
                - by FrontierSolution.from_dimacs_front_sol()
                - to accelerate the call of self.nb_activated_frontiers
655
                - as a criterion of uniqueness, to do set operations
656
657
658
659
660
661
        :type frontier_values: <frozenset <int>>
        :type ic_sequence: <list <list <int>>>
        :type current_step: <int>
        :type nb_activated_frontiers: <int>
        :type activated_frontier_values: <frozenset <int>>
    """
VIGNET Pierre's avatar
VIGNET Pierre committed
662

663
664
665
    def __init__(self, raw_sol):
        """Build a DimacsFrontierSol, a numeric representation of frontier values
        and timings from a raw solution
VIGNET Pierre's avatar
VIGNET Pierre committed
666

667
668
        :param raw_sol: raw solution
        :type raw_sol: <RawSolution>
VIGNET Pierre's avatar
VIGNET Pierre committed
669
        """
670
        # Frontier places
VIGNET Pierre's avatar
VIGNET Pierre committed
671
672
673
        # /!\ Most of the time spent in the constructor is due to this line
        # Already a frozenset but this attribute must be immutable for __hash__,
        # cast is a security.
674
        self.frontier_values = frozenset(raw_sol.frontier_pos_and_neg_values)
VIGNET Pierre's avatar
VIGNET Pierre committed
675

676
        # Activated input/events (clocks)
677
678
        # Callable of raw_sol method (avoid to store raw_sol in this object)
        self._ic_sequence_func = raw_sol.extract_act_input_clock_seq
679
        self.current_step = raw_sol.current_step
VIGNET Pierre's avatar
VIGNET Pierre committed
680

681
682
        # CLUnfolder
        self.unfolder = raw_sol.unfolder
VIGNET Pierre's avatar
VIGNET Pierre committed
683

684
685
686
687
        # Values of activated frontier places in the current Dimacs solution
        # Convenient attribute used:
        # - by FrontierSolution.from_dimacs_front_sol()
        # - to accelerate the call of self.nb_activated_frontiers
688
        # - as a criterion of uniqueness, to do set operations
689
        self.activated_frontier_values = raw_sol.extract_activated_frontier_values()
VIGNET Pierre's avatar
VIGNET Pierre committed
690

691
692
693
        # Pre-compute nb of activated frontiers in the current solution
        # PS: use numpy to accelerate this ? The cast is costly...
        # We could keep a separated function and use lru_cache instead...
VIGNET Pierre's avatar
VIGNET Pierre committed
694
        ## TODO: replace by len() call magic method
695
696
697
698
        self.nb_activated_frontiers = len(self.activated_frontier_values)

    @classmethod
    def get_unique_dimacs_front_sols_from_raw_sols(cls, raw_sols):
699
        """Get a tuple of DimacsFrontierSols from a list of RawSolutions.
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719

        The conversion extracts keeps only frontier values from RawSolutions.
        This functions eliminates the duplicates.

        Cf TestMCLAnalyser.py:523:
            raw_sols len 6
            tpl len: 6
        TestMCLAnalyser.py:559
            raw_sols len 12:
            tpl len: 7
        TestMCLAnalyser.py:667
            raw_sols len 7:
            tpl len: 1
        TestMCLAnalyser.py:700
            raw_sols len 7
            tpl len: 1

        ..note:: We need to index the result in MCLAnalyser.less_activated_solution()
            thus, this why we return a tuple here.

720
        ..note:: The tuple of DimacsFrontierSols is not sorted by order of calculation.
721
            Thus, the first item is not the first solution found.
722
            TODO: An order could be used to adjust the number of solutions
723
724
725
726
727
728
729
730
731
732
            asked during the pruning operation in __solve_with_inact_fsolution()

        :param raw_sols: List of raw solutions;
            most of the time obtained with sq_solutions()
        :return: Set of DimacsFrontierSol
        :type raw_sols: <list <RawSolution>>
        :rtype: <tuple <DimacsFrontierSol>>
        """
        return tuple({DimacsFrontierSol(sol) for sol in raw_sols})

733
734
735
736
737
738
    @property
    def ic_sequence(self):
        """Sequence of activated inputs and events (clocks) in the solution.

        (may be empty if data-flow model is without input)

VIGNET Pierre's avatar
VIGNET Pierre committed
739
740
        .. seealso:: RawSolution.extract_act_input_clock_seq()

741
742
743
        .. note:: Only used in FrontierSolution.from_dimacs_front_sol()
            (at the end of the search process for the cast into FrontierSolution)
            and for tests.
VIGNET Pierre's avatar
VIGNET Pierre committed
744
            => This step is expensive !
745
746
747
748
        """
        # Cf constructor
        return self._ic_sequence_func()

749
750
751
752
    def get_var_name(self, var_num):
        """For translation to symbolic representation
        Return the string that corresponds to he name of the variable value.
        :rtype: <str>
VIGNET Pierre's avatar
VIGNET Pierre committed
753
        """
754
        return self.unfolder.get_var_name(var_num)
VIGNET Pierre's avatar
VIGNET Pierre committed
755

VIGNET Pierre's avatar
VIGNET Pierre committed
756
    def nb_timed(self):
757
758
        """Count the number of events in the current Dimacs solution (not used)
        :rtype: <int>
VIGNET Pierre's avatar
VIGNET Pierre committed
759
        """
760
761
762
763
764
765
766
767
        # ic_sequence: list of strings which describes the successive activated
        # inputs and free events
        solution_events = (len(ic_act) for ic_act in self.ic_sequence)
        return sum(it.chain(*solution_events))

    def __len__(self):
        """Get the number of activated frontiers in the current DimacsFrontierSol
        :rtype: <int>
VIGNET Pierre's avatar
VIGNET Pierre committed
768
        """
769
        return len(self.activated_frontier_values)
VIGNET Pierre's avatar
VIGNET Pierre committed
770

771
772
773
774
775
776
777
778
779
    def __eq__(self, other):
        """Check if two DimacsFrontierSol have same frontiers values
        Used with __hash__

        ..warning:: We do not test other attributes than activated_frontier_values.
            ic_sequence might be necessary.

        :type other: <DimacsFrontierSol>
        :rtype: <boolean>
VIGNET Pierre's avatar
VIGNET Pierre committed
780
        """
781
782
        return self.activated_frontier_values == other.activated_frontier_values

783
    def __ne__(self, other):
VIGNET Pierre's avatar
VIGNET Pierre committed
784
        """Python 2 requires this in conjunction to __eq__..."""
785
786
        return self.__eq__(other)

787
788
789
790
791
792
    def __hash__(self):
        """Used to test unicity of DimacsFrontierSol in sets;
        Used with __eq__

        ..warning:: We do not test other attributes than activated_frontier_values.
            ic_sequence might be necessary.
VIGNET Pierre's avatar
VIGNET Pierre committed
793
        """
794
        return hash(self.activated_frontier_values)
VIGNET Pierre's avatar
VIGNET Pierre committed
795

796
797
798
799
800
801
    def __repr__(self):
        return str(self.activated_frontier_values)

    def __str__(self):
        """For tests and debug"""
        return "<DimacsFrontierSol - Activated frontiers values: %s>".format(self.activated_frontier_values)
VIGNET Pierre's avatar
VIGNET Pierre committed
802