From d19e8b67f33c355f76a6526b1ea57b1f9ada9049 Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Fri, 19 Jul 2024 16:03:14 +0200
Subject: [PATCH] Collect violated assumptions in DFIDModelChecker as well
---
.../src/tlc2/tool/DFIDModelChecker.java | 10 +++++++---
1 file changed, 7 insertions(+), 3 deletions(-)
diff --git a/tlatools/org.lamport.tlatools/src/tlc2/tool/DFIDModelChecker.java b/tlatools/org.lamport.tlatools/src/tlc2/tool/DFIDModelChecker.java
index c333ed588..a9cfb47b6 100644
--- a/tlatools/org.lamport.tlatools/src/tlc2/tool/DFIDModelChecker.java
+++ b/tlatools/org.lamport.tlatools/src/tlc2/tool/DFIDModelChecker.java
@@ -12,6 +12,7 @@ import tla2sany.semantic.OpDeclNode;
import tlc2.TLCGlobals;
import tlc2.output.EC;
import tlc2.output.MP;
+import tlc2.output.OutputCollector;
import tlc2.tool.fp.dfid.FPIntSet;
import tlc2.tool.fp.dfid.MemFPIntSet;
import tlc2.tool.impl.CallStackTool;
@@ -246,22 +247,25 @@ public class DFIDModelChecker extends AbstractChecker
{
ExprNode[] assumps = this.tool.getAssumptions();
boolean[] isAxiom = this.tool.getAssumptionIsAxiom();
+ int assumptionsError = EC.NO_ERROR;
for (int i = 0; i < assumps.length; i++)
{
try
{
if ((!isAxiom[i]) && !this.tool.isValid(assumps[i]))
{
- return MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
+ OutputCollector.addViolatedAssumption(assumps[i]);
+ assumptionsError = MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
}
} catch (Exception e)
{
// Assert.printStack(e);
- return MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,
+ OutputCollector.addViolatedAssumption(assumps[i]);
+ assumptionsError = MP.printError(EC.TLC_ASSUMPTION_EVALUATION_ERROR,
new String[] { assumps[i].toString(), e.getMessage() });
}
}
- return EC.NO_ERROR;
+ return assumptionsError;
}
/* Compute the set of initial states. */
--
GitLab