| /******************************************************************************* | |
| * 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 org.eclipse.emf.ecore.EObject; | |
| //import java.io.File; | |
| import java.io.StringReader; | |
| import java.net.HttpURLConnection; | |
| import java.util.Iterator; | |
| //import java.util.Set; | |
| import java.util.Set; | |
| import javax.xml.namespace.NamespaceContext; | |
| import javax.xml.parsers.DocumentBuilder; | |
| import javax.xml.parsers.DocumentBuilderFactory; | |
| import javax.xml.xpath.XPath; | |
| //import javax.xml.xpath.XPathConstants; | |
| //import javax.xml.xpath.XPathExpression; | |
| import javax.xml.xpath.XPathFactory; | |
| import org.eclipse.core.commands.ExecutionException; | |
| import org.eclipse.core.runtime.IAdaptable; | |
| import org.eclipse.core.runtime.IProgressMonitor; | |
| import org.eclipse.papyrus.infra.services.validation.commands.AbstractValidateCommand; | |
| import org.eclipse.gmf.runtime.common.core.command.CommandResult; | |
| import org.eclipse.emf.transaction.util.TransactionUtil; | |
| import org.eclipse.papyrus.infra.services.validation.IPapyrusDiagnostician; | |
| import org.eclipse.papyrus.infra.services.validation.Messages; | |
| //import org.eclipse.swt.SWT; | |
| //import org.eclipse.swt.widgets.Display; | |
| //import org.eclipse.swt.widgets.FileDialog; | |
| import org.eclipse.swt.widgets.Shell; | |
| import org.eclipse.ui.PartInitException; | |
| import org.eclipse.ui.PlatformUI; | |
| import org.eclipse.uml2.uml.internal.impl.ClassImpl; | |
| import org.eclipse.emf.common.util.EList; | |
| import org.eclipse.emf.common.util.TreeIterator; | |
| //import org.eclipse.uml2.uml.Class; | |
| //import org.eclipse.uml2.uml.Port; | |
| import org.eclipse.uml2.uml.Stereotype; | |
| import org.eclipse.uml2.uml.internal.impl.ElementImpl; | |
| import org.eclipse.xtext.util.Pair; | |
| import org.w3c.dom.Document; | |
| //import org.w3c.dom.Node; | |
| //import org.w3c.dom.NodeList; | |
| import org.xml.sax.InputSource; | |
| //import eu.hon.eclipse.vavmanager.RequestWriter; | |
| import org.eclipse.jface.dialogs.MessageDialog; | |
| /** | |
| * Communication with the V&V tools. | |
| * | |
| * @author E334628 | |
| * | |
| */ | |
| public class VAndVManagerCommand extends AbstractValidateCommand { | |
| static final Shell shell = PlatformUI.getWorkbench().getActiveWorkbenchWindow().getShell(); // shell needed for displaying an information window | |
| final static String urlStr = | |
| //"http://138.90.228.243:6080"; // Rak | |
| "http://147.251.51.238:8080"; // Pleiada pleiada01.fi.muni.cz | |
| /** | |
| * Constructor for validation with EcoreDiagnostician | |
| * | |
| * @param selectedElement | |
| * an element of the model to validate | |
| */ | |
| public VAndVManagerCommand(EObject selectedElement) { | |
| this(selectedElement, null); | |
| } | |
| /** | |
| * Constructor based on selected element and diagnostician | |
| * | |
| * @param selectedElement | |
| * an element of the model to validate | |
| * @param diagnostician | |
| * the diagnostician (e.g. EcoreDiagnostician) | |
| */ | |
| public VAndVManagerCommand(EObject selectedElement, IPapyrusDiagnostician diagnostician) { | |
| //super(Messages.ValidateModelCommand_ValidateModel, TransactionUtil.getEditingDomain(selectedElement), getTopOwner(selectedElement), diagnostician); | |
| super(Messages.ValidateModelCommand_ValidateModel, TransactionUtil.getEditingDomain(selectedElement), selectedElement, diagnostician); | |
| } | |
| /** | |
| * get the root element | |
| * | |
| * @param selectedElement | |
| * @return the root element | |
| */ | |
| /* private static EObject getTopOwner(EObject selectedElement) { | |
| EObject selectedObject = selectedElement; | |
| while (selectedObject.eContainer() != null) { | |
| selectedObject = selectedObject.eContainer(); | |
| } | |
| return selectedObject; | |
| } | |
| */ | |
| /** | |
| * {@inheritDoc} | |
| */ | |
| @Override | |
| protected CommandResult doExecuteWithResult(IProgressMonitor monitor, IAdaptable info) throws ExecutionException { | |
| // replace selection by model instead of current selection | |
| if (selectedElement != null) { | |
| runValidation(selectedElement); | |
| } | |
| return null; | |
| } | |
| /* Upload string to server. */ | |
| String uploadString(String strng) { | |
| /* Manual selection of a file. | |
| FileDialog fdLtl = new FileDialog(Display.getCurrent().getActiveShell(), SWT.OPEN); | |
| fdLtl.setText("Select the local LTL file to upload"); | |
| fdLtl.open(); | |
| String fileNameLtl = (fdLtl.getFilterPath()) + File.separator + fdLtl.getFileName(); | |
| */ | |
| String fileId = null; | |
| String resultOfUpload = null; | |
| if (! strng.isEmpty()) { | |
| Sender uploadSender = new Sender(); | |
| HttpURLConnection connUpload; | |
| connUpload = uploadSender.uploadString(strng, urlStr); | |
| if (connUpload != null) { | |
| Receiver receiverUpload = new Receiver(); | |
| resultOfUpload = receiverUpload.receive(connUpload); | |
| if (!resultOfUpload.isEmpty()) { // read id from "File already uploaded under id:3" | |
| int idx = resultOfUpload.indexOf("id:"); | |
| if (idx > 0) { | |
| fileId = resultOfUpload.substring(idx+3); | |
| } | |
| } | |
| } else { | |
| MessageDialog.openInformation(shell, "Info", "LTL could not be uploaded to the VerificationServer.\nMaybe the VerificationServer is down."); | |
| } | |
| } return fileId; | |
| } | |
| protected void runValidation(final EObject validateElement) { | |
| //Set<Port> ports = getUmlPortsFromClass(Class validateElement); | |
| //RequestWriter.getPorts((ElementImpl) validateElement); // TODO temporary code | |
| // Current workaround. Verification server does not read LTL from the message, but from an uploaded file. | |
| String fileIdLtl = null; | |
| String ltl = RequestWriter.extractGuarantee((ElementImpl) validateElement); // Guarantees contain the list of LTL formulas | |
| int numberOfReqs = ltl.split("\n").length; | |
| fileIdLtl = uploadString(ltl); | |
| // Current workaround. Verification server does not read LTL from the message, but from an uploaded file. | |
| String fileIdIO = null; | |
| //ltl = RequestWriter.extractAssume((ElementImpl) validateElement); // Assumptions contain the list of inputs and outputs | |
| String[] inputPortsNames = RequestWriter.getInputPortsNames((ElementImpl) validateElement); | |
| String[] outputPortsNames = RequestWriter.getOutputPortsNames((ElementImpl) validateElement); | |
| String[] inputOutputPortsNames = RequestWriter.getInputOutputPortsNames((ElementImpl) validateElement); | |
| Set<String> signals = RequestWriter.extractSignalsFromLtl(ltl); | |
| String inputsOutputs = RequestWriter.extractInputsAndOutputs(signals, | |
| inputPortsNames, outputPortsNames, inputOutputPortsNames); | |
| fileIdIO = uploadString(inputsOutputs); | |
| //if (Request.example == null) { | |
| Request.setExample(fileIdLtl, fileIdIO, numberOfReqs); | |
| //} | |
| //Class cl = validateElement.getClass(); | |
| EList<Stereotype> stList = ((ClassImpl) validateElement).getAppliedStereotypes(); | |
| /*boolean isContract = false; | |
| String stName; | |
| for (Stereotype st : stList) { | |
| stName = st.getName(); | |
| if (stName.equals("Contract")) { | |
| isContract = true; | |
| } | |
| } */ | |
| Request msg = Request.example; | |
| Sender sender = new Sender(); | |
| HttpURLConnection conn; | |
| conn = sender.sendMessage(msg); | |
| String result = null; | |
| int idx = -2; | |
| if (conn != null) { | |
| Receiver receiver = new Receiver(); | |
| result = receiver.receive(conn); | |
| idx = result.indexOf("report n."); | |
| } | |
| ResultBrowser resultBrowser = null; // = new ResultBrowser(); | |
| try { | |
| resultBrowser = (ResultBrowser) PlatformUI.getWorkbench().getActiveWorkbenchWindow().getActivePage().showView("eu.hon.eclipse.vavmanager.resultbrowser"); | |
| resultBrowser.changeDocument(result); | |
| } catch (PartInitException e) { | |
| // TODO Auto-generated catch block | |
| e.printStackTrace(); | |
| } | |
| // Monitor the model checking. | |
| String jobId = ""; | |
| if (idx > 0) { | |
| jobId = result.substring(idx+9).trim(); | |
| if (jobId.trim().length() != 0) { | |
| Request.setMonitor(jobId); | |
| Request monitorMsg = Request.monitor; | |
| //sender = new Sender(); | |
| //conn = sender.sendMessage(monitorMsg); | |
| result = null; | |
| Boolean isFinished = false; | |
| //if (conn != null) { | |
| Receiver receiver = new Receiver(); | |
| idx = 0; // reset idx and use below as a counter | |
| waitingForResult: | |
| while (result == null || !isFinished) { | |
| conn = sender.sendMessage(monitorMsg); | |
| result = receiver.receive(conn); | |
| if (result.startsWith("null\n")) { | |
| if (result.length() >= 6) { | |
| result = result.substring(5); | |
| } | |
| } | |
| isFinished = result.contains("Verification finished."); | |
| if (resultBrowser != null) { | |
| if (!isFinished) { | |
| try { | |
| Thread.sleep(1000); | |
| resultBrowser.changeDocument("... verification is running. " + idx); | |
| } catch (Exception e) { | |
| e.printStackTrace(); | |
| } | |
| idx++; | |
| if (idx > 10) { | |
| resultBrowser.changeDocument("Time-out reached without verification result.\n\n===\n\n" + result); | |
| break waitingForResult; | |
| } | |
| } else { | |
| DocumentBuilderFactory domFactory = DocumentBuilderFactory.newInstance(); | |
| domFactory.setNamespaceAware(true); // never forget this and define xpath.setName | |
| try { | |
| DocumentBuilder builder = domFactory.newDocumentBuilder(); | |
| //result = "<data><employee><name>A</name><title>Manager</title></employee></data>"; | |
| // result = "<RDF>aaa</RDF>"; | |
| //result = "<rdf:RDF xmlns:rdf=\"http://www.w3.org/1999/02/22-rdf-syntax-ns#\">aaa</rdf:RDF>"; | |
| result = result.replace("&", "&"); | |
| InputSource inputSource = new InputSource(new StringReader(result)); | |
| Document dDoc = builder.parse(inputSource); | |
| XPath xpath = XPathFactory.newInstance().newXPath(); | |
| xpath.setNamespaceContext( new NamespaceContext() { | |
| public String getNamespaceURI(String prefix) { | |
| switch (prefix) { | |
| case "rdf": return "http://www.w3.org/1999/02/22-rdf-syntax-ns#"; | |
| case "rdfs": return "http://www.w3.org/2000/01/rdf-schema#"; | |
| case "owl": return "http://www.w3.org/2002/07/owl"; | |
| case "dcterms": return "http://purl.org/dc/terms/"; | |
| case "pm": return "http://open-services.net/ns/perfmon#"; | |
| case "ems": return "http://open-services.net/ns/ems#"; | |
| case "oslc_auto": return "http://open-services.net/ns/auto#"; | |
| default: return "unknown xmlns"; | |
| } | |
| } | |
| public String getPrefix(String strng) { | |
| return null; | |
| } | |
| @SuppressWarnings("rawtypes") | |
| public Iterator getPrefixes(String strng) { | |
| return null; | |
| } | |
| } | |
| ); | |
| // V budoucnu: | |
| // //oslc_auto:AutomationResult/oslc_auto:contribution/oslc_auto:ParameterInstance/rdf:value/oslc:result/oslc:message | |
| // oslc_auto:AutomationResult bude muset mapovat na konkretni Automation Plan a Request. | |
| // | |
| String str = (String) xpath.evaluate("//oslc_auto:AutomationResult/rdf:description[3]", dDoc); | |
| //Node node = (Node) xPath.evaluate("//rdf:description/child::title[contains(text(),'partVerResult')]/../ems:numericValue[text()]", dDoc, XPathConstants.STRING); | |
| if (str.length() >= 1) { | |
| result = str.trim(); | |
| } | |
| } catch (RuntimeException e) { | |
| e.printStackTrace(); | |
| } catch (Exception e) { | |
| e.printStackTrace(); | |
| } | |
| try { | |
| resultBrowser.changeDocument(result); | |
| } catch (Exception e) { | |
| e.printStackTrace(); | |
| } | |
| } | |
| } | |
| } | |
| //} | |
| } | |
| } | |
| } | |
| // private IdentityCommand manageVAndVCommand; | |
| // /** | |
| // * <pre> | |
| // * | |
| // * Returns the command to execute (to be implemented | |
| // * in children implementing this class) | |
| // * | |
| // * @return the command to execute | |
| // * | |
| // * </pre> | |
| // */ | |
| // @Override | |
| // protected Command getCommand() | |
| // { | |
| // String label = "Manage V&V"; | |
| // manageVAndVCommand = new IdentityCommand(label, Activator.PLUGIN_ID); | |
| // return manageVAndVCommand; | |
| // } | |
| } |