MCLQuery.py 13.7 KB
Newer Older
1
# -*- coding: utf-8 -*-
VIGNET Pierre's avatar
VIGNET Pierre committed
2
3
4
## Filename    : MCLQuery.py
## Author(s)   : Michel Le Borgne
## Created     : 10 sept. 2012
5
6
## Revision    :
## Source      :
VIGNET Pierre's avatar
VIGNET Pierre committed
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
##
## Copyright 2012 : IRISA/IRSET
##
## This library is free software; you can redistribute it and/or modify it
## under the terms of the GNU General Public License as published
## by the Free Software Foundation; either version 2.1 of the License, or
## any later version.
##
## This library is distributed in the hope that it will be useful, but
## WITHOUT ANY WARRANTY, WITHOUT EVEN THE IMPLIED WARRANTY OF
## MERCHANTABILITY OR FITNESS FOR A PARTICULAR PURPOSE.  The software and
## documentation provided here under is on an "as is" basis, and IRISA has
## no obligations to provide maintenance, support, updates, enhancements
## or modifications.
## In no event shall IRISA be liable to any party for direct, indirect,
## special, incidental or consequential damages, including lost profits,
## arising out of the use of this software and its documentation, even if
## IRISA have been advised of the possibility of such damage.  See
## the GNU General Public License for more details.
##
## You should have received a copy of the GNU General Public License
## along with this library; if not, write to the Free Software Foundation,
## Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA.
##
## The original code contained here was initially developed by:
##
##     Michel Le Borgne.
##     IRISA
##     Symbiose team
##     IRISA  Campus de Beaulieu
37
38
##     35042 RENNES Cedex, FRANCE
##
VIGNET Pierre's avatar
VIGNET Pierre committed
39
40
41
42
43
44
##
## Contributor(s): Geoffroy Andrieux - IRISA/IRSET
##
"""
Query internal representation
"""
45
46
from cadbiom.models.clause_constraints.mcl.MCLSolutions import MCLException
from cadbiom import commons as cm
47
from logging import DEBUG
48
49

LOGGER = cm.logger()
VIGNET Pierre's avatar
VIGNET Pierre committed
50
51

class MCLSimpleQuery(object):
VIGNET Pierre's avatar
VIGNET Pierre committed
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
    """Class packaging the elements of a query


    Attributes:

        :param start_prop: start property; logical formulas
        :param inv_prop: invariant property; logical formulas
        :param final_prop: final property; logical formulas
        :param variant_prop: list of logical formulas
            :Example:
                ['', 'h2 and h2', '', 'h2']

        :param dim_start: start property in DIMACS form - optional
        :param dim_inv: invariant property in DIMACS form - optional
        :param dim_final: final property in DIMACS form - optional
        :param dim_variant_prop: list of lists of dimacs clauses
        :param steps_before_reach: number of shift before testing the
            final property - optional

        :type start_prop: <str>
        :type inv_prop: <str>
        :type final_prop: <str>
        :type variant_prop: <list <str>>
75

VIGNET Pierre's avatar
VIGNET Pierre committed
76
77
78
79
80
81
82
83
84
        :type dim_start: <list <DClause>>, default []
        :type dim_inv: <list <DClause>>, default []
        :type dim_final: <list <DClause>>, default []
        :type dim_variant_prop: <list <list <DClause>>
        :type steps_before_reach: <int>, default value 0

    NB: DClause: A clause coded as a list of DIMACS coded literals: <list <int>>

    """
VIGNET Pierre's avatar
VIGNET Pierre committed
85
86
87
88
89
90
    def __init__(self, start_prop, inv_prop, final_prop):
        """
        @param start_prop: init property - None is allowed
        @param inv_prop: invariant property - None allowed
        @param final_prop: final property - None is allowed
        """
91
        if LOGGER.getEffectiveLevel() == DEBUG:
VIGNET Pierre's avatar
VIGNET Pierre committed
92
93
94
            LOGGER.debug("MCLSimpleQuery params:: start prop: " + \
                         str(start_prop) + '; inv prop: ' + \
                         str(inv_prop) + '; final prop: ' + \
95
                         str(final_prop))
VIGNET Pierre's avatar
VIGNET Pierre committed
96
97
98
99
100
101
102
103
104
        self.start_prop = start_prop  # logical formula or None
        self.inv_prop = inv_prop      # logical formula or None
        self.variant_prop = []        # list<logical formula>
        self.final_prop = final_prop  # logical formula or None
        # dimacs form of preceding
        self.dim_start = []         # list<DClause>
        self.dim_inv = []           # list<DClause>
        self.dim_final = []         # list<DClause>
        self.dim_variant_prop = []  # list<list<DClause>>
105

VIGNET Pierre's avatar
VIGNET Pierre committed
106
        self.steps_before_reach = 0
107

VIGNET Pierre's avatar
VIGNET Pierre committed
108
109
    @classmethod
    def from_frontier_sol(cls, f_sol):
VIGNET Pierre's avatar
VIGNET Pierre committed
110
111
112
113
114
115
116
117
118
119
120
121
        """Build a query from a frontier solution

        Start property is based on activated frontiers.

        All frontiers that are not in activated_frontier
        **ARE NOT** forced to be inactivated with a negative value.

        Variant property enforces same timing on activated events,
        and the others are free.

        @param f_sol: the FrontierSolution (human readable solution)
        @param unfolder: unfolder in use
VIGNET Pierre's avatar
VIGNET Pierre committed
122
123
        """
        # start condition enforce activation of solution places
124
        start_prop = None
VIGNET Pierre's avatar
VIGNET Pierre committed
125
        if f_sol.activated_frontier:
126
127
            start_prop = " and ".join(f_sol.activated_frontier)

VIGNET Pierre's avatar
VIGNET Pierre committed
128
129
        # no invariant property
        inv_prop = None
130
131
132
133

        # no final property
        final_prop = None

VIGNET Pierre's avatar
VIGNET Pierre committed
134
        # variant property enforce same timing
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
        # Each event has a list of steps which it belongs
        # Ex: for steps: ['%', '% h2 h2', '%', '% h2']
        # variant property: ['', 'h2 and h2', '', 'h2']
        print("Reading ic_sequence from FrontierSolution...")

        # - Iterate on steps
        # - Get events names in each step
        # (remove the leading "%" and split the string on spaces)
        # - join events names with a logical operator " and "
        var_prop = [" and ".join(raw_step[1:].split()) for raw_step in f_sol.ic_sequence]
        ## TODO fix this (not sure of the behaviour if var_prop is [])
        if not var_prop:
            var_prop = None

        n_query = MCLSimpleQuery(start_prop, inv_prop, final_prop)
        n_query.variant_prop = var_prop
VIGNET Pierre's avatar
VIGNET Pierre committed
151
        return n_query
152
153


VIGNET Pierre's avatar
VIGNET Pierre committed
154
155
    @classmethod
    def from_frontier_sol_new_timing(cls, f_sol, unfolder):
VIGNET Pierre's avatar
VIGNET Pierre committed
156
157
158
159
160
161
162
163
164
165
        """Build a query from a frontier solution

        Start property is based on activated frontiers.

        Search all frontiers that are not in activated_frontier
        and force their inactivation with a negative value.

        **Variant property enforces new timing**

        @param f_sol: the FrontierSolution (human readable solution)
VIGNET Pierre's avatar
VIGNET Pierre committed
166
167
168
        @param unfolder: unfolder in use
        """
        # activation part of start condition
169
        start_prop = None
VIGNET Pierre's avatar
VIGNET Pierre committed
170
        if f_sol.activated_frontier:
171
172
            start_prop = " and ".join(f_sol.activated_frontier)

VIGNET Pierre's avatar
VIGNET Pierre committed
173
174
        # no invariant property
        inv_prop = None
175
176
177
178
179
180
181
182
183
184
185
186
187

        # no final property
        final_prop = None

        # variant property enforce new timing on activated events
        # Each event has a list of steps which it belongs
        # Ex: for steps: ['%', '% h2 h2', '%', '% h2']
        # variant property: ['', 'not (h2) or not (h2)', '', 'not (h2)']
        print("Reading ic_sequence from FrontierSolution...")

        # - Iterate on steps
        # - Get events names in each step
        # (remove the leading "%" and split the string on spaces)
VIGNET Pierre's avatar
VIGNET Pierre committed
188
189
        # - negation of each event with "not ( event )"
        # - join events names with a logical operator " or "
190
191
192
193
194
195
196
197
198
199
200
201
        var_prop = [" or ".join("not (" + icp + ")" for icp in raw_step[1:].split())
                    for raw_step in f_sol.ic_sequence]
        ## TODO fix this (not sure of the behaviour if var_prop is [])
        if not var_prop:
            var_prop = None

        # inactivation of other frontier places at start (DIMACS format)
        # Search all frontiers that are not in activated_frontier
        # and force their inactivation with a negative value.
        ## TODO: set operation...
        ## dim_start doit-il etre ordonné ?
        frontier = unfolder.frontier_values
VIGNET Pierre's avatar
VIGNET Pierre committed
202
203
204
205
        l_dstart = []
        for i_fr in frontier:
            name = unfolder.get_var_name(i_fr)
            if not name in f_sol.activated_frontier:
206
                l_dstart.append([-i_fr])
207

208
209
210
        n_query = MCLSimpleQuery(start_prop, inv_prop, final_prop)
        n_query.variant_prop = var_prop
        n_query.dim_start = l_dstart
VIGNET Pierre's avatar
VIGNET Pierre committed
211
        return n_query
212

VIGNET Pierre's avatar
VIGNET Pierre committed
213
214
    @classmethod
    def from_frontier_sol_same_timing(cls, f_sol, unfolder):
VIGNET Pierre's avatar
VIGNET Pierre committed
215
216
217
218
219
220
221
222
223
224
        """Build a query from a frontier solution

        Start property is based on activated frontiers.

        Search all frontiers that are not in activated_frontier
        and force their inactivation with a negative value.

        **Variant property enforces same timing on activated events,
        and the others are free.**

225
        @param f_sol: the FrontierSolution (human readable solution)
VIGNET Pierre's avatar
VIGNET Pierre committed
226
227
228
        @param unfolder: unfolder in use
        """
        # activation part of start condition
229
        start_prop = None
VIGNET Pierre's avatar
VIGNET Pierre committed
230
        if f_sol.activated_frontier:
231
232
            start_prop = " and ".join(f_sol.activated_frontier)

VIGNET Pierre's avatar
VIGNET Pierre committed
233
234
        # no invariant property
        inv_prop = None
235
236
237
238

        # no final property
        final_prop = None

239
        # variant property enforce same timing on activated events
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
        # Each event has a list of steps which it belongs
        # Ex: for steps: ['%', '% h2 h2', '%', '% h2']
        # variant property: ['', 'h2 and h2', '', 'h2']
        print("Reading ic_sequence from FrontierSolution...")

        # - Iterate on steps
        # - Get events names in each step
        # (remove the leading "%" and split the string on spaces)
        # - join events names with a logical operator " and "
        var_prop = [" and ".join(raw_step[1:].split()) for raw_step in f_sol.ic_sequence]
        ## TODO fix this (not sure of the behaviour if var_prop is [])
        if not var_prop:
            var_prop = None

        # inactivation of other frontier places at start (DIMACS format)
        # Search all frontiers that are not in activated_frontier
        # and force their inactivation with a negative value.
        ## TODO: set operation...
        ## dim_start doit-il etre ordonné ?
VIGNET Pierre's avatar
VIGNET Pierre committed
259
        l_dstart = []
260
        for i_fr in unfolder.frontier_values:
VIGNET Pierre's avatar
VIGNET Pierre committed
261
262
            name = unfolder.get_var_name(i_fr)
            if not name in f_sol.activated_frontier:
263
                l_dstart.append([-i_fr])
264
265


266
267
268
269
270
271
        n_query = MCLSimpleQuery(start_prop, inv_prop, final_prop)
        # list of logical formulas
        n_query.variant_prop = var_prop
        # start property in DIMACS format
        n_query.dim_start = l_dstart
        return n_query
272

VIGNET Pierre's avatar
VIGNET Pierre committed
273
274
275
    def set_dim_start(self, dim_start):
        """
        @param dim_start: start property in DIMACS format
VIGNET Pierre's avatar
VIGNET Pierre committed
276
        ## TODO: remove this in the rest of the project
VIGNET Pierre's avatar
VIGNET Pierre committed
277
278
        """
        self.dim_start = dim_start
279

280
    def merge(self, query):
VIGNET Pierre's avatar
VIGNET Pierre committed
281
282
283
284
285
286
287
        """Return a new query which is a merge of two queries into one.

        - start, invariant and final properties are merged.
        - If both queries have variant properties, they must be on the same horizon
        (number of steps).
        - steps before reach is set to zero.
        - dim properties are also merged: dim_start, dim_inv, dim_final
288

289
        @param query: a MCLSimpleQuery
290
291
        @raise MCLException: if the queries have variant properties on
        different horizons.
VIGNET Pierre's avatar
VIGNET Pierre committed
292
293
294
        """
        # merge of start properties
        if not self.start_prop:
295
296
297
            start_prop = query.start_prop
        elif not query.start_prop:
            start_prop = self.start_prop
VIGNET Pierre's avatar
VIGNET Pierre committed
298
        else:
299
            start_prop = "(" + self.start_prop + ") and (" + query.start_prop + ")"
VIGNET Pierre's avatar
VIGNET Pierre committed
300
301
        # merge of invariant properties
        if not self.inv_prop:
302
303
            i_prop = query.inv_prop
        elif not query.inv_prop:
VIGNET Pierre's avatar
VIGNET Pierre committed
304
305
            i_prop = self.inv_prop
        else:
306
            i_prop = "(" + self.inv_prop + ") and (" + query.inv_prop + ")"
VIGNET Pierre's avatar
VIGNET Pierre committed
307
308
        # merge of final properties
        if not self.final_prop:
309
310
311
            final_prop = query.final_prop
        elif not query.final_prop:
            final_prop = self.final_prop
VIGNET Pierre's avatar
VIGNET Pierre committed
312
        else:
313
            final_prop = "(" + self.final_prop + ") and (" + query.final_prop + ")"
314

315
        n_query = MCLSimpleQuery(start_prop, i_prop, final_prop)
VIGNET Pierre's avatar
VIGNET Pierre committed
316

VIGNET Pierre's avatar
VIGNET Pierre committed
317
        # merge of variant prop
318
        var_prop = None
VIGNET Pierre's avatar
VIGNET Pierre committed
319
        if not self.variant_prop:
320
321
322
            var_prop = query.variant_prop
        elif not query.variant_prop:
            var_prop = self.variant_prop
VIGNET Pierre's avatar
VIGNET Pierre committed
323
324
        else:
            ll1 = len(self.variant_prop)
325
            ll2 = len(query.variant_prop)
VIGNET Pierre's avatar
VIGNET Pierre committed
326
            if ll1 != ll2:
327
328
329
330
                raise MCLException(
                    "Tempting to merge two queries with variant prop of different lengths"
                    "current: {}; other: {}".format(ll1, ll2)
                )
VIGNET Pierre's avatar
VIGNET Pierre committed
331
            else:
332
                var_prop = []
333
334
335
336
337
338
339
340
341
342
343
                # 2 empty, 1 empty and not the other, none empty
                for a, b in zip(self.variant_prop, query.variant_prop):
                    if a and b:
                        var_prop.append(a + " and " + b)
                    elif a and not b:
                        var_prop.append(a)
                    elif not a and b:
                        var_prop.append(b)
                    else:
                        var_prop.append("")

344
        n_query.variant_prop = var_prop
345

VIGNET Pierre's avatar
VIGNET Pierre committed
346
        # merge of dim properties
347
348
349
        n_query.dim_start += query.dim_start
        n_query.dim_inv += query.dim_inv
        n_query.dim_final += query.dim_final
VIGNET Pierre's avatar
VIGNET Pierre committed
350
        return n_query
351

VIGNET Pierre's avatar
VIGNET Pierre committed
352
    def __str__(self):
VIGNET Pierre's avatar
VIGNET Pierre committed
353
        """Print logical formulas in query"""
VIGNET Pierre's avatar
VIGNET Pierre committed
354
355
        str_out = "Start_property: "
        if self.start_prop:
356
            str_out = str_out + self.start_prop
VIGNET Pierre's avatar
VIGNET Pierre committed
357
358
359
360
361
362
363
364
365
366
367
        str_out = str_out + "\nInv property: "
        if self.inv_prop:
            str_out = str_out + self.inv_prop
        str_out = str_out + "\nFinal property: "
        if self.final_prop:
            str_out = str_out + self.final_prop
        str_out = str_out + "\nVariant property: "
        if self.variant_prop:
#            str_out = str_out + self.variant_prop[0]
#            for prop in self.variant_prop[1:]:
#                str_out = str_out + ", " + prop
VIGNET Pierre's avatar
VIGNET Pierre committed
368
            str_out = str_out + str(self.variant_prop)
VIGNET Pierre's avatar
VIGNET Pierre committed
369
        return str_out