From 37d4ffa531ae67a2824c6ce5cb6712993914f0a4 Mon Sep 17 00:00:00 2001 From: Luca Di Stefano Date: Fri, 2 Aug 2019 13:04:50 +0200 Subject: [PATCH] Update README --- README.md | 45 +++++++++++++++++++++++---------------------- 1 file changed, 23 insertions(+), 22 deletions(-) diff --git a/README.md b/README.md index f839812..b56f9d2 100644 --- a/README.md +++ b/README.md @@ -1,32 +1,35 @@ -# SLiVER 1.0 • May 2018 +# SLiVER (Symbolic LAbS VERifier) -Symbolic LAbS VERifier +SLiver is a tool for the analysis of multi-agent systems specified in the +LAbS language [1]. At the moment, it support under-approximate analysis +via bounded model checking. + +This page contains binary releases of SLiVER for Linux x64 systems. ## Package contents +Typically, a SLiVER release will contain the following files and directories: + |Filename|Description |------------------|----------------------------------| -|README.txt |this file| +|README.txt |Installation instructions |sliver.py |SLiVER command-line front-end| |core/ |CSeq core framework| |labs/ |LAbS parser and translator| |lib/ |Frontend libraries| -|flock.labs |a simple, parametric LAbS system| -|*other files* |CSeq| - +|*.labs |Example LAbS specifications| +|cbmc-simulator |CBMC5.4 binary| +|*other files* |CSeq and Python libraries used by SLiVER| ## Installation To install SLiVER, please follow the steps below: -1. install the dependencies: - - Python 3.5 or higher - - backends: CBMC, ESBMC, CSeq - (none of the above tools is specifically required - but at least one of them is needed for verification). +1. install Python 3.5 or higher. - The bundled CSeq backend requires Python 2.7 with the `pycparser` module. +2. (Optional) Install Python 2.7 with the `pycparser` module + (required by the bundled CSeq backend). 2. create a directory, suppose this is called `/workspace` @@ -34,23 +37,16 @@ To install SLiVER, please follow the steps below: 4. extract the entire package contents in `/workspace` -5. set execution (+x) permissions for `sliver.py` +5. set execution (+x) permissions for `sliver.py`, `cseq.py`, `cbmc-simulator` 6. make sure that the backend's binary is in the search path, or amend the command strings in `sliver.py` accordingly. +7. Follow `/workspace/README.txt` for additional instructions. ## Usage -To try SLiVER, please use the following command: - - ./sliver.py --steps 12 --fair flock.labs birds=3 delta=22 grid=16 - -which should report that no property is violated. - -The following command should instead report that a property is violated: - - ./sliver.py --steps 12 --fair flock.labs birds=3 delta=21 grid=16 +All releases contain one or more examples. Please follow the README.txt file for specific instructions on how to analyse them. Invoking the tool with the `--help` switch: @@ -58,6 +54,11 @@ Invoking the tool with the `--help` switch: will provide further usage directions. +## Support + +If you encounter any issues while running SLiVER, please submit +an [issue](https://github.com/lou1306/sliver/issues). + ## Publications [1] R. De Nicola, L. Di Stefano, and O. Inverso, “Multi-Agent Systems with Virtual Stigmergy,” in: Mazzara M., Ober I., Salaün G. (eds) Software Technologies: Applications and Foundations. STAF 2018. Lecture Notes in Computer Science, vol 11176. Springer, 2018. [Link](https://link.springer.com/chapter/10.1007%2F978-3-030-04771-9_26)