org.eclipse.opencert.vavmanager/src/org/eclipse/opencert/vavmanager/RequestWriter.java

/*******************************************************************************
 * Copyright (c) 2017 Honeywell, Inc.
 *
 * All rights reserved. This program and the accompanying materials
 * are made available under the terms of the Eclipse Public License v2.0
 * which accompanies this distribution, and is available at
 * https://www.eclipse.org/org/documents/epl-2.0/EPL-2.0.html
 *
 * SPDX-License-Identifier: EPL-2.0
 *  
 * Contributors:
 *   Vit Koksa  <Vit.Koksa@honeywell.com>
 *   Initial API and implementation and/or initial documentation
 *******************************************************************************/

package org.eclipse.opencert.vavmanager;

import java.lang.reflect.Array;

//import org.polarsys.chess.contracts.profile.chesscontract.impl.ContractImpl;

import java.util.ArrayList;
import java.util.Arrays;
import java.util.HashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Set;
//import java.util.stream.Stream;

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.eclipse.jface.dialogs.MessageDialog;
import org.eclipse.swt.widgets.Shell;
import org.eclipse.ui.PlatformUI;
import org.eclipse.uml2.uml.Stereotype;
import org.eclipse.uml2.uml.Type;
import org.polarsys.chess.contracts.profile.chesscontract.Contract;
import org.polarsys.chess.contracts.profile.chesscontract.ContractProperty;
import org.polarsys.chess.contracts.profile.chesscontract.FormalProperty;
import org.eclipse.uml2.uml.internal.impl.PortImpl;
//import org.polarsys.chess.utils;
import org.eclipse.uml2.uml.internal.impl.PropertyImpl;
import org.eclipse.xtext.util.Pair;
//import org.eclipse.uml2.uml.internal.impl.ClassifierImpl;
//import org.eclipse.emf.common.util.EList;
//import org.eclipse.uml2.uml.Property;
//import org.eclipse.uml2.uml.Stereotype;
import org.eclipse.uml2.uml.Class;
//import org.eclipse.uml2.uml.Classifier;
import org.eclipse.uml2.uml.Element;
//import org.eclipse.uml2.uml.Port;
//import org.eclipse.uml2.uml.Constraint;
//import org.eclipse.uml2.uml.Namespace;
import org.polarsys.chess.contracts.profile.chesscontract.util.Constants;
import org.polarsys.chess.contracts.profile.chesscontract.util.ContractEntityUtil;
import org.polarsys.chess.contracts.profile.chesscontract.util.EntityUtil;

public class RequestWriter {
	private static final String CONTRACTPROP = "CHESSContract::ContractProperty";
	private static final String FORMPROP = "CHESSContract::FormalProperty";
	private static ContractEntityUtil contractEntityUtil = ContractEntityUtil.getInstance();
	private static EntityUtil entityUtil = EntityUtil.getInstance();

	/* Has the element a given stereotype? */
	public static Boolean hasStereotype(Element elt, String stereotype) {	// "Contract", "Block"
		return elementHasType(elt, stereotype);
	}

	/* Is the input really a Component? */
	public static Boolean isComponent(Element elt) {
		return elementHasType(elt, "Block");
	}

	/* Has the element a given stereotype? */
	public static Boolean elementHasType(Element elt, String type) {
		boolean hasType = false;
		EList<Stereotype> stList = ((Element) elt).getAppliedStereotypes();
		String stName;
		stereotypes:
		for (Stereotype st : stList) {
			stName = st.getName();
			if (stName.equals(type)) {
				hasType = true;
				break stereotypes;
			}
		}
		return hasType;
	}
	
	public static String mergeInputs(String inOuts) {	// inOuts = ".inputs i1, i2\n.outputs o1\n.inputs i1, i3, i4\n.outputs o2"
		String[] lines;
		lines = inOuts.split("\n");		// lines = [".inputs i1, i2", ".outputs o1", ".inputs i1, i3, i4", ".outputs o2"]
		String[] ins = Arrays.stream(lines).filter(x -> x.startsWith(".inputs")).toArray(String[]::new);	// ins = [".inputs i1, i2", ".inputs i1, i3, i4"]
		String[] outs = Arrays.stream(lines).filter(x -> x.startsWith(".outputs")).toArray(String[]::new);	// outs = [".outputs o1", ".outputs o2"]
		
		List<String> listOfInputs = new ArrayList<String>();	// listOfInputs = ["i1", "i2", "i3", "i4"]
		for (String insStr : ins) {
			lines = insStr.replaceFirst("^.inputs",  "").split(",");	// lines variable is recycled
			for (String inStr : lines) {
				listOfInputs.add(inStr.trim());
			}
		}
		Set<String> set = new HashSet<String>(listOfInputs);	// remove duplicates
		lines = set.toArray(new String[set.size()]);		// lines variable is recycled
		listOfInputs = Arrays.asList(lines);
		
		List<String> listOfOutputs = new ArrayList<String>();	// listOfOutputs = ["o1", "o2"]
		for (String outsStr : outs) {
			lines = outsStr.replaceFirst("^.outputs",  "").split(",");	// lines variable is recycled
			for (String outStr : lines) {
				listOfOutputs.add(outStr.trim());
			}
		}
		set = new HashSet<String>(listOfOutputs);	// remove duplicates
		lines = set.toArray(new String[set.size()]);		// lines variable is recycled
		listOfOutputs = Arrays.asList(lines);
		
		String stringOfInputs = String.join(" ", listOfInputs);	// stringOfInputs = "i1 i2 i3 i4"
		String stringOfOutputs = String.join(" ", listOfOutputs);	// stringOfOutputs = "o1 o2"
		String result = ".inputs " + stringOfInputs + "\n.outputs " + stringOfOutputs;
		return result;		// result = ".inputs i1 i2 i3 i4\n.outputs o1 o2"
	}
	
	public static String extractAssume(Element elt) {
		String assume = "";		// the variable whose content will be returned by the function
		
		/* Get the assumption of the contract. */
		if (hasStereotype(elt, "Contract")) {
			if (elt instanceof Class) {
				return "";	// Currently selected Contract is not supported. Classification of signals to either input or output is not realised. 
				//assume = contractEntityUtil.getAssumeStrFromUmlContract((Class) elt);
			} else {
				throw new RuntimeException("elt has the <Contract> stereotype, but is not of type Class.");
			}
		} else {
			
			/* Get the assumes of the component. */
			if (hasStereotype(elt, "Block")) {
				EList<ContractProperty> contrProp = contractEntityUtil.getContractProperties((Class) elt);
		        Class contractBaseClass = null;
		        Contract contract = null;
		        FormalProperty assumptionFP = null;
		        StringBuffer sBuf = new StringBuffer();
		        for (ContractProperty prop : contrProp){
		            contractBaseClass = (Class) prop.getBase_Property().getType();
		            contract = (Contract) contractBaseClass.getStereotypeApplication(contractBaseClass.getAppliedStereotype(Constants.CONTRACT));
		            assumptionFP = contract.getAssume();
		            sBuf.append("\n" + assumptionFP.getBase_Constraint().getSpecification().stringValue());
		        }
		        assume = sBuf.toString();
	            assume = mergeInputs(assume);
			}
		}
		
		return assume;
	}

	/**
	 * get the contents of the element
	 *
	 * @param selectedElement
	 * @return the root element
	 */
/*	private static TreeIterator<EObject> getAllContents(EObject selectedElement) {
		TreeIterator<EObject> selectedContents = selectedElement.eAllContents();
		return selectedContents;
	}
*/
	
	public static String extractGuaranteeFromComponent(Element elt) {
		String guarantee = "";		// the variable whose content will be returned by the function
		if (elt instanceof Class) {
			EList<ContractProperty> contrProp = contractEntityUtil.getContractProperties((Class) elt);
	        Class contractBaseClass = null;
	        Contract contract = null;
	        FormalProperty guaranteeFP = null;
	        StringBuffer sBuf = new StringBuffer();
	        for (ContractProperty prop : contrProp){
	            contractBaseClass = (Class) prop.getBase_Property().getType();
	            contract = (Contract) contractBaseClass.getStereotypeApplication(contractBaseClass.getAppliedStereotype(Constants.CONTRACT));
	            guaranteeFP = contract.getGuarantee();
	            sBuf.append("\n" + guaranteeFP.getBase_Constraint().getSpecification().stringValue());
	        }
	        guarantee = sBuf.toString();
	        return guarantee.trim();
		} else {
			MessageDialog.openInformation(VAndVManagerCommand.shell, "Selected element can have no related guarantee.", 
					"Please, change your selection.");
			return "";
		}
	}
	
	public static String extractGuarantee(Element elt) {
		String guarantee = "";		// the variable whose content will be returned by the function

		/* Get the guarantee of the contract. */
		if (hasStereotype(elt, "Contract")) {
			if (elt instanceof Class) {
				MessageDialog.openInformation(VAndVManagerCommand.shell, "The V&V Manager currently does not check contracts.",
						"The needed classification of signals as either inputs or outputs is not realised for contracts." 
						+ "\nPlease, do not select contracts for V&V Manager.");
				return "";
				//guarantee = contractEntityUtil.getGuaranteeStrFromUmlContract((Class) elt);
			} else {
				throw new RuntimeException("elt has the <Contract> stereotype, but is not of type Class.");
			}
		} else {
			
			/* Get the guarantees of the component (and optionally also of the subcomponents). */
			if (hasStereotype(elt, "Block")) {
				boolean alsoSub;
				// EList<Element> listObjs = elt.getOwnedElements();	// eContents();
				TreeIterator<EObject> titer = elt.eAllContents();	//getAllContents(elt);
				int nodeCount = 0;
				EObject eobj;
				PropertyImpl property;
				boolean isProperty;
				boolean isBlock;
				treeIteration:
				while (titer.hasNext()) {
					eobj = titer.next();
					String str = eobj.getClass().getName();
					isProperty = str.endsWith("PropertyImpl");
					if (isProperty) {	// && hasStereotype((Element)eobj, "part")) {
						property = (PropertyImpl) eobj;
						Type type = property.getType();
						EList<Stereotype> stereotypes = type.getAppliedStereotypes();
						for (Stereotype stype : stereotypes) {
							isBlock = stype.getName().equals("Block");
							if (isBlock) {
								nodeCount++;
								if (nodeCount == 1) {	// Validated element has at least one subcomponent.
									alsoSub = MessageDialog.openQuestion(VAndVManagerCommand.shell, "Include contracts of subcomponents?", 
											"The selected block has subblock(s). Should their formal properties be included in the validation/verification?");
									if (!alsoSub) {
										guarantee = extractGuaranteeFromComponent(elt);		// Process just the selected component.
										break treeIteration;	// while (titer.hasNext())
									}
								}
								guarantee += "\n" + extractGuaranteeFromComponent((Element) type);
							}
						}
					}
				}
				if (nodeCount == 0) {	// selected component has no subcomponents.
					guarantee = extractGuaranteeFromComponent(elt);
				}
			}
		}
		
		return guarantee.trim();
	}

	public static String extractLtl(Element contract) {
		//Class cl = contract.getClass();
		String ltl = "No LTL.";
		EList<Stereotype> stList = ((Element) contract).getAppliedStereotypes();
		boolean isContract = false;
		String stName;
		stereotypes:
		for (Stereotype st : stList) {
			stName = st.getName();
			if (stName.equals("Contract")) {
				isContract = true;
				if (contract instanceof Class) {
					//String str = contractEntityUtil.getAssumeStrFromUmlContract((Class) contract);
					ltl = contractEntityUtil.getGuaranteeStrFromUmlContract((Class) contract);
					break stereotypes;
				} else {
					throw new RuntimeException("elt has the <Contract> stereotype, but is not of type Class.");
				}
			}
		}

		/*
		List<Constraint> allFormalProps = new ArrayList<Constraint>();
		List<Property> allContractProperties = new ArrayList<Property>();
		
		if (contract instanceof Property){
			if (contract.getAppliedStereotype(CONTRACTPROP) != null){
				allContractProperties.add((Property) contract);
			}
		}
		if (contract instanceof Constraint && contract.getAppliedStereotype(FORMPROP) != null){
			allFormalProps.add((Constraint)contract);
		}

		if (isContract) {
			for (Element elt : contract.allOwnedElements()) {
				if (elt instanceof Constraint) {
					System.out.println("asdf");
				}
			}
			//Property pr = ((Classifier) contract).get  //getOwnedAttribute("Assume", null);
			List<Property> props = ((Classifier) contract).getAttributes();
			for (Property prop : props) {
				String propName = prop.getName();
				if  (propName.equals("Assume")) {
					ltl = "aaa";
				}
			}
		}
		if (contract != null) {
			//ContractImpl cntrct = (ContractImpl) contract;
			//ltl = cntrct.getAssume().getBase_Constraint().getSpecification().toString();
			return ltl;
		}
		*/
		return ltl;
	}

	public static String[] getInputPortsNames(Element elt) {
		String[] inputPortsNames = entityUtil.getInputPortsNames(elt,false);
		return inputPortsNames;
	}

	public static String[] getOutputPortsNames(Element elt) {
		String[] outputPortsNames = entityUtil.getOutputPortsNames(elt,false);
		return outputPortsNames;
	}

	public static String[] getInputOutputPortsNames(Element elt) {
		String[] inputOutputPortsNames = entityUtil.getInputOutputPortsNames(elt,false);
		return inputOutputPortsNames;
	}

/*	public static EList<PortImpl> getPorts(Element elt) {
		EList<PortImpl> portList = new BasicEList<PortImpl>();
		String[] inputPortNames, outputPortNames, inputOutputPortNames;
		// Get the guarantees of the component (and optionally also of the subcomponents).
		if (hasStereotype(elt, "Block")) {
			inputPortNames = entityUtil.getInputPortsNames(elt);
			outputPortNames = entityUtil.getOutputPortsNames(elt);
			inputOutputPortNames = entityUtil.getInputOutputPortsNames(elt);
			boolean alsoSub;
			//EList<Element> listObjs = elt.getOwnedElements();	// eContents();
			TreeIterator<EObject> titer = elt.eAllContents();	//getAllContents(elt);
			int nodeCount = 0;
			EObject eobj;
			PortImpl port;
			boolean isPort;
			boolean isBlock;
			int direction;
			treeIteration:
			while (titer.hasNext()) {
				eobj = titer.next();
				//String str = eobj.getClass().getName();
				//isPort = str.endsWith("PortImpl");
				isPort = entityUtil.isPort((Element) eobj);
				if (isPort) {	// && hasStereotype((Element)eobj, "part")) {
					direction = entityUtil.getPortDirection((Element) eobj);
					port = (PortImpl) eobj;
					portList.add(port);
					//Type type = port.getType();
				}
			}
		}
		return portList;
	}
*/

	static Set<String> extractSignalsFromLtl(String ltl) {
		String[] signals = null;
		Set<String> sigs = new HashSet<String>();	// signals and filtered signals
		signals = ltl.split("[()\n &|!]+");
		for (String sig : signals) {
			if (!sig.equals("G") && !sig.equals("X") && !sig.equals("F") && !sig.equals("U") && !sig.equals("->") && !sig.equals("<->")) {
				sigs.add(sig);
			}
		}
		return sigs;
	}

	/*
	 * result[0] .. inputs
	 * result[1] .. outputs
	 */
	static String extractInputsAndOutputs(Set<String> signalsFromLtl, 
			String[] inputPortNames, String[] outputPortsNames, String[] inputOutputPortsNames) {
		String inputs = "";
		String outputs = "";
		for (String sig : signalsFromLtl) {
			boolean isInput = false;
			boolean isOutput = false;
			for (String inp : inputPortNames) {
				if (sig.startsWith(inp) || sig.endsWith(inp)) {
					isInput = true;
				}
			}
			for (String outp : outputPortsNames) {
				if (sig.startsWith(outp) || sig.endsWith(outp)) {
					isOutput = true;
				}
			}
			for (String inoutp : inputOutputPortsNames) {
				if (sig.startsWith(inoutp) || sig.endsWith(inoutp)) {
					isOutput = true;
				}
			}
			if (isOutput) {
				outputs += " " + sig;
			}
			if (isInput) {
				inputs += " " + sig;
			}
			if (isInput && isOutput) {
				MessageDialog.openInformation(VAndVManagerCommand.shell, "The V&V Manager unable to distiguish input from output.",
						"The following signal seems to be input and output at the same time: " + sig 
						+ " . Not sure how to submit it to the verification." 
						+ "\nPlease, consider renaming of the signals or of the ports.");
			}
			if (! isInput && ! isOutput) {
				MessageDialog.openInformation(VAndVManagerCommand.shell, "The V&V Manager: signal neither input nor output.",
						"The following signal could be identified neither as input nor as output: " + sig 
						+ " . Not sure how to submit it to the verification." 
						+ "\nPlease, consider renaming of the signals or of the ports.");
			}
		}
		return ".inputs" + inputs + "\n.outputs" + outputs;
	}
}