Commit cf2e8421 authored by Ludwig Dickmanns's avatar Ludwig Dickmanns
Browse files

MCDC: Bugfix

* McdcTestSuiteGenerator: TestCases are now only added if it makes sense
to add them, i.e. if z3 has a satisfiable prepositional formula.

Issue-Ref: 3596
Issue-Url: https://af3-developer.fortiss.org/issues/3596


Signed-off-by: Ludwig Dickmanns's avatarLudwig Dickmanns <dickmanns@fortiss.org>
parent 56704340
......@@ -149,7 +149,7 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
}
Context ctx = new Context();
TestCase newTC = createTestCase(testSuite);
TestCase newTC = TestingModelFactory.eINSTANCE.createTestCase();
String currentName = Integer.toString(newTC.hashCode());
newTC.setName(currentName);
Expr reqZ3 = formalRequirementMcdcToZ3(currentName, ctx, req);
......@@ -213,6 +213,7 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
if(opt.Check() == Status.SATISFIABLE) {
Model model = opt.getModel();
retrieveValues(ctx, newTC, model);
testSuite.getTestCases().add(newTC);
}
checkTestSuite();
......
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