This repository contains source code for the LAbS code generator, which is used by the SLiVER tool to verify LAbS systems.
It contains four projects:
- LabsCore: basic data types and function to describe and manipulate LAbS syntax trees.
- LabsParser: a parser for- .labsfiles.
- Frontend: static checks and intermediate representation for LAbS systems.
- LabsTranslate: the code generator itself.
The included Makefile creates a full distribution, containing SLiVER,
LabsTranslate, and a set of example files.
- FParsec (parser combinators) for LabsParser;
- Argu (argument parser) for the LabsTranslateCLI;
- DotLiquid for code generation.
- FSharpPlus for generic programming, lenses, etc.
SLiVER also uses:
- Click for its CLI;
- pyparsing.py to translate counterexamples;
- CSeq for distributed bounded model checking (experimental).
Building LabsTranslate requires dotnet v3 or higher.
The included Makefile targets either x64 Linux or MacOs (version 10.12 "Sierra" and higher).
git clone <this repository> labs/
cd labs/
# Debug build (to edit/debug code) 
dotnet publish
# Release build
git submodule init # Only needed the 1st time
git submodule update
make [osx|linux]The release binaries will be within labs/build/.
To add support for CSeq, follow these additional steps:
- Download CSeq 1.9
- Extract the CSeq archive within the labsdirectory
- Rename the CSeq directory to cseq
- make [osx|linux]_cseq
Notice that CSeq support has only been tested under Linux.
[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
[2] R. De Nicola, L. Di Stefano, and O. Inverso, “Multi-Agent Systems with Virtual Stigmergy,” Science of Computer Programming 187, 2020. Link
[3] L. Di Stefano, F. Lang, and W. Serwe, “Combining SLiVER with CADP to Analyze Multi-agent Systems”, in COORDINATION, 2020. To appear. Link