Commit 1c741744 authored by Simon Barner's avatar Simon Barner
Browse files

Fix build after moving plugins to verification repository

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

Signed-off-by: Simon Barner's avatarSimon Barner <barner@fortiss.org>
parent 0aca2f4e
......@@ -61,9 +61,9 @@
<transformationProvider transformationName="booleanComparisonWorkaroundTransformationForOCRA">
<transformation transformation="org.fortiss.af3.ocra.generator.nusmv.OCRABooleanComparisonWorkaroundTransformation"></transformation>
</transformationProvider>
<transformationProvider transformationName="transformUserDefinedOCRAExpressions">
<transformation transformation="org.fortiss.af3.ocra.generator.nusmv.TransformUserDefinedOCRAExpressions"></transformation>
</transformationProvider>
<transformationProvider transformationName="transformUserDefinedOCRAExpressions">
<transformation transformation="org.fortiss.af3.ocra.generator.nusmv.TransformUserDefinedOCRAExpressions"></transformation>
</transformationProvider>
</extension>
</plugin>
OCRABooleanComparisonWorkaroundTransformation.java 9503d6616ae216b0da0023637f2676142ce80adc GREEN
ResolveNoVal.java 507f5f2038f469b1524c9d307286b13d891d697e GREEN
ResolveNoVal.java eff52a674a92d703f75f10d691c50ac459bed184 YELLOW
TransformUserDefinedOCRAExpressions.java 3782e214353820063cf4d009a2129bed9286f0f1 GREEN
......@@ -16,7 +16,6 @@
package org.fortiss.af3.ocra.generator.nusmv;
import static org.eclipse.emf.ecore.util.EcoreUtil.replace;
import static org.fortiss.af3.component.generator.nusmv.AF3ToNuSMVConsts._PRESENT;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.and;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.createVar;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.not;
......@@ -41,6 +40,10 @@ import org.fortiss.pragmatictransformation.service.IPragmaticTransformation;
*/
public class ResolveNoVal extends CacheSupportedTransformationBase {
// Constant value must be identical org.fortiss.af3.component.generator.nusmv.AF3ToNuSMVConsts._PRESENT;
/** The "present" variable name suffix. */
private static final String _PRESENT = "_PRESENT";
/** {@inheritDoc} */
@Override
public Object transform(Object c, IPragmaticTransformation deferredTransformation) {
......
ConstraintsTree.java 57ff6f266c77c0117a0853a53e6a29010c4904a2 GREEN
OCRAContractTree.java 813cb65f474297bd97be593ff2061d7e83c45068 GREEN
TLTree.java a58a9597e7ead632d3f7d806f310a951266b9d7f GREEN
TestTree.java 082730af7819d92aa319a8db16750216e96a6463 GREEN
TestTree.java 5c6d4e1c3b1ef602a35a12e151dab5af51015b75 YELLOW
......@@ -15,7 +15,7 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.specification.ui.editor.trees;
import static org.fortiss.af3.mira.utils.MiraUtils.getTestSuitesOfRequirement;
import static org.fortiss.af3.testing.utils.TestingUtils.getTestSuitesOfRequirement;
import static org.fortiss.af3.mira.utils.MiraUtils.getTraceConstraintInstances;
import static org.fortiss.af3.testing.utils.TestingModelElementFactory.createTestSuite;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.pickInstanceOf;
......
ContractEditorConfiguration.java 73f421a02775dd25450df99bf838bfb9574d793e GREEN
ContractEditorConfiguration.java 093f5b25295771d6f0466716df6206bd1fef20fe YELLOW
ContractSpecificationEditor.java e6d58bc217a787af5f8eb350aa2c3408a49a939e GREEN
ContractSpecificationEditorBinding.java 0f2a12493c81bcb0cdbbaea5f23127400d1a75f1 GREEN
......@@ -25,7 +25,7 @@ import org.eclipse.jface.text.TextAttribute;
import org.eclipse.jface.text.rules.IToken;
import org.eclipse.jface.text.rules.Token;
import org.eclipse.jface.text.rules.WordRule;
import org.fortiss.af3.component.ui.editor.code.CodeAndOCRAContractEditorConfiguration;
import org.fortiss.af3.component.ui.editor.code.CodeEditorConfigurationBase;
import org.fortiss.af3.ocra.model.contract.ContractContainer;
import org.fortiss.tooling.base.ui.editor.SourceEditorConfigurationBase;
......@@ -35,7 +35,7 @@ import org.fortiss.tooling.base.ui.editor.SourceEditorConfigurationBase;
* @author kanav
*/
public class ContractEditorConfiguration
extends CodeAndOCRAContractEditorConfiguration<ContractContainer> {
extends CodeEditorConfigurationBase<ContractContainer> {
/** Constructor. */
public ContractEditorConfiguration(ContractSpecificationEditor editor) {
......
......@@ -8,7 +8,10 @@ Bundle-ClassPath: .
Bundle-Vendor: %providerName
Bundle-Localization: plugin
Bundle-RequiredExecutionEnvironment: JavaSE-11
Export-Package: org.fortiss.af3.specification.constraint,
Export-Package: org.fortiss.af3.specification,
org.fortiss.af3.specification.compose,
org.fortiss.af3.specification.constraint,
org.fortiss.af3.specification.generator.nusmv,
org.fortiss.af3.specification.model,
org.fortiss.af3.specification.model.impl,
org.fortiss.af3.specification.model.tlspecification,
......@@ -16,14 +19,12 @@ Export-Package: org.fortiss.af3.specification.constraint,
org.fortiss.af3.specification.model.tlspecification.util,
org.fortiss.af3.specification.model.util,
org.fortiss.af3.specification.modelchecking.af3tonusmv,
org.fortiss.af3.specification.modelchecking.counterexample,
org.fortiss.af3.specification.utils
Bundle-ActivationPolicy: lazy
Bundle-Activator: org.fortiss.af3.specification.AF3SpecificationActivator
Require-Bundle: org.fortiss.af3.expression;visibility:=reexport,
org.fortiss.af3.mira;visibility:=reexport,
org.fortiss.pragmatictransformation,
org.fortiss.af3.tools,
org.fortiss.af3.state;visibility:=reexport,
org.fortiss.af3.ocra,
com.microsoft.z3,
org.fortiss.af3.component
org.fortiss.af3.component,
org.fortiss.af3.verification
......@@ -15,7 +15,8 @@ Require-Bundle: org.fortiss.af3.state;visibility:=reexport,
org.fortiss.tooling.base.ui;bundle-version="2.16.0",
org.fortiss.af3.tools,
com.microsoft.z3;bundle-version="2.13.0",
org.fortiss.af3.expression
org.fortiss.af3.expression,
org.fortiss.af3.mira
Bundle-RequiredExecutionEnvironment: JavaSE-11
Bundle-ActivationPolicy: lazy
Export-Package: org.fortiss.af3.testing,
......
......@@ -41,7 +41,7 @@
class="org.fortiss.af3.testing.model.mcdc.McdcPackage"
genModel="model/testing.genmodel"/>
</extension>
<extension point="org.eclipse.emf.ecore.generated_package">
<!-- @generated random-specification-model -->
<package
......
GenerateStateAutomatonUtils.java e0fbef151489a860ccf95778f9b658058994a781 GREEN
StatisticUtils.java d2ea1b26fc14f0b19d18604d330205b8aae3352e GREEN
StatisticUtils.java 70a7e47b5ab14e8d3b58b4cd8757c120a3215482 RED
TestingConstraintUtils.java 7c423db9009862b16a96c05ab7ef9a59d4af6c81 GREEN
TestingModelElementFactory.java 7fd804d4ea739bd515957d450591f4a1371553e2 RED
TestingUtils.java f79bf331b9a955181c0634537e5011bedcd0ac5e RED
TestingUtils.java cedaf25deb791a768f7ffd99a944da222a615b77 RED
......@@ -15,15 +15,20 @@
+--------------------------------------------------------------------------*/
package org.fortiss.af3.testing.utils;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.pickInstanceOf;
import java.util.ArrayList;
import java.util.HashMap;
import java.util.List;
import java.util.Map;
import org.eclipse.emf.common.util.EList;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.component.model.InputPort;
import org.fortiss.af3.component.model.OutputPort;
import org.fortiss.af3.component.model.Port;
import org.fortiss.af3.mira.model.Requirement;
import org.fortiss.af3.mira.model.functional.FormalSpecification;
import org.fortiss.af3.testing.constraint.TestSuiteConstraint;
import org.fortiss.af3.testing.model.TestCase;
import org.fortiss.af3.testing.model.TestInput;
......@@ -42,6 +47,7 @@ import org.fortiss.tooling.kernel.service.IConstraintService;
import org.fortiss.tooling.kernel.service.IElementCompositorService;
import org.fortiss.tooling.kernel.service.IPrototypeService;
import org.fortiss.tooling.kernel.utils.ConstraintsUtils.ErrorEmbeddingException;
import org.fortiss.tooling.kernel.utils.EcoreUtils;
/**
* //TODO(HP): #3617
......@@ -263,4 +269,25 @@ public class TestingUtils {
}
return null;
}
/**
* Returns the test suites contained in <code>req</code>.
* More precisely: if <code>req</code> contains *only one* formal specification with one root
* component, returns the test suites of this component.
* Returns an empty list in all other cases.
*/
public static List<TestSuite> getTestSuitesOfRequirement(Requirement req) {
List<TestSuite> ts = new ArrayList<TestSuite>();
List<Component> subComps = new ArrayList<Component>();
EList<FormalSpecification> specs = req.getFormalSpecifications();
for(FormalSpecification spec : specs) {
subComps.addAll(spec.getTopComponent().getSubComponents());
}
if(subComps.size() == 1) {
// get(0) due to the guard above
EList<IModelElementSpecification> subCompSpecs = subComps.get(0).getSpecifications();
ts = pickInstanceOf(TestSuite.class, subCompSpecs);
}
return ts;
}
}
......@@ -14,7 +14,7 @@ Require-Bundle: org.fortiss.pragmatictransformation;visibility:=reexport,
org.fortiss.af3.tools;visibility:=reexport,
org.fortiss.af3.state;visibility:=reexport,
org.fortiss.af3.ocra;visibility:=reexport,
com.microsoft.z3
com.microsoft.z3;visibility:=reexport
Export-Package: org.fortiss.af3.component.generator.nusmv,
org.fortiss.af3.component.utils,
org.fortiss.af3.expression.generator.nusmv,
......
Supports Markdown
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