Skip to content
Snippets Groups Projects
Commit 9e5b9657 authored by dgelessus's avatar dgelessus
Browse files

Try removing automatic "fixing" of input file paths

We can expect probcli, etc. to pass complete and correct paths. I hope.
parent 9b4d6d14
No related branches found
No related tags found
No related merge requests found
...@@ -401,13 +401,6 @@ public class TLC4B { ...@@ -401,13 +401,6 @@ public class TLC4B {
} }
private void handleMainFileName() { 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); mainfile = new File(filename);
if (!mainfile.exists()) { if (!mainfile.exists()) {
throw new TLC4BIOException("The file " + mainfile.getPath() + " does not exist."); throw new TLC4BIOException("The file " + mainfile.getPath() + " does not exist.");
......
...@@ -20,43 +20,43 @@ public class LTLTest { ...@@ -20,43 +20,43 @@ public class LTLTest {
@Test @Test
public void testCounterLTL() throws Exception { 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)); assertEquals(NoError, test(a));
} }
@Test @Test
public void testCounterError() throws Exception { 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)); assertEquals(TemporalPropertyViolation, test(a));
} }
@Test @Test
public void testFairnessCounterLTL() throws Exception { 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)); assertEquals(NoError, test(a));
} }
@Test @Test
public void testUniversalQuantificaitonLTL() throws Exception { 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)); assertEquals(TemporalPropertyViolation, test(a));
} }
@Test @Test
public void testExistentialQuantificationLTL() throws Exception { 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)); assertEquals(NoError, test(a));
} }
@Test @Test
public void testFairnessParameter() throws Exception { 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)); assertEquals(NoError, test(a));
} }
@Test @Test
public void testLTLStatePropertyViolation() throws Exception{ 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)); assertEquals(TemporalPropertyViolation, test(a));
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment