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

MCDC: Reformatting

* Cherry-picked 5855897f

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

Signed-off-by: Ludwig Dickmanns's avatarLudwig Dickmanns <dickmanns@fortiss.org>
parent b1576ecd
MCDCUtils.java 7ac114cd2a668169becb4ee2f4568d7b86607478 GREEN
MCDCUtils.java 9ddc7e1cb100e88955a6cba7a84c5512c998271a RED
......@@ -54,11 +54,15 @@ import com.microsoft.z3.Z3Exception;
/**
* Utility class transforming a {@link FormalRequirementMCDC} into an {@link Expr}.
* Contains {@link String}identifiers for the guard and the coverages.
*
* @author ludwig dickmanns
*/
public final class MCDCUtils {
public static final String CONDITION_COVERAGE = "_condition_coverage";
public static final String GUARD = "_guard";
/**
* Transforms a {@link ITerm} into a {@link Expr}.
*
......@@ -128,6 +132,8 @@ public final class MCDCUtils {
if(term instanceof FormalRequirementMCDC) {
FormalRequirementMCDC formalRequirementMCDC = (FormalRequirementMCDC)term;
BoolExpr guard = (BoolExpr)toZ3(prefix, ctx, formalRequirementMCDC.getGuard(), context);
BoolExpr guardName = ctx.mkBoolConst(prefix + GUARD);
ctx.mkEq(guardName, guard);
BoolExpr thenE = ctx.mkTrue();
BoolExpr elseE = ctx.mkTrue();
for(IStatementTerm statement : formalRequirementMCDC.getThenBlock().getStatements()) {
......
McdcTestSuiteGenerator.java 4281291934647d2c2c672db5008af8193d5edf0f RED
......@@ -15,26 +15,68 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.testing.mcdc.generator;
import static org.fortiss.af3.testing.utils.TestingModelElementFactory.createTestSuite;
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.toZ3;
import static org.fortiss.af3.testing.utils.TestingModelElementFactory.createTestCase;
import static org.fortiss.af3.testing.utils.TestingModelElementFactory.createTestStep;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.pickFirstInstanceOf;
import java.util.ArrayList;
import java.util.List;
import org.apache.commons.lang3.tuple.ImmutablePair;
import org.apache.commons.lang3.tuple.Pair;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.emf.common.util.EList;
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.FunctionCall;
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.ITerm;
import org.fortiss.af3.project.model.typesystem.IType;
import org.fortiss.af3.testing.extension.ITestSuiteGenerator;
import org.fortiss.af3.testing.extension.data.TestSuiteGenerationException;
import org.fortiss.af3.testing.model.TestCase;
import org.fortiss.af3.testing.model.TestInput;
import org.fortiss.af3.testing.model.TestOutput;
import org.fortiss.af3.testing.model.TestStep;
import org.fortiss.af3.testing.model.TestSuite;
import org.fortiss.af3.testing.model.TestSuiteSpecification;
import org.fortiss.af3.testing.model.TestingModelFactory;
import org.fortiss.af3.testing.model.mcdc.FormalRequirementMCDC;
import org.fortiss.af3.testing.model.mcdc.McdcSpecificationPart;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.Model;
import com.microsoft.z3.Optimize;
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.
*
* @author ludwig
* @author ludwig dickmanns
*/
public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
private TestSuite initialSuite;
private TestSuite testSuite;
private FormalRequirementMCDC req;
private Component component;
private List<FunctionCall> atoms;
private List<FunctionCall> verifiedAtoms = new ArrayList<FunctionCall>();
private List<Pair<TestCase, TestCase>> independencePairs =
new ArrayList<Pair<TestCase, TestCase>>();
private boolean ccVerified = false;
/**
* Constructor.
......@@ -42,7 +84,7 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
* @param initialSuite
*/
public McdcTestSuiteGenerator(TestSuite initialSuite) {
this.initialSuite = initialSuite;
this.testSuite = initialSuite;
}
/** {@inheritDoc} */
......@@ -52,16 +94,323 @@ public class McdcTestSuiteGenerator implements ITestSuiteGenerator {
McdcSpecificationPart spec =
pickFirstInstanceOf(McdcSpecificationPart.class, specification.getSpecifications());
TestSuite testSuite = createTestSuite("McdcTestSuite", spec.getTestSuiteSpecification());
testSuite.setGeneratedBy(getClass());
// TestSuite testSuite = createTestSuite("McdcTestSuite", spec.getTestSuiteSpecification());
// testSuite.setGeneratedBy(getClass());
this.req = spec.getFormalRequirementMCDC();
this.component = specification.getComponent();
this.testSuite.getInputPorts().addAll(component.getInputPorts());
this.testSuite.getOutputPorts().addAll(component.getOutputPorts());
this.atoms = getAtomsFromGuardMCDC(req.getGuard());
if(this.testSuite.getTestCases().size() > 1) {
checkTestSuite();
}
this.verificationStep();
// Decision coverage: guard tc 1 != guard tc 2
// Condition coverage: foreach var in inputs if var = flipVar
// ctx.mkNot(ctx.mkEq(var,flipVar)) else ctx.mkEq
return this.testSuite;
}
// Unique cause
private void verificationStep() {
// All atoms are verified
if(atoms.size() == verifiedAtoms.size()) {
System.out.println("Verified!");
return;
}
Context ctx = new Context();
// Feed z3 with existing test cases
addExistingDataToZ3(ctx);
// 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);
BoolExpr orClause = ctx.mkFalse();
// Iterate over all of the existing test cases
for(TestCase testCase : testSuite.getTestCases()) {
// createTestCase adds the new test case to the suite
if(testCase.getName() == newTC.getName()) {
continue;
}
// All possibilities for cc for this test case and the new one
BoolExpr cc = ctx.mkFalse();
// The second step contains the atoms and the taken branch
TestStep secondTestStep = testCase.getTestSteps().get(1);
// The only simulated output is the taken branch and is stored as BoolConst
BoolConst oldTakenBranchAf3Expr =
(BoolConst)secondTestStep.getOutputs().get(0).getSimulatedValue();
BoolExpr oldTakenBranch = ctx.mkBool(oldTakenBranchAf3Expr.getValue());
BoolExpr newTakenBranch = ctx.mkBoolConst(newTC.getName() + GUARD);
// Taken branches should differ for condition coverage
BoolExpr dc = ctx.mkNot(ctx.mkEq(oldTakenBranch, newTakenBranch));
FormalRequirementMCDC req = spec.getFormalRequirementMCDC();
EList<TestCase> initialTCs = initialSuite.getTestCases();
if(initialTCs != null && !initialTCs.isEmpty()) {
for(TestCase testCase : initialTCs) {
//
BoolExpr atomsAnd = ctx.mkTrue();
// Only one of the atoms should be different
for(int i = 0; i < atoms.size(); i++) {
BoolExpr andClause = ctx.mkTrue();
FunctionCall atom = atoms.get(i);
if(verifiedAtoms.contains(atom)) {
continue;
}
// Atoms are sorted in the inputs of the second step
List<TestInput> oldAtoms = secondTestStep.getInputs();
for(int j = 0; j < atoms.size(); j++) {
// The value of the atoms are stored as BoolConsts
BoolConst oldAtomAf3Expr = (BoolConst)oldAtoms.get(j).getValue();
BoolExpr oldAtom = ctx.mkBool(oldAtomAf3Expr.getValue());
BoolExpr newAtom =
(BoolExpr)toZ3(newTC.getName(), ctx, atoms.get(j), component);
BoolExpr same = ctx.mkEq(newAtom, oldAtom);
if(i == j) {
same = ctx.mkNot(same);
}
andClause = ctx.mkAnd(andClause, same);
}
cc = ctx.mkOr(cc, andClause);
}
// The branch must be different for cc
cc = ctx.mkAnd(cc, dc);
// cc for this test case is added to the overall orClause
orClause = ctx.mkOr(orClause, cc);
}
// 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(orClause, atomsClause, (BoolExpr)reqZ3);
if(opt.Check() == Status.SATISFIABLE) {
retrieveValues(ctx, newTC, opt);
}
checkTestSuite();
verificationStep();
}
/**
* @param ctx
*/
private void addExistingDataToZ3(Context ctx) {
for(TestCase testCase : testSuite.getTestCases()) {
// Already existing values of variables from old test cases are added to ctx
// The first step contains inputs and outputs
TestStep firstTestStep = testCase.getTestSteps().get(0);
for(TestInput testInput : firstTestStep.getInputs()) {
ITerm value = testInput.getValue();
toZ3(testCase.getName(), ctx, value, component);
}
for(TestOutput testOutput : firstTestStep.getOutputs()) {
ITerm value = testOutput.getSimulatedValue();
toZ3(testCase.getName(), ctx, value, component);
}
// The second step contains the atoms and the taken branch
// The inputs contain the atoms
TestStep secondTestStep = testCase.getTestSteps().get(1);
for(TestInput testInput : secondTestStep.getInputs()) {
ITerm value = testInput.getValue();
toZ3(testCase.getName(), ctx, value, component);
}
// The only simulated output is the taken branch
toZ3(testCase.getName(), ctx, secondTestStep.getOutputs().get(0).getSimulatedValue(),
component);
}
}
/**
* @param ctx
* @param newTC
* @param opt
*/
private void retrieveValues(Context ctx, TestCase newTC, Optimize opt) {
Model model = opt.getModel();
TestStep newTCFirstTestStep = createTestStep(newTC, null);
List<TestInput> newTCInputs = newTCFirstTestStep.getInputs();
List<TestOutput> newTCOutputs = newTCFirstTestStep.getOutputs();
TestStep newTCSecondTestStep = createTestStep(newTC, null);
List<TestInput> newTCAtoms = newTCSecondTestStep.getInputs();
List<TestOutput> newTCTakenBranch = newTCSecondTestStep.getOutputs();
// TODO factorize (outputPorts)
// Inputs.
for(InputPort inputPort : testSuite.getInputPorts()) {
TestInput testInput = TestingModelFactory.eINSTANCE.createTestInput();
IType type = inputPort.getVariableType();
String identifier = inputPort.getName();
Expr toBeRetrieved, result;
if(type instanceof TBool) {
toBeRetrieved = ctx.mkBoolConst(newTC.getName() + identifier);
result = model.getConstInterp(toBeRetrieved);
if(result.toString().equals("true")) {
testInput.setValue(boolConst(true));
newTCInputs.add(testInput);
continue;
}
if(result.toString().equals("false")) {
testInput.setValue(boolConst(false));
newTCInputs.add(testInput);
continue;
}
System.out.println("This should not be reached!");
}
if(type instanceof TInt) {
toBeRetrieved = ctx.mkIntConst(newTC.getName() + identifier);
result = model.getConstInterp(toBeRetrieved);
int r = Integer.parseInt(result.toString());
testInput.setValue(intConst(r));
newTCInputs.add(testInput);
continue;
}
if(type instanceof TDouble) {
toBeRetrieved = ctx.mkRealConst(newTC.getName() + identifier);
result = model.getConstInterp(toBeRetrieved);
double r = Double.parseDouble(result.toString());
testInput.setValue(doubleConst(r));
newTCInputs.add(testInput);
continue;
}
System.out.println("This should not be reached!");
}
// TODO factorize (inputPorts)
// Outputs
for(OutputPort outputPort : testSuite.getOutputPorts()) {
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);
result = model.getConstInterp(toBeRetrieved);
if(result.toString().equals("true")) {
testOutput.setSimulatedValue(boolConst(true));
newTCOutputs.add(testOutput);
continue;
}
if(result.toString().equals("false")) {
testOutput.setSimulatedValue(boolConst(false));
newTCOutputs.add(testOutput);
continue;
}
System.out.println("This should not be reached!");
}
if(type instanceof TInt) {
toBeRetrieved = ctx.mkIntConst(newTC.getName() + identifier);
result = model.getConstInterp(toBeRetrieved);
int r = Integer.parseInt(result.toString());
testOutput.setSimulatedValue(intConst(r));
newTCOutputs.add(testOutput);
continue;
}
if(type instanceof TDouble) {
toBeRetrieved = ctx.mkRealConst(newTC.getName() + identifier);
result = model.getConstInterp(toBeRetrieved);
double r = Double.parseDouble(result.toString());
testOutput.setSimulatedValue(doubleConst(r));
newTCOutputs.add(testOutput);
continue;
}
System.out.println("This should not be reached!");
}
// Atoms.
for(int i = 0; i < atoms.size(); i++) {
TestInput testInput = TestingModelFactory.eINSTANCE.createTestInput();
BoolExpr toBeRetrieved = ctx.mkBoolConst(newTC.getName() + "_atom_" + i);
Expr result = model.getConstInterp(toBeRetrieved);
if(result.toString().equals("true")) {
testInput.setValue(boolConst(true));
newTCAtoms.add(testInput);
continue;
}
if(result.toString().equals("false")) {
testInput.setValue(boolConst(false));
newTCAtoms.add(testInput);
continue;
}
System.out.println("This should not be reached!");
}
// Taken branch.
TestOutput testOutput = TestingModelFactory.eINSTANCE.createTestOutput();
BoolExpr toBeRetrieved = ctx.mkBoolConst(newTC.getName() + GUARD);
Expr result = model.getConstInterp(toBeRetrieved);
if(result.toString().equals("true")) {
testOutput.setSimulatedValue(boolConst(true));
newTCTakenBranch.add(testOutput);
return;
}
if(result.toString().equals("false")) {
testOutput.setSimulatedValue(boolConst(false));
newTCTakenBranch.add(testOutput);
return;
}
System.out.println("This should not be reached!");
}
private void checkTestSuite() {
EList<TestCase> testCases = testSuite.getTestCases();
for(int i = 0; i < testCases.size() - 1; i++) {
TestCase firstTestCase = testCases.get(i);
// First chosen branch
BoolConst firstBranch = (BoolConst)firstTestCase.getTestSteps().get(1).getOutputs()
.get(0).getSimulatedValue();
for(int j = i + 1; j < testCases.size(); j++) {
TestCase secondTestCase = testCases.get(j);
// Second chosen branch
BoolConst secondBranch = (BoolConst)secondTestCase.getTestSteps().get(1)
.getOutputs().get(0).getSimulatedValue();
// Different chosen branches: Check atoms for cc
if(firstBranch.getValue() != secondBranch.getValue()) {
// Check if any cc is verified by a pair
for(int k = 0; k < atoms.size(); k++) {
if(verifiedAtoms.contains(atoms.get(k))) {
continue;
}
boolean cc = true;
EList<TestInput> firstAtoms =
firstTestCase.getTestSteps().get(1).getInputs();
EList<TestInput> secondAtoms =
secondTestCase.getTestSteps().get(1).getInputs();
for(int l = 0; l < atoms.size(); l++) {
BoolConst tk1Atom = (BoolConst)firstAtoms.get(l).getValue();
BoolConst tk2Atom = (BoolConst)secondAtoms.get(l).getValue();
if(k == l) {
cc = cc && tk1Atom.getValue() != tk2Atom.getValue();
} else {
cc = cc && tk1Atom.getValue() == tk2Atom.getValue();
}
}
if(cc) {
verifiedAtoms.add(atoms.get(k));
independencePairs.add(new ImmutablePair<TestCase, TestCase>(
firstTestCase, secondTestCase));
}
}
}
}
}
return null;
}
}
......@@ -346,6 +346,8 @@ public class TestingModelElementFactory {
req.setGuard(guard);
req.setThenBlock(thenBlock);
req.setElseBlock(elseBlock);
req.getInputs().addAll(inputs);
req.getOutputs().addAll(outputs);
return req;
}
return null;
......
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