adapt handled error messages for TLC 2.18

and related minor changes

src/main/java/de/tlc4b/TLCRunner.java

@@ -41,8 +41,8 @@ public class TLCRunner {
 		System.arraycopy(args, 1, parameters, 0, parameters.length);
 		try {
 			TLC.main(parameters);
-		} catch (UnknownHostException | FileNotFoundException e) {
-			e.printStackTrace();
+		} catch (Exception e) {
+			throw new RuntimeException(e);
 		}
 	}
 

src/main/java/de/tlc4b/tlc/TLCResults.java

@@ -315,10 +315,6 @@ public class TLCResults implements ToolGlobals {
 				}
 				break;
 
-			case EC.TLC_ASSUMPTION_EVALUATION_ERROR:
-				tlcResult = evaluatingParameter(m.getParameters());
-				break;
-
 			case EC.TLC_VALUE_ASSERT_FAILED:
 				tlcResult = WellDefinednessError;
 				break;
@@ -329,6 +325,21 @@ public class TLCResults implements ToolGlobals {
 				}
 				break;
 
+			case EC.TLC_CONFIG_ID_HAS_VALUE: // LTL errors, Assertion violations
+				String kind = m.getParameters()[0];
+				String id = m.getParameters()[1];
+				// third param should be "FALSE" (we are already in error case here)
+				if (kind.contains("property") && id.startsWith("ASSERT_LTL")) {
+					tlcResult = TemporalPropertyViolation;
+				} else if (kind.contains("invariant") && id.startsWith("Assertion")) {
+					tlcResult = AssertionError;
+				} else {
+					// just as fall-back
+					tlcResult = evaluatingParameter(m.getParameters());
+				}
+				break;
+
+			case EC.TLC_ASSUMPTION_EVALUATION_ERROR:
 			case EC.GENERAL:
 				tlcResult = evaluatingParameter(m.getParameters());
 				break;
@@ -356,17 +367,18 @@ public class TLCResults implements ToolGlobals {
 				return AssertionError;
 			} else if (s.contains("The invariant of Invariant")) {
 				return InvariantViolation;
-			} else if (s.contains("In applying the function")) {
-				return WellDefinednessError;
-			} else if (s.contains("which is not in the domain of the function")) {
-				return WellDefinednessError;
-			} else if (s.contains("tlc2.module.TLC.Assert")) {
+			} else if (s.contains("In applying the function")
+				|| s.contains("which is not in the domain of the function")
+				|| s.contains("tlc2.module.TLC.Assert")
+				|| (s.contains("CHOOSE x \\in S: P, but no element of S satisfied P") && s.contains("module FunctionsAsRelations"))
+				// messages from BBuiltIns:
+				|| s.contains("Both operands of the modulo operator must be natural numbers")
+				|| s.contains("Division by zero")
+				|| s.contains("Applied the inter operator to an empty set")
+				|| s.replace("\n","").matches(".*The.*argument.*operator should be.*sequence.*")
+				|| s.replace("\n","").matches(".*The.*argument.*operator is an invalid number.*")) {
 				return WellDefinednessError;
-			} else if (s
-				.contains("CHOOSE x \\in S: P, but no element of S satisfied P")
-				&& s.contains("module FunctionsAsRelations")) {
-				return tlcResult = WellDefinednessError;
-			} else if (s.contains("The property of ASSERT_LTL")) {
+			} else if (s.contains("ASSERT_LTL")) {
 				return TemporalPropertyViolation;
 			}
 		}

src/main/java/de/tlc4b/tlc/TracePrinter.java

@@ -11,27 +11,7 @@ import de.tlc4b.exceptions.NotSupportedException;
 import tla2sany.semantic.OpDeclNode;
 import tlc2.tool.TLCState;
 import tlc2.tool.TLCStateInfo;
-import tlc2.value.FcnLambdaValue;
-import tlc2.value.FcnRcdValue;
-import tlc2.value.IntervalValue;
-import tlc2.value.LazyValue;
-import tlc2.value.ModelValue;
-import tlc2.value.RecordValue;
-import tlc2.value.SetCapValue;
-import tlc2.value.SetCupValue;
-import tlc2.value.SetDiffValue;
-import tlc2.value.SetEnumValue;
-import tlc2.value.SetOfFcnsValue;
-import tlc2.value.SetOfRcdsValue;
-import tlc2.value.SetOfTuplesValue;
-import tlc2.value.SetPredValue;
-import tlc2.value.StringValue;
-import tlc2.value.SubsetValue;
-import tlc2.value.TupleValue;
-import tlc2.value.UnionValue;
-import tlc2.value.Value;
-import tlc2.value.ValueEnumeration;
-import tlc2.value.ValueVec;
+import tlc2.value.impl.*;
 import util.UniqueString;
 import static tlc2.value.ValueConstants.*;
 
@@ -111,8 +91,7 @@ public class TracePrinter {
 					UniqueString var = constants.get(i).getName();
 					String bName = tlcOutputInfo.getBName(var.toString());
 					BType type = tlcOutputInfo.getBType(var.toString());
-					String value = parseValue(state.lookup(var), type)
-							.toString();
+					String value = parseValue((Value) state.lookup(var), type).toString();
 					expression.append(bName).append(" = ").append(value);
 				}
 			}
@@ -131,7 +110,7 @@ public class TracePrinter {
 			UniqueString var = variables.get(i).getName();
 			String bName = tlcOutputInfo.getBName(var.toString());
 			BType type = tlcOutputInfo.getBType(var.toString());
-			String value = parseValue(state.lookup(var), type).toString();
+			String value = parseValue((Value) state.lookup(var), type).toString();
 			expression.append(bName).append(" = ").append(value);
 		}
 		return expression;