Commit e2d0fcea authored by VIGNET Pierre's avatar VIGNET Pierre

[lib] Tests: CLU: Cover the new functionality that prune initial constraints...

[lib] Tests: CLU: Cover the new functionality that prune initial constraints according to start/invariant places
parent fd74ede3
......@@ -367,6 +367,9 @@ def init_forward_unfolding_part_1(unfolder):
unfolder._CLUnfolder__init_final_constraint_0()
unfolder._CLUnfolder__init_invariant_constraint_0()
unfolder._CLUnfolder__init_variant_constraints_0()
# Should be after init_initial and init_invariant
unfolder._CLUnfolder__prune_initial_no_frontier_constraint_0()
def init_forward_unfolding_part_2(unfolder):
"""Shift step only"""
......@@ -492,6 +495,13 @@ def test_init_forward_unfolding_solution_1_dimacs(feed_mclanalyser, numeric_prop
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)
.. 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]]
"""
mcla = feed_mclanalyser
......@@ -506,6 +516,13 @@ def test_init_forward_unfolding_solution_1_dimacs(feed_mclanalyser, numeric_prop
solutions = tuple(mcla.mac_search(query, 3))
assert solutions == ()
## 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)
def test_init_forward_unfolding_solution_2_text(feed_mclanalyser, textual_properties):
"""
......@@ -559,6 +576,13 @@ def test_init_forward_unfolding_solution_3(feed_mclanalyser, textual_properties,
("", "L", "C and K") => [], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]
[[13]], [[12]], [[3]] <= ("M", "L", "C")
No solution
.. 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]]
"""
mcla = feed_mclanalyser
......@@ -569,12 +593,18 @@ def test_init_forward_unfolding_solution_3(feed_mclanalyser, textual_properties,
query.dim_start, query.dim_inv, query.dim_final = numeric_properties[0]
mcla.unfolder.init_with_query(query)
init_forward_unfolding_solution_3(mcla)
init_forward_unfolding_solution_3(mcla, dimacs_check=False)
## Search solutions
solutions = tuple(mcla.mac_search(query, 3))
assert solutions == ()
## 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)
def test_init_forward_unfolding_solution_4(feed_mclanalyser, textual_properties):
"""
......@@ -600,7 +630,7 @@ def test_init_forward_unfolding_solution_4(feed_mclanalyser, textual_properties)
assert found == expected
def init_forward_unfolding_solution_1(mcla):
def init_forward_unfolding_solution_1(mcla, dimacs_check=True):
"""
- Test first part of init_forward_unfolding: init of constraints
- Test second part of init_forward_unfolding: shift of initialized constraints
......@@ -608,6 +638,13 @@ def init_forward_unfolding_solution_1(mcla):
Query:
start, invariant, final: ("M", "L", "C")
No solution (because inhibitor M is activated)
: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`
"""
unfolder = mcla.unfolder
......@@ -631,7 +668,10 @@ def init_forward_unfolding_solution_1(mcla):
# assert unfolder.dynamic_constraints == []
# no frontiers + M (start place)
assert unfolder.initial_constraints == [[-1], [-2], [-3], [-8], [-10], [-11], [-13], [-15], [13]]
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
# L
assert unfolder.invariant_constraints == [[[12]]]
......@@ -827,7 +867,7 @@ def init_forward_unfolding_solution_2(mcla):
assert unfolder.final_constraints == [[50, -94], [58, -94], [-50, -58, 94], [94]]
def init_forward_unfolding_solution_3(mcla):
def init_forward_unfolding_solution_3(mcla, dimacs_check=True):
"""
- Test first part of init_forward_unfolding: init of constraints
- Test second part of init_forward_unfolding: shift of initialized constraints
......@@ -844,6 +884,13 @@ def init_forward_unfolding_solution_3(mcla):
=> clauses redondantes en cas d'égalité des events entre l'attribut
au format texte et celui au format DIMACS.
(invariant_constraints)
: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`
"""
unfolder = mcla.unfolder
......@@ -859,8 +906,10 @@ def init_forward_unfolding_solution_3(mcla):
assert unfolder.shift_step == 47
# no frontiers + "M" (start place)
# TODO: voir sol1 y'a un pb ici...
assert unfolder.initial_constraints == [[-1], [-2], [-3], [-8], [-10], [-11], [-13], [-15], [13]]
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
# Just append DIMACS constraints of the query: "L" + [[12]]
assert unfolder.invariant_constraints == [[[12], [12]]]
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment