Clean up getting MPSat command for verification

workcraft · Apr 25, 2024 · 47a20b1 · 47a20b1
1 parent 3b5012c
commit 47a20b1
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 28 deletions.
diff --git a/...icationPlugin/src/org/workcraft/plugins/mpsat_verification/MpsatVerificationSettings.java b/...icationPlugin/src/org/workcraft/plugins/mpsat_verification/MpsatVerificationSettings.java
@@ -8,18 +8,11 @@
 import org.workcraft.plugins.mpsat_verification.tasks.CompositionOutputInterpreter.ConformationReportStyle;
 import org.workcraft.utils.BackendUtils;
 
-import java.io.File;
 import java.util.LinkedList;
 import java.util.List;
 
 public class MpsatVerificationSettings extends AbstractToolSettings {
 
-    private static final PropertyDeclaration<String> commandProperty;
-    private static final String COMMAND_DIRECTORY = "UnfoldingTools";
-    private static final String COMMAND_64BIT_DIRECTORY = "UnfoldingTools64";
-    private static final String COMMAND_REGEX = "^(?<prefix>.*[\\\\/])" + COMMAND_DIRECTORY + "(?<suffix>[\\\\/].+)$";
-    private static final String COMMAND_64BIT_REPLACEMENT = "${prefix}" + COMMAND_64BIT_DIRECTORY + "${suffix}";
-
     private static final LinkedList<PropertyDescriptor> properties = new LinkedList<>();
     private static final String prefix = "Tools.mpsatVerification";
 
@@ -35,7 +28,7 @@ public class MpsatVerificationSettings extends AbstractToolSettings {
     private static final String keyDebugCores = prefix + ".debugCores";
     private static final String keyConformationReportStyle = prefix + ".conformationReportStyle";
 
-    private static final String defaultCommand = BackendUtils.getToolPath(COMMAND_DIRECTORY, "mpsat");
+    private static final String defaultCommand = BackendUtils.getToolPath("UnfoldingTools", "mpsat");
     private static final int defaultThreadCount = 8;
     private static final boolean defaultReplicateSelfloopPlaces = true;
     private static final SolutionMode defaultSolutionMode = SolutionMode.MINIMUM_COST;
@@ -60,12 +53,10 @@ public class MpsatVerificationSettings extends AbstractToolSettings {
     private static ConformationReportStyle conformationReportStyle = defaultConformationReportStyle;
 
     static {
-        commandProperty = new PropertyDeclaration<>(String.class,
+        properties.add(new PropertyDeclaration<>(String.class,
                 "MPSat command for verification",
                 MpsatVerificationSettings::setCommand,
-                MpsatVerificationSettings::getProcessedCommand);
-
-        properties.add(commandProperty);
+                MpsatVerificationSettings::getCommand));
 
         properties.add(new PropertyDeclaration<>(Integer.class,
                 "Number of threads for unfolding (8 by default, 0 for automatic)",
@@ -166,19 +157,6 @@ public static void setCommand(String value) {
         command = value;
     }
 
-    public static String getProcessedCommand() {
-        if (defaultCommand.equals(command)) {
-            String processedCommand = command.replaceAll(COMMAND_REGEX, COMMAND_64BIT_REPLACEMENT);
-            File file = new File(processedCommand);
-            if (file.exists() && file.isFile() && file.canExecute()) {
-                commandProperty.setEditable(false);
-                return processedCommand;
-            }
-        }
-        commandProperty.setEditable(true);
-        return command;
-    }
-
     public static int getThreadCount() {
         return threadCount;
     }

diff --git a/...cationPlugin/src/org/workcraft/plugins/mpsat_verification/tasks/MpsatSyntaxCheckTask.java b/...cationPlugin/src/org/workcraft/plugins/mpsat_verification/tasks/MpsatSyntaxCheckTask.java
@@ -28,7 +28,7 @@ public Result<? extends ExternalProcessOutput> run(ProgressMonitor<? super Exter
         ArrayList<String> command = new ArrayList<>();
 
         // Name of the executable
-        String toolName = ExecutableUtils.getAbsoluteCommandPath(MpsatVerificationSettings.getProcessedCommand());
+        String toolName = ExecutableUtils.getAbsoluteCommandPath(MpsatVerificationSettings.getCommand());
         command.add(toolName);
 
         // Built-in arguments

diff --git a/...MpsatVerificationPlugin/src/org/workcraft/plugins/mpsat_verification/tasks/MpsatTask.java b/...MpsatVerificationPlugin/src/org/workcraft/plugins/mpsat_verification/tasks/MpsatTask.java
@@ -51,7 +51,7 @@ public Result<? extends MpsatOutput> run(ProgressMonitor<? super MpsatOutput> mo
         ArrayList<String> command = new ArrayList<>();
 
         // Name of the executable
-        String toolName = ExecutableUtils.getAbsoluteCommandPath(MpsatVerificationSettings.getProcessedCommand());
+        String toolName = ExecutableUtils.getAbsoluteCommandPath(MpsatVerificationSettings.getCommand());
         command.add(toolName);
 
         // Built-in arguments

diff --git a/...ficationPlugin/src/org/workcraft/plugins/mpsat_verification/tasks/MpsatUnfoldingTask.java b/...ficationPlugin/src/org/workcraft/plugins/mpsat_verification/tasks/MpsatUnfoldingTask.java
@@ -27,7 +27,7 @@ public Result<? extends MpsatOutput> run(ProgressMonitor<? super MpsatOutput> mo
         ArrayList<String> command = new ArrayList<>();
 
         // Name of the executable
-        String toolName = ExecutableUtils.getAbsoluteCommandPath(MpsatVerificationSettings.getProcessedCommand());
+        String toolName = ExecutableUtils.getAbsoluteCommandPath(MpsatVerificationSettings.getCommand());
         command.add(toolName);
 
         // Unfolding prefix mode