feed an LTL formula to LTSMin via a file (#53)

* feed an LTL formula to LTSMin via a file * Use try-with-resource block * add a test case of long LTL formula * cleanup code analysis errors * refactor testcase * move case in a separate test method * use a formula that is easier to modelcheck to reduce runtime --------- Co-authored-by: Markus Frohme <[email protected]>
LearnLib · Feb 15, 2023 · 5278418 · 5278418
1 parent dabab34
commit 5278418
Show file tree

Hide file tree

Showing 2 changed files with 47 additions and 2 deletions.
diff --git a/modelchecking/ltsmin/src/main/java/net/automatalib/modelcheckers/ltsmin/AbstractLTSmin.java b/modelchecking/ltsmin/src/main/java/net/automatalib/modelcheckers/ltsmin/AbstractLTSmin.java
@@ -17,13 +17,15 @@
 
 import java.io.File;
 import java.io.IOException;
+import java.io.Writer;
 import java.util.Collection;
 import java.util.Collections;
 import java.util.List;
 import java.util.function.Function;
 
 import com.google.common.collect.Lists;
 import net.automatalib.AutomataLibSettings;
+import net.automatalib.commons.util.IOUtil;
 import net.automatalib.commons.util.process.ProcessUtil;
 import net.automatalib.exception.ModelCheckingException;
 import net.automatalib.modelchecking.ModelChecker;
@@ -177,6 +179,25 @@ public Function<String, I> getString2Input() {
             throw new ModelCheckingException(ioe);
         }
 
+        final File ltlFile;
+
+        try {
+            // write LTL formula to a file because long formulae may cause problems as direct inputs to LTSmin
+            ltlFile = File.createTempFile("formula", ".ltl");
+
+            try (Writer w = IOUtil.asBufferedUTF8Writer(ltlFile)) {
+                // write to the file
+                w.write(formula);
+            } catch (IOException ioe) {
+                if (!keepFiles && !ltlFile.delete()) {
+                    LOGGER.warn("Could not delete file: " + ltlFile.getAbsolutePath());
+                }
+                throw ioe;
+            }
+        } catch (IOException ioe) {
+            throw new ModelCheckingException(ioe);
+        }
+
         final File gcf;
 
         try {
@@ -195,7 +216,7 @@ public Function<String, I> getString2Input() {
                                                                   // add the ETF file that contains the hypothesis
                                                                   etf.getAbsolutePath(),
                                                                   // add the LTL formula
-                                                                  "--ltl=" + formula,
+                                                                  "--ltl=" + ltlFile,
                                                                   // write the trace to this file
                                                                   "--trace=" + gcf.getAbsolutePath(),
                                                                   // use only one thread (hypotheses are always small)
@@ -259,6 +280,9 @@ public Function<String, I> getString2Input() {
                 if (!etf.delete()) {
                     LOGGER.warn("Could not delete file: " + etf.getAbsolutePath());
                 }
+                if (!ltlFile.delete()) {
+                    LOGGER.warn("Could not delete file: " + ltlFile.getAbsolutePath());
+                }
                 if (!gcf.delete()) {
                     LOGGER.warn("Could not delete file: " + gcf.getAbsolutePath());
                 }

diff --git a/...hecking/ltsmin/src/test/java/net/automatalib/modelcheckers/ltsmin/AbstractLTSminTest.java b/...hecking/ltsmin/src/test/java/net/automatalib/modelcheckers/ltsmin/AbstractLTSminTest.java
@@ -89,4 +89,25 @@ public void testFindCounterExample() {
         Assert.assertNotNull(ce);
         Assert.assertEquals(counterExample.computeOutput(input), ce.computeOutput(input));
     }
-}
+
+    /**
+     * It appears that the input buffer of LTSmin for input formulae is limited to 8192 (2^13) bytes. As a result, we
+     * need to pass longer formulae as a file. This test checks for compatibility with long formulae.
+     */
+    @Test
+    public void testLongFormula() {
+        final StringBuilder builder = new StringBuilder();
+        final int length = falseProperty.length();
+        final int max = ((1 << 13) / length) + 1;
+
+        for (int i = 0; i < max; i++) {
+            builder.append(falseProperty);
+            builder.append(" && ");
+        }
+        builder.append(falseProperty);
+
+        final R ce = getModelChecker().findCounterExample(automaton, alphabet, builder.toString());
+        Assert.assertNotNull(ce);
+        Assert.assertEquals(counterExample.computeOutput(input), ce.computeOutput(input));
+    }
+}