verifiablerobotics/slugs

SmalL bUt Complete GROne Synthesizer

slugs - SmalL bUt Complete GROne Synthesizer

Slugs is a stand-alone reactive synthesis tool for generalized reactivity(1) synthesis. It uses binary decision diagrams (BDDs) as the primary data structure for efficient symbolic reasoning.

If you want to cite slugs in a scientific paper, please cite its tool paper:

• Rüdiger Ehlers and Vasumathi Raman: Slugs: Extensible GR(1) Synthesis. 28th International Conference on Computer Aided Verification (CAV 2016), Volume 2, p.333-339

You can find an author-archived version of the paper here. The paper has an appendix that contains an introduction to using slugs and its input language.

The slugs distribution comes with the CUDD library for manipulating binary decision diagrams (BDDs), written by Fabio Somenzi. Please see the README and LICENSE files in the lib/cudd-3.0.0 folder for details. The dddmp library for loading and saving BDDs that comes with CUDD has other licensing terms than CUDD that permit only academic and educational use. Please consult the source files in the lib/cudd-3.0.0/dddmp folder for details.

An introduction video to reactive synthesis with a focus on generalized reactivity(1) synthesis here. It also contains a Slugs tool demo.

Installation

Requirements

• A moderately modern C++ and C compiler installed in a Unix-like environment, including the C++ library boost. Linux and MacOS should be fine.
• An installation of Python 2, version 2.7 or above. The Python curses library must be installed for the interactive specification debugger to be usable.

Using Slugs on Linux

In order to build slugs, open a terminal and type:

cd src; make

The slugs executable will be put into the src directory.

Using slugs on OS X

Things should generally work fine if you have a package management system (i.e. Homebrew or Macports) installed and follow the above instructions for Linux. Note that you will need to:

• have gcc, g++ in your $PATH,
• have installed at least the package: boost.

A short primer on the internal structure of slugs

The structure of slugs is documented in a doxygen compatible format. Internally, it uses the 'BFAbstractionLibrary' - It handles all calls to the BDD library, but allows to easily replace the BDD library actually used. For using the BFAbstractionLibrary, it suffices to include 'BF.h' - the choice of concrete BDD library used is done via preprocessor directives (see 'BF.h'). The 'BF' in 'BFAbstractionLibrary' stands for 'Boolean function'.

That library has a couple of classes:

• BF - The actual Boolean function. Supports operations like AND, OR, ..., using C++ operator overloading
• BFManager - It keeps a list of BF variables, provided TRUE or FALSE constants, and can compute variable vectors or cubes
• BFVarCube - An unsorted list of variables - used for existentially or universally quantifying out variables from BDDs
• BFVarVector - A sorted list of variables - used for replacing variables in BFs by other variables

There is also a library component for dumping BDDs - this is useful for debugging. For this to work, the application has to provide the dumping function with information about string names for BDD variable and the like. The 'Slugs' main container class inherits the class 'VariableInfoContainer' for this purpose.

The actual synthesis part is built around a class that is named "GR1Context". It is explained in the automatically generated doxygen documentation. The class GR1Context is the main class that can be inherited for modifications of the synthesis algorithm. The 'main' function in the file 'main.cpp' is concerned with building the proper context class for synthesis and running the synthesis algorithm then.

slugs's Issues

Counterstrategy synthesis doesn't work properly for "transition" liveness conditions

See the following example:

[INPUT]
ball
cat

[OUTPUT]
bit0

[ENV_TRANS]
| ! cat' ! ball'

[ENV_LIVENESS]
1

[ENV_INIT]
1

[SYS_TRANS]
| ! ball' ! bit0'
| ! cat' ! ! bit0'

[SYS_LIVENESS]
bit0'
! bit0'

[SYS_INIT]
! bit0

The counterstrategy synthesized does not prevent the goals. However, changing the goals to "current" time step fixes the problem and the counterstrategy is correct.

gcc g++ 4.7 needed to build SLUGS

I was trying to build slugs with gcc g++ 4.6.3 and I got the following errors:

g++ -c -pipe -g -g -Wextra -std=gnu++0x -mtune=native -malign-double -DHAVE_IEEE_754 -DBSD -DCUDD_COMPILER_OPTIONS_SET -Wall -W -DQT_WEBKIT -DUSE_CUDD -I/usr/share/qt4/mkspecs/linux-g++ -I. -I../lib/cudd-2.5.0/include -IBFAbstractionLibrary -o main.o main.cpp
In file included from extensionComputeCNFFormOfTheSpecification.hpp:4:0,
from main.cpp:38:
gr1context.hpp:32:20: error: function definition does not declare parameters
gr1context.hpp:33:20: error: function definition does not declare parameters
gr1context.hpp:34:18: error: function definition does not declare parameters
gr1context.hpp:35:18: error: function definition does not declare parameters
gr1context.hpp:36:18: error: function definition does not declare parameters
gr1context.hpp:37:18: error: function definition does not declare parameters
gr1context.hpp:38:18: error: function definition does not declare parameters
gr1context.hpp:39:18: error: function definition does not declare parameters
gr1context.hpp:40:25: error: function definition does not declare parameters
gr1context.hpp:41:25: error: function definition does not declare parameters
gr1context.hpp:42:25: error: function definition does not declare parameters
gr1context.hpp:43:25: error: function definition does not declare parameters

But after I install gcc g++ 4.7 as here:
http://charette.no-ip.com:81/programming/2011-12-24_GCCv47/

then I can build it. It's just a note that compiler matters and Ubuntu 12.04 originally comes with gcc g++ 4.6.3 and that is a problem. I'm not sure why it only happens this time.

Slugs Fuzzer needs to be updated

The slugs fuzzer currently does not produce initialization constraints. This should be changed at some point.

Minor question: Some non-error normal output is output into stderr instead of stdout

When the spec is realisable, the tool outputs the result into stderr instead of stdout.
Should it be std::cout instead of std::cerr? It seems as a normal-operation output, not an error. Unless it is by convention.
(when checking the tool performed as expected I check that stderr is empty; here it is not.)

extensionInteractiveStrategy.hpp
56:            std::cerr << "RESULT: Specification is realizable.\n";

extensionNondeterministicMotion.hpp
496:            std::cerr << "RESULT: Specification is realizable.\n";

synthesisContextBasics.cpp
112:        std::cerr << "RESULT: Specification is realizable.\n";

Two-dimensional cost / Infinite action cost

The two-dimensional cost-plugin does not currently work correctly in scenarios in which an infinite action cost cannot be avoided. The current master branch includes an example named "examples/twoDimensionalCost/sysInitRoboticsSemanticsTwoDimensionalCostExample" whose explicit-state implementation has no states.

Building slugs on m1 mac osx

Dear maintainer,

Thank you for making this tool. I'm trying to use this on m1 mac osx and got this error after hitting "make":

Undefined symbols for architecture arm64:
"__ZNKSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEE4findEcm", referenced from:
_ZN24XAnalyzeInitialPositionsI10GR1ContextLb1EE18printLargePreCubesE5BFBddS2 in main.o
_ZN24XAnalyzeInitialPositionsI10GR1ContextLb0EE18printLargePreCubesE5BFBddS2 in main.o
__ZN30XAbstractWinningTraceGeneratorI10GR1ContextE7executeEv in main.o
__ZN33XComputeInterestingRunOfTheSystemI10GR1ContextE10computeRunEv in main.o
"__ZNKSt3__112basic_stringIcNS_11char_traitsIcEENS_9allocatorIcEEE7compareEmmPKcm", referenced from:
_main in main.o
__ZN24XExtractExplicitStrategyI18XRoboticsSemanticsI7XIROSFSI10GR1ContextEELb1ELb1EE7executeEv in main.o
...

The list is long...

and at the end:
NOTE: a missing vtable usually means the first non-inline virtual member function has no definition.
ld: symbol(s) not found for architecture arm64
collect2: error: ld returned 1 exit status
make: *** [slugs] Error 1

I am not familiar with osx under arm. Is this an error caused by architecture?

Thanks again.

empty graph returned as explicit strategy for trivially realizable problem

Setting the assumption False to obtain a trivially realizable GR(1) spec results in an enumerated strategy that does not have any nodes. As of 4510283 the spec:

[INPUT]
x
[OUTPUT]
y
[SYS_LIVENESS]
0

is not realizable, as expected. The variation with:

[INPUT]
x
[OUTPUT]
y
[ENV_LIVENESS]
0
[SYS_LIVENESS]
0

is realizable, as expected.

The issue is with the spec:

[ENV_INIT]
0

Irrespective of the values for the other parts (for env and sys), the above spec returns:

RESULT: Specification is realizable.
{"version": 0,
 "slugs": "0.0.1",

 "variables": ["x", "y"],

 "nodes": {
}}

Correctly, it is realizable. But incorrectly for an enumerated strategy representation, the transducer graph has no nodes (it should have been non-empty, since any infinite system behavior is an admissible solution in this case).

It appears that the assumption on initial condition prevents the enumeration of the game graph in extensionExtractExplicitStrategy. Simplified, this line reads:

todoInit = winningPositions & initSys & initEnv

If initSys = False, then todoInit is the empty set, so an empty todoList will result, because there will be 0 iterations. As a result, no nodes will be enumerated later.

Changing that line to (assumption -> guarantee):

( (! initEnv) | (winningPositions & initSys) )

seems to fix the issue, returning for the previous spec:

[ENV_INIT]
0

the enumerated strategy:

{"version": 0,
 "slugs": "0.0.1",

 "variables": ["x", "y"],

 "nodes": {
"0": {
    "rank": 0,
    "state": [0, 0],
    "trans": [0, 2]
},

"1": {
    "rank": 0,
    "state": [0, 1],
    "trans": [0, 2]
},

"2": {
    "rank": 0,
    "state": [1, 0],
    "trans": [0, 2]
},

"3": {
    "rank": 0,
    "state": [1, 1],
    "trans": [0, 2]
}

}}

(minor) error thrown when more than one file name provided

When specifying a plugin needing more than one file name, I get:
"Error: You provided too many file names!"
I'm working around it for now by commenting lines 231-234 in main.cpp.

Backwards reachability computations do not enforce env safety unless "next" is used?

This is more of a kink than a bug:

In the following automaton, the environment is seemingly allowed to falsify one of its own safety requirements, specifically the mutex statement: [](s1 <-> !s2) (This is part of a larger LTLMoP specification. Please ask for the .spec file if it'd be helpful.)

The issue is resolved if the env safety is written in the "next" tense: [](next(s1) <-> next(!s2))

According to @vraman

The reason these states get generated is because the backwards reachability computations start from any winning states, including states from which the environment cannot move, and then add in transitions that do not violate the environment safety. The two states you point out are winning states, and included in this computation. Now, the transitions into these "dead" states do not technically violate the env safety unless the safety is expressed with a "next" operator. In other words, the transition still satisfies your original safety, even though the resulting state does not.

Not sure if it merits fixing, but seemed worth documenting.

tests of correctness of slugs?

Are there unit tests or other kinds of tests that demonstrate correctness of slugs? E.g., this might be a collection of tests that are performed using

make check

or make test, which would be run after cd src; make as in the README.

explicit

When I run the example water_reservoir.slugsin file in the slug with explicitStrategy, the output is the file attached. What do the values level@1, level@2, etc., mean? Is it possible to find the level of the reservoir at every state? If so, how?

water_reservoir.txt

Question regarding the format of the slug output

Dear tool maintainer,

I've been trying to use your tool in my work.
However, I'm a little confused about how to interpret the output of slugs.

For a very simple example

[OUTPUT]
g
[SYS_TRANS]
g->!g'
!g->g'

When I used --symbolicStrategy parameter
I get the following dddmp dump file

.ver DDDMP-2.0
.mode A
.varinfo 0
.nnodes 5
.nvars 4
.nsuppvars 3
.suppvarnames g g' _jx_b0
.orderedvarnames g g' _jx_b0 strat_type
.ids 0 1 2
.permids 0 1 2
.auxids 0 1 2
.nroots 1
.rootids -5
.nodes
1 T 1 0 0
2 2 2 1 -1
3 1 1 1 2
4 1 1 2 1
5 0 0 3 4
.end

My question is

1. How should I interpret this output ? What does it mean to have a negative rootid ?
2. Why don't we need a primed version of the variable _jx_b0 and strat_type ?

request to create versions (and releases)

Would you consider introducing versions as tags in this repository?

Otherwise, it is difficult to create reliable references to slugs. My motivating use-case is a script that fetches, builds, and runs slugs as part of tests for an interface that is being developed in TuLiP. Without tags, the only potentially reliable reference is commit hashes on master branch. However, to get a particular commit, it is necessary to clone the Slugs repository and checkout that particular commit. Furthermore, the clone must be of sufficient depth, which makes the solution a relatively heavy weight long-duration solution. Furthermore, it requires Git to be installed wherever the script is going to be used.

There are many other motivating use-cases for versioning. Tell me if you want more to be described here.

incomplete license description for CUDD

The CUDD sources tarball includes dddmp, which is not open source (and not under the same license as CUDD). E.g., consult the text at lines 15-24 of lib/cudd-3.0.0/dddmp/dddmp.h. This should be clarified in the README of slugs, which only mentions LICENSE "in the lib/cudd-3.0.0 folder".

How to change specification?

To use LTLMop I need to change robot transition \varphi^{s}_{t} because I do not want it to go to some regions at some times. However these specifications are generated as default. How can I change the default speifications?

How to use weak and strong "until"s in structuredslugs?

Cannot use the Structured slugs compiler tool, it seems like it might not support
BinaryTemporalFormula formula when having a until operator in the formula.
I tried to make a minimum working example here:

[INPUT]
R:0...2
B

[OUTPUT]
M:0...1

[SYS_LIVENESS]
R=3
R=0

[SYS_INIT]
!(M=1)

[ENV_TRANS]
(R=0 & M=0)->((R=0)**W**(R=2))
(R=0 & M=1)->(R'=0)
(R=1 & M=0)->((R=1)**W**(R=2))
(R=1 &  M=1)->(R'=0)
(R=1 & M=0)->(R'=2)
(R=2 & M=1)->(R'=1)

[ENV_INIT]
R=0
!B

[SYS_TRANS]
(B')->(M'=1)

[ENV_LIVENESS]
!B

and get:

Cannot parse sub-tree!
['BinaryTemporalFormula', ['CalculationSubformula', ['numID', 'R'], ['NumberComparisonOperator', ['EqualOperator', ('=',)]], ['numeral', '0']], ['WeakUntilOperator', ('W',)], ['CalculationSubformula', ['numID', 'R'], ['NumberComparisonOperator', ['EqualOperator', ('=',)]], ['numeral', '2']]]

Is there a specific syntax for W, or is it not supported this way?