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 .labs files.
• 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 LabsTranslate CLI;
• 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:

1. Download CSeq 1.9
2. Extract the CSeq archive within the labs directory
3. Rename the CSeq directory to cseq
4. 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