Commit 65a0b398 authored by Ludwig Dickmanns's avatar Ludwig Dickmanns
Browse files

MCDC: Test case generation

* McdcTestSuiteGenerator: Getter for atoms and independencePairs.
Removed print of model. Cleanup. Added TODOs.
* MCDCUtils: Added BoolExpr for retrieval of evaluated guard
(takenBranch).

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

Signed-off-by: Ludwig Dickmanns's avatarLudwig Dickmanns <dickmanns@fortiss.org>
parent e8a35775
......@@ -132,8 +132,9 @@ public final class MCDCUtils {
if(term instanceof FormalRequirementMCDC) {
FormalRequirementMCDC formalRequirementMCDC = (FormalRequirementMCDC)term;
BoolExpr guard = (BoolExpr)toZ3(prefix, ctx, formalRequirementMCDC.getGuard(), context);
// For retrieval of the taken branch
BoolExpr guardName = ctx.mkBoolConst(prefix + GUARD);
ctx.mkEq(guardName, guard);
BoolExpr guardConst = ctx.mkEq(guardName, guard);
BoolExpr thenE = ctx.mkTrue();
BoolExpr elseE = ctx.mkTrue();
for(IStatementTerm statement : formalRequirementMCDC.getThenBlock().getStatements()) {
......@@ -142,7 +143,8 @@ public final class MCDCUtils {
for(IStatementTerm statement : formalRequirementMCDC.getElseBlock().getStatements()) {
elseE = ctx.mkAnd(elseE, (BoolExpr)toZ3(prefix, ctx, statement, context));
}
return ctx.mkOr(ctx.mkAnd(guard, thenE), ctx.mkAnd(ctx.mkNot(guard), elseE));
BoolExpr ite = ctx.mkOr(ctx.mkAnd(guard, thenE), ctx.mkAnd(ctx.mkNot(guard), elseE));
return ctx.mkAnd(ite, guardConst);
}
return null;
}
......
......@@ -65,6 +65,8 @@ import com.microsoft.z3.Status;
* Inputs and outputs of the test case are stored in step one.
* Step two contains the evaluated atoms in TestInputs and the taken branch in TestOutputs.
*
* TODO stop when nothing new is verified
*
* @author ludwig dickmanns
*/
public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
......@@ -99,6 +101,7 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
this.req = spec.getFormalRequirementMCDC();
this.component = specification.getComponent();
// TODO Check if ports are already added?
this.testSuite.getInputPorts().addAll(component.getInputPorts());
this.testSuite.getOutputPorts().addAll(component.getOutputPorts());
this.atoms = getAtomsFromGuardMCDC(req.getGuard());
......@@ -125,7 +128,7 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
}
Context ctx = new Context();
// Feed z3 with existing test cases
addExistingDataToZ3(ctx);
// addExistingDataToZ3(ctx);
// New test case
TestCase newTC = createTestCase(testSuite);
......@@ -154,9 +157,6 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
// Taken branches should differ for condition coverage
BoolExpr dc = ctx.mkNot(ctx.mkEq(oldTakenBranch, newTakenBranch));
//
BoolExpr atomsAnd = ctx.mkTrue();
// Only one of the atoms should be different
for(int i = 0; i < atoms.size(); i++) {
BoolExpr andClause = ctx.mkTrue();
......@@ -207,6 +207,7 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
}
/**
*
* @param ctx
*/
private void addExistingDataToZ3(Context ctx) {
......@@ -298,7 +299,6 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
TestOutput testOutput = TestingModelFactory.eINSTANCE.createTestOutput();
IType type = outputPort.getVariableType();
String identifier = outputPort.getName();
System.out.println(model);
Expr toBeRetrieved, result;
if(type instanceof TBool) {
toBeRetrieved = ctx.mkBoolConst(newTC.getName() + identifier);
......@@ -413,4 +413,14 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
}
}
}
/** Returns atoms. */
public List<FunctionCall> getAtoms() {
return atoms;
}
/** Returns independencePairs. */
public List<Pair<TestCase, TestCase>> getIndependencePairs() {
return independencePairs;
}
}
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