Updated the protocol syntax to include its name and the

forward declaration of its states. Requiring states to be
forward declared helps to reduce the ammount of time a
typo in a state name can go unnoticed.

crates/btrun/src/fs_proto.rs

@@ -13,6 +13,13 @@ impl CallMsg for Open {
 }
 
 protocol! {
+    let name = FsProtocol;
+    let states = [
+        ServerInit, Listening,
+        Client,
+        FileInit, Open, Opened,
+        FileHandle,
+    ];
     ServerInit?Activate -> Listening;
 
     Client -> Client, service(Listening)!Query;
@@ -20,16 +27,16 @@ protocol! {
     Client?Query::Reply -> Client;
 
     Client -> Client, service(Listening)!Open;
-    Listening?Open -> Listening, Opened, Client!Open::Reply;
-    Client?Open::Reply -> Client, FileHandle;
+    Listening?Open -> Listening, Opened, Client!Open::Reply[Opened];
+    Client?Open::Reply[Opened] -> Client, FileHandle[Opened];
 
     FileInit?Activate -> FileInit;
     FileInit?Open -> Opened;
 
-    FileHandle -> FileHandle, Opened!FileOp;
+    FileHandle[Opened] -> FileHandle[Opened], Opened!FileOp;
     Opened?FileOp -> Opened, Client!FileOp::Reply;
-    FileClient?FileOp::Reply -> FileClient;
+    FileHandle?FileOp::Reply -> FileClient;
 
-    FileClient -> End, Opened!Close;
+    FileHandle[Opened] -> End, Opened!Close;
     Opened?Close -> End;
 }

crates/btrun/src/lib.rs

@@ -811,6 +811,11 @@ mod tests {
     // simple ping-pong protocol:
     //
     protocol! {
+        let name = PingPongProtocol;
+        let states = [
+            ClientInit, SentPing,
+            ServerInit, Listening,
+        ];
         ClientInit?Activate -> SentPing, Listening!Ping;
         ServerInit?Activate -> Listening;
         Listening?Ping -> End, SentPing!Ping::Reply;
@@ -1016,8 +1021,15 @@ mod tests {
 
     // Here's another protocol example. This is the Customer and Travel Agency protocol used as an
     // example in the survey paper "Behavioral Types in Programming Languages."
-    //
+    // Note that the Choosing state can send messages at any time, not just in response to another
+    // message because there is a transition from Choosing that doesn't use the receive operator
+    // (`?`).
     protocol! {
+        let name = TravelAgency;
+        let states = [
+            AgencyInit, Listening,
+            Choosing,
+        ];
         AgencyInit?Activate -> Listening;
         Choosing -> Choosing, Listening!Query|Accept|Reject;
         Listening?Query -> Listening, Choosing!Query::Reply;
@@ -1027,6 +1039,4 @@ mod tests {
         Listening?Reject -> End, Choosing!Reject:Reply;
         Choosing?Reject::Reply -> End;
     }
-    //
-    // The Choice message is from the runtime itself. It represents receiving input from a user.
 }

crates/btrun/src/sector_proto.rs

@@ -57,6 +57,8 @@ pub enum SectorMsgReply {
 }
 
 protocol! {
+    let name = SectorProtocol;
+    let states = [ServerInit, Listening, Client];
     ServerInit?Activate -> Listening;
     Client -> Client, service(Listening)!SectorMsg;
     Listening?SectorMsg -> Listening, Client!SectorMsg::Reply;