Commit 0e019808 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Tests: CLUnfolder: add asserts; fix typos; add doc

parent 68d57a39
......@@ -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]]
......
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