Skip to content
Snippets Groups Projects
Commit 5a4211c5 authored by Alberto Debiasi's avatar Alberto Debiasi
Browse files

added CompositeContractImplementation and ModelChecking commands 


Change-Id: Ib66c9b4a73352fee6a470d98d380e2561b4023d4
Signed-off-by: default avatarAlberto Debiasi <adebiasi@fbk.eu>
parent fea4ef64
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 92 additions and 15 deletions
plugins/contracts/org.polarsys.chess.contracts.verificationService/plugin.xml
+ 2
− 2
View file @ 5a4211c5
......@@ -121,7 +121,7 @@
<menu
label="//Debug Validation">
<command
commandId="org.polarsys.chess.verificationService.commands.debug.ModelCheckingOnFileCommand"
commandId="org.polarsys.chess.verificationService.commands.debug.CheckValidationPropertyOnFileCommand"
style="push">
</command>
</menu>
......@@ -140,7 +140,7 @@
style="push">
</command>
<command
commandId="org.polarsys.chess.verificationService.commands.debug.CheckValidationPropertyOnFileCommand"
commandId="org.polarsys.chess.verificationService.commands.debug.ModelCheckingOnFileCommand"
style="push">
</command>
</menu>
......
plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/CompositeContractImplementationCommand.java 0 → 100644
+ 58
− 0
View file @ 5a4211c5
package org.polarsys.chess.verificationService.commands;
import java.util.HashMap;
import org.eclipse.core.commands.ExecutionEvent;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.emf.ecore.resource.Resource;
import org.eclipse.uml2.uml.Class;
import org.polarsys.chess.service.internal.model.ChessSystemModel;
import org.polarsys.chess.service.utils.SelectionUtil;
import org.polarsys.chess.smvExport.services.SmvExportService;
import eu.fbk.eclipse.standardtools.ExecOcraCommands.services.OCRAExecService;
import eu.fbk.eclipse.standardtools.commands.AbstractJobCommand;
import eu.fbk.eclipse.standardtools.dialogs.MessageTimeModelDialog;
import eu.fbk.eclipse.standardtools.nuXmvService.utils.NuXmvDirectoryUtil;
import eu.fbk.eclipse.standardtools.utils.OCRADirectoryUtil;
public class CompositeContractImplementationCommand extends AbstractJobCommand {
private OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
private SelectionUtil selectionUtil = SelectionUtil.getInstance();
private SmvExportService smvExportService = SmvExportService.getInstance();
private OCRADirectoryUtil ocraDirectoryUtil = OCRADirectoryUtil.getInstance();
private NuXmvDirectoryUtil nuXmvDirectoryUtil = NuXmvDirectoryUtil.getInstance();
public CompositeContractImplementationCommand() {
super("Check Compositional Contract Implementation");
}
private Class umlSelectedComponent;
private Resource umlSelectedResource;
private boolean isDiscreteTime;
private boolean showPopups;
private String smvMapFilepath;
private String smvFilePath;
private String resultFilePath;
@Override
public void execPreJobOperations(ExecutionEvent event,IProgressMonitor monitor) throws Exception {
umlSelectedComponent = selectionUtil.getUmlComponentFromSelectedObject(event);
umlSelectedResource = umlSelectedComponent.eResource();
isDiscreteTime = MessageTimeModelDialog.openQuestion();
showPopups = true;
smvMapFilepath = ocraDirectoryUtil.getSmvMapFilePath();
smvFilePath = nuXmvDirectoryUtil.getSmvFileDirectory();
resultFilePath = ocraDirectoryUtil.getCommandCheckImplementationResultPath(umlSelectedComponent.getName());
}
@Override
public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
HashMap<String,String> smvPathComponentNameMap = smvExportService.exportSmv( umlSelectedComponent,showPopups,smvFilePath, monitor);
ocraExecService.executeCheckCompositeContractImplementation(umlSelectedComponent,umlSelectedResource, smvPathComponentNameMap, isDiscreteTime,showPopups,smvMapFilepath,resultFilePath,monitor);
}
}
plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ContractImplementationCommand.java
+ 1
− 1
View file @ 5a4211c5
......@@ -55,7 +55,7 @@ public class ContractImplementationCommand extends AbstractJobCommand {
isDiscreteTime = MessageTimeModelDialog.openQuestion();
showPopups = true;
ossFilepath = ocraDirectoryUtil.getOSSFilePath();
smvFilePath = nuXmvDirectoryUtil.getSmvFilePath();
smvFilePath = nuXmvDirectoryUtil.getSmvFileDirectory();
resultFilePath = ocraDirectoryUtil.getCommandCheckImplementationResultPath(umlSelectedComponent.getName());
}
......
plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/ModelCheckingCommand.java
+ 27
− 8
View file @ 5a4211c5
......@@ -11,18 +11,23 @@
package org.polarsys.chess.verificationService.commands;
import java.io.File;
import java.util.HashMap;
import org.eclipse.core.commands.ExecutionEvent;
import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.emf.ecore.resource.Resource;
import org.eclipse.uml2.uml.Class;
import org.polarsys.chess.service.internal.model.ChessSystemModel;
import org.polarsys.chess.service.utils.SelectionUtil;
import org.polarsys.chess.smvExport.services.SmvExportService;
import eu.fbk.eclipse.standardtools.ExecOcraCommands.services.OCRAExecService;
//import org.polarsys.chess.verificationService.services.SmvExportService;
import eu.fbk.eclipse.standardtools.commands.AbstractJobCommand;
import eu.fbk.eclipse.standardtools.nuXmvService.services.NuXmvService;
import eu.fbk.eclipse.standardtools.dialogs.MessageTimeModelDialog;
import eu.fbk.eclipse.standardtools.nuXmvService.services.NuXmvExecService;
import eu.fbk.eclipse.standardtools.nuXmvService.utils.NuXmvDirectoryUtil;
import eu.fbk.eclipse.standardtools.utils.OCRADirectoryUtil;
/**
*
......@@ -32,8 +37,11 @@ public class ModelCheckingCommand extends AbstractJobCommand {
private SelectionUtil selectionUtil = SelectionUtil.getInstance();
private SmvExportService smvExportService = SmvExportService.getInstance();
private NuXmvService nuXmvService = NuXmvService.getInstance();
private NuXmvExecService nuXmvExecService = NuXmvExecService.getInstance();
private static NuXmvDirectoryUtil nuXmvDirectoryUtil = NuXmvDirectoryUtil.getInstance();
private OCRADirectoryUtil ocraDirectoryUtil = OCRADirectoryUtil.getInstance();
private OCRAExecService ocraExecService = OCRAExecService.getInstance(ChessSystemModel.getInstance());
public ModelCheckingCommand() {
super("Model Checking");
......@@ -42,14 +50,22 @@ public class ModelCheckingCommand extends AbstractJobCommand {
private Class umlSelectedComponent;
private boolean showPopups;
private String smvFilePath;
private boolean isDiscreteTime;
private String monolithicSMVFilePath;
private String resultFilePath;
private String smvMapFilepath;
private Resource umlSelectedResource;
@Override
public void execPreJobOperations(ExecutionEvent event,IProgressMonitor monitor) throws Exception {
umlSelectedComponent = selectionUtil.getUmlComponentFromSelectedObject(event);
umlSelectedResource = umlSelectedComponent.eResource();
showPopups = true;
smvFilePath = nuXmvDirectoryUtil.getSmvFilePath();
resultFilePath = nuXmvDirectoryUtil.getCommandModelCheckingResultPath(umlSelectedComponent.getName());
isDiscreteTime = MessageTimeModelDialog.openQuestion();
smvFilePath = nuXmvDirectoryUtil.getSmvFileDirectory();
monolithicSMVFilePath = nuXmvDirectoryUtil.getMonolithicSMVFilePath(umlSelectedComponent.getName());
resultFilePath = nuXmvDirectoryUtil.getModelCheckingResultPath(umlSelectedComponent.getName());
smvMapFilepath = ocraDirectoryUtil.getSmvMapFilePath();
}
......@@ -57,9 +73,12 @@ public class ModelCheckingCommand extends AbstractJobCommand {
@Override
public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception {
File smvOutput = smvExportService.exportSingleSmv( umlSelectedComponent,showPopups,smvFilePath, monitor);
nuXmvService.executeModelChecking(smvOutput,resultFilePath);
//File smvOutput = smvExportService.exportSingleSmv( umlSelectedComponent,showPopups,smvFilePath, monitor);
//nuXmvExecService.executeModelChecking(smvOutput,resultFilePath);
}
HashMap<String,String> smvPathComponentNameMap = smvExportService.exportSmv( umlSelectedComponent,showPopups,smvFilePath, monitor);
ocraExecService.createMonolithicSMV(umlSelectedComponent, umlSelectedResource, smvPathComponentNameMap, isDiscreteTime, showPopups, smvMapFilepath, monolithicSMVFilePath, monitor);
nuXmvExecService.executeModelChecking(new File(monolithicSMVFilePath),resultFilePath);
}
}
plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/commands/debug/ModelCheckingOnFileCommand.java
+ 4
− 4
View file @ 5a4211c5
......@@ -18,7 +18,7 @@ import org.eclipse.core.runtime.IProgressMonitor;
import eu.fbk.eclipse.standardtools.commands.AbstractJobCommand;
import eu.fbk.eclipse.standardtools.nuXmvService.dialogs.NuXmvParametersDialog;
import eu.fbk.eclipse.standardtools.nuXmvService.services.NuXmvService;
import eu.fbk.eclipse.standardtools.nuXmvService.services.NuXmvExecService;
import eu.fbk.eclipse.standardtools.nuXmvService.utils.NuXmvDialogUtil;
import eu.fbk.eclipse.standardtools.nuXmvService.utils.NuXmvDirectoryUtil;
......@@ -29,7 +29,7 @@ import eu.fbk.eclipse.standardtools.nuXmvService.utils.NuXmvDirectoryUtil;
public class ModelCheckingOnFileCommand extends AbstractJobCommand {
private NuXmvService nuXmvService = NuXmvService.getInstance();
private NuXmvExecService nuXmvService = NuXmvExecService.getInstance();
private NuXmvDialogUtil nuXmvDialogUtil = NuXmvDialogUtil.getInstance();
private NuXmvDirectoryUtil nuXmvDirectoryUtil = NuXmvDirectoryUtil.getInstance();
......@@ -66,8 +66,8 @@ public class ModelCheckingOnFileCommand extends AbstractJobCommand {
if (goAhead) {
File smvFile = nuXmvDialogUtil.getSmvFileFromFileDialog(nuXmvDirectoryUtil.getSmvFilePath());
String resultFilePath = nuXmvDirectoryUtil.getCommandModelCheckingResultPath(smvFile.getName());
File smvFile = nuXmvDialogUtil.getSmvFileFromFileDialog(nuXmvDirectoryUtil.getSmvFileDirectory());
String resultFilePath = nuXmvDirectoryUtil.getModelCheckingResultPath(smvFile.getName());
nuXmvService.modelCheckingCommand(smvFile, property, alg_type, check_type,resultFilePath);
}
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment

Copyright © Eclipse Foundation, Inc. All Rights Reserved.     Privacy Policy | Terms of Use | Copyright Agent