From a6abcde920584e35276f2c824d691f7b6abe644b Mon Sep 17 00:00:00 2001 From: Marco Favorito Date: Sun, 28 Jan 2024 00:07:07 +0100 Subject: [PATCH 1/2] docs: make README more markdown-friendly --- README.md | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/README.md b/README.md index 4d23fae..2b192ee 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,7 +100,7 @@ sudo apt install graphviz libgraphviz-dev ``` -==== Run LYDIASYFT ==== +## Run LYDIASYFT 1. Reach executable file LydiaSyft From a2b701e192f1d127b69031d7229171c80b92a334 Mon Sep 17 00:00:00 2001 From: Marco Favorito Date: Sun, 28 Jan 2024 00:45:34 +0100 Subject: [PATCH 2/2] feat: add subcommands to CLI entrypoint This commit improves the CLI by adding several subcommands, one for each synthesis variant: 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 --- README.md | 58 ++++- src/CMakeLists.txt | 4 +- src/Main.cpp | 245 +++++------------- src/cli/base.cpp | 156 +++++++++++ src/cli/base.hpp | 96 +++++++ src/cli/fairness.cpp | 51 ++++ src/cli/fairness.hpp | 32 +++ src/cli/gr1.cpp | 89 +++++++ src/cli/gr1.hpp | 48 ++++ src/cli/maxset.cpp | 59 +++++ src/cli/maxset.hpp | 32 +++ src/cli/stability.cpp | 51 ++++ src/cli/stability.hpp | 30 +++ src/cli/synthesis.cpp | 44 ++++ src/cli/synthesis.hpp | 31 +++ src/synthesis/header/DfaGameSynthesizer.h | 15 +- .../header/FairReachabilitySynthesizer.h | 8 +- src/synthesis/header/GR1.h | 4 +- .../header/GR1ReachabilitySynthesizer.h | 38 +-- .../header/ReachabilityMaxSetSynthesizer.h | 2 +- .../header/ReachabilitySynthesizer.h | 2 - .../header/StableReachabilitySynthesizer.h | 2 - src/synthesis/header/Synthesizer.h | 1 + src/synthesis/header/Transducer.h | 21 +- src/synthesis/source/DfaGameSynthesizer.cpp | 25 +- .../source/FairReachabilitySynthesizer.cpp | 18 +- .../source/GR1ReachabilitySynthesizer.cpp | 47 ++-- .../source/ReachabilityMaxSetSynthesizer.cpp | 2 +- .../source/ReachabilitySynthesizer.cpp | 12 - .../source/StableReachabilitySynthesizer.cpp | 10 - src/synthesis/source/Transducer.cpp | 20 +- test/test_gr1reachability_synthesis.cpp | 16 +- 32 files changed, 953 insertions(+), 316 deletions(-) create mode 100644 src/cli/base.cpp create mode 100644 src/cli/base.hpp create mode 100644 src/cli/fairness.cpp create mode 100644 src/cli/fairness.hpp create mode 100644 src/cli/gr1.cpp create mode 100644 src/cli/gr1.hpp create mode 100644 src/cli/maxset.cpp create mode 100644 src/cli/maxset.hpp create mode 100644 src/cli/stability.cpp create mode 100644 src/cli/stability.hpp create mode 100644 src/cli/synthesis.cpp create mode 100644 src/cli/synthesis.hpp diff --git a/README.md b/README.md index 2b192ee..827b44a 100644 --- a/README.md +++ b/README.md @@ -102,10 +102,60 @@ sudo apt install graphviz libgraphviz-dev ## Run LYDIASYFT -1. Reach executable file 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): + +- Classical synthesis: + +``` +./build/bin/LydiaSyft synthesis -f example/test.tlsf # UNREALIZABLE +./build/bin/LydiaSyft synthesis -f example/test1.tlsf # REALIZABLE +``` + +- Maxset synthesis: - ```cd bin``` +``` +./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 +``` -2. Run example: - ```./Lydiasyft -f ../../example/test.tlsf``` +- 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);