Bassist

Coypright © 2011/2012 Ruediger Ehlers, Saarland University

Introduction

Bassist is a tool set for the synthesis of finite-state machines from temporal logic specifications in which each assumption and guarantee is in the common fragment of LTL and ACTL. Specification parts are written in LTL syntax. Bassist check automatically whether all specification parts are contained in the common fragment, and tests the realizability of the specification in case of a positive answer.

The current version, Bassist v.0.1 is a premature release where some sanity checks are still missing, a code review still needs to be performed, some optimizations are not implemented yet, and the documentation still has to be written. So use it with care.

Requirements

For correct operation of the Bassist tool set, a moderately modern Linux distribution with the following components is required:

In Ubuntu Linux, the presence of these components can be ensured by running sudo apt-get install build-essential libboost-dev picosat qt4-qmake. Python 2.x is installed by default on Ubuntu.

Installation

After extracting the archive to some directory, run the script “./download_libraries_and_make.sh” from the installation directory. The script will download two external tools, ltl2ba v.1.1 and ltl2dstar v.0.5.1 and the BDD library CuDD from their web sites, and extract these to the bassist directory. Afterwards, all tools will be compiled automatically by the script. Watch out for any error messages. At the end of the execution of the script, it gives you the possibility to test the synthesis process.

Usage

To check the realizability of a specification, run the “Tools/synthesize.py” script from any directory and provide a name to a specification XML file. If you also want a NuSMV model in case of realizability, provide the name of the output file as second parameter. An example specification file looks like this:

<?xml version=“1.0” encoding=“ISO-8859-1”?>
<!DOCTYPE SynthesisProblem SYSTEM “http://react.cs.uni-saarland.de/tools/
bassist/LinearTimeSynthesisProblem.dtd”>
<SynthesisProblem>
<Title>Simple Example</Description>
<Description>Simple Example</Description>
<Inputs>@
<Bit>in0</Bit>
<Bit>in1</Bit>
</Inputs>
<Outputs>
<Bit>out0</Bit>
<Bit>out1</Bit>
<Bit>out2</Bit>
</Outputs>
<Semantics type=“Mealy”/>
<Specification>
<PropertyGroup type=“Assumption-Guarantee”>
<PropertyGroup type=“Conjunction”>
<LTL>G F in0</LTL>
<LTL>G F in1</LTL>
</PropertyGroup>
<PropertyGroup type=“Conjunction”>
<LTL>G (in0 -> F out0)</LTL>
<LTL>G (in1 -> F out1)</LTL>
<LTL>G F out0 </LTL>
<LTL>G F out1 </LTL>
<LTL>G (!out0 | !out1)</LTL>
</PropertyGroup>
</PropertyGroup>
</Specification>
</SynthesisProblem>

The first two lines contain some XML information. A title or description for the specification is optional. Afterwards, lists of input and output atomic propositions for the system to be synthesized are given.

The file format used allows both Mealy- and Moore-type semantics to be defined. Currently, the Bassist tool set only supports Mealy-type semantics.

Afterwards, the actual specification is given. Bassist is optimized towards specifications that consist of a conjunction of assumptions, whose satisfaction implies the satisfaction of some conjunction of guarantees, and can only handle such specifications or special cases thereof. The specification parts can be given in standard LTL syntax.

If you choose to generate a NuSMV model in case of realizability, the model file will contain the specification. This way, the model file can be fed to NuSMV for verification directly.

Whether the specification is realizable or not is printed out in line starting with “-- Result:”. If you are only interested in this information and want to filter out all statistical information provided by the tool set, you can use grep to filter the information. As an example, you can run ../Tools/synthesize.py mutex.xml 2>&1 | grep "\-\- Result" from the Benchmarks directory.

Download

Bassist v.0.1, pre-alpha version from the 25th of January 2012

Contact

Rüdiger Ehlers