From ed05fef8f7dcbeab984fbad5983507c2436870cc Mon Sep 17 00:00:00 2001
From: Miles Vella <673-vella@users.noreply.gitlab.cs.uni-duesseldorf.de>
Date: Thu, 13 Mar 2025 15:32:59 +0100
Subject: [PATCH] fix renamer not respecting ACTION
---
src/main/java/de/tlc4b/analysis/Renamer.java | 1 +
src/test/java/de/tlc4b/tlc/integration/FixedBugs.java | 11 ++++++++++-
2 files changed, 11 insertions(+), 1 deletion(-)
diff --git a/src/main/java/de/tlc4b/analysis/Renamer.java b/src/main/java/de/tlc4b/analysis/Renamer.java
index dd9b2d4..223999a 100644
--- a/src/main/java/de/tlc4b/analysis/Renamer.java
+++ b/src/main/java/de/tlc4b/analysis/Renamer.java
@@ -39,6 +39,7 @@ public class Renamer extends DepthFirstAdapter {
private final HashSet<String> globalNames;
private final static Set<String> KEYWORDS = new HashSet<>();
static {
+ KEYWORDS.add("ACTION");
KEYWORDS.add("ASSUME");
KEYWORDS.add("ASSUMPTION");
KEYWORDS.add("AXIOM");
diff --git a/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java b/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java
index 90a8309..0874873 100644
--- a/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java
+++ b/src/test/java/de/tlc4b/tlc/integration/FixedBugs.java
@@ -6,7 +6,6 @@ import static org.junit.Assert.assertEquals;
import org.junit.Test;
-
public class FixedBugs {
@Test
@@ -20,4 +19,14 @@ public class FixedBugs {
+ "END";
assertEquals(Deadlock, testString(machine));
}
+
+ @Test
+ public void testActionIdentifier() throws Exception {
+ String machine =
+ "MACHINE Test\n"
+ + "CONSTANTS ACTION\n"
+ + "PROPERTIES ACTION={1, 2, 3} \n"
+ + "END";
+ assertEquals(NoError, testString(machine));
+ }
}
--
GitLab