Setting up unittest automation (#84)

* Added tests

* Trying to setup test automation

* Double check

* Another unit test try

* What happens if I remove conda?

* Could this be it?

* LTL interps depend on arch?

* Try this?

* This?

* Better?

* Maybe this updates some things?

* Better?

* ReGen parser

Author: sidprasad

.github/workflows/unittest.yaml

@@ -0,0 +1,25 @@
+name: Run Unit Tests
+
+on:
+  pull_request:
+    branches:
+      - main  # Run tests on pull requests targeting the 'main' branch
+
+jobs:
+  test:
+    runs-on: ubuntu-latest
+
+    steps:
+    # Step 1: Check out the code
+    - name: Check out code
+      uses: actions/checkout@v3
+
+    # Step 2: Build the Docker image
+    - name: Build Docker image
+      run: |
+        docker build -t ltltutor .
+
+    # Step 3: Run tests inside the Docker container
+    - name: Run tests in Docker container
+      run: |
+        docker run --rm ltltutor /bin/bash -c "source /venv/bin/activate && python -m unittest discover -s test -p 'test_*.py'"

runtests.sh

@@ -0,0 +1,7 @@
+#!/bin/bash
+
+# filepath: /home/sid/Desktop/ltltutor/run-tests.sh
+
+
+# Run the unittests
+python -m unittest discover -s test -p "test_*.py"

src/ltlnode.py

@@ -1,16 +1,22 @@
 # Description: This file contains the classes for the nodes of the LTL syntax tree.
 
+import os
+
+
+### TODO: Ideally, this should not be in 
+### src, but mocked in the test directory.
+
+
+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
-from spotutils import areEquivalent
-import random
 import ltltoeng
-import re
-
 
 
 SUPPORTED_SYNTAXES = ['Classic', 'Forge', 'Electrum']
@@ -26,12 +32,6 @@
 FINALLY_SYMBOL = 'F'
 UNTIL_SYMBOL = 'U'
 
-  
-## TODO: Too much is based on the Exact syntax. We should be able to
-## switch syntaxes. Should this be server side or client side?
-## If server side, we should have a way to switch syntaxes (__str__ vs __str__(syntax))
-
-
 
 class LTLNode(ABC):
     def __init__(self, type):

src/spotutils.py

@@ -32,13 +32,6 @@
 
 
 def areEquivalent(formula1, formula2):
-    
-    # Parse the formulas
-    # f1 = spot.formula(str(formula1))
-    # f2 = spot.formula(str(formula2))
-
-    # Check if they are equivalent
-    #return spot.formula.are_equivalent(f1, f2)
     return isSufficientFor(formula1, formula2) and isNecessaryFor(formula1, formula2)
 
 

test/test_ltlnode.py

@@ -1,9 +1,21 @@
 import unittest
-import codebook
+import sys
+import os
+
+
+# Add the src directory to sys.path
+sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), "../src")))
+
+
 from ltlnode import parse_ltl_string
+import codebook
 
 
-class TestCodebook(unittest.TestCase):
+"""
+Test cases for the conceptual mutation operators in the LTL misconceptions codebook.
+"""
+class TestConceptualMutator(unittest.TestCase):
+    
     def apply_and_check_misconception(self, code, test_cases):
         """
         Helper function to test multiple input/output pairs for a given misconception code.

test/test_codebook.py test/test_mutation.py

@@ -0,0 +1,108 @@
+import unittest
+import sys
+import os
+
+# Add the src directory to sys.path
+sys.path.insert(0, os.path.abspath(os.path.join(os.path.dirname(__file__), "../src")))
+
+from ltlnode import *
+
+
+## LTL String --> AST Node
+class TestParseLTLString(unittest.TestCase):
+    def test_parse_ltl_string(self):
+        test_cases = [
+            ("a", LiteralNode),
+            ("(abc)", LiteralNode),
+            ("a & b", AndNode),
+            ("a | b", OrNode),
+            ("a & b", AndNode),
+            ("a | b", OrNode),
+            ("!a", NotNode),
+            ("a -> b", ImpliesNode),
+            ("a <-> b", EquivalenceNode),
+            ("X(a)", NextNode),
+            ("F(a)", FinallyNode),
+            ("G(a)", GloballyNode),
+            ("X (a & b)", NextNode),
+            ("(X a) & b", AndNode),
+            ("(X a) | b", OrNode),
+            ("G((X a) | b)", GloballyNode),
+            ("a U b", UntilNode),
+            ("a & (b | c)", AndNode),
+            ("(a & b) | c", OrNode)
+        ]
+
+        for input_str, expected_node in test_cases:
+            with self.subTest(input=input_str, expected=expected_node):
+                self.assertIsInstance(parse_ltl_string(input_str), expected_node)
+
+
+"""
+Tests for the correspondence between Forge and Classic LTL syntax.
+"""
+class TestForgeClassicSyntaxCorrespondence(unittest.TestCase):
+    def test_parse_ltl_string(self):
+        test_cases = [
+            # Literals
+            ("a", "a"),
+            # Conjunction
+            ("a & b", "(a & b)"),
+            # Disjunction
+            ("a | b", "(a | b)"),
+            # Negation
+            ("!a", "!a"),
+            # Implication
+            ("a -> b", "(a -> b)"),
+            # Equivalence
+            ("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)"),
+        ]
+
+        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)))
+
+"""
+Tests for the correspondence between Electrum and Classic LTL syntax.
+"""
+class TestElectrumClassicSyntaxCorrespondence(unittest.TestCase):
+    def test_parse_ltl_string(self):
+        test_cases = [
+            # Literals
+            ("a", "a"),
+            # Conjunction
+            ("a & b", "(a & b)"),
+            # Disjunction
+            ("a | b", "(a | b)"),
+            # Negation
+            ("!a", "!a"),
+            # Implication
+            ("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)))
+
+
+
+if __name__ == "__main__":
+    unittest.main()