wip stalled needs BooleanValue
diff --git a/plugins/org.eclipse.ocl.pivot/.settings/.api_filters b/plugins/org.eclipse.ocl.pivot/.settings/.api_filters
index 8c45f42..e5d3ef0 100644
--- a/plugins/org.eclipse.ocl.pivot/.settings/.api_filters
+++ b/plugins/org.eclipse.ocl.pivot/.settings/.api_filters
@@ -731,6 +731,14 @@
</message_arguments>
</filter>
</resource>
+ <resource path="src/org/eclipse/ocl/pivot/evaluation/EvaluationEnvironment.java" type="org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment">
+ <filter id="404000815">
+ <message_arguments>
+ <message_argument value="org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment"/>
+ <message_argument value="replaceInternal(VariableDeclaration, Object)"/>
+ </message_arguments>
+ </filter>
+ </resource>
<resource path="src/org/eclipse/ocl/pivot/evaluation/EvaluationVisitor.java" type="org.eclipse.ocl.pivot.evaluation.EvaluationVisitor">
<filter comment="Bug 512402 workaround" id="576725006">
<message_arguments>
@@ -739,6 +747,32 @@
</message_arguments>
</filter>
</resource>
+ <resource path="src/org/eclipse/ocl/pivot/evaluation/Executor.java" type="org.eclipse.ocl.pivot.evaluation.Executor">
+ <filter id="404000815">
+ <message_arguments>
+ <message_argument value="org.eclipse.ocl.pivot.evaluation.Executor"/>
+ <message_argument value="popSymbolicEvaluationEnvironment()"/>
+ </message_arguments>
+ </filter>
+ <filter id="404000815">
+ <message_arguments>
+ <message_argument value="org.eclipse.ocl.pivot.evaluation.Executor"/>
+ <message_argument value="pushEvaluationEnvironment(NamedElement, Object)"/>
+ </message_arguments>
+ </filter>
+ <filter id="404000815">
+ <message_arguments>
+ <message_argument value="org.eclipse.ocl.pivot.evaluation.Executor"/>
+ <message_argument value="pushSymbolicEvaluationEnvironment(NamedElement, Object, Object)"/>
+ </message_arguments>
+ </filter>
+ <filter id="404000815">
+ <message_arguments>
+ <message_argument value="org.eclipse.ocl.pivot.evaluation.Executor"/>
+ <message_argument value="resetCaches()"/>
+ </message_arguments>
+ </filter>
+ </resource>
<resource path="src/org/eclipse/ocl/pivot/internal/context/AbstractParserContext.java" type="org.eclipse.ocl.pivot.internal.context.AbstractParserContext">
<filter comment="Bug 512402 workaround" id="576725006">
<message_arguments>
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/CompositeSymbolicConstraintImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/CompositeSymbolicConstraintImpl.java
new file mode 100644
index 0000000..d4d16e9
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/CompositeSymbolicConstraintImpl.java
@@ -0,0 +1,95 @@
+/**
+ * Copyright (c) 2010, 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ * E.D.Willink - Initial API and implementation
+ */
+package org.eclipse.ocl.pivot.internal.values;
+
+import java.util.ArrayList;
+import java.util.List;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
+import org.eclipse.ocl.pivot.values.SymbolicOperator;
+
+/**
+ * @since 1.12
+ */
+public class CompositeSymbolicConstraintImpl extends SymbolicUnknownValueImpl implements SymbolicConstraint
+{
+ protected final @NonNull List<@NonNull SymbolicConstraint> symbolicConstraints = new ArrayList<>();
+
+ /**
+ * <!-- begin-user-doc -->
+ * <!-- end-user-doc -->
+ * @generated NOT
+ */
+ public CompositeSymbolicConstraintImpl() {
+ super(TypeId.BOOLEAN, false, false); // FIXME inherited maBeInvalid/Null redundant
+ }
+
+ public void add(@NonNull SymbolicConstraint symbolicConstraint) {
+ assert symbolicConstraint.getTypeId2() == typeId;
+ assert symbolicConstraint instanceof SymbolicConstraintImpl;
+ assert !symbolicConstraints.contains(symbolicConstraint);
+ symbolicConstraints.add(symbolicConstraint);
+ }
+
+ @Override
+ public @Nullable SymbolicOperator getSymbolicOperator() {
+ return null;
+ }
+
+ @Override
+ public @Nullable Object getSymbolicValue() {
+ return null;
+ }
+
+ @Override
+ public boolean mayBeInvalid() {
+ for (@NonNull SymbolicConstraint symbolicConstraint : symbolicConstraints) {
+ if (symbolicConstraint.mayBeInvalid()) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ @Override
+ public boolean mayBeNull() {
+ for (@NonNull SymbolicConstraint symbolicConstraint : symbolicConstraints) {
+ if (symbolicConstraint.mayBeNull()) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ @Override
+ public /*final*/ @NonNull String toString() {
+ StringBuilder s = new StringBuilder();
+ toString(s, 100);
+ return s.toString();
+ }
+
+ @Override
+ public void toString(@NonNull StringBuilder s, int lengthLimit) {
+ s.append("{");
+ boolean isFirst = true;
+ for (@NonNull SymbolicConstraint symbolicConstraint : symbolicConstraints) {
+ if (!isFirst) {
+ s.append(",");
+ }
+ s.append(symbolicConstraint);
+ isFirst = false;
+ }
+ s.append("}");
+ }
+}
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NullValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NullValueImpl.java
index b71f0c9..c446809 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NullValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/NullValueImpl.java
@@ -161,7 +161,7 @@
}
@Override
- public String toString() {
+ public @NonNull String toString() {
return "null";
}
} //NullValueImpl
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicConstraintImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicConstraintImpl.java
new file mode 100644
index 0000000..8d78c05
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicConstraintImpl.java
@@ -0,0 +1,82 @@
+/**
+ * Copyright (c) 2010, 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ * E.D.Willink - Initial API and implementation
+ */
+package org.eclipse.ocl.pivot.internal.values;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.utilities.ValueUtil;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
+import org.eclipse.ocl.pivot.values.SymbolicOperator;
+
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>Symbolic Value</b></em>'.
+ * @since 1.12
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class SymbolicConstraintImpl extends SymbolicUnknownValueImpl implements SymbolicConstraint
+{
+ protected final @NonNull SymbolicOperator symbolicOperator;
+ protected final @Nullable Object symbolicValue;
+
+ /**
+ * <!-- begin-user-doc -->
+ * <!-- end-user-doc -->
+ * @generated NOT
+ */
+ public SymbolicConstraintImpl(@NonNull TypeId typeId, boolean mayBeNull, boolean mayBeInvalid, @NonNull SymbolicOperator symbolicOperator, @Nullable Object symbolicValue) {
+ super(typeId, mayBeNull, mayBeInvalid);
+ this.symbolicOperator = symbolicOperator;
+ this.symbolicValue = symbolicValue;
+ }
+
+ @Override
+ public @NonNull SymbolicOperator getSymbolicOperator() {
+ return symbolicOperator;
+ }
+
+ @Override
+ public @Nullable Object getSymbolicValue() {
+ return symbolicValue;
+ }
+
+ @Override
+ public boolean mayBeInvalid() {
+ return ValueUtil.mayBeInvalid(symbolicValue);
+ }
+
+ @Override
+ public boolean mayBeNull() {
+ switch (symbolicOperator) {
+ case EQUALS: return ValueUtil.mayBeNull(symbolicValue);
+ case NOT_EQUALS: return !ValueUtil.mayBeNull(symbolicValue);
+ case COMPARE_TO: return false;
+ }
+ throw new UnsupportedOperationException(symbolicOperator.toString());
+ }
+
+ @Override
+ public /*final*/ @NonNull String toString() {
+ StringBuilder s = new StringBuilder();
+ toString(s, 100);
+ return s.toString();
+ }
+
+ @Override
+ public void toString(@NonNull StringBuilder s, int lengthLimit) {
+ s.append(symbolicOperator);
+ s.append("-");
+ s.append(symbolicValue);
+ }
+}
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicResultValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicResultValueImpl.java
new file mode 100644
index 0000000..161e84f
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicResultValueImpl.java
@@ -0,0 +1,76 @@
+/**
+ * Copyright (c) 2010, 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ * E.D.Willink - Initial API and implementation
+ */
+package org.eclipse.ocl.pivot.internal.values;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
+import org.eclipse.ocl.pivot.library.InvertibleLibraryOperation;
+import org.eclipse.ocl.pivot.library.LibraryOperation;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
+
+/**
+ * <!-- begin-user-doc -->
+ * An implementation of the model object '<em><b>Symbolic Value</b></em>'.
+ * @since 1.12
+ * <!-- end-user-doc -->
+ *
+ * @generated
+ */
+public class SymbolicResultValueImpl extends SymbolicUnknownValueImpl {
+ private static final long serialVersionUID = 1L;
+
+ protected final @NonNull LibraryOperation operation;
+
+ protected final @Nullable Object sourceValue;
+ protected final @Nullable Object argumentValue;
+
+ /**
+ * <!-- begin-user-doc -->
+ * <!-- end-user-doc -->
+ * @generated NOT
+ */
+ public SymbolicResultValueImpl(@NonNull TypeId typeId, boolean mayBeNull, boolean mayBeInvalid,
+ @NonNull LibraryOperation operation, @Nullable Object sourceValue, @Nullable Object argumentValue) {
+ super(typeId, mayBeNull, mayBeInvalid);
+ this.operation = operation;
+ this.sourceValue = sourceValue;
+ this.argumentValue = argumentValue;
+ }
+
+ @Override
+ public void deduceFrom(@NonNull SymbolicExecutor symbolicExecutor, @NonNull SymbolicConstraint symbolicConstraint) {
+ if (operation instanceof InvertibleLibraryOperation) {
+ ((InvertibleLibraryOperation)operation).deduceFrom(symbolicExecutor, this, symbolicConstraint);
+ }
+ }
+
+ public @Nullable Object getArgumentValue() {
+ return argumentValue;
+ }
+
+ public @Nullable Object getSourceValue() {
+ return sourceValue;
+ }
+
+ @Override
+ public void toString(@NonNull StringBuilder s, int lengthLimit) {
+ s.append(operation.getClass().getSimpleName());
+ s.append("(");
+ s.append(sourceValue);
+ s.append(",");
+ s.append(argumentValue);
+ s.append(")");
+ s.append(":");
+ super.toString(s, lengthLimit);
+ }
+}
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicUnknownValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicUnknownValueImpl.java
index d05a896..674b967 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicUnknownValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicUnknownValueImpl.java
@@ -20,11 +20,13 @@
import org.eclipse.ocl.pivot.ids.OclVoidTypeId;
import org.eclipse.ocl.pivot.ids.TupleTypeId;
import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
import org.eclipse.ocl.pivot.messages.PivotMessages;
import org.eclipse.ocl.pivot.values.InvalidValueException;
import org.eclipse.ocl.pivot.values.NullValue;
import org.eclipse.ocl.pivot.values.OCLValue;
import org.eclipse.ocl.pivot.values.RealValue;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
import org.eclipse.ocl.pivot.values.SymbolicValue;
/**
@@ -60,6 +62,9 @@
// }
@Override
+ public void deduceFrom(@NonNull SymbolicExecutor symbolicExecutor, @NonNull SymbolicConstraint symbolicConstraint) {}
+
+ @Override
public @NonNull NullValue divideReal(@NonNull RealValue right) {
if (right.asDouble() == 1.0) {
return this;
@@ -72,6 +77,12 @@
}
@Override
+ public boolean equals(Object obj) {
+ // TODO Auto-generated method stub
+ return super.equals(obj);
+ }
+
+ @Override
public @NonNull CollectionTypeId getCollectionTypeId() {
throw new InvalidValueException(PivotMessages.ConvertibleValueRequired, "Invalid");
}
@@ -112,10 +123,12 @@
@Override
public void toString(@NonNull StringBuilder s, int lengthLimit) {
s.append(typeId);
- s.append("-");
- s.append(mayBeNull);
- s.append("-");
- s.append(mayBeInvalid);
+ s.append("[");
+ s.append(mayBeNull ? "?" : "1");
+ if (mayBeInvalid) {
+ s.append("!");
+ }
+ s.append("]");
}
@Override
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicValueImpl.java
index 6ef8ad2..8633f3d 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicValueImpl.java
@@ -13,6 +13,8 @@
import org.eclipse.emf.ecore.EClass;
import org.eclipse.jdt.annotation.NonNull;
import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
import org.eclipse.ocl.pivot.values.SymbolicValue;
import org.eclipse.ocl.pivot.values.ValuesPackage;
@@ -59,6 +61,9 @@
}
@Override
+ public void deduceFrom(@NonNull SymbolicExecutor symbolicExecutor, @NonNull SymbolicConstraint symbolicConstraint) {}
+
+ @Override
public @NonNull TypeId getTypeId() {
return getTypeId2();
}
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicVariableValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicVariableValueImpl.java
index 0398a4e..2d5721c 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicVariableValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/SymbolicVariableValueImpl.java
@@ -13,6 +13,9 @@
import org.eclipse.jdt.annotation.NonNull;
import org.eclipse.ocl.pivot.VariableDeclaration;
import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
/**
* <!-- begin-user-doc -->
@@ -25,14 +28,18 @@
public class SymbolicVariableValueImpl extends SymbolicValueImpl { //implements EObject {
protected final @NonNull VariableDeclaration variable;
+ protected final @NonNull SymbolicValue value;
/**
* <!-- begin-user-doc -->
* <!-- end-user-doc -->
* @param variable
+ * @param value
+ * @param object
* @generated NOT
*/
- public SymbolicVariableValueImpl(@NonNull VariableDeclaration variable) {
+ public SymbolicVariableValueImpl(@NonNull VariableDeclaration variable, @NonNull SymbolicValue value) {
this.variable = variable;
+ this.value = value;
}
// @Override
@@ -41,18 +48,36 @@
// }
@Override
- public @NonNull TypeId getTypeId() {
- return variable.getTypeId();
+ public void deduceFrom(@NonNull SymbolicExecutor symbolicExecutor, @NonNull SymbolicConstraint symbolicConstraint) {
+ symbolicExecutor.add(variable, symbolicConstraint);
}
@Override
+ public @NonNull TypeId getTypeId2() {
+ return variable.getTypeId();
+ }
+
+ public @NonNull SymbolicValue getValue() {
+ return value;
+ }
+
+// public @NonNull VariableDeclaration getVariable() {
+// return variable;
+// }
+
+ @Override
public boolean mayBeNull() {
- return !variable.isIsRequired();
+ boolean isRequired = variable.isIsRequired();
+ boolean mayBeNull = value.mayBeNull();
+ assert !isRequired || !mayBeNull;
+ return mayBeNull;
}
@Override
public void toString(@NonNull StringBuilder s, int lengthLimit) {
s.append(variable.getName());
+ s.append(":");
+ value.toString(s, lengthLimit);
}
/* @Override
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/UndefinedValueImpl.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/UndefinedValueImpl.java
index 98b114a..8e82939 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/UndefinedValueImpl.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/internal/values/UndefinedValueImpl.java
@@ -679,8 +679,15 @@
}
@Override
+ public /*final*/ @NonNull String toString() {
+ StringBuilder s = new StringBuilder();
+ toString(s, 100);
+ return s.toString();
+ }
+
+ @Override
public void toString(@NonNull StringBuilder s, int sizeLimit) {
- s.append(toString());
+ s.append(super.toString());
}
@Override
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/SymbolicConstraint.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/SymbolicConstraint.java
new file mode 100644
index 0000000..39ddc00
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/SymbolicConstraint.java
@@ -0,0 +1,22 @@
+/*******************************************************************************
+ * Copyright (c) 2010, 2018 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ * E.D.Willink - Initial API and implementation
+ *******************************************************************************/
+package org.eclipse.ocl.pivot.values;
+
+import org.eclipse.jdt.annotation.Nullable;
+
+/**
+ * @since 1.12
+ */
+public interface SymbolicConstraint extends SymbolicValue
+{
+ @Nullable SymbolicOperator getSymbolicOperator();
+ @Nullable Object getSymbolicValue();
+}
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/SymbolicOperator.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/SymbolicOperator.java
new file mode 100644
index 0000000..964adcf
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/SymbolicOperator.java
@@ -0,0 +1,21 @@
+/**
+ * Copyright (c) 2010, 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ * E.D.Willink - Initial API and implementation
+ */
+package org.eclipse.ocl.pivot.values;
+
+/**
+ * @since 1.12
+ */
+public enum SymbolicOperator
+{
+ EQUALS,
+ NOT_EQUALS,
+ COMPARE_TO
+} // SymbolicValue
diff --git a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/SymbolicValue.java b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/SymbolicValue.java
index f9e8da4..4bd080c 100644
--- a/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/SymbolicValue.java
+++ b/plugins/org.eclipse.ocl.pivot/emf-gen/org/eclipse/ocl/pivot/values/SymbolicValue.java
@@ -10,6 +10,8 @@
*/
package org.eclipse.ocl.pivot.values;
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
/**
* <!-- begin-user-doc -->
@@ -25,5 +27,10 @@
* @see org.eclipse.ocl.pivot.values.ValuesPackage#getSymbolicValue()
* @generated
*/
-public interface SymbolicValue extends Value {
+public interface SymbolicValue extends Value
+{
+ /**
+ * Update symbolicExecutor from any deductions that can be made from knowing that symbolicConstraint is observede.
+ */
+ void deduceFrom(@NonNull SymbolicExecutor symbolicExecutor, @NonNull SymbolicConstraint symbolicConstraint);
} // SymbolicValue
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/EvaluationEnvironment.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/EvaluationEnvironment.java
index 150a1bb..c0a93ec 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/EvaluationEnvironment.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/EvaluationEnvironment.java
@@ -16,6 +16,7 @@
import org.eclipse.jdt.annotation.Nullable;
import org.eclipse.ocl.pivot.NamedElement;
import org.eclipse.ocl.pivot.TypedElement;
+import org.eclipse.ocl.pivot.VariableDeclaration;
import org.eclipse.ocl.pivot.internal.evaluation.ExecutorInternal;
import org.eclipse.ocl.pivot.utilities.Adaptable;
import org.eclipse.ocl.pivot.utilities.Customizable;
@@ -35,16 +36,16 @@
@NonNull ExecutorInternal getExecutor();
EvaluationEnvironment.@Nullable EvaluationEnvironmentExtension getParentEvaluationEnvironment();
}
-
+
/**
* Adds the supplied variable declaration and value binding to the
* environment. The variable declaration must not already be bound.
- *
+ *
* @param referredVariable
* the variable declaration to add
* @param value
* the associated binding
- *
+ *
* @see #replace(TypedElement, Object)
*/
void add(@NonNull TypedElement referredVariable, @Nullable Object value);
@@ -58,7 +59,7 @@
/**
* Returns the value associated with the supplied variable declaration
- *
+ *
* @param referredVariable
* the name whose value is to be returned
* @return the value associated with the name
@@ -73,7 +74,7 @@
/**
* Removes the supplied variable declaration and binding from the
* environment (if it exists) and returns it.
- *
+ *
* @param referredVariable
* the variable declaration to remove
* @return the value associated with the removed variable declaration
@@ -83,13 +84,19 @@
/**
* Replaces the current value of the supplied variable declaration with the
* supplied value.
- *
+ *
* @param referredVariable
* the variable declaration
* @param value
* the new value
*/
void replace(@NonNull TypedElement referredVariable, @Nullable Object value);
+ /**
+ * @since 1.12
+ */
+ default @Nullable Object replaceInternal(@NonNull VariableDeclaration referredVariable, @Nullable Object value) {
+ return null;
+ }
/** @deprecated moved to Evaluator */
@Deprecated
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/Executor.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/Executor.java
index acaa6fb..961560d 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/Executor.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/evaluation/Executor.java
@@ -31,10 +31,14 @@
{
/**
* @since 1.3
+ * @deprecated all methods moved to Executor with Java 8 defaults
*/
+ @Deprecated
public interface ExecutorExtension extends Executor
{
+ @Override
@NonNull EvaluationEnvironment pushEvaluationEnvironment(@NonNull NamedElement executableObject, @Nullable Object caller);
+ @Override
void resetCaches();
}
void add(@NonNull TypedElement referredVariable, @Nullable Object value);
@@ -78,7 +82,17 @@
*/
@Deprecated
@NonNull EvaluationEnvironment pushEvaluationEnvironment(@NonNull NamedElement executableObject, @Nullable OCLExpression callingObject);
+ /**
+ * @since 1.12
+ */
+ default @NonNull EvaluationEnvironment pushEvaluationEnvironment(@NonNull NamedElement executableObject, @Nullable Object caller) {
+ return pushEvaluationEnvironment(executableObject, caller instanceof OCLExpression ? (OCLExpression)caller : null);
+ }
void replace(@NonNull TypedElement referredVariable, @Nullable Object value);
+ /**
+ * @since 1.12
+ */
+ default void resetCaches() {}
@Override
void setLogger(@Nullable EvaluationLogger logger);
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/ecore/EObjectOperation.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/ecore/EObjectOperation.java
index 73a35fd..72d43ee 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/ecore/EObjectOperation.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/ecore/EObjectOperation.java
@@ -23,7 +23,6 @@
import org.eclipse.ocl.pivot.Variable;
import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment;
import org.eclipse.ocl.pivot.evaluation.Executor;
-import org.eclipse.ocl.pivot.evaluation.Executor.ExecutorExtension;
import org.eclipse.ocl.pivot.internal.utilities.EnvironmentFactoryInternal.EnvironmentFactoryInternalExtension;
import org.eclipse.ocl.pivot.library.AbstractOperation;
import org.eclipse.ocl.pivot.utilities.ClassUtil;
@@ -61,7 +60,7 @@
}
}
ExpressionInOCL query = specification;
- EvaluationEnvironment nestedEvaluationEnvironment = ((ExecutorExtension)executor).pushEvaluationEnvironment(query, caller);
+ EvaluationEnvironment nestedEvaluationEnvironment = executor.pushEvaluationEnvironment(query, caller);
nestedEvaluationEnvironment.add(ClassUtil.nonNullModel(query.getOwnedContext()), boxedSourceAndArgumentValues[0]);
List<Variable> parameterVariables = query.getOwnedParameters();
int iMax = Math.min(parameterVariables.size(), boxedSourceAndArgumentValues.length-1);
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractExecutor.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractExecutor.java
index a351115..1647e24 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractExecutor.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/AbstractExecutor.java
@@ -35,7 +35,9 @@
import org.eclipse.ocl.pivot.TemplateParameter;
import org.eclipse.ocl.pivot.Type;
import org.eclipse.ocl.pivot.TypedElement;
+import org.eclipse.ocl.pivot.VariableDeclaration;
import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment;
+import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment.EvaluationEnvironmentExtension;
import org.eclipse.ocl.pivot.evaluation.EvaluationLogger;
import org.eclipse.ocl.pivot.evaluation.EvaluationVisitor;
import org.eclipse.ocl.pivot.evaluation.Evaluator;
@@ -542,11 +544,19 @@
public @NonNull EvaluationEnvironment pushEvaluationEnvironment(@NonNull NamedElement executableObject, @Nullable Object caller) {
EvaluationEnvironment.EvaluationEnvironmentExtension evaluationEnvironment2 = ClassUtil.nonNullState(evaluationEnvironment);
EvaluationEnvironment.EvaluationEnvironmentExtension nestedEvaluationEnvironment = createNestedEvaluationEnvironment(evaluationEnvironment2, executableObject, caller);
- evaluationEnvironment = nestedEvaluationEnvironment;
+ pushEvaluationEnvironment(nestedEvaluationEnvironment);
return nestedEvaluationEnvironment;
}
/**
+ * @since 1.12
+ */
+ protected EvaluationEnvironmentExtension pushEvaluationEnvironment(@NonNull EvaluationEnvironmentExtension nestedEvaluationEnvironment) {
+ assert nestedEvaluationEnvironment.getParentEvaluationEnvironment() == evaluationEnvironment;
+ return evaluationEnvironment = nestedEvaluationEnvironment;
+ }
+
+ /**
* @deprecated use TypedElement argument
*/
@Deprecated
@@ -561,6 +571,13 @@
}
/**
+ * @since 1.12
+ */
+ protected @Nullable Object replaceInternal(@NonNull VariableDeclaration referredVariable, @Nullable Object value) {
+ return evaluationEnvironment.replaceInternal(referredVariable, value);
+ }
+
+ /**
* @since 1.3
*/
@Override
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationEnvironment.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationEnvironment.java
index d56b93c..4ca6966 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationEnvironment.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationEnvironment.java
@@ -20,6 +20,7 @@
import org.eclipse.ocl.pivot.NamedElement;
import org.eclipse.ocl.pivot.OCLExpression;
import org.eclipse.ocl.pivot.TypedElement;
+import org.eclipse.ocl.pivot.VariableDeclaration;
import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment;
import org.eclipse.ocl.pivot.evaluation.ModelManager;
import org.eclipse.ocl.pivot.internal.messages.PivotMessagesInternal;
@@ -128,7 +129,8 @@
throw new IllegalArgumentException(message);
}
}
- variableValues.put(referredVariable, value);
+ Object oldValue = variableValues.put(referredVariable, value);
+
}
/**
@@ -262,6 +264,10 @@
public void replace(@NonNull TypedElement referredVariable, @Nullable Object value) {
variableValues.put(referredVariable, value);
}
+ @Override
+ public @Nullable Object replaceInternal(@NonNull VariableDeclaration referredVariable, @Nullable Object value) {
+ return variableValues.put(referredVariable, value);
+ }
/**
* Returns a string representation of the bindings
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationVisitor.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationVisitor.java
index 6443904..f8dbd65 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationVisitor.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/BasicEvaluationVisitor.java
@@ -71,8 +71,11 @@
import org.eclipse.ocl.pivot.evaluation.IterationManager;
import org.eclipse.ocl.pivot.ids.CollectionTypeId;
import org.eclipse.ocl.pivot.ids.TuplePartId;
+import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
import org.eclipse.ocl.pivot.internal.messages.PivotMessagesInternal;
import org.eclipse.ocl.pivot.internal.utilities.PivotUtilInternal;
+import org.eclipse.ocl.pivot.internal.values.SymbolicUnknownValueImpl;
+import org.eclipse.ocl.pivot.internal.values.SymbolicVariableValueImpl;
import org.eclipse.ocl.pivot.labels.ILabelGenerator;
import org.eclipse.ocl.pivot.library.EvaluatorMultipleIterationManager;
import org.eclipse.ocl.pivot.library.EvaluatorMultipleMapIterationManager;
@@ -332,17 +335,51 @@
*/
@Override
public Object visitIfExp(@NonNull IfExp ifExp) {
- OCLExpression condition = ifExp.getOwnedCondition();
+ OCLExpression condition = PivotUtil.getOwnedCondition(ifExp);
Object conditionValue = condition.accept(undecoratedVisitor);
Object evaluatedCondition = ValueUtil.asBoolean(conditionValue);
- OCLExpression expression = null;
if (evaluatedCondition == ValueUtil.TRUE_VALUE) {
- expression = ifExp.getOwnedThen();
+ OCLExpression expression = PivotUtil.getOwnedThen(ifExp);
+ return expression.accept(undecoratedVisitor);
+ }
+ else if (evaluatedCondition == ValueUtil.FALSE_VALUE) {
+ OCLExpression expression = PivotUtil.getOwnedElse(ifExp);
+ return expression.accept(undecoratedVisitor);
}
else {
- expression = ifExp.getOwnedElse();
+ boolean mayBeInvalid = ValueUtil.mayBeInvalid(conditionValue);
+ boolean mayBeNull = ValueUtil.mayBeNull(conditionValue);
+ SymbolicExecutor symbolicExecutor = (SymbolicExecutor)context;
+ try {
+ OCLExpression expression = PivotUtil.getOwnedThen(ifExp);
+ symbolicExecutor.pushSymbolicEvaluationEnvironment(expression, conditionValue, Boolean.TRUE);
+ Object thenValue = expression.accept(undecoratedVisitor);
+ if (ValueUtil.mayBeInvalid(thenValue)) {
+ mayBeInvalid = true;
+ }
+ if (ValueUtil.mayBeNull(thenValue)) {
+ mayBeNull = true;
+ }
+ }
+ finally {
+ context.popEvaluationEnvironment();
+ }
+ try {
+ OCLExpression expression = PivotUtil.getOwnedElse(ifExp);
+ symbolicExecutor.pushSymbolicEvaluationEnvironment(expression, conditionValue, Boolean.FALSE);
+ Object elseValue = expression.accept(undecoratedVisitor);
+ if (ValueUtil.mayBeInvalid(elseValue)) {
+ mayBeInvalid = true;
+ }
+ if (ValueUtil.mayBeNull(elseValue)) {
+ mayBeNull = true;
+ }
+ }
+ finally {
+ context.popEvaluationEnvironment();
+ }
+ return new SymbolicUnknownValueImpl(ifExp.getTypeId(), mayBeNull, mayBeInvalid);
}
- return expression.accept(undecoratedVisitor);
}
/**
@@ -922,6 +959,9 @@
if (value instanceof InvalidValueException) {
throw (InvalidValueException)value;
}
+ else if (value instanceof SymbolicValue) { // FIXME obsolete wrt SymbolicConstraint
+ return new SymbolicVariableValueImpl(variableDeclaration, (SymbolicValue)value);
+ }
else {
return value;
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java
index 1524b0d..556f007 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/evaluation/SymbolicEvaluationVisitor.java
@@ -95,10 +95,20 @@
return !element2value.containsKey(element);
}
+ public boolean isFalse(@NonNull Element element) {
+ Object object = element2value.get(element);
+ return object == Boolean.FALSE;
+ }
+
+ public boolean isTrue(@NonNull Element element) {
+ Object object = element2value.get(element);
+ return object == Boolean.TRUE;
+ }
+
public boolean mayBeInvalid(@NonNull Element element) {
Object object = element2value.get(element);
if (object == null) {
- return true;
+ return !element2value.containsKey(element); // null may not be invalid
}
if (object instanceof Value) {
return ((Value)object).mayBeInvalid();
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedOperation.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedOperation.java
index 431998b..6dc176a 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedOperation.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedOperation.java
@@ -22,7 +22,6 @@
import org.eclipse.ocl.pivot.Variable;
import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment;
import org.eclipse.ocl.pivot.evaluation.Executor;
-import org.eclipse.ocl.pivot.evaluation.Executor.ExecutorExtension;
import org.eclipse.ocl.pivot.library.AbstractOperation;
import org.eclipse.ocl.pivot.utilities.ClassUtil;
import org.eclipse.ocl.pivot.utilities.PivotUtil;
@@ -45,7 +44,7 @@
@Override
public @Nullable Object basicEvaluate(@NonNull Executor executor, @NonNull TypedElement caller, @Nullable Object @NonNull [] boxedSourceAndArgumentValues) {
PivotUtil.checkExpression(expressionInOCL);
- EvaluationEnvironment nestedEvaluationEnvironment = ((ExecutorExtension)executor).pushEvaluationEnvironment(expressionInOCL, caller);
+ EvaluationEnvironment nestedEvaluationEnvironment = executor.pushEvaluationEnvironment(expressionInOCL, caller);
nestedEvaluationEnvironment.add(ClassUtil.nonNullModel(expressionInOCL.getOwnedContext()), boxedSourceAndArgumentValues[0]);
List<Variable> parameters = expressionInOCL.getOwnedParameters();
if (!parameters.isEmpty()) {
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedProperty.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedProperty.java
index 978968c..9da7a40 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedProperty.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/ConstrainedProperty.java
@@ -56,7 +56,7 @@
}
}
PivotUtil.checkExpression(expression2);
- EvaluationEnvironment nestedEvaluationEnvironment = ((Executor.ExecutorExtension)executor).pushEvaluationEnvironment(expression2, (Object)null);
+ EvaluationEnvironment nestedEvaluationEnvironment = executor.pushEvaluationEnvironment(expression2, (Object)null);
Variable contextVariable = expression2.getOwnedContext();
if (contextVariable != null) {
nestedEvaluationEnvironment.add(contextVariable, sourceValue);
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/executor/ExecutorManager.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/executor/ExecutorManager.java
index 52de7d7..0859b22 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/executor/ExecutorManager.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/library/executor/ExecutorManager.java
@@ -25,6 +25,7 @@
import org.eclipse.ocl.pivot.StandardLibrary;
import org.eclipse.ocl.pivot.Type;
import org.eclipse.ocl.pivot.TypedElement;
+import org.eclipse.ocl.pivot.VariableDeclaration;
import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment;
import org.eclipse.ocl.pivot.evaluation.EvaluationLogger;
import org.eclipse.ocl.pivot.evaluation.Evaluator;
@@ -140,6 +141,11 @@
public void replace(@NonNull TypedElement referredVariable, @Nullable Object value) {}
@Override
+ public @Nullable Object replaceInternal(@NonNull VariableDeclaration referredVariable, @Nullable Object value) {
+ return null;
+ }
+
+ @Override
public <T> void setOption(@NonNull Option<T> option, @Nullable T value) {
}
};
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/PivotMetamodelManager.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/PivotMetamodelManager.java
index 8895fa3..47f8f3a 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/PivotMetamodelManager.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/PivotMetamodelManager.java
@@ -64,7 +64,6 @@
import org.eclipse.ocl.pivot.MapType;
import org.eclipse.ocl.pivot.Model;
import org.eclipse.ocl.pivot.Namespace;
-import org.eclipse.ocl.pivot.NavigationCallExp;
import org.eclipse.ocl.pivot.NullLiteralExp;
import org.eclipse.ocl.pivot.OCLExpression;
import org.eclipse.ocl.pivot.Operation;
@@ -102,7 +101,6 @@
import org.eclipse.ocl.pivot.internal.complete.StandardLibraryInternal;
import org.eclipse.ocl.pivot.internal.ecore.as2es.AS2Ecore;
import org.eclipse.ocl.pivot.internal.ecore.es2as.Ecore2AS;
-import org.eclipse.ocl.pivot.internal.evaluation.BasicOCLExecutor;
import org.eclipse.ocl.pivot.internal.evaluation.ExecutorInternal;
import org.eclipse.ocl.pivot.internal.evaluation.SymbolicEvaluationVisitor;
import org.eclipse.ocl.pivot.internal.library.ConstrainedOperation;
@@ -122,7 +120,6 @@
import org.eclipse.ocl.pivot.internal.utilities.OppositePropertyDetails;
import org.eclipse.ocl.pivot.internal.utilities.PivotConstantsInternal;
import org.eclipse.ocl.pivot.internal.utilities.PivotUtilInternal;
-import org.eclipse.ocl.pivot.internal.values.SymbolicNavigationCallValueImpl;
import org.eclipse.ocl.pivot.library.LibraryFeature;
import org.eclipse.ocl.pivot.library.LibraryProperty;
import org.eclipse.ocl.pivot.library.UnsupportedOperation;
@@ -640,6 +637,13 @@
return asString;
}
+ /**
+ * @since 1.12
+ */
+ protected SymbolicOCLExecutor createSymbolicExecutor(@NonNull ModelManager modelManager) {
+ return new SymbolicOCLExecutor((EnvironmentFactoryInternalExtension)environmentFactory, modelManager);
+ }
+
public @NonNull UnlimitedNaturalLiteralExp createUnlimitedNaturalLiteralExp(@NonNull Number unlimitedNaturalSymbol) { // FIXME move to PivotHelper
UnlimitedNaturalLiteralExp asUnlimitedNatural = PivotFactory.eINSTANCE.createUnlimitedNaturalLiteralExp();
asUnlimitedNatural.setUnlimitedNaturalSymbol(unlimitedNaturalSymbol);
@@ -1193,70 +1197,21 @@
*/
@Override
public @NonNull SymbolicEvaluationVisitor getSymbolicAnalysis(@NonNull ExpressionInOCL expressionInOCL, @Nullable Object context, @NonNull Object... parameters) {
- OCLExpression oclExpression = PivotUtil.getOwnedBody(expressionInOCL);
- OCLExpression contextExpression = FlowAnalysis.getControlExpression(oclExpression);
- // Map<@NonNull OCLExpression, @NonNull FlowAnalysis> oclExpression2flowAnalysis2 = oclExpression2flowAnalysis;
- // if (oclExpression2flowAnalysis2 == null) {
- // oclExpression2flowAnalysis2 = oclExpression2flowAnalysis = new HashMap<>();
- // }
-// ModelManager modelManager = environmentFactory.createModelManager(oclExpression);
- // Object context = null;
- ModelManager modelManager = null;
- // EvaluationVisitor evaluationVisitor = environmentFactory.createEvaluationVisitor(null, expressionInOCL, modelManager);
-
-
- // if (modelManager == null) {
- // let the evaluation environment create one
- modelManager = environmentFactory.createModelManager(context);
- // }
- // can determine a more appropriate context from the context
- // variable of the expression, to account for stereotype constraints
- // context = HelperUtil.getConstraintContext(rootEnvironment, context, expression);
- // ExecutorInternal executor = createExecutor(modelManager);
- ExecutorInternal executor = new BasicOCLExecutor((EnvironmentFactoryInternalExtension) environmentFactory, modelManager)
- {
- /* @Override
- protected @NonNull EvaluationEnvironmentExtension createRootEvaluationEnvironment(@NonNull NamedElement executableObject) {
- // return super.createRootEvaluationEnvironment(executableObject);
- return new BasicEvaluationEnvironment(this, executableObject)
- {
- @Override
- public void add(@NonNull TypedElement referredVariable, @Nullable Object value) {
- // TODO Auto-generated method stub
- super.add(referredVariable, value);
- }
- };
- } */
-
- @Override
- public @Nullable Object internalExecuteNavigationCallExp(@NonNull NavigationCallExp navigationCallExp, @NonNull Property referredProperty, @Nullable Object sourceValue) {
- return new SymbolicNavigationCallValueImpl(navigationCallExp, sourceValue);
- }
-
- @Override
- public Object internalExecuteOperationCallExp(@NonNull OperationCallExp operationCallExp, @Nullable Object @NonNull [] sourceAndArgumentValues) {
- return super.internalExecuteOperationCallExp(operationCallExp, sourceAndArgumentValues);
- }
-
- };
+ ModelManager modelManager = environmentFactory.createModelManager(context);
+ ExecutorInternal executor = createSymbolicExecutor(modelManager);
EvaluationEnvironment evaluationEnvironment = executor.initializeEvaluationEnvironment(expressionInOCL);
IdResolver idResolver = environmentFactory.getIdResolver();
Variable contextVariable = expressionInOCL.getOwnedContext();
if (contextVariable != null) {
- Object value = context; //new SymbolicVariableValueImpl(contextVariable); //idResolver.boxedValueOf(context);
- evaluationEnvironment.add(contextVariable, idResolver.boxedValueOf(value));
+ // Object value = new SymbolicVariableValueImpl(contextVariable, idResolver.boxedValueOf(context);
+ // Object value = new SymbolicVariableValueImpl(contextVariable, idResolver.boxedValueOf(context);
+ evaluationEnvironment.add(contextVariable, idResolver.boxedValueOf(context));
}
int i = 0;
for (Variable parameterVariable : PivotUtil.getOwnedParameters(expressionInOCL)) {
evaluationEnvironment.add(parameterVariable, idResolver.boxedValueOf(parameters[i++]));
}
EvaluationVisitor evaluationVisitor = executor.getEvaluationVisitor();
-
-
-
-
-// ExecutorInternal executor = ((EnvironmentFactoryExtension)environmentFactory).createExecutor(modelManager);
-// EvaluationVisitor evaluationVisitor = executor.getEvaluationVisitor();
SymbolicEvaluationVisitor symbolicEvaluationVisitor = new SymbolicEvaluationVisitor(evaluationVisitor);
try {
symbolicEvaluationVisitor.evaluate(expressionInOCL);
@@ -1264,11 +1219,6 @@
catch (InvalidValueException e) {
// Ok so some results are unarguably invalid.
}
- // FlowAnalysis flowAnalysis = oclExpression2flowAnalysis2.get(contextExpression);
- // if (flowAnalysis == null) {
- // flowAnalysis = environmentFactory.createFlowAnalysis(contextExpression);
- // oclExpression2flowAnalysis2.put(contextExpression, flowAnalysis);
- // }
return symbolicEvaluationVisitor;
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/SymbolicExecutor.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/SymbolicExecutor.java
new file mode 100644
index 0000000..93256a5
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/SymbolicExecutor.java
@@ -0,0 +1,28 @@
+/*******************************************************************************
+ * Copyright (c) 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ * E.D.Willink - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.ocl.pivot.internal.manager;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.NamedElement;
+import org.eclipse.ocl.pivot.VariableDeclaration;
+import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment;
+import org.eclipse.ocl.pivot.evaluation.Executor;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
+
+/**
+ * @since 1.12
+ */
+public interface SymbolicExecutor extends Executor
+{
+ void add(@NonNull VariableDeclaration variable, @NonNull SymbolicConstraint symbolicConstraint);
+ @NonNull EvaluationEnvironment pushSymbolicEvaluationEnvironment(@NonNull NamedElement executableObject, @Nullable Object symbolicValue, @Nullable Object constantValue);
+}
\ No newline at end of file
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/SymbolicOCLExecutor.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/SymbolicOCLExecutor.java
new file mode 100644
index 0000000..5e6c1be
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/internal/manager/SymbolicOCLExecutor.java
@@ -0,0 +1,81 @@
+/*******************************************************************************
+ * Copyright (c) 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ * E.D.Willink - initial API and implementation
+ *******************************************************************************/
+package org.eclipse.ocl.pivot.internal.manager;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.NamedElement;
+import org.eclipse.ocl.pivot.NavigationCallExp;
+import org.eclipse.ocl.pivot.OperationCallExp;
+import org.eclipse.ocl.pivot.Property;
+import org.eclipse.ocl.pivot.TypedElement;
+import org.eclipse.ocl.pivot.VariableDeclaration;
+import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment;
+import org.eclipse.ocl.pivot.evaluation.EvaluationEnvironment.EvaluationEnvironmentExtension;
+import org.eclipse.ocl.pivot.evaluation.ModelManager;
+import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.internal.evaluation.BasicOCLExecutor;
+import org.eclipse.ocl.pivot.internal.utilities.EnvironmentFactoryInternal.EnvironmentFactoryInternalExtension;
+import org.eclipse.ocl.pivot.internal.values.CompositeSymbolicConstraintImpl;
+import org.eclipse.ocl.pivot.internal.values.SymbolicConstraintImpl;
+import org.eclipse.ocl.pivot.internal.values.SymbolicNavigationCallValueImpl;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
+import org.eclipse.ocl.pivot.values.SymbolicOperator;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
+
+/**
+ * @since 1.12
+ */
+public class SymbolicOCLExecutor extends BasicOCLExecutor implements SymbolicExecutor
+{
+ public SymbolicOCLExecutor( @NonNull EnvironmentFactoryInternalExtension environmentFactory, @NonNull ModelManager modelManager) {
+ super(environmentFactory, modelManager);
+ }
+
+ @Override
+ public void add(@NonNull VariableDeclaration variable, @NonNull SymbolicConstraint symbolicConstraint) {
+ Object oldConstraint = super.replaceInternal(variable, symbolicConstraint);
+ if (oldConstraint != null) {
+ CompositeSymbolicConstraintImpl compositeSymbolicConstraint;
+ if (oldConstraint instanceof CompositeSymbolicConstraintImpl) {
+ compositeSymbolicConstraint = (CompositeSymbolicConstraintImpl) oldConstraint;
+ }
+ else {
+ compositeSymbolicConstraint = new CompositeSymbolicConstraintImpl();
+ compositeSymbolicConstraint.add((SymbolicConstraint)oldConstraint);
+ super.replaceInternal(variable, compositeSymbolicConstraint);
+ }
+ compositeSymbolicConstraint.add(symbolicConstraint);
+ }
+
+ }
+
+ @Override
+ public @Nullable Object internalExecuteNavigationCallExp(@NonNull NavigationCallExp navigationCallExp, @NonNull Property referredProperty, @Nullable Object sourceValue) {
+ return new SymbolicNavigationCallValueImpl(navigationCallExp, sourceValue);
+ }
+
+ @Override
+ public Object internalExecuteOperationCallExp(@NonNull OperationCallExp operationCallExp, @Nullable Object @NonNull [] sourceAndArgumentValues) {
+ return super.internalExecuteOperationCallExp(operationCallExp, sourceAndArgumentValues);
+ }
+
+ @Override
+ public @NonNull EvaluationEnvironment pushSymbolicEvaluationEnvironment(@NonNull NamedElement executableObject, @Nullable Object symbolicValue, @Nullable Object constantValue) {
+ EvaluationEnvironment.EvaluationEnvironmentExtension evaluationEnvironment2 = (EvaluationEnvironmentExtension) getEvaluationEnvironment(); //ClassUtil.nonNullState(evaluationEnvironment);
+ EvaluationEnvironment.EvaluationEnvironmentExtension nestedEvaluationEnvironment = createNestedEvaluationEnvironment(evaluationEnvironment2, executableObject, (TypedElement)null);
+ pushEvaluationEnvironment(nestedEvaluationEnvironment);
+ if (symbolicValue instanceof SymbolicValue) {
+ ((SymbolicValue)symbolicValue).deduceFrom(this, new SymbolicConstraintImpl(TypeId.BOOLEAN, false, false, SymbolicOperator.EQUALS, constantValue));
+ }
+ return nestedEvaluationEnvironment;
+ }
+}
\ No newline at end of file
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractEvaluatorIterableIterationManager.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractEvaluatorIterableIterationManager.java
index b2f51ed..6835ff4 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractEvaluatorIterableIterationManager.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractEvaluatorIterableIterationManager.java
@@ -127,7 +127,7 @@
if (accumulatorVariable != null) {
getEvaluationEnvironment().add(accumulatorVariable, accumulatorValue);
}
- ((Executor.ExecutorExtension)this.executor).pushEvaluationEnvironment(body, (Object)callExp);
+ this.executor.pushEvaluationEnvironment(body, (Object)callExp);
}
public AbstractEvaluatorIterableIterationManager(@NonNull AbstractEvaluatorIterableIterationManager<IV> iterationManager, @NonNull IV iterableValue) {
@@ -137,7 +137,7 @@
this.iterableValue = iterableValue;
this.accumulatorValue = iterationManager.accumulatorValue;
this.accumulatorVariable = iterationManager.accumulatorVariable;
- ((Executor.ExecutorExtension)this.executor).pushEvaluationEnvironment(body, (Object)callExp);
+ this.executor.pushEvaluationEnvironment(body, (Object)callExp);
}
@Override
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractEvaluatorIterationManager.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractEvaluatorIterationManager.java
index aa852ed..692c7e1 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractEvaluatorIterationManager.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/AbstractEvaluatorIterationManager.java
@@ -141,7 +141,7 @@
if (accumulatorVariable != null) {
getEvaluationEnvironment().add(accumulatorVariable, accumulatorValue);
}
- ((Executor.ExecutorExtension)this.executor).pushEvaluationEnvironment(body, (Object)callExp);
+ this.executor.pushEvaluationEnvironment(body, (Object)callExp);
}
public AbstractEvaluatorIterationManager(@NonNull AbstractEvaluatorIterationManager iterationManager, @NonNull CollectionValue collectionValue) {
@@ -151,7 +151,7 @@
this.collectionValue = collectionValue;
this.accumulatorValue = iterationManager.accumulatorValue;
this.accumulatorVariable = iterationManager.accumulatorVariable;
- ((Executor.ExecutorExtension)this.executor).pushEvaluationEnvironment(body, (Object)callExp);
+ this.executor.pushEvaluationEnvironment(body, (Object)callExp);
}
@Override
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/InvertibleLibraryOperation.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/InvertibleLibraryOperation.java
new file mode 100644
index 0000000..b90da9d
--- /dev/null
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/InvertibleLibraryOperation.java
@@ -0,0 +1,29 @@
+/*******************************************************************************
+ * Copyright (c) 2020 Willink Transformations and others.
+ * All rights reserved. This program and the accompanying materials
+ * are made available under the terms of the Eclipse Public License v2.0
+ * which accompanies this distribution, and is available at
+ * http://www.eclipse.org/legal/epl-v20.html
+ *
+ * Contributors:
+ * E.D.Willink - Initial API and implementation
+ *******************************************************************************/
+package org.eclipse.ocl.pivot.library;
+
+import org.eclipse.jdt.annotation.NonNull;
+import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
+
+/**
+ * An InvertibleLibraryOperation support deduction of operation input values from known output values.
+ *
+ * @since 1.12
+ */
+public interface InvertibleLibraryOperation
+{
+ /**
+ * Update symbolicExecutor from any deductions that can be made from knowing that resultValue satisfies resultConstraint.
+ */
+ void deduceFrom(@NonNull SymbolicExecutor symbolicExecutor, @NonNull SymbolicValue resultValue, @NonNull SymbolicConstraint resultConstraint);
+}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/logical/BooleanImpliesOperation2.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/logical/BooleanImpliesOperation2.java
index 199d7b3..5f1805e 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/logical/BooleanImpliesOperation2.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/logical/BooleanImpliesOperation2.java
@@ -17,6 +17,7 @@
import org.eclipse.ocl.pivot.OCLExpression;
import org.eclipse.ocl.pivot.OperationCallExp;
import org.eclipse.ocl.pivot.evaluation.Executor;
+import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
import org.eclipse.ocl.pivot.library.AbstractSimpleBinaryOperation;
import org.eclipse.ocl.pivot.utilities.ValueUtil;
import org.eclipse.ocl.pivot.values.InvalidValueException;
@@ -44,10 +45,21 @@
if (sourceValue == Boolean.FALSE) {
return TRUE_VALUE;
}
- Object firstArgument = executor.evaluate(argument0);
- Boolean sourceBoolean = ValueUtil.asBoolean(sourceValue);
- Boolean argBoolean = ValueUtil.asBoolean(firstArgument);
- return evaluate(sourceBoolean, argBoolean);
+ else if (sourceValue == Boolean.TRUE) {
+ Object firstArgument = executor.evaluate(argument0);
+ Boolean argBoolean = ValueUtil.asBoolean(firstArgument);
+ return argBoolean;
+ }
+ try {
+ ((SymbolicExecutor)executor).pushSymbolicEvaluationEnvironment(callExp.getOwnedSource(), sourceValue, Boolean.TRUE);
+ Object firstArgument = executor.evaluate(argument0);
+ Boolean sourceBoolean = ValueUtil.asBoolean(sourceValue);
+ Boolean argBoolean = ValueUtil.asBoolean(firstArgument);
+ return evaluate(sourceBoolean, argBoolean);
+ }
+ finally {
+ executor.popEvaluationEnvironment();
+ }
}
@Override
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyEqualOperation.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyEqualOperation.java
index 1f018af..995360b 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyEqualOperation.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyEqualOperation.java
@@ -13,19 +13,91 @@
import org.eclipse.jdt.annotation.NonNull;
import org.eclipse.jdt.annotation.Nullable;
import org.eclipse.ocl.pivot.Type;
+import org.eclipse.ocl.pivot.evaluation.Executor;
+import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
+import org.eclipse.ocl.pivot.internal.values.SymbolicConstraintImpl;
+import org.eclipse.ocl.pivot.internal.values.SymbolicResultValueImpl;
import org.eclipse.ocl.pivot.library.AbstractSimpleBinaryOperation;
+import org.eclipse.ocl.pivot.library.InvertibleLibraryOperation;
+import org.eclipse.ocl.pivot.utilities.ValueUtil;
import org.eclipse.ocl.pivot.values.InvalidValueException;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
+import org.eclipse.ocl.pivot.values.SymbolicOperator;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
/**
* OclAnyEqualOperation realises the OCLAny::=() library operation and
* regular derived implementations since the Value classes exhibit
* OCL value semantics.
*/
-public class OclAnyEqualOperation extends AbstractSimpleBinaryOperation
+public class OclAnyEqualOperation extends AbstractSimpleBinaryOperation implements InvertibleLibraryOperation
{
public static final @NonNull OclAnyEqualOperation INSTANCE = new OclAnyEqualOperation();
@Override
+ public void deduceFrom(@NonNull SymbolicExecutor symbolicExecutor, @NonNull SymbolicValue resultValue, @NonNull SymbolicConstraint resultConstraint) {
+ deduceFrom(symbolicExecutor, resultValue, resultConstraint, false);
+ }
+
+ /**
+ * @since 1.12
+ */
+ protected void deduceFrom(@NonNull SymbolicExecutor symbolicExecutor, @NonNull SymbolicValue resultValue, @NonNull SymbolicConstraint resultConstraint, boolean isInverted) {
+ SymbolicOperator thisSymbolicOperator = resultConstraint.getSymbolicOperator();
+ SymbolicOperator nestedSymbolicOperator = null;
+ if (thisSymbolicOperator == (isInverted ? SymbolicOperator.NOT_EQUALS : SymbolicOperator.EQUALS)) { // FIXME simplify, XOR
+ Object knownValue = resultConstraint.getSymbolicValue();
+ if (knownValue == Boolean.TRUE) {
+ nestedSymbolicOperator = SymbolicOperator.EQUALS;
+ }
+ else if (knownValue == Boolean.FALSE) {
+ nestedSymbolicOperator = SymbolicOperator.NOT_EQUALS;
+ }
+ }
+ else if (thisSymbolicOperator == (isInverted ? SymbolicOperator.EQUALS : SymbolicOperator.NOT_EQUALS)) {
+ Object knownValue = resultConstraint.getSymbolicValue();
+ if (knownValue == Boolean.TRUE) {
+ nestedSymbolicOperator = SymbolicOperator.NOT_EQUALS;
+ }
+ else if (knownValue == Boolean.FALSE) {
+ nestedSymbolicOperator = SymbolicOperator.EQUALS;
+ }
+ }
+ else {
+ throw new IllegalStateException(String.valueOf(thisSymbolicOperator));
+ }
+ if (nestedSymbolicOperator != null) {
+ Object sourceValue = ((SymbolicResultValueImpl)resultValue).getSourceValue();
+ Object argumentValue = ((SymbolicResultValueImpl)resultValue).getArgumentValue();
+ if (sourceValue instanceof SymbolicValue) {
+ ((SymbolicValue)sourceValue).deduceFrom(symbolicExecutor, new SymbolicConstraintImpl(TypeId.BOOLEAN, false, false, nestedSymbolicOperator, argumentValue));
+ }
+ if (argumentValue instanceof SymbolicValue) {
+ ((SymbolicValue)argumentValue).deduceFrom(symbolicExecutor, new SymbolicConstraintImpl(TypeId.BOOLEAN, false, false, nestedSymbolicOperator, sourceValue));
+ }
+ }
+ }
+
+ @Override
+ public @Nullable Object evaluate(@NonNull Executor executor, @NonNull TypeId returnTypeId,
+ @Nullable Object sourceValue, @Nullable Object argumentValue) {
+ if ((sourceValue instanceof SymbolicValue) || (argumentValue instanceof SymbolicValue)) {
+// boolean mayBeInvalid = ValueUtil.mayBeInvalid(sourceValue) || ValueUtil.mayBeInvalid(argumentValue);
+ if ((!ValueUtil.mayBeNull(sourceValue) && (argumentValue == null)) || ((sourceValue == null) && !ValueUtil.mayBeNull(argumentValue))) {
+ return evaluate(executor, sourceValue, argumentValue);
+// return new SymbolicBooleanValueImpl(returnTypeId, false, /*mayBeNull ||*/ mayBeInvalid, this, sourceValue, argumentValue);
+ }
+ else {
+ return new SymbolicResultValueImpl(returnTypeId, false, /*mayBeNull ||*/ false, this, sourceValue, argumentValue);
+ }
+ }
+ else {
+ return evaluate(executor, sourceValue, argumentValue);
+ }
+ }
+
+ @Override
public @NonNull Boolean evaluate(@Nullable Object left, @Nullable Object right) {
//
// A.2.2 is clear. 11.3.1 is vague.
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyNotEqualOperation.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyNotEqualOperation.java
index be97855..c4d258c 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyNotEqualOperation.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclAnyNotEqualOperation.java
@@ -13,8 +13,11 @@
import org.eclipse.jdt.annotation.NonNull;
import org.eclipse.jdt.annotation.Nullable;
import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.internal.manager.SymbolicExecutor;
import org.eclipse.ocl.pivot.messages.PivotMessages;
import org.eclipse.ocl.pivot.values.InvalidValueException;
+import org.eclipse.ocl.pivot.values.SymbolicConstraint;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
/**
@@ -27,6 +30,11 @@
public static final @NonNull OclAnyNotEqualOperation INSTANCE = new OclAnyNotEqualOperation();
@Override
+ public void deduceFrom(@NonNull SymbolicExecutor symbolicExecutor, @NonNull SymbolicValue resultValue, @NonNull SymbolicConstraint resultConstraint) {
+ deduceFrom(symbolicExecutor, resultValue, resultConstraint, true);
+ }
+
+ @Override
public @NonNull Boolean evaluate(@Nullable Object left, @Nullable Object right) {
Object equals = super.evaluate(left, right);
if (equals == Boolean.FALSE) {
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclComparableCompareToOperation.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclComparableCompareToOperation.java
index c6855cc..e92a286 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclComparableCompareToOperation.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclComparableCompareToOperation.java
@@ -12,9 +12,13 @@
import org.eclipse.jdt.annotation.NonNull;
import org.eclipse.jdt.annotation.Nullable;
+import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.internal.values.SymbolicConstraintImpl;
import org.eclipse.ocl.pivot.library.AbstractSimpleBinaryOperation;
import org.eclipse.ocl.pivot.utilities.ValueUtil;
import org.eclipse.ocl.pivot.values.IntegerValue;
+import org.eclipse.ocl.pivot.values.SymbolicOperator;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
/**
* OclComparableCompareToOperation realizes the abstract compareTo library operation using intrinsic Java functionality.
@@ -29,6 +33,11 @@
@SuppressWarnings("unchecked") int compareTo = ((Comparable<Object>)left).compareTo(right);
return integerValueOf(compareTo);
}
+ else if (left instanceof SymbolicValue) {
+ boolean mayBeInvalid = ValueUtil.mayBeInvalid(left) || ValueUtil.mayBeInvalid(right);
+ boolean mayBeNull = ValueUtil.mayBeNull(left) || ValueUtil.mayBeNull(right);
+ return new SymbolicConstraintImpl(TypeId.INTEGER, false, mayBeNull || mayBeInvalid, SymbolicOperator.COMPARE_TO, right);
+ }
else {
return integerValueOf(ValueUtil.throwUnsupportedCompareTo(left, right));
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclComparableComparisonOperation.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclComparableComparisonOperation.java
index eebce81..b776061 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclComparableComparisonOperation.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/library/oclany/OclComparableComparisonOperation.java
@@ -19,29 +19,28 @@
import org.eclipse.ocl.pivot.evaluation.Executor;
import org.eclipse.ocl.pivot.ids.IdResolver;
import org.eclipse.ocl.pivot.ids.TypeId;
+import org.eclipse.ocl.pivot.internal.values.SymbolicUnknownValueImpl;
import org.eclipse.ocl.pivot.library.AbstractUntypedBinaryOperation;
import org.eclipse.ocl.pivot.library.LibraryBinaryOperation;
import org.eclipse.ocl.pivot.library.LibraryConstants;
import org.eclipse.ocl.pivot.utilities.ValueUtil;
import org.eclipse.ocl.pivot.values.InvalidValueException;
+import org.eclipse.ocl.pivot.values.SymbolicValue;
/**
* OclComparableComparisonOperation provides the abstract support for a comparison operation.
*/
public abstract class OclComparableComparisonOperation extends AbstractUntypedBinaryOperation
-{
+{
/** @deprecated use Executor */
@Deprecated
@Override
public @Nullable Boolean evaluate(@NonNull Evaluator evaluator, @Nullable Object left, @Nullable Object right) {
- return evaluate(getExecutor(evaluator), left, right);
+ return evaluate(getExecutor(evaluator), left, right);
}
- /**
- * @since 1.1
- */
@Override
- public @NonNull Boolean evaluate(@NonNull Executor executor, @Nullable Object left, @Nullable Object right) {
+ public @Nullable Object evaluate(@NonNull Executor executor, @NonNull TypeId returnTypeId, @Nullable Object left, @Nullable Object right) {
StandardLibrary standardLibrary = executor.getStandardLibrary();
IdResolver idResolver = executor.getIdResolver();
CompleteInheritance leftType = idResolver.getDynamicTypeOf(left).getInheritance(standardLibrary);
@@ -61,13 +60,29 @@
}
if (implementation != null) {
Object comparison = implementation.evaluate(executor, TypeId.INTEGER, left, right);
+ if (comparison instanceof SymbolicValue) {
+ boolean mayBeInvalid = ValueUtil.mayBeInvalid(left) || ValueUtil.mayBeInvalid(right);
+ boolean mayBeNull = ValueUtil.mayBeNull(left) || ValueUtil.mayBeNull(right);
+ return new SymbolicUnknownValueImpl(TypeId.BOOLEAN, false, mayBeNull || mayBeInvalid);
+ }
intComparison = ValueUtil.asInteger(comparison);
return getResultValue(intComparison) != false; // FIXME redundant test to suppress warning
}
else {
- throw new InvalidValueException("Unsupported compareTo for ''{0}''", left != null ? left.getClass().getName() : NULL_STRING); //$NON-NLS-1$
+ // throw new InvalidValueException("Unsupported compareTo for ''{0}''", left != null ? left.getClass().getName() : NULL_STRING); //$NON-NLS-1$
+ ValueUtil.throwUnsupportedCompareTo(left, right);
+ return false;
}
}
+ /**
+ * @since 1.1
+ */
+ @Override
+ public @NonNull Boolean evaluate(@NonNull Executor executor, @Nullable Object left, @Nullable Object right) {
+ // FIXME This reverse hierarchy call is necessary to preserve API but accommodate SymbolicValue
+ return (Boolean)evaluate(executor, TypeId.BOOLEAN, left, right);
+ }
+
protected abstract boolean getResultValue(Integer comparison);
}
diff --git a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java
index 3644087..4298adc 100644
--- a/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java
+++ b/plugins/org.eclipse.ocl.pivot/src/org/eclipse/ocl/pivot/utilities/ValueUtil.java
@@ -1009,6 +1009,29 @@
}
/**
+ * @since 1.12
+ */
+ public static boolean mayBeInvalid(@Nullable Object value) {
+ if (value instanceof Value) {
+ return ((Value)value).mayBeInvalid();
+ }
+ return false;
+ }
+
+ /**
+ * @since 1.12
+ */
+ public static boolean mayBeNull(@Nullable Object value) {
+ if (value == null) {
+ return true;
+ }
+ else if (value instanceof Value) {
+ return ((Value)value).mayBeNull();
+ }
+ return false;
+ }
+
+ /**
* @since 1.1
*/
public static @NonNull NumberValue numberValueOf(@NonNull Number aNumber) {
diff --git a/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/FlowAnalysisTests.java b/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/FlowAnalysisTests.java
index c453f21..509db57 100644
--- a/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/FlowAnalysisTests.java
+++ b/tests/org.eclipse.ocl.examples.xtext.tests/src/org/eclipse/ocl/examples/test/xtext/FlowAnalysisTests.java
@@ -25,6 +25,7 @@
import org.eclipse.ocl.pivot.LetExp;
import org.eclipse.ocl.pivot.Model;
import org.eclipse.ocl.pivot.NullLiteralExp;
+import org.eclipse.ocl.pivot.NumericLiteralExp;
import org.eclipse.ocl.pivot.OCLExpression;
import org.eclipse.ocl.pivot.Operation;
import org.eclipse.ocl.pivot.OperationCallExp;
@@ -170,7 +171,7 @@
return ((MetamodelManagerInternal.MetamodelManagerInternalExtension2)metamodelManager).getFlowAnalysis(asExpression);
}
- protected @NonNull SymbolicEvaluationVisitor getSymbolicAnalysis(@NonNull ExpressionInOCL asExpressionInOCL, @Nullable Object context, @NonNull Object... parameters) {
+ protected @NonNull SymbolicEvaluationVisitor getSymbolicAnalysis(@NonNull ExpressionInOCL asExpressionInOCL, @Nullable Object context, @Nullable Object[] parameters) {
MetamodelManagerInternal metamodelManager = getMetamodelManager();
return ((MetamodelManagerInternal.MetamodelManagerInternalExtension2)metamodelManager).getSymbolicAnalysis(asExpressionInOCL, context, parameters);
}
@@ -259,14 +260,14 @@
// ocl.assertIsNonNull(asThenLiteralExp);
// ocl.assertIsNotKnown(asElseVariableExp);
- SymbolicEvaluationVisitor symbolicAnalysis1 = ocl.getSymbolicAnalysis(asExpressionInOCL, null);
+ SymbolicEvaluationVisitor symbolicAnalysis1 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, new Object[0]);
assert !symbolicAnalysis1.mayBeNull(asExpressionInOCL);
assert !symbolicAnalysis1.mayBeNull(asIf);
assert !symbolicAnalysis1.mayBeNull(asLetExp);
assert ocl.getIdResolver().oclEquals(symbolicAnalysis1.get(asIf), "null");
assert symbolicAnalysis1.isDead(asElseVariableExp);
- SymbolicEvaluationVisitor symbolicAnalysis2 = ocl.getSymbolicAnalysis(asExpressionInOCL, new SymbolicUnknownValueImpl(TypeId.STRING, false, false));
+ SymbolicEvaluationVisitor symbolicAnalysis2 = ocl.getSymbolicAnalysis(asExpressionInOCL, new SymbolicUnknownValueImpl(TypeId.STRING, false, false), new Object[0]);
assert !symbolicAnalysis2.mayBeNull(asExpressionInOCL);
assert !symbolicAnalysis2.mayBeNull(asIf);
assert !symbolicAnalysis2.mayBeNull(asLetExp);
@@ -278,13 +279,12 @@
public void testSymbolicAnalysis_BadDivide() throws Exception {
MyOCL ocl = new MyOCL();
ExpressionInOCL asExpressionInOCL = ocl.createQueryTestModel("BadDivide", "BadDivide(num : Real, den : Real) : Real",
- // "let num = 5.0 in den = 0.0 in num / den");
"num / den");
OperationCallExp asOperationCallExp = (OperationCallExp) asExpressionInOCL.getOwnedBody();
VariableExp asNumExp = (VariableExp) PivotUtil.getOwnedSource(asOperationCallExp);
VariableExp asDenExp = (VariableExp) PivotUtil.getOwnedArgument(asOperationCallExp, 0);
- SymbolicEvaluationVisitor symbolicAnalysis1 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, 5.0, 0.0);
+ SymbolicEvaluationVisitor symbolicAnalysis1 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, new Object[]{5.0, 0.0});
assert !symbolicAnalysis1.mayBeNull(asExpressionInOCL);
assert !symbolicAnalysis1.mayBeNull(asNumExp);
assert !symbolicAnalysis1.mayBeNull(asDenExp);
@@ -292,7 +292,109 @@
assert !symbolicAnalysis1.mayBeInvalid(asDenExp);
assert symbolicAnalysis1.mayBeInvalid(asOperationCallExp);
- SymbolicEvaluationVisitor symbolicAnalysis2 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, 5.0, 1.0);
+ SymbolicEvaluationVisitor symbolicAnalysis2 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, new Object[]{5.0, 1.0});
+ assert !symbolicAnalysis2.mayBeNull(asExpressionInOCL);
+ assert !symbolicAnalysis2.mayBeNull(asNumExp);
+ assert !symbolicAnalysis2.mayBeNull(asDenExp);
+ assert !symbolicAnalysis2.mayBeInvalid(asNumExp);
+ assert !symbolicAnalysis2.mayBeInvalid(asDenExp);
+ assert !symbolicAnalysis2.mayBeInvalid(asOperationCallExp);
+
+ SymbolicEvaluationVisitor symbolicAnalysis3 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, new Object[]{new SymbolicUnknownValueImpl(TypeId.REAL, false, false), 0.0});
+ assert !symbolicAnalysis3.mayBeNull(asExpressionInOCL);
+ assert !symbolicAnalysis3.mayBeNull(asNumExp);
+ assert !symbolicAnalysis3.mayBeNull(asDenExp);
+ assert !symbolicAnalysis3.mayBeInvalid(asNumExp);
+ assert !symbolicAnalysis3.mayBeInvalid(asDenExp);
+ assert symbolicAnalysis3.mayBeInvalid(asOperationCallExp);
+
+ SymbolicEvaluationVisitor symbolicAnalysis4 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, new Object[]{new SymbolicUnknownValueImpl(TypeId.REAL, false, false), 1.0});
+ assert !symbolicAnalysis4.mayBeNull(asExpressionInOCL);
+ assert !symbolicAnalysis4.mayBeNull(asNumExp);
+ assert !symbolicAnalysis4.mayBeNull(asDenExp);
+ assert !symbolicAnalysis4.mayBeInvalid(asNumExp);
+ assert !symbolicAnalysis4.mayBeInvalid(asDenExp);
+ assert !symbolicAnalysis4.mayBeInvalid(asOperationCallExp);
+
+ ocl.dispose();
+ }
+
+ public void testSymbolicAnalysis_ImpliesGuard() throws Exception {
+ MyOCL ocl = new MyOCL();
+ ExpressionInOCL asExpressionInOCL = ocl.createQueryTestModel("ImpliesGuard", "ImpliesGuard(x : Integer) : Boolean",
+ "x <> null implies2 x > 0");
+ OperationCallExp impliesExp = (OperationCallExp) asExpressionInOCL.getOwnedBody();
+ OperationCallExp notEqExp = (OperationCallExp) PivotUtil.getOwnedSource(impliesExp);
+ OperationCallExp gtExp = (OperationCallExp) PivotUtil.getOwnedArgument(impliesExp, 0);
+ VariableExp neSourceExp = (VariableExp) PivotUtil.getOwnedSource(notEqExp);
+ NullLiteralExp nullExp = (NullLiteralExp) PivotUtil.getOwnedArgument(notEqExp, 0);
+ VariableExp gtSourceExp = (VariableExp) PivotUtil.getOwnedSource(gtExp);
+ NumericLiteralExp zeroExp = (NumericLiteralExp) PivotUtil.getOwnedArgument(gtExp, 0);
+
+ assert nullExp.isNull();
+
+ /* SymbolicEvaluationVisitor symbolicAnalysis1 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, new Object[]{5});
+ assert !symbolicAnalysis1.mayBeNull(asExpressionInOCL);
+ assert !symbolicAnalysis1.mayBeNull(notEqExp);
+ assert !symbolicAnalysis1.mayBeNull(gtExp);
+
+ assert !symbolicAnalysis1.mayBeNull(neSourceExp);
+ assert symbolicAnalysis1.mayBeNull(nullExp);
+ assert !symbolicAnalysis1.mayBeNull(gtSourceExp);
+ assert !symbolicAnalysis1.mayBeNull(zeroExp);
+
+ assert !symbolicAnalysis1.mayBeInvalid(asExpressionInOCL);
+ assert !symbolicAnalysis1.mayBeInvalid(notEqExp);
+ assert !symbolicAnalysis1.mayBeInvalid(gtExp);
+
+ assert !symbolicAnalysis1.mayBeInvalid(neSourceExp);
+ assert !symbolicAnalysis1.mayBeInvalid(nullExp);
+ assert !symbolicAnalysis1.mayBeInvalid(gtSourceExp);
+ assert !symbolicAnalysis1.mayBeInvalid(zeroExp);
+
+ assert symbolicAnalysis1.isTrue(notEqExp);
+ assert symbolicAnalysis1.isTrue(gtExp);
+ assert symbolicAnalysis1.isTrue(asExpressionInOCL); */
+
+ /* SymbolicEvaluationVisitor symbolicAnalysis2 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, new Object[]{null});
+ assert !symbolicAnalysis2.mayBeNull(asExpressionInOCL);
+ assert !symbolicAnalysis2.mayBeNull(notEqExp);
+ assert symbolicAnalysis2.isDead(gtExp);
+
+ assert symbolicAnalysis2.mayBeNull(neSourceExp);
+ assert symbolicAnalysis2.mayBeNull(nullExp);
+ assert symbolicAnalysis2.isDead(gtSourceExp);
+ assert symbolicAnalysis2.isDead(zeroExp);
+
+ assert !symbolicAnalysis2.mayBeInvalid(asExpressionInOCL);
+ assert !symbolicAnalysis2.mayBeInvalid(notEqExp);
+
+ assert !symbolicAnalysis2.mayBeInvalid(neSourceExp);
+ assert !symbolicAnalysis2.mayBeInvalid(nullExp);
+
+ assert symbolicAnalysis2.isFalse(notEqExp);
+ assert symbolicAnalysis2.isTrue(asExpressionInOCL); */
+
+ SymbolicEvaluationVisitor symbolicAnalysis3 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, new Object[]{new SymbolicUnknownValueImpl(TypeId.INTEGER, true, false)});
+ assert !symbolicAnalysis3.mayBeNull(asExpressionInOCL);
+ assert !symbolicAnalysis3.mayBeNull(notEqExp);
+ assert !symbolicAnalysis3.mayBeNull(gtExp);
+
+ assert symbolicAnalysis3.mayBeNull(neSourceExp);
+ assert symbolicAnalysis3.mayBeNull(nullExp);
+ assert !symbolicAnalysis3.mayBeNull(gtSourceExp);
+ assert !symbolicAnalysis3.mayBeNull(zeroExp);
+
+ assert !symbolicAnalysis3.mayBeInvalid(asExpressionInOCL);
+ assert !symbolicAnalysis3.mayBeInvalid(notEqExp);
+
+ assert !symbolicAnalysis3.mayBeInvalid(neSourceExp);
+ assert !symbolicAnalysis3.mayBeInvalid(nullExp);
+
+ assert symbolicAnalysis3.isFalse(notEqExp);
+ assert symbolicAnalysis3.isTrue(asExpressionInOCL);
+
+/* SymbolicEvaluationVisitor symbolicAnalysis2 = ocl.getSymbolicAnalysis(asExpressionInOCL, null, 5.0, 1.0);
assert !symbolicAnalysis2.mayBeNull(asExpressionInOCL);
assert !symbolicAnalysis2.mayBeNull(asNumExp);
assert !symbolicAnalysis2.mayBeNull(asDenExp);
@@ -314,16 +416,8 @@
assert !symbolicAnalysis4.mayBeNull(asDenExp);
assert !symbolicAnalysis4.mayBeInvalid(asNumExp);
assert !symbolicAnalysis4.mayBeInvalid(asDenExp);
- assert !symbolicAnalysis4.mayBeInvalid(asOperationCallExp);
-// assert ocl.getIdResolver().oclEquals(symbolicAnalysis1.get(asIf), "null");
-// assert symbolicAnalysis1.isDead(asElseVariableExp);
+ assert !symbolicAnalysis4.mayBeInvalid(asOperationCallExp); */
-// SymbolicEvaluationVisitor symbolicAnalysis2 = ocl.getSymbolicAnalysis(asExpressionInOCL, new SymbolicUnknownValueImpl(TypeId.STRING, false, false));
-// assert !symbolicAnalysis2.mayBeNull(asExpressionInOCL);
-// assert !symbolicAnalysis2.mayBeNull(asIf);
-// assert !symbolicAnalysis2.mayBeNull(asLetExp);
-// assert ocl.getIdResolver().oclEquals(symbolicAnalysis2.get(asIf), "null");
-// assert symbolicAnalysis2.isDead(asThenLiteralExp); */
ocl.dispose();
}
