# Simplified Web Socket Protocol

```clafer
enum Request = open | close

abstract WebSocket
    xor request -> Request ?
        success
        failure
    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 ]
```

## Example scenarios

1. Web socket successfully opened and closed

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

<table border=1>
<tr>
<td>|WebSocket</td><td>WebSocket</td><td>|WebSocket</td><td>|WebSocket</td><td>|WebSocket</td><td>|WebSocket</td>
</tr><tr>
<td>|</td><td>&nbsp;&nbsp;request-&gt;open</td><td>|</td><td>|&nbsp;&nbsp;request-&gt;close</td><td>|</td><td>|</td>
</tr><tr>
<td>|</td><td>&nbsp;&nbsp;&nbsp;&nbsp;success</td><td>|</td><td>&nbsp;&nbsp;&nbsp;&nbsp;success</td><td>|</td><td>|</td>
</tr><tr>
<td>|&nbsp;&nbsp;ready</td><td>|&nbsp;&nbsp;ready</td><td>|&nbsp;&nbsp;opened</td><td>|</td><td>|&nbsp;&nbsp;closed</td><td>|&nbsp;&nbsp;closed</td>
</tr>
</table>

2. Web socket successfully opened but failed to be closed

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

<table border=1>
<tr>
<td>WebSocket</td><td>WebSocket</td><td>WebSocket</td><td>WebSocket</td><td>WebSocket</td><td>WebSocket</td>
</tr><tr>
<td></td><td>&nbsp;&nbsp;request-&gt;open</td><td></td><td>&nbsp;&nbsp;request-&gt;close</td><td></td><td></td>
</tr><tr>
<td></td><td>&nbsp;&nbsp;&nbsp;&nbsp;success</td><td></td><td>&nbsp;&nbsp;&nbsp;&nbsp;failure</td><td></td><td></td>
</tr><tr>
<td>&nbsp;&nbsp;ready</td><td>&nbsp;&nbsp;ready</td><td>&nbsp;&nbsp;opened</td><td></td><td>&nbsp;&nbsp;failed </td><td>&nbsp;failed </td>
</tr>
</table>

3. Web socket failed to be opened

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

<table border=1>
<tr>
<td>WebSocket</td><td>WebSocket</td><td>WebSocket</td><td>WebSocket</td>
</tr><tr>
<td></td><td>&nbsp;&nbsp;request-&gt;open</td><td></td><td></td>
</tr><tr>
<td></td><td>&nbsp;&nbsp;&nbsp;&nbsp;failure</td><td></td><td></td>
</tr><tr>
<td>&nbsp;&nbsp;ready</td><td>&nbsp;&nbsp;ready</td><td>&nbsp;&nbsp;failed</td><td>&nbsp;&nbsp;failed</td>
</tr>
</table>