From 5119e154f4a6a11152ea32fed612521bfd8def92 Mon Sep 17 00:00:00 2001
From: hansen <dominik_hansen@web.de>
Date: Thu, 17 Sep 2015 13:53:56 +0200
Subject: [PATCH] Print complete error message in case of an invariant
violation.
---
tlatools/src/tlc2/output/MP.java | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java
index fba524bba..593529e5e 100644
--- a/tlatools/src/tlc2/output/MP.java
+++ b/tlatools/src/tlc2/output/MP.java
@@ -358,7 +358,7 @@ public class MP
break;
case EC.TLC_INVARIANT_EVALUATION_FAILED:
- b.append("Evaluating invariant %1% failed.");
+ b.append("Evaluating invariant %1% failed:\n%2%");
break;
case EC.TLC_ACTION_PROPERTY_VIOLATED_BEHAVIOR:
--
GitLab