Skip to content
Snippets Groups Projects
Commit 61971375 authored by hansen's avatar hansen
Browse files

Fixed unhandled LTL parse error exception

parent c493dac9
No related branches found
No related tags found
No related merge requests found
......@@ -37,7 +37,7 @@ public class TLC4B {
private String ltlFormula;
private String constantsSetup;
public static void main(String[] args) throws IOException {
public static void main(String[] args) {
System.setProperty("apple.awt.UIElement", "true"); // avoiding pop up
// windows
TLC4B tlc4b = new TLC4B();
......@@ -52,6 +52,10 @@ public class TLC4B {
System.out.println("Model checking time: 0 sec");
System.out.println("Result: " + e.getError());
return;
} catch (IOException e) {
System.err.println(e.getMessage());
System.out.println("Model checking time: 0 sec");
System.out.println("Result: " + "I/O Error");
}
if (TLC4BGlobals.isRunTLC()) {
......
......@@ -163,7 +163,7 @@ public class LTLFormulaVisitor extends DepthFirstAdapter {
try {
start = parser.parse(bPredicate, false);
} catch (BException e) {
e.printStackTrace();
throw new LTLParseException(e.getMessage());
}
return start;
......
......@@ -18,12 +18,12 @@ import static de.tlc4b.tlc.TLCResults.TLCResult.NoError;
import static de.tlc4b.util.TestUtil.test;
@RunWith(PolySuite.class)
public class BasicsTest extends AbstractParseMachineTest {
public class BasicTest extends AbstractParseMachineTest {
private final File machine;
private final TLCResult error;
public BasicsTest(File machine, TLCResult result) {
public BasicTest(File machine, TLCResult result) {
this.machine = machine;
this.error = result;
}
......
package de.tlc4b.tlc.integration;
import org.junit.Test;
import de.tlc4b.TLC4B;
public class BugTest {
@Test
public void testTraceValues() {
String[] a = new String[] { "./src/test/resources/bugs/LTLParseError.mch" };
TLC4B.main(a);
}
}
\ No newline at end of file
MACHINE Test
DEFINITIONS
ASSERT_LTL_1 == "G(!a.({a:ID & a==aa} => F{a : xx}))"
SETS
ID={aa,bb}
CONSTANTS iv
PROPERTIES
iv:ID
VARIABLES xx
INVARIANT
xx:POW(ID)
INITIALISATION xx:={}
OPERATIONS
Set(yy) = SELECT yy:ID & yy /:xx THEN xx:= xx \/ {yy} END
END
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment