eve-mas/eve-parity

Equilibrium Verification Environment (EVE) is a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems.

EVE

Equilibrium Verification Environment

EVE (Equilibrium Verification Environment) is a formal verification tool for the automated analysis of temporal equilibrium properties of concurrent and multi-agent systems represented as multi-player games (see rational verification). Systems/Games in EVE are modelled using the Simple Reactive Module Language (SRML) as a collection of independent system components (players/agents in a game). These components/players are assumed to have goals expressed using Linear Temporal Logic (LTL) formulae. EVE checks for the existence of Nash equilibria in such systems and can be used to do rational synthesis and verification automatically.

We are always interested in improving EVE (e.g., faster techniques, new use cases, etc.). Please feel free to contact us for potential collaborations.

EVE ONLINE

EVE can be used via webservice from https://eve.cs.ox.ac.uk/eve

PUBLICATION

• J. Gutierrez, M. Najib, G. Perelli, and M. Wooldridge. Automated Temporal Equilibrium Analysis: Verification and Synthesis of Multi-Player Games. In Artificial Intelligence, 2020. PDF

• J. Gutierrez, M. Najib, G. Perelli, and M. Wooldridge. EVE: A Tool for Temporal Equilibrium Analysis. In Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA-2018), Los Angeles, October 2018. PDF

---

EVE has been tested on the following platforms:

1. Fedora
2. Ubuntu

EVE is also available preinstalled in Open Virtual Appliance (OVA) image running Lubuntu (lightweight Linux based on Ubuntu). This image (1.5 GB) can be downloaded from https://goo.gl/ikdSnw and can be directly run on VirtualBox (https://www.virtualbox.org/).

Windows Users

Windows users can run EVE via WSL Ubuntu (https://ubuntu.com/tutorials/install-ubuntu-on-wsl2-on-windows-10#1-overview). You may need to disable sanboxing when initialising OPAM (see: https://stackoverflow.com/questions/54987110/installing-ocaml-on-windows-10-using-wsl-ubuntu-problems-with-bwrap-bubblewr).

INSTALLATION

Prerequisites

Before installing EVE, make sure you have the following prerequisites installed:

1. python 3.x

2. OPAM (https://opam.ocaml.org/doc/Install.html) + OCaml version 4.03.0 >= and <= 4.07.0 (https://ocaml.org/docs/install.html). To see OCaml version ocaml --version. You may need to donwgrade your OCaml:

   • Run opam switch list, and switch to an available version between 4.03.0 >= and <= 4.07.0.
   • If there is no OCaml version between 4.03.0 >= and <= 4.07.0, run opam switch create 4.07.0

   To initialise OPAM (along with OCaml):

   • echo "y" | opam init
   • eval `opam config env`

3. Cairo (https://cairographics.org/download/) or Pycairo (https://pycairo.readthedocs.io/en/latest/index.html)

4. IGraph version 0.7 or later (http://igraph.org/python/)

Configuration Steps

1. Ensure all prerequisites are installed.
2. Go inside eve-py folder
3. Run shell script ./config.sh (you may need to run chmod +x config.sh) Make sure OCaml is version 4.03.0 >= and <= 4.07.0 before running config.sh

---

How to use

• usage: From inside folder eve-py/src execute the following command: $ python main.py [problem] [path/name of the file] [options]

• List of problems:

  a Parameter to solve A-Nash

  e Parameter to solve E-Nash

  n Parameter to solve Non-Emptiness

• List of optional arguments:

  -d Option to draw the structures

  -v Option to execute in verbose mode

• Example:

  $ python main.py a ../examples/a-nash_1 -d solves the A-Nash problem and draws the structures. The drawing will be saved in the current (src) folder as str.png.

Running experiments

1. Go to folder eve-py/src/experiments, there are 8 scripts (you may need to run chmod +x <script_filename.sh> to run these 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:
   • parser performance (ms)
   • construction peformance (ms)
   • PGSolver performance (ms)
   • non-emptiness/E-Nash/A-Nash performance (ms)
   • total number of parity game states
   • total number of parity game edges
   • maximum total number of sequentialised parity game states
   • maximum total number of sequentialised parity game edges
   • total time performance (ms)

eve-parity's Issues

Compilation fixes and Dockerfile

Hi,
I'm using EVE for an evaluation and came across some small issues when using it on a "modern" system. I fixed them locally + created a Dockerfile which is sufficient to build & run EVE (IMO more convenient than a whole VM).

I can provide the changes via MR or you can simply include them if you like :)

In src/

--- a/generatepun.py
+++ b/generatepun.py
@@ -58,4 +58,4 @@
     try:
-        PUN[pl_name]=map(int,ttpg_results[0].strip()[1:-1].replace(' ','').split(','))
+        PUN[pl_name]=list(map(int,ttpg_results[0].strip()[1:-1].replace(' ','').split(',')))
     except ValueError:
         PUN[pl_name]=[]

(map nowadays is lazy, this forces reading & parsing the result)

In ltl2ba:

--- a/buchi.c
+++ b/buchi.c
@@ -44,8 +44,9 @@
 
 extern FILE *tl_out;	
 BState *bstack, *bstates, *bremoved;
-BScc *scc_stack;
-int accept, bstate_count = 0, btrans_count = 0, rank;
+static BScc *scc_stack;
+int accept, bstate_count = 0, btrans_count = 0;
+static int rank;
 
 /********************************************************************\
 |*        Simplification of the generalized Buchi automaton         *|
--- a/generalized.c
+++ b/generalized.c
@@ -46,9 +46,10 @@
 extern char **sym_table;
 
 GState *gstack, *gremoved, *gstates, **init;
-GScc *scc_stack;
+static GScc *scc_stack;
 int init_size = 0, gstate_id = 1, gstate_count = 0, gtrans_count = 0;
-int *fin, *final, rank, scc_id, scc_size, *bad_scc;
+int *fin, *final, scc_id, scc_size, *bad_scc;
+static int rank;
 
 void print_generalized();

These are changes taken from https://github.com/utwente-fmt/ltl2ba/commit/f2426dfdeb327924f2035fdb6c88542c19c5ee13.patch
Newer cpp compilers seem to be more picky.

Dockerfile:

FROM debian:bullseye

RUN apt-get update && apt-get install -y python3 unzip opam python3-cairo python3-igraph python-is-python3 \
  && rm -rf /var/lib/apt/lists/*

RUN useradd user -g users --create-home
USER user
RUN opam init --yes --disable-sandboxing

COPY eve-parity-master.zip /home/user/
RUN cd /home/user \
  && unzip -q eve-parity-master.zip && rm eve-parity-master.zip \
  && mv /home/user/eve-parity-master /home/user/eve && cd /home/user/eve/eve-py/ \
  && find /home/user/eve/eve-py/ -name "*.sh" -print0 | xargs -0 chmod +x \
  && sed -i 's!opam install!opam install --yes!' config.sh \
  && ./config.sh

With the above change applied and sources provided as eve-parity-master.zip this builds a docker image to run eve.