Benchmark Gallery

17 real-world and classic protocols expressed as session types. Every benchmark has been verified through the full reticulate pipeline: parse, build state space, check lattice properties, and render the Hasse diagram.

17 Protocols
6 Use Parallel
17 Are Lattices
114 Total States

1. Java Iterator ✓

The java.util.Iterator protocol: repeatedly call hasNext, then next if TRUE or stop if FALSE.

rec X . hasNext . +{TRUE: next . X, FALSE: end}
4 states 4 transitions 2 SCCs
Hasse Diagram
0 ⊥ end 2 ⊤ hasNext 3 +{TRUE, FALSE} 2->3 hasNext 3->0 FALSE 4 next 3->4 TRUE 4->2 next

Analyze interactively →

2. File Object ✓

A file handle: open, then repeatedly read until EOF, then close. Models the classic open/read/close lifecycle.

open . rec X . read . +{data: X, eof: close . end}
5 states 5 transitions 4 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ open 3 read 1->3 open 4 +{data, eof} 3->4 read 4->3 data 5 close 4->5 eof 5->0 close

Analyze interactively →

3. SMTP ✓

Simplified SMTP session: connect, EHLO, then loop sending mail (MAIL/RCPT/DATA with OK or ERR) or QUIT.

connect . ehlo . rec X . &{mail: rcpt . data . +{OK: X, ERR: X}, quit: end}
7 states 8 transitions 4 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ connect 2 ehlo 1->2 connect 4 &{mail, quit} 2->4 ehlo 4->0 quit 5 rcpt 4->5 mail 6 data 5->6 rcpt 7 +{OK, ERR} 6->7 data 7->4 OK 7->4 ERR

Analyze interactively →

4. HTTP Connection ✓

A persistent HTTP connection: connect, then repeatedly send requests (with various response codes) or close.

connect . rec X . &{request: +{OK200: readBody . X, ERR4xx: X, ERR5xx: X}, close: end}
5 states 7 transitions 3 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ connect 3 &{request, close} 1->3 connect 3->0 close 4 +{OK200, ERR4xx, ERR5xx} 3->4 request 4->3 ERR4xx 4->3 ERR5xx 5 readBody 4->5 OK200 5->3 readBody

Analyze interactively →

5. OAuth 2.0 ✓

OAuth 2.0 authorization code flow: request authorization, obtain token, then use/refresh/revoke the token.

requestAuth . +{GRANTED: getToken . +{TOKEN: rec X . &{useToken: X, refreshToken: +{OK: X, EXPIRED: end}, revoke: end}, ERROR: end}, DENIED: end}
7 states 11 transitions 6 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ requestAuth 2 +{GRANTED, DENIED} 1->2 requestAuth 2->0 DENIED 3 getToken 2->3 GRANTED 4 +{TOKEN, ERROR} 3->4 getToken 4->0 ERROR 6 &{useToken, refreshToken, revoke} 4->6 TOKEN 6->0 revoke 6->6 useToken 7 +{OK, EXPIRED} 6->7 refreshToken 7->0 EXPIRED 7->6 OK

Analyze interactively →

6. Two-Buyer ∥ ✓

The two-buyer protocol: lookup an item, get price, then two buyers concurrently propose; buyer B may accept and pay or reject.

lookup . getPrice . (proposeA . end || proposeB . +{ACCEPT: pay . end, REJECT: end})
10 states 14 transitions 10 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ lookup 2 getPrice 1->2 lookup 7 (proposeA, proposeB) 2->7 getPrice 3 (end, proposeB) 4 (end, +{ACCEPT, REJECT}) 3->4 proposeB 4->0 REJECT 5 (end, pay) 4->5 ACCEPT 5->0 pay 6 (proposeA, end) 6->0 proposeA 7->3 proposeA 8 (proposeA, +{ACCEPT, REJECT}) 7->8 proposeB 8->4 proposeA 8->6 REJECT 9 (proposeA, pay) 8->9 ACCEPT 9->5 proposeA 9->6 pay

Analyze interactively →

7. MCP ∥ ✓

AI agent Model Context Protocol: initialize, then concurrently handle tool calls/listing/shutdown and notifications.

initialize . (rec X . &{callTool: +{RESULT: X, ERROR: X}, listTools: X, shutdown: end} || rec Y . +{NOTIFICATION: Y, DONE: end})
7 states 17 transitions 5 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ initialize 4 (&{callTool, listTools, shutdown}, +{NOT… 1->4 initialize 2 (end, +{NOTIFICATION, DONE}) 2->0 DONE 2->2 NOTIFICATION 3 (&{callTool, listTools, shutdown}, end) 3->0 shutdown 3->3 listTools 5 (+{RESULT, ERROR}, end) 3->5 callTool 4->2 shutdown 4->3 DONE 4->4 listTools 4->4 NOTIFICATION 6 (+{RESULT, ERROR}, +{NOTIFICATION, DONE}… 4->6 callTool 5->3 RESULT 5->3 ERROR 6->4 RESULT 6->4 ERROR 6->5 DONE 6->6 NOTIFICATION

Analyze interactively →

8. A2A ✓

Google's Agent-to-Agent protocol: send a task, then poll for status (WORKING/COMPLETED/FAILED) with cancellation support.

sendTask . rec X . +{WORKING: &{getStatus: X, cancel: end}, COMPLETED: getArtifact . end, FAILED: end}
5 states 7 transitions 4 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ sendTask 3 +{WORKING, COMPLETED, FAILED} 1->3 sendTask 3->0 FAILED 4 &{getStatus, cancel} 3->4 WORKING 5 getArtifact 3->5 COMPLETED 4->0 cancel 4->3 getStatus 5->0 getArtifact

Analyze interactively →

9. File Channel ∥ ✓

A file channel with concurrent read/write streams: open, then parallel read and write loops, then close.

open . +{OK: (rec X . &{read: X, doneRead: end} || rec Y . &{write: Y, doneWrite: end}) . close . end, ERR: end}
7 states 12 transitions 7 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ open 2 +{OK, ERR} 1->2 open 2->0 ERR 6 (&{read, doneRead}, &{write, doneWrite}) 2->6 OK 3 close 3->0 close 4 (end, &{write, doneWrite}) 4->3 doneWrite 4->4 write 5 (&{read, doneRead}, end) 5->3 doneRead 5->5 read 6->4 doneRead 6->5 doneWrite 6->6 read 6->6 write

Analyze interactively →

10. ATM ✓

An ATM session: insert card, enter PIN, authenticate, then perform banking operations or eject card.

insertCard . enterPIN . +{AUTH: rec X . &{checkBalance: X, withdraw: +{OK: X, INSUFFICIENT: X}, deposit: X, ejectCard: end}, REJECTED: ejectCard . end}
7 states 11 transitions 6 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ insertCard 2 enterPIN 1->2 insertCard 3 +{AUTH, REJECTED} 2->3 enterPIN 5 &{checkBalance, withdraw, deposit, eject… 3->5 AUTH 7 ejectCard 3->7 REJECTED 5->0 ejectCard 5->5 checkBalance 5->5 deposit 6 +{OK, INSUFFICIENT} 5->6 withdraw 6->5 OK 6->5 INSUFFICIENT 7->0 ejectCard

Analyze interactively →

11. Reentrant Lock ✓

A reentrant lock protocol: repeatedly lock/unlock with optional condition variable support (await/signal), or close.

rec X . &{lock: &{unlock: X, newCondition: await . signal . unlock . X}, close: end}
6 states 7 transitions 2 SCCs
Hasse Diagram
0 ⊥ end 2 ⊤ &{lock, close} 2->0 close 3 &{unlock, newCondition} 2->3 lock 3->2 unlock 4 await 3->4 newCondition 5 signal 4->5 await 6 unlock 5->6 signal 6->2 unlock

Analyze interactively →

12. WebSocket ∥ ✓

A WebSocket connection: connect, then if open, concurrently send/ping and receive messages/pong/close events.

connect . +{OPEN: (rec X . &{send: X, ping: X, closeSend: end} || rec Y . +{MESSAGE: Y, PONG: Y, CLOSE: end}), REFUSED: end}
6 states 15 transitions 6 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ connect 2 +{OPEN, REFUSED} 1->2 connect 2->0 REFUSED 5 (&{send, ping, closeSend}, +{MESSAGE, PO… 2->5 OPEN 3 (end, +{MESSAGE, PONG, CLOSE}) 3->0 CLOSE 3->3 MESSAGE 3->3 PONG 4 (&{send, ping, closeSend}, end) 4->0 closeSend 4->4 send 4->4 ping 5->3 closeSend 5->4 CLOSE 5->5 send 5->5 ping 5->5 MESSAGE 5->5 PONG

Analyze interactively →

13. DB Transaction ✓

A database transaction: begin, then repeatedly query or update (with results or errors), then commit or rollback.

begin . rec X . &{query: +{RESULT: X, ERROR: X}, update: +{ROWS: X, ERROR: X}, commit: end, rollback: end}
5 states 9 transitions 3 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ begin 3 &{query, update, commit, rollback} 1->3 begin 3->0 commit 3->0 rollback 4 +{RESULT, ERROR} 3->4 query 5 +{ROWS, ERROR} 3->5 update 4->3 RESULT 4->3 ERROR 5->3 ROWS 5->3 ERROR

Analyze interactively →

14. Pub/Sub ✓

A publish/subscribe client: connect, then subscribe, unsubscribe, poll for messages, or disconnect.

connect . rec X . &{subscribe: X, unsubscribe: X, poll: +{MSG: X, EMPTY: X}, disconnect: end}
4 states 7 transitions 3 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ connect 3 &{subscribe, unsubscribe, poll, disconne… 1->3 connect 3->0 disconnect 3->3 subscribe 3->3 unsubscribe 4 +{MSG, EMPTY} 3->4 poll 4->3 MSG 4->3 EMPTY

Analyze interactively →

15. DNS Resolver ✓

A DNS resolver: repeatedly query with various outcomes (ANSWER, NXDOMAIN, SERVFAIL, TIMEOUT with retry/abandon), or close.

rec X . &{query: +{ANSWER: X, NXDOMAIN: X, SERVFAIL: X, TIMEOUT: &{retry: X, abandon: end}}, close: end}
4 states 8 transitions 2 SCCs
Hasse Diagram
0 ⊥ end 2 ⊤ &{query, close} 2->0 close 3 +{ANSWER, NXDOMAIN, SERVFAIL, TIMEOUT} 2->3 query 3->2 ANSWER 3->2 NXDOMAIN 3->2 SERVFAIL 4 &{retry, abandon} 3->4 TIMEOUT 4->0 abandon 4->2 retry

Analyze interactively →

16. Reticulate Pipeline ∥ ✓

The reticulate web demo's own analysis pipeline as a session type. Verification and rendering run concurrently via the parallel constructor — a self-referential example.

input . parse . +{OK: buildStateSpace . +{OK: (checkLattice . checkTermination . checkWFPar . end || renderDiagram . end) . returnResult . end, ERROR: end}, ERROR: end}
14 states 18 transitions 14 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ input 2 parse 1->2 input 3 +{OK, ERROR} 2->3 parse 3->0 ERROR 4 buildStateSpace 3->4 OK 5 +{OK, ERROR} 4->5 buildStateSpace 5->0 ERROR 9 (checkLattice, renderDiagram) 5->9 OK 6 returnResult 6->0 returnResult 7 (end, renderDiagram) 7->6 renderDiagram 8 (checkLattice, end) 10 (checkTermination, end) 8->10 checkLattice 9->8 renderDiagram 11 (checkTermination, renderDiagram) 9->11 checkLattice 12 (checkWFPar, end) 10->12 checkTermination 11->10 renderDiagram 13 (checkWFPar, renderDiagram) 11->13 checkTermination 12->6 checkWFPar 13->7 checkWFPar 13->12 renderDiagram

Analyze interactively →

17. GitHub CI Workflow ∥ ✓

A GitHub Actions CI/CD pipeline: trigger, checkout, setup, then parallel lint and test jobs, then deploy on success (with rollback on failure) or stop on failure.

trigger . checkout . setup . (lint . end || test . end) . +{PASS: deploy . +{OK: end, FAIL: rollback . end}, FAIL: end}
11 states 13 transitions 11 SCCs
Hasse Diagram
0 ⊥ end 1 ⊤ trigger 2 checkout 1->2 trigger 3 setup 2->3 checkout 10 (lint, test) 3->10 setup 4 +{PASS, FAIL} 4->0 FAIL 5 deploy 4->5 PASS 6 +{OK, FAIL} 5->6 deploy 6->0 OK 7 rollback 6->7 FAIL 7->0 rollback 8 (end, test) 8->4 test 9 (lint, end) 9->4 lint 10->8 lint 10->9 test

Analyze interactively →