Commit 4127e7cd authored by Paul Fiterau Brostean's avatar Paul Fiterau Brostean
Browse files

Fixed test scenario. Updated ra with optimization discussed yesterday. Tests...

Fixed test scenario. Updated ra with optimization discussed yesterday. Tests pass, inferrence is slow on the 5th model.
parent b13eab76
......@@ -111,7 +111,7 @@ sut_m4 = RaTestScenario ("store_2_toggle_select_NS", [
([act(1), act(2), act(1), act(2)], True),
([act(1), act(2), act(1), act(2), act(1)], True),
([act(1), act(2), act(1), act(2), act(1), act(2)], True)
], 4, 2)
], 5, 2)
# Go to an accepting sink if the third value is different than the first two, else go to a rejecting sink
sut_m5 = RaTestScenario("store_2_third_diff", [
......
......@@ -63,9 +63,8 @@ class RaLearnerTest(unittest.TestCase):
min_locations = test_scenario.nr_locations - 1
max_locations = test_scenario.nr_locations + 1
num_regs = 0
result = ralearner._learn_model(min_locations, max_locations, num_regs) #
result = ralearner._learn_model(min_locations, max_locations, test_scenario.nr_registers + 1) #
return result
......
......@@ -179,9 +179,14 @@ class RAEncoder(Encoder):
mapper.valuation(c, r) == mapper.valuation(n, r)
)
),
])
path = [v for (l, v) in node.path()]
# Map to the right transition
z3.If(
# Map to the right transition
if value in path:
constraints.append(
z3.If(
z3.Exists(
[r],
z3.And(
......@@ -204,8 +209,12 @@ class RAEncoder(Encoder):
)
)
),
ra.transition(mapper.map(n), l, ra.fresh) == mapper.map(c)),
])
ra.transition(mapper.map(n), l, ra.fresh) == mapper.map(c))
)
else:
constraints.append(
ra.transition(mapper.map(n), l, ra.fresh) == mapper.map(c)
)
constraints.append(z3.Distinct(list(values)))
return constraints
Supports Markdown
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