- Notifications
You must be signed in to change notification settings - Fork2
License
whitemech/LydiaSyft
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Repository files navigation
LydiaSyft is an open-source software framework for reasoning and synthesis of Linear Tempora Logic formulas interpreted on finite traces (LTLf), integrating efficient data structures and techniques focused on LTLf specifications.
This project can be used either as a standalone CLI tool or as a C++ library that integrates with other projects. Among the implemented Data Structures and algorithms, we have:
DFA representation and manipulation:
- Explicit-state DFA (à la MONA):(N. Klarlund et al., 2002),(De Giacomo and Favorito, 2021)
- Symbolic-state DFA:(Zhu et al., 2017)
LTLf synthesis settings:
- Classical synthesis:(Zhu et al., 2017)
- MaxSet synthesis:(Zhu and De Giacomo, 2022)
- Synthesis with fairness assumptions:(Zhu et al., 2020)
- Synthesis with stability assumptions:(Zhu et al., 2020)
- Synthesis with environment GR(1) assumptions:(De Giacomo et al., 2022)
Currently, the system has been tested on Ubuntu 24.04 LTS, and should work on other Linux systems. We plan to fully support also MacOS and Windows systems.
The software depends on the following projects:
- CUDD: CU Decision Diagram package:https://github.com/KavrakiLab/cudd
- MONA (WhiteMech's fork):https://github.com/whitemech/MONA
- Lydia:https://github.com/whitemech/lydia
- Flex &Bison
- Graphviz
- Syfco: the Synthesis Format Conversion Tool:https://github.com/reactive-systems/syfco
- Slugs: SmalL bUt Complete GROne Synthesizer:https://github.com/VerifiableRobotics/slugs/
The instructions have been tested over a machine with Ubuntu 24.04 as operating system.
First, install the following system-wide dependencies:
sudo apt install -y \ automake \ build-essential \ cmake \ curl \ libtool \ wget \ unzipInstall flex and bison:
sudo apt-get install flex bisonFor the graphical features (automata and strategy visualization), graphviz need to be installed:
sudo apt install graphviz libgraphviz-devBuilding Syfco requires the Glasgow Haskell Compiler. To install the tool you can usestack:
curl -sSL https://get.haskellstack.org/ | shgit clone https://github.com/reactive-systems/syfco.gitcd syfcogit checkout 50585e0stack installThe installation should install thesyfco binary in a directory in teh system path.Then, make sure the binarysyfco can be found on your system path:which syfco.
When using the CLI, you can also provide the path to thesyfco binary manually by setting--syfco-path.
Slugs is required for solving LTLf synthesis with GR(1) conditions.
To build Slugs, run:
cd submodules/slugsgit checkout a188d83cd srcmake -j$(nproc --ignore 1)Make sure CUDD is installed. CUDD can be found at:
https://github.com/KavrakiLab/cudd.gitInstall CUDD:
autoreconf -f -i./configure --enable-silent-rules --enable-obj --enable-dddmp --prefix=/usr/localsudo make installTo install MONA system-wide:
git clone --recursive https://github.com/whitemech/MONA.gitcd MONAgit checkout v1.4-19.dev0./configure && make -j && sudo make -j install# copy headers manuallysudo mkdir -p /usr/local/include/monasudo cp Mem/mem.h Mem/gnuc.h Mem/dlmalloc.h BDD/bdd_external.h BDD/bdd_dump.h BDD/bdd_internal.h BDD/bdd.h BDD/hash.h DFA/dfa.h GTA/gta.h config.h /usr/local/include/monaThe 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 intosubmodules/lydia and follow the installationinstructions in theREADME.md.
By default, the CMake configuration will fetch z3 automatically from the GitHub repository.There might be required other dependencies.
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.zipunzip z3-4.8.12-x64-glibc-2.31.zipcd z3-4.8.12-x64-glibc-2.31sudo cp bin/libz3.a /usr/local/libsudo cp include/*.h /usr/local/include- Make build folder so your directory is not flooded with build files:
mkdir build && cd build- Run CMake to generate the makefile:
cmake -DCMAKE_BUILD_TYPE=Release ..- Compile using the generated makefile:
make -j$(nproc --ignore=1) LydiaSyft4.1. For solving LTLf synthesis with GR(1) conditions, please installslugs following submodules/slugs/README.md
- Compile and Run tests:
make -j$(nproc --ignore=1) tests./bin/testsUsage:
LydiaSyft: A compositional synthesizer for Linear Temporal Logic on finite traces (LTLf)Usage: LydiaSyft [OPTIONS] SUBCOMMANDOptions: -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) conditionsTo see the options of each subcommand, run:
LydiaSyft [SUBCOMMAND] --helpExamples (run commands from the root directory of the project):
- Classical synthesis:
./build/bin/LydiaSyft synthesis -f examples/test.tlsf # UNREALIZABLE./build/bin/LydiaSyft synthesis -f examples/test1.tlsf # REALIZABLE- Maxset synthesis:
./build/bin/LydiaSyft maxset -f examples/test1.tlsf # REALIZABLE- Fairness synthesis:
./build/bin/LydiaSyft fairness -f examples/fair_stable_test.tlsf -a examples/fair_stable_test_assumption.txt # REALIZABLE- Stability synthesis:
./build/bin/LydiaSyft stability -f examples/fair_stable_counter_test.tlsf -a examples/fair_stable_test_assumption.txt # REALIZABLE- GR(1) synthesis:
./build/bin/LydiaSyft gr1 \ -f examples/TLSF/GR1benchmarks/finding_nemo/finding_nemo_1.tlsf \ -g examples/TLSF/GR1benchmarks/finding_nemo/finding_nemo_1_env_gr1.txt \ -e examples/TLSF/GR1benchmarks/finding_nemo/finding_nemo_1_env_safety.ltlf \ -a examples/TLSF/GR1benchmarks/finding_nemo/finding_nemo_1_agn_safety.ltlf \ --slugs-path ./submodules/slugs/ # REALIZABLEThe software also provides C++ APIs. Here there is an example of usage:
#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"intmain(int argc,char ** argv) {// define the formula and the input/output variables std::string formula_str ="F(a | b)"; std::vector<std::string> input_vars{"a"}; std::vector<std::string> output_vars{"b"};// parse the formulaauto driver = std::make_shared<whitemech::lydia::parsers::ltlf::LTLfDriver>(); std::stringstreamformula_stream(formula_str); driver->parse(formula_stream); whitemech::lydia::ltlf_ptr formula = driver->get_result();// initialize the variables Syft::InputOutputPartition partition =Syft::InputOutputPartition::construct_from_input(input_vars, output_vars); 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);// build the explicit-state DFA Syft::ExplicitStateDfa explicit_dfa =Syft::ExplicitStateDfa::dfa_of_formula(*formula); Syft::ExplicitStateDfaAdd explicit_dfa_add =Syft::ExplicitStateDfaAdd::from_dfa_mona(var_mgr, explicit_dfa);// build the symbolic-state DFA from the explicit-state DFA Syft::SymbolicStateDfa symbolic_dfa =Syft::SymbolicStateDfa::from_explicit(std::move(explicit_dfa_add));// do synthesis var_mgr->partition_variables(partition.input_variables, partition.output_variables); Syft::Player starting_player = Syft::Player::Agent; Syft::Player protagonist_player = Syft::Player::Agent; Syft::LTLfSynthesizersynthesizer(symbolic_dfa, starting_player, protagonist_player, symbolic_dfa.final_states(), var_mgr->cudd_mgr()->bddOne()); Syft::SynthesisResult result = synthesizer.run(); std::cout << (result.realizability?"" :"NOT") <<"REALIZABLE" << std::endl;return0;}
More code examples can be found in theexamples/ folder.To build them, runmake examples.
The documentation is built using Doxygen. First, installdoxygen:
sudo apt install doxygenThen:
doxygen DoxyfileThis project is licensed under the GNU Affero General Public License. See theLICENSE file for details.
Copyright (C) 2024, Marco Favorito, Shufang Zhu. All rights reserved.