Revision ec5473b372ac1209325b03fa234f1fe6f0e7b2fa (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 ]

WebSocket1
  states
    ready

WebSocket2
  request->open
    success
  states
    ready

WebSocket3
  states
    opened

WebSocket4
  request->close
    success
  states
    opened

WebSocket5
  states
    closed
Compiling failed at line 41 column 1...
Duplicate name: WebSocket6Compiling failed at line 41 column 1...
Duplicate name: WebSocket6
WebSocket6
  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
WebSocket6
  states
    ready

WebSocket7
  request->open
    success
  states
    ready

WebSocket8
  states
    opened

WebSocket9
  request->close
    failed
  states
    opened

WebSocket10
  states
    failed

WebSocket11
  states
    failed

webSocketFailed : WebSocket
    [ ready --> request=open && request.failure --> failed --> failed ]
  1. Web socket failed to be opened
|WebSocket |WebSocket |WebSocket |WebSocket
| |  request->open | |
| |    failure | |
|  ready |  ready |  failed |  failed