Skip to content

Latest commit

 

History

History
156 lines (117 loc) · 4.68 KB

README.md

File metadata and controls

156 lines (117 loc) · 4.68 KB
Raw

SEVIA

SRML Games Equilibrium Verification via ISPL Analysis

This tool takes SRML file as an input and convert it to ISPL. It then runs MCMAS to check NE-Emptiness of the setting. Currently supporting memoryless fragment of SL.

SEVIA can be used online as a webservice from: http://eve.cs.ox.ac.uk/sevia.html

Instructions

Linux:

  • Copy the folder of SEVIA into MCMAS working directory.
  • Compile it by executing make command

MacOS:

  • Copy the (extracted) folder of SEVIA into MCMAS working directory.
  • Use Makefile_macos OR Makefile_macosx as the Makefile (rename it into Makefile)
  • Compile it by executing make command

Running SEVIA:

  • For RMG: your_pc_name[.../sevia]$ ./sevia -r name_of_the_input_file.rml
  • For CGS: your_pc_name[.../sevia]$ ./sevia -c name_of_the_input_file.rml

For verbose mode use -v option:

  • For RMG: your_pc_name[.../sevia]$ ./sevia -r -v name_of_the_input_file.rml
  • For CGS: your_pc_name[.../sevia]$ ./sevia -c -v name_of_the_input_file.rml

Makefile commands:

  • make : for compiling
  • make clean : for cleaning compiled files
  • make clean-out : for cleaning output folder

Naming the output file

  • The output file is available in folder ./output

If you run [yourpc@localhost sevia]$ ./sevia -[c/r] xyz.rml OR ./stic -[c/r] -v xyz.rml This will automatically name your generated ISPL file into xyz.ispl

If you run [yourpc@localhost sevia]$ ./sevia -[c/r] xyz.rml abc.ispl OR ./sevia -[c/r] -v xyz.rml abc.ispl This will name your generated ISPL file into abc.ispl

Input Format

A valid input is a (SRML) file containing:

modules module_name controls var_1,...,var_i
  init
  :: guard ~> var_1' := true/false ,..., var_i' := true/false;
   . . .
  :: guard ~> var_1' := true/false ,..., var_i' := true/false;
  update
  :: guard ~> var_1' := prop_formula ,..., var_i' := prop_formula;
   . . .
  :: guard ~> var_1' := prop_formula ,..., var_i' := prop_formula;
  goals
  :: LTL goal;

Formula Syntax

prop_formula syntax:
S := var | true | false | !S | S and S | S or S | S -> S | S <-> S

Module goals are represented as LTL formulae by the following syntax:
Z := var | true | false | !Z | Z and Z | Z or Z | X Z | F Z | G Z | Z -> Z | Z <-> Z

Example

  • This is matching pennies example
  • alice (resp. bob) holds coin ca (resp. cb)
  • They can flip their coins to either true or false
  init
  :: true ~> ca' := true;
  :: true ~> ca' := false;
  update
  :: true ~> ca' := true;
  :: true ~> ca' := false;
  goal
  :: X (ca <-> cb);
  
 module bob controls cb
  init
  :: true ~> cb' := false;
  :: true ~> cb' := true;
  update
  :: true ~> cb' := true;
  :: true ~> cb' := false;
  goal
  :: X !(ca <-> cb);


********************************************************
                        SEVIA          
  SRMLG Equilibrium Verification via ISPL Analysis        

*********************************************************
...
Compiling...

Translation finished
Output File: ./output.ispl
Compilation time (s): 0.000897
Running MCMAS on output file

Building reachable state space...
  Formula number 1: <<st_alice>> <<st_bob>> <<st_Env>> (alice, st_alice) (bob, st_bob) (Environment, st_Env) ((X (((! cb) || ca) && (cb || (! ca))) || [[alt_st_alice]] (alice, alt_st_alice) (! X (((! cb) || ca) && (cb || (! ca))))) && (X (! (((! cb) || ca) && (cb || (! ca)))) || [[alt_st_bob]] (bob, alt_st_bob) (! X (! (((! cb) || ca) && (cb || (! ca))))))), is FALSE in the model
execution time = 0.006
number of reachable states = 4
BDD memory in use = 8993824

Running Experiments

  1. Go to folder eve-py/src/experiments, there are 8 scripts:
    • bisim_ne_emptiness.sh
    • bisim_none_emptiness.sh
    • gossip_protocol_emptiness.sh
    • gossip_protocol_enash.sh
    • gossip_protocol_anash.sh
    • replica_control_emptiness.sh
    • replica_control_enash.sh
    • replica_control_anash.sh
  2. Execute the script <experiment_name>.sh using the command ./experiment_name.sh 8
  3. This will run the experiment "experiment_name" up until 8 steps.
  4. The experiment results are reported in the generated file exetime_experiment_name.txt with the following respective values separated by semicolons:
    • compilation time,
    • time for verifying the formula,
    • number of reachable states,
    • BDD memory size used in MCMAS engine,
    • the compiled ISPL file size,
    • whether there exists NE.

It will also generate textfile tcgen/totable.txt for table in latex. For more detailed instruction about the python files, see tcgen/README.txt