Added enum tests

Added 2 error tests for enum: when setting null on a field with an enum refinement, and on a function parameter refinement. A successful error test was added as well to test backtracking to a null state.

Author: cheestree

liquidjava-example/src/main/java/testSuite/CorrectEnumResetMode.java

@@ -0,0 +1,44 @@
+package testSuite;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@SuppressWarnings("unused")
+@StateSet({"photoMode", "videoMode", "noMode"})
+class CorrectEnumResetMode {
+	enum Mode {
+		Photo, Video, Unknown
+	}
+
+	Mode mode;
+
+	@StateRefinement(to="noMode(this)")
+	public CorrectEnumResetMode() {}
+
+	@StateRefinement(from="noMode(this) && mode == Mode.Photo", to="photoMode(this)")
+	@StateRefinement(from="noMode(this) && mode == Mode.Video", to="videoMode(this)")
+	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) {
+		CorrectEnumResetMode st = new CorrectEnumResetMode();
+		st.setMode(Mode.Photo);  // noMode -> photoMode
+		st.takePhoto();
+		st.resetMode();          // photoMode -> noMode
+		st.setMode(Mode.Video);  // noMode -> videoMode
+		st.takeVideo();
+	}
+}

liquidjava-example/src/main/java/testSuite/ErrorEnumFunctionRefinement.java

@@ -0,0 +1,22 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class ErrorEnumFunctionRefinement {
+    enum Color { Red, Green, Blue }
+
+	Color c;
+
+	Color changeColor(@Refinement("newColor == Color.Red || newColor == Color.Green") Color newColor) {
+		c = newColor; // correct
+		return c;
+	}
+	
+	public static void main(String[] args) {
+		ErrorEnumFunctionRefinement e = new ErrorEnumFunctionRefinement();
+		e.changeColor(Color.Red); // correct
+		e.changeColor(Color.Blue); // error
+	}
+}

liquidjava-example/src/main/java/testSuite/ErrorEnumNull.java

@@ -0,0 +1,16 @@
+// Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+class ErrorEnumNull {
+	enum Color {
+		Red, Green, Blue
+	}
+	
+	public static void main(String[] args) {
+		@Refinement("c == Color.Red || c == Color.Green")
+		Color c = null; // error
+	}
+}