VerifyValidator.java
/**
* Copyright (c) 2004-2025 Carnegie Mellon University and others. (see Contributors file).
* All Rights Reserved.
*
* NO WARRANTY. ALL MATERIAL IS FURNISHED ON AN "AS-IS" BASIS. CARNEGIE MELLON UNIVERSITY MAKES NO WARRANTIES OF ANY
* KIND, EITHER EXPRESSED OR IMPLIED, AS TO ANY MATTER INCLUDING, BUT NOT LIMITED TO, WARRANTY OF FITNESS FOR PURPOSE
* OR MERCHANTABILITY, EXCLUSIVITY, OR RESULTS OBTAINED FROM USE OF THE MATERIAL. CARNEGIE MELLON UNIVERSITY DOES NOT
* MAKE ANY WARRANTY OF ANY KIND WITH RESPECT TO FREEDOM FROM PATENT, TRADEMARK, OR COPYRIGHT INFRINGEMENT.
*
* This program and the accompanying materials are made available under the terms of the Eclipse Public License 2.0
* which is available at https://www.eclipse.org/legal/epl-2.0/
* SPDX-License-Identifier: EPL-2.0
*
* Created, in part, with funding and support from the United States Government. (see Acknowledgments file).
*
* This program includes and/or can make use of certain third party source code, object code, documentation and other
* files ("Third Party Software"). The Third Party Software that is used by this program is dependent upon your system
* configuration. By using this program, You agree to comply with any and all relevant Third Party Software terms and
* conditions contained in any such Third Party Software or separate license file distributed with such Third Party
* Software. The parties who own the Third Party Software ("Third Party Licensors") are intended third party benefici-
* aries to this license with respect to the terms applicable to their Third Party Software. Third Party Software li-
* censes only apply to the Third Party Software and not any other portion of this program or this program as a whole.
*/
package org.osate.verify.validation;
import com.google.common.base.Objects;
import com.google.inject.Inject;
import java.lang.reflect.Method;
import java.util.ArrayList;
import java.util.List;
import java.util.Set;
import java.util.function.Consumer;
import org.eclipse.emf.common.util.EList;
import org.eclipse.emf.common.util.URI;
import org.eclipse.emf.ecore.EClass;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.EPackage;
import org.eclipse.emf.ecore.util.EcoreUtil;
import org.eclipse.xtext.EcoreUtil2;
import org.eclipse.xtext.validation.Check;
import org.eclipse.xtext.xbase.lib.Conversions;
import org.eclipse.xtext.xbase.lib.Functions.Function1;
import org.eclipse.xtext.xbase.lib.IterableExtensions;
import org.eclipse.xtext.xbase.lib.ListExtensions;
import org.eclipse.xtext.xbase.lib.Procedures.Procedure2;
import org.osate.aadl2.Aadl2Factory;
import org.osate.aadl2.AadlBoolean;
import org.osate.aadl2.AadlInteger;
import org.osate.aadl2.AadlReal;
import org.osate.aadl2.AadlString;
import org.osate.aadl2.ComponentCategory;
import org.osate.aadl2.Connection;
import org.osate.aadl2.EndToEndFlow;
import org.osate.aadl2.Feature;
import org.osate.aadl2.MetaclassReference;
import org.osate.aadl2.NamedElement;
import org.osate.aadl2.Property;
import org.osate.aadl2.PropertyExpression;
import org.osate.aadl2.PropertyType;
import org.osate.aadl2.ReferenceType;
import org.osate.alisa.common.common.AVariableDeclaration;
import org.osate.alisa.common.common.AVariableReference;
import org.osate.alisa.common.common.ComputeDeclaration;
import org.osate.alisa.common.common.ModelRef;
import org.osate.alisa.common.common.PropertyRef;
import org.osate.alisa.common.common.TargetType;
import org.osate.alisa.common.common.TypeRef;
import org.osate.pluginsupport.ExecuteJavaUtil;
import org.osate.reqspec.reqSpec.ReqPredicate;
import org.osate.reqspec.reqSpec.Requirement;
import org.osate.reqspec.reqSpec.RequirementSet;
import org.osate.reqspec.reqSpec.SystemRequirementSet;
import org.osate.reqspec.reqSpec.ValuePredicate;
import org.osate.resolute.ResoluteUtil;
import org.osate.verify.internal.util.IVerifyGlobalReferenceFinder;
import org.osate.verify.internal.util.VerificationMethodDispatchers;
import org.osate.verify.internal.util.VerifyJavaUtil;
import org.osate.verify.internal.util.VerifyUtilExtension;
import org.osate.verify.typing.validation.VerifyTypeSystemValidator;
import org.osate.verify.verify.AgreeMethod;
import org.osate.verify.verify.Claim;
import org.osate.verify.verify.ComputeRef;
import org.osate.verify.verify.FormalParameter;
import org.osate.verify.verify.JUnit4Method;
import org.osate.verify.verify.JavaMethod;
import org.osate.verify.verify.MethodKind;
import org.osate.verify.verify.PluginMethod;
import org.osate.verify.verify.ResoluteMethod;
import org.osate.verify.verify.Verification;
import org.osate.verify.verify.VerificationActivity;
import org.osate.verify.verify.VerificationCondition;
import org.osate.verify.verify.VerificationMethod;
import org.osate.verify.verify.VerificationMethodRegistry;
import org.osate.verify.verify.VerificationPlan;
import org.osate.verify.verify.VerifyPackage;
/**
* Custom validation rules.
*
* see http://www.eclipse.org/Xtext/documentation.html#validation
*/
@SuppressWarnings("all")
public class VerifyValidator extends VerifyTypeSystemValidator {
public static final String INCORRECT_METHOD_PATH = "org.osate.verify.incorrectMethodPath";
public static final String INCORRECT_CLASS_PATH = "org.osate.verify.incorrectClassPath";
public static final String INCORRECT_METHOD_REFERENCE = "org.osate.verify.incorrectMethodReference";
public static final String MISSING_METHOD_REFERENCE = "org.osate.verify.missingMethodReference";
public static final String INCORRECT_METHOD_ID = "org.osate.verify.incorrectMethodID";
public static final String CLAIM_MISSING_REQUIREMENT = "org.osate.verify.claimMissingRequirement";
public static final String CLAIM_INVALID_REQUIREMENT = "org.osate.verify.claimInvalidRequirement";
public static final String MISSING_CLAIM_FOR_REQ = "org.osate.verify.missingClaimForReq";
public static final String MISSING_CLAIM_FOR_MULTIPLE_REQ = "org.osate.verify.missingClaimForMultipleReq";
public static final String CLAIM_REQ_FOR_NOT_VP_FOR = "org.osate.verify.claimReqForNotVpFor";
public static final String ILLEGAL_OBJECT_FOR_FILETYPE = "org.osate.verify.illegal.object.for.filetype";
public static final String MISSING_REQUIREMENTS_FOR_MULTIPLE_CLAIMS = "org.osate.verify.missingRequirementsForMultipleClaims";
public static final String MULTIPLE_CLAIMS_WITH_DUPLICATE_REQUIREMENTS = "org.osate.verify.multipleClaimsWithDuplicateRequirements";
public static final String METHOD_PARMS_DO_NOT_MATCH_RESOLUTE_DEFINITION = "org.osate.verify.METHOD_PARMS_DO_NOT_MATCH_RESOLUTE_DEFINITION";
public static final String MISMATCHED_TARGET = "org.osate.verify.MISMATCHED_TARGET";
@Override
protected List<EPackage> getEPackages() {
List<EPackage> _ePackages = super.getEPackages();
final List<EPackage> result = new ArrayList<EPackage>(_ePackages);
result.add(VerifyPackage.eINSTANCE);
result.add(EPackage.Registry.INSTANCE.getEPackage("http://aadl.info/AADL/2.0"));
return result;
}
@Inject
private IVerifyGlobalReferenceFinder verifyGlobalRefFinder;
@Check
public void deprecateVerificationMethodBoolReport(final VerificationMethod vm) {
boolean _isIsPredicate = vm.isIsPredicate();
if (_isIsPredicate) {
this.warning("Keyword \'boolean\' is deprecated", VerifyPackage.Literals.VERIFICATION_METHOD__IS_PREDICATE);
}
boolean _isIsResultReport = vm.isIsResultReport();
if (_isIsResultReport) {
this.warning("Keyword \'report\' is deprecated", VerifyPackage.Literals.VERIFICATION_METHOD__IS_RESULT_REPORT);
}
}
@Check
public void checkMethodPath(final JavaMethod method) {
final ArrayList<Class<?>> params = VerifyJavaUtil.getParameterClasses(method);
final Method result = ExecuteJavaUtil.getJavaMethod(method.getMethodPath(), ((Class<?>[])Conversions.unwrapArray(params, Class.class)));
if ((result == null)) {
String _methodPath = method.getMethodPath();
String _plus = ("Could not find method: " + _methodPath);
this.warning(_plus, VerifyPackage.Literals.JAVA_METHOD__METHOD_PATH,
VerifyValidator.INCORRECT_METHOD_PATH);
}
}
@Check
public void checkClassPath(final JUnit4Method method) {
final Class<?> result = ExecuteJavaUtil.getJavaClass(method.getClassPath());
if ((result == null)) {
String _classPath = method.getClassPath();
String _plus = ("Could not find JUnit4 test class: " + _classPath);
this.warning(_plus,
VerifyPackage.Literals.JUNIT4_METHOD__CLASS_PATH, VerifyValidator.INCORRECT_CLASS_PATH);
}
}
@Check
public void checkMethodID(final PluginMethod method) {
final Object result = VerificationMethodDispatchers.eInstance.dispatchVerificationMethod(method, null, null);
if ((result == null)) {
this.warning("Plugin verification method ID not found", VerifyPackage.Literals.PLUGIN_METHOD__METHOD_ID,
VerifyValidator.INCORRECT_METHOD_ID);
}
}
@Check
public void checkAgreeMethod(final AgreeMethod method) {
this.warning("Execution of AGREE verification methods is not supported",
VerifyPackage.Literals.VERIFICATION_METHOD__METHOD_KIND);
}
@Check
public void checkMethodReference(final VerificationCondition cond) {
VerificationMethod _method = cond.getMethod();
boolean _tripleEquals = (_method == null);
if (_tripleEquals) {
this.warning("Verification precondition or validation should have a verification method reference",
VerifyPackage.Literals.VERIFICATION_CONDITION__METHOD, VerifyValidator.MISSING_METHOD_REFERENCE);
}
}
@Check
public void checkMissingMethodReference(final VerificationActivity va) {
VerificationMethod _method = va.getMethod();
boolean _tripleEquals = (_method == null);
if (_tripleEquals) {
this.warning("Verification activity should have a method reference",
VerifyPackage.Literals.VERIFICATION_ACTIVITY__METHOD, VerifyValidator.MISSING_METHOD_REFERENCE);
}
}
@Check
public void checkConsistentTarget(final VerificationActivity va) {
final VerificationMethod vm = va.getMethod();
if ((vm != null)) {
Claim _containingClaim = VerifyUtilExtension.getContainingClaim(va);
Requirement _requirement = null;
if (_containingClaim!=null) {
_requirement=_containingClaim.getRequirement();
}
final Requirement req = _requirement;
NamedElement _targetElement = null;
if (req!=null) {
_targetElement=req.getTargetElement();
}
final NamedElement target = _targetElement;
EList<ComponentCategory> _componentCategory = null;
if (req!=null) {
_componentCategory=req.getComponentCategory();
}
final EList<ComponentCategory> cat = _componentCategory;
if (((target == null) && (((!cat.isEmpty()) || Objects.equal(req.getTargetType(), TargetType.COMPONENT)) || Objects.equal(req.getTargetType(),
TargetType.ROOT)))) {
boolean _not = (!(((vm.getTargetType() == TargetType.COMPONENT) || (vm.getTargetType() == TargetType.ELEMENT)) ||
(vm.getTargetType() == TargetType.ROOT)));
if (_not) {
this.error(
"Requirement is for component while verification method is not for component, element, or root", va, VerifyPackage.Literals.VERIFICATION_ACTIVITY__METHOD, VerifyValidator.MISMATCHED_TARGET);
}
} else {
if ((((req.getTargetType() == TargetType.FEATURE) || (target instanceof Feature)) &&
(!(((vm.getTargetType() == TargetType.FEATURE) || (vm.getTargetType() == TargetType.ELEMENT)) ||
(vm.getMethodKind() instanceof PluginMethod))))) {
this.error("Requirement is for Feature while verification method is not for Feature", va,
VerifyPackage.Literals.VERIFICATION_ACTIVITY__METHOD, VerifyValidator.MISMATCHED_TARGET);
} else {
if ((((req.getTargetType() == TargetType.FLOW) || (target instanceof EndToEndFlow)) &&
(!(((vm.getTargetType() == TargetType.FLOW) || (vm.getTargetType() == TargetType.ELEMENT)) ||
(vm.getMethodKind() instanceof PluginMethod))))) {
this.error("Requirement is for Flow while verification method is not for Flow", va,
VerifyPackage.Literals.VERIFICATION_ACTIVITY__METHOD, VerifyValidator.MISMATCHED_TARGET);
} else {
if ((((req.getTargetType() == TargetType.CONNECTION) || (target instanceof Connection)) &&
(!(((vm.getTargetType() == TargetType.CONNECTION) || (vm.getTargetType() == TargetType.ELEMENT)) ||
(vm.getMethodKind() instanceof PluginMethod))))) {
this.error("Requirement is for Flow while verification method is not for Flow", va,
VerifyPackage.Literals.VERIFICATION_ACTIVITY__METHOD, VerifyValidator.MISMATCHED_TARGET);
}
}
}
}
}
}
@Check
public void checkVerificationActivityParams(final VerificationActivity va) {
final EList<PropertyExpression> actualParameters = va.getActuals();
final VerificationMethod method = va.getMethod();
final EList<FormalParameter> expectedParms = method.getFormals();
int _size = expectedParms.size();
int _size_1 = actualParameters.size();
boolean _notEquals = (_size != _size_1);
if (_notEquals) {
this.warning(
"The number of actual parameters differs from the number of formal parameters for verification activity", va, VerifyPackage.Literals.VERIFICATION_ACTIVITY__METHOD);
}
}
@Check
public void checkVerificationActivityReturnCompute(final VerificationActivity va) {
final EList<ComputeRef> computeParameters = va.getComputes();
boolean _isEmpty = computeParameters.isEmpty();
if (_isEmpty) {
return;
}
final VerificationMethod method = va.getMethod();
final EList<FormalParameter> resultParms = method.getResults();
int _size = computeParameters.size();
int _size_1 = resultParms.size();
boolean _greaterThan = (_size > _size_1);
if (_greaterThan) {
this.error("The number of actual return parameters is less than the number of compute variable assignments", va,
VerifyPackage.Literals.VERIFICATION_ACTIVITY__COMPUTES);
}
Claim _containingClaim = VerifyUtilExtension.getContainingClaim(va);
Requirement _requirement = null;
if (_containingClaim!=null) {
_requirement=_containingClaim.getRequirement();
}
ReqPredicate _predicate = null;
if (_requirement!=null) {
_predicate=_requirement.getPredicate();
}
final ReqPredicate predicate = _predicate;
if ((predicate instanceof ValuePredicate)) {
final List<AVariableReference> varrefs = EcoreUtil2.<AVariableReference>getAllContentsOfType(predicate, AVariableReference.class);
for (final AVariableReference varref : varrefs) {
{
final AVariableDeclaration variable = varref.getVariable();
if ((variable instanceof ComputeDeclaration)) {
final Function1<ComputeRef, Boolean> _function = (ComputeRef cp) -> {
ComputeDeclaration _compute = cp.getCompute();
return Boolean.valueOf(Objects.equal(_compute, variable));
};
boolean _exists = IterableExtensions.<ComputeRef>exists(computeParameters, _function);
boolean _not = (!_exists);
if (_not) {
String _name = ((ComputeDeclaration)variable).getName();
String _plus = ("Compute variable \'" + _name);
String _plus_1 = (_plus +
"\' used in value predicate but not assigned in method call");
this.error(_plus_1, va,
VerifyPackage.Literals.VERIFICATION_ACTIVITY__COMPUTES);
}
}
}
}
}
}
@Check
public void checkForDuplicateClaims(final VerificationPlan vp) {
final EList<Claim> claims = vp.getClaim();
final Consumer<Claim> _function = (Claim it) -> {
EcoreUtil.resolveAll(it);
};
claims.forEach(_function);
final String vpUri = EcoreUtil.getURI(vp).toString();
final Consumer<Claim> _function_1 = (Claim claim) -> {
final Function1<Claim, Boolean> _function_2 = (Claim it) -> {
return Boolean.valueOf(((!Objects.equal(it, claim)) && Objects.equal(it.getRequirement(), claim.getRequirement())));
};
final Iterable<Claim> possibleDuplicates = IterableExtensions.<Claim>filter(claims, _function_2);
int _size = IterableExtensions.size(possibleDuplicates);
boolean _greaterThan = (_size > 0);
if (_greaterThan) {
final ArrayList<String> duplicateUris = new ArrayList<String>();
duplicateUris.add(vpUri);
duplicateUris.add(claim.getRequirement().getName());
final Consumer<Claim> _function_3 = (Claim it) -> {
duplicateUris.add(EcoreUtil.getURI(it).toString());
};
possibleDuplicates.forEach(_function_3);
this.warning("Multiple Claims with duplicate Requirements", claim, VerifyPackage.Literals.CLAIM__REQUIREMENT,
VerifyValidator.MULTIPLE_CLAIMS_WITH_DUPLICATE_REQUIREMENTS, ((String[])Conversions.unwrapArray(duplicateUris, String.class)));
}
};
claims.forEach(_function_1);
}
@Check
public void checkMultipleInvalidRequirementsForClaims(final VerificationPlan vp) {
final EList<Claim> claims = vp.getClaim();
final Consumer<Claim> _function = (Claim it) -> {
EcoreUtil.resolveAll(it);
};
claims.forEach(_function);
final RequirementSet sysreqs = vp.getRequirementSet();
final EList<Requirement> sysreqsContent = sysreqs.getRequirements();
final String vpURI = EcoreUtil.getURI(vp).toString();
final Function1<Claim, Requirement> _function_1 = (Claim it) -> {
return it.getRequirement();
};
final Set<Requirement> claimsRequirements = IterableExtensions.<Requirement>toSet(ListExtensions.<Claim, Requirement>map(claims, _function_1));
final Function1<Requirement, Boolean> _function_2 = (Requirement it) -> {
boolean _contains = claimsRequirements.contains(it);
return Boolean.valueOf((!_contains));
};
final Iterable<Requirement> requirementsWithoutClaims = IterableExtensions.<Requirement>filter(sysreqsContent, _function_2);
int _size = IterableExtensions.size(requirementsWithoutClaims);
final boolean organizeClaims = (_size > 0);
final Function1<Claim, Boolean> _function_3 = (Claim it) -> {
Requirement _requirement = it.getRequirement();
return Boolean.valueOf((_requirement == null));
};
final Iterable<Claim> claimsMissingRequirements = IterableExtensions.<Claim>filter(claims, _function_3);
final ArrayList<String> missingReqURIs = new ArrayList<String>();
final Consumer<Requirement> _function_4 = (Requirement req) -> {
missingReqURIs.add(EcoreUtil.getURI(req).toString());
};
requirementsWithoutClaims.forEach(_function_4);
final Function1<Claim, Boolean> _function_5 = (Claim claim) -> {
boolean _and = false;
Requirement _requirement = null;
if (claim!=null) {
_requirement=claim.getRequirement();
}
boolean _tripleNotEquals = (_requirement != null);
if (!_tripleNotEquals) {
_and = false;
} else {
boolean _eIsProxy = claim.getRequirement().eIsProxy();
_and = _eIsProxy;
}
return Boolean.valueOf(_and);
};
final Iterable<Claim> claimsRequirementsUnresolved = IterableExtensions.<Claim>filter(claims, _function_5);
final ArrayList<Claim> claimsWithMissingReqs = new ArrayList<Claim>();
final Consumer<Claim> _function_6 = (Claim cl) -> {
if ((!organizeClaims)) {
this.error("Claim is missing requirement", cl, null, VerifyValidator.CLAIM_MISSING_REQUIREMENT, vpURI);
} else {
claimsWithMissingReqs.add(cl);
}
};
claimsMissingRequirements.forEach(_function_6);
final Consumer<Claim> _function_7 = (Claim cl) -> {
if ((!organizeClaims)) {
String _elvis = null;
String _name = cl.getRequirement().getName();
if (_name != null) {
_elvis = _name;
} else {
_elvis = "";
}
String reqName = _elvis;
int _length = reqName.length();
boolean _greaterThan = (_length > 0);
if (_greaterThan) {
reqName = (reqName + " ");
}
String _name_1 = sysreqs.getName();
String _plus = ((("Requirement " + reqName) + "does not exist in ") + _name_1);
String _plus_1 = (_plus + ".");
this.error(_plus_1, cl,
VerifyPackage.Literals.CLAIM__REQUIREMENT, VerifyValidator.CLAIM_INVALID_REQUIREMENT, vpURI);
} else {
claimsWithMissingReqs.add(cl);
}
};
claimsRequirementsUnresolved.forEach(_function_7);
int _size_1 = claimsWithMissingReqs.size();
boolean _greaterThan = (_size_1 > 0);
if (_greaterThan) {
final String[] uris = ((String[])Conversions.unwrapArray(missingReqURIs, String.class));
this.error("Claims with missing or unresolved Requirements", vp, VerifyPackage.Literals.VERIFICATION_PLAN__NAME,
VerifyValidator.MISSING_REQUIREMENTS_FOR_MULTIPLE_CLAIMS, uris);
}
}
@Check
public void checkClaimsForRequirement(final VerificationPlan vp) {
final RequirementSet systemRequirements = vp.getRequirementSet();
final EList<Requirement> requirements = systemRequirements.getRequirements();
final Consumer<Requirement> _function = (Requirement req) -> {
boolean _isEmpty = req.getRefinesReference().isEmpty();
if (_isEmpty) {
final Function1<Claim, Boolean> _function_1 = (Claim claim) -> {
Requirement _requirement = claim.getRequirement();
return Boolean.valueOf((_requirement == req));
};
boolean _exists = IterableExtensions.<Claim>exists(vp.getClaim(), _function_1);
boolean _not = (!_exists);
if (_not) {
String _name = req.getName();
String _plus = ("No claim for requirement " + _name);
this.warning(_plus, vp, VerifyPackage.Literals.VERIFICATION_PLAN__NAME,
VerifyValidator.MISSING_CLAIM_FOR_REQ, req.getName(), EcoreUtil.getURI(req).toString());
}
}
};
requirements.forEach(_function);
}
@Check
public void checkClaimsForMultipleRequirement(final VerificationPlan vp) {
final RequirementSet systemRequirements = vp.getRequirementSet();
final EList<Requirement> requirements = systemRequirements.getRequirements();
final List<String> missingRequirements = new ArrayList<String>();
final Consumer<Requirement> _function = (Requirement req) -> {
if ((req.getRefinesReference().isEmpty() && (!IterableExtensions.<Claim>exists(vp.getClaim(), ((Function1<Claim, Boolean>) (Claim claim) -> {
Requirement _requirement = claim.getRequirement();
return Boolean.valueOf((_requirement == req));
}))))) {
missingRequirements.add(EcoreUtil.getURI(req).toString());
}
};
requirements.forEach(_function);
int _size = missingRequirements.size();
boolean _greaterThan = (_size > 1);
if (_greaterThan) {
this.warning("Missing claims for multiple requirements", vp, VerifyPackage.Literals.VERIFICATION_PLAN__NAME,
VerifyValidator.MISSING_CLAIM_FOR_MULTIPLE_REQ, ((String[])Conversions.unwrapArray(missingRequirements, String.class)));
}
}
@Check
public void checkVerificationMethodSignature(final VerificationMethod vm) {
MethodKind _methodKind = vm.getMethodKind();
final MethodKind methodKind = _methodKind;
boolean _matched = false;
if (methodKind instanceof ResoluteMethod) {
_matched=true;
boolean _isResoluteInstalled = ResoluteUtil.isResoluteInstalled();
boolean _not = (!_isResoluteInstalled);
if (_not) {
return;
}
final EList<FormalParameter> fparams = vm.getFormals();
final EObject mreforproxy = ((ResoluteMethod)methodKind).getMethodReference();
if (((mreforproxy == null) || (!ResoluteUtil.getResolute().isFunctionDefinition(mreforproxy)))) {
return;
}
final NamedElement mref = ((NamedElement) mreforproxy);
final List<NamedElement> aparams = ResoluteUtil.getResolute().getArgs(mref);
final String methodRefName = mref.getName();
TargetType _targetType = vm.getTargetType();
final boolean hasComponentType = (_targetType != null);
int _xifexpression = (int) 0;
if (hasComponentType) {
int _size = fparams.size();
_xifexpression = (_size + 1);
} else {
_xifexpression = fparams.size();
}
final int fcount = _xifexpression;
int _size_1 = aparams.size();
boolean _notEquals = (fcount != _size_1);
if (_notEquals) {
String _name = vm.getName();
String _plus = ("method " + _name);
String _plus_1 = (_plus +
"\'s number of parameters does not match the number of arguments for the Resolute method ");
String _plus_2 = (_plus_1 + methodRefName);
this.warning(_plus_2, vm, VerifyPackage.Literals.VERIFICATION_METHOD__NAME,
VerifyValidator.METHOD_PARMS_DO_NOT_MATCH_RESOLUTE_DEFINITION);
return;
}
int _xifexpression_1 = (int) 0;
if (hasComponentType) {
_xifexpression_1 = 1;
} else {
_xifexpression_1 = 0;
}
final int i = _xifexpression_1;
final Procedure2<FormalParameter, Integer> _function = (FormalParameter vmParm, Integer j) -> {
final NamedElement aparam = aparams.get(((j).intValue() + i));
final EObject baseType = ResoluteUtil.getResolute().getType(aparam);
boolean _matchResoluteType = this.matchResoluteType(vmParm.getType(), baseType);
boolean _not_1 = (!_matchResoluteType);
if (_not_1) {
String _name_1 = vm.getName();
String _plus_3 = ("method " + _name_1);
String _plus_4 = (_plus_3 + "\'s parameter ");
String _name_2 = vmParm.getName();
String _plus_5 = (_plus_4 + _name_2);
String _plus_6 = (_plus_5 + " does not match the type of ");
String _name_3 = aparam.getName();
String _plus_7 = (_plus_6 + _name_3);
String _plus_8 = (_plus_7 + " in the Resolute method ");
String _plus_9 = (_plus_8 + methodRefName);
this.warning(_plus_9, vm,
VerifyPackage.Literals.VERIFICATION_METHOD__NAME,
VerifyValidator.METHOD_PARMS_DO_NOT_MATCH_RESOLUTE_DEFINITION);
return;
}
};
IterableExtensions.<FormalParameter>forEach(fparams, _function);
}
}
/**
* @since 5.0
*/
public boolean matchResoluteType(final PropertyType formalType, final EObject resoluteType) {
boolean _xblockexpression = false;
{
boolean _isBaseType = ResoluteUtil.getResolute().isBaseType(resoluteType);
if (_isBaseType) {
boolean _matched = false;
if (formalType instanceof AadlBoolean) {
_matched=true;
return ResoluteUtil.getResolute().getTypeName(resoluteType).equalsIgnoreCase("bool");
}
if (!_matched) {
if (formalType instanceof AadlReal) {
_matched=true;
return ResoluteUtil.getResolute().getTypeName(resoluteType).equalsIgnoreCase("real");
}
}
if (!_matched) {
if (formalType instanceof AadlInteger) {
_matched=true;
return ResoluteUtil.getResolute().getTypeName(resoluteType).equalsIgnoreCase("int");
}
}
if (!_matched) {
if (formalType instanceof AadlString) {
_matched=true;
return ResoluteUtil.getResolute().getTypeName(resoluteType).equalsIgnoreCase("string");
}
}
if (!_matched) {
if (formalType instanceof PropertyRef) {
_matched=true;
final Property prop = ((PropertyRef)formalType).getRef();
PropertyType _elvis = null;
PropertyType _referencedPropertyType = null;
if (prop!=null) {
_referencedPropertyType=prop.getReferencedPropertyType();
}
if (_referencedPropertyType != null) {
_elvis = _referencedPropertyType;
} else {
PropertyType _ownedPropertyType = prop.getOwnedPropertyType();
_elvis = _ownedPropertyType;
}
final PropertyType propType = _elvis;
boolean _matched_1 = false;
if (propType instanceof ReferenceType) {
_matched_1=true;
return this.matchReferenceType(((ReferenceType)propType), resoluteType);
}
return this.matchResoluteType(propType, resoluteType);
}
}
if (!_matched) {
if (formalType instanceof ModelRef) {
_matched=true;
return ResoluteUtil.getResolute().getTypeName(resoluteType).equalsIgnoreCase("aadl");
}
}
if (!_matched) {
if (formalType instanceof TypeRef) {
_matched=true;
final PropertyType propType = ((TypeRef)formalType).getRef();
boolean _matched_1 = false;
if (propType instanceof ReferenceType) {
_matched_1=true;
return this.matchReferenceType(((ReferenceType)propType), resoluteType);
}
return this.matchResoluteType(propType, resoluteType);
}
}
}
_xblockexpression = false;
}
return _xblockexpression;
}
/**
* @since 5.0
*/
public boolean matchReferenceType(final ReferenceType propType, final EObject resoluteType) {
boolean _xblockexpression = false;
{
boolean _isBaseType = ResoluteUtil.getResolute().isBaseType(resoluteType);
if (_isBaseType) {
boolean _equalsIgnoreCase = ResoluteUtil.getResolute().getTypeName(resoluteType).equalsIgnoreCase("aadl");
if (_equalsIgnoreCase) {
return true;
}
final MetaclassReference metaclassreference = Aadl2Factory.eINSTANCE.createMetaclassReference();
metaclassreference.getMetaclassNames().add(ResoluteUtil.getResolute().getTypeName(resoluteType));
final EClass refEclass = metaclassreference.getMetaclass();
EList<MetaclassReference> _namedElementReferences = propType.getNamedElementReferences();
for (final MetaclassReference mcri : _namedElementReferences) {
boolean _isSuperTypeOf = refEclass.isSuperTypeOf(mcri.getMetaclass());
if (_isSuperTypeOf) {
return true;
}
}
}
_xblockexpression = false;
}
return _xblockexpression;
}
@Check
public void checkFileTypeContents(final Verification verification) {
final URI verificationURI = EcoreUtil.getURI(verification);
final String fileExt = verificationURI.fileExtension().toLowerCase();
final EList<EObject> contents = verification.getContents();
if (fileExt != null) {
switch (fileExt) {
case "verify":
final Consumer<EObject> _function = (EObject content) -> {
boolean _matched = false;
if (content instanceof VerificationPlan) {
_matched=true;
}
if (!_matched) {
if (content instanceof VerificationMethodRegistry) {
_matched=true;
this.fileTypeError(fileExt, "verification methods", content);
}
}
if (!_matched) {
this.fileTypeError(fileExt, content.getClass().getName(), content);
}
};
contents.forEach(_function);
break;
case "methodregistry":
final Consumer<EObject> _function_1 = (EObject content) -> {
boolean _matched = false;
if (content instanceof VerificationMethodRegistry) {
_matched=true;
}
if (!_matched) {
if (content instanceof VerificationPlan) {
_matched=true;
this.fileTypeError(fileExt, "verification plan", content);
}
}
if (!_matched) {
this.fileTypeError(fileExt, content.getClass().getName(), content);
}
};
contents.forEach(_function_1);
break;
default:
break;
}
} else {
}
}
public void fileTypeError(final String fileType, final String partName, final EObject part) {
this.warning((((partName + " not allowed in \'") + fileType) + "\' file."), part, null);
}
@Check
public void checkVerificationPlanUniqueToComponentClassifier(final VerificationPlan vp) {
final RequirementSet sysReq = vp.getRequirementSet();
if ((sysReq instanceof SystemRequirementSet)) {
final Iterable<VerificationPlan> vps = this.verifyGlobalRefFinder.getAllVerificationPlansForRequirements(sysReq, vp);
int _size = IterableExtensions.size(vps);
boolean _greaterThan = (_size > 1);
if (_greaterThan) {
String _name = ((SystemRequirementSet)sysReq).getName();
String _plus = ("Other Verification Plans exist for \'" + _name);
String _plus_1 = (_plus +
"\'. Only one Verification Plans is allowed for a specific System Requirements.");
this.error(_plus_1, vp,
VerifyPackage.Literals.VERIFICATION_PLAN__REQUIREMENT_SET);
}
}
}
}