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

MCDC: Advantageous test case

* McdcTestSuiteGenerator can now create a test case, which is
advantageous for the generation of mcdc test cases.
* In McdcUtils the method isAtom(...) was made public for usage in
generateAdvantageousTestCase.

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

Signed-off-by: Ludwig Dickmanns's avatarLudwig Dickmanns <dickmanns@fortiss.org>
parent 33f5ff48
......@@ -248,7 +248,7 @@ public final class McdcUtils {
}
/** Helper method checking whether the object is an atom. */
private static boolean isAtom(EObject eObject) {
public static boolean isAtom(EObject eObject) {
if(eObject instanceof FunctionCall) {
FunctionCall functionCall = (FunctionCall)eObject;
IFunction function = functionCall.getFunction();
......
......@@ -15,11 +15,15 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.testing.mcdc.generator;
import static com.microsoft.z3.Status.SATISFIABLE;
import static org.fortiss.af3.expression.model.terms.EOperator.AND;
import static org.fortiss.af3.expression.model.terms.EOperator.OR;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.boolConst;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.doubleConst;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.intConst;
import static org.fortiss.af3.testing.mcdc.McdcUtils.GUARD;
import static org.fortiss.af3.testing.mcdc.McdcUtils.getAtomsFromGuardMCDC;
import static org.fortiss.af3.testing.mcdc.McdcUtils.isAtom;
import static org.fortiss.af3.testing.mcdc.McdcUtils.toZ3;
import static org.fortiss.af3.testing.utils.TestingModelElementFactory.createTestCase;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.pickFirstInstanceOf;
......@@ -35,10 +39,15 @@ import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.component.model.InputPort;
import org.fortiss.af3.component.model.OutputPort;
import org.fortiss.af3.expression.model.terms.BoolConst;
import org.fortiss.af3.expression.model.terms.EOperator;
import org.fortiss.af3.expression.model.terms.FunctionCall;
import org.fortiss.af3.expression.model.terms.IExpressionTerm;
import org.fortiss.af3.expression.model.terms.PredefinedFunction;
import org.fortiss.af3.expression.model.types.TBool;
import org.fortiss.af3.expression.model.types.TDouble;
import org.fortiss.af3.expression.model.types.TInt;
import org.fortiss.af3.project.model.typesystem.IFunction;
import org.fortiss.af3.project.model.typesystem.ITerm;
import org.fortiss.af3.project.model.typesystem.IType;
import org.fortiss.af3.testing.extension.ITestSuiteGenerator;
import org.fortiss.af3.testing.extension.data.TestSuiteGenerationException;
......@@ -107,6 +116,10 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
checkTestSuite();
}
if(this.testSuite.getTestCases().size() == 0) {
generateAdvantageousTestCase();
}
this.verificationStep();
return this.testSuite;
......@@ -304,6 +317,94 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
}
}
private void generateAdvantageousTestCase() {
Context ctx = new Context();
// New test case
TestCase newTC = createTestCase(testSuite);
// Unique (?) name
newTC.setName(Integer.toString(newTC.hashCode()));
// Add new test case constraints from the requirement to ctx
Expr reqZ3 = toZ3(newTC.getName(), ctx, req, component);
IExpressionTerm guard = req.getGuard();
BoolExpr intelligentAssignment = recursiveAssignment(newTC, guard, ctx, true);
// Naming of atoms for retrieval
BoolExpr atomsClause = ctx.mkTrue();
for(int i = 0; i < atoms.size(); i++) {
BoolExpr atomI = (BoolExpr)toZ3(newTC.getName(), ctx, atoms.get(i), component);
BoolExpr atomIName = ctx.mkBoolConst(newTC.getName() + "_atom_" + i);
BoolExpr atomConst = ctx.mkEq(atomIName, atomI);
atomsClause = ctx.mkAnd(atomsClause, atomConst);
}
Optimize opt = ctx.mkOptimize();
opt.Add(intelligentAssignment, atomsClause, (BoolExpr)reqZ3);
if(opt.Check() == SATISFIABLE) {
retrieveValues(ctx, newTC, opt);
}
}
/**
* - true and: all terms true
* - true or : all but one term false
* - false and: all but one term true
* - false or : all terms false
*/
private BoolExpr recursiveAssignment(TestCase testCase, ITerm term, Context ctx,
boolean shouldEvaluateTo) {
// There should only be {@link FunctionCall}s in the guard.
FunctionCall functionCall = (FunctionCall)term;
if(isAtom(functionCall)) {
Expr atom = toZ3(testCase.getName(), ctx, functionCall, component);
return ctx.mkEq(atom, ctx.mkBool(shouldEvaluateTo));
}
IFunction function = functionCall.getFunction();
if(function instanceof PredefinedFunction) {
PredefinedFunction predefinedFunction = (PredefinedFunction)function;
EOperator operator = predefinedFunction.getOperator();
EList<ITerm> arguments = functionCall.getArguments();
if(arguments == null || arguments.size() == 0) {
return null;
}
if(operator == AND) {
BoolExpr and = ctx.mkTrue();
ITerm argument = arguments.get(0);
BoolExpr argumentZ3;
if(shouldEvaluateTo) {
argumentZ3 = recursiveAssignment(testCase, argument, ctx, true);
} else {
argumentZ3 = recursiveAssignment(testCase, argument, ctx, false);
}
and = ctx.mkAnd(and, argumentZ3);
for(int i = 1; i < arguments.size(); i++) {
argument = arguments.get(i);
argumentZ3 = recursiveAssignment(testCase, argument, ctx, true);
and = ctx.mkAnd(and, argumentZ3);
}
return and;
}
if(operator == OR) {
BoolExpr and = ctx.mkTrue();
ITerm argument = arguments.get(0);
BoolExpr argumentZ3;
if(shouldEvaluateTo) {
argumentZ3 = recursiveAssignment(testCase, argument, ctx, true);
} else {
argumentZ3 = recursiveAssignment(testCase, argument, ctx, false);
}
and = ctx.mkAnd(and, argumentZ3);
for(int i = 1; i < arguments.size(); i++) {
argument = arguments.get(i);
argumentZ3 = recursiveAssignment(testCase, argument, ctx, false);
and = ctx.mkAnd(and, argumentZ3);
}
return and;
}
}
return null;
}
private void checkTestSuite() {
EList<TestCase> testCases = testSuite.getTestCases();
for(int i = 0; i < testCases.size() - 1; i++) {
......
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