From 22a91728e57eb3d5830e63eb1739b39502bd0890 Mon Sep 17 00:00:00 2001 From: Shufang-Zhu Date: Sun, 21 Jan 2024 17:50:33 +0000 Subject: [PATCH] stability synthesizer, passed tests --- ...est.tlsf => fair_stable_counter_test.tlsf} | 0 ...sf => fair_stable_counter_unrea_test.tlsf} | 2 +- .../{fair_test.tlsf => fair_stable_test.tlsf} | 0 ...on.txt => fair_stable_test_assumption.txt} | 0 ..._test.tlsf => fair_stable_unrea_test.tlsf} | 0 .../header/StableReachabilitySynthesizer.h | 59 +++++++ .../source/StableReachabilitySynthesizer.cpp | 160 ++++++++++++++++++ test/test_fair_synthesis.cpp | 16 +- test/test_stable_synthesis.cpp | 106 ++++++++++++ test/utils.hpp | 10 +- 10 files changed, 339 insertions(+), 14 deletions(-) rename example/{fair_counter_test.tlsf => fair_stable_counter_test.tlsf} (100%) rename example/{fair_counter_unrea_test.tlsf => fair_stable_counter_unrea_test.tlsf} (98%) rename example/{fair_test.tlsf => fair_stable_test.tlsf} (100%) rename example/{fair_test_assumption.txt => fair_stable_test_assumption.txt} (100%) rename example/{fair_unrea_test.tlsf => fair_stable_unrea_test.tlsf} (100%) create mode 100644 src/synthesis/header/StableReachabilitySynthesizer.h create mode 100644 src/synthesis/source/StableReachabilitySynthesizer.cpp create mode 100644 test/test_stable_synthesis.cpp diff --git a/example/fair_counter_test.tlsf b/example/fair_stable_counter_test.tlsf similarity index 100% rename from example/fair_counter_test.tlsf rename to example/fair_stable_counter_test.tlsf diff --git a/example/fair_counter_unrea_test.tlsf b/example/fair_stable_counter_unrea_test.tlsf similarity index 98% rename from example/fair_counter_unrea_test.tlsf rename to example/fair_stable_counter_unrea_test.tlsf index 9e8532b..d8c861a 100644 --- a/example/fair_counter_unrea_test.tlsf +++ b/example/fair_stable_counter_unrea_test.tlsf @@ -2,7 +2,7 @@ INFO { TITLE: "Fair-LTLf-test" DESCRIPTION: "Fair-LTLf-test example" SEMANTICS: Finite,Moore - TARGET: Moore + TARGET: Mealy } MAIN { diff --git a/example/fair_test.tlsf b/example/fair_stable_test.tlsf similarity index 100% rename from example/fair_test.tlsf rename to example/fair_stable_test.tlsf diff --git a/example/fair_test_assumption.txt b/example/fair_stable_test_assumption.txt similarity index 100% rename from example/fair_test_assumption.txt rename to example/fair_stable_test_assumption.txt diff --git a/example/fair_unrea_test.tlsf b/example/fair_stable_unrea_test.tlsf similarity index 100% rename from example/fair_unrea_test.tlsf rename to example/fair_stable_unrea_test.tlsf diff --git a/src/synthesis/header/StableReachabilitySynthesizer.h b/src/synthesis/header/StableReachabilitySynthesizer.h new file mode 100644 index 0000000..9f79d1b --- /dev/null +++ b/src/synthesis/header/StableReachabilitySynthesizer.h @@ -0,0 +1,59 @@ +// +// Created by shuzhu on 21/01/24. +// + +#ifndef LYDIASYFT_STABLEREACHABILITYSYNTHESIZER_H +#define LYDIASYFT_STABLEREACHABILITYSYNTHESIZER_H + +#include "DfaGameSynthesizer.h" + +namespace Syft { + +/** + * \brief A single-strategy-synthesizer for a Buchi-reachability game given as a symbolic-state DFA. + */ + class StableReachabilitySynthesizer : public DfaGameSynthesizer { + private: + + CUDD::BDD goal_states_; + CUDD::BDD state_space_; + + + //fair + CUDD::BDD assumption_; + + protected: + CUDD::BDD load_CNF(const std::string& filename) const; + + public: + + /** + * \brief Construct a single-strategy-synthesizer for the given Buchi-reachability game. + * + * \param spec A symbolic-state DFA representing the Buchi-reachability game. + * \param starting_player The player that moves first each turn. + * \param goal_states The set of states that the agent must reach to win. + */ + StableReachabilitySynthesizer(SymbolicStateDfa spec, Player starting_player, Player protagonist_player, + CUDD::BDD goal_states, CUDD::BDD state_space, + std::string& assumption_filename); + + + + /** + * \brief Solves the coBuchi-reachability game. + * + * \return The result consists of + * realizability + * a set of agent winning states + * a transducer representing a winning strategy or nullptr if the game is unrealizable. + */ + virtual SynthesisResult run() const final; + + std::unique_ptr AbstractSingleStrategy(SynthesisResult result) const; + + }; + +} + +#endif //LYDIASYFT_STABLEREACHABILITYSYNTHESIZER_H diff --git a/src/synthesis/source/StableReachabilitySynthesizer.cpp b/src/synthesis/source/StableReachabilitySynthesizer.cpp new file mode 100644 index 0000000..01ff5ea --- /dev/null +++ b/src/synthesis/source/StableReachabilitySynthesizer.cpp @@ -0,0 +1,160 @@ +// +// Created by shuzhu on 21/01/24. +// + + +#include "StableReachabilitySynthesizer.h" +#include "string_utilities.h" + +#include +#include + +namespace Syft { + + StableReachabilitySynthesizer::StableReachabilitySynthesizer(SymbolicStateDfa spec, + Player starting_player, Player protagonist_player, + CUDD::BDD goal_states, + CUDD::BDD state_space, + std::string& assumption_filename) + : DfaGameSynthesizer(spec, starting_player, protagonist_player) + , goal_states_(goal_states), state_space_(state_space) + { + assumption_ = load_CNF(assumption_filename); + } + + + SynthesisResult StableReachabilitySynthesizer::run() const { + SynthesisResult result; + CUDD::BDD winning_states = state_space_; + CUDD::BDD winning_moves = winning_states; + int c = 0; + int inner_c = 0; + + while (true) { +// var_mgr_->dump_dot(winning_states.Add(), "winning_states_"+ std::to_string(c)+".dot"); +// var_mgr_->dump_dot(winning_moves.Add(), "winning_moves_"+ std::to_string(c)+".dot"); + CUDD::BDD new_winning_states, new_winning_moves; + // inner least fixpoint + CUDD::BDD inner_winning_states = state_space_ & goal_states_; + CUDD::BDD inner_winning_moves = inner_winning_states; + + while (true) { +// var_mgr_->dump_dot(inner_winning_states.Add(), "inner_winning_states_"+ std::to_string(c)+".dot"); +// var_mgr_->dump_dot(inner_winning_moves.Add(), "inner_winning_moves_"+ std::to_string(c)+".dot"); + CUDD::BDD new_inner_winning_states, new_inner_winning_moves; + + CUDD::BDD transitions_to_winning_states_or_goal = + (winning_states | goal_states_).VectorCompose(transition_vector_); +// var_mgr_->dump_dot(transitions_to_winning_states_or_goal.Add(), "transitions_to_winning_states_or_goal.dot"); + CUDD::BDD transitions_to_inner_winning_states_or_goal = + (inner_winning_states | goal_states_).VectorCompose(transition_vector_); +// var_mgr_->dump_dot(transitions_to_inner_winning_states_or_goal.Add(), "transitions_to_inner_winning_states_or_goal.dot"); +// var_mgr_->dump_dot(assumption_.Add(), "assumption.dot"); + CUDD::BDD assumption_constrained_transitions = ((!assumption_ | transitions_to_inner_winning_states_or_goal)) * transitions_to_winning_states_or_goal; +// var_mgr_->dump_dot(assumption_constrained_transitions.Add(), "assumption_constrained_transitions.dot"); + if (starting_player_ == Player::Agent) { + // Quantify all variables that the outputs don't depend on + CUDD::BDD quantified_X_transitions_to_inner_winning_states = quantify_independent_variables_->apply(assumption_constrained_transitions); + new_inner_winning_moves = inner_winning_moves | quantified_X_transitions_to_inner_winning_states; + + new_inner_winning_states = project_into_states(new_inner_winning_moves); + } else { + CUDD::BDD transitions_to_inner_winning_states = quantify_independent_variables_->apply(assumption_constrained_transitions); +// var_mgr_->dump_dot((quantify_independent_variables_->apply(assumption_constrained_transitions)).Add(), "quantified_assumption_constrained_transitions.dot"); + CUDD::BDD new_collected_inner_winning_states = project_into_states(transitions_to_inner_winning_states); + new_inner_winning_states = inner_winning_states | new_collected_inner_winning_states; +// var_mgr_->dump_dot(new_inner_winning_states.Add(), "states.dot"); + new_inner_winning_moves = inner_winning_moves | ((!inner_winning_states) & new_collected_inner_winning_states & transitions_to_inner_winning_states); + + } + + if (new_inner_winning_states == inner_winning_states) { + if (starting_player_ == Player::Agent) { +// CUDD::BDD transitions_to_winning_states = preimage(inner_winning_states); +// CUDD::BDD quantified_X_transitions_to_inner_winning_states = quantify_independent_variables_->apply(transitions_to_winning_states); +// new_inner_winning_moves = inner_winning_moves & quantified_X_transitions_to_inner_winning_states; + new_winning_moves = winning_moves & inner_winning_moves; + new_winning_states = winning_states & inner_winning_states; + } else { + CUDD::BDD transitions_to_winning_states = preimage(inner_winning_states); + new_winning_states = winning_states & inner_winning_states; + new_winning_moves = winning_moves & transitions_to_winning_states; + } + break; + } + + inner_winning_moves = new_inner_winning_moves; + inner_winning_states = new_inner_winning_states; + inner_c++; + } + + + if (includes_initial_state(new_winning_states)) { + result.realizability = true; + result.winning_states = new_winning_states; + result.winning_moves = new_winning_moves; + result.transducer = nullptr; + return result; + + } else if (new_winning_states == winning_states) { + result.realizability = false; + result.winning_states = new_winning_states; + result.winning_moves = new_winning_moves; + result.transducer = nullptr; + return result; + } + + winning_moves = new_winning_moves; + winning_states = new_winning_states; + c++; + } + + } + + 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(); + std::vector clause_line; + std::string line; + while(getline(f, line)) { + CUDD::BDD clause = var_mgr_->cudd_mgr()->bddZero(); + std::set clause_set; + std::set neg_clause_set; + + if (f.is_open()) { + clause_line = split(line, " "); + + for (int i = 0; i < clause_line.size(); i++){ + std::string c = clause_line[i]; + CUDD::BDD literal_bdd; + if(c[0] == '!'){ + std::string var_name = c.substr(1, c.length()-1); + literal_bdd = !(var_mgr_->name_to_variable(var_name)); + } + else{ + literal_bdd = var_mgr_->name_to_variable(c); + } + clause = clause + literal_bdd; + } + } + if(clause != var_mgr_->cudd_mgr()->bddZero()){ + assumption = assumption * clause; + } + + } + f.close(); + return assumption; + + } + +} diff --git a/test/test_fair_synthesis.cpp b/test/test_fair_synthesis.cpp index 1050c95..79ebf2a 100644 --- a/test/test_fair_synthesis.cpp +++ b/test/test_fair_synthesis.cpp @@ -14,7 +14,7 @@ TEST_CASE("Fair Synthesis test", "[fair synthesis]") { Syft::Parser parser; - parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSYNTHESIS_TEST_TLSF); + parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSTABLESYNTHESIS_TEST_TLSF); bool sys_first = parser.get_sys_first(); @@ -52,7 +52,7 @@ TEST_CASE("Fair Synthesis test", "[fair synthesis]") { Syft::FairReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player, protagonist_player, symbolic_dfa.final_states(), - var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSYNTHESIS_TEST_ASSUMPTION); + var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSTABLESYNTHESIS_TEST_ASSUMPTION); Syft::SynthesisResult result = synthesizer.run(); bool expected = true; @@ -61,7 +61,7 @@ TEST_CASE("Fair Synthesis test", "[fair synthesis]") { TEST_CASE("Fair Synthesis unrealizability test", "[fair synthesis]") { Syft::Parser parser; - parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSYNTHESIS_UNREA_TEST_TLSF); + parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSTABLESYNTHESIS_UNREA_TEST_TLSF); bool sys_first = parser.get_sys_first(); @@ -99,7 +99,7 @@ TEST_CASE("Fair Synthesis unrealizability test", "[fair synthesis]") { Syft::FairReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player, protagonist_player, symbolic_dfa.final_states(), - var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSYNTHESIS_TEST_ASSUMPTION); + var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSTABLESYNTHESIS_TEST_ASSUMPTION); Syft::SynthesisResult result = synthesizer.run(); bool expected = false; @@ -108,7 +108,7 @@ TEST_CASE("Fair Synthesis unrealizability test", "[fair synthesis]") { TEST_CASE("Fair Synthesis of realizable counter_1", "[fair synthesis]") { Syft::Parser parser; - parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSYNTHESIS_COUNTER_TEST_TLSF); + parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSTABLESYNTHESIS_COUNTER_TEST_TLSF); bool sys_first = parser.get_sys_first(); @@ -144,7 +144,7 @@ TEST_CASE("Fair Synthesis of realizable counter_1", "[fair synthesis]") { Syft::FairReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player, protagonist_player, symbolic_dfa.final_states(), - var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSYNTHESIS_TEST_ASSUMPTION); + var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSTABLESYNTHESIS_TEST_ASSUMPTION); Syft::SynthesisResult result = synthesizer.run(); bool expected = true; @@ -153,7 +153,7 @@ TEST_CASE("Fair Synthesis of realizable counter_1", "[fair synthesis]") { TEST_CASE("Fair Synthesis of unrealizable counter_1", "[fair synthesis]") { Syft::Parser parser; - parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSYNTHESIS_COUNTER_UNREA_TEST_TLSF); + parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSTABLESYNTHESIS_COUNTER_UNREA_TEST_TLSF); bool sys_first = parser.get_sys_first(); @@ -191,7 +191,7 @@ TEST_CASE("Fair Synthesis of unrealizable counter_1", "[fair synthesis]") { Syft::FairReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player, protagonist_player, symbolic_dfa.final_states(), - var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSYNTHESIS_TEST_ASSUMPTION); + var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSTABLESYNTHESIS_TEST_ASSUMPTION); Syft::SynthesisResult result = synthesizer.run(); bool expected = false; diff --git a/test/test_stable_synthesis.cpp b/test/test_stable_synthesis.cpp new file mode 100644 index 0000000..f0d9510 --- /dev/null +++ b/test/test_stable_synthesis.cpp @@ -0,0 +1,106 @@ +// +// Created by shuzhu on 21/01/24. +// +#include "catch2/catch_test_macros.hpp" +#include "catch2/generators/catch_generators_all.hpp" + +#include "ExplicitStateDfaMona.h" +#include "InputOutputPartition.h" +#include "StableReachabilitySynthesizer.h" +#include "Preprocessing.h" +#include "Parser.h" +#include "utils.hpp" +#include + + +TEST_CASE("Stable Synthesis of realizable counter_1", "[stable synthesis]") { + Syft::Parser parser; + parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSTABLESYNTHESIS_COUNTER_TEST_TLSF); + + 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; + + 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}); + + 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)); + + var_mgr->partition_variables(partition.input_variables, + partition.output_variables); + + Syft::StableReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player, + protagonist_player, symbolic_dfa.final_states(), + var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSTABLESYNTHESIS_TEST_ASSUMPTION); + Syft::SynthesisResult result = synthesizer.run(); + + bool expected = true; + REQUIRE(result.realizability == expected); +} + +TEST_CASE("Stable Synthesis of unrealizable counter_1", "[stable synthesis]") { + Syft::Parser parser; + parser = Syft::Parser::read_from_file(Syft::Test::SYFCO_LOCATION, Syft::Test::FAIRSTABLESYNTHESIS_COUNTER_UNREA_TEST_TLSF); + + 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; + + 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}); + + 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); +// explicit_dfa.dump_dot("explicit_dfa.dot"); + + Syft::SymbolicStateDfa symbolic_dfa = Syft::SymbolicStateDfa::from_explicit( + std::move(explicit_dfa)); + +// symbolic_dfa.dump_dot("symbolic_dfa.dot"); + var_mgr->partition_variables(partition.input_variables, + partition.output_variables); + + Syft::StableReachabilitySynthesizer synthesizer(symbolic_dfa, starting_player, + protagonist_player, symbolic_dfa.final_states(), + var_mgr->cudd_mgr()->bddOne(), Syft::Test::FAIRSTABLESYNTHESIS_TEST_ASSUMPTION); + Syft::SynthesisResult result = synthesizer.run(); + + bool expected = false; + REQUIRE(result.realizability == expected); +} diff --git a/test/utils.hpp b/test/utils.hpp index 5443d51..09ce14a 100644 --- a/test/utils.hpp +++ b/test/utils.hpp @@ -19,11 +19,11 @@ namespace Syft::Test { static std::string EXAMPLE_TEST_TLSF = ROOT_DIRECTORY + "/example/test.tlsf"; static std::string EXAMPLE_001_TLSF = ROOT_DIRECTORY + "/example/001.tlsf"; static std::string DATASET_FOLDER = ROOT_DIRECTORY + "/example/TLSF"; - static std::string FAIRSYNTHESIS_COUNTER_TEST_TLSF = ROOT_DIRECTORY + "/example/fair_counter_test.tlsf"; - static std::string FAIRSYNTHESIS_COUNTER_UNREA_TEST_TLSF = ROOT_DIRECTORY + "/example/fair_counter_unrea_test.tlsf"; - static std::string FAIRSYNTHESIS_TEST_TLSF = ROOT_DIRECTORY + "/example/fair_test.tlsf"; - static std::string FAIRSYNTHESIS_UNREA_TEST_TLSF = ROOT_DIRECTORY + "/example/fair_unrea_test.tlsf"; - static std::string FAIRSYNTHESIS_TEST_ASSUMPTION = ROOT_DIRECTORY + "/example/fair_test_assumption.txt"; + static std::string FAIRSTABLESYNTHESIS_COUNTER_TEST_TLSF = ROOT_DIRECTORY + "/example/fair_stable_counter_test.tlsf"; + static std::string FAIRSTABLESYNTHESIS_COUNTER_UNREA_TEST_TLSF = ROOT_DIRECTORY + "/example/fair_stable_counter_unrea_test.tlsf"; + static std::string FAIRSTABLESYNTHESIS_TEST_TLSF = ROOT_DIRECTORY + "/example/fair_stable_test.tlsf"; + static std::string FAIRSTABLESYNTHESIS_UNREA_TEST_TLSF = ROOT_DIRECTORY + "/example/fair_stable_unrea_test.tlsf"; + static std::string FAIRSTABLESYNTHESIS_TEST_ASSUMPTION = ROOT_DIRECTORY + "/example/fair_stable_test_assumption.txt"; inline std::string get_time_str() { // Get current time as a time_point object