Commit 9b799cd4 authored by Hernan Ponce de Leon's avatar Hernan Ponce de Leon
Browse files

Merge branch '3465-IStatementTerm_toZ3' of https://git.fortiss.org/af3/af3.git...

Merge branch '3465-IStatementTerm_toZ3' of https://git.fortiss.org/af3/af3.git into 3465-IStatementTerm_toZ3
parents 8318b00d 52e8dc01
MCDCUtils.java 72786d523866026c2420e04e167b81f6d2ab742a YELLOW
MCDCUtils.java 8e4c09ba90443f0e369e52de21d3c1dcb6701828 YELLOW
......@@ -42,7 +42,6 @@ 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.project.model.typesystem.VarBase;
import org.fortiss.af3.testing.model.mcdc.FormalRequirementMCDC;
import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.BoolExpr;
......
......@@ -15,9 +15,12 @@
+--------------------------------------------------------------------------*/
package test.org.fortiss.af3.testing.mcdc;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.and;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.createVar;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.greaterThan;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.intConst;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.lowerEqual;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.lowerThan;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.or;
import static org.fortiss.af3.testing.mcdc.MCDCUtils.getAtomsFromGuardMCDC;
import org.fortiss.af3.expression.model.terms.FunctionCall;
......@@ -37,21 +40,25 @@ public class TestGetAtomsFromGuardMCDC {
IExpressionTerm guard, a, b;
Var v1 = createVar("v1");
Var v2 = createVar("v2");
a = lowerEqual(v1, intConst(42));
b = ExpressionModelElementFactory.greaterThan(intConst(42), v2);
guard = ExpressionModelElementFactory.and(a, b);
a = lowerThan(v1, intConst(42));
b = or(greaterThan(v2, intConst(42)), ExpressionModelElementFactory.equal(v1, v2));
guard = and(a, b);
System.out.println(guard);
System.out.println();
System.out.println("Guard");
for(FunctionCall functionCall : getAtomsFromGuardMCDC(guard)) {
System.out.println(functionCall);
}
System.out.println();
System.out.println("a");
for(FunctionCall functionCall : getAtomsFromGuardMCDC(a)) {
System.out.println(functionCall);
}
System.out.println();
System.out.println("b");
for(FunctionCall functionCall : getAtomsFromGuardMCDC(b)) {
System.out.println(functionCall);
......
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