--- title: Behavioral Modeling - WebSocket Protocol categories: behavioral ... # Simplified Web Socket Protocol > Note: this is a contrived example, not the actual protocol. 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.
```clafer WebSocket11 states ready ``` ```clafer WebSocket12 states ready request->open success ``` ```clafer WebSocket13 states opened ``` ```clafer WebSocket14 states opened request->close success ``` ```clafer WebSocket15 states closed ``` ```clafer WebSocket16 states closed ```
### 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
```clafer WebSocket21 states ready ``` ```clafer WebSocket22 states ready request->open success ``` ```clafer WebSocket23 states opened ``` ```clafer WebSocket24 states opened request->close failure ``` ```clafer WebSocket25 states failed ``` ```clafer WebSocket26 states failed ```
### Web socket failed to be opened ```clafer webSocketFailed : WebSocket [ ready --> request=open && request.failure --> failed --> failed ] ``` #### Trace 3
```clafer WebSocket31 states ready ``` ```clafer WebSocket32 states ready request->open failure ``` ```clafer WebSocket33 states failed ``` ```clafer WebSocket34 states failed ```