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

Writes out the SMV file always and now can call NuSMV with the file's name...

Writes out the SMV file always and now can call NuSMV with the file's name instead writing the file contents in a pipe
parent 08d37ca1
...@@ -45,7 +45,7 @@ public class RolesAbsRefine { ...@@ -45,7 +45,7 @@ public class RolesAbsRefine {
private int lastpriority; private int lastpriority;
private NuSMVMode mode;// mode private NuSMVMode mode;// mode
public boolean skipSMVFile = true; public boolean skipSMVFile = false;
public RolesAbsRefine(RBACInstance inRbac) { public RolesAbsRefine(RBACInstance inRbac) {
...@@ -103,9 +103,18 @@ public class RolesAbsRefine { ...@@ -103,9 +103,18 @@ public class RolesAbsRefine {
System.out.println(String.format("Estimate Diameter - No of Roles %d Diameter %d", System.out.println(String.format("Estimate Diameter - No of Roles %d Diameter %d",
curInstance.getNumRoles(), bound)); curInstance.getNumRoles(), bound));
result = NuSMV.BMC(bound, nusmv.getNuSMVCode()); if (skipSMVFile) {
result = NuSMV.BMC(bound, nusmv.getNuSMVCode());
} else {
result = NuSMV.BMCFile(bound, nusmv.getFilename());
}
} else { } else {
result = NuSMV.SMC(nusmv.getNuSMVCode());
if (skipSMVFile) {
result = NuSMV.SMC(nusmv.getNuSMVCode());
} else {
result = NuSMV.SMCFile(nusmv.getFilename());
}
} }
return result; return result;
......
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