Skip to content

GitLab

Commit 68a0aeb0 authored by Johannes Eder's avatar Johannes Eder
Browse files

No commit message 

No commit message
parent 5ac0368d
Expand all Hide whitespace changes
Inline Side-by-side
org.fortiss.af3.exploration/trunk/META-INF/MANIFEST.MF
View file @ 68a0aeb0
......@@ -67,7 +67,6 @@ Require-Bundle: org.eclipse.core.runtime,
org.fortiss.af3.platform;visibility:=reexport,
org.fortiss.af3.project;visibility:=reexport,
org.fortiss.af3.safety;bundle-version="2.9.0";visibility:=reexport,
org.fortiss.tooling.kernel;visibility:=reexport,
org.fortiss.af3.deployment;bundle-version="2.9.0";visibility:=reexport,
org.fortiss.af3.msc;bundle-version="2.9.0";visibility:=reexport,
org.fortiss.tooling.kernel.ui;bundle-version="2.9.0";visibility:=reexport,
......
org.fortiss.af3.exploration/trunk/test-src/test/org/fortiss/af3/exploration/DSLtoSMT.java
View file @ 68a0aeb0
......@@ -17,20 +17,11 @@ $Id: codetemplates.xml 1 2011-01-01 00:00:01Z hoelzl $
+--------------------------------------------------------------------------*/
package test.org.fortiss.af3.exploration;
import static com.microsoft.z3.Z3javaAPIWrapper.createAddition;
import static com.microsoft.z3.Z3javaAPIWrapper.createDivision;
import static com.microsoft.z3.Z3javaAPIWrapper.createMultiplication;
import static com.microsoft.z3.Z3javaAPIWrapper.createSubtraction;
import java.util.ArrayList;
import model.BinaryOperator;
import model.Expression;
import model.ModelElementExpression;
import model.ModelElementLiteral;
import model.ModelFactory;
import model.Set;
import model.UnaryOperator;
import model.arithmetic.ArithmeticExpression;
import model.arithmetic.ArithmeticFactory;
import model.arithmetic.Div;
......@@ -39,25 +30,26 @@ import model.arithmetic.ModelElementPropertyLiteral;
import model.arithmetic.Mul;
import model.arithmetic.Plus;
import model.boolean_.BooleanFactory;
import model.boolean_.Implies;
import model.boolean_.ForAll;
import model.boolean_.QuantifierExpression;
import model.boolean_.allocation.Allocation;
import model.boolean_.allocation.AllocationFactory;
import model.boolean_.comparison.ComparisonFactory;
import model.boolean_.comparison.Less;
import org.fortiss.af3.component.utils.ComponentModelElementFactory;
import org.fortiss.af3.platform.model.annotation.MemoryPerNode;
import org.fortiss.af3.platform.utils.PlatformModelElementFactory;
import org.eclipse.emf.common.util.EList;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.component.model.ComponentArchitecture;
import org.fortiss.af3.component.model.annotation.MemoryRequirement;
import org.fortiss.af3.exploration.ExplorationActivator;
import org.fortiss.af3.project.model.FileProject;
import org.fortiss.af3.project.utils.ProjectUtils;
import org.fortiss.tooling.base.annotation.AnnotationEntry;
import org.fortiss.tooling.base.annotation.IAnnotationValueService;
import org.fortiss.tooling.base.model.element.IAnnotatedSpecification;
import org.fortiss.tooling.base.model.element.IModelElement;
import org.junit.Before;
import org.fortiss.tooling.kernel.utils.EcoreUtils;
import org.junit.Test;
import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Z3javaAPIWrapper;
/**
*
......@@ -71,96 +63,97 @@ public class DSLtoSMT {
private QuantifierExpression forAllQuantifier2;
private QuantifierExpression forAllQuantifier;
/** Set up a sample constraint. */
@Before
public void setup3() {
// x+y < a+b
forAllQuantifier = BooleanFactory.eINSTANCE.createForAll();
forAllQuantifier2 = BooleanFactory.eINSTANCE.createForAll();
Set set = ModelFactory.eINSTANCE.createSet();
Set set2 = ModelFactory.eINSTANCE.createSet();
forAllQuantifier.setSet(set);
forAllQuantifier2.setSet(set2);
forAllQuantifier.setExpression(forAllQuantifier2);
for(int i = 0; i < 7; i++) {
ModelElementExpression modelElementExpression =
ModelFactory.eINSTANCE.createModelElementExpression();
if(i % 2 == 0) {
forAllQuantifier.getSet().getEntries()
.add(ComponentModelElementFactory.createComponent());
} else {
forAllQuantifier2.getSet().getEntries()
.add(PlatformModelElementFactory.createGenericExecutionUnit("ECU" + i));
}
}
Implies implies = BooleanFactory.eINSTANCE.createImplies();
Less less = ComparisonFactory.eINSTANCE.createLess();
ModelElementPropertyLiteral model3 =
ArithmeticFactory.eINSTANCE.createModelElementPropertyLiteral();
ModelElementPropertyLiteral model4 =
ArithmeticFactory.eINSTANCE.createModelElementPropertyLiteral();
model3.setSetReference(set);
model3.setSpecificationType(MemoryPerNode.class);
model4.setSetReference(set2);
model4.setSpecificationType(MemoryPerNode.class);
less.setLeft(model3);
less.setRight(model4);
Allocation allocation = AllocationFactory.eINSTANCE.createAllocation();
ModelElementLiteral model1 = ModelFactory.eINSTANCE.createModelElementLiteral();
model1.setSetReference(set2);
ModelElementLiteral model2 = ModelFactory.eINSTANCE.createModelElementLiteral();
model2.setSetReference(set);
allocation.setLeft(model1);
allocation.setRight(model2);
implies.setLeft(allocation);
implies.setRight(less);
forAllQuantifier2.setExpression(implies);
}
// /** Set up a sample constraint. */
// @Before
// public void setup3() {
//
// // x+y < a+b
// forAllQuantifier = BooleanFactory.eINSTANCE.createForAll();
// forAllQuantifier2 = BooleanFactory.eINSTANCE.createForAll();
//
// Set set = ModelFactory.eINSTANCE.createSet();
// Set set2 = ModelFactory.eINSTANCE.createSet();
//
// forAllQuantifier.setSet(set);
// forAllQuantifier2.setSet(set2);
//
// forAllQuantifier.setExpression(forAllQuantifier2);
//
// for(int i = 0; i < 7; i++) {
// ModelElementExpression modelElementExpression =
// ModelFactory.eINSTANCE.createModelElementExpression();
// if(i % 2 == 0) {
// forAllQuantifier.getSet().getEntries()
// .add(ComponentModelElementFactory.createComponent());
// } else {
// forAllQuantifier2.getSet().getEntries()
// .add(PlatformModelElementFactory.createGenericExecutionUnit("ECU" + i));
// }
// }
//
// Implies implies = BooleanFactory.eINSTANCE.createImplies();
//
// Less less = ComparisonFactory.eINSTANCE.createLess();
// ModelElementPropertyLiteral model3 =
// ArithmeticFactory.eINSTANCE.createModelElementPropertyLiteral();
// ModelElementPropertyLiteral model4 =
// ArithmeticFactory.eINSTANCE.createModelElementPropertyLiteral();
// model3.setSetReference(set);
// // model3.setSpecificationType(MemoryPerNode.class);
// model4.setSetReference(set2);
// // model4.setSpecificationType(MemoryPerNode.class);
// less.setLeft(model3);
// less.setRight(model4);
//
// Allocation allocation = AllocationFactory.eINSTANCE.createAllocation();
// ModelElementLiteral model1 = ModelFactory.eINSTANCE.createModelElementLiteral();
// model1.setSetReference(set2);
// ModelElementLiteral model2 = ModelFactory.eINSTANCE.createModelElementLiteral();
// model2.setSetReference(set);
// allocation.setLeft(model1);
// allocation.setRight(model2);
//
// implies.setLeft(allocation);
// implies.setRight(less);
//
// forAllQuantifier2.setExpression(implies);
//
// }
/** Returns an {@link Expression} as a list of all leafs in the expression tree */
public static ArrayList<? extends Expression> expressionToList(Expression expression) {
if(expression instanceof QuantifierExpression) {
ArrayList<? extends Expression> expr =
expressionToList(((QuantifierExpression)expression).getExpression());
ArrayList<Expression> result = new ArrayList<>();
result.add(expression);
// result.addAll(((QuantifierExpression)expression).getSe);
result.addAll(expr);
return result;
} else if(expression instanceof BinaryOperator<?>) {
ArrayList<? extends Expression> left =
expressionToList(((BinaryOperator<?>)expression).getLeft());
ArrayList<? extends Expression> right =
expressionToList(((BinaryOperator<?>)expression).getRight());
ArrayList<Expression> result = new ArrayList<>();
result.addAll(left);
result.add(expression);
result.addAll(right);
return result;
} else if(expression instanceof UnaryOperator<?>) {
ArrayList<? extends Expression> right =
expressionToList(((UnaryOperator<?>)expression).getRight());
ArrayList<Expression> result = new ArrayList<>();
result.add(expression);
result.addAll(right);
return right;
} else {
ArrayList<Expression> list = new ArrayList<Expression>();
list.add(expression);
return list;
}
}
//
// /** Returns an {@link Expression} as a list of all leafs in the expression tree */
// public static ArrayList<? extends Expression> expressionToList(Expression expression) {
// if(expression instanceof QuantifierExpression) {
// ArrayList<? extends Expression> expr =
// expressionToList(((QuantifierExpression)expression).getExpression());
// ArrayList<Expression> result = new ArrayList<>();
// result.add(expression);
// // result.addAll(((QuantifierExpression)expression).getSe);
// result.addAll(expr);
// return result;
// } else if(expression instanceof BinaryOperator<?>) {
// ArrayList<? extends Expression> left =
// expressionToList(((BinaryOperator<?>)expression).getLeft());
// ArrayList<? extends Expression> right =
// expressionToList(((BinaryOperator<?>)expression).getRight());
// ArrayList<Expression> result = new ArrayList<>();
// result.addAll(left);
// result.add(expression);
// result.addAll(right);
// return result;
// } else if(expression instanceof UnaryOperator<?>) {
// ArrayList<? extends Expression> right =
// expressionToList(((UnaryOperator<?>)expression).getRight());
// ArrayList<Expression> result = new ArrayList<>();
// result.add(expression);
// result.addAll(right);
// return right;
// } else {
// ArrayList<Expression> list = new ArrayList<Expression>();
// list.add(expression);
// return list;
// }
// }
private Context context = new Context();
......@@ -174,13 +167,13 @@ public class DSLtoSMT {
toSMT((ArithmeticExpression)((BinaryOperator<?>)arithExpr).getRight(),
elementSet1, elementSet2);
if(arithExpr instanceof Plus) {
return createAddition(context, left, right);
return Z3javaAPIWrapper.createAddition(context, left, right);
} else if(arithExpr instanceof Minus) {
return createSubtraction(context, left, right);
return Z3javaAPIWrapper.createSubtraction(context, left, right);
} else if(arithExpr instanceof Div) {
return createDivision(context, left, right);
return Z3javaAPIWrapper.createDivision(context, left, right);
} else if(arithExpr instanceof Mul) {
return createMultiplication(context, left, right);
return Z3javaAPIWrapper.createMultiplication(context, left, right);
}
} else if(arithExpr instanceof ModelElementPropertyLiteral) {
if(((ModelElementPropertyLiteral)arithExpr).getSetReference().getEntries()
......@@ -190,11 +183,36 @@ public class DSLtoSMT {
((ModelElementPropertyLiteral)arithExpr).getSpecificationType();
AnnotationEntry annotationEntry =
IAnnotationValueService.INSTANCE.getAnnotationEntry(elementSet1);
Object annotationValueProvider = annotationEntry.getSpecificationValue(eClass);// etAnnotationValueProvider(eClass);
Object annotationValue = annotationEntry.getSpecificationValue(eClass);
if(annotationValue instanceof String) {
// TODO
} else {
// if it is not a string it must be a number
Double value = (Double)annotationValue;
}
} else if(((ModelElementPropertyLiteral)arithExpr).getSetReference().getEntries()
.contains(elementSet2)) {
// TODO copy paste code
// belongs to set 2
Class<? extends IAnnotatedSpecification> eClass =
((ModelElementPropertyLiteral)arithExpr).getSpecificationType();
AnnotationEntry annotationEntry =
IAnnotationValueService.INSTANCE.getAnnotationEntry(elementSet1);
Object annotationValue = annotationEntry.getSpecificationValue(eClass);
if(annotationValue instanceof String) {
// TODO
// make const expr with sort=annotationValue
} else {
// if it is not a string it must be a number
Double value = (Double)annotationValue;
}
}
} else if(arithExpr instanceof ModelElementLiteral) {
// to function declaration
}
return null;
......@@ -204,8 +222,61 @@ public class DSLtoSMT {
*
*/
@Test
private void test() {
// TODO Auto-generated method stub
public void test() {
Expression exp = createExp();
}
/**
*
*/
private Expression createExp() {
FileProject project =
ProjectUtils.loadProjectFromPlugin(ExplorationActivator.PLUGIN_ID,
"test-data/ConstraintProject.af3_23", true);
// schedule = findContentElementByNameAndClass(project, "Schedule", Schedule.class);
EList<ComponentArchitecture> cas =
EcoreUtils.getChildrenWithType(project, ComponentArchitecture.class);
// EList<PlatformArchitecture> pas = getChildrenWithType(project,
// PlatformArchitecture.class);
EList<Component> components = EcoreUtils.getChildrenWithType(cas.get(0), Component.class);
Set set1 = ModelFactory.eINSTANCE.createSet();
Set set2 = ModelFactory.eINSTANCE.createSet();
int i = 0;
for(Component c : components) {
// skip first element
if(i == 0) {
continue;
}
if(i % 2 == 0) {
set1.getEntries().add(c);
} else {
set2.getEntries().add(c);
}
++i;
}
Plus plus = ArithmeticFactory.eINSTANCE.createPlus();
ModelElementPropertyLiteral elementPropertyLiteral =
ArithmeticFactory.eINSTANCE.createModelElementPropertyLiteral();
elementPropertyLiteral.setSetReference(set1);
elementPropertyLiteral.setSpecificationType(MemoryRequirement.class);
ModelElementPropertyLiteral elementPropertyLiteral2 =
ArithmeticFactory.eINSTANCE.createModelElementPropertyLiteral();
elementPropertyLiteral2.setSetReference(set2);
elementPropertyLiteral2.setSpecificationType(MemoryRequirement.class);
plus.setLeft(elementPropertyLiteral);
plus.setRight(elementPropertyLiteral2);
ForAll forAll = BooleanFactory.eINSTANCE.createForAll();
forAll.setSet(set1);
ForAll forAll2 = BooleanFactory.eINSTANCE.createForAll();
forAll2.setSet(set2);
forAll.setExpression(forAll2);
return plus;
}
}
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