diff --git a/README.md b/README.md index 4d23fae..827b44a 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,8 @@ -###Compilation Instructions using CMake +# LydiaSyft: A Compositional Symbolic Synthesis Framework for LTLf Specification -=== System-wide dependencies === +## Compilation Instructions using CMake + +### System-wide dependencies We assume the software will be built on a Ubuntu 22.04 machine. @@ -18,7 +20,7 @@ sudo apt install -y \ ``` -==== Install CUDD ==== +### Install CUDD 0.1 Make sure CUDD is installed. CUDD can be found at: @@ -36,14 +38,14 @@ sudo apt install -y \ autoreconf -i -==== Install FLEX, BISON ==== +### Install FLEX, BISON 0.3 Install flex and bison: sudo apt-get install flex bison -==== Install LYDIA ==== +### Install LYDIA cd submodules cd lydia @@ -51,7 +53,7 @@ sudo apt install -y \ Follow the instructions to complete the installation of lydia. -==== Install Z3 ==== +### 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. @@ -67,7 +69,7 @@ cp bin/libz3.a /usr/local/lib cp include/*.h /usr/local/include ``` -=== Graphviz === +### Graphviz For the graphical features (automata and strategy visualization), graphviz need to be installed: @@ -76,7 +78,7 @@ sudo apt install graphviz libgraphviz-dev ``` -==== Build LYDIASYFT ==== +## Build LYDIASYFT 1. Make build folder so your directory is not flooded with build files: @@ -98,12 +100,62 @@ sudo apt install graphviz libgraphviz-dev ``` -==== Run LYDIASYFT ==== +## 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 +``` -1. Reach executable file LydiaSyft +To see the options of each subcommand, run: + +``` +LydiaSyft [SUBCOMMAND] --help +``` - ```cd bin``` +Examples (run commands from the root directory of the project): -2. Run example: - ```./Lydiasyft -f ../../example/test.tlsf``` +- Classical synthesis: +``` +./build/bin/LydiaSyft synthesis -f example/test.tlsf # UNREALIZABLE +./build/bin/LydiaSyft synthesis -f example/test1.tlsf # REALIZABLE +``` + +- Maxset synthesis: + +``` +./build/bin/LydiaSyft maxset -f example/test.tlsf +``` + +- Fairness synthesis: + +``` +./build/bin/LydiaSyft .fairness -f example/fair_stable_test.tlsf -a example/fair_stable_test_assumption.txt # REALIZABLE +``` + +- Stability synthesis: + +``` +./build/bin/LydiaSyft stability -f example/fair_stable_counter_test.tlsf -a example/fair_stable_test_assumption.txt # REALIZABLE +``` + +- GR(1) synthesis: + +``` +./cmake-build-debug/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/src/slugs +``` diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index b44475d..10093c6 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -2,8 +2,8 @@ add_subdirectory(utils) add_subdirectory(parser) add_subdirectory(synthesis) -include_directories(${UTILS_INCLUDE_PATH} ${PARSER_INCLUDE_PATH} ${SYNTHESIS_INCLUDE_PATH} ${EXT_INCLUDE_PATH}) -add_executable(LydiaSyft Main.cpp) +include_directories(cli ${UTILS_INCLUDE_PATH} ${PARSER_INCLUDE_PATH} ${SYNTHESIS_INCLUDE_PATH} ${EXT_INCLUDE_PATH}) +add_executable(LydiaSyft Main.cpp cli/base.cpp cli/fairness.cpp cli/gr1.cpp cli/maxset.cpp cli/stability.cpp cli/synthesis.cpp) target_link_libraries(LydiaSyft ${PARSER_LIB_NAME} ${SYNTHESIS_LIB_NAME} ${UTILS_LIB_NAME} ${LYDIA_LIBRARIES}) diff --git a/src/Main.cpp b/src/Main.cpp index f22fb3a..13002b0 100644 --- a/src/Main.cpp +++ b/src/Main.cpp @@ -4,203 +4,96 @@ #include "Stopwatch.h" -#include "parser/Parser.h" -#include "ExplicitStateDfaMona.h" -#include "ReachabilitySynthesizer.h" -#include "ReachabilityMaxSetSynthesizer.h" +#include "cli/base.hpp" +#include "cli/fairness.hpp" +#include "cli/gr1.hpp" +#include "cli/stability.hpp" +#include "cli/synthesis.hpp" +#include "cli/maxset.hpp" #include "InputOutputPartition.h" #include "Preprocessing.h" #include #include -#include int main(int argc, char ** argv) { CLI::App app { - "LydiaSyft: A compositional synthesizer for Linear Temporal Logic on finite traces (LTLf)" + "LydiaSyft: A compositional synthesizer for Linear Temporal Logic on finite traces (LTLf)" }; + app.set_help_all_flag("--help-all", "Expand all help"); - std::string formula_file; - - app.add_option("-f,--spec-file", formula_file, "Specification file")-> - required() -> check(CLI::ExistingFile); - + // shared arguments bool print_strategy = false; app.add_flag("-p, --print-strategy", print_strategy, "Print out the synthesized strategy (default: false)"); bool print_times = false; app.add_flag("-t, --print-times", print_times, "Print out running times of each step (default: false)"); - bool maxset = false; - app.add_flag("-m,--maxset", maxset, "Maxset flag (Default: false)"); + std::string formula_file; + std::string path_to_syfco; + std::string assumption_file; + std::string gr1_file; + std::optional env_safety_file; + std::optional agent_safety_file; + std::string path_to_slugs; + + // 'synthesis' subcommand + CLI::App *synthesis = app.add_subcommand("synthesis", "solve a classical LTLf synthesis problem"); + Syft::add_spec_file_option(synthesis, formula_file); + Syft::add_syfco_option(synthesis, path_to_syfco); + + // 'maxset' subcommand + CLI::App *maxset = app.add_subcommand("maxset", "solve LTLf synthesis with maximally permissive strategies"); + Syft::add_spec_file_option(maxset, formula_file); + Syft::add_syfco_option(maxset, path_to_syfco); + + // 'fairness' subcommand + CLI::App *fairness = app.add_subcommand("fairness", "solve LTLf synthesis with fairness assumptions"); + Syft::add_spec_file_option(fairness, formula_file); + Syft::add_syfco_option(fairness, path_to_syfco); + Syft::add_assumption_file_option(fairness, assumption_file); + + // 'stability' subcommand + CLI::App *stability = app.add_subcommand("stability", "solve LTLf synthesis with stability assumptions"); + Syft::add_spec_file_option(stability, formula_file); + Syft::add_syfco_option(stability, path_to_syfco); + Syft::add_assumption_file_option(stability, assumption_file); + + // 'gr1' subcommand + CLI::App *gr1 = app.add_subcommand("gr1", "Solve LTLf synthesis with GR(1) conditions"); + Syft::add_spec_file_option(gr1, formula_file); + Syft::add_syfco_option(gr1, path_to_syfco); + Syft::add_slugs_option(gr1, path_to_slugs); + Syft::add_gr1_file_option(gr1, gr1_file); + Syft::add_env_safety_file_option(gr1, env_safety_file); + Syft::add_agent_safety_file_option(gr1, agent_safety_file); + + app.require_subcommand(1); CLI11_PARSE(app, argc, argv); - Syft::Stopwatch total_time_stopwatch; // stopwatch for end-to-end execution - total_time_stopwatch.start(); - - Syft::Stopwatch aut_time_stopwatch; // stopwatch for abstract single strategy - aut_time_stopwatch.start(); - - Syft::Parser parser; - // the parser assumes "syfco" is in the current working directory - parser = Syft::Parser::read_from_file("./syfco", formula_file); - bool sys_first = parser.get_sys_first(); - - Syft::Player starting_player = sys_first? Syft::Player::Agent : Syft::Player::Environment; - Syft::Player protagonist_player = Syft::Player::Agent; - bool realizability; - - Syft::InputOutputPartition partition = - Syft::InputOutputPartition::construct_from_input(parser.get_input_variables(), parser.get_output_variables()); - std::shared_ptr var_mgr = std::make_shared(); - var_mgr->create_named_variables(partition.input_variables); - var_mgr->create_named_variables(partition.output_variables); - - // Parsing the formula - std::shared_ptr driver; - driver = std::make_shared(); - std::stringstream formula_stream(parser.get_formula()); - driver->parse(formula_stream); - whitemech::lydia::ltlf_ptr parsed_formula = driver->get_result(); - // Apply no-empty semantics - auto context = driver->context; - auto not_end = context->makeLtlfNotEnd(); - parsed_formula = context->makeLtlfAnd({parsed_formula, not_end}); - - if (!maxset) { -// abstract single strategy -// preprocessing - auto one_step_result = preprocessing(*parsed_formula, partition, *var_mgr, starting_player); - bool preprocessing_success = one_step_result.realizability.has_value(); - if (preprocessing_success and one_step_result.realizability.value()) { - std::cout << Syft::REALIZABLE_STR << std::endl; - - CUDD::BDD move = one_step_result.winning_move; - auto total_time = total_time_stopwatch.stop(); - if (print_strategy) { - var_mgr->dump_dot(move.Add(), "strategy.dot"); - } - - if (print_times) { - std::cout << "Total time: " - << total_time.count() << " ms" << std::endl; - } - return 0; - } else if (preprocessing_success and !one_step_result.realizability.value()) { - std::cout << Syft::UNREALIZABLE_STR << std::endl; - auto total_time = total_time_stopwatch.stop(); - - if (print_times) { - std::cout << "Total time: " - << total_time.count() << " ms" << std::endl; - } - return 0; - } else { - // Preprocessing was not successful. Continuing with full DFA construction." - } - - Syft::ExplicitStateDfaMona explicit_dfa_mona = Syft::ExplicitStateDfaMona::dfa_of_formula(*parsed_formula); - - Syft::ExplicitStateDfa explicit_dfa = Syft::ExplicitStateDfa::from_dfa_mona(var_mgr, explicit_dfa_mona); - - Syft::SymbolicStateDfa symbolic_dfa = Syft::SymbolicStateDfa::from_explicit( - std::move(explicit_dfa)); - - auto aut_time = aut_time_stopwatch.stop(); - if (print_times) { - std::cout << "DFA construction time: " - << aut_time.count() << " ms" << std::endl; - } - - var_mgr->partition_variables(partition.input_variables, - partition.output_variables); - - Syft::ReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player, - protagonist_player, symbolic_dfa.final_states(), - var_mgr->cudd_mgr()->bddOne()); - Syft::SynthesisResult result = synthesizer.run(); - - realizability = result.realizability; - if (realizability == true) { - std::cout << Syft::REALIZABLE_STR << std::endl; - - Syft::Stopwatch abstract_single_strategy_time_stopwatch; // stopwatch for abstract single strategy - abstract_single_strategy_time_stopwatch.start(); - - auto transducer = synthesizer.AbstractSingleStrategy(std::move(result)); - if (print_strategy) { - transducer->dump_dot("strategy.dot"); - } - auto abstract_single_strategy_time = abstract_single_strategy_time_stopwatch.stop(); - if (print_times) { - std::cout << "Abstract single strategy time: " - << abstract_single_strategy_time.count() << " ms" << std::endl; - } - } else { - std::cout << Syft::UNREALIZABLE_STR << std::endl; - } - } else { - // abstract max strategy - Syft::ExplicitStateDfaMona explicit_dfa_mona = Syft::ExplicitStateDfaMona::dfa_of_formula(*parsed_formula); - Syft::ExplicitStateDfa explicit_dfa = Syft::ExplicitStateDfa::from_dfa_mona(var_mgr, explicit_dfa_mona); - - Syft::SymbolicStateDfa symbolic_dfa = Syft::SymbolicStateDfa::from_explicit( - std::move(explicit_dfa)); - - auto aut_time = aut_time_stopwatch.stop(); - if (print_times) { - std::cout << "DFA construction time: " - << aut_time.count() << " ms" << std::endl; - } - - Syft::Stopwatch nondef_strategy_time_stopwatch; // stopwatch for strategy_generator construction - nondef_strategy_time_stopwatch.start(); - - var_mgr->partition_variables(partition.input_variables, - partition.output_variables); - - Syft::ReachabilityMaxSetSynthesizer synthesizer(symbolic_dfa, starting_player, - protagonist_player, symbolic_dfa.final_states(), - var_mgr->cudd_mgr()->bddOne()); - Syft::SynthesisResult result = synthesizer.run(); - - realizability = result.realizability; - if (realizability == true) { - - auto nondef_strategy_time = nondef_strategy_time_stopwatch.stop(); - if (print_times) { - std::cout << "Nondeferring strategy generator construction time: " - << nondef_strategy_time.count() << " ms" << std::endl; - } - - Syft::Stopwatch def_strategy_time_stopwatch; // stopwatch for abstract max-deferring strategy - def_strategy_time_stopwatch.start(); - - Syft::MaxSet maxset_strategy = synthesizer.AbstractMaxSet(std::move(result)); - - auto def_strategy_time = def_strategy_time_stopwatch.stop(); - if (print_times) { - std::cout << "Deferring strategy generator construction time: " - << def_strategy_time.count() << " ms" << std::endl; - } - std::cout << Syft::REALIZABLE_STR << std::endl; - if (print_strategy) { - synthesizer.dump_dot(maxset_strategy, "def_strategy.dot", "nondef_strategy.dot"); - } - } - else{ - std::cout << Syft::UNREALIZABLE_STR << std::endl; - } - } - auto total_time = total_time_stopwatch.stop(); + std::shared_ptr driver = std::make_shared(); - if (print_times) { - std::cout << "Total time: " - << total_time.count() << " ms" << std::endl; - } + if (app.got_subcommand(synthesis)){ + Syft::SynthesisRunner(driver, formula_file, path_to_syfco, print_strategy, print_times).run(); + } + else if (app.got_subcommand(maxset)){ + Syft::MaxSetRunner(driver, formula_file, path_to_syfco, print_strategy, print_times).run(); + } + else if (app.got_subcommand(fairness)) { + Syft::FairnessRunner(driver, formula_file, path_to_syfco, assumption_file, print_strategy, print_times).run(); + } + else if (app.got_subcommand(stability)) { + Syft::StabilityRunner(driver, formula_file, path_to_syfco, assumption_file, print_times, print_times).run(); + } + else if (app.got_subcommand(gr1)) { + Syft::GR1Runner(driver, formula_file, path_to_syfco, path_to_slugs, gr1_file, env_safety_file, agent_safety_file, print_strategy, print_times).run(); + } + else { + assert(false && "CLI Parsing Error"); + } - return 0; + return 0; } diff --git a/src/cli/base.cpp b/src/cli/base.cpp new file mode 100644 index 0000000..cb93f4c --- /dev/null +++ b/src/cli/base.cpp @@ -0,0 +1,156 @@ +// +// Created by marcofavorito on 23/01/24. +// + +#include "base.hpp" +#include "lydia/parser/ltlf/driver.hpp" +#include "InputOutputPartition.h" +#include "Synthesizer.h" +#include "Preprocessing.h" + +namespace Syft { + + void Printer::dump_transducer_if_enabled(const Transducer& transducer, const std::string& output_file) const { + if (print_strategy_) { + transducer.dump_dot(output_file); + } + } + + void Printer::dump_add_if_enabled(const std::shared_ptr& var_mgr, const CUDD::ADD& add, const std::string &output_file) const { + if (print_strategy_) { + var_mgr->dump_dot(add, output_file); + } + } + + void Printer::dump_maxset_if_enabled(const ReachabilityMaxSetSynthesizer& maxset_synthesizer, const MaxSet& maxset_strategy, const std::string& def_strategy_output_file, const std::string& nondef_strategy_output_file) const { + if (print_strategy_) { + maxset_synthesizer.dump_dot(maxset_strategy, def_strategy_output_file, nondef_strategy_output_file); + } + } + + void Printer::print_times_if_enabled(const std::string& message, std::chrono::milliseconds time) const { + if (print_times_) { + out_ << message << ": " << time.count() << " ms" << std::endl; + } + } + + void add_assumption_file_option(CLI::App* app, std::string& assumption_file) { + app->add_option("-a,--assumption-file", assumption_file, "Assumption file")->required() -> check(CLI::ExistingFile); + } + + void add_gr1_file_option(CLI::App* app, std::string& gr1_file) { + app->add_option("-g,--gr1-file", gr1_file, "GR(1) specification file")->required() -> check(CLI::ExistingFile); + } + + void add_env_safety_file_option(CLI::App* app, std::optional& env_safety_file) { + app->add_option("-e,--env-safety-file", env_safety_file, "Formula file for the environment safety assumptions")->required() -> check(CLI::ExistingFile); + } + + void add_agent_safety_file_option(CLI::App* app, std::optional& agent_safety_file) { + app->add_option("-a,--agent-safety-file", agent_safety_file, "Formula file for the agent safety assumptions")->required() -> check(CLI::ExistingFile); + } + + void add_spec_file_option(CLI::App* app, std::string& spec_file) { + app->add_option("-f,--spec-file", spec_file, "Specification file")->required() -> check(CLI::ExistingFile); + } + + void add_syfco_option(CLI::App* app, std::string& path_to_syfco) { + app->add_option("-s,--syfco-path", path_to_syfco, "Path to Syfco binary") -> default_val(DEFAULT_SYFCO_PATH_) -> check(CLI::ExistingFile); + } + + void add_slugs_option(CLI::App* app, std::string& path_to_slugs) { + app->add_option("-S,--slugs-path", path_to_slugs, "Path to Slugs root directory") -> default_val(DEFAULT_SLUGS_PATH_) -> check(CLI::ExistingDirectory); + } + + TLSFArgs parse_tlsf(const std::shared_ptr& driver, const std::string& path_to_syfco, const std::string& formula_file) { + Syft::Parser parser; + // the parser assumes "syfco" is in the current working directory + parser = Syft::Parser::read_from_file(path_to_syfco, formula_file); + bool sys_first = parser.get_sys_first(); + + // get starting player and protagonist player + Syft::Player starting_player = sys_first? Syft::Player::Agent : Syft::Player::Environment; + Syft::Player protagonist_player = Syft::Player::Agent; + + Syft::InputOutputPartition partition = + Syft::InputOutputPartition::construct_from_input(parser.get_input_variables(), parser.get_output_variables()); + + // Parsing the formula + whitemech::lydia::ltlf_ptr parsed_formula = Syft::parse_formula(driver, parser.get_formula()); + + return {starting_player, protagonist_player, partition, parsed_formula}; + } + + whitemech::lydia::ltlf_ptr parse_formula(const std::shared_ptr& driver, const std::string& formula) { + std::stringstream formula_stream(formula); + driver->parse(formula_stream); + whitemech::lydia::ltlf_ptr parsed_formula = driver->get_result(); + // Apply no-empty semantics + auto context = driver->context; + auto not_end = context->makeLtlfNotEnd(); + parsed_formula = context->makeLtlfAnd({parsed_formula, not_end}); + return parsed_formula; + } + + std::shared_ptr build_var_mgr(const InputOutputPartition& partition) { + std::shared_ptr var_mgr = std::make_shared(); + var_mgr->create_named_variables(partition.input_variables); + var_mgr->create_named_variables(partition.output_variables); + return var_mgr; + } + + SymbolicStateDfa do_dfa_construction(const whitemech::lydia::LTLfFormula &formula, const std::shared_ptr &var_mgr) { + ExplicitStateDfaMona explicit_dfa_mona = ExplicitStateDfaMona::dfa_of_formula(formula); + ExplicitStateDfa explicit_dfa = ExplicitStateDfa::from_dfa_mona(var_mgr, explicit_dfa_mona); + SymbolicStateDfa symbolic_dfa = SymbolicStateDfa::from_explicit(explicit_dfa); + return symbolic_dfa; + } + + bool BaseRunner::handle_preprocessing_result_(const OneStepSynthesisResult& one_step_result, Stopwatch& total_time_stopwatch) const { + bool preprocessing_success = one_step_result.realizability.has_value(); + if (preprocessing_success and one_step_result.realizability.value()) { + CUDD::BDD move = one_step_result.winning_move; + auto total_time = total_time_stopwatch.stop(); + printer_.print_realizable(); + printer_.dump_add_if_enabled(var_mgr_, move.Add(), "strategy.dot"); + printer_.print_times_if_enabled("Total time", total_time); + return true; + } else if (preprocessing_success and !one_step_result.realizability.value()) { + auto total_time = total_time_stopwatch.stop(); + printer_.print_unrealizable(); + printer_.print_times_if_enabled("Total time", total_time); + return true; + } else { + // Preprocessing was not successful. Continuing with full DFA construction." + } + return false; + } + + Syft::SymbolicStateDfa BaseRunner::do_dfa_construction_() const { + Stopwatch aut_time_stopwatch_; + aut_time_stopwatch_.start(); + auto symbolic_dfa = do_dfa_construction(*args_.formula, var_mgr_); + auto aut_time = aut_time_stopwatch_.stop(); + printer_.print_times_if_enabled("DFA construction time", aut_time); + return symbolic_dfa; + } + + void BaseRunner::handle_synthesis_result_(const DfaGameSynthesizer& synthesizer, const SynthesisResult &result) const { + if (result.realizability) { + printer_.print_realizable(); + + // abstract single strategy + Syft::Stopwatch abstract_single_strategy_time_stopwatch; + abstract_single_strategy_time_stopwatch.start(); + auto transducer = synthesizer.AbstractSingleStrategy(result); + auto abstract_single_strategy_time = abstract_single_strategy_time_stopwatch.stop(); + printer_.print_times_if_enabled("Abstract single strategy time", abstract_single_strategy_time); + + // dump strategy + printer_.dump_transducer_if_enabled(*transducer, "strategy.dot"); + } else { + printer_.print_unrealizable(); + } + } + +} \ No newline at end of file diff --git a/src/cli/base.hpp b/src/cli/base.hpp new file mode 100644 index 0000000..dc9b75d --- /dev/null +++ b/src/cli/base.hpp @@ -0,0 +1,96 @@ +// +// Created by marcofavorito on 23/01/24. +// + +#ifndef LYDIASYFT_CLI_BASE_HPP +#define LYDIASYFT_CLI_BASE_HPP + +#include +#include +#include "lydia/types.hpp" +#include "Player.h" +#include "VarMgr.h" +#include "Parser.h" +#include "InputOutputPartition.h" +#include "Transducer.h" +#include "Stopwatch.h" +#include "Synthesizer.h" +#include "ReachabilityMaxSetSynthesizer.h" +#include "lydia/parser/ltlf/driver.hpp" + + +namespace Syft { + static const std::string DEFAULT_SYFCO_PATH_ = "./syfco"; + static const std::string DEFAULT_SLUGS_PATH_ = "./slugs"; + + struct TLSFArgs { + const Player starting_player; + const Player protagonist_player; + const InputOutputPartition partition; + const whitemech::lydia::ltlf_ptr formula; + }; + + class Printer { + private: + const bool print_strategy_; + const bool print_times_; + + // for output messages + std::ostream& out_; + + public: + Printer(bool print_strategy, bool print_times, std::ostream& out) : + print_strategy_(print_strategy), print_times_(print_times), out_(out) {} + + void dump_transducer_if_enabled(const Transducer& transducer, const std::string& output_file = "strategy.dot") const; + void dump_add_if_enabled(const std::shared_ptr& var_mgr, const CUDD::ADD& add, const std::string &output_file) const; + void dump_maxset_if_enabled(const ReachabilityMaxSetSynthesizer& maxset_synthesizer, const MaxSet& maxset_strategy, const std::string& def_strategy_output_file = "def_strategy.dot", const std::string& nondef_strategy_output_file = "nondef_strategy.dot") const; + + void print_times_if_enabled(const std::string& message, std::chrono::milliseconds time) const; + void print_realizable() const { out_ << Syft::REALIZABLE_STR << std::endl; } + void print_unrealizable() const { out_ << Syft::UNREALIZABLE_STR << std::endl; } + + }; + + + void add_assumption_file_option(CLI::App*, std::string&); + void add_gr1_file_option(CLI::App*, std::string&); + void add_env_safety_file_option(CLI::App*, std::optional&); + void add_agent_safety_file_option(CLI::App*, std::optional&); + void add_spec_file_option(CLI::App*, std::string&); + void add_syfco_option(CLI::App*, std::string&); + void add_slugs_option(CLI::App*, std::string&); + + TLSFArgs parse_tlsf(const std::shared_ptr& driver, const std::string& path_to_syfco, const std::string& formula_file); + whitemech::lydia::ltlf_ptr parse_formula(const std::shared_ptr& driver, const std::string& formula); + std::shared_ptr build_var_mgr(const InputOutputPartition& partition); + + SymbolicStateDfa do_dfa_construction(const whitemech::lydia::LTLfFormula& formula, const std::shared_ptr& var_mgr); + + class BaseRunner { + protected: + const std::string formula_file_; + const std::string path_to_syfco_; + + const TLSFArgs args_; + const std::shared_ptr var_mgr_; + + const Printer printer_; + + std::shared_ptr driver_; + + bool handle_preprocessing_result_(const OneStepSynthesisResult& one_step_result, Stopwatch& total_time_stopwatch) const; + void handle_synthesis_result_(const DfaGameSynthesizer& synthesizer, const SynthesisResult& result) const; + SymbolicStateDfa do_dfa_construction_() const; + public: + BaseRunner(const std::shared_ptr& driver, const std::string& formula_file, const std::string& path_to_syfco, bool print_strategy, bool print_times) : + driver_(driver), + formula_file_(formula_file), path_to_syfco_(path_to_syfco), + printer_(print_strategy, print_times, std::cout), + args_(parse_tlsf(driver, path_to_syfco, formula_file)), + var_mgr_(build_var_mgr(args_.partition)) {} + }; + +} + +#endif //LYDIASYFT_CLI_BASE_HPP diff --git a/src/cli/fairness.cpp b/src/cli/fairness.cpp new file mode 100644 index 0000000..73b83d4 --- /dev/null +++ b/src/cli/fairness.cpp @@ -0,0 +1,51 @@ +// +// Created by marcofavorito on 22/01/24. +// + +#include + +#include "synthesis.hpp" +#include +#include +#include + +#include "Stopwatch.h" + +#include "../parser/Parser.h" +#include "ExplicitStateDfaMona.h" +#include "ReachabilitySynthesizer.h" +#include "ReachabilityMaxSetSynthesizer.h" +#include "InputOutputPartition.h" +#include "Preprocessing.h" +#include "fairness.hpp" +#include "FairReachabilitySynthesizer.h" + +#include +#include +#include + + +namespace Syft { + + void Syft::FairnessRunner::run() const { + Syft::Stopwatch total_time_stopwatch; + total_time_stopwatch.start(); + + // proceed with DFA construction + auto symbolic_dfa = do_dfa_construction_(); + + // do maxset synthesis + do_fairness_synthesis_(symbolic_dfa); + + auto total_time = total_time_stopwatch.stop(); + printer_.print_times_if_enabled("Total time", total_time); + } + + void FairnessRunner::do_fairness_synthesis_(const SymbolicStateDfa &symbolic_dfa) const { + Syft::FairReachabilitySynthesizer synthesizer(symbolic_dfa, args_.starting_player, + args_.protagonist_player, symbolic_dfa.final_states(), + var_mgr_->cudd_mgr()->bddOne(), assumption_filename_); + Syft::SynthesisResult result = synthesizer.run(); + handle_synthesis_result_(synthesizer, result); + } +} diff --git a/src/cli/fairness.hpp b/src/cli/fairness.hpp new file mode 100644 index 0000000..41a7ee0 --- /dev/null +++ b/src/cli/fairness.hpp @@ -0,0 +1,32 @@ +// +// Created by marcofavorito on 22/01/24. +// + +#ifndef LYDIASYFT_CLI_FAIRNESS_H +#define LYDIASYFT_CLI_FAIRNESS_H + +#include + + +namespace Syft { + + class FairnessRunner : public BaseRunner { + private: + const std::string assumption_filename_; + + void do_fairness_synthesis_(const SymbolicStateDfa &dfa) const; + + public: + FairnessRunner(const std::shared_ptr& driver, + const std::string &formula_file, const std::string &path_to_syfco, + const std::string &assumption_filename, bool print_strategy, bool print_times) : BaseRunner( + driver, formula_file, path_to_syfco, print_strategy, print_times), assumption_filename_(assumption_filename) {} + + void run() const; + + }; + +} + + +#endif //LYDIASYFT_CLI_FAIRNESS_H diff --git a/src/cli/gr1.cpp b/src/cli/gr1.cpp new file mode 100644 index 0000000..b2e8348 --- /dev/null +++ b/src/cli/gr1.cpp @@ -0,0 +1,89 @@ +// +// Created by marcofavorito on 22/01/24. +// + +#include + +#include "synthesis.hpp" + +#include "Stopwatch.h" + +#include "ExplicitStateDfaMona.h" +#include "ReachabilityMaxSetSynthesizer.h" +#include "InputOutputPartition.h" +#include "Preprocessing.h" +#include "gr1.hpp" +#include "GR1.h" +#include "GR1ReachabilitySynthesizer.h" + +#include + + +namespace Syft { + + void Syft::GR1Runner::run() const { + Syft::Stopwatch total_time_stopwatch; + total_time_stopwatch.start(); + + // proceed with DFAs construction + auto agent_safety_dfa = do_dfa_construction_with_message_(*agent_safety_, var_mgr_, "Agent Safety DFA construction time"); + auto env_safety_dfa = do_dfa_construction_with_message_(*env_safety_, var_mgr_, "Env Safety DFA construction time"); + auto agent_goal_dfa = do_dfa_construction_with_message_(*args_.formula, var_mgr_, "Agent Goal DFA construction time"); + + // do GR(1) synthesis + do_gr1_synthesis_(agent_safety_dfa, env_safety_dfa, agent_goal_dfa); + + auto total_time = total_time_stopwatch.stop(); + printer_.print_times_if_enabled("Total time", total_time); + } + + Syft::SymbolicStateDfa GR1Runner::do_dfa_construction_with_message_(const whitemech::lydia::LTLfFormula& formula, const std::shared_ptr& var_mgr, const std::string& msg) const { + Stopwatch aut_time_stopwatch_; + aut_time_stopwatch_.start(); + auto symbolic_dfa = do_dfa_construction(formula, var_mgr); + auto aut_time = aut_time_stopwatch_.stop(); + printer_.print_times_if_enabled(msg, aut_time); + return symbolic_dfa; + } + + void GR1Runner::do_gr1_synthesis_(const SymbolicStateDfa& agent_safety_dfa, const SymbolicStateDfa& env_safety_dfa, const SymbolicStateDfa& agent_goal_dfa) const { + Syft::GR1 gr1 = Syft::GR1::read_from_gr1_file(var_mgr_, gr1_file_); + Syft::GR1ReachabilitySynthesizer synthesizer(var_mgr_, gr1, env_safety_dfa, + agent_goal_dfa, agent_safety_dfa, path_to_slugs_, "problem"); + Syft::SynthesisResult result = synthesizer.run(); + handle_gr1_synthesis_result_(synthesizer, result); + } + + void GR1Runner::handle_gr1_synthesis_result_(const GR1ReachabilitySynthesizer &synthesizer, + const SynthesisResult &result) const { + if (result.realizability) { + printer_.print_realizable(); + + // TODO + // // abstract single strategy + // Syft::Stopwatch abstract_single_strategy_time_stopwatch; + // abstract_single_strategy_time_stopwatch.start(); + // auto transducer = abstract_single_strategy(result.winning_moves, var_mgr_, ...); + // auto abstract_single_strategy_time = abstract_single_strategy_time_stopwatch.stop(); + // printer_.print_times_if_enabled("Abstract single strategy time", abstract_single_strategy_time); + // // dump strategy + // printer_.dump_transducer_if_enabled(*transducer, "strategy.dot"); + } else { + printer_.print_unrealizable(); + } + } + + std::string read_assumption_file_if_file_specified_(const std::optional& filename) { + if (!filename.has_value()) { + return "true"; + } + std::ifstream file(filename.value()); + if (!file.good()) { + throw std::runtime_error("File " + filename.value() + " not found"); + } + std::string assumption_str; + std::getline(file, assumption_str); + return assumption_str; + } + +} diff --git a/src/cli/gr1.hpp b/src/cli/gr1.hpp new file mode 100644 index 0000000..7ff8af8 --- /dev/null +++ b/src/cli/gr1.hpp @@ -0,0 +1,48 @@ +// +// Created by marcofavorito on 22/01/24. +// + +#ifndef LYDIASYFT_CLI_GR1_H +#define LYDIASYFT_CLI_GR1_H + +#include +#include "GR1ReachabilitySynthesizer.h" + + +namespace Syft { + + std::string read_assumption_file_if_file_specified_(const std::optional &filename); + + class GR1Runner : public BaseRunner { + private: + const std::string path_to_slugs_; + const std::string gr1_file_; + const std::optional env_safety_file_; + const std::optional agent_safety_file_; + + const whitemech::lydia::ltlf_ptr agent_safety_; + const whitemech::lydia::ltlf_ptr env_safety_; + + Syft::SymbolicStateDfa do_dfa_construction_with_message_(const whitemech::lydia::LTLfFormula& formula, const std::shared_ptr& var_mgr, const std::string& msg) const; + void do_gr1_synthesis_(const SymbolicStateDfa& dfa, const SymbolicStateDfa& dfa1, const SymbolicStateDfa& dfa2) const; + void handle_gr1_synthesis_result_(const GR1ReachabilitySynthesizer& synthesizer, const SynthesisResult &result) const; + + + public: + GR1Runner(const std::shared_ptr& driver, + const std::string &formula_file, const std::string &path_to_syfco, const std::string &path_to_slugs, + const std::string &gr1_file, const std::optional &env_safety_file, const std::optional &agent_safety_file, + bool print_strategy, bool print_times) : BaseRunner(driver, formula_file, path_to_syfco, print_strategy, print_times), + path_to_slugs_(path_to_slugs), gr1_file_(gr1_file), + env_safety_file_(env_safety_file), + agent_safety_file_(agent_safety_file), + agent_safety_(parse_formula(driver_, read_assumption_file_if_file_specified_(agent_safety_file_))), + env_safety_(parse_formula(driver_, read_assumption_file_if_file_specified_(env_safety_file_))) {} + + void run() const; + }; + +} + + +#endif //LYDIASYFT_CLI_GR1_H diff --git a/src/cli/maxset.cpp b/src/cli/maxset.cpp new file mode 100644 index 0000000..693690e --- /dev/null +++ b/src/cli/maxset.cpp @@ -0,0 +1,59 @@ +// +// Created by marcofavorito on 22/01/24. +// + +#include "synthesis.hpp" +#include "Stopwatch.h" +#include "ReachabilityMaxSetSynthesizer.h" +#include "Preprocessing.h" +#include "maxset.hpp" +#include + + +namespace Syft { + + void MaxSetRunner::run() { + Syft::Stopwatch total_time_stopwatch; + total_time_stopwatch.start(); + + // proceed with DFA construction + auto symbolic_dfa = do_dfa_construction_(); + + // do maxset synthesis + do_maxset_synthesis(symbolic_dfa); + + auto total_time = total_time_stopwatch.stop(); + printer_.print_times_if_enabled("Total time", total_time); + } + + void MaxSetRunner::do_maxset_synthesis(const SymbolicStateDfa& symbolic_dfa) { + Syft::Stopwatch nondef_strategy_time_stopwatch; // stopwatch for strategy_generator construction + nondef_strategy_time_stopwatch.start(); + + var_mgr_->partition_variables(args_.partition.input_variables, args_.partition.output_variables); + + Syft::ReachabilityMaxSetSynthesizer synthesizer(symbolic_dfa, args_.starting_player, + args_.protagonist_player, symbolic_dfa.final_states(), + var_mgr_->cudd_mgr()->bddOne()); + Syft::SynthesisResult result = synthesizer.run(); + + if (result.realizability) { + printer_.print_realizable(); + + auto nondef_strategy_time = nondef_strategy_time_stopwatch.stop(); + printer_.print_times_if_enabled("Nondeferring strategy generator construction time", nondef_strategy_time); + + Syft::Stopwatch def_strategy_time_stopwatch; + def_strategy_time_stopwatch.start(); + Syft::MaxSet maxset_strategy = synthesizer.AbstractMaxSet(result); + auto def_strategy_time = def_strategy_time_stopwatch.stop(); + printer_.print_times_if_enabled("Deferring strategy generator construction time", def_strategy_time); + + printer_.dump_maxset_if_enabled(synthesizer, maxset_strategy, "def_strategy.dot", "nondef_strategy.dot"); + } + else{ + printer_.print_unrealizable(); + } + } + +} diff --git a/src/cli/maxset.hpp b/src/cli/maxset.hpp new file mode 100644 index 0000000..72595c1 --- /dev/null +++ b/src/cli/maxset.hpp @@ -0,0 +1,32 @@ +// +// Created by marcofavorito on 22/01/24. +// + +#ifndef LYDIASYFT_CLI_MAXSET_H +#define LYDIASYFT_CLI_MAXSET_H + +#include + + +namespace Syft { + + + class MaxSetRunner : public BaseRunner { + private: + Syft::Stopwatch aut_time_stopwatch_; // stopwatch for automata construction + Syft::Stopwatch nondef_strategy_time_stopwatch_; // stopwatch for nondeferring strategy + Syft::Stopwatch def_strategy_time_stopwatch_; // stopwatch for deferring strategy + + void do_maxset_synthesis(const SymbolicStateDfa& dfa); + public: + MaxSetRunner(const std::shared_ptr& driver, const std::string& formula_file, const std::string& path_to_syfco, bool print_strategy, bool print_times) : + BaseRunner(driver, formula_file, path_to_syfco, print_strategy, print_times) {} + void run(); + + }; + + +} + + +#endif //LYDIASYFT_CLI_MAXSET_H diff --git a/src/cli/stability.cpp b/src/cli/stability.cpp new file mode 100644 index 0000000..81fd22a --- /dev/null +++ b/src/cli/stability.cpp @@ -0,0 +1,51 @@ +// +// Created by marcofavorito on 22/01/24. +// + +#include + +#include "synthesis.hpp" +#include +#include +#include + +#include "Stopwatch.h" + +#include "../parser/Parser.h" +#include "ExplicitStateDfaMona.h" +#include "ReachabilitySynthesizer.h" +#include "ReachabilityMaxSetSynthesizer.h" +#include "InputOutputPartition.h" +#include "Preprocessing.h" +#include "stability.hpp" +#include "StableReachabilitySynthesizer.h" + +#include +#include +#include + + +namespace Syft { + + void StabilityRunner::run() { + Syft::Stopwatch total_time_stopwatch; + total_time_stopwatch.start(); + + // proceed with DFA construction + auto symbolic_dfa = do_dfa_construction_(); + + // do maxset synthesis + do_stability_synthesis_(symbolic_dfa); + + auto total_time = total_time_stopwatch.stop(); + printer_.print_times_if_enabled("Total time", total_time); + } + + void StabilityRunner::do_stability_synthesis_(const Syft::SymbolicStateDfa &symbolic_dfa) { + Syft::StableReachabilitySynthesizer synthesizer(symbolic_dfa, args_.starting_player, + args_.protagonist_player, symbolic_dfa.final_states(), + var_mgr_->cudd_mgr()->bddOne(), assumption_filename_); + Syft::SynthesisResult result = synthesizer.run(); + handle_synthesis_result_(synthesizer, result); + } +} diff --git a/src/cli/stability.hpp b/src/cli/stability.hpp new file mode 100644 index 0000000..d325ac0 --- /dev/null +++ b/src/cli/stability.hpp @@ -0,0 +1,30 @@ +// +// Created by marcofavorito on 22/01/24. +// + +#ifndef LYDIASYFT_CLI_STABILITY_H +#define LYDIASYFT_CLI_STABILITY_H + +#include + + +namespace Syft { + + class StabilityRunner : public BaseRunner { + private: + std::string assumption_filename_; + + void do_stability_synthesis_(const SymbolicStateDfa &symbolic_dfa); + + public: + StabilityRunner(const std::shared_ptr& driver, + const std::string &formula_file, const std::string &path_to_syfco, + const std::string &assumption_filename, bool print_strategy, bool print_times) : BaseRunner( + driver, formula_file, path_to_syfco, print_strategy, print_times), assumption_filename_(assumption_filename) {} + + void run(); + + }; +} + +#endif //LYDIASYFT_CLI_STABILITY_H \ No newline at end of file diff --git a/src/cli/synthesis.cpp b/src/cli/synthesis.cpp new file mode 100644 index 0000000..8a625c1 --- /dev/null +++ b/src/cli/synthesis.cpp @@ -0,0 +1,44 @@ +// +// Created by marcofavorito on 22/01/24. +// + +#include "synthesis.hpp" +#include "Stopwatch.h" +#include "ReachabilitySynthesizer.h" +#include "Preprocessing.h" +#include + + +namespace Syft { + + void SynthesisRunner::do_synthesis_(const SymbolicStateDfa& symbolic_dfa) { + var_mgr_->partition_variables(args_.partition.input_variables, args_.partition.output_variables); + Syft::ReachabilitySynthesizer synthesizer(symbolic_dfa, args_.starting_player, + args_.protagonist_player, symbolic_dfa.final_states(), + var_mgr_->cudd_mgr()->bddOne()); + Syft::SynthesisResult result = synthesizer.run(); + handle_synthesis_result_(synthesizer, result); + } + + void SynthesisRunner::run() { + Syft::Stopwatch total_time_stopwatch; + total_time_stopwatch.start(); + + // preprocessing + auto one_step_result = preprocessing(*args_.formula, args_.partition, *var_mgr_, args_.starting_player); + if (handle_preprocessing_result_(one_step_result, total_time_stopwatch)) { + // preprocessing was successful + return; + } + + // proceed with DFA construction + auto symbolic_dfa = do_dfa_construction_(); + + // do synthesis + do_synthesis_(symbolic_dfa); + + auto total_time = total_time_stopwatch.stop(); + printer_.print_times_if_enabled("Total time", total_time); + } + +} diff --git a/src/cli/synthesis.hpp b/src/cli/synthesis.hpp new file mode 100644 index 0000000..cca680b --- /dev/null +++ b/src/cli/synthesis.hpp @@ -0,0 +1,31 @@ +// +// Created by marcofavorito on 22/01/24. +// + +#ifndef LYDIASYFT_CLI_SYNTHESIS_H +#define LYDIASYFT_CLI_SYNTHESIS_H + +#include +#include "VarMgr.h" +#include "Stopwatch.h" +#include "base.hpp" +#include "ReachabilitySynthesizer.h" + + +namespace Syft { + + class SynthesisRunner : public BaseRunner { + private: + + void do_synthesis_(const SymbolicStateDfa &symbolic_dfa); + + public: + SynthesisRunner(const std::shared_ptr& driver, const std::string &formula_file, const std::string &path_to_syfco, bool print_strategy, + bool print_times) : BaseRunner(driver, formula_file, path_to_syfco, print_strategy, print_times) {} + + void run(); + + }; +} + +#endif //LYDIASYFT_CLI_SYNTHESIS_H diff --git a/src/synthesis/header/DfaGameSynthesizer.h b/src/synthesis/header/DfaGameSynthesizer.h index 4dbddad..d9b8b2d 100644 --- a/src/synthesis/header/DfaGameSynthesizer.h +++ b/src/synthesis/header/DfaGameSynthesizer.h @@ -8,6 +8,13 @@ namespace Syft { +std::unique_ptr abstract_single_strategy(const CUDD::BDD& winning_moves, + const std::shared_ptr& var_mgr, + const std::vector& initial_vector, + const std::vector& transition_vector, + Player starting_player); +std::unordered_map synthesize_strategy(const CUDD::BDD& winning_moves, const std::shared_ptr& var_mgr); + /** * \brief A synthesizer for a game whose arena is a symbolic-state DFA. */ @@ -25,10 +32,7 @@ class DfaGameSynthesizer : public Synthesizer { CUDD::BDD preimage(const CUDD::BDD& winning_states) const; CUDD::BDD project_into_states(const CUDD::BDD& winning_moves) const; - - std::unordered_map synthesize_strategy( - const CUDD::BDD& winning_moves) const; - + bool includes_initial_state(const CUDD::BDD& winning_states) const; public: @@ -40,6 +44,7 @@ class DfaGameSynthesizer : public Synthesizer { * * \param spec A symbolic-state DFA representing the game's arena. * \param starting_player The player that moves first each turn. + * \param protagonist_player The player for which we aim to find the winning strategy. */ DfaGameSynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player); @@ -51,6 +56,8 @@ class DfaGameSynthesizer : public Synthesizer { */ virtual SynthesisResult run() const override = 0; + + std::unique_ptr AbstractSingleStrategy(const SynthesisResult& result) const; }; } diff --git a/src/synthesis/header/FairReachabilitySynthesizer.h b/src/synthesis/header/FairReachabilitySynthesizer.h index 8c328c2..213bf22 100644 --- a/src/synthesis/header/FairReachabilitySynthesizer.h +++ b/src/synthesis/header/FairReachabilitySynthesizer.h @@ -34,9 +34,9 @@ namespace Syft { * \param starting_player The player that moves first each turn. * \param goal_states The set of states that the agent must reach to win. */ - FairReachabilitySynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player, - CUDD::BDD goal_states, CUDD::BDD state_space, - std::string& assumption_filename); + FairReachabilitySynthesizer(const SymbolicStateDfa& spec, Player starting_player, Player protagonist_player, + const CUDD::BDD& goal_states, const CUDD::BDD& state_space, + const std::string& assumption_filename); @@ -50,8 +50,6 @@ namespace Syft { */ virtual SynthesisResult run() const final; - std::unique_ptr AbstractSingleStrategy(SynthesisResult result) const; - }; } diff --git a/src/synthesis/header/GR1.h b/src/synthesis/header/GR1.h index 27a43d7..11aa782 100644 --- a/src/synthesis/header/GR1.h +++ b/src/synthesis/header/GR1.h @@ -54,7 +54,7 @@ namespace Syft { /** * \brief Stores a player justice */ - static CUDD::BDD read_gr1_justice(std::shared_ptr& var_mgr, + static CUDD::BDD read_gr1_justice(const std::shared_ptr& var_mgr, std::istream& in, std::size_t& line_number){ std::string line; @@ -103,7 +103,7 @@ namespace Syft { * \param gr1_filename The name of the file to read the GR(1) condition from. * \return The GR(1) condition stored in the file */ - static GR1 read_from_gr1_file(std::shared_ptr& var_mgr, + static GR1 read_from_gr1_file(const std::shared_ptr& var_mgr, const std::string& gr1_filename) { GR1 gr1; std::ifstream in(gr1_filename); diff --git a/src/synthesis/header/GR1ReachabilitySynthesizer.h b/src/synthesis/header/GR1ReachabilitySynthesizer.h index 95ee8f2..06c68ec 100644 --- a/src/synthesis/header/GR1ReachabilitySynthesizer.h +++ b/src/synthesis/header/GR1ReachabilitySynthesizer.h @@ -11,21 +11,19 @@ #include "Stopwatch.h" #include "SymbolicStateDfa.h" #include "Synthesizer.h" - +#include "DfaGameSynthesizer.h" namespace Syft { - class GR1ReachabilitySynthesizer{ + class GR1ReachabilitySynthesizer { private: - std::shared_ptr var_mgr_; - GR1 gr1_; - SymbolicStateDfa env_safety_; - SymbolicStateDfa agn_safety_; - SymbolicStateDfa agn_reach_; - Player starting_player_; - - CUDD::BDD safe_states_ = var_mgr_->cudd_mgr()->bddOne(); + const std::shared_ptr& var_mgr_; + const GR1& gr1_; + const SymbolicStateDfa& env_safety_; + const SymbolicStateDfa& agn_safety_; + const SymbolicStateDfa& agn_reach_; + const std::string& benchmark_name_; std::string slugs_dir_; @@ -42,7 +40,7 @@ namespace Syft { * \param GR1 game arena * \param The file that should be written to */ - void print_variables(const SymbolicStateDfa arena, const std::string& filename) const; + void print_variables(const SymbolicStateDfa& arena, const std::string& filename) const; /** * \brief Prints out INITIAL conditions in Slugs format @@ -66,9 +64,10 @@ namespace Syft { * c | d * * \param GR1 game arena + * \param var_mgr var manager * \param The file that should be written to */ - void print_transitions(const SymbolicStateDfa arena, const std::string& filename) const; + void print_transitions(const SymbolicStateDfa& arena, const CUDD::BDD& safe_states, const std::string& filename) const; /** * \brief Prints out LIVENESS constraints in Slugs format @@ -77,17 +76,16 @@ namespace Syft { * [SYS_LIVENESS] * d * c = 2 - * \param GR1 game arena * \param The file that should be written to */ - void print_liveness_constraints(const SymbolicStateDfa arena, const std::string& filename) const; + void print_liveness_constraints(const std::string& filename) const; /** * Get the path to the SLUGS binary. * * @return the path to the SLUGS binary. */ - std::string get_slugs_path(); + std::string get_slugs_path() const; public: @@ -101,11 +99,12 @@ namespace Syft { * \param slugs_dir The root directory of the SLUGS project * */ - GR1ReachabilitySynthesizer(std::shared_ptr var_mgr, GR1 gr1, SymbolicStateDfa env_safety, - SymbolicStateDfa agn_reach, SymbolicStateDfa agn_safety, std::string slugs_dir); + GR1ReachabilitySynthesizer(const std::shared_ptr& var_mgr, const GR1& gr1, const SymbolicStateDfa& env_safety, + const SymbolicStateDfa& agn_reach, const SymbolicStateDfa& agn_safety, const std::string& slugs_dir, + const std::string& benchmark_name); const std::string exec_slugs(const std::string& slugs, const std::string& slugs_input_file, - const std::string& slugs_res_file, const std::string& slugs_strategy_file); + const std::string& slugs_res_file, const std::string& slugs_strategy_file) const; /** * \brief Solves the LTLf/GR(1) game. @@ -115,7 +114,8 @@ namespace Syft { * a set of agent winning states * a transducer representing a winning strategy or nullptr if the game is unrealizable. */ - SynthesisResult run(std::string& benchmark_name); + SynthesisResult run() const; + }; } #endif //LYDIASYFT_GR1REACHABILITYSYNTHESIZER_H diff --git a/src/synthesis/header/ReachabilityMaxSetSynthesizer.h b/src/synthesis/header/ReachabilityMaxSetSynthesizer.h index 3aff088..04bbdce 100644 --- a/src/synthesis/header/ReachabilityMaxSetSynthesizer.h +++ b/src/synthesis/header/ReachabilityMaxSetSynthesizer.h @@ -44,7 +44,7 @@ namespace Syft { */ virtual SynthesisResult run() const final; - MaxSet AbstractMaxSet(SynthesisResult result) const; + MaxSet AbstractMaxSet(const SynthesisResult&) const; void dump_dot(MaxSet maxset, const std::string& def_filename, const std::string& nondef_filename) const; diff --git a/src/synthesis/header/ReachabilitySynthesizer.h b/src/synthesis/header/ReachabilitySynthesizer.h index bd6434f..89b764a 100644 --- a/src/synthesis/header/ReachabilitySynthesizer.h +++ b/src/synthesis/header/ReachabilitySynthesizer.h @@ -36,8 +36,6 @@ namespace Syft { */ virtual SynthesisResult run() const final; - std::unique_ptr AbstractSingleStrategy(SynthesisResult result) const; - }; } diff --git a/src/synthesis/header/StableReachabilitySynthesizer.h b/src/synthesis/header/StableReachabilitySynthesizer.h index 9f79d1b..b1edca0 100644 --- a/src/synthesis/header/StableReachabilitySynthesizer.h +++ b/src/synthesis/header/StableReachabilitySynthesizer.h @@ -50,8 +50,6 @@ namespace Syft { */ virtual SynthesisResult run() const final; - std::unique_ptr AbstractSingleStrategy(SynthesisResult result) const; - }; } diff --git a/src/synthesis/header/Synthesizer.h b/src/synthesis/header/Synthesizer.h index cb3d419..b2a0700 100644 --- a/src/synthesis/header/Synthesizer.h +++ b/src/synthesis/header/Synthesizer.h @@ -18,6 +18,7 @@ namespace Syft { CUDD::BDD winning_states; CUDD::BDD winning_moves; std::unique_ptr transducer; + CUDD::BDD safe_states; }; struct OneStepSynthesisResult{ diff --git a/src/synthesis/header/Transducer.h b/src/synthesis/header/Transducer.h index f1a6278..23e5d34 100644 --- a/src/synthesis/header/Transducer.h +++ b/src/synthesis/header/Transducer.h @@ -20,20 +20,19 @@ namespace Syft { class Transducer { private: - std::shared_ptr var_mgr_; - - std::vector initial_vector_; - std::unordered_map output_function_; - std::vector transition_function_; - Player starting_player_; - Player protagonist_player_; + const std::shared_ptr& var_mgr_; + const std::vector& initial_vector_; + const std::unordered_map& output_function_; + const std::vector& transition_function_; + const Player starting_player_; + const Player protagonist_player_; public: - Transducer(std::shared_ptr var_mgr, - std::vector initial_vector, - std::unordered_map output_function, - std::vector transition_function, + Transducer(const std::shared_ptr& var_mgr, + const std::vector& initial_vector, + const std::unordered_map& output_function, + const std::vector& transition_function, Player starting_player, Player protagonist_player = Player::Agent); diff --git a/src/synthesis/source/DfaGameSynthesizer.cpp b/src/synthesis/source/DfaGameSynthesizer.cpp index d14a1ce..73e4b61 100644 --- a/src/synthesis/source/DfaGameSynthesizer.cpp +++ b/src/synthesis/source/DfaGameSynthesizer.cpp @@ -73,12 +73,12 @@ bool DfaGameSynthesizer::includes_initial_state( return winning_states.Eval(copy.data()).IsOne(); } -std::unordered_map DfaGameSynthesizer::synthesize_strategy( - const CUDD::BDD& winning_moves) const { +std::unordered_map synthesize_strategy(const CUDD::BDD& winning_moves, + const std::shared_ptr& var_mgr){ std::vector parameterized_output_function; int* output_indices; - CUDD::BDD output_cube = var_mgr_->output_cube(); - std::size_t output_count = var_mgr_->output_variable_count(); + CUDD::BDD output_cube = var_mgr->output_cube(); + std::size_t output_count = var_mgr->output_variable_count(); // Need to negate the BDD because b.SolveEqn(...) solves the equation b = 0 CUDD::BDD pre = (!winning_moves).SolveEqn(output_cube, @@ -117,7 +117,7 @@ std::unordered_map DfaGameSynthesizer::synthesize_strategy( int parameter_index = index_copy[j]; // Can be anything, set to the constant 1 for simplicity - CUDD::BDD parameter_value = var_mgr_->cudd_mgr()->bddOne(); + CUDD::BDD parameter_value = var_mgr->cudd_mgr()->bddOne(); output_function[output_index] = output_function[output_index].Compose(parameter_value, @@ -128,4 +128,19 @@ std::unordered_map DfaGameSynthesizer::synthesize_strategy( return output_function; } +std::unique_ptr DfaGameSynthesizer::AbstractSingleStrategy(const SynthesisResult& result) const { + return abstract_single_strategy(result.winning_moves, var_mgr_, initial_vector_, spec_.transition_function(), starting_player_); +} + +std::unique_ptr abstract_single_strategy( + const CUDD::BDD& winning_moves, + const std::shared_ptr& var_mgr, + const std::vector& initial_vector, + const std::vector& transition_vector, + Player starting_player) { + std::unordered_map strategy = synthesize_strategy(winning_moves, var_mgr); + auto transducer = std::make_unique(var_mgr, initial_vector, strategy, transition_vector, starting_player); + return transducer; +} + } diff --git a/src/synthesis/source/FairReachabilitySynthesizer.cpp b/src/synthesis/source/FairReachabilitySynthesizer.cpp index 978366a..cb98953 100644 --- a/src/synthesis/source/FairReachabilitySynthesizer.cpp +++ b/src/synthesis/source/FairReachabilitySynthesizer.cpp @@ -10,11 +10,9 @@ namespace Syft { - FairReachabilitySynthesizer::FairReachabilitySynthesizer(SymbolicStateDfa spec, - Player starting_player, Player protagonist_player, - CUDD::BDD goal_states, - CUDD::BDD state_space, - std::string& assumption_filename) + FairReachabilitySynthesizer::FairReachabilitySynthesizer(const SymbolicStateDfa& spec, Player starting_player, Player protagonist_player, + const CUDD::BDD& goal_states, const CUDD::BDD& state_space, + const std::string& assumption_filename) : DfaGameSynthesizer(spec, starting_player, protagonist_player) , goal_states_(goal_states), state_space_(state_space) { @@ -105,16 +103,6 @@ namespace Syft { } - std::unique_ptr FairReachabilitySynthesizer::AbstractSingleStrategy(SynthesisResult result) const { - std::unordered_map strategy = synthesize_strategy( - result.winning_moves); - - auto transducer = std::make_unique( - var_mgr_, initial_vector_, strategy, spec_.transition_function(), - starting_player_); - return transducer; - } - CUDD::BDD FairReachabilitySynthesizer::load_CNF(const std::string& filename) const{ std::ifstream f(filename.c_str()); CUDD::BDD assumption = var_mgr_->cudd_mgr()->bddOne(); diff --git a/src/synthesis/source/GR1ReachabilitySynthesizer.cpp b/src/synthesis/source/GR1ReachabilitySynthesizer.cpp index 3636b27..e903c3b 100644 --- a/src/synthesis/source/GR1ReachabilitySynthesizer.cpp +++ b/src/synthesis/source/GR1ReachabilitySynthesizer.cpp @@ -8,13 +8,13 @@ namespace Syft { - GR1ReachabilitySynthesizer::GR1ReachabilitySynthesizer(std::shared_ptr var_mgr, GR1 gr1, SymbolicStateDfa env_safety, - SymbolicStateDfa agn_reach, SymbolicStateDfa agn_safety, std::string slugs_dir) + GR1ReachabilitySynthesizer::GR1ReachabilitySynthesizer(const std::shared_ptr& var_mgr, const GR1& gr1, const SymbolicStateDfa& env_safety, + const SymbolicStateDfa& agn_reach, const SymbolicStateDfa& agn_safety, const std::string& slugs_dir, const std::string& benchmark_name) : var_mgr_(var_mgr), gr1_(gr1), env_safety_(env_safety), agn_reach_(agn_reach), - agn_safety_(agn_safety), slugs_dir_{slugs_dir} + agn_safety_(agn_safety), slugs_dir_{slugs_dir}, benchmark_name_{benchmark_name} {} - void GR1ReachabilitySynthesizer::print_variables(const SymbolicStateDfa arena, const std::string& filename) const{ + void GR1ReachabilitySynthesizer::print_variables(const SymbolicStateDfa& arena, const std::string& filename) const{ std::ofstream to_slugs; to_slugs.open(filename); if(to_slugs.is_open()) { @@ -69,7 +69,7 @@ namespace Syft { } - void GR1ReachabilitySynthesizer::print_transitions(const SymbolicStateDfa arena, const std::string& filename) const { + void GR1ReachabilitySynthesizer::print_transitions(const SymbolicStateDfa& arena, const CUDD::BDD& safe_states, const std::string& filename) const { std::ofstream to_slugs; to_slugs.open(filename, std::ios::app); if(to_slugs.is_open()) { @@ -81,13 +81,13 @@ namespace Syft { std::unordered_map rename_map; std::vector output_variable_labels = var_mgr_->output_variable_labels(); - for (std::string output_variable_label : output_variable_labels){ + for (const std::string& output_variable_label : output_variable_labels){ std::string output_variable_new_label = output_variable_label+'\''; rename_map["("+output_variable_label+")"] = "("+output_variable_new_label+")"; } std::vector input_variable_labels = var_mgr_->input_variable_labels(); - for (std::string input_variable_label : input_variable_labels){ + for (const std::string& input_variable_label : input_variable_labels){ std::string input_variable_new_label = input_variable_label+'\''; rename_map["("+input_variable_label+")"] = "("+input_variable_new_label+")"; } @@ -100,9 +100,6 @@ namespace Syft { rename_state_vars_map["(Z" + std::to_string(i)+")"] = "("+state_variable_new_label+")"; } - - - to_slugs<<"[SYS_TRANS]\n"; for (size_t i = 0; i < transition_function.size(); i++){ std::string tran = var_mgr_->bdd_to_string(transition_function[i]); @@ -125,7 +122,7 @@ namespace Syft { to_slugs<bdd_to_string(safe_states_); + std::string safe_states_string = var_mgr_->bdd_to_string(safe_states); to_slugs<cudd_mgr()->bddOne() || justice == var_mgr_->cudd_mgr()->bddZero()) { to_slugs<bdd_to_string(justice))<<"\n"; } @@ -170,7 +167,7 @@ namespace Syft { to_slugs<<"\n\n"; to_slugs<<"[SYS_LIVENESS]\n"; - for (CUDD::BDD justice : gr1_.agn_justices){ + for (const CUDD::BDD& justice : gr1_.agn_justices){ if (justice == var_mgr_->cudd_mgr()->bddOne() || justice == var_mgr_->cudd_mgr()->bddZero()) { to_slugs<bdd_to_string(justice))<<"\n"; } @@ -185,7 +182,7 @@ namespace Syft { } } - const std::string GR1ReachabilitySynthesizer::exec_slugs(const std::string& slugs, const std::string& slugs_input_file, const std::string& slugs_res_file, const std::string& slugs_strategy_file) { + const std::string GR1ReachabilitySynthesizer::exec_slugs(const std::string& slugs, const std::string& slugs_input_file, const std::string& slugs_res_file, const std::string& slugs_strategy_file) const { std::string result; std::string run_slugs = slugs + " --counterStrategy " + slugs_input_file + " > " + slugs_strategy_file + " 2> "+slugs_res_file; @@ -220,7 +217,7 @@ namespace Syft { return result; } - SynthesisResult GR1ReachabilitySynthesizer::run(std::string& benchmark_name) { + SynthesisResult GR1ReachabilitySynthesizer::run() const { Syft::Stopwatch reduction_to_gr1_stopwatch; // stopwatch for reducing to GR1 reduction_to_gr1_stopwatch.start(); std::cout << "* Start reducing to GR1 game...\n"; @@ -235,13 +232,13 @@ namespace Syft { SymbolicStateDfa arena = SymbolicStateDfa::product({env_safety_, reach_safe}); CUDD::BDD arena_initial_state_bdd = agn_reach_.initial_state_bdd() & agn_safety_.initial_state_bdd() & env_safety_.initial_state_bdd(); - safe_states_ = (env_safety_.final_states() & !(reach_safe.final_states())) | arena_initial_state_bdd; + CUDD::BDD safe_states = (env_safety_.final_states() & !(reach_safe.final_states())) | arena_initial_state_bdd; - std::string to_slugs_parser = benchmark_name + ".parser"; + std::string to_slugs_parser = benchmark_name_ + ".parser"; print_variables(arena, to_slugs_parser); print_initial_conditions(arena_initial_state_bdd, to_slugs_parser); - print_transitions(arena, to_slugs_parser); - print_liveness_constraints(arena, to_slugs_parser); + print_transitions(arena, safe_states, to_slugs_parser); + print_liveness_constraints(to_slugs_parser); auto reduction_to_gr1_time = reduction_to_gr1_stopwatch.stop(); std::cout << "* Finish reducing to GR1 game, took time: " @@ -251,7 +248,7 @@ namespace Syft { gr1_game_stopwatch.start(); std::cout << "* Start calling GR1 game solver Slugs...\n"; - std::string slugs_input_file = benchmark_name+".slugsin"; + std::string slugs_input_file = benchmark_name_+".slugsin"; std::string slugs_parser = slugs_dir_ + "/tools/StructuredSlugsParser/compiler.py"; std::string run_slugs_parser = "python3 "+ slugs_parser + " " + to_slugs_parser + " > " + slugs_input_file; @@ -262,8 +259,8 @@ namespace Syft { system(detele_to_slugs_parser.c_str()); std::string slugs= get_slugs_path(); - std::string slugs_strategy_file= benchmark_name+".strategy"; - std::string slugs_res_file= benchmark_name+".res"; + std::string slugs_strategy_file= benchmark_name_+".strategy"; + std::string slugs_res_file= benchmark_name_+".res"; std::string slugs_result = exec_slugs(slugs, slugs_input_file, slugs_res_file, slugs_strategy_file); std::string detele_slugs_input_file = "rm "+slugs_input_file; @@ -279,13 +276,13 @@ namespace Syft { } else{ result.realizability = true; + result.safe_states = safe_states; } return result; } - std::string GR1ReachabilitySynthesizer::get_slugs_path() { + std::string GR1ReachabilitySynthesizer::get_slugs_path() const { return slugs_dir_ + "/src/slugs"; } - } diff --git a/src/synthesis/source/ReachabilityMaxSetSynthesizer.cpp b/src/synthesis/source/ReachabilityMaxSetSynthesizer.cpp index b422b6c..110588b 100644 --- a/src/synthesis/source/ReachabilityMaxSetSynthesizer.cpp +++ b/src/synthesis/source/ReachabilityMaxSetSynthesizer.cpp @@ -60,7 +60,7 @@ namespace Syft { } - MaxSet ReachabilityMaxSetSynthesizer::AbstractMaxSet(SynthesisResult result) const { + MaxSet ReachabilityMaxSetSynthesizer::AbstractMaxSet(const SynthesisResult& result) const { MaxSet maxset; maxset.nondeferring_strategy = result.winning_moves; maxset.deferring_strategy = result.winning_moves | (result.winning_states & preimage(result.winning_states)); diff --git a/src/synthesis/source/ReachabilitySynthesizer.cpp b/src/synthesis/source/ReachabilitySynthesizer.cpp index adb93b8..b75c08a 100644 --- a/src/synthesis/source/ReachabilitySynthesizer.cpp +++ b/src/synthesis/source/ReachabilitySynthesizer.cpp @@ -56,16 +56,4 @@ namespace Syft { } - std::unique_ptr ReachabilitySynthesizer::AbstractSingleStrategy(SynthesisResult result) const { - std::unordered_map strategy = synthesize_strategy( - result.winning_moves); - - auto transducer = std::make_unique( - var_mgr_, initial_vector_, strategy, spec_.transition_function(), - starting_player_); - return transducer; - } - - - } diff --git a/src/synthesis/source/StableReachabilitySynthesizer.cpp b/src/synthesis/source/StableReachabilitySynthesizer.cpp index 01ff5ea..b9d62f9 100644 --- a/src/synthesis/source/StableReachabilitySynthesizer.cpp +++ b/src/synthesis/source/StableReachabilitySynthesizer.cpp @@ -111,16 +111,6 @@ namespace Syft { } - std::unique_ptr StableReachabilitySynthesizer::AbstractSingleStrategy(SynthesisResult result) const { - std::unordered_map strategy = synthesize_strategy( - result.winning_moves); - - auto transducer = std::make_unique( - var_mgr_, initial_vector_, strategy, spec_.transition_function(), - starting_player_); - return transducer; - } - CUDD::BDD StableReachabilitySynthesizer::load_CNF(const std::string& filename) const{ std::ifstream f(filename.c_str()); CUDD::BDD assumption = var_mgr_->cudd_mgr()->bddOne(); diff --git a/src/synthesis/source/Transducer.cpp b/src/synthesis/source/Transducer.cpp index 5e2a387..47705be 100644 --- a/src/synthesis/source/Transducer.cpp +++ b/src/synthesis/source/Transducer.cpp @@ -4,18 +4,18 @@ namespace Syft { -Transducer::Transducer(std::shared_ptr var_mgr, - std::vector initial_vector, - std::unordered_map output_function, - std::vector transition_function, +Transducer::Transducer(const std::shared_ptr& var_mgr, + const std::vector& initial_vector, + const std::unordered_map& output_function, + const std::vector& transition_function, Player starting_player, Player protagonist_player) - : var_mgr_(std::move(var_mgr)) - , initial_vector_(std::move(initial_vector)) - , output_function_(std::move(output_function)) - , transition_function_(std::move(transition_function)) - , starting_player_(starting_player) - , protagonist_player_(protagonist_player) + : var_mgr_(var_mgr), + initial_vector_(initial_vector), + output_function_(output_function), + transition_function_(transition_function), + starting_player_(starting_player), + protagonist_player_(protagonist_player) {} void Transducer::dump_dot(const std::string& filename) const { diff --git a/test/test_gr1reachability_synthesis.cpp b/test/test_gr1reachability_synthesis.cpp index b331f9c..0e6d819 100644 --- a/test/test_gr1reachability_synthesis.cpp +++ b/test/test_gr1reachability_synthesis.cpp @@ -1,9 +1,6 @@ // // Created by shuzhu on 21/01/24. // -// -// Created by shuzhu on 21/01/24. -// #include "catch2/catch_test_macros.hpp" #include "catch2/generators/catch_generators_all.hpp" @@ -97,11 +94,11 @@ TEST_CASE("GR1 Synthesis test", "[gr1 synthesis]") { + std::string benchmark_name = "hand_shake"; Syft::GR1ReachabilitySynthesizer synthesizer(var_mgr, gr1, symbolic_dfa_env_safety, - symbolic_dfa_agn_goal, symbolic_dfa_agn_safety, Syft::Test::SLUGS_DIR_LOCATION); + symbolic_dfa_agn_goal, symbolic_dfa_agn_safety, Syft::Test::SLUGS_DIR_LOCATION, benchmark_name); - std::string benchmark_name = "hand_shake"; - Syft::SynthesisResult result = synthesizer.run(benchmark_name); + Syft::SynthesisResult result = synthesizer.run(); bool expected = true; REQUIRE(result.realizability == expected); @@ -189,12 +186,11 @@ TEST_CASE("GR1 Synthesis finding_nemo", "[gr1 synthesis]") { - Syft::GR1ReachabilitySynthesizer synthesizer(var_mgr, gr1, symbolic_dfa_env_safety, - symbolic_dfa_agn_goal, symbolic_dfa_agn_safety, Syft::Test::SLUGS_DIR_LOCATION); - std::string benchmark_name = "finding_nemo"; + Syft::GR1ReachabilitySynthesizer synthesizer(var_mgr, gr1, symbolic_dfa_env_safety, + symbolic_dfa_agn_goal, symbolic_dfa_agn_safety, Syft::Test::SLUGS_DIR_LOCATION, benchmark_name); - Syft::SynthesisResult result = synthesizer.run(benchmark_name); + Syft::SynthesisResult result = synthesizer.run(); bool expected = true; REQUIRE(result.realizability == expected);