Commit d84c7632 authored by Jonathan Shahen's avatar Jonathan Shahen

Updating so that NuSMV class is no longer static

parent 45a3ae29
...@@ -17,6 +17,7 @@ import mohawk.math.CalculateDiameter; ...@@ -17,6 +17,7 @@ import mohawk.math.CalculateDiameter;
import mohawk.output.WriteNuSMV; import mohawk.output.WriteNuSMV;
import mohawk.output.WriteRBACSpec; import mohawk.output.WriteRBACSpec;
import mohawk.rbac.RBACInstance; import mohawk.rbac.RBACInstance;
import mohawk.singleton.MohawkSettings;
/** /**
* @author kjayaram * @author kjayaram
...@@ -105,6 +106,7 @@ public class RolesAbsRefine { ...@@ -105,6 +106,7 @@ public class RolesAbsRefine {
// NuSMV bmc // NuSMV bmc
Boolean result; Boolean result;
NuSMV runNuSMV = new NuSMV(MohawkSettings.getInstance().getNuSMV_filepath());
if (mode == NuSMVMode.BMC) { if (mode == NuSMVMode.BMC) {
// CalculateDiameter diameter = new CalculateDiameter(); // NEVER USED // CalculateDiameter diameter = new CalculateDiameter(); // NEVER USED
int bound = CalculateDiameter.GetDiameter(curInstance); int bound = CalculateDiameter.GetDiameter(curInstance);
...@@ -112,20 +114,20 @@ public class RolesAbsRefine { ...@@ -112,20 +114,20 @@ public class RolesAbsRefine {
curInstance.getNumRoles(), bound)); curInstance.getNumRoles(), bound));
if (skipSMVFile) { if (skipSMVFile) {
result = NuSMV.BMC(bound, nusmv.getNuSMVCode()); result = runNuSMV.BMC(bound, nusmv.getNuSMVCode());
} else { } else {
result = NuSMV.BMCFile(bound, nusmv.getFilename()); result = runNuSMV.BMCFile(bound, nusmv.getFilename());
} }
} else { } else {
if (skipSMVFile) { if (skipSMVFile) {
result = NuSMV.SMC(nusmv.getNuSMVCode()); result = runNuSMV.SMC(nusmv.getNuSMVCode());
} else { } else {
result = NuSMV.SMCFile(nusmv.getFilename()); result = runNuSMV.SMCFile(nusmv.getFilename());
} }
} }
returnValue = NuSMV.execProcess.exitValue(); returnValue = runNuSMV.execProcess.exitValue();
return result; return result;
} }
......
...@@ -2,7 +2,6 @@ package mohawk.singleton; ...@@ -2,7 +2,6 @@ package mohawk.singleton;
import java.util.logging.Level; import java.util.logging.Level;
import mohawk.global.nusmv.NuSMV;
import mohawk.global.results.MohawkResults; import mohawk.global.results.MohawkResults;
import mohawk.global.results.TestingResult; import mohawk.global.results.TestingResult;
import mohawk.global.timing.MohawkTiming; import mohawk.global.timing.MohawkTiming;
...@@ -30,7 +29,6 @@ public class MohawkSettings { ...@@ -30,7 +29,6 @@ public class MohawkSettings {
public void setNuSMV_filepath(String nuSMV_filepath) { public void setNuSMV_filepath(String nuSMV_filepath) {
NuSMV_filepath = nuSMV_filepath; NuSMV_filepath = nuSMV_filepath;
NuSMV.NuSMVProcessName = nuSMV_filepath;
} }
// Helpers // Helpers
......
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