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

# Simplified Web Socket Protocol

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

```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

### Web socket successfully opened and closed

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

#### Trace 1

<table>
<tr>
<td>
```clafer
WebSocket11
  states
    ready
```
</td>
<td>
```clafer
WebSocket12
  states
    ready
  request->open
    success
```
</td>
<td>
```clafer
WebSocket13
  states
    opened
```
</td>
<td>
```clafer
WebSocket14
  states
    opened
  request->close
    success
```
</td>
<td>
```clafer
WebSocket15
  states
    closed
```
</td>
<td>
```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>
```clafer
WebSocket21
  states
    ready
```
</td>
<td>
```clafer
WebSocket22
  states
    ready
  request->open
    success
```
</td>
<td>
```clafer
WebSocket23
  states
    opened
```
</td>
<td>
```clafer
WebSocket24
  states
    opened
  request->close
    failure
```
</td>
<td>
```clafer
WebSocket25
  states
    failed
```
</td>
<td>
```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>
```clafer
WebSocket31
  states
    ready
```
</td>
<td>
```clafer
WebSocket32
  states
    ready
  request->open
    failure
```
</td>
<td>
```clafer
WebSocket33
  states
    failed
```
</td>
<td>
```clafer
WebSocket34
  states
    failed
```
</td>
</table>