From 9e5b965740fa86bed211b5969f35e77aa42d8129 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 30 Jul 2024 16:10:08 +0200
Subject: [PATCH] Try removing automatic "fixing" of input file paths
We can expect probcli, etc. to pass complete and correct paths. I hope.
---
src/main/java/de/tlc4b/TLC4B.java | 7 -------
.../java/de/tlc4b/tlc/integration/LTLTest.java | 14 +++++++-------
2 files changed, 7 insertions(+), 14 deletions(-)
diff --git a/src/main/java/de/tlc4b/TLC4B.java b/src/main/java/de/tlc4b/TLC4B.java
index 3e341c9..403a33a 100644
--- a/src/main/java/de/tlc4b/TLC4B.java
+++ b/src/main/java/de/tlc4b/TLC4B.java
@@ -401,13 +401,6 @@ public class TLC4B {
}
private void handleMainFileName() {
- // the following lines fix incorrect file names
- filename = filename.replace("\\", File.separator);
- filename = filename.replace("/", File.separator);
- if (!filename.toLowerCase().endsWith(".mch") && !filename.toLowerCase().endsWith(".sys")) {
- filename = filename + ".mch";
- }
-
mainfile = new File(filename);
if (!mainfile.exists()) {
throw new TLC4BIOException("The file " + mainfile.getPath() + " does not exist.");
diff --git a/src/test/java/de/tlc4b/tlc/integration/LTLTest.java b/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
index 8cbe47c..63f87ae 100644
--- a/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
+++ b/src/test/java/de/tlc4b/tlc/integration/LTLTest.java
@@ -20,43 +20,43 @@ public class LTLTest {
@Test
public void testCounterLTL() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\CounterLTL.mch" };
+ String[] a = new String[] { "src/test/resources/ltl/CounterLTL.mch" };
assertEquals(NoError, test(a));
}
@Test
public void testCounterError() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\CounterError.mch" };
+ String[] a = new String[] { "src/test/resources/ltl/CounterError.mch" };
assertEquals(TemporalPropertyViolation, test(a));
}
@Test
public void testFairnessCounterLTL() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\FairnessCounter.mch" };
+ String[] a = new String[] { "src/test/resources/ltl/FairnessCounter.mch" };
assertEquals(NoError, test(a));
}
@Test
public void testUniversalQuantificaitonLTL() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\UniveralQuatification.mch" };
+ String[] a = new String[] { "src/test/resources/ltl/UniveralQuatification.mch" };
assertEquals(TemporalPropertyViolation, test(a));
}
@Test
public void testExistentialQuantificationLTL() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\ExistentialQuantification.mch" };
+ String[] a = new String[] { "src/test/resources/ltl/ExistentialQuantification.mch" };
assertEquals(NoError, test(a));
}
@Test
public void testFairnessParameter() throws Exception {
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\Fairness_Parameter.mch" };
+ String[] a = new String[] { "src/test/resources/ltl/Fairness_Parameter.mch" };
assertEquals(NoError, test(a));
}
@Test
public void testLTLStatePropertyViolation() throws Exception{
- String[] a = new String[] { ".\\src\\test\\resources\\ltl\\StatePropertyViolation.mch" };
+ String[] a = new String[] { "src/test/resources/ltl/StatePropertyViolation.mch" };
assertEquals(TemporalPropertyViolation, test(a));
}
--
GitLab