Added enum tests, adjusted grammar

Added some more enum tests for different situations (like as parameters or fields with enum refinements). Merged CorrectEnumResetMode into CorrectEnumUsage (redundant having a separate one that only tests resetting to null) Refactored enumCreate as suggested. Refactored grammar to follow Enumerate class.
liquid-java · rcosta358 · Apr 11, 2026 · Mar 3, 2026 · Mar 3, 2026 · Mar 4, 2026
commit e3e49d28b5a454822b319c47ff8addd89019d206
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumField.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumField.java
@@ -0,0 +1,23 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class CorrectEnumField {
+    enum Color {
+        Red, Green, Blue
+    }
+
+    @Refinement("color != Color.Blue")
+    Color color;
+
+    void setColor(@Refinement("c != Color.Blue") Color c) {
+        color = c;
+    }
+
+    public static void main(String[] args) {
+        CorrectEnumField cef = new CorrectEnumField();
+        cef.setColor(Color.Red);   // correct
+        cef.setColor(Color.Green); // correct
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumParam.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumParam.java
@@ -0,0 +1,19 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class CorrectEnumParam {
+    enum Status {
+        Active, Inactive, Pending
+    }
+
+    Status process(@Refinement("status == Status.Inactive") Status status) {
+        return Status.Active;
+    }
+
+    public static void main(String[] args) {
+        CorrectEnumParam cep = new CorrectEnumParam();
+        cep.process(Status.Inactive); // correct
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java
diff --git a/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java b/liquidjava-example/src/main/java/testSuite/CorrectEnumUsage.java
@@ -19,15 +19,27 @@ public CorrectEnumUsage() {}
 	public void setMode(Mode mode) {
 		this.mode = mode;
 	}
+
+	@StateRefinement(from="photoMode(this)", to="noMode(this)")
+	@StateRefinement(from="videoMode(this)", to="noMode(this)")
+	public void resetMode() {
+		this.mode = null;
+	}
 
 	@StateRefinement(from="photoMode(this)")
 	public void takePhoto() {}
+
+	@StateRefinement(from="videoMode(this)")
+	public void takeVideo() {}
 
 
 	public static void main(String[] args) {
 		// Correct
 		CorrectEnumUsage st = new CorrectEnumUsage();
-		st.setMode(Mode.Photo);
+		st.setMode(Mode.Photo);  // noMode -> photoMode
 		st.takePhoto();
+		st.resetMode();          // photoMode -> noMode
+		st.setMode(Mode.Video);  // noMode -> videoMode
+		st.takeVideo();
 	}
 }
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java b/liquidjava-example/src/main/java/testSuite/ErrorEnumNegation.java
@@ -0,0 +1,19 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class ErrorEnumNegation {
+    enum Status {
+        Active, Inactive, Pending
+    }
+
+    void process(@Refinement("status != Status.Inactive") Status status) {}
+
+    public static void main(String[] args) {
+        ErrorEnumNegation e = new ErrorEnumNegation();
+        e.process(Status.Active);   // correct
+        e.process(Status.Inactive); // error
+    }
+}
diff --git a/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java b/liquidjava-example/src/main/java/testingInProgress/EnumRefinementMessage.java
@@ -2,7 +2,7 @@
 
 import liquidjava.specification.Refinement;
 
-public class EnumRefinementMessage {
+class EnumRefinementMessage {
     enum Mode {
         Photo, Video, Unknown
     }

diff --git a/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4 b/liquidjava-verifier/src/main/antlr4/rj/grammar/RJ.g4
@@ -38,13 +38,14 @@ literalExpression:
 	|	literal						#lit
 	| 	ID 							#var
 	|	functionCall				#invocation
-	|	enumCall					#enum
+	|	enumerate					#enum
 	;
 
- functionCall:
+functionCall:
  		ghostCall
  	|	aliasCall
-	|	dotCall;
+	|	dotCall
+	;
 
 dotCall:
 		OBJECT_TYPE '(' args? ')'
@@ -56,8 +57,8 @@ ghostCall:
 aliasCall:
 	ID_UPPER '(' args? ')';
 
-enumCall: 
-	ENUM_CALL;
+enumerate: 
+	ENUM;
 
 args:	pred (',' pred)* ;
 
@@ -98,7 +99,7 @@ ARITHOP : '+'|'*'|'/'|'%';//|'-';
 
 BOOL    : 'true' | 'false';
 ID_UPPER: ([A-Z][a-zA-Z0-9]*);
-ENUM_CALL: [A-Z][a-zA-Z0-9_]* '.' [A-Z][a-zA-Z0-9_]*;
+ENUM: [A-Z][a-zA-Z0-9_]* '.' [A-Z][a-zA-Z0-9_]*;
 OBJECT_TYPE:
 		  (([a-zA-Z][a-zA-Z0-9]+) ('.' [a-zA-Z][a-zA-Z0-9]*)+);
 ID     	: '#'*[a-zA-Z_][a-zA-Z0-9_#]*;

diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java
@@ -239,11 +239,9 @@ private List<Expression> getArgs(ArgsContext args) throws LJError {
     }
 
     private Enumerate enumCreate(EnumContext enumContext) {
-        String enumText = enumContext.enumCall().getText();
-        int lastDot = enumText.lastIndexOf('.');
-        String enumTypeName = enumText.substring(0, lastDot);
-        String enumConstName = enumText.substring(lastDot + 1);
-        return new Enumerate(enumTypeName, enumConstName);
+        String enumText = enumContext.enumerate().getText();
+        String[] parts = enumText.split("\\.");
+        return new Enumerate(parts[0], parts[1]);
     }
 
     private Expression literalCreate(LiteralContext literalContext) throws LJError {