Commit 336ec804 authored by VIGNET Pierre's avatar VIGNET Pierre
Browse files

[lib] Fix test_delay1_w_ic with new solutions of the new solver

These solutions are much more accurate and don't trigger useless clocks in the steps of the solutions
parent 9d60e7f1
......@@ -229,7 +229,81 @@ class TestMCLAnaLyzer(unittest.TestCase):
def test_delay1_w_ic(self):
"""
simple delay computation with clock sequence
"""
First test: f_prop = "C4"
# old solver
[[], [], [3], []]
[[-1, -2, -3, 4, -5, -6, -7, -8, -9, -10, -11, -12, 13, -14, -15, 16],
[-1, -2, -3, -4, -5, -6, 7, -8, -9, -10, -11, 12, -13, -14, -15, 16],
[-1, -2, 3, -4, -5, 6, -7, -8, -9, -10, -11, 12, -13, 14, -15, 16], #3>0 free clocks: (3, ':', 'h2')
[1, -2, -3, -4, -5, -6, -7, 8, 9, -10, 11, 12, -13, -14, -15, -16]]
['A1', 'C1', 'B1']
['A2', 'C2', 'B1']
['h2', 'A3', 'C2', '_lit0', 'B1'] # activated clock: h2
['_lit2', 'A4', 'B2', '_lit3', 'C2']
[[], [], [], []]
[[-1, -2, -3, 4, -5, -6, -7, -8, -9, -10, -11, -12, 13, -14, -15, -16],
[-1, -2, -3, -4, -5, -6, 7, -8, -9, -10, -11, 12, -13, -14, -15, -16],
[-1, -2, -3, -4, -5, 6, -7, -8, -9, -10, -11, 12, -13, -14, -15, -16],
[1, -2, -3, -4, -5, -6, -7, 8, -9, -10, 11, 12, -13, -14, -15, -16]]
['A1', 'C1']
['A2', 'C2']
['A3', 'C2']
['_lit2', 'A4', '_lit3', 'C2']
# new solver (no clock used => better solution):
[[], [], [], []]
[[-1, -2, -3, 4, -5, -6, -7, -8, -9, -10, -11, -12, 13, -14, -15, -16],
[-1, -2, -3, -4, -5, -6, 7, -8, -9, -10, -11, 12, -13, -14, -15, -16],
[-1, -2, -3, -4, -5, 6, -7, -8, -9, -10, -11, 12, -13, -14, -15, -16],
[1, -2, -3, -4, -5, -6, -7, 8, -9, -10, 11, 12, -13, -14, -15, -16]]
['A1', 'C1']
['A2', 'C2']
['A3', 'C2']
['_lit2', 'A4', '_lit3', 'C2']
[[], [], [], []]
[[-1, -2, -3, 4, -5, -6, -7, -8, -9, -10, -11, -12, 13, -14, -15, 16],
[-1, -2, -3, -4, -5, -6, 7, -8, -9, -10, -11, 12, -13, -14, -15, 16],
[-1, -2, -3, -4, -5, 6, -7, -8, -9, -10, -11, 12, -13, -14, -15, 16],
[1, -2, -3, -4, -5, -6, -7, 8, -9, -10, 11, 12, -13, -14, -15, 16]]
['A1', 'C1', 'B1']
['A2', 'C2', 'B1']
['A3', 'C2', 'B1']
['_lit2', 'A4', '_lit3', 'C2', 'B1']
.. note:: Debugging of solutions - help:
for i, sol in enumerate(lsol, 1):
print("Sol", i)
# [[], [], [], []]
print(sol.extract_act_input_clock_seq())
# [[....], [....], [....], [....]]
print(x.unflatten())
# Convert literal values to str, display only activated ones (val > 0)
for step in sol.unflatten():
print([sol.get_unfolder().get_var_name(val) for val in step
if val > 0])
"""
def debug_solutions(lsol):
"""Make human readable the status of literals at each step of a sol
"""
for i, sol in enumerate(lsol, 1):
print("Sol", i)
# [[], [], [], []]
print(sol.extract_act_input_clock_seq())
# [[....], [....], [....], [....]]
print(sol.unflatten())
# Convert literal values to str, display only activated ones (val > 0)
for step in sol.unflatten():
print([sol.get_unfolder().get_var_name(val) for val in step
if val > 0])
rep = ErrorRep()
mcla = MCLAnalyser(rep)
mcla.build_from_cadlang("examples/delay1.cal")
......@@ -238,14 +312,16 @@ class TestMCLAnaLyzer(unittest.TestCase):
inv_prop = None
f_prop = "C4"
query = MCLSimpleQuery(st_prop, inv_prop, f_prop)
# 4 steps, 1 solution
lsol = mcla.sq_solutions(query, 4, 1, mcla.unfolder.get_frontier())
sol = lsol[0]
ic_seq = sol.extract_act_input_clock_seq()
#print ic_seq
expected_sol = [[], [], [], [3]]
expected_sol = [[], [], [], []]
debug_solutions(lsol)
res = len(lsol) != 0
res = res and lit_sol_equal(expected_sol, ic_seq)
self.assert_(res, 'Error clock sequence for C4')
self.assert_(res, 'Error clock sequence for C4; expected: {}'.format(expected_sol))
f_prop = "C4 and not C3"
query = MCLSimpleQuery(None, None, f_prop)
......@@ -253,10 +329,11 @@ class TestMCLAnaLyzer(unittest.TestCase):
sol = lsol[0]
ic_seq = sol.extract_act_input_clock_seq()
#print ic_seq
expected_sol = [[], [], [], [3]]
expected_sol = [[], [], [], []]
debug_solutions(lsol)
res = len(lsol) != 0
res = res and lit_sol_equal(expected_sol, ic_seq)
self.assert_(res, 'Error clock sequence for C4 and not C3')
self.assert_(res, 'Error clock sequence for C4 and not C3; expected: {}'.format(expected_sol))
f_prop = "C3 and C4"
query = MCLSimpleQuery(None, None, f_prop)
......@@ -264,10 +341,12 @@ class TestMCLAnaLyzer(unittest.TestCase):
sol = lsol[0]
ic_seq = sol.extract_act_input_clock_seq()
#print ic_seq
# h2 is mandatory to get C3
expected_sol = [[], [3], [], []]
debug_solutions(lsol)
res = len(lsol) != 0
res = res and lit_sol_equal(expected_sol, ic_seq)
self.assert_(res, 'Error clock sequence for C4')
self.assert_(res, 'Error clock sequence for C4; expected: {}'.format(expected_sol))
def test_input1(self):
......
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