Compilation Instructions using CMake
System-wide dependencies
We assume the software will be built on a Ubuntu 22.04 machine.
First, install the following system-wide dependencies:
sudo apt install -y \
automake \
cmake \
gcc \
g++ \
libtool \
wget \
unzip
Install CUDD
0.1 Make sure CUDD is installed. CUDD can be found at:
https://github.com/KavrakiLab/cudd.git
0.2 Install CUDD:
./configure --enable-silent-rules --enable-obj --enable-dddmp --prefix=[install location]
sudo make install
If you get an error about aclocal, this might be due to either
a. Not having automake:
sudo apt-get install automake
b. Needing to reconfigure, do this before configuring:
autoreconf -i
Install FLEX, BISON
0.3 Install flex and bison:
sudo apt-get install flex bison
Install LYDIA
The tool requires the installation of Lydia, which will be triggered by the CMake configuration.
However, if you want to install Lydia manually, you can co into submodules/lydia
and follow the installation instructions in the README.md
.
Install Z3
By default, the CMake configuration will fetch z3 automatically from the GitHub repository. In order to disable this behaviour, you can configure the project by setting -DZ3_FETCH=OFF.
In that case, you have to have the library installed on your system. To link the static library of z3, you have to install z3 manually:
wget https://github.com/Z3Prover/z3/releases/download/z3-4.8.12/z3-4.8.12-x64-glibc-2.31.zip
unzip z3-4.8.12-x64-glibc-2.31.zip
cd z3-4.8.12-x64-glibc-2.31
cp bin/libz3.a /usr/local/lib
cp include/*.h /usr/local/include
Graphviz
For the graphical features (automata and strategy visualization), graphviz need to be installed:
sudo apt install graphviz libgraphviz-dev
Build LYDIASYFT
- Make build folder so your directory is not flooded with build files:
- Run CMake to generate the makefile:
cmake -DCMAKE_BUILD_TYPE=Release ..
- Compile using the generated makefile:
make -j$(nproc --ignore=1) LydiaSyft
4.1. For solving LTLf synthesis with GR(1) conditions, please install slugs
following submodules/slugs/README.md
- Compile and Run tests:
make -j$(nproc --ignore=1) tests
./bin/tests
Run LYDIASYFT
Usage:
LydiaSyft: A compositional synthesizer for Linear Temporal Logic on finite traces (LTLf)
Usage: ./cmake-build-debug/bin/LydiaSyft [OPTIONS] SUBCOMMAND
Options:
-h,--help Print this help message and exit
--help-all Expand all help
-p,--print-strategy Print out the synthesized strategy (default: false)
-t,--print-times Print out running times of each step (default: false)
Subcommands:
synthesis solve a classical LTLf synthesis problem
maxset solve LTLf synthesis with maximally permissive strategies
fairness solve LTLf synthesis with fairness assumptions
stability solve LTLf synthesis with stability assumptions
gr1 Solve LTLf synthesis with GR(1) conditions
To see the options of each subcommand, run:
LydiaSyft [SUBCOMMAND] --help
Examples (run commands from the root directory of the project):
./build/bin/LydiaSyft synthesis -f example/test.tlsf # UNREALIZABLE
./build/bin/LydiaSyft synthesis -f example/test1.tlsf # REALIZABLE
./build/bin/LydiaSyft maxset -f example/test1.tlsf
./build/bin/LydiaSyft fairness -f example/fair_stable_test.tlsf -a example/fair_stable_test_assumption.txt # REALIZABLE
./build/bin/LydiaSyft stability -f example/fair_stable_counter_test.tlsf -a example/fair_stable_test_assumption.txt # REALIZABLE
./build/bin/LydiaSyft gr1 -f example/GR1benchmarks/finding_nemo_agn_goal.tlsf -g example/GR1benchmarks/finding_nemo_env_gr1.txt -e example/GR1benchmarks/finding_nemo_env_safety.ltlf -a example/GR1benchmarks/finding_nemo_agn_safety.ltlf --slugs-path ./submodules/slugs/ # REALIZABLE
Quickstart
The software also provides C++ APIs. Here there is an example:
#include <memory>
#include <sstream>
#include <string>
#include <vector>
#include <lydia/parser/ltlf/driver.hpp>
#include "automata/ExplicitStateDfa.h"
#include "automata/ExplicitStateDfaAdd.h"
#include "automata/SymbolicStateDfa.h"
#include "game/InputOutputPartition.h"
#include "Player.h"
#include "VarMgr.h"
#include "synthesizer/LTLfSynthesizer.h"
int main(int argc, char ** argv) {
std::string formula_str = "F(a | b)";
std::vector<std::string> input_vars{"a"};
std::vector<std::string> output_vars{"b"};
auto driver = std::make_shared<whitemech::lydia::parsers::ltlf::LTLfDriver>();
std::stringstream formula_stream(formula_str);
driver->parse(formula_stream);
whitemech::lydia::ltlf_ptr formula = driver->get_result();
std::shared_ptr<Syft::VarMgr> var_mgr = std::make_shared<Syft::VarMgr>();
var_mgr->create_named_variables(partition.input_variables);
var_mgr->create_named_variables(partition.output_variables);
std::move(explicit_dfa_add));
var_mgr->partition_variables(partition.input_variables, partition.output_variables);
Syft::Player starting_player = Syft::Player::Agent;
Syft::Player protagonist_player = Syft::Player::Agent;
var_mgr->cudd_mgr()->bddOne());
std::cout << (result.realizability? "" : "NOT ") << "REALIZABLE" << std::endl;
return 0;
}
A DFA with explicit states and symbolic transitions represented in ADDs.
Definition: ExplicitStateDfaAdd.h:18
static ExplicitStateDfaAdd from_dfa_mona(std::shared_ptr< VarMgr > var_mgr, const ExplicitStateDfa &explicit_dfa)
Constructs an explicit-state DFA in ADD representation from an explicit-state DFA.
Definition: ExplicitStateDfaAdd.cpp:44
A DFA with explicit states and symbolic transitions.
Definition: ExplicitStateDfa.h:22
static ExplicitStateDfa dfa_of_formula(const whitemech::lydia::LTLfFormula &formula)
Construct an explicit-state DFA from a given formula using Lydia.
Definition: ExplicitStateDfa.cpp:35
A single-strategy-synthesizer for an LTLf formula given as a symbolic-state DFA.
Definition: LTLfSynthesizer.h:15
A DFA with symbolic states and transitions.
Definition: SymbolicStateDfa.h:18
CUDD::BDD final_states() const
Returns the BDD encoding the set of final states.
Definition: SymbolicStateDfa.cpp:135
static SymbolicStateDfa from_explicit(const ExplicitStateDfaAdd &explicit_dfa)
Converts an explicit DFA to a symbolic representation.
Definition: SymbolicStateDfa.cpp:92
Definition: Synthesizer.h:16
Implemented Data Structures and Algorithm
- DFA representation and manipulation:
- LTLf synthesis settings:
Documentation
The documentation is built using Doxygen. First, install doxygen
:
Then: