TestCLUnfolder.py 46.1 KB
Newer Older
1
# -*- coding: utf-8 -*-
VIGNET Pierre's avatar
VIGNET Pierre committed
2 3 4
## Filename    : TestCLUnfolder.py
## Author(s)   : Michel Le Borgne
## Created     : 13 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
##
## Contributor(s):
##
42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82
"""Unitary Test of the unfolder

Test forward initialization for various models and properties types

Pytest call:
    pytest cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py::test_init_forward

Query attributes:
    self.dim_start = []         # list<DClause>
    self.dim_inv = []           # list<DClause>
    self.dim_final = []         # list<DClause>
    self.dim_variant = []       # list<list<DClause>>

CLUnfolder attributes that contain query attributes:
    self.__initial_property = None    # logical formula - literal boolean expression
    self.__dimacs_initial = None      # list of DIMACS clauses
    self.__final_property = None      # logical formula
    self.__dimacs_final = None        # list of DIMACS clauses
    self.__invariant_property = None  # logical formula
    self.__dimacs_invariant = None    # list of DIMACS clauses
    self.__variant_property = None    # list<logic formulas>
    self.__dimacs_variant = None      # list<list<DIMACS clauses>>

CLUnfolder attributes that contain clauses:
    self.__precomputed_variant_constraints = None  # list<list<DIMACS clauses>>
    dynamic_constraints
    initial_constraints
    invariant_constraints
    variant_constraints
    final_constraints

.. note:: Mangling prefix for protected attributes: unfolder._CLUnfolder__*

:Example to get a mapping of numeric clauses to str clauses:

    mappings = [[unfolder.get_var_name(value) for value in clause]
        for clause in dynamic_constraints[0]]

.. TODO:
    - search solutions for the given properties
"""
83
from __future__ import print_function
VIGNET Pierre's avatar
VIGNET Pierre committed
84
import unittest
85 86
import pytest
import pkg_resources
VIGNET Pierre's avatar
VIGNET Pierre committed
87

88 89 90
from cadbiom.models.guard_transitions.chart_model import ChartModel
from cadbiom.models.guard_transitions.analyser.ana_visitors import TableVisitor
from cadbiom.models.clause_constraints.CLDynSys import CLDynSys
91
from cadbiom.models.clause_constraints.mcl.MCLTranslators import GT2Clauses
92
from cadbiom.models.clause_constraints.mcl.CLUnfolder import CLUnfolder
93 94
from cadbiom.models.clause_constraints.mcl.MCLAnalyser import MCLAnalyser
from cadbiom.models.clause_constraints.mcl.MCLQuery import MCLSimpleQuery
95
from cadbiom.models.clause_constraints.mcl.MCLSolutions import MCLException
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


class ErrorReporter(object):
    """error reporter of the compil type"""
    def __init__(self):
        self.context = ""
        self.error = False
        pass

    def display(self, mess):
        """
        just printing
        """
        self.error = True
        print('\n>> '+self.context+"  "+mess)

    def display_info(self, mess):
        """
        just printing
        """
        print('\n-- '+mess)

    def set_context(self, cont):
        """
        for transition compiling
        """
        self.context = cont

VIGNET Pierre's avatar
VIGNET Pierre committed
124 125 126 127 128 129 130 131 132 133 134
def model1():
    """
    A simple ChartModel with two nodes and a transition
    """
    # build dynamical system
    model = ChartModel("Test")
    root = model.get_root()
    node_1 = root.add_simple_node('n1', 0, 0)
    node_2 = root.add_simple_node('n2', 0, 0)
    root.add_transition(node_1, node_2)
    return model
135

VIGNET Pierre's avatar
VIGNET Pierre committed
136 137
def model2():
    """
138
    ChartModel model1 + 3 nodes and 2 transitions and a cycle without start
VIGNET Pierre's avatar
VIGNET Pierre committed
139 140 141 142 143 144 145 146 147 148 149 150 151 152
    """
    # build dynamical system
    model = model1()
    root = model.get_root()
    node_3 = root.add_simple_node('n3', 0, 0)
    node_4 = root.add_simple_node('n4', 0, 0)
    root.add_transition(node_3, node_4)
    node_5 = root.add_simple_node('n5', 0, 0)
    root.add_transition(node_4, node_5)
    root.add_transition(node_5, node_3)
    return model

def model3():
    """
153
    ChartModel model2 + 1 node + 1 start node and a transition
VIGNET Pierre's avatar
VIGNET Pierre committed
154 155 156 157 158 159 160 161 162 163 164
    """
    # build dynamical system
    model = model2()
    root = model.get_root()
    node_s = root.add_start_node('n3', 0, 0)
    node_3 = model.get_simple_node('n3')
    root.add_transition(node_s, node_3)
    return model

def model4():
    """
165 166 167 168 169
    ChartModel with:
        - 1 input node: in1
        - 5 nodes: n1, n2, n3, n4, n5
        - 5 transitions: n1-n2, n3-n4, n4-n5, n5-n3, in1-n1
        - 2 free clocks: hh1: (n3 or n4) on n1-n2, hh2: (n1 and n3) on n4-n5
VIGNET Pierre's avatar
VIGNET Pierre committed
170 171 172 173 174 175 176 177 178 179 180 181 182
    """
    model = ChartModel("Test")
    root = model.get_root()
    node_1 = root.add_simple_node('n1', 0, 0)
    node_2 = root.add_simple_node('n2', 0, 0)
    tr0 = root.add_transition(node_1, node_2)
    tr0.set_event('hh1')
    tr0.set_condition("n3 or n4")
    node_3 = root.add_simple_node('n3', 0, 0)
    node_4 = root.add_simple_node('n4', 0, 0)
    root.add_transition(node_3, node_4)
    node_5 = root.add_simple_node('n5', 0, 0)
    tr1 = root.add_transition(node_4, node_5)
183
    root.add_transition(node_5, node_3)
VIGNET Pierre's avatar
VIGNET Pierre committed
184 185 186 187 188
    tr1.set_event("hh2")
    tr1.set_condition("n1 and n3")
    node_i =  root.add_input_node('in1', 0, 0)
    tri = root.add_transition(node_i, node_1)
    tri.set_condition("n5")
189 190 191 192 193 194

    # Frontier test: Add a start node on n3 or do not attempt any frontier
    # place because there is a SCC composed of n3, n4, n5.
    #node_s = root.add_start_node('s1', 0, 0)
    #root.add_transition(node_s, node_3)

VIGNET Pierre's avatar
VIGNET Pierre committed
195 196 197
    return model

def create_unfolder(model):
198
    """Return an unfolder for the given model"""
VIGNET Pierre's avatar
VIGNET Pierre committed
199 200 201 202 203 204
    tvisit = TableVisitor(None) # no error display
    model.accept(tvisit)
    cld = CLDynSys( tvisit.tab_symb, None)
    reporter = ErrorReporter()
    cvisit = GT2Clauses(cld, reporter, True)
    model.accept(cvisit)
205
    # unfolder
VIGNET Pierre's avatar
VIGNET Pierre committed
206 207
    return CLUnfolder(cld)

208 209
@pytest.fixture()
def textual_properties():
VIGNET Pierre's avatar
VIGNET Pierre committed
210
    """start, invariant, final properties in textual form"""
211
    return (
212
        ("M", "L", "C"), # No solution (because inhibitor M is activated)
213 214
        ("", "L", "C and K"), # Solution: D E F I L
        ("", "", "C"), # Solutions: F E L D, D E F I
215 216 217
    )

@pytest.fixture()
218
def numeric_properties():
VIGNET Pierre's avatar
VIGNET Pierre committed
219
    """start, invariant, final properties in DIMACS form"""
220
    return (
221
        # "M", "L", "C"
222
        ([[13]], [[12]], [[3]]),
223
        # "", "L", "C and K"
224 225 226 227 228
        ([], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]),
    )

@pytest.fixture()
def feed_mclanalyser():
229 230 231 232 233 234 235
    """Setup MCLAnalyser with a bcx model

    15 places: A, B, C, D, E, F, G, H, I, J, K, L, M, N, P
    8 clocks: _h2, _h3, _h4, _h5, _h6, _h7, _h_0, _h_1
    Frontiers: D, E, F, G, I, L, N

    """
236
    rep = ErrorReporter()
237
    # debug: Force __var_list to be sorted at the output of base_var_set from
238 239 240 241 242 243 244 245
    # CLDynSys for reproductibility in tests (literals naming)
    mcla = MCLAnalyser(rep, debug=True)
    filename = pkg_resources.resource_filename(
        __name__, # package name
        "examples/example_model.bcx"
    )
    mcla.build_from_chart_file(filename)
    return mcla
246

VIGNET Pierre's avatar
VIGNET Pierre committed
247 248 249 250 251 252 253

class TestCLUnfolder(unittest.TestCase):
    """
    Test public and some private methods (test_method form)
    """
    def test_var_name(self):
        """
254
        Test of variables at initial state uncoding and decoding
VIGNET Pierre's avatar
VIGNET Pierre committed
255 256 257
        """
        model = model1()
        unfolder = create_unfolder(model)
258 259 260 261 262 263

        # Test unfolder init and internal dynamic system
        assert unfolder._CLUnfolder__shift_step == 2
        assert unfolder.shift_step_init == 2
        assert unfolder.get_var_number() == 2

VIGNET Pierre's avatar
VIGNET Pierre committed
264 265 266
        # naming and coding variables
        cn1 = unfolder.var_dimacs_code('n1')
        cn2 = unfolder.var_dimacs_code('n2')
267

VIGNET Pierre's avatar
VIGNET Pierre committed
268 269 270
        res = unfolder.get_var_name(cn1) == 'n1'
        res = res and (unfolder.get_var_name(cn2) == 'n2')
        self.assert_(res,'Error in variable name 1')
271

VIGNET Pierre's avatar
VIGNET Pierre committed
272 273 274 275
        res = unfolder.get_var_name(7) == 'n1'
        self.assert_(res,'Error in variable name 2')
        res = unfolder.get_var_name(8) == 'n2'
        self.assert_(res,'Error in variable name 3')
276

VIGNET Pierre's avatar
VIGNET Pierre committed
277 278 279 280
        res = unfolder.get_var_indexed_name(7) == 'n1_3'
        self.assert_(res,'Error in variable name 4')
        res = unfolder.get_var_indexed_name(8) == 'n2_3'
        self.assert_(res,'Error in variable name 5')
281

282 283
        # Test number of variables
        assert unfolder.get_system_var_number() == unfolder.get_var_number()
284 285


VIGNET Pierre's avatar
VIGNET Pierre committed
286 287 288 289
    def test_frontier(self):
        """
        Test frontier computation and encoding
        """
290
        ## model1
VIGNET Pierre's avatar
VIGNET Pierre committed
291 292 293
        model = model1()
        unfolder = create_unfolder(model)
        # test frontier: should be n1
294 295
        frontier_value = unfolder.frontier_values[0]
        res = unfolder.get_var_name(frontier_value) == 'n1'
296
        res = res and (len(unfolder.frontier_values) == 1)
VIGNET Pierre's avatar
VIGNET Pierre committed
297
        self.assert_(res,'Error in frontier: model1')
298

299
        ## model2 (one cycle without start)
VIGNET Pierre's avatar
VIGNET Pierre committed
300 301
        model = model2()
        unfolder = create_unfolder(model)
302

VIGNET Pierre's avatar
VIGNET Pierre committed
303
        # test frontier: should be n1
304 305
        frontier_value = unfolder.frontier_values[0]
        res = unfolder.get_var_name(frontier_value) == 'n1'
306
        res = res and (len(unfolder.frontier_values) == 1)
307
        self.assert_(res,'Error in frontier: model2')
VIGNET Pierre's avatar
VIGNET Pierre committed
308

309
        ## model3: same as model2 but with a start on n3
VIGNET Pierre's avatar
VIGNET Pierre committed
310 311
        model = model3()
        unfolder = create_unfolder(model)
312

VIGNET Pierre's avatar
VIGNET Pierre committed
313
        # test frontier - should be {n1, n3}
314 315 316 317
        frontier_values = unfolder.frontier_values
        res = len(frontier_values) == 2
        res = res and unfolder.get_var_name(frontier_values[0]) == 'n1'
        res = res and unfolder.get_var_name(frontier_values[1]) == 'n3'
318 319
        self.assert_(res,'Error in frontier: model3')

320
        ## model4 - No frontiers (even if we can get input node in1 in the solutions)
VIGNET Pierre's avatar
VIGNET Pierre committed
321 322
        model = model4()
        unfolder = create_unfolder(model)
323
        res = len(unfolder.frontier_values) == 0
324 325 326
        self.assert_(res,'Error in frontier: model4')


VIGNET Pierre's avatar
VIGNET Pierre committed
327 328 329 330 331 332 333
    def test_free_clocks_inputs(self):
        """
        test on free clocks and input computation
        """
        # model3: no free clock, no input
        model = model3()
        unfolder = create_unfolder(model)
334
        lfc = unfolder.free_clocks
335
        self.assertEqual(len(lfc), 0, 'Error in free clocks: model3')
336
        lin = unfolder.inputs
337
        self.assertEqual(len(lin), 0,'Error in inputs 1')
338

VIGNET Pierre's avatar
VIGNET Pierre committed
339 340 341
        # model4: two free clocks and one input
        model = model4()
        unfolder = create_unfolder(model)
342
        lfc = unfolder.free_clocks
343
        self.assertEqual(len(lfc), 2, 'Error in free clocks: model4')
344
        found_names = {unfolder.get_var_name(clock) for clock in lfc}
345 346 347 348 349
        self.assertEqual(
            found_names,
            {'hh2', 'hh1'},
            'Error in free clocks names: model4'
        )
350
        lin = unfolder.inputs
351
        self.assertEqual(len(lin), 1, 'Error in inputs: model4')
352
        found_names = {unfolder.get_var_name(inpt) for inpt in lin}
353
        self.assertEqual(found_names, {'in1'}, 'Error in inputs names: model4')
354 355


356 357 358 359 360 361 362 363 364 365 366 367 368 369
def init_forward_unfolding_part_1(unfolder):
    """Initialization step only"""

    unfolder._CLUnfolder__shift_direction = 'FORWARD'
    unfolder._CLUnfolder__current_step = 1
    unfolder._CLUnfolder__shift_step = unfolder.shift_step_init  # back to basic!
    unfolder._CLUnfolder__aux_code_table = dict()            # flush auxiliary variables
    unfolder._CLUnfolder__aux_list = []                      # idem

    # Init properties to generate all variable num codes
    unfolder._CLUnfolder__init_initial_constraint_0()
    unfolder._CLUnfolder__init_final_constraint_0()
    unfolder._CLUnfolder__init_invariant_constraint_0()
    unfolder._CLUnfolder__init_variant_constraints_0()
370 371 372
    # Should be after init_initial and init_invariant
    unfolder._CLUnfolder__prune_initial_no_frontier_constraint_0()

373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393

def init_forward_unfolding_part_2(unfolder):
    """Shift step only"""

    # Now shifting is possible
    unfolder._CLUnfolder__forward_init_dynamic()
    unfolder._CLUnfolder__shift_final()
    unfolder._CLUnfolder__shift_invariant()
    # PS: __variant_constraints si already initialized for the first step.

def test_init_unfolder(feed_mclanalyser):

    mcla = feed_mclanalyser
    unfolder = mcla.unfolder # shortcut

    # Initialization step only
    init_forward_unfolding_part_1(mcla.unfolder)

    ## Test CLDynSys
    # 15 places
    assert unfolder.get_var_number() == 46
394
    assert unfolder.shift_step_init == 46
395 396 397

    # __var_list is built on casted set; MCLAnalyser is un debug mode
    # so the list is sorted
398
    # 47 elems but max id for literals is 46
399 400 401 402 403 404 405 406 407 408 409 410 411 412
    expected = [
        '##',
        'A', 'B', 'C', 'D', 'E', 'F', 'G', 'H', 'I', 'J', 'K', 'L', 'M', 'N', 'P',
        '_h2', '_h3', '_h4', '_h5', '_h6', '_h7', '_h_0', '_h_1', '_lit0', '_lit1',
        '_lit10', '_lit11', '_lit12', '_lit13', '_lit14', '_lit15', '_lit16',
        '_lit17', '_lit18', '_lit19', '_lit2', '_lit20', '_lit21', '_lit22',
        '_lit3', '_lit4', '_lit5', '_lit6', '_lit7', '_lit8', '_lit9'
    ]

    print(unfolder._CLUnfolder__var_list)
    assert unfolder._CLUnfolder__var_list == expected

    ## Test mapping of variables names to values
    expected_var_code_table = {
413
        '_lit22': 39, '_lit20': 37, '_lit21': 38, '_lit19': 35, '_lit15': 31,
414
        '_lit18': 34, '_lit6': 43, '_lit17': 33, '_lit13': 29, '_lit9': 46,
415 416 417
        '_lit8': 45,  '_lit16': 32, '_lit12': 28, '_lit3': 40, '_lit2': 36,
        '_lit1': 25, '_lit0': 24, '_lit7': 44, '_lit11': 27, '_lit5': 42,
        '_lit4': 41, '_lit14': 30, '_lit10': 26,
418
        'A': 1, 'C': 3, 'B': 2, 'E': 5, 'D': 4, 'G': 7, 'F': 6, 'I': 9, 'H': 8,
419 420 421
        'K': 11, 'J': 10, 'M': 13, 'L': 12, 'N': 14, 'P': 15,
        '_h_0': 22, '_h_1': 23, '_h4': 18, '_h5': 19, '_h6': 20, '_h7': 21,
        '_h2': 16, '_h3': 17,
422 423
    }

424
    # Check presence of all basic literals (no future ones with "`" counted)
425 426 427 428 429 430
    found_var_code_table = list(unfolder._CLUnfolder__var_code_table.items())
    print(found_var_code_table)
    for lit_name_val in expected_var_code_table.items():
        assert lit_name_val in found_var_code_table

    # var_code_table is twice as big as __var_list items
431
    # (future literals with "`" are added in found_var_code_table)
432 433 434
    assert len(found_var_code_table) == 2 * len(expected_var_code_table)

    ## Test frontiers, places, values and names
435
    # D E F G I L N
436
    print("Frontier values", unfolder.frontier_values)
437
    assert set(unfolder.frontier_values) == {4, 5, 6, 7, 9, 12, 14}
438 439 440 441 442 443 444 445 446 447 448 449 450 451 452

    frontiers_values_mapping = {
        value: unfolder.get_var_name(value) for value in unfolder.frontier_values
    }
    print("Frontiers values mapping", frontiers_values_mapping)
    assert frontiers_values_mapping == {4: 'D', 5: 'E', 6: 'F', 7: 'G', 9: 'I', 12: 'L', 14: 'N'}

    found = unfolder.frontiers_negative_values
    print("Frontiers negatives values", found)
    assert found == frozenset([-14, -12, -9, -7, -6, -5, -4])

    found = unfolder.frontiers_pos_and_neg
    assert found == frozenset([4, 5, 6, 7, 9, 12, 14, -14, -12, -9, -7, -6, -5, -4])

    # Check clocks
453
    free_clocks = unfolder.free_clocks
454 455 456 457
    print("Free clocks/events", free_clocks)
    assert free_clocks == frozenset([16, 17, 18, 19, 20, 21, 22, 23])

    clocks_values_mapping = {
458
        value: unfolder.get_var_name(value) for value in unfolder.free_clocks
459
    }
460
    print("Free clocks/events values mapping", clocks_values_mapping)
461 462 463 464 465 466
    assert clocks_values_mapping == {16: '_h2', 17: '_h3', 18: '_h4', 19: '_h5', 20: '_h6', 21: '_h7', 22: '_h_0', 23: '_h_1'}

    # Check input places
    assert unfolder._CLUnfolder__inputs == frozenset()

    # Not frontiers: A B C H J K M P
467
    found = unfolder.no_frontier_values
468
    print("Places that are not frontiers", found)
469
    assert found == {1, 2, 3, 8, 10, 11, 13, 15}
470 471


472
def test_init_forward_unfolding_solution_1_text(feed_mclanalyser, textual_properties):
473 474 475 476 477
    """
    Query:
        start, invariant, final: ("M", "L", "C")
        No solution (because inhibitor M is activated)
    """
478
    mcla = feed_mclanalyser
479 480

    ### Textual properties
481
    # "M", "L", "C"
482 483 484 485
    start, invariant, final = textual_properties[0]
    query = MCLSimpleQuery(start, invariant, final)
    mcla.unfolder.init_with_query(query)
    init_forward_unfolding_solution_1(mcla)
486 487 488 489 490

    ## Search solutions
    solutions = tuple(mcla.mac_search(query, 3))
    assert solutions == ()

491

492 493 494 495 496 497
def test_init_forward_unfolding_solution_1_dimacs(feed_mclanalyser, numeric_properties):
    """
    Query:
        dim_start, dim_inv, dim_final = [[13]], [[12]], [[3]]
        DIMACS equiv of: start, invariant, final: ("M", "L", "C"):
        No solution (because inhibitor M is activated)
498 499 500 501 502 503 504

    .. note:: Actuellement, pas de solution à cause de initial_constraints
        qui contient 2 clauses contraires: [-13] et [13].
        En effet, les valeurs DIMACS ne sont pas controlées contrairement aux
        propriétés textuelles. M en tant que start place n'est donc pas retiré
        de la liste des places non frontières (__no_frontier_init).
        Ex: [[-1], [-2], [-3], [-8], [-10], [-11], [-13], [-15], [13]]
505 506 507
    """
    mcla = feed_mclanalyser

508 509
    ### DIMACS properties
    query = MCLSimpleQuery(None, None, None)
510
    # [[13]], [[12]], [[3]]
511
    query.dim_start, query.dim_inv, query.dim_final = numeric_properties[0]
512
    mcla.unfolder.init_with_query(query)
513
    init_forward_unfolding_solution_1(mcla, dimacs_check=False)
514

515 516 517
    ## Search solutions
    solutions = tuple(mcla.mac_search(query, 3))
    assert solutions == ()
518

519 520 521 522 523 524 525
    ## Test without disabling initial_constraints check
    # Note: By reusing the unfolder here we bypass its locked status.
    # This will not be authorized with textual properties.
    # Exception is expected
    with pytest.raises(AssertionError, match=r".*At index 6 diff: \[-13\] != \[-15\].*"):
        init_forward_unfolding_solution_1(mcla)

526

527
def test_init_forward_unfolding_solution_2_text(feed_mclanalyser, textual_properties):
528 529 530 531 532
    """
    Query:
        start, invariant, final: ("", "L", "C and K")
        Solution: D E F I L
    """
533 534
    mcla = feed_mclanalyser

535 536 537 538 539 540 541
    ### Textual properties
    start, invariant, final = textual_properties[1]

    query = MCLSimpleQuery(start, invariant, final)
    mcla.unfolder.init_with_query(query)

    init_forward_unfolding_solution_2(mcla)
542 543 544 545 546 547 548

    ## Search solutions
    solutions = tuple(mcla.mac_search(query, 3))
    print("solutions:", solutions)
    assert len(solutions) == 1
    assert solutions[0].activated_frontier == {"I", "E", "D", "F", "L"}

549

550 551 552 553 554 555 556 557 558
def test_init_forward_unfolding_solution_2_dimacs(feed_mclanalyser, numeric_properties):
    """
    Query:
        dim_start, dim_inv, dim_final = [], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]
        DIMACS equiv of: start, invariant, final: ("", "L", "C and K")
        Solution: D E F I L
    """
    mcla = feed_mclanalyser

559 560 561
    ### DIMACS properties
    # "C and K" property requires an auxiliary literal which can only be added
    # from the textual version of this property.
VIGNET Pierre's avatar
VIGNET Pierre committed
562 563
    # Adding new literals in dimacs form is currently not allowed
    # (without the argument check_query=False of init_with_query).
564
    query = MCLSimpleQuery(None, None, None)
565 566 567 568 569 570
    query.dim_start, query.dim_inv, query.dim_final = numeric_properties[1]
    # Exception is expected
    with pytest.raises(ValueError, match=r".*47.*"):
        mcla.unfolder.init_with_query(query)
        # Never reach this point
        # init_forward_unfolding_solution_2(mcla)
571 572


573
def test_init_forward_unfolding_solution_3(feed_mclanalyser, textual_properties, numeric_properties):
574 575 576 577 578 579
    """
    Query:
        start, invariant, final: Union of textual and DIMACS properties:
            ("", "L", "C and K") => [], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]
            [[13]], [[12]], [[3]] <= ("M", "L", "C")
        No solution
580 581 582 583 584 585 586

    .. note:: Actuellement, pas de solution à cause de initial_constraints
        qui contient 2 clauses contraires: [-13] et [13].
        En effet, les valeurs DIMACS ne sont pas controlées contrairement aux
        propriétés textuelles. M en tant que start place n'est donc pas retiré
        de la liste des places non frontières (__no_frontier_init).
        Ex: [[-1], [-2], [-3], [-8], [-10], [-11], [-13], [-15], [13]]
587
    """
588 589 590 591
    mcla = feed_mclanalyser

    # Note: The second set creates auxiliary clauses that we could not insert
    # in DIMACS form in the query so we use the text form for it.
592
    # DIMACS data comes from the simple first numeric_properties ([[13]], [[12]], [[3]])
593 594 595 596
    query = MCLSimpleQuery(*textual_properties[1])
    query.dim_start, query.dim_inv, query.dim_final = numeric_properties[0]
    mcla.unfolder.init_with_query(query)

597
    init_forward_unfolding_solution_3(mcla, dimacs_check=False)
598

599 600 601
    ## Search solutions
    solutions = tuple(mcla.mac_search(query, 3))
    assert solutions == ()
602

603 604 605 606 607 608
    ## Test without disabling initial_constraints check
    mcla.unfolder.init_with_query(query)
    # Exception is expected
    with pytest.raises(AssertionError, match=r".*At index 6 diff: \[-13\] != \[-15\].*"):
        init_forward_unfolding_solution_3(mcla)

609

610 611 612 613 614 615
def test_init_forward_unfolding_solution_4(feed_mclanalyser, textual_properties):
    """
    Query:
        start, invariant, final: ("", "", "C")
        Solutions: D E F L, D E F I
    """
616 617 618 619 620 621 622 623 624
    mcla = feed_mclanalyser

    # Note: The second set creates auxiliary clauses that we could not insert
    # in DIMACS form in the query so we use the text form for it.
    query = MCLSimpleQuery(*textual_properties[2])
    mcla.unfolder.init_with_query(query)

    init_forward_unfolding_solution_4(mcla)

625 626 627 628 629 630 631 632
    ## Search solutions
    solutions = set(mcla.mac_search(query, 3))
    print("solutions:", solutions)
    assert len(solutions) == 2
    found = {solution.activated_frontier for solution in solutions}
    expected = {frozenset(["D", "E", "F", "L"]), frozenset(["D", "E", "F", "I"])}
    assert found == expected

633

634
def init_forward_unfolding_solution_1(mcla, dimacs_check=True):
635 636 637 638
    """
    - Test first part of init_forward_unfolding: init of constraints
    - Test second part of init_forward_unfolding: shift of initialized constraints

639 640 641
    Query:
        start, invariant, final: ("M", "L", "C")
        No solution (because inhibitor M is activated)
642 643 644 645 646 647 648

    :key dimacs_check: (Optional) Boolean used to check expected initial
        constraints. For now, only literals in textual properties are removed
        from the CLUnfolder __no_frontier_init variable. DIMACS literals are
        not filtered and could lead to falsely unsatisfactory problems.

        .. seealso:: :meth:`test_init_forward_unfolding_solution_1_dimacs`
649
    """
650
    unfolder = mcla.unfolder
651

652 653 654
    ## Init constraints ########################################################

    init_forward_unfolding_part_1(mcla.unfolder)
655

656 657 658 659 660
    print("dynamic_constraints:", unfolder.dynamic_constraints)
    print("initial_constraints:", unfolder.initial_constraints)
    print("invariant_constraints:", unfolder.invariant_constraints)
    print("variant_constraints:", unfolder.variant_constraints)
    print("final_constraints:", unfolder.final_constraints)
661 662 663 664 665

    # No auxiliary variables
    assert unfolder._CLUnfolder__aux_code_table == dict()
    assert unfolder._CLUnfolder__aux_list == []

666
    # MCLA could be reused, so __dynamic_constraints could not be empty here
667 668 669 670 671
    # artificial reset
    # unfolder._CLUnfolder__dynamic_constraints = []
    # assert unfolder.dynamic_constraints == []

    # no frontiers + M (start place)
672 673 674 675
    if dimacs_check:
        expected_initial_constraints = [[-1], [-2], [-3], [-8], [-10], [-11], [-15], [13]]
        assert unfolder.initial_constraints == expected_initial_constraints
    expected_initial_constraints = unfolder.initial_constraints
676 677 678 679 680 681 682 683 684 685

    # L
    assert unfolder.invariant_constraints == [[[12]]]

    # No variant constraint
    assert unfolder.variant_constraints == []

    # C
    assert unfolder.final_constraints == [[3]]

686
    ## Shift constraints #######################################################
687 688 689

    init_forward_unfolding_part_2(unfolder)

690 691 692
    print("dynamic_constraints:", unfolder.dynamic_constraints)
    print("invariant_constraints:", unfolder.invariant_constraints)
    print("final_constraints:", unfolder.final_constraints)
693

694
    # Shift of the system clauses and auxiliary clauses is made now.
695
    expected = [
696
        # [_lit0, _h2] [_lit0, D] [_h2, D, _lit0] [P, _lit5] [L, _lit5] [P, L, _lit5]
697
        [[-24, 16], [-24, 4], [-16, -4, 24], [-15, 42], [-12, 42], [15, 12, -42],
698
        # [_lit5, _lit4] [K, _lit4] [_lit5, K, _lit4] [B, _lit3] [_lit4, _lit3] [B, _lit4, _lit3]
699
        [-42, 41], [-11, 41], [42, 11, -41], [2, -40], [41, -40], [-2, -41, 40],
700
        # [_lit3, _lit2] [M, _lit2] [_lit3, M, _lit2] [A, _lit1] [_lit2, _lit1] [A, _lit2, _lit1]
701
        [40, -36], [-13, -36], [-40, 13, 36], [1, -25], [36, -25], [-1, -36, 25],
702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720
        # [_lit6, _h_0] [_lit6, _lit1] [_h_0, _lit1, _lit6]
        [-43, 22], [-43, 25], [-22, -25, 43],
        # [A, _lit0, A] [A, _lit0, _lit6] [A, _lit0] [A, A, _lit6]
        [-47, 24, 1], [-47, 24, -43], [47, -24], [47, -1, 43],
        # [E, _lit7] [F, _lit7] [E, F, _lit7] [_lit8, _h3] [_lit8, _lit7] [_h3, _lit7, _lit8]
        [5, -44], [6, -44], [-5, -6, 44], [-45, 17], [-45, 44], [-17, -44, 45],
        # [A, _lit11] [_lit4, _lit11] [A, _lit4, _lit11] [_lit11, _lit10] [M, _lit10] [_lit11, M, _lit10]
        [1, -27], [41, -27], [-1, -41, 27], [27, -26], [-13, -26], [-27, 13, 26],
        # [B, _lit9] [_lit10, _lit9] [B, _lit10, _lit9] [_lit14, _h_0] [_lit14, _lit9] [_h_0, _lit9, _lit14]
        [2, -46], [26, -46], [-2, -26, 46], [-30, 22], [-30, 46], [-22, -46, 30],
        # [B, _lit8, B] [B, _lit8, _lit14] [B, _lit8] [B, B, _lit14]
        [-48, 45, 2], [-48, 45, -30], [48, -45], [48, -2, 30],
        # [_lit15, _lit14] [_lit15, _lit6] [_lit14, _lit6, _lit15] [C, _lit15, C] [C, _lit15] [C, C]
        [31, -30], [31, -43], [30, 43, -31], [-49, 31, 3], [49, -31], [49, -3],
        # [D, D] [D, _lit0] [D, D, _lit0] [E, E] [E, _lit8] [E, E, _lit8]
        [-50, 4], [-50, -24], [50, -4, 24], [-51, 5], [-51, -45], [51, -5, 45],
        # [F, F] [F, F] [_lit16, _h7] [_lit16, G] [_h7, G, _lit16]
        [-52, 6], [52, -6], [-32, 21], [-32, 7], [-21, -7, 32],
        # [G, G] [G, _lit16] [G, G, _lit16] [H, _lit16, H] [H, _lit16] [H, H]
721
        [-53, 7], [-53, -32], [53, -7, 32], [-54, 32, 8], [54, -32], [54, -8],
722
        # [_lit17, _h6] [_lit17, K] [_h6, K, _lit17] [_lit18, _h4] [_lit18, I] [_h4, I, _lit18]
723
        [-33, 20], [-33, 11], [-20, -11, 33], [-34, 18], [-34, 9], [-18, -9, 34],
724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742
        # [I, _lit17, I] [I, _lit17, _lit18] [I, _lit17] [I, I, _lit18]
        [-55, 33, 9], [-55, 33, -34], [55, -33], [55, -9, 34],
        # [_lit19, _h5] [_lit19, J] [_h5, J, _lit19]
        [-35, 19], [-35, 10], [-19, -10, 35],
        # [J, _lit18, J] [J, _lit18, _lit19] [J, _lit18] [J, J, _lit19]
        [-56, 34, 10], [-56, 34, -35], [56, -34], [56, -10, 35],
        # [K, _lit19, K] [K, _lit19, _lit17] [K, _lit19] [K, K, _lit17]
        [-57, 35, 11], [-57, 35, -33], [57, -35], [57, -11, 33],
        # [L, L] [L, L] [_lit20, _h_1] [_lit20, N] [_h_1, N, _lit20]
        [-58, 12], [58, -12], [-37, 23], [-37, 14], [-23, -14, 37],
        # [_lit21, _h_1] [_lit21, N] [_h_1, N, _lit21] [_lit22, _lit20] [_lit22, _lit21] [_lit20, _lit21, _lit22]
        [-38, 23], [-38, 14], [-23, -14, 38], [39, -37], [39, -38], [37, 38, -39],
        # [N, N] [N, _lit22] [N, N, _lit22] [M, _lit20, M] [M, _lit20] [M, M]
        [-60, 14], [-60, -39], [60, -14, 39], [-59, 37, 13], [59, -37], [59, -13],
        # [P, _lit21, P] [P, _lit21] [P, P]
        [-61, 38, 15], [61, -38], [61, -15],
        # [_h4, I] [_h5, J] [_h6, K] [_h7, G] [_h2, D] [_h3, E]
        [-18, 9], [-19, 10], [-20, 11], [-21, 7], [-16, 4], [-17, 5],
        # [_h_0, A, B] [_h_1, N, N]
743 744
        [-22, 1, 2], [-23, 14, 14]]]

745 746 747 748
    # No changes
    assert unfolder.initial_constraints == expected_initial_constraints

    # Crap dynamic_constraints test
749 750
    assert unfolder.dynamic_constraints == expected

751
    # L : 12 + 46 = 58
752 753 754 755 756
    assert unfolder.invariant_constraints == [[[12]], [[58]]]

    # No variant constraint (not shifted in second part of init_forward_unfolding)
    assert unfolder.variant_constraints == []

757
    # C : 3 + 46 = 49
758 759 760 761 762 763 764 765
    assert unfolder.final_constraints == [[49]]


def init_forward_unfolding_solution_2(mcla):
    """
    - Test first part of init_forward_unfolding: init of constraints
    - Test second part of init_forward_unfolding: shift of initialized constraints

766 767
    Query:
        start, invariant, final: ("", "L", "C and K")
768
        Solution: D E F I L
769
    """
770 771 772
    unfolder = mcla.unfolder

    ## Init constraints ########################################################
773

774
    init_forward_unfolding_part_1(mcla.unfolder)
775

776 777 778 779 780
    print("dynamic_constraints:", unfolder.dynamic_constraints)
    print("initial_constraints:", unfolder.initial_constraints)
    print("invariant_constraints:", unfolder.invariant_constraints)
    print("variant_constraints:", unfolder.variant_constraints)
    print("final_constraints:", unfolder.final_constraints)
781

782
    # Auxiliary variables: "C and K" property is added
783 784 785
    assert unfolder._CLUnfolder__aux_code_table == {'_lit47': 47}
    assert unfolder._CLUnfolder__aux_list == ['_lit47']

786
    # MCLA could be reused, so __dynamic_constraints could not be empty here
787 788 789 790 791
    # artificial reset
    # unfolder._CLUnfolder__dynamic_constraints = []
    # assert unfolder.dynamic_constraints == []

    # no frontiers + nothing (no start place)
792 793
    expected_initial_constraints = [[-1], [-2], [-3], [-8], [-10], [-11], [-13], [-15]]
    assert unfolder.initial_constraints == expected_initial_constraints
794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815

    # L
    assert unfolder.invariant_constraints == [[[12]]]

    # No variant constraint
    assert unfolder.variant_constraints == []

    # "C and K" = _lit47
    # C, not _lit47
    # K, not _lit47
    # not C, not K, _lit47
    # _lit47
    assert unfolder.final_constraints == [[3, -47], [11, -47], [-3, -11, 47], [47]]

    # PS:
    # "C or K" = _lit47
    # not C, _lit47
    # not K, _lit47
    # C, K, not _lit47
    # _lit47
    #[[-3, 47], [-11, 47], [3, 11, -47], [47]]

816
    ## Shift constraints #######################################################
817 818 819

    init_forward_unfolding_part_2(unfolder)

820 821 822 823
    print("dynamic_constraints:", unfolder.dynamic_constraints)
    print("initial_constraints:", unfolder.initial_constraints)
    print("invariant_constraints:", unfolder.invariant_constraints)
    print("final_constraints:", unfolder.final_constraints)
824 825

    # Shift of the system clauses (and syst aux clauses)
826 827 828
    # System variables: max id is 46
    # Max value in the initial constraints: 47
    # => This last one is an auxiliary variable
829
    assert unfolder.get_var_number() == 46
830
    assert unfolder.shift_step == 47
831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853
    expected = [
        [[-24, 16], [-24, 4], [-16, -4, 24], [-15, 42], [-12, 42], [15, 12, -42],
        [-42, 41], [-11, 41], [42, 11, -41], [2, -40], [41, -40], [-2, -41, 40],
        [40, -36], [-13, -36], [-40, 13, 36], [1, -25], [36, -25], [-1, -36, 25],
        [-43, 22], [-43, 25], [-22, -25, 43], [-48, 24, 1], [-48, 24, -43],
        [48, -24], [48, -1, 43], [5, -44], [6, -44], [-5, -6, 44], [-45, 17],
        [-45, 44], [-17, -44, 45], [1, -27], [41, -27], [-1, -41, 27], [27, -26],
        [-13, -26], [-27, 13, 26], [2, -46], [26, -46], [-2, -26, 46], [-30, 22],
        [-30, 46], [-22, -46, 30], [-49, 45, 2], [-49, 45, -30], [49, -45],
        [49, -2, 30], [31, -30], [31, -43], [30, 43, -31], [-50, 31, 3], [50, -31],
        [50, -3], [-51, 4], [-51, -24], [51, -4, 24], [-52, 5], [-52, -45],
        [52, -5, 45], [-53, 6], [53, -6], [-32, 21], [-32, 7], [-21, -7, 32],
        [-54, 7], [-54, -32], [54, -7, 32], [-55, 32, 8], [55, -32], [55, -8],
        [-33, 20], [-33, 11], [-20, -11, 33], [-34, 18], [-34, 9], [-18, -9, 34],
        [-56, 33, 9], [-56, 33, -34], [56, -33], [56, -9, 34], [-35, 19], [-35, 10],
        [-19, -10, 35], [-57, 34, 10], [-57, 34, -35], [57, -34], [57, -10, 35],
        [-58, 35, 11], [-58, 35, -33], [58, -35], [58, -11, 33], [-59, 12],
        [59, -12], [-37, 23], [-37, 14], [-23, -14, 37], [-38, 23], [-38, 14],
        [-23, -14, 38], [39, -37], [39, -38], [37, 38, -39], [-61, 14], [-61, -39],
        [61, -14, 39], [-60, 37, 13], [60, -37], [60, -13], [-62, 38, 15],
        [62, -38], [62, -15], [-18, 9], [-19, 10], [-20, 11], [-21, 7], [-16, 4],
        [-17, 5], [-22, 1, 2], [-23, 14, 14]]]

854 855 856 857
    # No changes
    assert unfolder.initial_constraints == expected_initial_constraints

    # Crap dynamic_constraints test
858 859
    assert unfolder.dynamic_constraints == expected

860
    # L : 12 + shift_step (47) = 59
861 862 863 864 865 866 867 868 869 870
    assert unfolder.invariant_constraints == [[[12]], [[59]]]

    # No variant constraint (not shifted in second part of init_forward_unfolding)
    assert unfolder.variant_constraints == []

    # "C and K" = _lit47 = 47
    # Shift: [[3, -47], [11, -47], [-3, -11, 47], [47]] with shift_step (47)
    assert unfolder.final_constraints == [[50, -94], [58, -94], [-50, -58, 94], [94]]


871
def init_forward_unfolding_solution_3(mcla, dimacs_check=True):
872 873 874 875 876 877 878 879 880
    """
    - Test first part of init_forward_unfolding: init of constraints
    - Test second part of init_forward_unfolding: shift of initialized constraints

    Query:
        start, invariant, final: Union of textual and DIMACS properties:
            ("", "L", "C and K") => [], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]
            [[13]], [[12]], [[3]] <= ("M", "L", "C")
        No solution
881 882 883 884 885 886 887

    .. todo:: This test contains some stupid results from the generator of
        clauses.

        => clauses redondantes en cas d'égalité des events entre l'attribut
        au format texte et celui au format DIMACS.
        (invariant_constraints)
888 889 890 891 892 893 894

    :key dimacs_check: (Optional) Boolean used to check expected initial
        constraints. For now, only literals in textual properties are removed
        from the CLUnfolder __no_frontier_init variable. DIMACS literals are
        not filtered and could lead to falsely unsatisfactory problems.

        .. seealso:: :meth:`test_init_forward_unfolding_solution_3`
895 896 897 898 899 900 901
    """
    unfolder = mcla.unfolder

    ## Init constraints ########################################################

    init_forward_unfolding_part_1(mcla.unfolder)

902 903 904 905
    print("dynamic_constraints:", unfolder.dynamic_constraints)
    print("initial_constraints:", unfolder.initial_constraints)
    print("invariant_constraints:", unfolder.invariant_constraints)
    print("final_constraints:", unfolder.final_constraints)
906 907 908 909

    assert unfolder.shift_step == 47

    # no frontiers + "M" (start place)
910 911 912 913
    if dimacs_check:
        expected_initial_constraints = [[-1], [-2], [-3], [-8], [-10], [-11], [-15], [13]]
        assert unfolder.initial_constraints == expected_initial_constraints
    expected_initial_constraints = unfolder.initial_constraints
914 915

    # Just append DIMACS constraints of the query: "L" + [[12]]
916
    assert unfolder.invariant_constraints == [[[12], [12]]]
917 918 919
    # Idem: "C and K" + "C" = [3, -47], [11, -47], [-3, -11, 47], [47] + [3]
    assert unfolder.final_constraints == [[3, -47], [11, -47], [-3, -11, 47], [47], [3]]

920 921 922 923 924 925 926 927 928 929 930 931 932
    ## Shift constraints #######################################################

    init_forward_unfolding_part_2(unfolder)

    print("initial_constraints:", unfolder.initial_constraints)
    print("invariant_constraints:", unfolder.invariant_constraints)
    print("final_constraints:", unfolder.final_constraints)

    # Shift values by adding 47
    assert unfolder.invariant_constraints == [[[12], [12]], [[59], [59]]]

    assert unfolder.final_constraints == [[50, -94], [58, -94], [-50, -58, 94], [94], [50]]

933

934 935 936 937 938 939 940
def init_forward_unfolding_solution_4(mcla):
    """
    - Test first part of init_forward_unfolding: init of constraints
    - Test second part of init_forward_unfolding: shift of initialized constraints

    Query:
        start, invariant, final: ("", "", "C")
941
        Solutions: F E L D, D E F I
942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011
    """
    unfolder = mcla.unfolder

    ## Init constraints ########################################################

    # __no_frontier_init not already initialized
    # (initial_constraints and invariant_constraints must be initialized beforehand)
    assert unfolder._CLUnfolder__no_frontier_init == []

    init_forward_unfolding_part_1(mcla.unfolder)

    print("initial_constraints:", unfolder.initial_constraints)
    print("final_constraints:", unfolder.final_constraints)

    assert unfolder.shift_step == 46

    expected_initial_constraints = [[-1], [-2], [-3], [-8], [-10], [-11], [-13], [-15]]
    assert unfolder._CLUnfolder__no_frontier_init == expected_initial_constraints
    assert unfolder.initial_constraints == expected_initial_constraints

    ## Shift constraints #######################################################

    init_forward_unfolding_part_2(unfolder)

    print("initial_constraints:", unfolder.initial_constraints)
    print("final_constraints:", unfolder.final_constraints)

    assert unfolder.final_constraints == [[49]]


def test_init_forward_unfolding_variant_constraints(feed_mclanalyser):
    """Test variant_prop and dim_variant attributes of a query

    .. todo:: This test contains some stupid results from the generator of
        clauses.

        => clauses redondantes en cas d'égalité des events dans 1 formule
        (Ex: "h2 and h2")

        => clauses redondantes en cas d'égalité des events entre l'attribut
        au format texte et celui au format DIMACS.

        => On peut mettre n'importe quel nom d'event, aucun test n'est fait
        pour vérifier qu'il existe dans le modèle.
    """

    mcla = feed_mclanalyser
    unfolder = mcla.unfolder

    # Test values of events
    print(mcla.unfolder._CLUnfolder__var_code_table)

    h2_value = mcla.unfolder.var_dimacs_code("_h2")
    assert h2_value == 16

    h3_value = mcla.unfolder.var_dimacs_code("_h3")
    assert h3_value == 17

    h0_value = mcla.unfolder.var_dimacs_code("_h_0")
    assert h0_value == 22

    query = MCLSimpleQuery(None, None, None)
    query.variant_prop = ["_h2", "_h_0"]

    unfolder.init_with_query(query)
    unfolder.init_forward_unfolding()

    # Check copy of query attribute
    assert unfolder._CLUnfolder__variant_property == query.variant_prop

1012
    # Check conversion of query attribute into literals
1013 1014 1015 1016
    expected = [[[16]], [[22]]]
    assert unfolder._CLUnfolder__precomputed_variant_constraints == expected

    # Check merge of 2 equivalent attributes
1017
    # text ("_h2", "_h_0") + dimacs ([[[16]], [[22]]])
1018 1019 1020 1021 1022 1023 1024 1025
    # TODO: => stupid result
    query.dim_variant = [[[16]], [[22]]]
    unfolder.init_with_query(query)
    unfolder.init_forward_unfolding()

    expected = [[[16], [16]], [[22], [22]]]
    assert unfolder._CLUnfolder__precomputed_variant_constraints == expected

1026
    # Check merge of 2 different attributes (size is different)
1027 1028
    query.dim_variant = [[[16]], [[22]], []]
    unfolder.init_with_query(query)
1029
    # Exception is expected (must be the same size)
1030 1031 1032 1033 1034
    with pytest.raises(MCLException, match=r".*Incoherent variant properties.*"):
        unfolder.init_forward_unfolding()

    ##
    # Check the input of unknown DIMACS literals
1035
    # See the absence of check_query=False argument of init_with_query()
1036 1037 1038 1039 1040 1041 1042
    query.variant_prop = None
    query.dim_variant = [[[16, -47], [17, -47], [-16, -17, 47], [47]], [[22]]]
    # With check_query enabled
    with pytest.raises(ValueError, match=r".*47.*"):
        unfolder.init_with_query(query)

    # With check_query disabled
1043
    # => this causes an incorrect initialization but without error
1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080
    unfolder.init_with_query(query, check_query=False)
    unfolder.init_forward_unfolding()

    ##
    ## aucun test sur les noms des events
    # TODO: => stupid result
    query.variant_prop = ["PoUeT"]
    query.dim_variant = None
    mcla.unfolder.init_with_query(query)
    mcla.unfolder.init_forward_unfolding()
    # => no problem

    ## formule ici a priori difficile à parser...
    ## clauses fonctionnelles mais ineptes...
    # TODO: => stupid result
    query.variant_prop = ["_h2", "_h2 and _h2"]
    query.dim_variant = None
    mcla.unfolder.init_with_query(query)
    mcla.unfolder.init_forward_unfolding()

    expected = [[[16]], [[16, -47], [16, -47], [-16, -16, 47], [47]]]
    assert unfolder._CLUnfolder__precomputed_variant_constraints == expected
    assert unfolder.shift_step == 47

    ##
    # Check the compilation of a complex textual trajectory (a real solution)
    query.variant_prop = ["_h2 and _h3", "_h_0"]
    query.dim_variant = None
    unfolder.init_with_query(query)
    unfolder.init_forward_unfolding()

    expected = [[[16, -47], [17, -47], [-16, -17, 47], [47]], [[22]]]
    assert unfolder._CLUnfolder__precomputed_variant_constraints == expected
    # Creation of the auxiliary variable: 47
    print(unfolder._CLUnfolder__aux_list)
    print(unfolder._CLUnfolder__aux_code_table)
    # It is important to test this, because an auxiliary variable was previously