diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationAssertionPropertyCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationAssertionPropertyCommand.java index 78b81c2ed350b734abaa8b9ea7fd99fb6d747c01..8dd679444a652afa4664ae22ab95122cb0383129 100644 --- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationAssertionPropertyCommand.java +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationAssertionPropertyCommand.java @@ -115,12 +115,7 @@ public class CheckValidationAssertionPropertyCommand extends AbstractJobCommand @Override public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception { - String[] expression = new String[1]; // It will be filled by the method - commandExecuted = ocraExecService.executeValidationAssertionProperty(umlSelectedComponent, selectedInstantiatedArchitectureConfiguration,umlSelectedResource, - isDiscreteTime, usexTextValidation, showPopups, ossFilepath, resultFilePath, monitor, true, expression,contextList); - if(commandExecuted){ - conditions = createConditions(expression[0].split("#")); - } + } @@ -154,6 +149,14 @@ public class CheckValidationAssertionPropertyCommand extends AbstractJobCommand @Override public void execPostJobOperations(ExecutionEvent event, NullProgressMonitor nullProgressMonitor) throws Exception { + + String[] expression = new String[1]; // It will be filled by the method + commandExecuted = ocraExecService.executeValidationAssertionProperty(umlSelectedComponent, selectedInstantiatedArchitectureConfiguration,umlSelectedResource, + isDiscreteTime, usexTextValidation, showPopups, ossFilepath, resultFilePath, nullProgressMonitor, true, expression,contextList); + if(commandExecuted){ + conditions = createConditions(expression[0].split("#")); + } + if (commandExecuted) { // Store the result diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationContractPropertyCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationContractPropertyCommand.java index e5c124253140901aa60fcb318a243601f49fd293..5883db63e75e81ef574cd04b7c8e3618e4772765 100644 --- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationContractPropertyCommand.java +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/CheckValidationContractPropertyCommand.java @@ -112,12 +112,7 @@ public class CheckValidationContractPropertyCommand extends AbstractJobCommand { @Override public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception { - String[] expression = new String[1]; // It will be filled by the method - commandExecuted = ocraExecService.executeValidationContractProperty(umlSelectedComponent, selectedInstantiatedArchitectureConfiguration, umlSelectedResource, - isDiscreteTime, usexTextValidation, showPopups, ossFilepath, resultFilePath, monitor, true, expression,contextList); - if(commandExecuted){ - conditions = createConditions(expression[0].split("#")); - } + } private EList<String> createConditions(String[] expression) { @@ -145,7 +140,15 @@ public class CheckValidationContractPropertyCommand extends AbstractJobCommand { } @Override - public void execPostJobOperations(ExecutionEvent event, NullProgressMonitor nullProgressMonitor) throws Exception { + public void execPostJobOperations(ExecutionEvent event, NullProgressMonitor monitor) throws Exception { + + String[] expression = new String[1]; // It will be filled by the method + commandExecuted = ocraExecService.executeValidationContractProperty(umlSelectedComponent, selectedInstantiatedArchitectureConfiguration, umlSelectedResource, + isDiscreteTime, usexTextValidation, showPopups, ossFilepath, resultFilePath, monitor, true, expression,contextList); + if(commandExecuted){ + conditions = createConditions(expression[0].split("#")); + } + if (commandExecuted) { // Store the result diff --git a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ModelCheckingCommand.java b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ModelCheckingCommand.java index 00027530509aaeb223353cb46a693921d0ebf80e..236e0b4a20095f369070ba976f62b2581fe568f4 100644 --- a/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ModelCheckingCommand.java +++ b/plugins/contracts/org.polarsys.chess.contracts.verificationService/src/org/polarsys/chess/verificationService/ui/commands/ModelCheckingCommand.java @@ -87,6 +87,8 @@ public class ModelCheckingCommand extends AbstractJobCommand { private boolean commandExecuted; private EList<String> conditions; private List<AnalysisContextElement> contextList; + String generatedSmvFilePath; + boolean internalExecution = true; @Override public void execPreJobOperations(ExecutionEvent event, IProgressMonitor monitor) throws Exception { @@ -144,8 +146,7 @@ public class ModelCheckingCommand extends AbstractJobCommand { public void execJobCommand(ExecutionEvent event, IProgressMonitor monitor) throws Exception { if (!isProgrExec) { - final String generatedSmvFilePath; - final boolean internalExecution = true; + if (isLeafComponent(umlSelectedComponent)) { generatedSmvFilePath = smvExportService.exportSingleSmv(umlSelectedComponent, showPopups, @@ -163,13 +164,7 @@ public class ModelCheckingCommand extends AbstractJobCommand { logger.debug("createMonolithicSMV done"); } - // Compose the conditions - String[] expression = new String[1]; // It will be filled by the - // method - commandExecuted = nuXmvExecService.executeModelChecking(generatedSmvFilePath, resultFilePath, - event.getParameter("algorithm_type"), event.getParameter("check_type"), - event.getParameter("property"), isProgrExec, internalExecution, expression,contextList); - conditions = createConditions(expression[0].split("#")); + } } @@ -194,6 +189,14 @@ public class ModelCheckingCommand extends AbstractJobCommand { @Override public void execPostJobOperations(ExecutionEvent event, NullProgressMonitor nullProgressMonitor) throws Exception { + + // Compose the conditions + String[] expression = new String[1]; // It will be filled by the + // method + commandExecuted = nuXmvExecService.executeModelChecking(generatedSmvFilePath, resultFilePath, + event.getParameter("algorithm_type"), event.getParameter("check_type"), + event.getParameter("property"), isProgrExec, internalExecution, expression,contextList); + conditions = createConditions(expression[0].split("#")); // If requested to store the data, execute the command here, cannot be // called later if (commandExecuted) {