Commit 0fa2871a authored by Jonathan Shahen's avatar Jonathan Shahen

Moved to Globals repo

parent 2019dfa0
/**
* The MIT License
*
* Copyright (c) 2010 Karthick Jayaraman
*
* Permission is hereby granted, free of charge, to any person obtaining a copy
* of this software and associated documentation files (the "Software"), to deal
* in the Software without restriction, including without limitation the rights
* to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
* copies of the Software, and to permit persons to whom the Software is
* furnished to do so, subject to the following conditions:
*
* The above copyright notice and this permission notice shall be included in
* all copies or substantial portions of the Software.
*
* THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
* IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
* FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
* AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
* LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
* OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
* THE SOFTWARE.
*/
package mohawk.nusmv;
import java.io.*;
import java.nio.file.*;
import java.util.Arrays;
import java.util.List;
import java.util.logging.Logger;
/**
* @author kjayaram
*
* Class Name : NuSMV
*
* This class declares a
*
*/
public class NuSMV {
public final static Logger logger = Logger.getLogger("mohawk");
public static Process execProcess = null;
/**
*
*/
public NuSMV() {
}
// Function to call the symbolic model checker
// Takes the NuSMV code as input
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(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
// Returns TRUE is the QUERY is reachable, FALSE if it is unreachable
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
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(strLine + "\n");
System.out.print('.');
}
System.out.println("Done Reading\n");
System.out.println("################### NuSMV Output ###################");
System.out.println(_lastOutput.toString());
System.out.println("################### NuSMV Output ###################");
execProcess.waitFor();
try {
Path nusmvLog = Paths.get("latestNuSMVOutput.txt");
Files.write(nusmvLog, _lastOutput.toString().getBytes());
} catch (Exception e) {
// do not send this error up
System.out.println("[ERROR] Failed to write out the NuSMV log");
}
if (_lastOutput.toString().indexOf("= FALSE is false") != -1) { return true; }
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 = "";
// Run the NuSMV engine
Process execProcess = rt.exec(commands);
execProcess.getOutputStream().write(smvmodel.getBytes());
execProcess.getOutputStream().flush();
execProcess.getOutputStream().close();
BufferedReader bufread = new BufferedReader(new InputStreamReader(execProcess.getInputStream()));
BufferedReader bufread_err = new BufferedReader(new InputStreamReader(execProcess.getErrorStream()));
String strLine = null;
while ((strLine = bufread.readLine()) != null) {
strOutput = strOutput + strLine + "\n";
}
System.out.println(strOutput);
String strLine_err = "";
while ((strLine = bufread_err.readLine()) != null) {
strLine_err = strLine_err + strLine + "\n";
}
System.out.println("------------------ERROR Buffer------------------");
System.out.println(strLine_err);
System.out.println("------------------ERROR Buffer------------------");
if (strOutput.indexOf("false") != -1)
return true;
return false;
}
}
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