Commit bd498ad7 authored by Jonathan Shahen's avatar Jonathan Shahen

Small refinements but an error still exists when invoking NuSMV

parent deab72b6
......@@ -213,10 +213,11 @@ public class MohawkMain {
} else {
logger.fine("[OPTION] Using a specific SMV File: "
+ cmd.getOptionValue("smvfile"));
// SMV_helper.addSpecFile(cmd.getOptionValue("smvfile"));
SMV_helper.smvFilepath = cmd.getOptionValue("smvfile");
}
} else {
logger.fine("[OPTION] No SMV File included");
logger.fine("[OPTION] No SMV Filename included, saving file under: "
+ SMV_helper.smvFilepath);
}
// Grab the SPEC file
......
......@@ -31,9 +31,9 @@ import java.io.InputStreamReader;
/**
* @author kjayaram
*
* Class Name : NuSMV
* Class Name : NuSMV
*
* This class declares a
* This class declares a
*
*/
public class NuSMV {
......@@ -45,28 +45,26 @@ public class NuSMV {
// TODO Auto-generated constructor stub
}
// Function to call the symbolic model checker
// 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.
return RunNuSMV(commands, smvmodel);
public static Boolean SMC(String smvmodel) throws IOException {
String commands = "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(int bound, String smvmodel) throws IOException {
String commands = String.format("NuSMV -bmc -bmc_length %d", bound);
return RunNuSMV(commands, smvmodel);
}
// Run the NuSMV engine using the specified command and input
private static Boolean RunNuSMV(String commands, String smvmodel) throws IOException
{
Runtime rt = Runtime.getRuntime();
String strOutput = null;
private static Boolean RunNuSMV(String commands, String smvmodel)
throws IOException {
Runtime rt = Runtime.getRuntime();
String strOutput = "";
// Run the NuSMV engine
Process execProcess = rt.exec(commands);
......@@ -74,19 +72,27 @@ public class NuSMV {
execProcess.getOutputStream().flush();
execProcess.getOutputStream().close();
BufferedReader bufread = new BufferedReader(new InputStreamReader(execProcess
.getInputStream()));
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) {
if (strOutput == null)
strOutput = strLine;
else
strOutput = strOutput + "\n" + strLine;
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;
......
......@@ -136,7 +136,7 @@ public class RBAC2SMV {
+ " written to " + nusmvfile);
}
private static int getCASize(Map<String, Vector<CAEntry>> mCA) {
public static int getCASize(Map<String, Vector<CAEntry>> mCA) {
int size = 0;
Collection<Vector<CAEntry>> carules = mCA.values();
Iterator<Vector<CAEntry>> iterator = carules.iterator();
......
......@@ -21,8 +21,6 @@ import mohawk.collections.RoleDepTree;
*/
public class RolesAbsRefine {
public RolesAbsRefine(RBACInstance inRbac) {
mode = NuSMVMode.BMC; // Default mode is BMC
......@@ -37,8 +35,10 @@ public class RolesAbsRefine {
buildTree();
}
public void setMode(NuSMVMode curmode) { this.mode = curmode; }
public void setMode(NuSMVMode curmode) {
this.mode = curmode;
}
private void firstabstraction() {
Set<String> sFirstSetRoles = new HashSet<String>();
......@@ -237,14 +237,14 @@ public class RolesAbsRefine {
for (int i : UnSlicedCond.keySet()) {
if (mMapping.containsKey(i)) {
int iNewIndex = mMapping.get(i); // getNewRoleIndex(i);
SlicedCond.addConditional(iNewIndex, UnSlicedCond
.getConditional(i));
SlicedCond.addConditional(iNewIndex,
UnSlicedCond.getConditional(i));
}
}
}
CAEntry newCAE = new CAEntry(cae.getAdminRole(), SlicedCond, cae
.getRole());
CAEntry newCAE = new CAEntry(cae.getAdminRole(), SlicedCond,
cae.getRole());
return newCAE;
}
......@@ -256,8 +256,8 @@ public class RolesAbsRefine {
for (int i = 0; i < nextsetroles.size(); i++) {
String strRole = nextsetroles.get(i);
mMapping.put(allroles.indexOf(strRole), nextsetroles
.indexOf(strRole));
mMapping.put(allroles.indexOf(strRole),
nextsetroles.indexOf(strRole));
}
}
......@@ -314,27 +314,27 @@ public class RolesAbsRefine {
WriteRBACSpec writer = new WriteRBACSpec("rbac.st");
try {
writer.Write2File(nextinstance, "rbacinstancefile"
+ fileno);
writer.Write2File(nextinstance, "rbacinstancefile" + fileno);
} catch (IOException e1) {
// TODO Auto-generated catch block
e1.printStackTrace();
}
// NuSMV bmc mode
CalculateDiameter diameter = new CalculateDiameter();
CalculateDiameter diameter = new CalculateDiameter();
int bound = diameter.GetDiameter(nextinstance);
System.out.println(String.format("Estimate Diameter - No of Roles %d Diameter %d",nextinstance.getNumRoles(), bound));
System.out.println(String.format(
"Estimate Diameter - No of Roles %d Diameter %d",
nextinstance.getNumRoles(), bound));
// NuSMV bmc
Boolean result;
if(mode == NuSMVMode.BMC)
if (mode == NuSMVMode.BMC)
result = NuSMV.BMC(bound, nusmv.getNuSMVCode());
else
result = NuSMV.SMC(nusmv.getNuSMVCode());
if(result)
{
if (result) {
System.out.println("Found counter example in step "
+ (fileno));
WriteMapping(nextinstance, "ROLEMAPPING");
......@@ -356,6 +356,19 @@ public class RolesAbsRefine {
}
}
/**
* A quick function to see if this will get rid of the NuSMV error that is
* given when trying to use the SMV code generated by RBAC2SMV.java
*
* @author Jonathan Shahen
* @return
*/
public RBACInstance refineOnly() {
refine();
return nextinstance;
}
public void WriteMapping(RBACInstance inrbacinstance, String filename)
throws IOException {
......
......@@ -7,6 +7,7 @@ import java.util.logging.Logger;
import mohawk.RBACInstance;
import mohawk.RBACSpecReader;
import mohawk.RolesAbsRefine;
import mohawk.WriteNuSMV;
public class SMVSpecHelper {
......@@ -78,15 +79,18 @@ public class SMVSpecHelper {
+ specFile.getName());
}
RBACSpecReader reader = new RBACSpecReader(specFile.getAbsolutePath());
RBACInstance rbac = reader.getRBAC();
WriteNuSMV nusmv = new WriteNuSMV(nusmvFile.getAbsolutePath(),
"smvtemplate");
try {
if (rbac != null) {
nusmv.fillAttributes(rbac);
}
RBACSpecReader reader = new RBACSpecReader(
specFile.getAbsolutePath());
RBACInstance rbac = reader.getRBAC();
RolesAbsRefine absrefine = new RolesAbsRefine(rbac);
RBACInstance rbac_refined = absrefine.refineOnly();
WriteNuSMV nusmv = new WriteNuSMV(nusmvFile.getAbsolutePath(),
"smvtemplate");
nusmv.fillAttributes(rbac_refined);
nusmv.writeFile();
} catch (IOException e1) {
logger.severe("[ERROR] Unable to write to the SMV file: "
......
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