Commit 5855897f authored by Ludwig Dickmanns's avatar Ludwig Dickmanns
Browse files

MCDC: Test case generation

* McdcTestSuiteGenerator: Initial implementation generate() (Not tested
yet). Added a method checking the test suite for verified atoms
(superficially tested).
* MCDCUtils: Added name for the guard for the retrieval of the taken
branch.
* TestingModelElementFactory: Inputs and outputs are now added to the
FormalRequirementMCDC


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

Signed-off-by: Ludwig Dickmanns's avatarLudwig Dickmanns <dickmanns@fortiss.org>
parent f8a08860
<?xml version="1.0" encoding="UTF-8"?>
<genmodel:GenModel xmi:version="2.0"
xmlns:xmi="http://www.omg.org/XMI"
xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore"
xmlns:genmodel="http://www.eclipse.org/emf/2002/GenModel"
copyrightText="(c) 2017 fortiss GmbH. GENERATED CODE: Do not edit, see Ecore metamodel instead!"
modelDirectory="/org.fortiss.af3.project/generated-src"
editDirectory="/org.fortiss.af3.project.edit/generated-src"
editorDirectory="/org.fortiss.af3.project.editor/generated-src"
modelPluginID="org.fortiss.af3.project" modelName="Model"
modelPluginClass=""
editPluginClass="org.fortiss.af3.project.model.provider.ModelEditPlugin"
editorPluginClass="org.fortiss.af3.project.model.presentation.ModelEditorPlugin"
testsDirectory="/org.fortiss.af3.project.tests/test-src"
importerID="org.eclipse.emf.importer.ecore" containmentProxies="true"
complianceLevel="8.0" copyrightFields="false"
usedGenPackages="platform:/resource/org.fortiss.tooling.kernel/model/kernel.genmodel#//model platform:/resource/org.fortiss.tooling.base/model/base.genmodel#//model">
<foreignModel>project.ecore</foreignModel>
<genPackages prefix="AF3Project"
basePackage="org.fortiss.af3.project" disposableProviderFactory="true"
ecorePackage="project.ecore#/">
<genClasses
ecoreClass="project.ecore#//ProjectConfiguration">
<genFeatures property="None" children="true"
createChild="true"
ecoreFeature="ecore:EReference project.ecore#//ProjectConfiguration/configurationElements" />
</genClasses>
<genClasses image="false"
ecoreClass="project.ecore#//IProjectConfigurationElement" />
<genClasses ecoreClass="project.ecore#//FileProject">
<genFeatures property="None" children="true"
createChild="true"
ecoreFeature="ecore:EReference project.ecore#//FileProject/rootElements" />
<genFeatures createChild="false"
ecoreFeature="ecore:EAttribute project.ecore#//FileProject/af3Version" />
</genClasses>
<genClasses ecoreClass="project.ecore#//FileLibrary" />
<genClasses
ecoreClass="project.ecore#//LibraryProjectConfiguration" />
<genClasses
ecoreClass="project.ecore#//ParameterDefinition">
<genFeatures createChild="false"
ecoreFeature="ecore:EAttribute project.ecore#//ParameterDefinition/value" />
<genFeatures property="None" children="true"
createChild="true"
ecoreFeature="ecore:EReference project.ecore#//ParameterDefinition/type" />
</genClasses>
<genClasses image="false"
ecoreClass="project.ecore#//ITraceableArtifact" />
<nestedGenPackages prefix="Configuration"
basePackage="org.fortiss.af3.project.model"
disposableProviderFactory="true"
ecorePackage="project.ecore#//configuration">
<genClasses
ecoreClass="project.ecore#//configuration/TypeSystemConfiguration">
<genFeatures property="None" children="true"
createChild="true"
ecoreFeature="ecore:EReference project.ecore#//configuration/TypeSystemConfiguration/typesystem" />
</genClasses>
<genClasses
ecoreClass="project.ecore#//configuration/DevelopmentProcessConfiguration">
<genFeatures property="None" children="true"
createChild="true"
ecoreFeature="ecore:EReference project.ecore#//configuration/DevelopmentProcessConfiguration/development" />
</genClasses>
</nestedGenPackages>
<nestedGenPackages prefix="Typesystem"
basePackage="org.fortiss.af3.project.model"
disposableProviderFactory="true"
ecorePackage="project.ecore#//typesystem">
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/ITypeSystem" />
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/ITypeScope">
<genOperations
ecoreOperation="project.ecore#//typesystem/ITypeScope/getDefinitionElement">
<genParameters
ecoreParameter="project.ecore#//typesystem/ITypeScope/getDefinitionElement/type" />
</genOperations>
<genOperations
ecoreOperation="project.ecore#//typesystem/ITypeScope/getITypeDefinitions" />
</genClasses>
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/ITypeDefinition">
<genOperations
ecoreOperation="project.ecore#//typesystem/ITypeDefinition/createIType" />
</genClasses>
<genClasses image="false"
<genmodel:GenModel xmi:version="2.0" xmlns:xmi="http://www.omg.org/XMI" xmlns:ecore="http://www.eclipse.org/emf/2002/Ecore"
xmlns:genmodel="http://www.eclipse.org/emf/2002/GenModel" copyrightText="(c) 2017 fortiss GmbH. GENERATED CODE: Do not edit, see Ecore metamodel instead!"
modelDirectory="/org.fortiss.af3.project/generated-src" editDirectory="/org.fortiss.af3.project.edit/generated-src"
editorDirectory="/org.fortiss.af3.project.editor/generated-src" modelPluginID="org.fortiss.af3.project"
modelName="Model" modelPluginClass="" editPluginClass="org.fortiss.af3.project.model.provider.ModelEditPlugin"
editorPluginClass="org.fortiss.af3.project.model.presentation.ModelEditorPlugin"
testsDirectory="/org.fortiss.af3.project.tests/test-src" importerID="org.eclipse.emf.importer.ecore"
containmentProxies="true" complianceLevel="8.0" copyrightFields="false" usedGenPackages="platform:/resource/org.fortiss.tooling.kernel/model/kernel.genmodel#//model platform:/resource/org.fortiss.tooling.base/model/base.genmodel#//model">
<foreignModel>project.ecore</foreignModel>
<genPackages prefix="AF3Project" basePackage="org.fortiss.af3.project" disposableProviderFactory="true"
ecorePackage="project.ecore#/">
<genClasses ecoreClass="project.ecore#//ProjectConfiguration">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference project.ecore#//ProjectConfiguration/configurationElements"/>
</genClasses>
<genClasses image="false" ecoreClass="project.ecore#//IProjectConfigurationElement"/>
<genClasses ecoreClass="project.ecore#//FileProject">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference project.ecore#//FileProject/rootElements"/>
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute project.ecore#//FileProject/af3Version"/>
</genClasses>
<genClasses ecoreClass="project.ecore#//FileLibrary"/>
<genClasses ecoreClass="project.ecore#//LibraryProjectConfiguration"/>
<genClasses ecoreClass="project.ecore#//ParameterDefinition">
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute project.ecore#//ParameterDefinition/value"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference project.ecore#//ParameterDefinition/type"/>
</genClasses>
<genClasses image="false" ecoreClass="project.ecore#//ITraceableArtifact"/>
<nestedGenPackages prefix="Configuration" basePackage="org.fortiss.af3.project.model"
disposableProviderFactory="true" ecorePackage="project.ecore#//configuration">
<genClasses ecoreClass="project.ecore#//configuration/TypeSystemConfiguration">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference project.ecore#//configuration/TypeSystemConfiguration/typesystem"/>
</genClasses>
<genClasses ecoreClass="project.ecore#//configuration/DevelopmentProcessConfiguration">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference project.ecore#//configuration/DevelopmentProcessConfiguration/development"/>
</genClasses>
</nestedGenPackages>
<nestedGenPackages prefix="Typesystem" basePackage="org.fortiss.af3.project.model"
disposableProviderFactory="true" ecorePackage="project.ecore#//typesystem">
<genClasses image="false" ecoreClass="project.ecore#//typesystem/ITypeSystem"/>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/ITypeScope">
<genOperations ecoreOperation="project.ecore#//typesystem/ITypeScope/getDefinitionElement">
<genParameters ecoreParameter="project.ecore#//typesystem/ITypeScope/getDefinitionElement/type"/>
</genOperations>
<genOperations ecoreOperation="project.ecore#//typesystem/ITypeScope/getITypeDefinitions"/>
</genClasses>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/ITypeDefinition">
<genOperations ecoreOperation="project.ecore#//typesystem/ITypeDefinition/createIType"/>
</genClasses>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/IType">
<genOperations ecoreOperation="project.ecore#//typesystem/IType/getTypeClassName"
body="return this.toString();"/>
<genOperations ecoreOperation="project.ecore#//typesystem/IType/isAssignableFrom"
body="return this.equals(other);">
<genOperations
ecoreOperation="project.ecore#//typesystem/IType/isAssignableFrom"
body="return this.equals(other);">
<genParameters
ecoreParameter="project.ecore#//typesystem/IType/isAssignableFrom/other" />
</genOperations>
</genClasses>
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/ITerm" />
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/IFunction" />
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/FunctionCallBase">
<genFeatures property="None" children="true"
createChild="true"
ecoreFeature="ecore:EReference project.ecore#//typesystem/FunctionCallBase/function" />
<genFeatures property="None" children="true"
createChild="true"
ecoreFeature="ecore:EReference project.ecore#//typesystem/FunctionCallBase/arguments" />
</genClasses>
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/IFunctionScope">
<genOperations
ecoreOperation="project.ecore#//typesystem/IFunctionScope/getDefinitionElement">
<genParameters
ecoreParameter="project.ecore#//typesystem/IFunctionScope/getDefinitionElement/type" />
</genOperations>
<genOperations
ecoreOperation="project.ecore#//typesystem/IFunctionScope/getIFunctionDefinitions" />
</genClasses>
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/IFunctionDefinition" />
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/IVariableScope">
<genOperations
ecoreOperation="project.ecore#//typesystem/IVariableScope/getDefinitionElement">
<genParameters
ecoreParameter="project.ecore#//typesystem/IVariableScope/getDefinitionElement/var" />
</genOperations>
<genOperations
ecoreOperation="project.ecore#//typesystem/IVariableScope/getParentVariableScope" />
</genClasses>
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/VarBase">
<genFeatures createChild="false"
ecoreFeature="ecore:EAttribute project.ecore#//typesystem/VarBase/identifier" />
</genClasses>
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/IVariableDefinition">
<genOperations
ecoreOperation="project.ecore#//typesystem/IVariableDefinition/getVariableType" />
<genOperations
ecoreOperation="project.ecore#//typesystem/IVariableDefinition/getVar" />
</genClasses>
<genClasses
ecoreClass="project.ecore#//typesystem/DummyTypeSystem" />
<genClasses image="false"
ecoreClass="project.ecore#//typesystem/IComplexVar">
<genOperations
ecoreOperation="project.ecore#//typesystem/IComplexVar/getVarDefinition">
<genParameters
ecoreParameter="project.ecore#//typesystem/IComplexVar/getVarDefinition/context" />
</genOperations>
<genOperations
ecoreOperation="project.ecore#//typesystem/IComplexVar/getVarType">
<genParameters
ecoreParameter="project.ecore#//typesystem/IComplexVar/getVarType/context" />
</genOperations>
</genClasses>
</nestedGenPackages>
<nestedGenPackages prefix="Development"
basePackage="org.fortiss.af3.project.model"
disposableProviderFactory="true"
ecorePackage="project.ecore#//development">
<genClasses image="false"
ecoreClass="project.ecore#//development/IDevelopmentProcess" />
<genClasses
ecoreClass="project.ecore#//development/DummyDevelopmentProcess" />
<genClasses
ecoreClass="project.ecore#//development/ConstraintBasedDevelopmentProcess" />
</nestedGenPackages>
<nestedGenPackages prefix="Execution"
basePackage="org.fortiss.af3.project.model"
disposableProviderFactory="true"
ecorePackage="project.ecore#//execution">
<genClasses
ecoreClass="project.ecore#//execution/ExecutionConfigurationStore">
<genFeatures property="None" children="true"
createChild="true"
ecoreFeature="ecore:EReference project.ecore#//execution/ExecutionConfigurationStore/configurations" />
</genClasses>
<genClasses
ecoreClass="project.ecore#//execution/ExecutionConfiguration">
<genFeatures property="None" children="true"
createChild="true"
ecoreFeature="ecore:EReference project.ecore#//execution/ExecutionConfiguration/configurationParts" />
</genClasses>
<genClasses
ecoreClass="project.ecore#//execution/ExecutionConfigurationPart" />
</nestedGenPackages>
</genPackages>
<genParameters ecoreParameter="project.ecore#//typesystem/IType/isAssignableFrom/other"/>
</genOperations>
</genClasses>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/ITerm"/>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/IFunction"/>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/FunctionCallBase">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference project.ecore#//typesystem/FunctionCallBase/function"/>
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference project.ecore#//typesystem/FunctionCallBase/arguments"/>
</genClasses>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/IFunctionScope">
<genOperations ecoreOperation="project.ecore#//typesystem/IFunctionScope/getDefinitionElement">
<genParameters ecoreParameter="project.ecore#//typesystem/IFunctionScope/getDefinitionElement/type"/>
</genOperations>
<genOperations ecoreOperation="project.ecore#//typesystem/IFunctionScope/getIFunctionDefinitions"/>
</genClasses>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/IFunctionDefinition"/>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/IVariableScope">
<genOperations ecoreOperation="project.ecore#//typesystem/IVariableScope/getDefinitionElement">
<genParameters ecoreParameter="project.ecore#//typesystem/IVariableScope/getDefinitionElement/var"/>
</genOperations>
<genOperations ecoreOperation="project.ecore#//typesystem/IVariableScope/getParentVariableScope"/>
</genClasses>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/VarBase">
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute project.ecore#//typesystem/VarBase/identifier"/>
</genClasses>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/IVariableDefinition">
<genOperations ecoreOperation="project.ecore#//typesystem/IVariableDefinition/getVariableType"/>
<genOperations ecoreOperation="project.ecore#//typesystem/IVariableDefinition/getVar"/>
</genClasses>
<genClasses ecoreClass="project.ecore#//typesystem/DummyTypeSystem"/>
<genClasses image="false" ecoreClass="project.ecore#//typesystem/IComplexVar">
<genOperations ecoreOperation="project.ecore#//typesystem/IComplexVar/getVarDefinition">
<genParameters ecoreParameter="project.ecore#//typesystem/IComplexVar/getVarDefinition/context"/>
</genOperations>
<genOperations ecoreOperation="project.ecore#//typesystem/IComplexVar/getVarType">
<genParameters ecoreParameter="project.ecore#//typesystem/IComplexVar/getVarType/context"/>
</genOperations>
</genClasses>
</nestedGenPackages>
<nestedGenPackages prefix="Development" basePackage="org.fortiss.af3.project.model"
disposableProviderFactory="true" ecorePackage="project.ecore#//development">
<genClasses image="false" ecoreClass="project.ecore#//development/IDevelopmentProcess"/>
<genClasses ecoreClass="project.ecore#//development/DummyDevelopmentProcess"/>
<genClasses ecoreClass="project.ecore#//development/ConstraintBasedDevelopmentProcess"/>
</nestedGenPackages>
<nestedGenPackages prefix="Execution" basePackage="org.fortiss.af3.project.model"
disposableProviderFactory="true" ecorePackage="project.ecore#//execution">
<genClasses ecoreClass="project.ecore#//execution/ExecutionConfigurationStore">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference project.ecore#//execution/ExecutionConfigurationStore/configurations"/>
</genClasses>
<genClasses ecoreClass="project.ecore#//execution/ExecutionConfiguration">
<genFeatures property="None" children="true" createChild="true" ecoreFeature="ecore:EReference project.ecore#//execution/ExecutionConfiguration/configurationParts"/>
</genClasses>
<genClasses ecoreClass="project.ecore#//execution/ExecutionConfigurationPart"/>
</nestedGenPackages>
</genPackages>
</genmodel:GenModel>
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);