Commit 2e3e1577 authored by Sudeep Kanav's avatar Sudeep Kanav
Browse files

removed lazy result from the toolRunner

refs 3089
parent 8495fa8f
......@@ -39,7 +39,6 @@ import org.conqat.lib.commons.filesystem.FileSystemUtils;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.ocra.model.contract.Contract;
import org.fortiss.af3.ocra.textgen.OCRATextGenerator;
import org.fortiss.af3.tools.base.ILazyResult;
import org.fortiss.af3.tools.base.ToolRunnerBase;
import org.fortiss.af3.tools.base.UnknownLanguageFragmentException;
import org.fortiss.af3.tools.nusmv.model.NuSMVFile;
......@@ -57,12 +56,9 @@ import org.fortiss.af3.tools.nusmv.run.NuSMVRunner;
*/
public class OCRARunner extends ToolRunnerBase<Component, NuSMVResult> {
/**
* @throws UnknownLanguageFragmentException
* @throws ModelCheckingException
*/
public static NuSMVResult checkContractComposition(Component c, Contract con)
throws UnknownLanguageFragmentException, ModelCheckingException {
/** Performs the contract verification using OCRA refinement. */
public NuSMVResult checkContractComposition(Component c, Contract con)
throws ModelCheckingException {
try {
final File modelFile = materialiseModelFile(c);
final File cmdFile = materialiseScriptFile(modelFile, con);
......@@ -79,7 +75,7 @@ public class OCRARunner extends ToolRunnerBase<Component, NuSMVResult> {
}
/** */
public static NuSMVResult checkContractImplementation(Component c, Contract con, Module m)
public NuSMVResult checkContractImplementation(Component c, Contract con, Module m)
throws UnknownLanguageFragmentException, ModelCheckingException {
try {
final File modelFile = materialiseModelFile(c);
......@@ -116,15 +112,6 @@ public class OCRARunner extends ToolRunnerBase<Component, NuSMVResult> {
}
}
/** Returns the version string or the specified tool. */
public static String getToolVersionString(Tool tool) {
try {
return tool.testToolAvailability();
} catch(IOException | InterruptedException | ExecutionException e) {
return null;
}
}
/** Materialises the logical file into a physical file. */
private static File materialiseModelFile(Component c) throws IOException {
// TODO IMO there should be a function which just returns the file name to be created,
......@@ -200,65 +187,30 @@ public class OCRARunner extends ToolRunnerBase<Component, NuSMVResult> {
return commandFile;
}
/**
* Viable Tools for Model Checking with this class.
* Not public since a caller should NEVER EVER have to care about the inner workings.
* This is also not a differentiation in an inheritance-manner but a hard match of
* specifications with nuxmv being a total superset of nusmv. The whole sense of this
* differentiation is to not force nuxmv users to install nusmv.
*/
private static enum Tool {
/** NuSMV, command NuSMV.exe or nusmv */
ocra;
/** returns the commandline string to call the Tool */
String getToolCommand() {
return (ocra) + (isWindowsOperatingSystem() ? "-win64.exe" : "");
}
/**
* test the availability of the tool
*
* @return null if the tool is not available, otherwise tool + version
*/
String testToolAvailability() throws IOException, InterruptedException, ExecutionException {
// shouldn't getToolCommand respect the tool parameter?
Pair<String, String> outputs = smokeToolRunWithException(this.getToolCommand(), "-h");
if(outputs != null && outputs.getSecond().length() > 0) {
// help message goes to std::err and starts with *** This is NuSMV <version>
String helpMessage = outputs.getSecond();
int start = helpMessage.indexOf("ocra");
return this + " " + helpMessage.substring(start + 5, start + 11);
}
return null;
}
}
/** Calls NuSMV for a model and a commandFile and returns the output. */
private static List<String> callOCRA(File cmdFile) throws ModelCheckingException {
for(Tool t : Tool.values())
try {
String command = t.getToolCommand() + " -source " + cmdFile.getAbsolutePath();
info(plugin, "calling OCRA: " + command);
Process process = Runtime.getRuntime().exec(command);
List<Future<List<String>>> outputs =
Executors.newFixedThreadPool(2).invokeAll(
Arrays.asList(new StreamConsumer(process.getInputStream()),
new StreamConsumer(process.getErrorStream())));
// Should not wait at all since invokeAll waits for completion.
// But anyway, consistent way to get the exitvalue:
int exitvalue = process.waitFor();
if(exitvalue != 0)
throw new ModelCheckingException(outputs.get(1).get());
// get-justification: declared fixed size;
return outputs.get(0).get();
} catch(IOException | ExecutionException | InterruptedException e) {
continue;
}
private List<String> callOCRA(File cmdFile) throws ModelCheckingException {
// TODO try to put this in the Task
try {
String command = getToolCommand() + " -source " + cmdFile.getAbsolutePath();
info(plugin, "calling OCRA: " + command);
Process process = Runtime.getRuntime().exec(command);
List<Future<List<String>>> outputs =
Executors.newFixedThreadPool(2).invokeAll(
Arrays.asList(new StreamConsumer(process.getInputStream()),
new StreamConsumer(process.getErrorStream())));
// Should not wait at all since invokeAll waits for completion.
// But anyway, consistent way to get the exitvalue:
int exitvalue = process.waitFor();
if(exitvalue != 0)
throw new ModelCheckingException(outputs.get(1).get());
// get-justification: declared fixed size;
return outputs.get(0).get();
} catch(IOException | ExecutionException | InterruptedException e) {
e.printStackTrace();
}
throw new ModelCheckingException(
Arrays.asList("None of the tools could be invoked correctly"));
......@@ -266,19 +218,32 @@ public class OCRARunner extends ToolRunnerBase<Component, NuSMVResult> {
/** {@inheritDoc} */
@Override
public ILazyResult<NuSMVResult> runTool() throws Exception {
public NuSMVResult runTool() throws Exception {
return null;
}
/** {@inheritDoc} */
@Override
public String testToolAvailability() {
// shouldn't getToolCommand respect the tool parameter?
Pair<String, String> outputs = null;
try {
outputs = smokeToolRunWithException(this.getToolCommand(), "-h");
} catch(IOException | InterruptedException | ExecutionException e) {
e.printStackTrace();
}
if(outputs != null && outputs.getSecond().length() > 0) {
// Help message goes to std::err and starts with *** This is NuSMV <version>
String helpMessage = outputs.getSecond();
int start = helpMessage.indexOf("ocra");
return this + " " + helpMessage.substring(start + 5, start + 11);
}
return null;
}
/** {@inheritDoc} */
@Override
protected String getToolCommand() {
return null;
return "ocra" + (isWindowsOperatingSystem() ? "-win64.exe" : "");
}
}
......@@ -17,15 +17,11 @@ package org.fortiss.af3.specification.constraint;
import static org.fortiss.tooling.kernel.utils.ConstraintsUtils.createErrorStatus;
import java.util.ArrayList;
import java.util.List;
import org.fortiss.af3.component.model.Component;
import org.fortiss.af3.specification.model.TimedOutConstraintInstance;
import org.fortiss.af3.specification.utils.AnalysisConstraintsUtils;
import org.fortiss.af3.state.model.StateAutomaton;
import org.fortiss.af3.state.utils.StateAutomatonUtils;
import org.fortiss.af3.tools.base.ILazyResult;
import org.fortiss.tooling.kernel.model.constraints.ConstraintInstance;
import org.fortiss.tooling.kernel.model.constraints.IConstrained;
import org.fortiss.tooling.kernel.model.constraints.IConstraintInstanceStatus;
......@@ -38,9 +34,6 @@ import org.fortiss.tooling.kernel.utils.ConstraintsUtils;
*/
public abstract class StateAutomatonConstraintBase extends AbstractFormalVerificationConstraint {
/** Stores the latest analysis. Useful to allow cancellation. */
protected List<ILazyResult<?>> storedAnalyses = new ArrayList<ILazyResult<?>>();
/** {@inheritDoc} */
@Override
public IConstraintInstanceStatus verify(ConstraintInstance cstr) {
......@@ -67,17 +60,6 @@ public abstract class StateAutomatonConstraintBase extends AbstractFormalVerific
@Override
public void cancel(ConstraintInstance constraint) {
// Cancel previous analyses.
if(storedAnalyses != null) {
for(ILazyResult<?> analysis : storedAnalyses) {
if(analysis != null) {
try {
analysis.cancel();
} catch(NullPointerException e) {
// Nothing to do - the analysis has probably already been disposed meanwhile
}
}
}
}
}
/**
......
......@@ -74,8 +74,9 @@ public class OCRAAnalysis {
checkContractRefinement(Component c, Contract con)
throws UnknownLanguageFragmentException, ModelCheckingException {
OCRAAnalysis mca = new OCRAAnalysis(c);
OCRARunner ocraRunner = new OCRARunner();
NuSMVResult res =
OCRARunner.checkContractComposition(mca.getTransformedComponent(),
ocraRunner.checkContractComposition(mca.getTransformedComponent(),
mca.getTransformedContract(con));
if(res == null) {
System.out.println("OCRA Result is null;");
......@@ -90,8 +91,9 @@ public class OCRAAnalysis {
checkContractImplementation(Component c, Contract con)
throws UnknownLanguageFragmentException, ModelCheckingException {
OCRAAnalysis mca = new OCRAAnalysis(c);
OCRARunner ocraRunner = new OCRARunner();
NuSMVResult res =
OCRARunner.checkContractImplementation(mca.getTransformedComponent(),
ocraRunner.checkContractImplementation(mca.getTransformedComponent(),
mca.getTransformedContract(con), mca.getNuSMVModule());
return mca.constructResult(res);
}
......
GenericGCCDeploymentTestSuiteValidator.java 0f4f6c3e31e3bf4619155e1e2eff48e795234a35 GREEN
GenericGCCDeploymentTestSuiteValidator.java c53d79dd317b08c820304382d48e9eeaefc308b3 YELLOW
......@@ -162,14 +162,14 @@ public class GenericGCCDeploymentTestSuiteValidator implements ITestSuiteValidat
/** Runs the configure, make, and built program. */
private List<String> runToolChain() throws TimeoutException {
ConfigureRunner confRunner = new ConfigureRunner(targetLocation);
List<String> result = confRunner.runTool().get(TIMEOUT_IN_MILLISECONDS);
List<String> result = confRunner.runTooWithTimeout(TIMEOUT_IN_MILLISECONDS);
MakeRunner makeRunner = new MakeRunner(new File(targetLocation, "Makefile"));
result = makeRunner.runTool().get(TIMEOUT_IN_MILLISECONDS);
result = makeRunner.runTooWithTimeout(TIMEOUT_IN_MILLISECONDS);
File buildDir = new File(targetLocation, "LocalMachine/build");
BuiltProgramRunner localRunner = new BuiltProgramRunner("./LocalMachine.run", buildDir);
result = localRunner.runTool().get(TIMEOUT_IN_MILLISECONDS);
result = localRunner.runTooWithTimeout(TIMEOUT_IN_MILLISECONDS);
return result;
}
}
GenericGCCPlatformTestSuiteValidator.java 36731e2ed3c0a02afa3b28f1f63f8d5ffec41e46 GREEN
GenericGCCPlatformTestSuiteValidator.java 4d08266b9034c44971cb1d72949043a157cd6d64 YELLOW
HardwarePlatformTestSuiteValidator.java 65790fad3a0ae2214acfeada59743fab33b15220 GREEN
SourcePackageGenerator.java 7bfeafd7be7b7760ef0a801a394beeca0a215f01 GREEN
......@@ -162,18 +162,18 @@ public class GenericGCCPlatformTestSuiteValidator implements ITestSuiteValidator
/** Runs the configure, make, and built program. */
private List<String> runToolChain() throws TimeoutException {
ConfigureRunner confRunner = new ConfigureRunner(targetLocation);
List<String> result = confRunner.runTool().get(TIMEOUT_IN_MILLISECONDS);
List<String> result = confRunner.runTooWithTimeout(TIMEOUT_IN_MILLISECONDS);
for(String str : result)
LoggingUtils.info(Af3TestingActivator.getDefault(), str);
MakeRunner makeRunner = new MakeRunner(new File(targetLocation, "Makefile"));
result = makeRunner.runTool().get(TIMEOUT_IN_MILLISECONDS);
result = makeRunner.runTooWithTimeout(TIMEOUT_IN_MILLISECONDS);
for(String str : result)
LoggingUtils.info(Af3TestingActivator.getDefault(), str);
File buildDir = new File(targetLocation, "LocalMachine/build");
BuiltProgramRunner localRunner = new BuiltProgramRunner("./LocalMachine.run", buildDir);
result = localRunner.runTool().get(TIMEOUT_IN_MILLISECONDS);
result = localRunner.runTooWithTimeout(TIMEOUT_IN_MILLISECONDS);
for(String str : result)
LoggingUtils.info(Af3TestingActivator.getDefault(), str);
......
......@@ -26,7 +26,7 @@ package org.fortiss.af3.tools.base;
public interface IToolRunner<T> {
/** Runs the tool and returns the results. */
public ILazyResult<T> runTool() throws Exception;
public T runTool() throws Exception;
/**
* Tests the tool availability.
......
......@@ -59,8 +59,29 @@ public abstract class SimpleToolRunnerBase extends ToolRunnerBase<INamedElement,
/** {@inheritDoc} */
@Override
public ILazyResult<List<String>> runTool() {
return new LazyResultBase(new SimpleToolRunningTask());
public List<String> runTool() {
try {
return (new SimpleToolRunningTask()).call();
} catch(Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
return null;
}
/**
* Runs the tool with a timout in milliseconds. Same as the function runTool but with a timeout.
*/
public List<String> runTooWithTimeout(int timeOutInMilliseconds) {
try {
SimpleToolRunningTask task = new SimpleToolRunningTask();
task.timeoutInMilliseconds = timeOutInMilliseconds;
return task.call();
} catch(Exception e) {
// TODO Auto-generated catch block
e.printStackTrace();
}
return null;
}
/**
......@@ -69,8 +90,8 @@ public abstract class SimpleToolRunnerBase extends ToolRunnerBase<INamedElement,
private class SimpleToolRunningTask extends ToolRunningTask {
/** Constructor. */
SimpleToolRunningTask() {
super(SimpleToolRunnerBase.this.physicalFile, new SimpleResultBuilder(),
computeCmdArray());
super(SimpleToolRunnerBase.this.physicalFile.getParentFile(),
new SimpleResultBuilder(), computeCmdArray());
}
}
......
......@@ -17,7 +17,6 @@ package org.fortiss.af3.tools.base;
import static java.lang.String.join;
import static java.util.Arrays.asList;
import static java.util.concurrent.Executors.newFixedThreadPool;
import static java.util.stream.Collectors.toList;
import static org.fortiss.tooling.base.utils.SystemUtils.interpretProcessExitValues;
import static org.fortiss.tooling.kernel.utils.LoggingUtils.error;
......@@ -32,18 +31,15 @@ import java.io.IOException;
import java.io.InputStream;
import java.io.InputStreamReader;
import java.text.DecimalFormat;
import java.util.ArrayList;
import java.util.Arrays;
import java.util.List;
import java.util.Random;
import java.util.concurrent.Callable;
import java.util.concurrent.CancellationException;
import java.util.concurrent.ExecutionException;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.Future;
import java.util.concurrent.TimeUnit;
import java.util.concurrent.TimeoutException;
import org.conqat.lib.commons.collections.Pair;
import org.eclipse.core.runtime.IPath;
......@@ -172,12 +168,15 @@ public abstract class ToolRunnerBase<S extends INamedElement, T> implements IToo
* TODO(VA): improve comment. Why calling this a task?
*/
protected class ToolRunningTask implements Callable<T> {
// TODO not sure what is the purpose of physical file here. It is used to get the parent
// directory, i.e., the one in which the command is run. Other than that this file is
// deleted if it is the debug mode.
/** The process that runs the external tool. */
protected Process toolRunnerProcess;
/** The file that contains the textual tool code. */
protected File physicalFile;
/** The directory in which the command is run and in which the relevant files reside. */
protected File parentDirectory;
/** The result builder. */
protected IResultBuilder<T> resultBuilder;
......@@ -185,49 +184,20 @@ public abstract class ToolRunnerBase<S extends INamedElement, T> implements IToo
/** The command array for running the tool. */
protected String[] cmdArray;
/**
* Set timeout for the tool command. By default it is 0 which means tool is run without a
* timeout. If this value is greater than 0 only then the command is invoked with a timeout.
*/
protected int timeoutInMilliseconds = 0;
/** Constructor. */
protected ToolRunningTask(File physicalFile, IResultBuilder<T> resultBuilder,
protected ToolRunningTask(File parentDirectory, IResultBuilder<T> resultBuilder,
String[] cmdArray) {
this.physicalFile = physicalFile;
this.parentDirectory = parentDirectory;
this.resultBuilder = resultBuilder;
this.cmdArray = cmdArray;
}
/** Processes the results of the tool-run. */
protected T doProcessRunResults(List<String> errorLines, List<String> normalLines)
throws IOException, Exception {
String errorMessage = join("\n", errorLines);
if(errorMessage.length() > 0) {
throw new Exception(getToolCommand() + " running errors\n" + errorMessage);
}
if(normalLines.size() == 0) {
logRuntimeError();
throw new Exception("No result from running " + getToolCommand() + " :-( !!");
}
if(!DEBUG) {
physicalFile.delete();
}
return resultBuilder.buildResult(normalLines);
}
/** Logs a runtime error. */
protected void logRuntimeError() throws Exception {
String path = physicalFile.getAbsolutePath();
String errorMsg = "Error on running " + getToolCommand() + " on file: " + path;
error(plugin, errorMsg + " The file was not deleted and can be debugged!");
}
/** Destroys the running process. */
protected void destroyRunningProcess() {
if(toolRunnerProcess != null) {
toolRunnerProcess.destroy();
}
}
/** {@inheritDoc} */
@Override
public T call() throws Exception {
......@@ -235,21 +205,21 @@ public abstract class ToolRunnerBase<S extends INamedElement, T> implements IToo
// TODO Sudeep: Not happy with this list of consumers
String cmdStringForInfo =
"Running " + getToolCommand() + " " + Arrays.toString(cmdArray);
String filePathForInfo =
physicalFile.getName() + " in directory " + physicalFile.getParent();
info(plugin, cmdStringForInfo + " on file " + filePathForInfo + ".");
info(plugin, cmdStringForInfo + ".");
long initialTimeStamp = System.currentTimeMillis();
File parentFile = physicalFile.getParentFile();
toolRunnerProcess = Runtime.getRuntime().exec(cmdArray, null, parentFile);
toolRunnerProcess = Runtime.getRuntime().exec(cmdArray, null, parentDirectory);
List<StreamConsumer> resultStreams =
asList(new StreamConsumer(toolRunnerProcess.getInputStream()),
new StreamConsumer(toolRunnerProcess.getErrorStream()));
ExecutorService threadPool = Executors.newFixedThreadPool(2);
List<Future<List<String>>> outputs =
Executors.newFixedThreadPool(2).invokeAll(resultStreams);
(timeoutInMilliseconds > 0) ? threadPool.invokeAll(resultStreams,
timeoutInMilliseconds, TimeUnit.MILLISECONDS) : threadPool
.invokeAll(resultStreams);
int exitValue = toolRunnerProcess.waitFor();
......@@ -275,70 +245,36 @@ public abstract class ToolRunnerBase<S extends INamedElement, T> implements IToo
return doProcessRunResults(errlines, normallines);
}
}
/**
* Base class for a lazy result.
*
* TODO(VA) Improve comment. It just repeats the name of the class.
* What justifies the existence of the class?
*/
protected class LazyResultBase implements ILazyResult<T> {
/** Processes the results of the tool-run. */
protected T doProcessRunResults(List<String> errorLines, List<String> normalLines)
throws IOException, Exception {
/** The tasks for running the tool. */
private List<ToolRunningTask> toolRunningTasks;
String errorMessage = join("\n", errorLines);
if(errorMessage.length() > 0) {
throw new Exception(getToolCommand() + " running errors\n" + errorMessage);
}
/** Constructor. */
protected LazyResultBase(ToolRunningTask toolRunningTask) {
this.toolRunningTasks = new ArrayList<ToolRunningTask>();
this.toolRunningTasks.add(toolRunningTask);
}
if(normalLines.size() == 0) {
logRuntimeError();
throw new Exception("No result from running " + getToolCommand() + " :-( !!");
}
/** Constructor. */
protected LazyResultBase(List<ToolRunningTask> toolRunningTasks) {
this.toolRunningTasks = toolRunningTasks;
return resultBuilder.buildResult(normalLines);
}
/** {@inheritDoc} */
@Override
public T get(long timeoutInMilliseconds) throws TimeoutException {
ExecutorService executorService = newFixedThreadPool(this.toolRunningTasks.size());
try {
return executorService.invokeAny(this.toolRunningTasks, timeoutInMilliseconds,
TimeUnit.MILLISECONDS);
} catch(TimeoutException to) {
destroyRunningProcess();
throw to;
} catch(InterruptedException ie) {
// Cancelled by user
destroyRunningProcess();
throw new CancellationException();
} catch(ExecutionException exec) {
// No process finished successfully
exec.printStackTrace();
destroyRunningProcess();
error(plugin, "No process has finished successfully", exec);
throw new RuntimeException(exec);
} finally {
destroyRunningProcess();
executorService.shutdown();
}
/** Logs a runtime error. */
protected void logRuntimeError() throws Exception {
String path = parentDirectory.getAbsolutePath();
String errorMsg = "Error on running " + getToolCommand() + " on file: " + path;
error(plugin, errorMsg);
}
/** Destroys the running process. */
protected void destroyRunningProcess() {
this.cancel();
}
/** {@inheritDoc} */
@Override
public boolean cancel() {
for(ToolRunningTask t : toolRunningTasks) {
t.destroyRunningProcess();
if(toolRunnerProcess != null) {
toolRunnerProcess.destroy();
}
return true;
}
}
}
......@@ -41,11 +41,12 @@ import java.util.concurrent.ExecutionException;
import java.util.concurrent.Executors;
import java.util.concurrent.Future;
import java.util.function.Function;
import java.util.stream.Stream;