Add Test with Typestates

Author: rcosta358

liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_typestate_correct/Counter.java

@@ -0,0 +1,23 @@
+package testSuite.classes.state_refinement_no_to_typestate_correct;
+
+import liquidjava.specification.StateRefinement;
+import liquidjava.specification.StateSet;
+
+@StateSet({"empty", "one", "many"})
+public class Counter {
+
+    @StateRefinement(to="empty(this)")
+    public Counter() {}
+
+    @StateRefinement(from="empty(this)", to="one(this)")
+    public void addFirst() {}
+
+    @StateRefinement(from="one(this)", to="many(this)")
+    public void addSecond() {}
+
+    @StateRefinement(from="one(this) || many(this)")
+    public void inspect() {}
+
+    @StateRefinement(from="many(this)")
+    public void consumeOne() {}
+}

liquidjava-example/src/main/java/testSuite/classes/state_refinement_no_to_typestate_correct/Test.java

@@ -0,0 +1,12 @@
+package testSuite.classes.state_refinement_no_to_typestate_correct;
+
+public class Test {
+
+    public void test() {
+        Counter counter = new Counter();
+        counter.addFirst();
+        counter.addSecond();
+        counter.inspect();
+        counter.consumeOne();
+    }
+}