VerifyUtilExtension.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.internal.util;

import com.google.common.collect.HashMultimap;
import java.util.HashMap;
import java.util.Set;
import org.eclipse.emf.common.util.URI;
import org.eclipse.emf.ecore.EObject;
import org.eclipse.emf.ecore.util.EcoreUtil;
import org.eclipse.xtext.EcoreUtil2;
import org.osate.aadl2.ComponentClassifier;
import org.osate.aadl2.util.Aadl2Util;
import org.osate.categories.categories.CategoryFilter;
import org.osate.categories.util.CategoriesUtil;
import org.osate.reqspec.reqSpec.Requirement;
import org.osate.reqspec.reqSpec.RequirementSet;
import org.osate.reqspec.reqSpec.SystemRequirementSet;
import org.osate.result.AnalysisResult;
import org.osate.verify.verify.ArgumentExpr;
import org.osate.verify.verify.Claim;
import org.osate.verify.verify.ElseExpr;
import org.osate.verify.verify.VerificationActivity;
import org.osate.verify.verify.VerificationMethod;
import org.osate.verify.verify.VerificationPlan;

/**
 * @since 4.0
 */
@SuppressWarnings("all")
public class VerifyUtilExtension {
  private static final HashMultimap<String, String> hasRunRecord = HashMultimap.<String, String>create();

  private static final HashMap<String, URI> analysisResultRecord = new HashMap<String, URI>();

  public static boolean getHasRun(final String analysisID, final EObject target) {
    final Set<String> value = VerifyUtilExtension.hasRunRecord.get(analysisID);
    return value.contains(EcoreUtil.getURI(target).toString());
  }

  public static void setHasRun(final String analysisID, final EObject target) {
    VerifyUtilExtension.hasRunRecord.put(analysisID, EcoreUtil.getURI(target).toString());
  }

  public static void unsetHasRun(final String analysisID, final EObject target) {
    VerifyUtilExtension.hasRunRecord.remove(analysisID, EcoreUtil.getURI(target).toString());
  }

  public static void setAnalysisResult(final EObject target, final AnalysisResult analysisResult) {
    VerifyUtilExtension.analysisResultRecord.put(EcoreUtil.getURI(target).toString(), EcoreUtil.getURI(analysisResult));
  }

  public static AnalysisResult getAnalysisResult(final EObject target) {
    AnalysisResult _xblockexpression = null;
    {
      final URI result = VerifyUtilExtension.analysisResultRecord.get(EcoreUtil.getURI(target).toString());
      EObject _eObject = EcoreUtil2.getResourceSet(target).getEObject(result, true);
      _xblockexpression = ((AnalysisResult) _eObject);
    }
    return _xblockexpression;
  }

  public static void clearAllHasRunRecords() {
    VerifyUtilExtension.hasRunRecord.clear();
    VerifyUtilExtension.analysisResultRecord.clear();
  }

  public static boolean hasFail(final ElseExpr cee) {
    ArgumentExpr _fail = cee.getFail();
    return (_fail != null);
  }

  public static boolean hasTimeout(final ElseExpr cee) {
    ArgumentExpr _timeout = cee.getTimeout();
    return (_timeout != null);
  }

  public static boolean hasError(final ElseExpr cee) {
    ArgumentExpr _error = cee.getError();
    return (_error != null);
  }

  public static VerificationPlan containingVerificationPlan(final EObject sh) {
    return EcoreUtil2.<VerificationPlan>getContainerOfType(sh, VerificationPlan.class);
  }

  public static Claim getContainingClaim(final EObject sh) {
    return EcoreUtil2.<Claim>getContainerOfType(sh, Claim.class);
  }

  public static VerificationMethod getContainingVerificationMethod(final EObject sh) {
    return EcoreUtil2.<VerificationMethod>getContainerOfType(sh, VerificationMethod.class);
  }

  public static String ordinal(final Integer i) {
    String _xblockexpression = null;
    {
      final String[] suffixes = new String[10];
      for (int m = 0; (m < suffixes.length); m++) {
        String _switchResult = null;
        switch (m) {
          case 1:
            _switchResult = "st";
            break;
          case 2:
            _switchResult = "nd";
            break;
          case 3:
            _switchResult = "rd";
            break;
          default:
            _switchResult = "th";
            break;
        }
        suffixes[m] = _switchResult;
      }
      String _switchResult = null;
      final int _switchValue = ((i).intValue() % 100);
      switch (_switchValue) {
        case 11:
        case 12:
        case 13:
          _switchResult = (i + "th");
          break;
        default:
          String _xblockexpression_1 = null;
          {
            final int suffIdx = ((i).intValue() % 10);
            String _get = suffixes[suffIdx];
            _xblockexpression_1 = (i + _get);
          }
          _switchResult = _xblockexpression_1;
          break;
      }
      _xblockexpression = _switchResult;
    }
    return _xblockexpression;
  }

  public static void newArrayofSize(final int i) {
    throw new UnsupportedOperationException("TODO: auto-generated method stub");
  }

  public static boolean evaluateRequirementFilter(final Requirement req, final CategoryFilter filter) {
    if ((filter == null)) {
      return true;
    }
    boolean _isNull = Aadl2Util.isNull(req);
    if (_isNull) {
      return false;
    }
    return CategoriesUtil.matches(req.getCategory(), filter.getCategory(), filter.isAnyCategory());
  }

  public static boolean evaluateRequirementFilter(final Claim claim, final CategoryFilter filter) {
    if ((filter == null)) {
      return true;
    }
    final Requirement req = claim.getRequirement();
    boolean _isNull = Aadl2Util.isNull(req);
    if (_isNull) {
      return false;
    }
    boolean _isEmpty = req.getCategory().isEmpty();
    if (_isEmpty) {
      return true;
    }
    return CategoriesUtil.matches(req.getCategory(), filter.getCategory(), filter.isAnyCategory());
  }

  public static boolean evaluateVerificationMethodFilter(final VerificationActivity va, final CategoryFilter filter) {
    if ((filter == null)) {
      return true;
    }
    final VerificationMethod vm = va.getMethod();
    if ((vm == null)) {
      return false;
    }
    return CategoriesUtil.matches(vm.getCategory(), filter.getCategory(), filter.isAnyCategory());
  }

  public static boolean evaluateVerificationActivityFilter(final VerificationActivity va, final CategoryFilter filter) {
    if ((filter == null)) {
      return true;
    }
    return CategoriesUtil.matches(va.getCategory(), filter.getCategory(), filter.isAnyCategory());
  }

  public static String constructVerificationActivityReference(final VerificationActivity va) {
    final Claim claim = VerifyUtilExtension.getContainingClaim(va);
    final VerificationPlan plan = VerifyUtilExtension.containingVerificationPlan(va);
    String _name = plan.getName();
    String _plus = (_name + "#");
    String _constructClaimReferencePath = VerifyUtilExtension.constructClaimReferencePath(claim);
    String _plus_1 = (_plus + _constructClaimReferencePath);
    String _plus_2 = (_plus_1 + "#");
    String _name_1 = va.getName();
    return (_plus_2 + _name_1);
  }

  public static String constructClaimReference(final Claim claim) {
    final VerificationPlan plan = VerifyUtilExtension.containingVerificationPlan(claim);
    String _name = plan.getName();
    String _plus = (_name + "#");
    String _constructClaimReferencePath = VerifyUtilExtension.constructClaimReferencePath(claim);
    return (_plus + _constructClaimReferencePath);
  }

  public static String constructClaimReferencePath(final Claim claim) {
    final EObject parent = claim.eContainer();
    if ((parent instanceof Claim)) {
      String _constructClaimReferencePath = VerifyUtilExtension.constructClaimReferencePath(((Claim)parent));
      String _plus = (_constructClaimReferencePath + ".");
      String _name = claim.getRequirement().getName();
      return (_plus + _name);
    }
    return claim.getRequirement().getName();
  }

  public static ComponentClassifier getTargetClassifier(final VerificationPlan vp) {
    final RequirementSet rs = vp.getRequirementSet();
    if ((rs instanceof SystemRequirementSet)) {
      return ((SystemRequirementSet)rs).getTarget();
    }
    return null;
  }
}