TestCLUnfolder.py 50.5 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


class ErrorReporter(object):
    """error reporter of the compil type"""
VIGNET Pierre's avatar
VIGNET Pierre committed
100

101 102 103 104 105 106 107 108 109 110
    def __init__(self):
        self.context = ""
        self.error = False
        pass

    def display(self, mess):
        """
        just printing
        """
        self.error = True
VIGNET Pierre's avatar
VIGNET Pierre committed
111
        print("\n>> " + self.context + "  " + mess)
112 113 114 115 116

    def display_info(self, mess):
        """
        just printing
        """
VIGNET Pierre's avatar
VIGNET Pierre committed
117
        print("\n-- " + mess)
118 119 120 121 122 123 124

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

VIGNET Pierre's avatar
VIGNET Pierre committed
125

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

VIGNET Pierre's avatar
VIGNET Pierre committed
138

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

VIGNET Pierre's avatar
VIGNET Pierre committed
154

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

VIGNET Pierre's avatar
VIGNET Pierre committed
167

VIGNET Pierre's avatar
VIGNET Pierre committed
168 169
def model4():
    """
170 171 172 173 174
    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
175 176 177
    """
    model = ChartModel("Test")
    root = model.get_root()
VIGNET Pierre's avatar
VIGNET Pierre committed
178 179
    node_1 = root.add_simple_node("n1", 0, 0)
    node_2 = root.add_simple_node("n2", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
180
    tr0 = root.add_transition(node_1, node_2)
VIGNET Pierre's avatar
VIGNET Pierre committed
181
    tr0.set_event("hh1")
VIGNET Pierre's avatar
VIGNET Pierre committed
182
    tr0.set_condition("n3 or n4")
VIGNET Pierre's avatar
VIGNET Pierre committed
183 184
    node_3 = root.add_simple_node("n3", 0, 0)
    node_4 = root.add_simple_node("n4", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
185
    root.add_transition(node_3, node_4)
VIGNET Pierre's avatar
VIGNET Pierre committed
186
    node_5 = root.add_simple_node("n5", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
187
    tr1 = root.add_transition(node_4, node_5)
188
    root.add_transition(node_5, node_3)
VIGNET Pierre's avatar
VIGNET Pierre committed
189 190
    tr1.set_event("hh2")
    tr1.set_condition("n1 and n3")
VIGNET Pierre's avatar
VIGNET Pierre committed
191
    node_i = root.add_input_node("in1", 0, 0)
VIGNET Pierre's avatar
VIGNET Pierre committed
192 193
    tri = root.add_transition(node_i, node_1)
    tri.set_condition("n5")
194 195 196

    # 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.
VIGNET Pierre's avatar
VIGNET Pierre committed
197 198
    # node_s = root.add_start_node('s1', 0, 0)
    # root.add_transition(node_s, node_3)
199

VIGNET Pierre's avatar
VIGNET Pierre committed
200 201
    return model

VIGNET Pierre's avatar
VIGNET Pierre committed
202

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

VIGNET Pierre's avatar
VIGNET Pierre committed
214

215 216
@pytest.fixture()
def textual_properties():
VIGNET Pierre's avatar
VIGNET Pierre committed
217
    """start, invariant, final properties in textual form"""
218
    return (
VIGNET Pierre's avatar
VIGNET Pierre committed
219 220 221
        ("M", "L", "C"),  # No solution (because inhibitor M is activated)
        ("", "L", "C and K"),  # Solution: D E F I L
        ("", "", "C"),  # Solutions: F E L D, D E F I
222 223
    )

VIGNET Pierre's avatar
VIGNET Pierre committed
224

225
@pytest.fixture()
226
def numeric_properties():
VIGNET Pierre's avatar
VIGNET Pierre committed
227
    """start, invariant, final properties in DIMACS form"""
228
    return (
229
        # "M", "L", "C"
230
        ([[13]], [[12]], [[3]]),
231
        # "", "L", "C and K"
232 233 234
        ([], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]),
    )

VIGNET Pierre's avatar
VIGNET Pierre committed
235

236 237
@pytest.fixture()
def feed_mclanalyser():
238 239 240 241 242 243 244
    """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

    """
245
    rep = ErrorReporter()
246
    # debug: Force __var_list to be sorted at the output of base_var_set from
247 248 249 250 251 252 253 254
    # 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
255

VIGNET Pierre's avatar
VIGNET Pierre committed
256 257 258 259 260

class TestCLUnfolder(unittest.TestCase):
    """
    Test public and some private methods (test_method form)
    """
VIGNET Pierre's avatar
VIGNET Pierre committed
261

VIGNET Pierre's avatar
VIGNET Pierre committed
262 263
    def test_var_name(self):
        """
264
        Test of variables at initial state uncoding and decoding
VIGNET Pierre's avatar
VIGNET Pierre committed
265 266 267
        """
        model = model1()
        unfolder = create_unfolder(model)
268 269 270 271 272 273

        # 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
274
        # naming and coding variables
VIGNET Pierre's avatar
VIGNET Pierre committed
275 276
        cn1 = unfolder.var_dimacs_code("n1")
        cn2 = unfolder.var_dimacs_code("n2")
277

VIGNET Pierre's avatar
VIGNET Pierre committed
278 279 280
        res = unfolder.get_var_name(cn1) == "n1"
        res = res and (unfolder.get_var_name(cn2) == "n2")
        self.assert_(res, "Error in variable name 1")
281

VIGNET Pierre's avatar
VIGNET Pierre committed
282 283 284 285
        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")
286

VIGNET Pierre's avatar
VIGNET Pierre committed
287 288 289 290
        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")
291

292 293
        # Test number of variables
        assert unfolder.get_system_var_number() == unfolder.get_var_number()
294

VIGNET Pierre's avatar
VIGNET Pierre committed
295 296 297 298
    def test_frontier(self):
        """
        Test frontier computation and encoding
        """
299
        ## model1
VIGNET Pierre's avatar
VIGNET Pierre committed
300 301 302
        model = model1()
        unfolder = create_unfolder(model)
        # test frontier: should be n1
303
        frontier_value = unfolder.frontier_values[0]
VIGNET Pierre's avatar
VIGNET Pierre committed
304
        res = unfolder.get_var_name(frontier_value) == "n1"
305
        res = res and (len(unfolder.frontier_values) == 1)
VIGNET Pierre's avatar
VIGNET Pierre committed
306
        self.assert_(res, "Error in frontier: model1")
307

308
        ## model2 (one cycle without start)
VIGNET Pierre's avatar
VIGNET Pierre committed
309 310
        model = model2()
        unfolder = create_unfolder(model)
311

VIGNET Pierre's avatar
VIGNET Pierre committed
312
        # test frontier: should be n1
313
        frontier_value = unfolder.frontier_values[0]
VIGNET Pierre's avatar
VIGNET Pierre committed
314
        res = unfolder.get_var_name(frontier_value) == "n1"
315
        res = res and (len(unfolder.frontier_values) == 1)
VIGNET Pierre's avatar
VIGNET Pierre committed
316
        self.assert_(res, "Error in frontier: model2")
VIGNET Pierre's avatar
VIGNET Pierre committed
317

318
        ## model3: same as model2 but with a start on n3
VIGNET Pierre's avatar
VIGNET Pierre committed
319 320
        model = model3()
        unfolder = create_unfolder(model)
321

VIGNET Pierre's avatar
VIGNET Pierre committed
322
        # test frontier - should be {n1, n3}
323 324
        frontier_values = unfolder.frontier_values
        res = len(frontier_values) == 2
VIGNET Pierre's avatar
VIGNET Pierre committed
325 326 327
        res = res and unfolder.get_var_name(frontier_values[0]) == "n1"
        res = res and unfolder.get_var_name(frontier_values[1]) == "n3"
        self.assert_(res, "Error in frontier: model3")
328

329
        ## model4 - No frontiers (even if we can get input node in1 in the solutions)
VIGNET Pierre's avatar
VIGNET Pierre committed
330 331
        model = model4()
        unfolder = create_unfolder(model)
332
        res = len(unfolder.frontier_values) == 0
VIGNET Pierre's avatar
VIGNET Pierre committed
333
        self.assert_(res, "Error in frontier: model4")
334

VIGNET Pierre's avatar
VIGNET Pierre committed
335 336 337 338 339 340 341
    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)
342
        lfc = unfolder.free_clocks
VIGNET Pierre's avatar
VIGNET Pierre committed
343
        self.assertEqual(len(lfc), 0, "Error in free clocks: model3")
344
        lin = unfolder.inputs
VIGNET Pierre's avatar
VIGNET Pierre committed
345
        self.assertEqual(len(lin), 0, "Error in inputs 1")
346

VIGNET Pierre's avatar
VIGNET Pierre committed
347 348 349
        # model4: two free clocks and one input
        model = model4()
        unfolder = create_unfolder(model)
350
        lfc = unfolder.free_clocks
VIGNET Pierre's avatar
VIGNET Pierre committed
351
        self.assertEqual(len(lfc), 2, "Error in free clocks: model4")
352
        found_names = {unfolder.get_var_name(clock) for clock in lfc}
353
        self.assertEqual(
VIGNET Pierre's avatar
VIGNET Pierre committed
354
            found_names, {"hh2", "hh1"}, "Error in free clocks names: model4"
355
        )
356
        lin = unfolder.inputs
VIGNET Pierre's avatar
VIGNET Pierre committed
357
        self.assertEqual(len(lin), 1, "Error in inputs: model4")
358
        found_names = {unfolder.get_var_name(inpt) for inpt in lin}
VIGNET Pierre's avatar
VIGNET Pierre committed
359
        self.assertEqual(found_names, {"in1"}, "Error in inputs names: model4")
360 361


362 363 364
def init_forward_unfolding_part_1(unfolder):
    """Initialization step only"""

VIGNET Pierre's avatar
VIGNET Pierre committed
365
    unfolder._CLUnfolder__shift_direction = "FORWARD"
366 367
    unfolder._CLUnfolder__current_step = 1
    unfolder._CLUnfolder__shift_step = unfolder.shift_step_init  # back to basic!
VIGNET Pierre's avatar
VIGNET Pierre committed
368 369
    unfolder._CLUnfolder__aux_code_table = dict()  # flush auxiliary variables
    unfolder._CLUnfolder__aux_list = []  # idem
370 371 372 373 374 375

    # 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()
376 377 378
    # Should be after init_initial and init_invariant
    unfolder._CLUnfolder__prune_initial_no_frontier_constraint_0()

379 380 381 382 383 384 385 386 387 388

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.

VIGNET Pierre's avatar
VIGNET Pierre committed
389

390 391 392
def test_init_unfolder(feed_mclanalyser):

    mcla = feed_mclanalyser
VIGNET Pierre's avatar
VIGNET Pierre committed
393
    unfolder = mcla.unfolder  # shortcut
394 395 396 397 398 399 400

    # Initialization step only
    init_forward_unfolding_part_1(mcla.unfolder)

    ## Test CLDynSys
    # 15 places
    assert unfolder.get_var_number() == 46
401
    assert unfolder.shift_step_init == 46
402 403 404

    # __var_list is built on casted set; MCLAnalyser is un debug mode
    # so the list is sorted
405
    # 47 elems but max id for literals is 46
406 407 408 409 410 411 412 413 414 415 416 417 418 419
    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 = {
420
        '_lit22': 39, '_lit20': 37, '_lit21': 38, '_lit19': 35, '_lit15': 31,
421
        '_lit18': 34, '_lit6': 43, '_lit17': 33, '_lit13': 29, '_lit9': 46,
422 423 424
        '_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,
425
        'A': 1, 'C': 3, 'B': 2, 'E': 5, 'D': 4, 'G': 7, 'F': 6, 'I': 9, 'H': 8,
426 427 428
        '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,
429 430
    }

431
    # Check presence of all basic literals (no future ones with "`" counted)
432 433 434 435 436 437
    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
438
    # (future literals with "`" are added in found_var_code_table)
439 440 441
    assert len(found_var_code_table) == 2 * len(expected_var_code_table)

    ## Test frontiers, places, values and names
442
    # D E F G I L N
443
    print("Frontier values", unfolder.frontier_values)
444
    assert set(unfolder.frontier_values) == {4, 5, 6, 7, 9, 12, 14}
445 446 447 448 449 450 451 452 453 454 455 456 457 458 459

    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
460
    free_clocks = unfolder.free_clocks
461 462 463 464
    print("Free clocks/events", free_clocks)
    assert free_clocks == frozenset([16, 17, 18, 19, 20, 21, 22, 23])

    clocks_values_mapping = {
465
        value: unfolder.get_var_name(value) for value in unfolder.free_clocks
466
    }
467
    print("Free clocks/events values mapping", clocks_values_mapping)
VIGNET Pierre's avatar
VIGNET Pierre committed
468 469 470 471 472 473 474 475 476 477
    assert clocks_values_mapping == {
        16: "_h2",
        17: "_h3",
        18: "_h4",
        19: "_h5",
        20: "_h6",
        21: "_h7",
        22: "_h_0",
        23: "_h_1",
    }
478 479 480 481 482

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

    # Not frontiers: A B C H J K M P
483
    found = unfolder.no_frontier_values
484
    print("Places that are not frontiers", found)
485
    assert found == {1, 2, 3, 8, 10, 11, 13, 15}
486 487


488
def test_init_forward_unfolding_solution_1_text(feed_mclanalyser, textual_properties):
489 490 491 492 493
    """
    Query:
        start, invariant, final: ("M", "L", "C")
        No solution (because inhibitor M is activated)
    """
494
    mcla = feed_mclanalyser
495 496

    ### Textual properties
497
    # "M", "L", "C"
498 499 500 501
    start, invariant, final = textual_properties[0]
    query = MCLSimpleQuery(start, invariant, final)
    mcla.unfolder.init_with_query(query)
    init_forward_unfolding_solution_1(mcla)
502 503 504 505 506

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

507

508 509 510 511 512 513
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)
514 515 516 517 518 519 520

    .. 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]]
521 522 523
    """
    mcla = feed_mclanalyser

524 525
    ### DIMACS properties
    query = MCLSimpleQuery(None, None, None)
526
    # [[13]], [[12]], [[3]]
527
    query.dim_start, query.dim_inv, query.dim_final = numeric_properties[0]
528
    mcla.unfolder.init_with_query(query)
529
    init_forward_unfolding_solution_1(mcla, dimacs_check=False)
530

531 532 533
    ## Search solutions
    solutions = tuple(mcla.mac_search(query, 3))
    assert solutions == ()
534

535 536 537 538
    ## 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
VIGNET Pierre's avatar
VIGNET Pierre committed
539 540 541
    with pytest.raises(
        AssertionError, match=r".*At index 6 diff: \[-13\] != \[-15\].*"
    ):
542 543
        init_forward_unfolding_solution_1(mcla)

544

545
def test_init_forward_unfolding_solution_2_text(feed_mclanalyser, textual_properties):
546 547 548 549 550
    """
    Query:
        start, invariant, final: ("", "L", "C and K")
        Solution: D E F I L
    """
551 552
    mcla = feed_mclanalyser

553 554 555 556 557 558 559
    ### 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)
560 561 562 563 564 565 566

    ## 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"}

567

568 569 570 571 572 573 574 575 576
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

577 578 579
    ### 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
580 581
    # Adding new literals in dimacs form is currently not allowed
    # (without the argument check_query=False of init_with_query).
582
    query = MCLSimpleQuery(None, None, None)
583 584 585 586 587 588
    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)
589 590


591
def test_init_forward_unfolding_solution_3(feed_mclanalyser, textual_properties, numeric_properties):
592 593 594 595 596 597
    """
    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
598 599 600 601 602 603 604

    .. 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]]
605
    """
606 607 608 609
    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.
610
    # DIMACS data comes from the simple first numeric_properties ([[13]], [[12]], [[3]])
611 612 613 614
    query = MCLSimpleQuery(*textual_properties[1])
    query.dim_start, query.dim_inv, query.dim_final = numeric_properties[0]
    mcla.unfolder.init_with_query(query)

615
    init_forward_unfolding_solution_3(mcla, dimacs_check=False)
616

617 618 619
    ## Search solutions
    solutions = tuple(mcla.mac_search(query, 3))
    assert solutions == ()
620

621 622 623
    ## Test without disabling initial_constraints check
    mcla.unfolder.init_with_query(query)
    # Exception is expected
VIGNET Pierre's avatar
VIGNET Pierre committed
624 625 626
    with pytest.raises(
        AssertionError, match=r".*At index 6 diff: \[-13\] != \[-15\].*"
    ):
627 628
        init_forward_unfolding_solution_3(mcla)

629

630 631 632 633 634 635
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
    """
636 637 638 639 640 641 642 643 644
    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)

645 646 647 648 649 650 651 652
    ## 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

653

654
def init_forward_unfolding_solution_1(mcla, dimacs_check=True):
655 656 657 658
    """
    - Test first part of init_forward_unfolding: init of constraints
    - Test second part of init_forward_unfolding: shift of initialized constraints

659 660 661
    Query:
        start, invariant, final: ("M", "L", "C")
        No solution (because inhibitor M is activated)
662 663 664 665 666 667 668

    :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`
669
    """
670
    unfolder = mcla.unfolder
671

672 673 674
    ## Init constraints ########################################################

    init_forward_unfolding_part_1(mcla.unfolder)
675

676 677 678 679 680
    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)
681 682 683 684 685

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

686
    # MCLA could be reused, so __dynamic_constraints could not be empty here
687 688 689 690 691
    # artificial reset
    # unfolder._CLUnfolder__dynamic_constraints = []
    # assert unfolder.dynamic_constraints == []

    # no frontiers + M (start place)
692 693 694 695
    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
696 697 698 699 700 701 702 703 704 705

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

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

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

706
    ## Shift constraints #######################################################
707 708 709

    init_forward_unfolding_part_2(unfolder)

710 711 712
    print("dynamic_constraints:", unfolder.dynamic_constraints)
    print("invariant_constraints:", unfolder.invariant_constraints)
    print("final_constraints:", unfolder.final_constraints)
713

714
    # Shift of the system clauses and auxiliary clauses is made now.
715
    expected = [
716
        # [_lit0, _h2] [_lit0, D] [_h2, D, _lit0] [P, _lit5] [L, _lit5] [P, L, _lit5]
717
        [[-24, 16], [-24, 4], [-16, -4, 24], [-15, 42], [-12, 42], [15, 12, -42],
718
        # [_lit5, _lit4] [K, _lit4] [_lit5, K, _lit4] [B, _lit3] [_lit4, _lit3] [B, _lit4, _lit3]
719
        [-42, 41], [-11, 41], [42, 11, -41], [2, -40], [41, -40], [-2, -41, 40],
720
        # [_lit3, _lit2] [M, _lit2] [_lit3, M, _lit2] [A, _lit1] [_lit2, _lit1] [A, _lit2, _lit1]
721
        [40, -36], [-13, -36], [-40, 13, 36], [1, -25], [36, -25], [-1, -36, 25],
722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740
        # [_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]
741
        [-53, 7], [-53, -32], [53, -7, 32], [-54, 32, 8], [54, -32], [54, -8],
742
        # [_lit17, _h6] [_lit17, K] [_h6, K, _lit17] [_lit18, _h4] [_lit18, I] [_h4, I, _lit18]
743
        [-33, 20], [-33, 11], [-20, -11, 33], [-34, 18], [-34, 9], [-18, -9, 34],
744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762
        # [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]
763 764
        [-22, 1, 2], [-23, 14, 14]]]

765 766 767 768
    # No changes
    assert unfolder.initial_constraints == expected_initial_constraints

    # Crap dynamic_constraints test
769 770
    assert unfolder.dynamic_constraints == expected

771
    # L : 12 + 46 = 58
772 773 774 775 776
    assert unfolder.invariant_constraints == [[[12]], [[58]]]

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

777
    # C : 3 + 46 = 49
778 779 780 781 782 783 784 785
    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

786 787
    Query:
        start, invariant, final: ("", "L", "C and K")
788
        Solution: D E F I L
789
    """
790 791 792
    unfolder = mcla.unfolder

    ## Init constraints ########################################################
793

794
    init_forward_unfolding_part_1(mcla.unfolder)
795

796 797 798 799 800
    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)
801

802
    # Auxiliary variables: "C and K" property is added
VIGNET Pierre's avatar
VIGNET Pierre committed
803 804
    assert unfolder._CLUnfolder__aux_code_table == {"_lit47": 47}
    assert unfolder._CLUnfolder__aux_list == ["_lit47"]
805

806
    # MCLA could be reused, so __dynamic_constraints could not be empty here
807 808 809 810 811
    # artificial reset
    # unfolder._CLUnfolder__dynamic_constraints = []
    # assert unfolder.dynamic_constraints == []

    # no frontiers + nothing (no start place)
812 813
    expected_initial_constraints = [[-1], [-2], [-3], [-8], [-10], [-11], [-13], [-15]]
    assert unfolder.initial_constraints == expected_initial_constraints
814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833

    # 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
VIGNET Pierre's avatar
VIGNET Pierre committed
834
    # [[-3, 47], [-11, 47], [3, 11, -47], [47]]
835

836
    ## Shift constraints #######################################################
837 838 839

    init_forward_unfolding_part_2(unfolder)

840 841 842 843
    print("dynamic_constraints:", unfolder.dynamic_constraints)
    print("initial_constraints:", unfolder.initial_constraints)
    print("invariant_constraints:", unfolder.invariant_constraints)
    print("final_constraints:", unfolder.final_constraints)
844 845

    # Shift of the system clauses (and syst aux clauses)
846 847 848
    # System variables: max id is 46
    # Max value in the initial constraints: 47
    # => This last one is an auxiliary variable
849
    assert unfolder.get_var_number() == 46
850
    assert unfolder.shift_step == 47
851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873
    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]]]

874 875 876 877
    # No changes
    assert unfolder.initial_constraints == expected_initial_constraints

    # Crap dynamic_constraints test
878 879
    assert unfolder.dynamic_constraints == expected

880
    # L : 12 + shift_step (47) = 59
881 882 883 884 885 886 887 888 889 890
    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]]


891
def init_forward_unfolding_solution_3(mcla, dimacs_check=True):
892 893 894 895 896 897 898 899 900
    """
    - 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
901 902 903 904 905 906 907

    .. 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)
908 909 910 911 912 913 914

    :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`
915 916 917 918 919 920 921
    """
    unfolder = mcla.unfolder

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

    init_forward_unfolding_part_1(mcla.unfolder)

922 923 924 925
    print("dynamic_constraints:", unfolder.dynamic_constraints)
    print("initial_constraints:", unfolder.initial_constraints)
    print("invariant_constraints:", unfolder.invariant_constraints)
    print("final_constraints:", unfolder.final_constraints)
926 927 928 929

    assert unfolder.shift_step == 47

    # no frontiers + "M" (start place)
930 931 932 933
    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
934 935

    # Just append DIMACS constraints of the query: "L" + [[12]]