Revision f905918571b3c813811f21e6555d5dee61772506 (click the page title to view the current version)

Behavioral/WebSocketProtocol

Simplified Web Socket Protocol

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
webSocketOpenedClosed : WebSocket
    [ ready --> request=open && request.success --> opened -->> request=close && request.success --> closed --> closed ]
Compiling failed at line 22 column 1...
Duplicate name: WebSocket1Compiling failed at line 22 column 1...
Duplicate name: WebSocket1
WebSocket1
  states
    ready

WebSocket2
  request->open
    success
  states
    ready

WebSocket3
  states
    opened

WebSocket4
  request->close
    success
  states
    opened

WebSocket1
  states
    closed

WebSocket5
  states
    closed

webSocketOpenedFailed : WebSocket
    [ ready --> request=open && request.success --> opened -->> request=close && request.failure --> failed --> failed ]
  1. Web socket successfully opened but failed to be closed
webSocketFailed : WebSocket
    [ ready --> request=open && request.failure --> failed --> failed ]
|WebSocket |WebSocket |WebSocket |WebSocket |WebSocket |WebSocket
| |  request->open | |  request->close | |
| |    success | |    failure | |
|  ready |  ready |  opened | |  failed | failed
  1. Web socket failed to be opened
|WebSocket |WebSocket |WebSocket |WebSocket
| |  request->open | |
| |    failure | |
|  ready |  ready |  failed |  failed