# 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>
<tr>
<td>
```clafer
WebSocket1
  states
    ready
```
</td>
<td>
```clafer
WebSocket2
  request->open
    success
  states
    ready
```
</td>
<td>
```clafer
WebSocket3
  states
    opened
```
</td>
<td>
```clafer
WebSocket4
  request->close
    success
  states
    opened
```
</td>
<td>
```clafer
WebSocket5
  states
    closed
```
</td>
<td>
```clafer
WebSocket6
  states
    closed
```
</td>
</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>
<tr>
<td>
```clafer
WebSocket7
  states
    ready
```
</td>
<td>
```clafer
WebSocket8
  request->open
    success
  states
    ready
```
</td>
<td>
```clafer
WebSocket9
  states
    opened
```
</td>
<td>
```clafer
WebSocket10
  request->close
    failure
  states
    opened
```
</td>
<td>
```clafer
WebSocket11
  states
    failed
```
</td>
<td>
```clafer
WebSocket12
  states
    failed
```
</td>
</table>

3. Web socket failed to be opened

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

<table>
<tr>
<td>
```clafer
WebSocket13
  states
    ready
```
</td>
<td>
```clafer
WebSocket14
  request->open
    failure
  states
    ready
```
</td>
<td>
```clafer
WebSocket15
  states
    failed
```
</td>
<td>
```clafer
WebSocket16
  states
    failed
```
</td>
</table>