Session Type Demo (based on WIP code)

session.md

Session Type Demo

Models interactions between a user and an ATM based on the expository example in http://www.di.unito.it/~dezani/papers/sto.pdf

User perspective

Session Type:

!String. &{ success: ⊕{ deposit: !Real. ?Real. end
                      | withdraw: !Real. &{ dispense: end
                                          | overdraft: end
                                          }. end
                      }
          | failure: end
          }. end

Sequence Diagram (mermaid):

sequenceDiagram
User-->ATM: link
User-->>ATM: identifier : String
alt
ATM->>User: success
alt
User->>ATM: deposit
User-->>ATM: amount : Real
ATM-->>User: balance : Real
else
User->>ATM: withdraw
User-->>ATM: amount : Real
alt
ATM->>User: dispense
else
ATM->>User: overdraft
end
end
else
ATM->>User: failure
end

Possible Session Flows (4):

!identifier:String. &success. ⊕deposit. !amount:Real. ?balance:Real. end. 
!identifier:String. &success. ⊕withdraw. !amount:Real. &dispense. end. 
!identifier:String. &success. ⊕withdraw. !amount:Real. &overdraft. end. 
!identifier:String. &failure. end. 

ATM perspective

Session Type:

?String. ⊕{ success: &{ deposit: ?Real. !Real. end
                      | withdraw: ?Real. ⊕{ dispense: end
                                          | overdraft: end
                                          }. end
                      }
          | failure: end
          }. end

Sequence Diagram (mermaid):

sequenceDiagram
ATM-->User: link
User-->>ATM: identifier : String
alt
ATM->>User: success
alt
User->>ATM: deposit
User-->>ATM: amount : Real
ATM-->>User: balance : Real
else
User->>ATM: withdraw
User-->>ATM: amount : Real
alt
ATM->>User: dispense
else
ATM->>User: overdraft
end
end
else
ATM->>User: failure
end

Possible Session Flows (4):

?identifier:String. ⊕success. &deposit. ?amount:Real. !balance:Real. end. 
?identifier:String. ⊕success. &withdraw. ?amount:Real. ⊕dispense. end. 
?identifier:String. ⊕success. &withdraw. ?amount:Real. ⊕overdraft. end. 
?identifier:String. ⊕failure. end.