- added check contract composite implementation

eu.fbk.tools.adapter/eu.fbk.tools.adapter.core/src/main/java/eu/fbk/tools/adapter/ToolParameterConstants.java

@@ -45,4 +45,5 @@ public interface ToolParameterConstants
     final String PARAM_COMPONENTS_MAPPING     	= "componentsMapping";
     final String PARAM_DISABLE_PRINT  	        = "disablePrint";
     final String PARAM_OLD_MODEL_FORMAT        	= "oldModelFormat";
+    final String PARAM_SKIP_REFINEMENT_CHECK   	= "skipRefinementCheck";
 }

eu.fbk.tools.adapter/eu.fbk.tools.adapter.core/src/main/java/eu/fbk/tools/adapter/ocra/CheckContractCompositeImplementation.java

+/*******************************************************************************
+ * Copyright (c) 2017 Fondazione Bruno Kessler
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *******************************************************************************/
+package eu.fbk.tools.adapter.ocra;
+
+import java.io.File;
+import java.net.URI;
+import java.net.URISyntaxException;
+import java.util.ArrayList;
+import java.util.List;
+
+import org.apache.commons.lang3.StringUtils;
+import org.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import eu.fbk.tools.adapter.ToolCommand;
+import eu.fbk.tools.adapter.ToolFunctionParameter;
+import eu.fbk.tools.adapter.ToolParameterConstants;
+
+/**
+ * The Class CheckContractCompositeImplementation.
+ *
+ * @author braghieri
+ */
+public class CheckContractCompositeImplementation extends OcraFunction
+{
+	private static final Logger logger = LoggerFactory.getLogger(CheckContractCompositeImplementation.class);
+
+	public static final String FUNCTION_NAME = "ocra_check_composite_impl";
+
+	private URI componentsMapping;
+
+	private Boolean oldSmvFormat;
+
+	private Boolean skipRefinementCheck;
+
+	public CheckContractCompositeImplementation()
+	{
+		this(null, null);
+	}
+
+	public CheckContractCompositeImplementation(URI contractModel, URI componentsMapping)
+	{
+		super(FUNCTION_NAME);
+
+		setContractModel(contractModel);
+		setComponentsMapping(componentsMapping);
+	}
+
+	public URI getComponentsMapping() {
+		return componentsMapping;
+	}
+
+	public void setComponentsMapping(URI componentsMapping)
+	{
+		if( componentsMapping != null && componentsMapping.getScheme() == null )
+		{
+			this.componentsMapping = new File(componentsMapping.getPath()).toURI();
+		}
+		else
+		{
+			this.componentsMapping = componentsMapping;
+		}
+	}
+
+	public Boolean getOldSmvFormat() {
+		return oldSmvFormat;
+	}
+
+	public void setOldSmvFormat(Boolean oldSmvFormat) {
+		this.oldSmvFormat = oldSmvFormat;
+	}
+
+	public Boolean getSkipRefinementCheck() {
+		return skipRefinementCheck;
+	}
+
+	public void setSkipRefinementCheck(Boolean skipRefinementCheck) {
+		this.skipRefinementCheck = skipRefinementCheck;
+	}
+
+	@Override
+	protected void prepareCommands() {
+		final ToolCommand command = new ToolCommand(FUNCTION_NAME);
+		if( getContractModel() != null )
+		{
+			command.addArgument("-i", getLocalFile(getContractModel()));
+		}
+
+		if( getComponentsMapping() != null )
+		{
+			command.addArgument("-m", getLocalFile(getComponentsMapping()));
+		}
+
+		if( getAlgorithmType() != null )
+		{
+			command.addArgument("-a", getAlgorithmType().name());
+		}
+
+		if( getBoundLength() != null )
+		{
+			command.addArgument("-k",getBoundLength().toString());
+		}
+
+		if( skipRefinementCheck != null && skipRefinementCheck )
+		{
+			command.addArgument("-R");
+		}
+
+		if( !StringUtils.isBlank(getResultFile()) )
+		{
+			command.addArgument("-f", "xml");
+			command.addArgument("-o", getResultFile());
+		}
+
+		commands.add(new ToolCommand("set on_failure_script_quits"));
+
+		if( oldSmvFormat != null && oldSmvFormat )
+		{
+			commands.add(new ToolCommand("set ocra_old_smv_format"));
+		}
+
+		commands.add(command);
+		commands.add(new ToolCommand("quit"));
+	}
+
+	@Override
+	public List<ToolFunctionParameter> getParameters()
+	{
+		final List<ToolFunctionParameter> parameters = new ArrayList<ToolFunctionParameter>();
+
+		super.getParameters(parameters);
+
+		if( componentsMapping != null)
+		{
+			parameters.add(new ToolFunctionParameter(ToolParameterConstants.PARAM_COMPONENTS_MAPPING, componentsMapping.toString(), true));
+		}
+
+		if( oldSmvFormat != null )
+		{
+			parameters.add(new ToolFunctionParameter(ToolParameterConstants.PARAM_OLD_MODEL_FORMAT, oldSmvFormat.toString(), true));
+		}
+
+		if( skipRefinementCheck != null )
+		{
+			parameters.add(new ToolFunctionParameter(ToolParameterConstants.PARAM_SKIP_REFINEMENT_CHECK, skipRefinementCheck.toString(), true));
+		}
+
+		return parameters;
+	}
+
+	@Override
+	protected void setParameter(ToolFunctionParameter parameter)
+	{
+		switch( parameter.name )
+		{
+			case ToolParameterConstants.PARAM_COMPONENTS_MAPPING:
+				try
+				{
+					componentsMapping = new URI(parameter.value);
+				}
+				catch (URISyntaxException e)
+				{
+					logger.error(e.toString());
+				}
+				break;
+
+			case ToolParameterConstants.PARAM_OLD_MODEL_FORMAT:
+				try
+				{
+					oldSmvFormat = Boolean.valueOf(parameter.value);
+				}
+				catch (Exception e)
+				{
+					logger.error(e.toString());
+				}
+				break;
+
+			case ToolParameterConstants.PARAM_SKIP_REFINEMENT_CHECK:
+				try
+				{
+					skipRefinementCheck = Boolean.valueOf(parameter.value);
+				}
+				catch (Exception e)
+				{
+					logger.error(e.toString());
+				}
+				break;
+
+			default:
+				super.setParameter(parameter);
+				break;
+		}
+	}
+}

eu.fbk.tools.adapter/eu.fbk.tools.adapter.core/src/main/java/eu/fbk/tools/adapter/ocra/CheckContractImplementation.java

@@ -173,6 +173,11 @@ public class CheckContractImplementation extends OcraFunction
 			parameters.add(new ToolFunctionParameter(ToolParameterConstants.PARAM_CONTRACT_NAME, contractName));
 		}
 
+		if( oldSmvFormat != null )
+		{
+			parameters.add(new ToolFunctionParameter(ToolParameterConstants.PARAM_OLD_MODEL_FORMAT, oldSmvFormat.toString(), true));
+		}
+
 		return parameters;
 	}
 

eu.fbk.tools.adapter/eu.fbk.tools.adapter.ui/plugin.xml

@@ -186,6 +186,51 @@
                name="Result File Destination"
                optional="true">
          </commandParameter>
+      </command>
+      <command
+            categoryId="eu.fbk.tools.adapter"
+            defaultHandler="eu.fbk.tools.adapter.ui.commands.contract.CheckContractCompositeImplementationCommand"
+            id="eu.fbk.tools.adapter.ui.commands.contract.CheckContractCompositeImplementationCommand"
+            name="Check Contract Composite Implementation">
+         <commandParameter
+               id="contract_model"
+               name="ContractModel"
+               optional="false">
+         </commandParameter>
+         <commandParameter
+               id="map_file"
+               name="MapFile"
+               optional="false">
+         </commandParameter>
+         <commandParameter
+               id="time_model"
+               name="TimeModel"
+               optional="true"
+               values="discrete, hybrid">
+         </commandParameter>
+         <commandParameter
+               id="algorithm_type"
+               name="AlgorithmType"
+               optional="true"
+               values="auto, bdd, bmc, ic3">
+         </commandParameter>
+         <commandParameter
+               id="async_execution"
+               name="Asynchronous Execution"
+               optional="true"
+               values="true, false">
+         </commandParameter>
+         <commandParameter
+               id="old_model_format"
+               name="Old Model Format"
+               optional="true"
+               values="true, false">
+         </commandParameter>
+         <commandParameter
+               id="result_file"
+               name="Result File Destination"
+               optional="true">
+         </commandParameter>
       </command>
        <command
             categoryId="eu.fbk.tools.adapter"
@@ -301,6 +346,11 @@
                      commandId="eu.fbk.tools.adapter.ui.commands.contract.CheckContractImplementation"
                      icon="icons/contract_verification.png"
                      label="Check Implementation">
+               </command>
+               <command
+                     commandId="eu.fbk.tools.adapter.ui.commands.contract.CheckContractCompositeImplementationCommand"
+                     icon="icons/contract_verification.png"
+                     label="Check Composite Implementation">
                </command>
                 <command
                      commandId="eu.fbk.tools.adapter.ui.commands.contract.CheckValidationProperty"

eu.fbk.tools.adapter/eu.fbk.tools.adapter.ui/src/main/java/eu/fbk/tools/adapter/ui/commands/contract/CheckContractCompositeImplementationCommand.java

+
+package eu.fbk.tools.adapter.ui.commands.contract;
+
+import static org.eclipse.ui.PlatformUI.getWorkbench;
+
+import java.io.File;
+
+import org.apache.commons.lang3.StringUtils;
+import org.eclipse.core.commands.ExecutionEvent;
+import org.eclipse.core.commands.ExecutionException;
+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.slf4j.Logger;
+import org.slf4j.LoggerFactory;
+
+import eu.fbk.tools.adapter.ToolRunner;
+import eu.fbk.tools.adapter.ocra.CheckContractCompositeImplementation;
+import eu.fbk.tools.adapter.ocra.OcraFunction.AlgorithmType;
+import eu.fbk.tools.adapter.ui.dialog.contract.ContractCompositeImplementationParametersDialog;
+import eu.fbk.tools.adapter.ui.progress.ToolJob;
+
+
+/**
+ * The Class CheckContractCompositeImplementationCommand.
+ *
+ * @author braghieri
+ */
+public class CheckContractCompositeImplementationCommand extends AbstractCheckContractCommand
+{
+	private static final Logger logger = LoggerFactory.getLogger(CheckContractCompositeImplementationCommand.class);
+
+	private String mapFileName;
+
+	public CheckContractCompositeImplementationCommand()
+	{
+		super("Check Contract Composite Implementation");
+	}
+
+	@Override
+	public Object execute(ExecutionEvent event) throws ExecutionException
+	{
+		if( isOslcEnabled() )
+		{
+			displayError(getCommandDescription(), "Functionality over OSLC not implemented yet.");
+			logger.error("Unsupported functionality");
+			return null;
+		}
+
+		if( !preprocessEvent(event) )
+		{
+			return null;
+		}
+
+		mapFileName = event.getParameter("map_file");
+		if( StringUtils.isBlank(mapFileName) )
+		{
+			final Display display = getWorkbench().getDisplay();
+			final Runnable runnable = new Runnable()
+			{
+				@Override
+				public void run()
+				{
+					final Shell shell = display.getActiveShell();
+					final FileDialog fd = new FileDialog(shell, SWT.OPEN);
+					fd.setText("Choose the map file");
+
+					final String[] filterExt = {"*.txt"};
+					fd.setFilterExtensions(filterExt);
+
+					mapFileName = fd.open();
+				}
+			};
+
+			display.syncExec(runnable);
+		}
+
+		if( StringUtils.isBlank(mapFileName) )
+		{
+			displayError(getCommandDescription(), "Map file has not been specified, can't execute the command.");
+			logger.error("Missing map file");
+			return null;
+		}
+
+		// removes quotes if present in the file name
+		mapFileName = mapFileName.replace("\"", "");
+
+		if( !new File(mapFileName).exists() )
+		{
+			displayError(getCommandDescription(), "Component to model mapping file not exists, can't execute the command.");
+			logger.error("Component to model mapping file " + mapFileName + " not exists");
+			return false;
+		}
+
+		logger.debug("Set component to model mapping filename to " + mapFileName);
+
+
+		final CheckContractCompositeImplementation function = new CheckContractCompositeImplementation(stringToURI(contractFileName), stringToURI(mapFileName));
+
+		function.setTimeModel(timeModel);
+
+		final String algorithmType = event.getParameter("algorithm_type");
+		if( !StringUtils.isBlank(algorithmType) )
+		{
+			try
+			{
+				function.setAlgorithmType(AlgorithmType.valueOf(algorithmType));
+			}
+			catch (Exception e)
+			{
+				displayError(getCommandDescription(), "Invalid algorithm type parameter value, can't execute the command.");
+				logger.error("Invalid algorithm type parameter value: " + algorithmType);
+				return null;
+			}
+
+			// for debug purpose
+			logger.debug("Set algorithm type to " + function.getAlgorithmType().name());
+		}
+
+		final String oldModelFormat = event.getParameter("old_model_format");
+		if( !StringUtils.isBlank(oldModelFormat) )
+		{
+			try
+			{
+				function.setOldSmvFormat(Boolean.valueOf(oldModelFormat));
+			}
+			catch (Exception e)
+			{
+				logger.error("Invalid old model parameter value: " + oldModelFormat);
+			}
+		}
+
+		function.setBoundLength(10);
+
+		if( isDevelopmentModeEnabled() )
+		{
+			final Display display = getWorkbench().getDisplay();
+			final Runnable runnable = new Runnable()
+			{
+				@Override
+				public void run()
+				{
+					final Shell shell = display.getActiveShell();
+					final ContractCompositeImplementationParametersDialog dialog = new ContractCompositeImplementationParametersDialog(shell, function, asyncExecution);
+
+					dialog.open();
+
+					if( dialog.goAhead() )
+					{
+						function.setTimeModel(dialog.getTimeModel());
+						function.setAlgorithmType(dialog.getAlgorithmType());
+						function.setBoundLength(dialog.getBound());
+						function.setOldSmvFormat(dialog.getOldSmvFormat());
+
+						asyncExecution = dialog.getAsyncExecution();
+					}
+				}
+			};
+
+			display.syncExec(runnable);
+		}
+
+		final ToolRunner runner = prepareRunner(function);
+
+		if( asyncExecution != null )
+		{
+			if( asyncExecution && !runner.supportAsynchronousExecution() )
+			{
+				displayError(getCommandDescription(), "Asynchronous execution is not supported");
+				return null;
+			}
+
+			runner.setAsynchronousExecution(asyncExecution);
+		}
+
+		if( extResultFile != null )
+		{
+			runner.setExtResultFile(extResultFile);
+		}
+
+		final ToolJob job = new ToolJob(getCommandDescription(), runner);
+
+		job.setUser(true);
+		job.schedule();
+
+		return null;
+	}
+}

eu.fbk.tools.adapter/eu.fbk.tools.adapter.ui/src/main/java/eu/fbk/tools/adapter/ui/dialog/contract/ContractCompositeImplementationParametersDialog.java

+/*******************************************************************************
+ * Copyright (c) 2013-2015 Fondazione Bruno Kessler
+ *
+ * Licensed under the Apache License, Version 2.0 (the "License");
+ * you may not use this file except in compliance with the License.
+ * You may obtain a copy of the License at
+ *
+ * http://www.apache.org/licenses/LICENSE-2.0
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and
+ * limitations under the License.
+ *
+ *******************************************************************************/
+package eu.fbk.tools.adapter.ui.dialog.contract;
+
+import org.eclipse.jface.dialogs.Dialog;
+import org.eclipse.jface.dialogs.IDialogConstants;
+import org.eclipse.swt.SWT;
+import org.eclipse.swt.graphics.Point;
+import org.eclipse.swt.layout.GridData;
+import org.eclipse.swt.layout.GridLayout;
+import org.eclipse.swt.widgets.Button;
+import org.eclipse.swt.widgets.Combo;
+import org.eclipse.swt.widgets.Composite;
+import org.eclipse.swt.widgets.Control;
+import org.eclipse.swt.widgets.Label;
+import org.eclipse.swt.widgets.Shell;
+import org.eclipse.swt.widgets.Spinner;
+
+import eu.fbk.tools.adapter.ocra.CheckContractCompositeImplementation;
+import eu.fbk.tools.adapter.ocra.OcraFunction.AlgorithmType;
+import eu.fbk.tools.adapter.ocra.OcraFunction.TimeModel;
+
+/**
+ * The Class ContractRefinementParametersDialog.
+ *
+ * @author braghieri
+ */
+public class ContractCompositeImplementationParametersDialog extends Dialog {
+
+	private Combo   timeModelCombo;
+	private Combo   algorithmTypeCombo;
+	private Spinner boundSpinner;
+	private Button  oldSmvFormatCheckBox;
+	private Button  asyncCheckBox;
+
+	private TimeModel timeModel = TimeModel.discrete;
+	private AlgorithmType algorithmType;
+	private Integer bound;
+	private Boolean oldSmvFormat = false;
+	private Boolean asyncExecution = false;
+
+	private String [] timeModels = {TimeModel.discrete.name(), TimeModel.hybrid.name()};
+	private String [] algorithmTypes = {"", "auto", "bdd", "bmc","ic3"};
+
+	/** The go ahead. */
+	private boolean goAhead = false;
+
+	/**
+	 * Create the dialog.
+	 *
+	 * @param parentShell
+	 */
+	public ContractCompositeImplementationParametersDialog(Shell parentShell)
+	{
+		super(parentShell);