Normalize Forge/Electrum keywords in lexer

src/ltlLexer.py

@@ -1,6 +1,7 @@
 # Generated from ltl.g4 by ANTLR 4.13.2
 from antlr4 import *
 from io import StringIO
+import re
 import sys
 if sys.version_info[1] > 5:
     from typing import TextIO
@@ -92,7 +93,26 @@ class ltlLexer(Lexer):
 
     grammarFileName = "ltl.g4"
 
+    _keyword_map = {
+        "after": "AFTER",
+        "next_state": "NEXT_STATE",
+        "eventually": "EVENTUALLY",
+        "always": "ALWAYS",
+        "until": "UNTIL",
+    }
+
+    _keyword_pattern = re.compile(r"\b(" + "|".join(_keyword_map.keys()) + r")\b", re.IGNORECASE)
+
+    @classmethod
+    def _normalize_keywords(cls, text: str) -> str:
+        return cls._keyword_pattern.sub(lambda m: cls._keyword_map[m.group(1).lower()], text)
+
     def __init__(self, input=None, output:TextIO = sys.stdout):
+        if isinstance(input, str):
+            input = InputStream(self._normalize_keywords(input))
+        elif input is not None and hasattr(input, "strdata"):
+            input = InputStream(self._normalize_keywords(input.strdata))
+
         super().__init__(input, output)
         self.checkVersion("4.13.2")
         self._interp = LexerATNSimulator(self, self.atn, self.decisionsToDFA, PredictionContextCache())

src/ltlnode.py

@@ -10,13 +10,13 @@
 from spotutils import areEquivalent
 
 
-from ltlListener import ltlListener
-from antlr4 import CommonTokenStream, ParseTreeWalker
-from antlr4 import ParseTreeWalker, CommonTokenStream, InputStream
-from ltlLexer import ltlLexer
-from ltlParser import ltlParser
-from abc import ABC, abstractmethod
-import ltltoeng
+from ltlListener import ltlListener
+from antlr4 import CommonTokenStream, ParseTreeWalker
+from antlr4 import ParseTreeWalker, CommonTokenStream, InputStream
+from ltlLexer import ltlLexer
+from ltlParser import ltlParser
+from abc import ABC, abstractmethod
+import ltltoeng
 
 
 SUPPORTED_SYNTAXES = ['Classic', 'Forge', 'Electrum']
@@ -247,11 +247,11 @@ def __to_english__(self):
 
         return f"{lhs} until {rhs}"
 
-    def __forge__(self):
-        return f"({self.left.__forge__()} UNTIL {self.right.__forge__()})"
-    
-    def __electrum__(self):
-        return f"({self.left.__forge__()} UNTIL {self.right.__forge__()})"
+    def __forge__(self):
+        return f"({self.left.__forge__()} until {self.right.__forge__()})"
+
+    def __electrum__(self):
+        return f"({self.left.__electrum__()} until {self.right.__electrum__()})"
 
 
 class NextNode(UnaryOperatorNode):
@@ -266,11 +266,11 @@ def __to_english__(self):
         op = self.operand.__to_english__().rstrip('.')
         return f"in the next step, {op}"
 
-    def __forge__(self):
-        return f"(NEXT_STATE {self.operand.__forge__()})"
-    
-    def __electrum__(self):
-        return f"(AFTER {self.operand.__electrum__()})"
+    def __forge__(self):
+        return f"(next_state {self.operand.__forge__()})"
+
+    def __electrum__(self):
+        return f"(after {self.operand.__electrum__()})"
 
 
 class GloballyNode(UnaryOperatorNode):
@@ -296,11 +296,11 @@ def __to_english__(self):
         english = ltltoeng.choose_best_sentence(patterns)
         return english
 
-    def __forge__(self):
-        return f"(ALWAYS {self.operand.__forge__()})"
-    
-    def __electrum__(self):
-        return f"(ALWAYS {self.operand.__electrum__()})"
+    def __forge__(self):
+        return f"(always {self.operand.__forge__()})"
+
+    def __electrum__(self):
+        return f"(always {self.operand.__electrum__()})"
 
 
 class FinallyNode(UnaryOperatorNode):
@@ -325,11 +325,11 @@ def __to_english__(self):
 
         return f"eventually, {op}"
 
-    def __forge__(self):
-        return f"(EVENTUALLY {self.operand.__forge__()})"
-    
-    def __electrum__(self):
-        return f"(EVENTUALLY {self.operand.__electrum__()})"
+    def __forge__(self):
+        return f"(eventually {self.operand.__forge__()})"
+
+    def __electrum__(self):
+        return f"(eventually {self.operand.__electrum__()})"
 
 
 class OrNode(BinaryOperatorNode):
@@ -463,9 +463,9 @@ def __to_english__(self):
 
 
 
-def parse_ltl_string(s):
-    # Create an input stream from the string
-    input_stream = InputStream(s)
+def parse_ltl_string(s):
+    # Create an input stream from the string
+    input_stream = InputStream(s)
 
     # Create a lexer and a token stream
     lexer = ltlLexer(input_stream)

test/test_parsing.py

@@ -145,13 +145,16 @@ def test_parse_ltl_string(self):
             ("a <-> b", "(a <-> b)"),
             # Next
             ("NEXT_STATE a", "(X a)"),
-            # Eventually
-            ("EVENTUALLY a", "(F a)"),
-            # Globally
-            ("ALWAYS a", "(G a)"),
-            # Until
-            ("a UNTIL b", "(a U b)"),
-        ]
+            # Eventually
+            ("EVENTUALLY a", "(F a)"),
+            ("eventually a", "(F a)"),
+            # Globally
+            ("ALWAYS a", "(G a)"),
+            ("always a", "(G a)"),
+            # Until
+            ("a UNTIL b", "(a U b)"),
+            ("a until b", "(a U b)"),
+        ]
 
         for forge, classic in test_cases:
             with self.subTest(input=forge, expected=classic):
@@ -160,7 +163,7 @@ def test_parse_ltl_string(self):
 """
 Tests for the correspondence between Electrum and Classic LTL syntax.
 """
-class TestElectrumClassicSyntaxCorrespondence(unittest.TestCase):
+class TestElectrumClassicSyntaxCorrespondence(unittest.TestCase):
     def test_parse_ltl_string(self):
         test_cases = [
             # Literals
@@ -175,20 +178,50 @@ def test_parse_ltl_string(self):
             ("a -> b", "(a -> b)"),
             # Equivalence
             ("a <-> b", "(a <-> b)"),
-            # Next
-            ("AFTER a", "(X a)"),
-            # Eventually
-            ("EVENTUALLY a", "(F a)"),
-            # Globally
-            ("ALWAYS a", "(G a)"),
-            # Until
-            ("a UNTIL b", "(a U b)"),
-        ]
-
-        for forge, classic in test_cases:
-            with self.subTest(input=forge, expected=classic):
-                self.assertEqual(str(parse_ltl_string(forge)), str(parse_ltl_string(classic)))
-
+            # Next
+            ("AFTER a", "(X a)"),
+            ("after a", "(X a)"),
+            # Eventually
+            ("EVENTUALLY a", "(F a)"),
+            ("eventually a", "(F a)"),
+            # Globally
+            ("ALWAYS a", "(G a)"),
+            ("always a", "(G a)"),
+            # Until
+            ("a UNTIL b", "(a U b)"),
+            ("a until b", "(a U b)"),
+        ]
+
+        for forge, classic in test_cases:
+            with self.subTest(input=forge, expected=classic):
+                self.assertEqual(str(parse_ltl_string(forge)), str(parse_ltl_string(classic)))
+
+
+class TestForgeElectrumRendering(unittest.TestCase):
+    def test_forge_outputs_lowercase_keywords(self):
+        test_cases = [
+            ("X a", "(next_state a)"),
+            ("F a", "(eventually a)"),
+            ("G a", "(always a)"),
+            ("a U b", "(a until b)"),
+        ]
+
+        for classic, forge in test_cases:
+            with self.subTest(input=classic, expected=forge):
+                self.assertEqual(parse_ltl_string(classic).__forge__(), forge)
+
+    def test_electrum_outputs_lowercase_keywords(self):
+        test_cases = [
+            ("X a", "(after a)"),
+            ("F a", "(eventually a)"),
+            ("G a", "(always a)"),
+            ("a U b", "(a until b)"),
+        ]
+
+        for classic, electrum in test_cases:
+            with self.subTest(input=classic, expected=electrum):
+                self.assertEqual(parse_ltl_string(classic).__electrum__(), electrum)
+
 
 
 if __name__ == "__main__":