diff --git a/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py b/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py
index 87727b5be38c1e1408f4c386f4ad9f0e66c5ff52..66c9e8aecd20e7f69f63e9e87437f48ff27b935e 100644
--- a/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py
+++ b/library/cadbiom/models/clause_constraints/mcl/TestCLUnfolder.py
@@ -190,24 +190,32 @@ def create_unfolder(model):
def textual_properties():
"""start, invariant, final"""
return (
- ("M", "L", "C"), # No solution (M activated)
+ ("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
)
@pytest.fixture()
-def numerical_properties():
+def numeric_properties():
return (
+ # "M", "L", "C"
([[13]], [[12]], [[3]]),
+ # "", "L", "C and K"
([], [[12]], [[3, -47], [11, -47], [-3, -11, 47], [47]]),
)
@pytest.fixture()
def feed_mclanalyser():
- """Setup MCLAnalyser with a bcx model"""
+ """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
+
+ """
rep = ErrorReporter()
- # Force __var_list to be sorted at the output of base_var_set from
+ # debug: Force __var_list to be sorted at the output of base_var_set from
# CLDynSys for reproductibility in tests (literals naming)
mcla = MCLAnalyser(rep, debug=True)
filename = pkg_resources.resource_filename(
@@ -361,6 +369,7 @@ def test_init_unfolder(feed_mclanalyser):
## Test CLDynSys
# 15 places
assert unfolder.get_var_number() == 46
+ assert unfolder.shift_step_init == 46
# __var_list is built on casted set; MCLAnalyser is un debug mode
# so the list is sorted
@@ -378,30 +387,31 @@ def test_init_unfolder(feed_mclanalyser):
## Test mapping of variables names to values
expected_var_code_table = {
- '_lit22': 39, '_lit20': 37, '_lit21': 38, '_lit19': 35,
+ '_lit22': 39, '_lit20': 37, '_lit21': 38, '_lit19': 35, '_lit15': 31,
'_lit18': 34, '_lit6': 43, '_lit17': 33, '_lit13': 29, '_lit9': 46,
- '_lit8': 45, '_h_0': 22, '_h_1': 23, '_lit16': 32, '_lit12': 28,
- '_lit3': 40, '_lit2': 36, '_lit1': 25, '_lit0': 24, '_lit7': 44,
- '_lit11': 27, '_lit5': 42, '_lit4': 41,
+ '_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,
'A': 1, 'C': 3, 'B': 2, 'E': 5, 'D': 4, 'G': 7, 'F': 6, 'I': 9, 'H': 8,
- 'K': 11, 'J': 10, 'M': 13, 'L': 12, '_lit15': 31, 'N': 14, 'P': 15,
- '_lit14': 30, '_h4': 18, '_h5': 19, '_h6': 20, '_h7': 21, '_h2': 16,
- '_h3': 17, '_lit10': 26
+ '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,
}
- # Check presence of all basic literals (not future ones with "`" added)
+ # Check presence of all basic literals (no future ones with "`" counted)
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
- # (future literals with "`" are added)
+ # (future literals with "`" are added in found_var_code_table)
assert len(found_var_code_table) == 2 * len(expected_var_code_table)
## Test frontiers, places, values and names
+ # D E F G I L N
print("Frontier values", unfolder.frontier_values)
- assert set(unfolder.frontier_values) == {4, 5, 6, 7, 9, 12, 14} # D E F G I L N
+ assert set(unfolder.frontier_values) == {4, 5, 6, 7, 9, 12, 14}
frontiers_values_mapping = {
value: unfolder.get_var_name(value) for value in unfolder.frontier_values
@@ -424,7 +434,7 @@ def test_init_unfolder(feed_mclanalyser):
clocks_values_mapping = {
value: unfolder.get_var_name(value) for value in unfolder.free_clocks
}
- print("Clocks values mapping", clocks_values_mapping)
+ print("Free clocks/events values mapping", clocks_values_mapping)
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
@@ -432,12 +442,11 @@ def test_init_unfolder(feed_mclanalyser):
# Not frontiers: A B C H J K M P
found = unfolder._CLUnfolder__no_frontier_init
- print("Places not frontiers", found)
+ print("Places that are not frontiers", found)
assert found == [[-1], [-2], [-3], [-8], [-10], [-11], [-13], [-15]]
-
-def test_init_forward(feed_mclanalyser, textual_properties, numerical_properties):
+def test_init_forward(feed_mclanalyser, textual_properties, numeric_properties):
"""Test forward initialization for various models and properties types
Specific call:
@@ -447,7 +456,7 @@ def test_init_forward(feed_mclanalyser, textual_properties, numerical_properties
self.dim_start = [] # list<DClause>
self.dim_inv = [] # list<DClause>
self.dim_final = [] # list<DClause>
- self.dim_variant_prop = [] # list<list<DClause>>
+ self.dim_variant = [] # list<list<DClause>>
CLUnfolder attributes that contain query attributes:
self.__initial_property = None # logical formula - literal boolean expression
@@ -476,7 +485,7 @@ def test_init_forward(feed_mclanalyser, textual_properties, numerical_properties
"""
mcla = feed_mclanalyser
- ## First properties
+ ## First properties ########################################################
### Textual properties
start, invariant, final = textual_properties[0]
@@ -487,16 +496,13 @@ def test_init_forward(feed_mclanalyser, textual_properties, numerical_properties
## TODO: search sol
### DIMACS properties
- dim_start, dim_inv, dim_final = numerical_properties[0]
query = MCLSimpleQuery(None, None, None)
- query.dim_start = dim_start
- query.dim_inv = dim_inv
- query.dim_final = dim_final
+ query.dim_start, query.dim_inv, query.dim_final = numeric_properties[0]
mcla.unfolder.init_with_query(query)
init_forward_unfolding_solution_1(mcla)
- ## Second properties
+ ## Second properties #######################################################
### Textual properties
start, invariant, final = textual_properties[1]
@@ -506,14 +512,17 @@ def test_init_forward(feed_mclanalyser, textual_properties, numerical_properties
init_forward_unfolding_solution_2(mcla)
## TODO: search sol
- ### DIMACS properties: TODO: marche pas: les litéraux supplémentaires ne sont pas pris en compte...
- dim_start, dim_inv, dim_final = numerical_properties[1]
+ ### DIMACS properties
+ # "C and K" property requires an auxiliary literal which can only be added
+ # from the textual version of this property.
+ # Adding new literals in dimacs form is currently not allowed.
query = MCLSimpleQuery(None, None, None)
- query.dim_start = dim_start
- query.dim_inv = dim_inv
- query.dim_final = dim_final
- mcla.unfolder.init_with_query(query)
- init_forward_unfolding_solution_2(mcla)
+ 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)
@@ -522,12 +531,15 @@ def init_forward_unfolding_solution_1(mcla):
- Test first part of init_forward_unfolding: init of constraints
- Test second part of init_forward_unfolding: shift of initialized constraints
- ("M", "L", "C"), # No solution (M activated)
+ Query:
+ start, invariant, final: ("M", "L", "C")
+ No solution (because inhibitor M is activated)
"""
- unfolder = mcla.unfolder # shortcut
- init_forward_unfolding_part_1(mcla.unfolder)
+ unfolder = mcla.unfolder
- ############################################################################
+ ## Init constraints ########################################################
+
+ init_forward_unfolding_part_1(mcla.unfolder)
print(unfolder.dynamic_constraints)
print(unfolder.initial_constraints)
@@ -539,7 +551,7 @@ def init_forward_unfolding_solution_1(mcla):
assert unfolder._CLUnfolder__aux_code_table == dict()
assert unfolder._CLUnfolder__aux_list == []
- # MCLA could be reused, so __dynamic_constraints is not empty at this step
+ # MCLA could be reused, so __dynamic_constraints could not be empty here
# artificial reset
# unfolder._CLUnfolder__dynamic_constraints = []
# assert unfolder.dynamic_constraints == []
@@ -556,7 +568,7 @@ def init_forward_unfolding_solution_1(mcla):
# C
assert unfolder.final_constraints == [[3]]
- ############################################################################
+ ## Shift constraints #######################################################
init_forward_unfolding_part_2(unfolder)
@@ -564,8 +576,7 @@ def init_forward_unfolding_solution_1(mcla):
print(unfolder.invariant_constraints)
print(unfolder.final_constraints)
- # Shift of the system clauses (and syst aux clauses)
- # The maximum value is 46 since there is 46 literals
+ # Shift of the system clauses and auxiliary clauses is made now.
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],
@@ -592,13 +603,13 @@ def init_forward_unfolding_solution_1(mcla):
# Crap
assert unfolder.dynamic_constraints == expected
- # L
+ # L : 12 + 46 = 58
assert unfolder.invariant_constraints == [[[12]], [[58]]]
# No variant constraint (not shifted in second part of init_forward_unfolding)
assert unfolder.variant_constraints == []
- # C + 46
+ # C : 3 + 46 = 49
assert unfolder.final_constraints == [[49]]
@@ -607,12 +618,15 @@ 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
- ("", "L", "C and K") # I E D F
+ Query:
+ start, invariant, final: ("", "L", "C and K")
+ Solution: I E D F
"""
- unfolder = mcla.unfolder # shortcut
- init_forward_unfolding_part_1(mcla.unfolder)
+ unfolder = mcla.unfolder
+
+ ## Init constraints ########################################################
- ############################################################################
+ init_forward_unfolding_part_1(mcla.unfolder)
print(unfolder.dynamic_constraints)
print(unfolder.initial_constraints)
@@ -620,11 +634,11 @@ def init_forward_unfolding_solution_2(mcla):
print(unfolder.variant_constraints)
print(unfolder.final_constraints)
- # No auxiliary variables: "C and K" property is added
+ # Auxiliary variables: "C and K" property is added
assert unfolder._CLUnfolder__aux_code_table == {'_lit47': 47}
assert unfolder._CLUnfolder__aux_list == ['_lit47']
- # MCLA could be reused, so __dynamic_constraints is not empty at this step
+ # MCLA could be reused, so __dynamic_constraints could not be empty here
# artificial reset
# unfolder._CLUnfolder__dynamic_constraints = []
# assert unfolder.dynamic_constraints == []
@@ -653,7 +667,7 @@ def init_forward_unfolding_solution_2(mcla):
# _lit47
#[[-3, 47], [-11, 47], [3, 11, -47], [47]]
- ############################################################################
+ ## Shift constraints #######################################################
init_forward_unfolding_part_2(unfolder)
@@ -691,7 +705,7 @@ def init_forward_unfolding_solution_2(mcla):
# Crap
assert unfolder.dynamic_constraints == expected
- # L : 12 + shift_step (47)
+ # L : 12 + shift_step (47) = 59
assert unfolder.invariant_constraints == [[[12]], [[59]]]
# No variant constraint (not shifted in second part of init_forward_unfolding)
@@ -706,7 +720,7 @@ def test_shift(feed_mclanalyser, textual_properties):
"""Test shift of constraints during the solutions search"""
mcla = feed_mclanalyser
- unfolder = mcla.unfolder # shortcut
+ unfolder = mcla.unfolder
start, invariant, final = textual_properties[0]
@@ -777,7 +791,7 @@ def test_shift(feed_mclanalyser, textual_properties):
# L = 12: + 46 + 46 => 104
assert unfolder.invariant_constraints == [[[12]], [[58]], [[104]]]
- # C = 3: + 46 + 46 =>
+ # C = 3: + 46 + 46 => 95
assert unfolder.final_constraints == [[95]]