-
Notifications
You must be signed in to change notification settings - Fork 2
Guide to Implementing Your Own Protocols
This document walks through how to generate TypeScript APIs for a simple Adder web-service.
In the Adder web-service, clients either:
- Submit two integers to the server, and receive the sum; or
- Request to exit the service.
The Adder protocol can be located under
~/protocols/Adder.scr.
You can use the other web applications
under ~/case-studies as a template,
but this guide will walk through the steps
from scratch.
Note: This guide will require you to write new source code files
using a terminal editor. The Docker image comes with vim and nano
installed. If you wish to install additional software for editing, obtain
sudo access with the password dev.
We will create the Adder web-service under
the ~/case-studies directory.
This will hold both the server and client roles.
Run the following commands to initialise the Adder server as a Node application using TypeScript.
$ mkdir -p ~/case-studies/Adder
$ cd ~/case-studies/AdderRun the following commands to copy the package.json and tsconfig.json files from the Battleships application,
as the dependencies will be the same.
We need the build scripts and dependencies from
package.json, and the TypeScript project configurations fromtsconfig.json.
Optional:
You may also change the name and description fields of the
package.json file to refer to the Adder web-service.
$ cd /home/dev/case-studies/Adder
$ cp ../Battleships/package.json ../Battleships/tsconfig.json ./Run the following commands to set up the Node project.
$ cd /home/dev/case-studies/Adder
# Source code for server will go inside 'src'
$ mkdir src
# Install dependencies
$ npm iRun the following commands to initialise the Adder client as a React application using TypeScript.
$ cd /home/dev/case-studies/Adder
# Create React application with TypeScript project setup.
# This will take a couple of minutes...
$ npx create-react-app client --template typescript
# Install dependencies
$ cd client && npm iWe have the minimal scaffolding of the Adder web-service.
Run the following commands to generate the APIs for the
server.
The APIs will be generated under /home/dev/case-studies/Adder/src.
$ cd /home/dev/case-studies/Adder
$ codegen \
~/protocols/Adder.scr \ # use this Scribble file
Adder \ # generate Adder protocol
Svr \ # for Svr role
node \ # targeting Node endpoint
-o src \ # output to `src` pathRun the following commands to generate the APIs for the
client.
The APIs will be generated under /home/dev/case-studies/Adder/client/src.
# Note that this is the "client" subdirectory inside Adder.
$ cd /home/dev/case-studies/Adder/client
^^^^^^
$ codegen \
~/protocols/Adder.scr \ # use this Scribble file
Adder \ # generate Adder protocol
Client \ # for Client role
browser \ # targeting browser endpoint
-s Svr \ # with `Svr` as server role
-o src \ # output to `src` pathWe have the TypeScript APIs required for a communication-safe implementation of the Adder web-service.
We proceed to write the application logic for both endpoints, leveraging the generated APIs to guarantee communication-safety by construction.
Create the file, /home/dev/case-studies/Adder/src/index.ts, and add the following file content.
You may omit the comments, they are included here simply to guide you and provide context.
Here, we are simulating a 2-second delay at the server role when computing the sum. This property allows us to assess how our client endpoint responds to network delays and verify that channel reuse is impossible even under these conditions.
// =============
// Set up server
// =============
import express from "express";
import path from "path";
import http from "http";
import WebSocket from "ws";
const app = express();
// Serve client-side static files.
app.use(express.static(path.join(__dirname, "client")));
// Create WebSocket server.
const server = http.createServer(app);
const wss = new WebSocket.Server({ server });
// ==================
// Implement protocol
// ==================
import {
Session, // Holds named constructors for main EFSM states.
Svr, // Constructor for session runtime.
} from "./Adder/Svr";
// This function performs the sum after a simulated 2 second delay
const sumAfterTwoSeconds = (x: number, y: number) => new Promise<number>((resolve, reject) => {
setTimeout(() => resolve(x + y), 2000);
});
const adderServerLogic = (sessionID: string) => {
// This function gets invoked whenever a new session is created,
// and is assigned an unique identifier. It isn't particularly useful
// for the Adder web-service, but the other case studies (e.g. Battleships)
// make use of this to keep track of independent game states. You could
// try log the messages received along with the session ID to inspect the
// independent sessions.
const handleRequest = Session.Initial({
// Initial state handles a branching operation:
// either receiving 'ADD' with 2 numbers, or 'QUIT'.
ADD: async (Next, num1, num2) => {
// `Next` is a named constructor for successor states,
// which is useful for code-completion in editors/IDEs.
// `num1` and `num2` are inferred to be numbers.
const sum = await sumAfterTwoSeconds(num1, num2);
// Send the RES message with the sum, and continue
// onto the initial state by recursion.
return Next.RES([sum], handleRequest);
},
// Continue onto the terminal state,
// marked by `Session.Terminal`.
QUIT: Session.Terminal,
});
return handleRequest;
};
// ============
// Execute EFSM
// ============
new Svr(
wss,
(sessionID, role, reason) => {
// Simple cancellation handler
console.error(`${sessionID}: ${role} cancelled session because of ${reason}`);
},
adderServerLogic,
);
const PORT = process.env.PORT ?? 8080;
server.listen(PORT, () => {
console.log(`Listening on port ${PORT}...`);
});We proceed to implement the React application for the Client endpoint.
We need to implement a React component for each state of the Client's EFSM.
These states are located inside /home/dev/case-studies/Adder/client/src/Adder/Client,
and are prefixed with S__.tsx, as shown below.
The
.tsxfile extension denotes that the TypeScript source file also uses the JSX syntax extension.
$ ls -l /home/dev/case-studies/Adder/client/src/Adder/Client
total 52
-rw-r--r-- 1 dev dev 512 Dec 31 16:39 Cancellation.ts
-rw-r--r-- 1 dev dev 10484 Dec 31 16:39 Client.tsx
-rw-r--r-- 1 dev dev 752 Dec 31 16:39 EFSM.ts
-rw-r--r-- 1 dev dev 309 Dec 31 16:39 Message.ts
-rw-r--r-- 1 dev dev 285 Dec 31 16:39 Roles.ts
-rw-r--r-- 1 dev dev 983 Dec 31 16:39 S5.tsx # state
-rw-r--r-- 1 dev dev 352 Dec 31 16:39 S6.tsx # state
-rw-r--r-- 1 dev dev 1709 Dec 31 16:39 S7.tsx # state
-rw-r--r-- 1 dev dev 570 Dec 31 16:39 Session.ts
-rw-r--r-- 1 dev dev 717 Dec 31 16:39 Types.ts
-rw-r--r-- 1 dev dev 304 Dec 31 16:39 index.tsNote: your state identifiers may differ, but there should be only three state components generated.
By convention, we will group our component implementations in a subdirectory.
$ mkdir /home/dev/case-studies/Adder/client/src/componentsEach of the generated EFSM state components define an abstract React class component. To instantiate the session runtime for the web application, we need to define custom implementations of each state component.
The Client's EFSM defines three states:
- A send state to either send
ADDorQUITmessages (which is also the initial state); - A receive state pending the receipt of the
RESmessage with the sum; - A terminal state after sending the
QUITmessage.
Inspect each of the generated EFSM state components to figure out which state identifier corresponds to which state.
It is likely that the state with the lexicographically smallest identifier corresponds to the initial state, and the state with the second lexicographically smallest identifier corresponds to the terminal state.
The send state corresponds to S5.tsx at the time of writing.
If your send state has a different state identifier, you can confirm that
it is a send state by referring to the class doc.
$ cat /home/dev/case-studies/Adder/client/src/Adder/Client/S5.tsx
/* ...snip... */
/**
* __Sends to Svr.__ Possible message:
*
* * __QUIT__()
* * __ADD__(number, number)
*/
export default abstract class S5<ComponentState = {}> extends React.Component<Props, ComponentState>
{
/* ...snip... */
Create a React class component that inherits from this abstract base class.
Here we name the component SelectionScreen.tsx.
$ cd /home/dev/case-studies/Adder/client/src/components
$ touch SelectionScreen.tsxImplement the SelectionScreen component.
The sample code below displays two text boxes to keep track of the operands
for the ADD message, and exposes two buttons labelled Submit and Quit Adder
to trigger the ADD and QUIT selections respectively.
For simplicity, we will use the
localStorageAPI to keep track of the operands submitted to the Adder service. The other case studies use the React Context API to propagate the shared data.
// SelectionScreen.tsx
import React from 'react';
import { S5 } from '../Adder/Client';
// This UI component needs to keep track of the numbers entered
// by the user. React components can keep track of mutable state.
type ComponentState = {
num1: number,
num2: number,
};
export default class SelectionScreen extends S5<ComponentState> {
// To update the internal state, we call `this.setState(obj)`,
// where `obj` is an object literal mapping property names
// to their updated values.
state = {
num1: 0,
num2: 0,
};
// The `render` method corresponds to the view function
// explained in the literature. The view function returns the UI
// components to be rendered on the DOM.
render() {
// `this.ADD` is a component factory that takes a DOM event and a
// callback and returns a React component with the IO action bound
// inside. Here, we are building a React component named 'Submit' such that,
// when the user "clicks" on it, the callback is triggered and returns the
// payload to send along with the "ADD" message. The payload must be typed as
// a tuple of two numbers, as per the Scribble protocol specification.
const Submit = this.ADD('onClick', ev => {
const { num1, num2 } = this.state;
localStorage.setItem('operands', `${num1},${num2}`);
return [num1, num2];
});
// Likewise, `this.ADD` generates a React component that, when clicked on,
// sends the "QUIT" message with no payload (denoted by empty tuple).
const Quit = this.QUIT('onClick', ev => {
return [];
});
return (
<div>
<input
type='number'
placeholder='Num1'
// When the user changes their input in this textbox, interpret
// the input value as a Number and update the entry for `num1` in
// the component state. This allows `this.ADD` to access the latest value
// when sending the "ADD" message.
onChange={(ev) => this.setState({ num1: Number(ev.target.value) })}
/>
<input
type='number'
placeholder='Num2'
onChange={(ev) => this.setState({ num2: Number(ev.target.value) })}
/>
<Submit>
{
// Any UI component inside the "Submit" component will inherit the
// event listeners in the parent, so when the user clicks on the button labelled
// 'Submit', the behaviour for `this.ADD` described above will be triggered.
}
<button>Submit</button>
</Submit>
<hr />
<Quit>
<button>Quit Adder</button>
</Quit>
</div>
);
}
};The receive state corresponds to S7.tsx at the time of writing.
If your receive state has a different state identifier, you can confirm that
it is a receive state by referring to the class doc.
$ cat /home/dev/case-studies/Adder/client/src/Adder/Client/S7.tsx
/* ...snip... */
/**
* __Receives from Svr.__ Possible message:
*
* * __RES__(number)
*/
export default abstract class S7<ComponentState = {}> extends React.Component<Props, ComponentState>
{
/* ...snip... */
abstract RES(payload1: number, ): MaybePromise<void>;
};
Note: The abstract class defines an abstract method RES(number): void,
which functions as a hook,
as it is invoked by the session runtime once the message is received.
Create a React class component that inherits from this abstract base class.
Here we name the component WaitingScreen.tsx.
Recall that the Adder server takes 2 seconds to respond to an addition request. This React component will be rendered whilst waiting to receive the response from the Adder server, hence it is aptly named "WaitingScreen".
$ cd /home/dev/case-studies/Adder/client/src/components
$ touch WaitingScreen.tsxImplement the WaitingScreen component.
The sample code below displays some waiting text, and when the RES
message is received, it displays an alert that logs the sum of the operands.
The operands are accessed through the localStorage API in the same way
that they were stored through the SelectionScreen.tsx component.
// WaitingScreen.tsx
import React from 'react';
import { S7 } from '../Adder/Client';
export default class WaitingScreen extends S7 {
RES(sum: number) {
// Fetch operands from localStorage API.
const [num1, num2] = localStorage
.getItem('operands')!
.split(',')
.map(x => Number(x)) as [number, number];
// Display alert to user
alert(`${num1} + ${num2} = ${sum}`);
}
render() {
return (
<div>
<h2>Waiting for sum...</h2>
</div>
);
}
};The terminal state corresponds to S6.tsx at the time of writing.
If your terminal state has a different state identifier, you can confirm that
it is a terminal state by referring to the class doc.
$ cat /home/dev/case-studies/Adder/client/src/Adder/Client/S6.tsx
/* ...snip... */
/**
* __Terminal state__.
*/
export default abstract class S6<ComponentState = {}> extends React.Component<Props, ComponentState>
{
componentDidMount() {
this.props.terminate();
}
};
Create a React class component that inherits from this abstract base class.
Here we name the component EndScreen.tsx.
$ cd /home/dev/case-studies/Adder/client/src/components
$ touch EndScreen.tsxImplement the EndScreen component.
The sample code below displays a helpful message and nothing more.
More complex web applications can leverage the componentDidMount
hook to perform any required clean-up when the session terminates.
// EndScreen.tsx
import React from 'react';
import { S6 } from '../Adder/Client';
export default class EndScreen extends S6 {
render() {
return (
<div>
<h2>Closed Connection to Adder Service</h2>
<p>Please refresh the window to connect again.</p>
</div>
);
}
};React components define a hierarchy of UI views.
By construction from the create-react-app scaffolding, the
top of the hierarchy is defined in
/home/dev/case-studies/Adder/client/src/App.tsx.
Modify this component so that the main application renders the session runtime of the Adder protocol for the Client role. The instantiation of the session runtime requires some additional React components, which we label with footnotes in the code and explain later.
The session runtime itself is also a React component. It is responsible for:
- keeping track of the current EFSM state;
- rendering the custom implementation of the corresponding EFSM state; and
- ensuring that the IO actions made available on the DOM only corresponds to the permitted transitions in the current EFSM state.
// App.tsx
import React from 'react';
import './App.css';
// Import the session runtime component.
import { Client } from './Adder/Client';
// Import our custom state implementations.
import SelectionScreen from './components/SelectionScreen';
import WaitingScreen from './components/WaitingScreen';
import EndScreen from './components/EndScreen';
function App() {
const origin = window.location.origin;
const endpoint = origin.replace(/^http/, 'ws');
return (
<div className='App'>
<h1>Adder Service</h1>
<Client
endpoint={endpoint}
// Map each state identifier to the corresponding
// concrete state implementation.
states={{
S5: SelectionScreen,
S6: EndScreen,
S7: WaitingScreen,
}}
// {1}
waiting={
<div>
<p>Connection to Server...</p>
</div>
}
// {2}
connectFailed={
<div>
<p>ERROR: cannot connect to Server...</p>
</div>
}
// {3}
cancellation={(role, reason) => {
return (
<p>{role} cancelled session due to {reason}</p>
);
}}
/>
</div>
);
}
export default App;-
{1} defines the UI to be displayed when waiting for the session to start.
-
{2} defines the UI to be displayed if the Client fails to connect to the server.
-
{3} defines a function that is invoked whenever the session is cancelled before reaching the terminal state (e.g. if the Server goes down), and is parameterised with the role that cancelled the session and the reason (if any). This function renders the UI to be displayed when the session is cancelled.
This is used by game-based case studies (e.g. Noughts and Crosses, Battleships) to declare the current player as the winner if the opponent disconnected, as it interprets the opponent's disconnection as a forfeit.
We are now in a position to test the Adder web-service. Run the following command to build both the server and client endpoints. The TypeScript Compiler is executed to check for typing violations, and upon success, compiles both endpoints into JavaScript code that can be executed by the Node.js runtime and the browser respectively.
$ cd /home/dev/case-studies/Adder
$ npm run build
> [email protected] build /home/dev/case-studies/Adder
> tsc && cd client && npm run build && mv build client && rm -rf ../build/client && mv client ../build
/* ...snip... */Run the following command to start the Adder web-service.
$ cd /home/dev/case-studies/Adder
$ npm startNavigate to http://localhost:8080 on your browser to
use the Adder service.
Observe that, even though there is a delay between sending the
ADD message and receiving the RES message, by construction
from the generated APIs, it is impossible for the client to
submit another ADD message whilst waiting for the RES message.
This property seems trivial for the Adder example, but it is crucial for other use-cases such as the Travel Agency case study. where travellers should not be able to make more than one inquiry at a time.
Congratulations, you have implemented your first communication-safe web application!
We list some ideas for extending the Adder web-service with modern web programming practices:
- Modernise the UI using external libraries. Two popular examples are Material-UI and React-Bootstrap.
- Display the sum on the DOM rather than an alert. You can refer to the other case studies for how to propagate state using the React Context API, as well as how to extract common UI elements in individual components to reuse across different EFSM states.