Add Connection Example

Author: rcosta358

pages/examples/connection.md

@@ -0,0 +1,53 @@
+---
+title: Connection
+parent: Examples
+nav_order: 6
+permalink: /examples/connection/
+description: A typestate protocol with a value-dependent conditional transition.
+---
+
+# Connection
+
+This example models a small object protocol where the target state of `connect` depends on a boolean parameter. Because the transition is value-dependent, this protocol does not encode to a DFA based only on the current state and method call.
+
+```java
+import liquidjava.specification.*;
+
+@StateSet({"disconnected", "guest", "authenticated"})
+public class Connection {
+    @StateRefinement(to="disconnected()")
+    public Connection() {}
+
+    @StateRefinement(from="disconnected()", to="hasToken ? authenticated() : guest()")
+    public void connect(boolean hasToken) {}
+
+    @StateRefinement(from="guest() && hasToken", to="authenticated()")
+    public void authenticate(boolean hasToken) {}
+
+    @StateRefinement(from="authenticated()")
+    public void sendData() {}
+
+    @StateRefinement(from="guest() || authenticated()", to="disconnected()")
+    public void disconnect() {}
+}
+```
+
+```java
+Connection conn = new Connection();
+conn.connect(true);
+conn.sendData();
+conn.disconnect();
+```
+
+```java
+Connection conn = new Connection();
+conn.connect(false);
+conn.sendData(); // State Refinement Error
+```
+
+LiquidJava enforces the intended protocol:
+
+- The `connect` method can be called from `disconnected()`, and the target state depends on the value of `hasToken`
+- The `authenticate` method can only be called from `guest()`, and only transitions to `authenticated()` if `hasToken` is true
+- The `sendData` method can only be called from `authenticated()`
+- The `disconnect` method can be called from either `guest()` or `authenticated()`, and always transitions back to `disconnected()`

pages/examples/downloader.md

@@ -14,16 +14,16 @@ This example models a simple downloader object that tracks the progress of a dow
 @Ghost("int progress")
 @StateSet({"created", "downloading", "completed"})
 public class Downloader {
-    @StateRefinement(to="created(this) && progress(this) == 0")
+    @StateRefinement(to="created() && progress() == 0")
     public Downloader() {}
 
-    @StateRefinement(from="created(this) && progress(this) == 0", to="downloading(this) && progress(this) == 0")
+    @StateRefinement(from="created() && progress() == 0", to="downloading() && progress() == 0")
     public void start() {}
 
-    @StateRefinement(from="downloading(this)", to="downloading(this) && progress(this) == percentage")
-    public void update(@Refinement("percentage > progress(this)") int percentage) {}
+    @StateRefinement(from="downloading()", to="downloading() && progress() == percentage")
+    public void update(@Refinement("percentage > progress()") int percentage) {}
 
-    @StateRefinement(from="downloading(this) && progress(this) == 100", to="completed(this)")
+    @StateRefinement(from="downloading() && progress() == 100", to="completed()")
     public void finish() {}
 }
 ```

pages/examples/reentrant-lock.md

@@ -1,7 +1,7 @@
 ---
 title: ReentrantLock
 parent: Examples
-nav_order: 6
+nav_order: 7
 permalink: /examples/reentrant-lock/
 description: An external typestate refinement for ReentrantLock.
 ---