AssureConstructor.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.assure.generator;
import com.google.common.collect.Iterables;
import com.google.inject.Inject;
import java.util.Collections;
import java.util.List;
import org.eclipse.emf.common.util.BasicEList;
import org.eclipse.emf.common.util.EList;
import org.eclipse.emf.common.util.UniqueEList;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.xtext.xbase.lib.Conversions;
import org.eclipse.xtext.xbase.lib.Extension;
import org.eclipse.xtext.xbase.lib.Functions.Function1;
import org.eclipse.xtext.xbase.lib.IterableExtensions;
import org.osate.aadl2.ComponentCategory;
import org.osate.aadl2.ComponentClassifier;
import org.osate.aadl2.ComponentImplementation;
import org.osate.aadl2.ComponentType;
import org.osate.aadl2.Connection;
import org.osate.aadl2.EndToEndFlow;
import org.osate.aadl2.Feature;
import org.osate.aadl2.NamedElement;
import org.osate.aadl2.Subcomponent;
import org.osate.aadl2.util.Aadl2Util;
import org.osate.alisa.common.common.TargetType;
import org.osate.alisa.common.util.CommonUtilExtension;
import org.osate.alisa.workbench.alisa.AssuranceCase;
import org.osate.alisa.workbench.alisa.AssurancePlan;
import org.osate.alisa.workbench.util.IAlisaGlobalReferenceFinder;
import org.osate.assure.assure.AssuranceCaseResult;
import org.osate.assure.assure.AssureFactory;
import org.osate.assure.assure.ClaimResult;
import org.osate.assure.assure.ElseResult;
import org.osate.assure.assure.Metrics;
import org.osate.assure.assure.ModelResult;
import org.osate.assure.assure.NestedClaimReference;
import org.osate.assure.assure.PreconditionResult;
import org.osate.assure.assure.PredicateResult;
import org.osate.assure.assure.QualifiedClaimReference;
import org.osate.assure.assure.QualifiedVAReference;
import org.osate.assure.assure.SubsystemResult;
import org.osate.assure.assure.ThenResult;
import org.osate.assure.assure.ValidationResult;
import org.osate.assure.assure.VerificationActivityResult;
import org.osate.assure.assure.VerificationExpr;
import org.osate.assure.assure.VerificationResult;
import org.osate.assure.util.AssureUtilExtension;
import org.osate.pluginsupport.ExecuteJavaUtil;
import org.osate.reqspec.reqSpec.IncludeGlobalRequirement;
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.reqspec.reqSpec.WhenCondition;
import org.osate.reqspec.util.IReqspecGlobalReferenceFinder;
import org.osate.reqspec.util.ReqSpecUtilExtension;
import org.osate.result.ResultType;
import org.osate.verify.internal.util.IVerifyGlobalReferenceFinder;
import org.osate.verify.internal.util.VerifyUtilExtension;
import org.osate.verify.verify.AllExpr;
import org.osate.verify.verify.ArgumentExpr;
import org.osate.verify.verify.Claim;
import org.osate.verify.verify.ElseExpr;
import org.osate.verify.verify.RefExpr;
import org.osate.verify.verify.ThenExpr;
import org.osate.verify.verify.VerificationActivity;
import org.osate.verify.verify.VerificationCondition;
import org.osate.verify.verify.VerificationMethod;
import org.osate.verify.verify.VerificationPlan;
import org.osate.verify.verify.VerificationPrecondition;
import org.osate.verify.verify.VerificationValidation;
/**
* Generates code from your model files on save.
*
* see http://www.eclipse.org/Xtext/documentation.html#TutorialCodeGeneration
*/
@SuppressWarnings("all")
public class AssureConstructor implements IAssureConstructor {
private final AssureFactory factory = AssureFactory.eINSTANCE;
private EList<VerificationPlan> globalPlans;
private EList<Claim> globalClaims;
private boolean isRoot = true;
@Override
public AssuranceCaseResult generateFullAssuranceCase(final AssuranceCase acs) {
AssuranceCaseResult _xblockexpression = null;
{
UniqueEList<VerificationPlan> _uniqueEList = new UniqueEList<VerificationPlan>();
this.globalPlans = _uniqueEList;
UniqueEList<Claim> _uniqueEList_1 = new UniqueEList<Claim>();
this.globalClaims = _uniqueEList_1;
this.isRoot = true;
_xblockexpression = this.constructAssuranceCaseResult(acs, null);
}
return _xblockexpression;
}
public AssuranceCaseResult constructAssuranceCaseResult(final AssuranceCase acs, final ComponentClassifier cl) {
AssuranceCaseResult _xblockexpression = null;
{
AssuranceCaseResult acr = this.factory.createAssuranceCaseResult();
acr.setName(acs.getName());
acr.setMetrics(this.factory.createMetrics());
Metrics _metrics = acr.getMetrics();
_metrics.setTbdCount(0);
final EList<ModelResult> mrs = acr.getModelResult();
EList<AssurancePlan> _assurancePlans = acs.getAssurancePlans();
for (final AssurancePlan acp : _assurancePlans) {
if ((CommonUtilExtension.isSameorExtends(acp.getTarget(), acs.getSystem()) && ((cl == null) || CommonUtilExtension.isSameorExtends(cl, acp.getTarget())))) {
final ModelResult modelResultInstance = this.constructModelResult(acp);
if ((modelResultInstance != null)) {
mrs.add(modelResultInstance);
}
}
}
_xblockexpression = acr;
}
return _xblockexpression;
}
public ModelResult constructModelResult(final AssurancePlan acp) {
ModelResult _xblockexpression = null;
{
Iterable<VerificationPlan> myplans = Collections.EMPTY_LIST;
ComponentClassifier cc = null;
if ((acp != null)) {
myplans = acp.getAssure();
cc = acp.getTarget();
if ((IterableExtensions.isEmpty(myplans) && (!Aadl2Util.isNull(cc)))) {
myplans = this.vReferenceFinder.getVerificationPlans(cc, acp);
}
this.globalPlans.addAll(acp.getAssureGlobal());
}
ModelResult mr = this.factory.createModelResult();
mr.setPlan(acp);
mr.setTarget(acp.getTarget());
mr.setMetrics(this.factory.createMetrics());
Metrics _metrics = mr.getMetrics();
_metrics.setTbdCount(0);
this.doAssurancePlanClaimResultsParts(acp, myplans, cc, mr.getClaimResult(), mr.getSubsystemResult(), mr.getSubAssuranceCase(),
false);
if (((((Object[])Conversions.unwrapArray(mr.getClaimResult(), Object.class)).length == 0) && (((Object[])Conversions.unwrapArray(mr.getSubsystemResult(), Object.class)).length == 0))) {
return null;
}
_xblockexpression = mr;
}
return _xblockexpression;
}
public void doAssurancePlanClaimResultsParts(final AssurancePlan assurancePlan, final Iterable<VerificationPlan> vplans, final ComponentClassifier cc, final EList<ClaimResult> claimResultList, final EList<SubsystemResult> subsystemResultList, final EList<AssuranceCaseResult> subAssuranceCaseList, final boolean globalOnly) {
final int globalPlansTop = this.globalPlans.size();
final int globalClaimsTop = this.globalClaims.size();
final Iterable<SystemRequirementSet> sysreqs = this.rRreferenceFinder.getSystemRequirementSets(cc);
for (final VerificationPlan vplan : vplans) {
EList<Claim> _claim = vplan.getClaim();
for (final Claim claim : _claim) {
this.generateClaimResult(claim, claimResultList);
}
}
for (final SystemRequirementSet reqs : sysreqs) {
{
final EList<IncludeGlobalRequirement> includes = reqs.getInclude();
for (final IncludeGlobalRequirement incl : includes) {
EObject _include = incl.getInclude();
if ((_include instanceof RequirementSet)) {
EObject _include_1 = incl.getInclude();
final Iterable<VerificationPlan> plans = this.vReferenceFinder.getAllVerificationPlansForRequirements(((RequirementSet) _include_1), reqs);
boolean _isLocal = incl.isLocal();
if (_isLocal) {
for (final VerificationPlan vplan_1 : plans) {
final Function1<Claim, Boolean> _function = (Claim cl) -> {
Requirement _requirement = cl.getRequirement();
EList<ComponentCategory> _componentCategory = null;
if (_requirement!=null) {
_componentCategory=_requirement.getComponentCategory();
}
return Boolean.valueOf(ReqSpecUtilExtension.matchingCategory(_componentCategory, cc.getCategory()));
};
Iterable<Claim> _filter = IterableExtensions.<Claim>filter(vplan_1.getClaim(), _function);
for (final Claim claim_1 : _filter) {
this.generateAllClaimResult(claim_1, cc, claimResultList);
}
}
} else {
Iterables.<VerificationPlan>addAll(this.globalPlans, plans);
}
} else {
EObject _include_2 = incl.getInclude();
if ((_include_2 instanceof Requirement)) {
EObject _include_3 = incl.getInclude();
final Requirement greq = ((Requirement) _include_3);
final RequirementSet greqs = ReqSpecUtilExtension.containingRequirementSet(greq);
final Iterable<VerificationPlan> plans_1 = this.vReferenceFinder.getAllVerificationPlansForRequirements(greqs, reqs);
for (final VerificationPlan vp : plans_1) {
EList<Claim> _claim_1 = vp.getClaim();
for (final Claim claim_2 : _claim_1) {
boolean _equals = claim_2.getRequirement().getName().equals(greq.getName());
if (_equals) {
Requirement _requirement = claim_2.getRequirement();
EList<ComponentCategory> _componentCategory = null;
if (_requirement!=null) {
_componentCategory=_requirement.getComponentCategory();
}
boolean _matchingCategory = ReqSpecUtilExtension.matchingCategory(_componentCategory, cc.getCategory());
if (_matchingCategory) {
boolean _isLocal_1 = incl.isLocal();
if (_isLocal_1) {
this.generateAllClaimResult(claim_2, cc, claimResultList);
} else {
NamedElement _targetElement = incl.getTargetElement();
boolean _tripleNotEquals = (_targetElement != null);
if (_tripleNotEquals) {
boolean _whenHolds = this.whenHolds(claim_2, cc);
if (_whenHolds) {
this.generateClaimResult(claim_2, claimResultList, incl.getTargetElement());
}
} else {
this.globalClaims.add(claim_2);
}
}
}
}
}
}
}
}
}
}
}
for (final VerificationPlan vplan_1 : this.globalPlans) {
final Function1<Claim, Boolean> _function = (Claim cl) -> {
Requirement _requirement = cl.getRequirement();
EList<ComponentCategory> _componentCategory = null;
if (_requirement!=null) {
_componentCategory=_requirement.getComponentCategory();
}
return Boolean.valueOf(ReqSpecUtilExtension.matchingCategory(_componentCategory, cc.getCategory()));
};
Iterable<Claim> _filter = IterableExtensions.<Claim>filter(vplan_1.getClaim(), _function);
for (final Claim claim_1 : _filter) {
this.generateAllClaimResult(claim_1, cc, claimResultList);
}
}
final Function1<Claim, Boolean> _function_1 = (Claim cl) -> {
Requirement _requirement = cl.getRequirement();
EList<ComponentCategory> _componentCategory = null;
if (_requirement!=null) {
_componentCategory=_requirement.getComponentCategory();
}
return Boolean.valueOf(ReqSpecUtilExtension.matchingCategory(_componentCategory, cc.getCategory()));
};
Iterable<Claim> _filter_1 = IterableExtensions.<Claim>filter(this.globalClaims, _function_1);
for (final Claim claim_2 : _filter_1) {
this.generateAllClaimResult(claim_2, cc, claimResultList);
}
if ((cc instanceof ComponentImplementation)) {
EList<Subcomponent> _allSubcomponents = ((ComponentImplementation)cc).getAllSubcomponents();
for (final Subcomponent subc : _allSubcomponents) {
this.generateSubsystemPlans(subc, assurancePlan, subsystemResultList, subAssuranceCaseList, globalOnly);
}
}
int plansize = this.globalPlans.size();
while ((plansize > globalPlansTop)) {
{
this.globalPlans.remove((plansize - 1));
plansize = (plansize - 1);
}
}
int claimsize = this.globalClaims.size();
while ((claimsize > globalClaimsTop)) {
{
this.globalClaims.remove((claimsize - 1));
claimsize = (claimsize - 1);
}
}
}
public boolean whenHolds(final Claim claim, final ComponentClassifier cc) {
boolean _xblockexpression = false;
{
final Requirement req = claim.getRequirement();
final WhenCondition when = req.getWhencondition();
if ((when != null)) {
final String function = when.getCondition();
if ((function != null)) {
NamedElement _elvis = null;
NamedElement _targetElement = req.getTargetElement();
if (_targetElement != null) {
_elvis = _targetElement;
} else {
_elvis = cc;
}
final NamedElement ne = _elvis;
final Object res = ExecuteJavaUtil.invokeJavaMethod(function, ne);
if ((res instanceof Boolean)) {
return ((Boolean) res).booleanValue();
}
}
}
_xblockexpression = true;
}
return _xblockexpression;
}
public void generateAllClaimResult(final Claim claim, final ComponentClassifier cc, final EList<ClaimResult> claimResultlist) {
boolean _whenHolds = this.whenHolds(claim, cc);
boolean _not = (!_whenHolds);
if (_not) {
return;
}
TargetType _targetType = claim.getRequirement().getTargetType();
boolean _tripleEquals = (_targetType == TargetType.CONNECTION);
if (_tripleEquals) {
if ((cc instanceof ComponentImplementation)) {
Iterable<Connection> _crossConnections = CommonUtilExtension.getCrossConnections(((ComponentImplementation)cc));
for (final Connection conn : _crossConnections) {
this.generateClaimResult(claim, claimResultlist, conn);
}
}
return;
} else {
TargetType _targetType_1 = claim.getRequirement().getTargetType();
boolean _tripleEquals_1 = (_targetType_1 == TargetType.FLOW);
if (_tripleEquals_1) {
if ((cc instanceof ComponentImplementation)) {
EList<EndToEndFlow> _allEndToEndFlows = ((ComponentImplementation)cc).getAllEndToEndFlows();
for (final EndToEndFlow etef : _allEndToEndFlows) {
this.generateClaimResult(claim, claimResultlist, etef);
}
}
return;
} else {
TargetType _targetType_2 = claim.getRequirement().getTargetType();
boolean _tripleEquals_2 = (_targetType_2 == TargetType.FEATURE);
if (_tripleEquals_2) {
EList<Feature> _allFeatures = cc.getAllFeatures();
for (final Feature feature : _allFeatures) {
this.generateClaimResult(claim, claimResultlist, feature);
}
return;
} else {
this.generateClaimResult(claim, claimResultlist);
}
}
}
}
public void generateClaimResult(final Claim claim, final EList<ClaimResult> claimResultlist) {
this.generateClaimResult(claim, claimResultlist, claim.getRequirement().getTargetElement());
}
public void generateClaimResult(final Claim claim, final EList<ClaimResult> claimResultlist, final NamedElement forTargetElement) {
final EList<VerificationActivityResult> claimvas = this.doGenerateVA(claim);
if ((((((Object[])Conversions.unwrapArray(claimvas, Object.class)).length == 0) && (claim.getSubclaim() == null)) && (claim.getAssert() == null))) {
return;
}
final ClaimResult claimResult = this.factory.createClaimResult();
final QualifiedClaimReference qcr = this.factory.createQualifiedClaimReference();
qcr.setVerificationPlan(VerifyUtilExtension.containingVerificationPlan(claim));
final NestedClaimReference ncr = this.factory.createNestedClaimReference();
ncr.setRequirement(claim.getRequirement());
qcr.setRequirement(this.constructClaimReferencePath(claim, ncr));
claimResult.setTargetReference(qcr);
claimResult.setMetrics(this.factory.createMetrics());
Metrics _metrics = claimResult.getMetrics();
_metrics.setTbdCount(0);
claimResult.setModelElement(forTargetElement);
EList<Claim> _subclaim = claim.getSubclaim();
boolean _tripleNotEquals = (_subclaim != null);
if (_tripleNotEquals) {
EList<Claim> _subclaim_1 = null;
if (claim!=null) {
_subclaim_1=claim.getSubclaim();
}
for (final Claim subclaim : _subclaim_1) {
this.generateClaimResult(subclaim, claimResult.getSubClaimResult(), claim.getRequirement().getTargetElement());
}
}
ArgumentExpr _assert = claim.getAssert();
boolean _tripleNotEquals_1 = (_assert != null);
if (_tripleNotEquals_1) {
this.construct(claimResult.getVerificationActivityResult(), claim.getAssert());
} else {
for (final VerificationActivityResult claimva : claimvas) {
claimResult.getVerificationActivityResult().add(claimva);
}
}
final ReqPredicate predicate = claim.getRequirement().getPredicate();
if ((predicate instanceof ValuePredicate)) {
boolean _containsComputeVariables = AssureUtilExtension.containsComputeVariables(((ValuePredicate)predicate));
boolean _not = (!_containsComputeVariables);
if (_not) {
claimResult.setPredicateResult(this.generatePredicateResult(claim));
}
}
claimResultlist.add(claimResult);
}
public PredicateResult generatePredicateResult(final Claim claim) {
PredicateResult _xblockexpression = null;
{
final PredicateResult predicate = this.factory.createPredicateResult();
final QualifiedClaimReference ref = this.factory.createQualifiedClaimReference();
ref.setVerificationPlan(VerifyUtilExtension.containingVerificationPlan(claim));
final NestedClaimReference nested = this.factory.createNestedClaimReference();
nested.setRequirement(claim.getRequirement());
ref.setRequirement(this.constructClaimReferencePath(claim, nested));
predicate.setTargetReference(ref);
predicate.setMetrics(this.factory.createMetrics());
Metrics _metrics = predicate.getMetrics();
_metrics.setTbdCount(0);
_xblockexpression = predicate;
}
return _xblockexpression;
}
@Inject
private IAlisaGlobalReferenceFinder arefFinder;
public void generateSubsystemPlans(final Subcomponent subc, final AssurancePlan parentap, final EList<SubsystemResult> subsystemResultList, final EList<AssuranceCaseResult> subAssuranceCaseList, final boolean globalOnly) {
final ComponentClassifier cc = subc.getAllClassifier();
if ((cc == null)) {
return;
}
final boolean prevIsRoot = this.isRoot;
this.isRoot = false;
if ((globalOnly || this.isAssumeSubsystem(subc, parentap))) {
this.generateSubsystemGlobalOnly(subc, parentap, subsystemResultList);
} else {
if ((cc instanceof ComponentType)) {
this.generateSubsystemVerificationPlansGlobals(subc, parentap, subsystemResultList);
} else {
final Iterable<AssuranceCase> subacs = this.arefFinder.getAssuranceCases(cc);
boolean _isEmpty = IterableExtensions.isEmpty(subacs);
if (_isEmpty) {
this.generateSubsystemVerificationPlansGlobals(subc, parentap, subsystemResultList);
} else {
for (final AssuranceCase subac : subacs) {
subAssuranceCaseList.add(this.constructAssuranceCaseResult(subac, cc));
}
}
}
}
this.isRoot = prevIsRoot;
}
/**
* sub: system of interest as subcomponent of another system
*/
public void generateSubsystemVerificationPlansGlobals(final Subcomponent sub, final AssurancePlan mp, final EList<SubsystemResult> subsystemResultList) {
Iterable<VerificationPlan> myplans = Collections.EMPTY_LIST;
ComponentClassifier cc = null;
boolean _isNull = Aadl2Util.isNull(sub);
boolean _not = (!_isNull);
if (_not) {
cc = sub.getAllClassifier();
boolean _isNull_1 = Aadl2Util.isNull(cc);
boolean _not_1 = (!_isNull_1);
if (_not_1) {
myplans = this.vReferenceFinder.getVerificationPlans(cc, mp);
}
}
final SubsystemResult ssr = this.factory.createSubsystemResult();
ssr.setTargetSystem(sub);
ssr.setMetrics(this.factory.createMetrics());
Metrics _metrics = ssr.getMetrics();
_metrics.setTbdCount(0);
this.doAssurancePlanClaimResultsParts(mp, myplans, cc, ssr.getClaimResult(), ssr.getSubsystemResult(), null, false);
subsystemResultList.add(ssr);
}
/**
* sub: system of interest as subcomponent of another system only for global requirements from enclosing case
* Otherwiase it was marked as assume, i.e., local assurance case/verification plans are not executed
*/
public void generateSubsystemGlobalOnly(final Subcomponent sub, final AssurancePlan mp, final EList<SubsystemResult> subsystemResultList) {
Iterable<VerificationPlan> myplans = Collections.EMPTY_LIST;
final SubsystemResult ssr = this.factory.createSubsystemResult();
ssr.setTargetSystem(sub);
ssr.setMetrics(this.factory.createMetrics());
Metrics _metrics = ssr.getMetrics();
_metrics.setTbdCount(0);
this.doAssurancePlanClaimResultsParts(mp, myplans, sub.getAllClassifier(), ssr.getClaimResult(), ssr.getSubsystemResult(), null,
true);
subsystemResultList.add(ssr);
}
public boolean isAssumeSubsystem(final Subcomponent subc, final AssurancePlan parentacp) {
if ((parentacp == null)) {
return false;
}
boolean _isAssumeAll = parentacp.isAssumeAll();
if (_isAssumeAll) {
return true;
}
final EList<Subcomponent> assumes = parentacp.getAssumeSubsystems();
for (final Subcomponent sub : assumes) {
boolean _equalsIgnoreCase = sub.getName().equalsIgnoreCase(subc.getName());
if (_equalsIgnoreCase) {
return true;
}
}
return false;
}
public EList<VerificationActivityResult> doGenerateVA(final Claim claim) {
EList<VerificationActivityResult> _xblockexpression = null;
{
final EList<VerificationActivityResult> returnList = new BasicEList<VerificationActivityResult>();
EList<VerificationActivity> _activities = claim.getActivities();
for (final VerificationActivity va : _activities) {
this.addVAR(va, returnList);
}
_xblockexpression = returnList;
}
return _xblockexpression;
}
public void addVAR(final VerificationActivity va, final EList<VerificationActivityResult> vaList) {
final Claim claim = VerifyUtilExtension.getContainingClaim(va);
if (((va.getMethod().getTargetType() == TargetType.ROOT) && (!this.isRoot))) {
return;
}
final VerificationActivityResult vaResult = this.factory.createVerificationActivityResult();
final QualifiedVAReference qvr = this.factory.createQualifiedVAReference();
qvr.setVerificationPlan(VerifyUtilExtension.containingVerificationPlan(va));
final NestedClaimReference ncr = this.factory.createNestedClaimReference();
ncr.setRequirement(claim.getRequirement());
qvr.setRequirement(this.constructClaimReferencePath(claim, ncr));
qvr.setVerificationActivity(va);
vaResult.setTargetReference(qvr);
vaResult.setType(ResultType.TBD);
vaResult.setMetrics(this.factory.createMetrics());
Metrics _metrics = vaResult.getMetrics();
_metrics.setTbdCount(0);
VerificationMethod _method = va.getMethod();
VerificationCondition _precondition = null;
if (_method!=null) {
_precondition=_method.getPrecondition();
}
boolean _tripleNotEquals = (_precondition != null);
if (_tripleNotEquals) {
vaResult.setPreconditionResult(this.doConstruct(va.getMethod().getPrecondition(), va));
}
VerificationMethod _method_1 = va.getMethod();
VerificationCondition _validation = null;
if (_method_1!=null) {
_validation=_method_1.getValidation();
}
boolean _tripleNotEquals_1 = (_validation != null);
if (_tripleNotEquals_1) {
vaResult.setValidationResult(this.doConstruct(va.getMethod().getValidation(), va));
}
vaList.add(vaResult);
}
public NestedClaimReference constructClaimReferencePath(final Claim claim, final NestedClaimReference ncr) {
final EObject parent = claim.eContainer();
if ((parent instanceof Claim)) {
final NestedClaimReference parentNcr = this.factory.createNestedClaimReference();
parentNcr.setRequirement(((Claim)parent).getRequirement());
parentNcr.setSub(ncr);
return this.constructClaimReferencePath(((Claim)parent), parentNcr);
}
return ncr;
}
@Inject
@Extension
private IReqspecGlobalReferenceFinder rRreferenceFinder;
@Inject
@Extension
private IVerifyGlobalReferenceFinder vReferenceFinder;
public void construct(final List<VerificationExpr> arl, final ArgumentExpr expr) {
boolean _matched = false;
if (expr instanceof AllExpr) {
_matched=true;
this.doConstruct(arl, ((AllExpr)expr));
}
if (!_matched) {
if (expr instanceof ThenExpr) {
_matched=true;
this.doConstruct(arl, ((ThenExpr)expr));
}
}
if (!_matched) {
if (expr instanceof ElseExpr) {
_matched=true;
this.doConstruct(arl, ((ElseExpr)expr));
}
}
if (!_matched) {
if (expr instanceof RefExpr) {
_matched=true;
this.doConstruct(arl, ((RefExpr)expr));
}
}
}
public void doConstruct(final List<VerificationExpr> arl, final AllExpr expr) {
EList<ArgumentExpr> _elements = expr.getElements();
for (final ArgumentExpr subexpr : _elements) {
this.construct(arl, subexpr);
}
}
public void doConstruct(final List<VerificationExpr> arl, final ThenExpr expr) {
final ThenResult thenres = this.factory.createThenResult();
thenres.setMetrics(this.factory.createMetrics());
Metrics _metrics = thenres.getMetrics();
_metrics.setTbdCount(0);
this.construct(thenres.getFirst(), expr.getLeft());
this.construct(thenres.getSecond(), expr.getSuccessor());
boolean _isEmpty = thenres.getFirst().isEmpty();
if (_isEmpty) {
return;
}
boolean _isEmpty_1 = thenres.getSecond().isEmpty();
if (_isEmpty_1) {
EList<VerificationExpr> _first = thenres.getFirst();
Iterables.<VerificationExpr>addAll(arl, _first);
} else {
arl.add(thenres);
}
}
public void doConstruct(final List<VerificationExpr> arl, final ElseExpr expr) {
final ElseResult elseres = this.factory.createElseResult();
elseres.setMetrics(this.factory.createMetrics());
Metrics _metrics = elseres.getMetrics();
_metrics.setTbdCount(0);
this.construct(elseres.getFirst(), expr.getLeft());
this.construct(elseres.getError(), expr.getError());
ArgumentExpr _fail = expr.getFail();
boolean _tripleNotEquals = (_fail != null);
if (_tripleNotEquals) {
this.construct(elseres.getFail(), expr.getFail());
}
ArgumentExpr _timeout = expr.getTimeout();
boolean _tripleNotEquals_1 = (_timeout != null);
if (_tripleNotEquals_1) {
this.construct(elseres.getTimeout(), expr.getTimeout());
}
boolean _isEmpty = elseres.getFirst().isEmpty();
if (_isEmpty) {
return;
}
if (((elseres.getError().isEmpty() && elseres.getFail().isEmpty()) && elseres.getTimeout().isEmpty())) {
EList<VerificationExpr> _first = elseres.getFirst();
Iterables.<VerificationExpr>addAll(arl, _first);
} else {
arl.add(elseres);
}
}
public void doConstruct(final List<VerificationExpr> arl, final RefExpr expr) {
final VerificationActivity va = expr.getVerification();
if ((va == null)) {
return;
}
final VerificationActivityResult vr = this.factory.createVerificationActivityResult();
vr.setType(ResultType.TBD);
final QualifiedVAReference qvr = this.factory.createQualifiedVAReference();
qvr.setVerificationPlan(VerifyUtilExtension.containingVerificationPlan(va));
final NestedClaimReference ncr = this.factory.createNestedClaimReference();
final Claim claim = VerifyUtilExtension.getContainingClaim(va);
ncr.setRequirement(claim.getRequirement());
qvr.setRequirement(this.constructClaimReferencePath(claim, ncr));
qvr.setVerificationActivity(va);
vr.setTargetReference(qvr);
vr.setMetrics(this.factory.createMetrics());
Metrics _metrics = vr.getMetrics();
_metrics.setTbdCount(0);
arl.add(vr);
VerificationMethod _method = va.getMethod();
VerificationCondition _precondition = null;
if (_method!=null) {
_precondition=_method.getPrecondition();
}
boolean _tripleNotEquals = (_precondition != null);
if (_tripleNotEquals) {
vr.setPreconditionResult(this.doConstruct(va.getMethod().getPrecondition(), va));
}
VerificationMethod _method_1 = va.getMethod();
VerificationCondition _validation = null;
if (_method_1!=null) {
_validation=_method_1.getValidation();
}
boolean _tripleNotEquals_1 = (_validation != null);
if (_tripleNotEquals_1) {
vr.setValidationResult(this.doConstruct(va.getMethod().getValidation(), va));
}
}
public VerificationResult doConstruct(final VerificationCondition vc, final VerificationActivity va) {
VerificationResult vcr = null;
boolean _matched = false;
if (vc instanceof VerificationValidation) {
_matched=true;
vcr = this.factory.createValidationResult();
((ValidationResult) vcr).setTarget(va.getMethod());
}
if (!_matched) {
if (vc instanceof VerificationPrecondition) {
_matched=true;
vcr = this.factory.createPreconditionResult();
((PreconditionResult) vcr).setTarget(va.getMethod());
}
}
vcr.setType(ResultType.TBD);
vcr.setMetrics(this.factory.createMetrics());
Metrics _metrics = vcr.getMetrics();
_metrics.setTbdCount(0);
return vcr;
}
}