From fbc2ffa275b0c8810d7e5264bd73facf53d796ab Mon Sep 17 00:00:00 2001
From: Miles Vella <673-vella@users.noreply.gitlab.cs.uni-duesseldorf.de>
Date: Tue, 18 Mar 2025 10:26:03 +0100
Subject: [PATCH] re-enable silent ignore of return parameters because tests
depend on this behaviour
why?
---
src/main/java/de/tlc4b/prettyprint/TLAPrinter.java | 14 +++++++++-----
1 file changed, 9 insertions(+), 5 deletions(-)
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 3ca0919..de62cec 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -669,12 +669,16 @@ public class TLAPrinter extends DepthFirstAdapter {
PExpression right = copy2.get(i);
AIdentifierExpression assigned = getAssignedIdentifier(left);
- if (!machineContext.getVariables().containsKey(Utils.getAIdentifierAsString(assigned))) {
- throw new NotSupportedException("can only assign to machine variables");
+ if (machineContext.getVariables().containsKey(Utils.getAIdentifierAsString(assigned))) {
+ assigned.apply(this);
+ moduleStringAppend(" = ");
+ printAssignmentRhs(assigned, right);
+ } else {
+ // these are either errors in the machine or return parameters
+ // ignore them for now because some tests depend on this behaviour
+ moduleStringAppend("TRUE");
+ // TODO: throw new NotSupportedException("can only assign to machine variables");
}
- assigned.apply(this);
- moduleStringAppend(" = ");
- printAssignmentRhs(assigned, right);
if (i < copy.size() - 1) {
moduleStringAppend(" /\\ ");
--
GitLab