Commit a84bfcc4 authored by Jonathan Shahen's avatar Jonathan Shahen
Browse files

Fixed errors but still unable to complete positive3.mohawk and...

Fixed errors but still unable to complete positive3.mohawk and positive4.mohawk (They TIMEOUT), this problem lies within Mohawk 2.0
parent 618652ef
......@@ -27,6 +27,8 @@ package mohawk.nusmv;
import java.io.BufferedReader;
import java.io.IOException;
import java.io.InputStreamReader;
import java.util.Arrays;
import java.util.List;
/**
* @author kjayaram
......@@ -46,21 +48,60 @@ public class NuSMV {
// Function to call the symbolic model checker
// Takes the NuSMV code as input
public static Boolean SMC(String smvmodel) throws IOException {
String commands = "NuSMV"; // Commandline to invoke the NuSMV symbolic
// model checker.
public static Boolean SMC(String smvmodel) throws IOException, InterruptedException {
List<String> commands = Arrays.asList("NuSMV"); // Commandline to invoke the NuSMV symbolic model checker.
return RunNuSMV(commands, smvmodel);
}
// Call the NuSMV symbolic model checker
// The bound and SMV model are passed as inputs
public static Boolean BMC(int bound, String smvmodel) throws IOException {
String commands = String.format("NuSMV -bmc -bmc_length %d", bound);
public static Boolean BMC(Integer bound, String smvmodel) throws IOException, InterruptedException {
List<String> commands = Arrays.asList("NuSMV", "-bmc", "-bmc_length", bound.toString());
return RunNuSMV(commands, smvmodel);
}
// Run the NuSMV engine using the specified command and input
private static Boolean RunNuSMV(String commands, String smvmodel) throws IOException {
private static Boolean RunNuSMV(List<String> commands, String smvmodel) throws IOException, InterruptedException {
// Run the NuSMV engine
ProcessBuilder builder = new ProcessBuilder(commands);
builder.redirectErrorStream(true); // combine the Error into the normal stream
Process execProcess = builder.start();
execProcess.getOutputStream().write(smvmodel.getBytes());
execProcess.getOutputStream().flush();
execProcess.getOutputStream().close();
BufferedReader bufread = new BufferedReader(new InputStreamReader(execProcess.getInputStream()));
String strLine = null;
StringBuilder _lastOutput = new StringBuilder();
System.out.print("Reading Lines");
while ((strLine = bufread.readLine()) != null) {
_lastOutput.append("\t" + strLine + "\n");
System.out.print('.');
}
System.out.println("Done Reading\n");
System.out.println(_lastOutput.toString());
execProcess.waitFor();
if (_lastOutput.toString().indexOf("false") != -1) { return true; }
return false;
}
public static Boolean BMC_old(int bound, String smvmodel) throws IOException, InterruptedException {
String commands = String.format("NuSMV -bmc -bmc_length %d", bound);
return RunNuSMV_old(commands, smvmodel);
}
public static Boolean SMC_old(String smvmodel) throws IOException {
String commands = "NuSMV"; // Commandline to invoke the NuSMV symbolic model checker.
return RunNuSMV_old(commands, smvmodel);
}
// Run the NuSMV engine using the specified command and input
private static Boolean RunNuSMV_old(String commands, String smvmodel) throws IOException {
Runtime rt = Runtime.getRuntime();
String strOutput = "";
......
Markdown is supported
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