<commit_before>package org.osate.xtext.aadl2.agcl.analysis.algorithms;

import java.util.ArrayList;
import java.util.List;

import org.apache.log4j.Logger;
import org.eclipse.xtext.serializer.ISerializer;
import org.osate.xtext.aadl2.agcl.agcl.AGCLAssumption;
import org.osate.xtext.aadl2.agcl.agcl.AGCLContract;
import org.osate.xtext.aadl2.agcl.agcl.AGCLGuarantee;
import org.osate.xtext.aadl2.agcl.agcl.AgclFactory;
import org.osate.xtext.aadl2.agcl.agcl.BooleanConstant;
import org.osate.xtext.aadl2.agcl.agcl.PSLConjunction;
import org.osate.xtext.aadl2.agcl.agcl.PSLExpression;
import org.osate.xtext.aadl2.agcl.agcl.PSLImplication;
import org.osate.xtext.aadl2.agcl.agcl.PSLSpec;
import org.osate.xtext.aadl2.agcl.analysis.AGCLAnalysisPlugin;
import org.osate.xtext.aadl2.agcl.analysis.util.AGCLSyntaxUtil;
import org.osate.xtext.aadl2.agcl.analysis.verifiers.ModelChecker;
import org.osate.xtext.aadl2.agcl.analysis.verifiers.NuSMVModelChecker;
import org.osate.xtext.aadl2.agcl.analysis.visitors.ViewpointContext;

/**
 * This class is intended to provide common attributes and functionality for the concrete algorithm classes.
 * 
 * <p>The main method provided is {@link #checkContractRefinement(AGCLContract, AGCLContract, String, String)}.
 * 
 * @author <NAME>
 *
 */
public abstract class AnalysisAlgorithmBase {

	protected final ViewpointContext viewpointContext;
	protected final ISerializer serializer;
	protected final ModelChecker checker;

	public AnalysisAlgorithmBase(ViewpointContext viewpointContext) {
		this.viewpointContext = viewpointContext;
		this.serializer = AGCLAnalysisPlugin.getDefault().getSerializer();
		this.checker = AGCLAnalysisPlugin.getDefault().getActiveModelChecker();
	}
	
	/**
	 * Checks whether a contract C1 is a refinement of another contract C2, this is, whether the following
	 * PSL specifications are valid:
	 * 
	 *  <p> A2 -> A1, and
	 *  <p> G1 -> G2
	 *  
	 *  <p>where A1 and A2 are the assumptions of C1 and C2 respectively, and G1 and G2 are their guarantees.
	 *  
	 *  <p> Note the implications are contra-variant on the assumptions and co-variant on the guarantees.
	 *  
	 *  <p> The result is collected in the model-checker's results collection ({@link ModelChecker#getResults()})
	 *  
	 * @param contract1		contract C1
	 * @param contract2		contract C2
	 * @param viewpointName	the name of the analysis viewpoint under verification
	 * @param componentName	the name of the component for which this analysis is being performed. Usually it should be
	 * 		the name of the component owning contract C1, for child/parent checks, or the name of the component
	 * 		that owns contract C2, for compositional analysis.
	 */
	public void checkContractRefinement(AGCLContract contract1, AGCLContract contract2, String viewpointName, String componentName) {
		AGCLAssumption assumption1 = contract1.getAssumption();
		AGCLAssumption assumption2 = contract2.getAssumption();
		AGCLGuarantee guarantee1 = contract1.getGuarantee();
		AGCLGuarantee guarantee2 = contract2.getGuarantee();
		PSLSpec assumption1spec = AGCLSyntaxUtil.deepCopy(assumption1.getSpec());
		PSLSpec assumption2spec = AGCLSyntaxUtil.deepCopy(assumption2.getSpec());
		PSLSpec guarantee1spec = AGCLSyntaxUtil.deepCopy(guarantee1.getSpec());
		PSLSpec guarantee2spec = AGCLSyntaxUtil.deepCopy(guarantee2.getSpec());
		Logger.getLogger(getClass()).debug("assumption1 = '" + serializer.serialize(assumption1spec) + " ast = " + AGCLSyntaxUtil.astStr(assumption1spec));
		Logger.getLogger(getClass()).debug("assumption2 = '" + serializer.serialize(assumption2spec) + " ast = " + AGCLSyntaxUtil.astStr(assumption2spec));
		Logger.getLogger(getClass()).debug("guarantee1 = '" + serializer.serialize(guarantee1spec) + " ast = " + AGCLSyntaxUtil.astStr(guarantee1spec));
		Logger.getLogger(getClass()).debug("guarantee2 = '" + serializer.serialize(guarantee2spec) + " ast = " + AGCLSyntaxUtil.astStr(guarantee2spec));
		PSLSpec assumptionsImplication = makeImplication(assumption2spec, assumption1spec);
		PSLSpec guaranteesImplication = makeImplication(guarantee1spec, guarantee2spec);
		PSLSpec combined = makeConjunction(assumptionsImplication, guaranteesImplication);
		NuSMVModelChecker theChecker = (NuSMVModelChecker) checker;  // TODO: make it independent of NuSMV
		Logger.getLogger(getClass()).debug("checking '" + serializer.serialize(combined) + "'");
		theChecker.checkSpecValidity(combined, viewpointName, componentName, "refinement");
	}

	/**
	 * @param spec1	a PSL spec S1 
	 * @param spec2	a PSL spec S2
	 * @return a combined PSL spec of the form S1 -> S2
	 */
	protected PSLSpec makeImplication(PSLSpec spec1, PSLSpec spec2) {
		PSLExpression expr1 = spec1.getExpr();
		PSLExpression expr2 = spec2.getExpr();
		PSLSpec newSpec = AgclFactory.eINSTANCE.createPSLSpec();
		PSLImplication newExpr = AgclFactory.eINSTANCE.createPSLImplication();
		newExpr.setLeft(expr1);
		newExpr.setRight(expr2);
		newSpec.setExpr(newExpr);
		return newSpec;
	}
	
	/**
	 * @param spec1	a PSL spec S1 
	 * @param spec2	a PSL spec S2
	 * @return a combined PSL spec of the form S1 & S2
	 */
	protected PSLSpec makeConjunction(PSLSpec spec1, PSLSpec spec2) {
		PSLExpression expr1 = spec1.getExpr();
		PSLExpression expr2 = spec2.getExpr();
		PSLSpec newSpec = AgclFactory.eINSTANCE.createPSLSpec();
		PSLConjunction newExpr = AgclFactory.eINSTANCE.createPSLConjunction();
		newExpr.setLeft(expr1);
		newExpr.setRight(expr2);
		newSpec.setExpr(newExpr);
		return newSpec;
	}
	
	/**
	 * @param specs	a list of PSL specs S1, S2, ..., Sn
	 * @return a combined PSL spec of the form ( ...((S1 & S2) & ... ) & Sn
	 */
	protected PSLSpec makeNaryConjunction(List<PSLSpec> specs) {
		PSLSpec newSpec = AgclFactory.eINSTANCE.createPSLSpec();
		List<PSLExpression> expressions = new ArrayList<PSLExpression>();
		for (PSLSpec spec : specs) {
			expressions.add(spec.getExpr());
		}
		PSLExpression newExpr = makeNaryExprConjunction(expressions);
		newSpec.setExpr(newExpr);
		return newSpec;
	}

	protected PSLExpression makeNaryExprConjunction(List<PSLExpression> expressions) {
		if (expressions.isEmpty()) {
			BooleanConstant newConstant = AgclFactory.eINSTANCE.createBooleanConstant();
			newConstant.setVal("TRUE");
			return newConstant;
		}
		else if (expressions.size() == 1) {
			return expressions.get(0);   // should I deep copy?
		}
		else {
			PSLExpression newExpr = expressions.get(0);
			for (PSLExpression subexpression : expressions.subList(1, expressions.size())) {
				PSLConjunction newConjunction = AgclFactory.eINSTANCE.createPSLConjunction();
				newConjunction.setLeft(newExpr);
				newConjunction.setRight(subexpression);
				newExpr = newConjunction;
			}
			return newExpr;
		}
	}
	
}<commit_msg>- Added deep copy to makeNareExprConjunction since it turns out, the Ecore model generated for the Xtext grammar doesn't support sharing of AST nodes.<commit_after>package org.osate.xtext.aadl2.agcl.analysis.algorithms;

import java.util.ArrayList;
import java.util.List;

import org.apache.log4j.Logger;
import org.eclipse.xtext.serializer.ISerializer;
import org.osate.xtext.aadl2.agcl.agcl.AGCLAssumption;
import org.osate.xtext.aadl2.agcl.agcl.AGCLContract;
import org.osate.xtext.aadl2.agcl.agcl.AGCLGuarantee;
import org.osate.xtext.aadl2.agcl.agcl.AgclFactory;
import org.osate.xtext.aadl2.agcl.agcl.BooleanConstant;
import org.osate.xtext.aadl2.agcl.agcl.PSLConjunction;
import org.osate.xtext.aadl2.agcl.agcl.PSLExpression;
import org.osate.xtext.aadl2.agcl.agcl.PSLImplication;
import org.osate.xtext.aadl2.agcl.agcl.PSLSpec;
import org.osate.xtext.aadl2.agcl.analysis.AGCLAnalysisPlugin;
import org.osate.xtext.aadl2.agcl.analysis.util.AGCLSyntaxUtil;
import org.osate.xtext.aadl2.agcl.analysis.verifiers.ModelChecker;
import org.osate.xtext.aadl2.agcl.analysis.verifiers.NuSMVModelChecker;
import org.osate.xtext.aadl2.agcl.analysis.visitors.ViewpointContext;

/**
 * This class is intended to provide common attributes and functionality for the concrete algorithm classes.
 * 
 * <p>The main method provided is {@link #checkContractRefinement(AGCLContract, AGCLContract, String, String)}.
 * 
 * @author <NAME>
 *
 */
public abstract class AnalysisAlgorithmBase {

	protected final ViewpointContext viewpointContext;
	protected final ISerializer serializer;
	protected final ModelChecker checker;

	public AnalysisAlgorithmBase(ViewpointContext viewpointContext) {
		this.viewpointContext = viewpointContext;
		this.serializer = AGCLAnalysisPlugin.getDefault().getSerializer();
		this.checker = AGCLAnalysisPlugin.getDefault().getActiveModelChecker();
	}
	
	/**
	 * Checks whether a contract C1 is a refinement of another contract C2, this is, whether the following
	 * PSL specifications are valid:
	 * 
	 *  <p> A2 -> A1, and
	 *  <p> G1 -> G2
	 *  
	 *  <p>where A1 and A2 are the assumptions of C1 and C2 respectively, and G1 and G2 are their guarantees.
	 *  
	 *  <p> Note the implications are contra-variant on the assumptions and co-variant on the guarantees.
	 *  
	 *  <p> The result is collected in the model-checker's results collection ({@link ModelChecker#getResults()})
	 *  
	 * @param contract1		contract C1
	 * @param contract2		contract C2
	 * @param viewpointName	the name of the analysis viewpoint under verification
	 * @param componentName	the name of the component for which this analysis is being performed. Usually it should be
	 * 		the name of the component owning contract C1, for child/parent checks, or the name of the component
	 * 		that owns contract C2, for compositional analysis.
	 */
	public void checkContractRefinement(AGCLContract contract1, AGCLContract contract2, String viewpointName, String componentName) {
		AGCLAssumption assumption1 = contract1.getAssumption();
		AGCLAssumption assumption2 = contract2.getAssumption();
		AGCLGuarantee guarantee1 = contract1.getGuarantee();
		AGCLGuarantee guarantee2 = contract2.getGuarantee();
		PSLSpec assumption1spec = AGCLSyntaxUtil.deepCopy(assumption1.getSpec());
		PSLSpec assumption2spec = AGCLSyntaxUtil.deepCopy(assumption2.getSpec());
		PSLSpec guarantee1spec = AGCLSyntaxUtil.deepCopy(guarantee1.getSpec());
		PSLSpec guarantee2spec = AGCLSyntaxUtil.deepCopy(guarantee2.getSpec());
		Logger.getLogger(getClass()).debug("assumption1 = '" + serializer.serialize(assumption1spec) + " ast = " + AGCLSyntaxUtil.astStr(assumption1spec));
		Logger.getLogger(getClass()).debug("assumption2 = '" + serializer.serialize(assumption2spec) + " ast = " + AGCLSyntaxUtil.astStr(assumption2spec));
		Logger.getLogger(getClass()).debug("guarantee1 = '" + serializer.serialize(guarantee1spec) + " ast = " + AGCLSyntaxUtil.astStr(guarantee1spec));
		Logger.getLogger(getClass()).debug("guarantee2 = '" + serializer.serialize(guarantee2spec) + " ast = " + AGCLSyntaxUtil.astStr(guarantee2spec));
		PSLSpec assumptionsImplication = makeImplication(assumption2spec, assumption1spec);
		PSLSpec guaranteesImplication = makeImplication(guarantee1spec, guarantee2spec);
		PSLSpec combined = makeConjunction(assumptionsImplication, guaranteesImplication);
		NuSMVModelChecker theChecker = (NuSMVModelChecker) checker;  // TODO: make it independent of NuSMV
		Logger.getLogger(getClass()).debug("checking '" + serializer.serialize(combined) + "'");
		theChecker.checkSpecValidity(combined, viewpointName, componentName, "refinement");
	}

	/**
	 * @param spec1	a PSL spec S1 
	 * @param spec2	a PSL spec S2
	 * @return a combined PSL spec of the form S1 -> S2
	 */
	protected PSLSpec makeImplication(PSLSpec spec1, PSLSpec spec2) {
		PSLExpression expr1 = spec1.getExpr();
		PSLExpression expr2 = spec2.getExpr();
		PSLSpec newSpec = AgclFactory.eINSTANCE.createPSLSpec();
		PSLImplication newExpr = AgclFactory.eINSTANCE.createPSLImplication();
		newExpr.setLeft(expr1);
		newExpr.setRight(expr2);
		newSpec.setExpr(newExpr);
		return newSpec;
	}
	
	/**
	 * @param spec1	a PSL spec S1 
	 * @param spec2	a PSL spec S2
	 * @return a combined PSL spec of the form S1 & S2
	 */
	protected PSLSpec makeConjunction(PSLSpec spec1, PSLSpec spec2) {
		PSLExpression expr1 = spec1.getExpr();
		PSLExpression expr2 = spec2.getExpr();
		PSLSpec newSpec = AgclFactory.eINSTANCE.createPSLSpec();
		PSLConjunction newExpr = AgclFactory.eINSTANCE.createPSLConjunction();
		newExpr.setLeft(expr1);
		newExpr.setRight(expr2);
		newSpec.setExpr(newExpr);
		return newSpec;
	}
	
	/**
	 * @param specs	a list of PSL specs S1, S2, ..., Sn
	 * @return a combined PSL spec of the form ( ...((S1 & S2) & ... ) & Sn
	 */
	protected PSLSpec makeNaryConjunction(List<PSLSpec> specs) {
		PSLSpec newSpec = AgclFactory.eINSTANCE.createPSLSpec();
		List<PSLExpression> expressions = new ArrayList<PSLExpression>();
		for (PSLSpec spec : specs) {
			expressions.add(spec.getExpr());
		}
		PSLExpression newExpr = makeNaryExprConjunction(expressions);
		newSpec.setExpr(newExpr);
		return newSpec;
	}

	protected PSLExpression makeNaryExprConjunction(List<PSLExpression> expressions) {
		if (expressions.isEmpty()) {
			BooleanConstant newConstant = AgclFactory.eINSTANCE.createBooleanConstant();
			newConstant.setVal("TRUE");
			return newConstant;
		}
		else if (expressions.size() == 1) {
			return AGCLSyntaxUtil.deepCopy(expressions.get(0));   // should I deep copy?
		}
		else {
			PSLExpression newExpr = AGCLSyntaxUtil.deepCopy(expressions.get(0));
			for (PSLExpression subexpression : expressions.subList(1, expressions.size())) {
				PSLConjunction newConjunction = AgclFactory.eINSTANCE.createPSLConjunction();
				newConjunction.setLeft(newExpr);
				newConjunction.setRight(AGCLSyntaxUtil.deepCopy(subexpression));
				newExpr = newConjunction;
			}
			return newExpr;
		}
	}
	
}
{'fraction_non_alphanumeric': 0.10520543939172394, 'fraction_numerical': 0.015206901593800263, 'mean_word_length': 5.093095768374165, 'pattern_counts': {'":': 0, '<': 25, '<?xml version=': 0, '>': 31, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '265685', 'n_tokens_mistral': 4744, 'n_tokens_neox': 4422, 'n_words': 971}