Commit fabe3efc authored by Alexander Diewald's avatar Alexander Diewald
Browse files

Merge remote-tracking branch 'origin/master' into 3641

parents 6f2cb47f e2be998b
......@@ -17,7 +17,8 @@ Require-Bundle: org.fortiss.af3.generator.common;bundle-version="2.14.0";visibil
org.fortiss.af3.project;visibility:=reexport,
org.fortiss.tooling.kernel;visibility:=reexport,
org.fortiss.tooling.base;visibility:=reexport,
org.fortiss.pragmatictransformation;bundle-version="2.14.0"
org.fortiss.pragmatictransformation;bundle-version="2.14.0",
com.microsoft.z3;bundle-version="2.14.0"
Export-Package: org.antlr.stringtemplate,
org.antlr.stringtemplate.language,
org.fortiss.af3.expression,
......
DataDictionaryUtils.java 67bd95a8f9eb89303b502f3831f228c85134f5bf GREEN
ExpressionModelElementFactory.java bb0dab610b1de6579292af12f07b99cf5d9d87ca GREEN
ExpressionUtils.java 02ee13866fa9eee9fed5bc5f31976ceaa71f1d77 GREEN
ExpressionUtils.java 9a07de5974cf670daecc83a7214a07206fd7e3fc GREEN
LibraryElementsFactory.java d0b803949097a7c840ced1d92c302ec4cef2054a GREEN
NoValSpecialTreatmentUtils.java 5d7736859de2bedc2ac5173e6090824f38acaf51 GREEN
OperatorStrengthUtils.java d876a3518cc01a8ab209f4b0d464fb4d030da96c GREEN
......
......@@ -40,15 +40,18 @@ import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.not
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.structAccess;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.structureConst;
import static org.fortiss.af3.project.utils.TypeScopeUtils.getVisibleITypeDefinitions;
import static org.fortiss.af3.project.utils.VariableScopeUtils.getVarType;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.copy;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashMap;
import java.util.List;
import java.util.stream.Collectors;
import org.eclipse.core.runtime.Assert;
import org.eclipse.emf.common.util.BasicEList;
import org.eclipse.emf.common.util.EList;
import org.eclipse.emf.common.util.TreeIterator;
import org.eclipse.emf.ecore.EObject;
import org.fortiss.af3.expression.language.TypeChecker;
......@@ -62,11 +65,14 @@ import org.fortiss.af3.expression.model.definitions.Structure;
import org.fortiss.af3.expression.model.definitions.StructureMember;
import org.fortiss.af3.expression.model.definitions.TypeDefinition;
import org.fortiss.af3.expression.model.terms.ArrayConst;
import org.fortiss.af3.expression.model.terms.BoolConst;
import org.fortiss.af3.expression.model.terms.ComplexVar;
import org.fortiss.af3.expression.model.terms.Const;
import org.fortiss.af3.expression.model.terms.DoubleConst;
import org.fortiss.af3.expression.model.terms.EOperator;
import org.fortiss.af3.expression.model.terms.FunctionCall;
import org.fortiss.af3.expression.model.terms.IExpressionTerm;
import org.fortiss.af3.expression.model.terms.IntConst;
import org.fortiss.af3.expression.model.terms.PredefinedFunction;
import org.fortiss.af3.expression.model.terms.StructureConst;
import org.fortiss.af3.expression.model.terms.StructureMemberConst;
......@@ -85,6 +91,12 @@ import org.fortiss.af3.project.model.typesystem.IType;
import org.fortiss.af3.project.model.typesystem.ITypeDefinition;
import org.fortiss.af3.project.utils.TypeScopeUtils;
import com.microsoft.z3.ArithExpr;
import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;
import com.microsoft.z3.Expr;
import com.microsoft.z3.IntExpr;
/**
* Utility class for everything related to the expressions language.
*
......@@ -781,4 +793,164 @@ public class ExpressionUtils {
public static boolean isStructureType(IType t) {
return t instanceof TDefinedType && ((TDefinedType)t).getDef() instanceof Structure;
}
/**
* Recursively transforms a {@link ITerm} into a {@link Expr}.
*
* {@link BoolConst}s, {@link IntConst}s, {@link DoubleConst}s, {@link Var}s,
* {@link FunctionCall}s with a {@link PredefinedFunction}s and Assignments can be
* transformed.
*
* @param prefix
* - a prefix used to identify the {@link ITerm}.
* @param ctx
* - the z3 {@link Context}.
* @param term
* - the {@link ITerm} to be transformed.
* @return the {@link Expr} for an {@link ITerm} or <code>null</code> for invalid inputs.
*/
public static Expr expressionToZ3(String prefix, Context ctx, ITerm term) {
if(term instanceof BoolConst) {
return ctx.mkBool(((BoolConst)term).getValue());
}
if(term instanceof IntConst) {
return ctx.mkInt(((IntConst)term).getValue());
}
if(term instanceof DoubleConst) {
return ctx.mkReal(Double.toString(((DoubleConst)term).getValue()));
}
if(term instanceof Var) {
Var var = (Var)term;
return createVarOfType(getVarType(var), prefix + var.getIdentifier(), ctx);
}
if(term instanceof FunctionCall) {
IFunction function = ((FunctionCall)term).getFunction();
if(function instanceof PredefinedFunction) {
PredefinedFunction predefinedFunction = (PredefinedFunction)function;
EOperator operator = predefinedFunction.getOperator();
EList<ITerm> arguments = ((FunctionCall)term).getArguments();
if(arguments.size() == 1) {
// The if clause assures that the list contains exactly one argument.
Expr arg0 = expressionToZ3(prefix, ctx, arguments.get(0));
return unaryOperator(ctx, operator, arg0);
}
if(arguments.size() == 2) {
// The if clause assures that the list contains exactly two arguments.
Expr arg0 = expressionToZ3(prefix, ctx, arguments.get(0));
Expr arg1 = expressionToZ3(prefix, ctx, arguments.get(1));
return binaryOperator(ctx, operator, arg0, arg1);
}
return multipleOperator(prefix, ctx, operator, arguments);
}
}
if(term instanceof Assignment) {
Assignment assignment = (Assignment)term;
Var variable = assignment.getVariable();
Expr rhs = expressionToZ3(prefix, ctx, assignment.getValue());
Expr lhs =
createVarOfType(getVarType(variable), prefix + variable.getIdentifier(), ctx);
if(lhs != null) {
return ctx.mkEq(lhs, rhs);
}
}
return null;
}
/** Unary Operators of {@link PredefinedFunction}. */
private static Expr unaryOperator(Context ctx, EOperator operator, Expr arg0) {
switch(operator) {
case NOT:
return ctx.mkNot((BoolExpr)arg0);
case NEGATE:
return ctx.mkUnaryMinus((ArithExpr)arg0);
default:
return null;
}
}
/** Binary Operators of {@link PredefinedFunction}. */
private static Expr binaryOperator(Context ctx, EOperator operator, Expr arg0, Expr arg1) {
switch(operator) {
case ADD:
return ctx.mkAdd((ArithExpr)arg0, (ArithExpr)arg1);
case SUBTRACT:
return ctx.mkSub((ArithExpr)arg0, (ArithExpr)arg1);
case MULTIPLY:
return ctx.mkMul((ArithExpr)arg0, (ArithExpr)arg1);
case DIVIDE:
return ctx.mkDiv((ArithExpr)arg0, (ArithExpr)arg1);
case MODULO:
return ctx.mkMod((IntExpr)arg0, (IntExpr)arg1);
case LOWER_THAN:
return ctx.mkLt((ArithExpr)arg0, (ArithExpr)arg1);
case GREATER_THAN:
return ctx.mkGt((ArithExpr)arg0, (ArithExpr)arg1);
case LOWER_EQUAL:
return ctx.mkLe((ArithExpr)arg0, (ArithExpr)arg1);
case GREATER_EQUAL:
return ctx.mkGe((ArithExpr)arg0, (ArithExpr)arg1);
case EQUAL:
return ctx.mkEq(arg0, arg1);
case NOT_EQUAL:
return ctx.mkNot(ctx.mkEq(arg0, arg1));
case OR:
return ctx.mkOr((BoolExpr)arg0, (BoolExpr)arg1);
case AND:
return ctx.mkAnd((BoolExpr)arg0, (BoolExpr)arg1);
default:
return null;
}
}
/** Operator with multiple arguments of {@link PredefinedFunction}. */
private static Expr multipleOperator(String prefix, Context ctx, EOperator operator,
EList<ITerm> args) {
if(operator == EOperator.ADD || operator == EOperator.SUBTRACT ||
operator == EOperator.MULTIPLY) {
List<ArithExpr> tmp = args.stream().map(e -> (ArithExpr)expressionToZ3(prefix, ctx, e))
.collect(Collectors.toList());
switch(operator) {
case ADD:
return ctx.mkAdd(tmp.toArray(new ArithExpr[tmp.size()]));
case SUBTRACT:
return ctx.mkSub(tmp.toArray(new ArithExpr[tmp.size()]));
case MULTIPLY:
return ctx.mkMul(tmp.toArray(new ArithExpr[tmp.size()]));
}
}
if(operator == EOperator.OR || operator == EOperator.AND) {
List<BoolExpr> tmp = args.stream().map(e -> (BoolExpr)expressionToZ3(prefix, ctx, e))
.collect(Collectors.toList());
switch(operator) {
case OR:
return ctx.mkOr(tmp.toArray(new BoolExpr[tmp.size()]));
case AND:
return ctx.mkAnd(tmp.toArray(new BoolExpr[tmp.size()]));
}
}
return null;
}
/**
* @param type
* - the {@link IType} of the variable.
* @param name
* - the name of the variable.
* @param ctx
* - the Z3 {@link Context}
* @return
* - the corresponding Z3 {@link Expr}.
*/
private static Expr createVarOfType(IType type, String name, Context ctx) {
if(type instanceof TBool) {
return ctx.mkBoolConst(name);
}
if(type instanceof TInt) {
return ctx.mkIntConst(name);
}
if(type instanceof TDouble) {
return ctx.mkRealConst(name);
}
return null;
}
}
......@@ -4,7 +4,7 @@ ExternalSystemHandler.java 0b8613287068e6cd7dad78b52e1511a4ce58c8c1 GREEN
GlossaryEntryHandler.java e8d9100791c218e8897cf64f1beaf6afb42adeb5 GREEN
GlossaryHandler.java 5399ca3ba430b1f25f40e2b8f99fea126e686d34 GREEN
RequirementDocumentHandler.java cc7fd71e170994ce39896012a72ad939c5fa8888 GREEN
RequirementHandler.java 7f74239187d1cbe85c7b4820a27ee91579e7b61c GREEN
RequirementHandler.java faad09fcfac2d40a44396869f8a0eda15e6b84d2 GREEN
RequirementRelationStatusHandler.java 4fca19e5048f4379ff98228c0b3065bfeb90122e GREEN
RequirementSourceHandler.java 032d9d026478ccf43711d15056763a70e8c21a8e GREEN
RequirementSpecificationHandler.java 8b40f9f3be20cdd70d7c7f9822c4e14c462284b7 GREEN
......
......@@ -23,6 +23,7 @@ import static org.fortiss.af3.mira.ui.utils.RequirementUtils.getRequirementNavig
import java.util.ArrayList;
import java.util.List;
import org.eclipse.emf.common.util.TreeIterator;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.jface.resource.ImageDescriptor;
import org.fortiss.af3.mira.model.DerivedRequirementSpecification;
......@@ -36,6 +37,7 @@ import org.fortiss.af3.mira.model.safety.HazardRequirementSpecification;
import org.fortiss.af3.mira.model.safety.MooNSolutionRequirementSpecification;
import org.fortiss.af3.mira.model.timing.TimingRequirement;
import org.fortiss.af3.project.model.ParameterDefinition;
import org.fortiss.af3.testing.model.TestSuite;
import org.fortiss.tooling.base.model.element.IModelElementSpecification;
import org.fortiss.tooling.kernel.ui.extension.IModelElementHandler;
import org.fortiss.tooling.kernel.ui.extension.base.NamedCommentedModelElementHandlerBase;
......@@ -66,7 +68,15 @@ public class RequirementHandler extends NamedCommentedModelElementHandlerBase<Re
/** {@inheritDoc} */
@Override
public List<EObject> getSubnodes(Requirement element) {
return new ArrayList<EObject>(element.getContainedElements());
List<EObject> list = new ArrayList<EObject>(element.getContainedElements());
TreeIterator<EObject> treeIterator = element.eAllContents();
while(treeIterator.hasNext()) {
EObject eObject = treeIterator.next();
if(eObject instanceof TestSuite) {
list.add(eObject);
}
}
return list;
}
/** {@inheritDoc} */
......
......@@ -236,7 +236,9 @@ ocraTerm returns [IExpressionTerm result] :
| '(' e1=primaryTerm 'until' e2=primaryTerm ')' {$result = createBinaryOCRATerm(BinaryModalOperator.UNTIL, $e1.result, $e2.result);}
| '(' e1=primaryTerm 'releases' e2=primaryTerm ')'{$result = createBinaryOCRATerm(BinaryModalOperator.RELEASES, $e1.result, $e2.result);}
| '(' e1=primaryTerm 'since' e2=primaryTerm ')'{$result = createBinaryOCRATerm(BinaryModalOperator.SINCE, $e1.result, $e2.result);}
| '(' e1=primaryTerm 'triggered' e2=primaryTerm ')'{$result = createBinaryOCRATerm(BinaryModalOperator.TRIGGERED, $e1.result, $e2.result);}
| '(' e1=primaryTerm 'triggered' e2=primaryTerm ')'{$result = createBinaryOCRATerm(BinaryModalOperator.TRIGGERED, $e1.result, $e2.result);}
| '(' e1=primaryTerm 'within' e3=nativeJavaInt ')'{$result = createWithin($e1.result, $e3.result);}
;
varidConstTermInParenthesis returns [Var result] :
......
ocra.ecore 80c48750dfaa43765f96fee650e8c76082ea0e17 RED
ocra.ecore abcdb56b11219ed0179826a23de9dbb79683d8e5 RED
......@@ -106,6 +106,16 @@
<eStructuralFeatures xsi:type="ecore:EReference" name="port" eType="ecore:EClass platform:/resource/org.fortiss.af3.expression/model/expression.ecore#//terms/Var"
containment="true"/>
</eClassifiers>
<eClassifiers xsi:type="ecore:EClass" name="Within" eSuperTypes="#//contract/ocraterms/OthelloConstraint">
<eOperations name="toString" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EString">
<eAnnotations source="http://www.eclipse.org/emf/2002/GenModel">
<details key="body" value="return OthelloConstraintStaticImpl.toStringTimedFuture(this);"/>
</eAnnotations>
</eOperations>
<eStructuralFeatures xsi:type="ecore:EReference" name="futureExpression" eType="ecore:EClass platform:/resource/org.fortiss.af3.expression/model/expression.ecore#//terms/IExpressionTerm"
containment="true"/>
<eStructuralFeatures xsi:type="ecore:EAttribute" name="timeLimit" eType="ecore:EDataType http://www.eclipse.org/emf/2002/Ecore#//EInt"/>
</eClassifiers>
</eSubpackages>
</eSubpackages>
<eSubpackages name="types" nsURI="http://www.fortiss.org/af3/ocra/types" nsPrefix="org-fortiss-af3-ocra-types">
......
......@@ -89,6 +89,13 @@
<genOperations ecoreOperation="ocra.ecore#//contract/ocraterms/PortChange/toString"
body="return OthelloConstraintStaticImpl.toStringChangeTerm(this);"/>
</genClasses>
<genClasses ecoreClass="ocra.ecore#//contract/ocraterms/Within">
<genFeatures notify="false" createChild="false" propertySortChoices="true"
ecoreFeature="ecore:EReference ocra.ecore#//contract/ocraterms/Within/futureExpression"/>
<genFeatures createChild="false" ecoreFeature="ecore:EAttribute ocra.ecore#//contract/ocraterms/Within/timeLimit"/>
<genOperations ecoreOperation="ocra.ecore#//contract/ocraterms/Within/toString"
body="return OthelloConstraintStaticImpl.toStringTimedFuture(this);"/>
</genClasses>
</nestedGenPackages>
</nestedGenPackages>
<nestedGenPackages prefix="Types" basePackage="org.fortiss.af3.ocra.model" disposableProviderFactory="true"
......
......@@ -60,8 +60,10 @@
</transformationProvider>
<transformationProvider transformationName="booleanComparisonWorkaroundTransformationForOCRA">
<transformation transformation="org.fortiss.af3.ocra.generator.nusmv.OCRABooleanComparisonWorkaroundTransformation"></transformation>
</transformationProvider>
</transformationProvider>
<transformationProvider transformationName="transformUserDefinedOCRAExpressions">
<transformation transformation="org.fortiss.af3.ocra.generator.nusmv.TransformUserDefinedOCRAExpressions"></transformation>
</transformationProvider>
</extension>
</plugin>
ContractConstraintChecker.java aee130ec91b8c6aa3599bf8a5d914ba5295c4f98 GREEN
OCRATypeChecker.java 2b43bebbc057672317cbae60211fec801152bd53 GREEN
OCRATypeChecker.java cf84112f30615683e77c96e22a1e37d443e309b5 GREEN
package org.fortiss.af3.ocra.constraint;
import static org.fortiss.af3.expression.language.TypeCheckStatus.combineStatuses;
import static org.fortiss.af3.expression.language.TypeCheckStatus.errorStatus;
import static org.fortiss.af3.expression.language.TypeCheckStatus.nullTermStatus;
import static org.fortiss.af3.expression.language.TypeCheckStatus.ok;
......@@ -14,6 +15,7 @@ import org.fortiss.af3.ocra.model.contract.ocraterms.BinaryOCRATerm;
import org.fortiss.af3.ocra.model.contract.ocraterms.OthelloConstraint;
import org.fortiss.af3.ocra.model.contract.ocraterms.PortChange;
import org.fortiss.af3.ocra.model.contract.ocraterms.UnaryOCRATerm;
import org.fortiss.af3.ocra.model.contract.ocraterms.Within;
import org.fortiss.af3.project.model.typesystem.ITerm;
import org.fortiss.af3.project.model.typesystem.IType;
import org.fortiss.af3.project.model.typesystem.IVariableDefinition;
......@@ -54,13 +56,17 @@ public class OCRATypeChecker extends TypeChecker {
}
return errorStatus(vd.getVar().getIdentifier() + " is not an output port.");
}
if(term instanceof Within) {
Within tf = (Within)term;
return typecheck(tf.getFutureExpression(), boolType(), context);
}
// At this point term is a {@link BinaryOCRATerm} as remaining options have been ruled out.
// There are only 3 kinds of {@link OthelloConstraint}.
IExpressionTerm e1 = ((BinaryOCRATerm)term).getFirstCondition();
IExpressionTerm e2 = ((BinaryOCRATerm)term).getSecondCondition();
return TypeCheckStatus.combineStatuses(typecheck(e1, boolType(), context),
return combineStatuses(typecheck(e1, boolType(), context),
typecheck(e2, boolType(), context));
}
}
OCRABooleanComparisonWorkaroundTransformation.java 9503d6616ae216b0da0023637f2676142ce80adc GREEN
ResolveNoVal.java 507f5f2038f469b1524c9d307286b13d891d697e GREEN
TransformUserDefinedOCRAExpressions.java 3782e214353820063cf4d009a2129bed9286f0f1 GREEN
/*-------------------------------------------------------------------------+
| Copyright 2017 fortiss GmbH |
| |
| Licensed under the Apache License, Version 2.0 (the "License"); |
| you may not use this file except in compliance with the License. |
| You may obtain a copy of the License at |
| |
| http://www.apache.org/licenses/LICENSE-2.0 |
| |
| Unless required by applicable law or agreed to in writing, software |
| distributed under the License is distributed on an "AS IS" BASIS, |
| WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. |
| See the License for the specific language governing permissions and |
| limitations under the License. |
+--------------------------------------------------------------------------*/
package org.fortiss.af3.ocra.generator.nusmv;
import static org.eclipse.emf.ecore.util.EcoreUtil.copy;
import static org.eclipse.emf.ecore.util.EcoreUtil.replace;
import static org.fortiss.af3.expression.utils.ExpressionModelElementFactory.or;
import static org.fortiss.af3.ocra.utils.OCRAContractFactory.createUnaryOCRATerm;
import static org.fortiss.tooling.kernel.utils.EcoreUtils.getChildrenWithType;
import java.util.ArrayList;
import java.util.List;
import org.eclipse.emf.common.util.EList;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.expression.model.terms.IExpressionTerm;
import org.fortiss.af3.ocra.model.contract.Contract;
import org.fortiss.af3.ocra.model.contract.ocraterms.UnaryModalOperator;
import org.fortiss.af3.ocra.model.contract.ocraterms.Within;
import org.fortiss.pragmatictransformation.service.CacheSupportedTransformationBase;
import org.fortiss.pragmatictransformation.service.IPragmaticTransformation;
/**
* <p>
* OCRA does not handle {@code x==y} kind of expressions properly when {@code x, y} are booleans,
* i.e., it produces an error when the specification contains equality or inequality operators
* between booleans.
* </p>
*
* <p>
* This class transforms {@code x==y} to {@code x && y || !x && !y}.
* </p>
*
* @author kanav
*/
public class TransformUserDefinedOCRAExpressions extends CacheSupportedTransformationBase {
/** {@inheritDoc} */
@Override
public Object transform(Object c, IPragmaticTransformation deferredTransformation) {
if(c instanceof Component) {
getChildrenWithType((Component)c, Contract.class)
.forEach(con -> deferredTransformation.buildTransformation(con));
return c;
} else if(c instanceof Contract) {
EList<Within> timeFutureExps = getChildrenWithType((Contract)c, Within.class);
for(Within wi : timeFutureExps) {
List<IExpressionTerm> exps = new ArrayList<IExpressionTerm>();
IExpressionTerm fExp = copy(wi.getFutureExpression());
// It means weak causality. In case we want strong causality we have to remove only
// this line.
exps.add(copy(fExp));
for(int i = 1; i <= wi.getTimeLimit(); i++) {
fExp = createUnaryOCRATerm(UnaryModalOperator.THEN, copy(fExp));
exps.add(copy(fExp));
}
replace(wi, or(exps));
}
return c;
}
return null;
}
}
OthelloConstraintStaticImpl.java acd991023b661233bd10364585bcc5f836c8f28a GREEN
OthelloConstraintStaticImpl.java 1fec3b4e4016e38eb229ba1ad4503544a5f6157c GREEN
......@@ -23,6 +23,7 @@ import org.fortiss.af3.ocra.model.contract.ocraterms.BinaryOCRATerm;
import org.fortiss.af3.ocra.model.contract.ocraterms.OthelloConstraint;
import org.fortiss.af3.ocra.model.contract.ocraterms.PortChange;
import org.fortiss.af3.ocra.model.contract.ocraterms.UnaryOCRATerm;
import org.fortiss.af3.ocra.model.contract.ocraterms.Within;
/**
* The complex implementation for methods of {@link OthelloConstraintImpl}.
......@@ -81,4 +82,10 @@ public class OthelloConstraintStaticImpl {
// Only done because this is required by the OCRA language
return "change(" + pc.getPort().getIdentifier() + ")";
}
/** Converts a {@link Within} expression to a {@link String}. */
public static String toStringTimedFuture(Within wi) {
// Only done because this is required by the OCRA language
return "((" + wi.getFutureExpression() + ") within " + wi.getTimeLimit() + ")";
}
}
OCRAContractFactory.java 30fcfe4fe45834ad4912222b9c9880b2e5ec3f2b GREEN
OCRAContractFactory.java b87e78591535536dba7bb3934dcdfc9bf87d30ca GREEN
OCRAContractUtils.java 5c402a6d13571c2a191072c27693d3065cb33021 GREEN
......@@ -28,6 +28,7 @@ import org.fortiss.af3.ocra.model.contract.ocraterms.OcratermsFactory;
import org.fortiss.af3.ocra.model.contract.ocraterms.PortChange;
import org.fortiss.af3.ocra.model.contract.ocraterms.UnaryModalOperator;
import org.fortiss.af3.ocra.model.contract.ocraterms.UnaryOCRATerm;
import org.fortiss.af3.ocra.model.contract.ocraterms.Within;
/**
* This class provides the factory methods for OCRA model elements.
......@@ -95,4 +96,12 @@ public class OCRAContractFactory {
pc.setPort(v);
return pc;
}
/** Create the timed future expression. */
public static Within createWithin(IExpressionTerm futureExpression, int timeLimit) {
Within wi = OcratermsFactory.eINSTANCE.createWithin();
wi.setFutureExpression(futureExpression);
wi.setTimeLimit(timeLimit);
return wi;
}
}
ContractEditorConfiguration.java da1319d3e4dda5fe41e449683e719200d361eaa2 GREEN
ContractEditorConfiguration.java 73f421a02775dd25450df99bf838bfb9574d793e GREEN
ContractSpecificationEditor.java e6d58bc217a787af5f8eb350aa2c3408a49a939e GREEN
ContractSpecificationEditorBinding.java 0f2a12493c81bcb0cdbbaea5f23127400d1a75f1 GREEN
......@@ -60,6 +60,7 @@ public class ContractEditorConfiguration
keywords.add("since");
keywords.add("triggered");
keywords.add("change");
keywords.add("within");
keywords.add("NoVal");
addWordsToRule(keywords, keywordsRule, keywordToken);
......
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