[lib] Tests: CLUnfolder: solutions of tests are tested now

library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py

@@ -232,8 +232,8 @@ def textual_properties():
     """start, invariant, final properties in textual form"""
     return (
         ("M", "L", "C"), # No solution (because inhibitor M is activated)
-        ("", "L", "C and K"), # Solution: I E D F
-        ("", "", "C"), # Solutions: F E L D, I E D F
+        ("", "L", "C and K"), # Solution: D E F I L
+        ("", "", "C"), # Solutions: F E L D, D E F I
     )
 
 @pytest.fixture()
@@ -489,7 +489,11 @@ def test_init_unfolder(feed_mclanalyser):
 
 
 def test_init_forward_unfolding_solution_1(feed_mclanalyser, textual_properties, numeric_properties):
-
+    """
+    Query:
+        start, invariant, final: ("M", "L", "C")
+        No solution (because inhibitor M is activated)
+    """
     mcla = feed_mclanalyser
 
     ### Textual properties
@@ -499,7 +503,11 @@ def test_init_forward_unfolding_solution_1(feed_mclanalyser, textual_properties,
     mcla.unfolder.init_with_query(query)
 
     init_forward_unfolding_solution_1(mcla)
-    ## TODO: search sol
+
+    ## Search solutions
+    solutions = tuple(mcla.mac_search(query, 3))
+    assert solutions == ()
+
 
     ### DIMACS properties
     query = MCLSimpleQuery(None, None, None)
@@ -507,9 +515,17 @@ def test_init_forward_unfolding_solution_1(feed_mclanalyser, textual_properties,
     mcla.unfolder.init_with_query(query)
     init_forward_unfolding_solution_1(mcla)
 
+    ## Search solutions
+    solutions = tuple(mcla.mac_search(query, 3))
+    assert solutions == ()
 
-def test_init_forward_unfolding_solution_2(feed_mclanalyser, textual_properties, numeric_properties):
 
+def test_init_forward_unfolding_solution_2(feed_mclanalyser, textual_properties, numeric_properties):
+    """
+    Query:
+        start, invariant, final: ("", "L", "C and K")
+        Solution: D E F I L
+    """
     mcla = feed_mclanalyser
 
     ### Textual properties
@@ -519,7 +535,13 @@ def test_init_forward_unfolding_solution_2(feed_mclanalyser, textual_properties,
     mcla.unfolder.init_with_query(query)
 
     init_forward_unfolding_solution_2(mcla)
-    ## TODO: search sol
+
+    ## 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"}
+
 
     ### DIMACS properties
     # "C and K" property requires an auxiliary literal which can only be added
@@ -535,7 +557,13 @@ def test_init_forward_unfolding_solution_2(feed_mclanalyser, textual_properties,
 
 
 def test_init_forward_unfolding_solution_3(feed_mclanalyser, textual_properties, numeric_properties):
-
+    """
+    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
+    """
     mcla = feed_mclanalyser
 
     # Note: The second set creates auxiliary clauses that we could not insert
@@ -547,9 +575,17 @@ def test_init_forward_unfolding_solution_3(feed_mclanalyser, textual_properties,
 
     init_forward_unfolding_solution_3(mcla)
 
+    ## Search solutions
+    solutions = tuple(mcla.mac_search(query, 3))
+    assert solutions == ()
 
-def test_init_forward_unfolding_solution_4(feed_mclanalyser, textual_properties):
 
+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
+    """
     mcla = feed_mclanalyser
 
     # Note: The second set creates auxiliary clauses that we could not insert
@@ -559,6 +595,14 @@ def test_init_forward_unfolding_solution_4(feed_mclanalyser, textual_properties)
 
     init_forward_unfolding_solution_4(mcla)
 
+    ## 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
+
 
 def init_forward_unfolding_solution_1(mcla):
     """
@@ -654,7 +698,7 @@ def init_forward_unfolding_solution_2(mcla):
 
     Query:
         start, invariant, final: ("", "L", "C and K")
-        Solution: I E D F
+        Solution: D E F I L
     """
     unfolder = mcla.unfolder
 
@@ -794,7 +838,7 @@ def init_forward_unfolding_solution_4(mcla):
 
     Query:
         start, invariant, final: ("", "", "C")
-        Solutions: F E L D, I E D F
+        Solutions: F E L D, D E F I
     """
     unfolder = mcla.unfolder