From 72274a50fa34d0647d01c78d4472ebaadd9236c6 Mon Sep 17 00:00:00 2001
From: Miles Vella <673-vella@users.noreply.gitlab.cs.uni-duesseldorf.de>
Date: Tue, 18 Mar 2025 00:48:00 +0100
Subject: [PATCH] disable handling of output parameters for now
I don't think they have ever worked
---
.../tlc4b/analysis/UsedStandardModules.java | 38 +++++++++++++++++--
.../java/de/tlc4b/prettyprint/TLAPrinter.java | 3 ++
.../de/tlc4b/prettyprint/OperationsTest.java | 2 +
3 files changed, 39 insertions(+), 4 deletions(-)
diff --git a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
index d707ac2..f39af12 100644
--- a/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
+++ b/src/main/java/de/tlc4b/analysis/UsedStandardModules.java
@@ -127,6 +127,8 @@ public class UsedStandardModules extends DepthFirstAdapter {
private final Set<StandardModule> extendedStandardModules;
private final Typechecker typechecker;
+ private boolean inAssignment = false;
+
public UsedStandardModules(Start start, Typechecker typechecker,
TypeRestrictor typeRestrictor, TLAModule tlaModule) {
this.extendedStandardModules = new HashSet<>();
@@ -435,11 +437,17 @@ public class UsedStandardModules extends DepthFirstAdapter {
// Function call
public void inAFunctionExpression(AFunctionExpression node) {
BType type = typechecker.getType(node.getIdentifier());
- if (type instanceof FunctionType) {
- extendedStandardModules.add(StandardModule.Functions);
+ if (inAssignment) {
+ if (type instanceof FunctionType) {
+ extendedStandardModules.add(StandardModule.Functions);
+ } else {
+ extendedStandardModules.add(StandardModule.FunctionsAsRelations);
+ extendedStandardModules.add(StandardModule.Relations);
+ }
} else {
- extendedStandardModules.add(StandardModule.FunctionsAsRelations);
- extendedStandardModules.add(StandardModule.Relations);
+ if (type instanceof SetType) {
+ extendedStandardModules.add(StandardModule.FunctionsAsRelations);
+ }
}
}
@@ -521,6 +529,28 @@ public class UsedStandardModules extends DepthFirstAdapter {
// function assignments are handled in "inAFunctionExpression"
}
+ @Override
+ public void caseAAssignSubstitution(AAssignSubstitution node) {
+ inAAssignSubstitution(node);
+ {
+ inAssignment = true;
+ List<PExpression> copy = new ArrayList<PExpression>(node.getLhsExpression());
+ for(PExpression e : copy)
+ {
+ e.apply(this);
+ }
+ inAssignment = false;
+ }
+ {
+ List<PExpression> copy = new ArrayList<PExpression>(node.getRhsExpressions());
+ for(PExpression e : copy)
+ {
+ e.apply(this);
+ }
+ }
+ outAAssignSubstitution(node);
+ }
+
public void inADirectProductExpression(ADirectProductExpression node) {
extendedStandardModules.add(StandardModule.Relations);
}
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 1d6bcd9..3ca0919 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -669,6 +669,9 @@ 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");
+ }
assigned.apply(this);
moduleStringAppend(" = ");
printAssignmentRhs(assigned, right);
diff --git a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
index bad0b01..030914c 100644
--- a/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
+++ b/src/test/java/de/tlc4b/prettyprint/OperationsTest.java
@@ -2,6 +2,7 @@ package de.tlc4b.prettyprint;
import static de.tlc4b.util.TestUtil.compare;
+import org.junit.Ignore;
import org.junit.Test;
import de.tlc4b.exceptions.SubstitutionException;
@@ -386,6 +387,7 @@ public class OperationsTest {
}
@Test
+ @Ignore("output params aren't working")
public void testOutputParams() throws Exception {
String machine = "MACHINE test\n"
+ "VARIABLES x\n"
--
GitLab