---
title: Behavioral Modeling - WebSocket Protocol
categories: behavioral
...

# Simplified Web Socket Protocol

> Note: this is a contrived example, not the actual protocol.

```{.clafer .links}
```

First, we'd like to express the states of the websocket and the transitions among them. 
When a websocket is created it starts in the state `ready`, which we model as the `initial` state.
Upon entering each state initially, the websocket is not accepting any requests. 
Furthermore, in the states `closed` and `failed`, the websocket is not accepting any requests permanently. 

The request, if exists, points to either `open` or `close`. 
The children of the request indicate `success` or `failure` of the request. 

```clafer
enum Request = open | close

abstract WebSocket
    xor states
        initial ready
            [ initially no request ]
            [ request=open -[request.success]-> opened ]
            [ request=open -[request.failure]-> failed ]
        opened 
            [ initially no request ]
            [ request=close -[request.success]->  closed ]
            [ request=close -[request.failure]->  failed ]
        closed --> closed
            [ no request ]
        failed --> failed
            [ no request ]
    xor request -> Request ?
        success
        failure
```

## Example scenarios

The example scenarios serve as test cases, whereby we can state the intended behavior of the websocket.
In each case, the constraint must be consistent with the behavior specified above; however, it can be underspecified.
For example, the socket can remain in the state `opened` for an arbitrary number of snapshots until the request to close is received.
We express that using the transition `-->>`.
In the other cases, state changes must occur in the next snapshot as required by `-->`. 

### Web socket successfully opened and closed

```clafer
webSocketOpenedClosed : WebSocket
    [ ready --> request=open && request.success --> opened -->> request=close && request.success --> closed --> closed ]
```

We call such a temporal constraint a *trace specification*. 

#### Trace 1

Since, the trace specification and the behavior of the websocket are consistent, a trace generator can produce the following trace.

<table>
<tr>
<td valign="top">
```clafer
WebSocket11
  states
    ready
```
</td>
<td valign="top">
```clafer
WebSocket12
  states
    ready
  request->open
    success
```
</td>
<td valign="top">
```clafer
WebSocket13
  states
    opened
```
</td>
<td valign="top">
```clafer
WebSocket14
  states
    opened
  request->close
    success
```
</td>
<td valign="top">
```clafer
WebSocket15
  states
    closed
```
</td>
<td valign="top">
```clafer
WebSocket16
  states
    closed
```
</td>
</table>

### Web socket successfully opened but failed to be closed

```clafer
webSocketOpenedFailed : WebSocket
    [ ready --> request=open && request.success --> opened -->> request=close && request.failure --> failed --> failed ]
```

#### Trace 2

<table>
<tr>
<td valign="top">
```clafer
WebSocket21
  states
    ready
```
</td>
<td valign="top">
```clafer
WebSocket22
  states
    ready
  request->open
    success
```
</td>
<td valign="top">
```clafer
WebSocket23
  states
    opened
```
</td>
<td valign="top">
```clafer
WebSocket24
  states
    opened
  request->close
    failure
```
</td>
<td valign="top">
```clafer
WebSocket25
  states
    failed
```
</td>
<td valign="top">
```clafer
WebSocket26
  states
    failed
```
</td>
</table>

### Web socket failed to be opened

```clafer
webSocketFailed : WebSocket
    [ ready --> request=open && request.failure --> failed --> failed ]
```

#### Trace 3

<table>
<tr>
<td valign="top">
```clafer
WebSocket31
  states
    ready
```
</td>
<td valign="top">
```clafer
WebSocket32
  states
    ready
  request->open
    failure
```
</td>
<td valign="top">
```clafer
WebSocket33
  states
    failed
```
</td>
<td valign="top">
```clafer
WebSocket34
  states
    failed
```
</td>
</table>