SEVIA Online

This is SEVIA (SRML Verification via ISPL Analysis) online. This tool compile SRML code into ISPL code and calls MCMAS to verify SL formulae. Using this we can solve (Nash equilibrium) Non-Emptiness problem or verify manually inputted SL formulae. SEVIA accepts both SL formulae (defined in imperfect recall semantics) and SL[1G] formulae (defined in perfect recall semantics). The syntax guide for SL formulae can be found here.

Input your SRML code describing your multi-agent system/game by using either:

  1. Via Upload; you can upload your SRML code file and run SEVIA,
  2. Via TextArea; you can write or copy/paste your SRML code in the designated text area and run SEVIA.



To run:

  1. chose the modelling of the game (RMG or CGS),
  2. choose the preferred input method (Via Upload or Via TextArea),
  3. select from the dropdown list (Non-Emptiness or Input SL Formula),
  4. click the "Run" button to start computing.





Input your SRML code via file upload

Select modelling:

Select problem to solve:

Input SL formulae below. End each formula with a semi-colon ";".


Select text file to upload:

(Time limit: 300 seconds)

Input your SRML code via TextArea

Select modelling:

Select problem to solve:

Input SL formulae below. End each formula with a semi-colon ";".




Insert SRML code here:


(Time limit: 300 seconds)