From 64461bd174b373294a7c6d5c9a94a5f60e68ab03 Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Sun, 22 Aug 2021 12:33:57 +0200 Subject: [PATCH 1/2] fix: move dfs strategy in another module --- libs/core/include/cynthia/core.hpp | 79 ++----- libs/core/include/cynthia/sdd_to_formula.hpp | 3 +- libs/core/include/cynthia/strategies/dfs.hpp | 54 +++++ libs/core/include/cynthia/to_sdd.hpp | 8 +- libs/core/src/core.cpp | 216 +++--------------- libs/core/src/sdd_to_formula.cpp | 3 +- libs/core/src/strategies/dfs.cpp | 211 +++++++++++++++++ libs/core/src/to_sdd.cpp | 3 +- .../unit/test_core/test_complex_formulas.cpp | 11 +- .../test_core/test_core_basic_formulas.cpp | 101 ++++---- libs/core/tests/unit/test_to_sdd.cpp | 10 +- 11 files changed, 382 insertions(+), 317 deletions(-) create mode 100644 libs/core/include/cynthia/strategies/dfs.hpp create mode 100644 libs/core/src/strategies/dfs.cpp diff --git a/libs/core/include/cynthia/core.hpp b/libs/core/include/cynthia/core.hpp index 3ebea86..65752a2 100644 --- a/libs/core/include/cynthia/core.hpp +++ b/libs/core/include/cynthia/core.hpp @@ -48,72 +48,29 @@ bool is_realizable(const logic::ltlf_ptr& formula, return synthesis.is_realizable(); } -class ForwardSynthesis : public ISynthesis { +class Context { public: - class Context { - public: - logic::ltlf_ptr formula; - logic::Context* ast_manager; - InputOutputPartition partition; - logic::ltlf_ptr nnf_formula; - logic::ltlf_ptr xnf_formula; - Closure closure_; - Statistics statistics_; - std::map prop_to_id; - std::map discovered; - Vtree* vtree_ = nullptr; - SddManager* manager = nullptr; - utils::Logger logger; - size_t indentation = 0; - Context(const logic::ltlf_ptr& formula, - const InputOutputPartition& partition); - ~Context() { - if (vtree_) { - sdd_vtree_free(vtree_); - } - if (manager) { - sdd_manager_free(manager); - } - } - - logic::ltlf_ptr get_formula(size_t index) const { - if (index < closure_.nb_formulas()) { - return closure_.get_formula(index); - } - index -= closure_.nb_formulas(); - if (index < partition.input_variables.size()) { - return ast_manager->make_atom(partition.input_variables[index]); - } - index -= partition.input_variables.size(); - return ast_manager->make_atom(partition.output_variables[index]); - } - }; - ForwardSynthesis(const logic::ltlf_ptr& formula, - const InputOutputPartition& partition) - : context_{formula, partition}, ISynthesis(formula, partition){}; + logic::ltlf_ptr formula; + logic::Context* ast_manager; + InputOutputPartition partition; + logic::ltlf_ptr nnf_formula; + logic::ltlf_ptr xnf_formula; + Closure closure_; + Statistics statistics_; + std::map prop_to_id; + std::map discovered; + Vtree* vtree_ = nullptr; + SddManager* manager = nullptr; + utils::Logger logger; + size_t indentation = 0; + Context(const logic::ltlf_ptr& formula, + const InputOutputPartition& partition); + ~Context(); + logic::ltlf_ptr get_formula(size_t index) const; static std::map compute_prop_to_id_map(const Closure& closure, const InputOutputPartition& partition); - bool is_realizable() override; - - bool forward_synthesis_(); - -private: - Context context_; - template - inline void print_search_debug(const char* fmt, const Arg1& arg1, - const Args&... args) { - context_.logger.debug( - (std::string(context_.indentation, '\t') + fmt).c_str(), arg1, args...); - }; - inline void print_search_debug(const char* fmt) { - context_.logger.debug( - (std::string(context_.indentation, '\t') + fmt).c_str()); - }; - strategy_t system_move_(const logic::ltlf_ptr& formula, - std::set& path); - strategy_t env_move_(SddNodeWrapper& wrapper, std::set& path); }; } // namespace core diff --git a/libs/core/include/cynthia/sdd_to_formula.hpp b/libs/core/include/cynthia/sdd_to_formula.hpp index c5c6391..f477644 100644 --- a/libs/core/include/cynthia/sdd_to_formula.hpp +++ b/libs/core/include/cynthia/sdd_to_formula.hpp @@ -21,8 +21,7 @@ namespace cynthia { namespace core { -logic::ltlf_ptr sdd_to_formula(SddNode* sdd_node, - ForwardSynthesis::Context& context_); +logic::ltlf_ptr sdd_to_formula(SddNode* sdd_node, Context& context_); } // namespace core } // namespace cynthia diff --git a/libs/core/include/cynthia/strategies/dfs.hpp b/libs/core/include/cynthia/strategies/dfs.hpp new file mode 100644 index 0000000..05d409e --- /dev/null +++ b/libs/core/include/cynthia/strategies/dfs.hpp @@ -0,0 +1,54 @@ +#pragma once +/* + * This file is part of Cynthia. + * + * Cynthia is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Cynthia is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Cynthia. If not, see . + */ + +namespace cynthia { +namespace core { + +class ForwardDfsSynthesis : public ISynthesis { +public: + ForwardDfsSynthesis(const logic::ltlf_ptr& formula, + const InputOutputPartition& partition) + : context_{formula, partition}, ISynthesis(formula, partition){}; + + bool is_realizable() override; + + bool forward_synthesis_(); + +private: + Context context_; + + template + inline void print_search_debug(const char* fmt, const Arg1& arg1, + const Args&... args) { + context_.logger.debug( + (std::string(context_.indentation, '\t') + fmt).c_str(), arg1, args...); + }; + + inline void print_search_debug(const char* fmt) { + context_.logger.debug( + (std::string(context_.indentation, '\t') + fmt).c_str()); + }; + + strategy_t system_move_(const logic::ltlf_ptr& formula, + std::set& path); + + strategy_t env_move_(SddNodeWrapper& wrapper, std::set& path); +}; + +} // namespace core +} // namespace cynthia \ No newline at end of file diff --git a/libs/core/include/cynthia/to_sdd.hpp b/libs/core/include/cynthia/to_sdd.hpp index aa005d5..0d0432d 100644 --- a/libs/core/include/cynthia/to_sdd.hpp +++ b/libs/core/include/cynthia/to_sdd.hpp @@ -24,12 +24,11 @@ namespace core { class ToSddVisitor : public logic::Visitor { private: - ForwardSynthesis::Context& context_; + Context& context_; SddNode* result{}; public: - explicit ToSddVisitor(ForwardSynthesis::Context& context) - : context_{context} {} + explicit ToSddVisitor(Context& context) : context_{context} {} void visit(const logic::LTLfTrue&) override; void visit(const logic::LTLfFalse&) override; void visit(const logic::LTLfPropTrue&) override; @@ -57,8 +56,7 @@ class ToSddVisitor : public logic::Visitor { } }; -SddNode* to_sdd(const logic::LTLfFormula& formula, - ForwardSynthesis::Context& context); +SddNode* to_sdd(const logic::LTLfFormula& formula, Context& context); // returns an SDD node representing ( node1 => node2 ) SddNode* sdd_imply(SddNode* node1, SddNode* node2, SddManager* manager); diff --git a/libs/core/src/core.cpp b/libs/core/src/core.cpp index 113fae6..f89cc3a 100644 --- a/libs/core/src/core.cpp +++ b/libs/core/src/core.cpp @@ -33,24 +33,25 @@ ISynthesis::ISynthesis(const logic::ltlf_ptr& formula, const InputOutputPartition& partition) : formula{formula}, partition{partition} {} -bool ForwardSynthesis::is_realizable() { - bool result = forward_synthesis_(); - return result; -} - -bool ForwardSynthesis::forward_synthesis_() { - auto path = std::set{}; - auto root_sdd_node = to_sdd(*context_.xnf_formula, context_); - auto sdd_formula_id = sdd_id(root_sdd_node); - auto strategy = system_move_(context_.xnf_formula, path); - bool result = strategy[sdd_formula_id] != sdd_manager_false(context_.manager); - context_.logger.info("Explored states: {}", - context_.statistics_.nb_visited_nodes()); - return result; +Context::Context(const logic::ltlf_ptr& formula, + const InputOutputPartition& partition) + : logger{"cynthia"}, formula{formula}, partition{partition}, + ast_manager{&formula->ctx()} { + nnf_formula = logic::to_nnf(*formula); + auto formula_str = logic::to_string(*nnf_formula); + xnf_formula = xnf(*nnf_formula); + Closure closure_object = closure(*xnf_formula); + closure_ = closure_object; + auto builder = VTreeBuilder(closure_, partition); + vtree_ = builder.get_vtree(); + manager = sdd_manager_new(vtree_); + prop_to_id = compute_prop_to_id_map(closure_, partition); + statistics_ = Statistics(); } -std::map ForwardSynthesis::compute_prop_to_id_map( - const Closure& closure, const InputOutputPartition& partition) { +std::map +Context::compute_prop_to_id_map(const Closure& closure, + const InputOutputPartition& partition) { std::map result; size_t offset = closure.nb_formulas(); size_t i = offset; @@ -63,181 +64,26 @@ std::map ForwardSynthesis::compute_prop_to_id_map( return result; } -strategy_t ForwardSynthesis::system_move_(const logic::ltlf_ptr& formula, - std::set& path) { - strategy_t success_strategy, failure_strategy; - context_.indentation += 1; - auto formula_str = logic::to_string(*formula); - auto sdd = SddNodeWrapper(to_sdd(*formula, context_)); - auto sdd_formula_id = sdd_id(sdd.get_raw()); - context_.statistics_.visit_node(sdd_formula_id); - success_strategy[sdd_formula_id] = sdd_manager_true(context_.manager); - failure_strategy[sdd_formula_id] = sdd_manager_false(context_.manager); - this->print_search_debug("State {}", sdd_formula_id); - if (eval(*formula)) { - this->print_search_debug("{} accepting!", sdd_formula_id); - context_.discovered[sdd_formula_id] = true; - context_.indentation -= 1; - return success_strategy; - } - - if (context_.discovered.find(sdd_formula_id) != context_.discovered.end()) { - context_.indentation -= 1; - bool is_success = context_.discovered[sdd_formula_id]; - if (is_success) { - this->print_search_debug("{} already discovered, success", - sdd_formula_id); - return success_strategy; - } else { - this->print_search_debug("{} already discovered, failure", - sdd_formula_id); - return failure_strategy; - } - } else if (path.find(sdd_formula_id) != path.end()) { - this->print_search_debug("Already visited state {}, failure", - sdd_formula_id); - context_.discovered[sdd_formula_id] = false; - context_.indentation -= 1; - return failure_strategy; +logic::ltlf_ptr Context::get_formula(size_t index) const { + if (index < closure_.nb_formulas()) { + return closure_.get_formula(index); } - - path.insert(sdd_formula_id); - if (!sdd.is_decision()) { - auto system_move_str = - logic::to_string(*sdd_to_formula(sdd.get_raw(), context_)); - this->print_search_debug("system move (unique): {}", system_move_str); - auto new_strategy = env_move_(sdd, path); - if (!new_strategy.empty()) { - path.erase(sdd_formula_id); - context_.discovered[sdd_formula_id] = true; - context_.indentation -= 1; - return success_strategy; - } - } else if (sdd.get_raw()->vtree->parent != NULL) { - // not at the vtree root; it means that system choice is irrelevant - this->print_search_debug("system choice is irrelevant"); - auto env_state_node = sdd; - auto new_strategy = env_move_(env_state_node, path); - if (!new_strategy.empty()) { - this->print_search_debug("Any system move is a success from state {}!", - sdd_formula_id); - path.erase(sdd_formula_id); - // all system moves are OK, since it does not have control - context_.discovered[sdd_formula_id] = true; - context_.indentation -= 1; - return success_strategy; - } - } else { - // is a decision node - auto child_it = sdd.begin(); - auto children_end = sdd.end(); - - if (child_it == children_end) { - path.erase(sdd_formula_id); - context_.discovered[sdd_formula_id] = false; - context_.indentation -= 1; - return failure_strategy; - } - - while (child_it != children_end) { - auto system_move = child_it.get_prime(); - auto system_move_str = - logic::to_string(*sdd_to_formula(system_move, context_)); - this->print_search_debug("checking system move: {}", system_move_str); - auto env_state_node = SddNodeWrapper(child_it.get_sub()); - ++child_it; - if (sdd_node_is_false(system_move)) - continue; - auto new_strategy = env_move_(env_state_node, path); - if (!new_strategy.empty()) { - this->print_search_debug("System move {} from state {} is successful", - sdd_formula_id, system_move_str); - path.erase(sdd_formula_id); - new_strategy[sdd_formula_id] = system_move; - context_.discovered[sdd_formula_id] = true; - context_.indentation -= 1; - return new_strategy; - } - } + index -= closure_.nb_formulas(); + if (index < partition.input_variables.size()) { + return ast_manager->make_atom(partition.input_variables[index]); } - - this->print_search_debug("State {} is failure", sdd_formula_id); - path.erase(sdd_formula_id); - context_.discovered[sdd_formula_id] = false; - context_.indentation -= 1; - return failure_strategy; + index -= partition.input_variables.size(); + return ast_manager->make_atom(partition.output_variables[index]); } -strategy_t ForwardSynthesis::env_move_(SddNodeWrapper& wrapper, - std::set& path) { - logic::ltlf_ptr next_state, sdd_formula; - context_.indentation += 1; - if (!wrapper.is_decision()) { - sdd_formula = sdd_to_formula(wrapper.get_raw(), context_); - auto sdd_formula_str = logic::to_string(*sdd_formula); - next_state = xnf(*strip_next(*sdd_formula)); - auto next_state_str = logic::to_string(*next_state); - auto sdd_next_state = SddNodeWrapper(to_sdd(*next_state, context_)); - auto sdd_next_state_id = sdd_id(sdd_next_state.get_raw()); - this->print_search_debug("env move forced to next state {}", - sdd_next_state_id); - auto strategy = system_move_(next_state, path); - context_.indentation -= 1; - if (strategy[sdd_next_state_id] == sdd_manager_false(context_.manager)) - return strategy_t{}; - return strategy; - } else if (wrapper.get_raw()->vtree->parent->parent != NULL) { - // parent is not the vtree root; it means that environment choice is - // irrelevant - this->print_search_debug("env choice is irrelevant"); - sdd_formula = sdd_to_formula(wrapper.get_raw(), context_); - next_state = xnf(*strip_next(*sdd_formula)); - auto sdd_next_state = SddNodeWrapper(to_sdd(*next_state, context_)); - auto sdd_next_state_id = sdd_id(sdd_next_state.get_raw()); - auto strategy = system_move_(next_state, path); - context_.indentation -= 1; - if (strategy[sdd_next_state_id] == sdd_manager_false(context_.manager)) - return strategy_t{}; - return strategy; - } else { - auto child_it = wrapper.begin(); - auto children_end = wrapper.end(); - strategy_t final_strategy; - for (; child_it != children_end; ++child_it) { - auto env_action = sdd_to_formula(child_it.get_prime(), context_); - auto env_action_str = logic::to_string(*env_action); - sdd_formula = sdd_to_formula(child_it.get_sub(), context_); - next_state = xnf(*strip_next(*sdd_formula)); - auto next_state_str = logic::to_string(*next_state); - auto sdd_next_state = SddNodeWrapper(to_sdd(*next_state, context_)); - auto sdd_next_state_id = sdd_id(sdd_next_state.get_raw()); - this->print_search_debug("env move: {}", env_action_str); - auto strategy = system_move_(next_state, path); - if (strategy[sdd_next_state_id] == sdd_manager_false(context_.manager)) { - context_.indentation -= 1; - return strategy_t{}; - } - final_strategy.insert(strategy.begin(), strategy.end()); - } - context_.indentation -= 1; - return final_strategy; +Context::~Context() { + if (vtree_) { + sdd_vtree_free(vtree_); + } + if (manager) { + sdd_manager_free(manager); } } -ForwardSynthesis::Context::Context(const logic::ltlf_ptr& formula, - const InputOutputPartition& partition) - : logger{"cynthia"}, formula{formula}, partition{partition}, - ast_manager{&formula->ctx()} { - nnf_formula = logic::to_nnf(*formula); - auto formula_str = logic::to_string(*nnf_formula); - xnf_formula = xnf(*nnf_formula); - Closure closure_object = closure(*xnf_formula); - closure_ = closure_object; - auto builder = VTreeBuilder(closure_, partition); - vtree_ = builder.get_vtree(); - manager = sdd_manager_new(vtree_); - prop_to_id = compute_prop_to_id_map(closure_, partition); - statistics_ = Statistics(); -} } // namespace core } // namespace cynthia diff --git a/libs/core/src/sdd_to_formula.cpp b/libs/core/src/sdd_to_formula.cpp index 40098b2..cbf0cdc 100644 --- a/libs/core/src/sdd_to_formula.cpp +++ b/libs/core/src/sdd_to_formula.cpp @@ -21,8 +21,7 @@ namespace cynthia { namespace core { -logic::ltlf_ptr sdd_to_formula(SddNode* sdd_node, - ForwardSynthesis::Context& context_) { +logic::ltlf_ptr sdd_to_formula(SddNode* sdd_node, Context& context_) { if (sdd_node_is_false(sdd_node)) { return context_.ast_manager->make_ff(); } diff --git a/libs/core/src/strategies/dfs.cpp b/libs/core/src/strategies/dfs.cpp new file mode 100644 index 0000000..2068fd8 --- /dev/null +++ b/libs/core/src/strategies/dfs.cpp @@ -0,0 +1,211 @@ +/* + * This file is part of Cynthia. + * + * Cynthia is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Cynthia is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Cynthia. If not, see . + */ + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace cynthia { +namespace core { + +bool ForwardDfsSynthesis::is_realizable() { + bool result = forward_synthesis_(); + return result; +} + +bool ForwardDfsSynthesis::forward_synthesis_() { + auto path = std::set{}; + auto root_sdd_node = to_sdd(*context_.xnf_formula, context_); + auto sdd_formula_id = sdd_id(root_sdd_node); + auto strategy = system_move_(context_.xnf_formula, path); + bool result = strategy[sdd_formula_id] != sdd_manager_false(context_.manager); + context_.logger.info("Explored states: {}", + context_.statistics_.nb_visited_nodes()); + return result; +} + +strategy_t ForwardDfsSynthesis::system_move_(const logic::ltlf_ptr& formula, + std::set& path) { + strategy_t success_strategy, failure_strategy; + context_.indentation += 1; + auto formula_str = logic::to_string(*formula); + auto sdd = SddNodeWrapper(to_sdd(*formula, context_)); + auto sdd_formula_id = sdd_id(sdd.get_raw()); + context_.statistics_.visit_node(sdd_formula_id); + success_strategy[sdd_formula_id] = sdd_manager_true(context_.manager); + failure_strategy[sdd_formula_id] = sdd_manager_false(context_.manager); + this->print_search_debug("State {}", sdd_formula_id); + if (eval(*formula)) { + this->print_search_debug("{} accepting!", sdd_formula_id); + context_.discovered[sdd_formula_id] = true; + context_.indentation -= 1; + return success_strategy; + } + + if (context_.discovered.find(sdd_formula_id) != context_.discovered.end()) { + context_.indentation -= 1; + bool is_success = context_.discovered[sdd_formula_id]; + if (is_success) { + this->print_search_debug("{} already discovered, success", + sdd_formula_id); + return success_strategy; + } else { + this->print_search_debug("{} already discovered, failure", + sdd_formula_id); + return failure_strategy; + } + } else if (path.find(sdd_formula_id) != path.end()) { + this->print_search_debug("Already visited state {}, failure", + sdd_formula_id); + context_.discovered[sdd_formula_id] = false; + context_.indentation -= 1; + return failure_strategy; + } + + path.insert(sdd_formula_id); + if (!sdd.is_decision()) { + auto system_move_str = + logic::to_string(*sdd_to_formula(sdd.get_raw(), context_)); + this->print_search_debug("system move (unique): {}", system_move_str); + auto new_strategy = env_move_(sdd, path); + if (!new_strategy.empty()) { + path.erase(sdd_formula_id); + context_.discovered[sdd_formula_id] = true; + context_.indentation -= 1; + return success_strategy; + } + } else if (sdd.get_raw()->vtree->parent != NULL) { + // not at the vtree root; it means that system choice is irrelevant + this->print_search_debug("system choice is irrelevant"); + auto env_state_node = sdd; + auto new_strategy = env_move_(env_state_node, path); + if (!new_strategy.empty()) { + this->print_search_debug("Any system move is a success from state {}!", + sdd_formula_id); + path.erase(sdd_formula_id); + // all system moves are OK, since it does not have control + context_.discovered[sdd_formula_id] = true; + context_.indentation -= 1; + return success_strategy; + } + } else { + // is a decision node + auto child_it = sdd.begin(); + auto children_end = sdd.end(); + + if (child_it == children_end) { + path.erase(sdd_formula_id); + context_.discovered[sdd_formula_id] = false; + context_.indentation -= 1; + return failure_strategy; + } + + while (child_it != children_end) { + auto system_move = child_it.get_prime(); + auto system_move_str = + logic::to_string(*sdd_to_formula(system_move, context_)); + this->print_search_debug("checking system move: {}", system_move_str); + auto env_state_node = SddNodeWrapper(child_it.get_sub()); + ++child_it; + if (sdd_node_is_false(system_move)) + continue; + auto new_strategy = env_move_(env_state_node, path); + if (!new_strategy.empty()) { + this->print_search_debug("System move {} from state {} is successful", + sdd_formula_id, system_move_str); + path.erase(sdd_formula_id); + new_strategy[sdd_formula_id] = system_move; + context_.discovered[sdd_formula_id] = true; + context_.indentation -= 1; + return new_strategy; + } + } + } + + this->print_search_debug("State {} is failure", sdd_formula_id); + path.erase(sdd_formula_id); + context_.discovered[sdd_formula_id] = false; + context_.indentation -= 1; + return failure_strategy; +} + +strategy_t ForwardDfsSynthesis::env_move_(SddNodeWrapper& wrapper, + std::set& path) { + logic::ltlf_ptr next_state, sdd_formula; + context_.indentation += 1; + if (!wrapper.is_decision()) { + sdd_formula = sdd_to_formula(wrapper.get_raw(), context_); + auto sdd_formula_str = logic::to_string(*sdd_formula); + next_state = xnf(*strip_next(*sdd_formula)); + auto next_state_str = logic::to_string(*next_state); + auto sdd_next_state = SddNodeWrapper(to_sdd(*next_state, context_)); + auto sdd_next_state_id = sdd_id(sdd_next_state.get_raw()); + this->print_search_debug("env move forced to next state {}", + sdd_next_state_id); + auto strategy = system_move_(next_state, path); + context_.indentation -= 1; + if (strategy[sdd_next_state_id] == sdd_manager_false(context_.manager)) + return strategy_t{}; + return strategy; + } else if (wrapper.get_raw()->vtree->parent->parent != NULL) { + // parent is not the vtree root; it means that environment choice is + // irrelevant + this->print_search_debug("env choice is irrelevant"); + sdd_formula = sdd_to_formula(wrapper.get_raw(), context_); + next_state = xnf(*strip_next(*sdd_formula)); + auto sdd_next_state = SddNodeWrapper(to_sdd(*next_state, context_)); + auto sdd_next_state_id = sdd_id(sdd_next_state.get_raw()); + auto strategy = system_move_(next_state, path); + context_.indentation -= 1; + if (strategy[sdd_next_state_id] == sdd_manager_false(context_.manager)) + return strategy_t{}; + return strategy; + } else { + auto child_it = wrapper.begin(); + auto children_end = wrapper.end(); + strategy_t final_strategy; + for (; child_it != children_end; ++child_it) { + auto env_action = sdd_to_formula(child_it.get_prime(), context_); + auto env_action_str = logic::to_string(*env_action); + sdd_formula = sdd_to_formula(child_it.get_sub(), context_); + next_state = xnf(*strip_next(*sdd_formula)); + auto next_state_str = logic::to_string(*next_state); + auto sdd_next_state = SddNodeWrapper(to_sdd(*next_state, context_)); + auto sdd_next_state_id = sdd_id(sdd_next_state.get_raw()); + this->print_search_debug("env move: {}", env_action_str); + auto strategy = system_move_(next_state, path); + if (strategy[sdd_next_state_id] == sdd_manager_false(context_.manager)) { + context_.indentation -= 1; + return strategy_t{}; + } + final_strategy.insert(strategy.begin(), strategy.end()); + } + context_.indentation -= 1; + return final_strategy; + } +} + +} // namespace core +} // namespace cynthia diff --git a/libs/core/src/to_sdd.cpp b/libs/core/src/to_sdd.cpp index 969d37b..e67ba68 100644 --- a/libs/core/src/to_sdd.cpp +++ b/libs/core/src/to_sdd.cpp @@ -152,8 +152,7 @@ SddNode* ToSddVisitor::apply(const logic::LTLfFormula& formula) { return result; } -SddNode* to_sdd(const logic::LTLfFormula& formula, - ForwardSynthesis::Context& context) { +SddNode* to_sdd(const logic::LTLfFormula& formula, Context& context) { ToSddVisitor visitor{context}; return visitor.apply(formula); } diff --git a/libs/core/tests/unit/test_core/test_complex_formulas.cpp b/libs/core/tests/unit/test_core/test_complex_formulas.cpp index 45a65bc..cdb87f5 100644 --- a/libs/core/tests/unit/test_core/test_complex_formulas.cpp +++ b/libs/core/tests/unit/test_core/test_complex_formulas.cpp @@ -18,6 +18,7 @@ #include #include #include +#include #include namespace cynthia { @@ -34,7 +35,7 @@ TEST_CASE("forward synthesis of random formula 1") { auto not_end = temp->ctx().make_not_end(); auto formula = temp->ctx().make_and({temp, not_end}); auto partition = InputOutputPartition({"p5"}, {"p0", "p1", "p3", "p4"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } @@ -47,7 +48,7 @@ TEST_CASE("forward synthesis of random formula 2") { auto not_end = temp->ctx().make_not_end(); auto formula = temp->ctx().make_and({temp, not_end}); auto partition = InputOutputPartition({"p1", "p0", "p4"}, {"p3"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } TEST_CASE("forward synthesis of random formula 3") { @@ -60,7 +61,7 @@ TEST_CASE("forward synthesis of random formula 3") { auto not_end = temp->ctx().make_not_end(); auto formula = temp->ctx().make_and({temp, not_end}); auto partition = InputOutputPartition({"p5", "p3"}, {"p1", "p0", "p4"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } TEST_CASE("forward synthesis of random formula 4") { @@ -72,7 +73,7 @@ TEST_CASE("forward synthesis of random formula 4") { auto not_end = temp->ctx().make_not_end(); auto formula = temp->ctx().make_and({temp, not_end}); auto partition = InputOutputPartition({"p2", "p4"}, {"p1", "p0"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } TEST_CASE("forward synthesis of random formula 5") { @@ -84,7 +85,7 @@ TEST_CASE("forward synthesis of random formula 5") { auto not_end = temp->ctx().make_not_end(); auto formula = temp->ctx().make_and({temp, not_end}); auto partition = InputOutputPartition({"p0"}, {"dummy"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(!result); } diff --git a/libs/core/tests/unit/test_core/test_core_basic_formulas.cpp b/libs/core/tests/unit/test_core/test_core_basic_formulas.cpp index 1a63429..3311229 100644 --- a/libs/core/tests/unit/test_core/test_core_basic_formulas.cpp +++ b/libs/core/tests/unit/test_core/test_core_basic_formulas.cpp @@ -17,6 +17,7 @@ #include #include +#include namespace cynthia { namespace core { @@ -26,7 +27,7 @@ TEST_CASE("forward synthesis of 'tt'") { logic::Context context; auto partition = InputOutputPartition({"a"}, {"b"}); auto tt = context.make_tt(); - bool result = is_realizable(tt, partition); + bool result = is_realizable(tt, partition); REQUIRE(result); } @@ -34,7 +35,7 @@ TEST_CASE("forward synthesis of 'ff'") { logic::Context context; auto partition = InputOutputPartition({"a"}, {"b"}); auto ff = context.make_ff(); - bool result = is_realizable(ff, partition); + bool result = is_realizable(ff, partition); REQUIRE(!result); } @@ -42,7 +43,7 @@ TEST_CASE("forward synthesis of 'true'") { logic::Context context; auto partition = InputOutputPartition({"a"}, {"b"}); auto true_ = context.make_prop_true(); - bool result = is_realizable(true_, partition); + bool result = is_realizable(true_, partition); REQUIRE(result); } @@ -50,7 +51,7 @@ TEST_CASE("forward synthesis of 'false'") { logic::Context context; auto partition = InputOutputPartition({"a"}, {"b"}); auto false_ = context.make_prop_false(); - bool result = is_realizable(false_, partition); + bool result = is_realizable(false_, partition); REQUIRE(!result); } TEST_CASE("forward synthesis of atom") { @@ -59,12 +60,12 @@ TEST_CASE("forward synthesis of atom") { SECTION("atom controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(a, partition); + bool result = is_realizable(a, partition); REQUIRE(result); } SECTION("atom not-controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(a, partition); + bool result = is_realizable(a, partition); REQUIRE(!result); } } @@ -75,12 +76,12 @@ TEST_CASE("forward synthesis of not atom") { SECTION("atom controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(not_a, partition); + bool result = is_realizable(not_a, partition); REQUIRE(result); } SECTION("atom not-controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(not_a, partition); + bool result = is_realizable(not_a, partition); REQUIRE(!result); } } @@ -93,22 +94,22 @@ TEST_CASE("forward synthesis of 'a and b'") { SECTION("left not-controllable, right not-controllable") { auto partition = InputOutputPartition({"a", "b"}, {"c"}); - bool result = is_realizable(a_and_b, partition); + bool result = is_realizable(a_and_b, partition); REQUIRE(!result); } SECTION("left not-controllable, right controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(a_and_b, partition); + bool result = is_realizable(a_and_b, partition); REQUIRE(!result); } SECTION("left controllable, right not-controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(a_and_b, partition); + bool result = is_realizable(a_and_b, partition); REQUIRE(!result); } SECTION("left controllable, right controllable") { auto partition = InputOutputPartition({"c"}, {"a", "b"}); - bool result = is_realizable(a_and_b, partition); + bool result = is_realizable(a_and_b, partition); REQUIRE(result); } } @@ -120,22 +121,22 @@ TEST_CASE("forward synthesis of 'a or b'") { auto a_or_b = context.make_or({a, b}); SECTION("left not-controllable, right not-controllable") { auto partition = InputOutputPartition({"a", "b"}, {"c"}); - bool result = is_realizable(a_or_b, partition); + bool result = is_realizable(a_or_b, partition); REQUIRE(!result); } SECTION("left not-controllable, right controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(a_or_b, partition); + bool result = is_realizable(a_or_b, partition); REQUIRE(result); } SECTION("left controllable, right not-controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(a_or_b, partition); + bool result = is_realizable(a_or_b, partition); REQUIRE(result); } SECTION("left controllable, right controllable") { auto partition = InputOutputPartition({"c"}, {"a", "b"}); - bool result = is_realizable(a_or_b, partition); + bool result = is_realizable(a_or_b, partition); REQUIRE(result); } } @@ -147,12 +148,12 @@ TEST_CASE("forward synthesis of 'X[!]a' (controllable)") { SECTION("body controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(next_a, partition); + bool result = is_realizable(next_a, partition); REQUIRE(result); } SECTION("body not-controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(next_a, partition); + bool result = is_realizable(next_a, partition); REQUIRE(!result); } } @@ -164,12 +165,12 @@ TEST_CASE("forward synthesis of 'X a'") { SECTION("body controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(weak_next_a, partition); + bool result = is_realizable(weak_next_a, partition); REQUIRE(result); } SECTION("body not-controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(weak_next_a, partition); + bool result = is_realizable(weak_next_a, partition); REQUIRE(result); } } @@ -182,12 +183,12 @@ TEST_CASE("forward synthesis of 'X a', non-empty trace") { SECTION("body controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } SECTION("body not-controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } } @@ -199,22 +200,22 @@ TEST_CASE("forward synthesis of 'a U b'") { SECTION("head non-controllable, tail non-controllable") { auto partition = InputOutputPartition({"a", "b"}, {"c"}); - bool result = is_realizable(a_until_b, partition); + bool result = is_realizable(a_until_b, partition); REQUIRE(!result); } SECTION("head non-controllable, tail controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(a_until_b, partition); + bool result = is_realizable(a_until_b, partition); REQUIRE(result); } SECTION("head controllable, tail non-controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(a_until_b, partition); + bool result = is_realizable(a_until_b, partition); REQUIRE(!result); } SECTION("head controllable, tail controllable") { auto partition = InputOutputPartition({"c"}, {"a", "b"}); - bool result = is_realizable(a_until_b, partition); + bool result = is_realizable(a_until_b, partition); REQUIRE(result); } } @@ -228,22 +229,22 @@ TEST_CASE("forward synthesis of 'a R b'") { SECTION("head non-controllable, tail non-controllable") { auto partition = InputOutputPartition({"a", "b"}, {"c"}); - bool result = is_realizable(a_release_b, partition); + bool result = is_realizable(a_release_b, partition); REQUIRE(result); } SECTION("head non-controllable, tail controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(a_release_b, partition); + bool result = is_realizable(a_release_b, partition); REQUIRE(result); } SECTION("head controllable, tail non-controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(a_release_b, partition); + bool result = is_realizable(a_release_b, partition); REQUIRE(result); } SECTION("head controllable, tail controllable") { auto partition = InputOutputPartition({"c"}, {"a", "b"}); - bool result = is_realizable(a_release_b, partition); + bool result = is_realizable(a_release_b, partition); REQUIRE(result); } } @@ -255,12 +256,12 @@ TEST_CASE("forward synthesis of 'F a'") { SECTION("tail not-controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(eventually_a, partition); + bool result = is_realizable(eventually_a, partition); REQUIRE(!result); } SECTION("tail controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(eventually_a, partition); + bool result = is_realizable(eventually_a, partition); REQUIRE(result); } } @@ -273,12 +274,12 @@ TEST_CASE("forward synthesis of 'G a'") { SECTION("tail not-controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(always_a, partition); + bool result = is_realizable(always_a, partition); REQUIRE(result); } SECTION("tail controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(always_a, partition); + bool result = is_realizable(always_a, partition); REQUIRE(result); } } @@ -291,12 +292,12 @@ TEST_CASE("forward synthesis of 'G a', non-empty trace") { SECTION("tail not-controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(!result); } SECTION("tail controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } } @@ -312,12 +313,12 @@ TEST_CASE("forward synthesis of 'G(a | !b)', non-empty trace") { SECTION("b controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } SECTION("a controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } } @@ -331,12 +332,12 @@ TEST_CASE("forward synthesis of 'X(F(p0))'") { auto formula = context.make_and({next, not_end}); SECTION("p0 uncontrollable") { auto partition = InputOutputPartition({"p0"}, {"p1"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } SECTION("p0 controllable") { auto partition = InputOutputPartition({"p1"}, {"p0"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } } @@ -355,12 +356,12 @@ TEST_CASE("forward synthesis of '((a) & (X(~(a)))) | ((~(a)) & (X(a)))'") { SECTION("a uncontrollable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } SECTION("a controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } } @@ -376,22 +377,22 @@ TEST_CASE("forward synthesis of 'p0 R (F(p1))'") { SECTION("p0 controllable, p1 controllable") { auto partition = InputOutputPartition({"dummy"}, {"p0", "p1"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } SECTION("p0 uncontrollable, p1 controllable") { auto partition = InputOutputPartition({"p0"}, {"p1"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } SECTION("p0 controllable, p1 uncontrollable") { auto partition = InputOutputPartition({"p1"}, {"p0"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(!result); } SECTION("p0 uncontrollable, p1 uncontrollable") { auto partition = InputOutputPartition({"p0", "p1"}, {"dummy"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(!result); } } @@ -409,22 +410,22 @@ TEST_CASE("forward synthesis of '(X(F(~b))) U (G(a))'") { SECTION("a controllable, b controllable") { auto partition = InputOutputPartition({"dummy"}, {"a", "b"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } SECTION("a uncontrollable, b controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(!result); } SECTION("a controllable, b uncontrollable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(result); } SECTION("a uncontrollable, b uncontrollable") { auto partition = InputOutputPartition({"a", "b"}, {"dummy"}); - bool result = is_realizable(formula, partition); + bool result = is_realizable(formula, partition); REQUIRE(!result); } } diff --git a/libs/core/tests/unit/test_to_sdd.cpp b/libs/core/tests/unit/test_to_sdd.cpp index 24d11af..89b06dd 100644 --- a/libs/core/tests/unit/test_to_sdd.cpp +++ b/libs/core/tests/unit/test_to_sdd.cpp @@ -29,7 +29,7 @@ TEST_CASE("Test SDD of tt", "[core][SDD]") { auto logic_context = logic::Context(); auto partition = InputOutputPartition({"a"}, {"b"}); auto tt = logic_context.make_tt(); - auto context = ForwardSynthesis::Context(tt, partition); + auto context = Context(tt, partition); auto sdd = to_sdd(*tt, context); REQUIRE(sdd_size(sdd) == 0); } @@ -38,7 +38,7 @@ TEST_CASE("Test SDD of ff", "[core][SDD]") { auto logic_context = logic::Context(); auto partition = InputOutputPartition({"a"}, {"b"}); auto ff = logic_context.make_ff(); - auto context = ForwardSynthesis::Context(ff, partition); + auto context = Context(ff, partition); auto sdd = to_sdd(*ff, context); REQUIRE(sdd_size(sdd) == 0); } @@ -47,7 +47,7 @@ TEST_CASE("Test SDD of true", "[core][SDD]") { auto logic_context = logic::Context(); auto partition = InputOutputPartition({"a"}, {"b"}); auto true_ = logic_context.make_prop_true(); - auto context = ForwardSynthesis::Context(true_, partition); + auto context = Context(true_, partition); auto sdd = to_sdd(*true_, context); REQUIRE(sdd_size(sdd) == 0); } @@ -56,7 +56,7 @@ TEST_CASE("Test SDD of false", "[core][SDD]") { auto logic_context = logic::Context(); auto partition = InputOutputPartition({"a"}, {"b"}); auto false_ = logic_context.make_prop_true(); - auto context = ForwardSynthesis::Context(false_, partition); + auto context = Context(false_, partition); auto sdd = to_sdd(*false_, context); REQUIRE(sdd_size(sdd) == 0); } @@ -64,7 +64,7 @@ TEST_CASE("Test SDD of a", "[core][SDD]") { auto logic_context = logic::Context(); auto partition = InputOutputPartition({"a"}, {"b"}); auto a = logic_context.make_atom("a"); - auto context = ForwardSynthesis::Context(a, partition); + auto context = Context(a, partition); auto sdd = to_sdd(*a, context); REQUIRE(sdd_size(sdd) == 2); } From 6f7596442e6f8cddbc18c8e51a160850a2b1b9aa Mon Sep 17 00:00:00 2001 From: MarcoFavorito Date: Mon, 23 Aug 2021 14:43:51 +0200 Subject: [PATCH 2/2] wip: partial implementation of ao* --- libs/core/include/cynthia/core.hpp | 10 + libs/core/include/cynthia/sddcpp.hpp | 8 +- .../cynthia/strategies/breadth_first.hpp | 190 +++++++++++++++ .../strategies/{dfs.hpp => depth_first.hpp} | 14 +- libs/core/src/sddcpp.cpp | 10 + libs/core/src/strategies/breadth_first.cpp | 225 ++++++++++++++++++ .../strategies/{dfs.cpp => depth_first.cpp} | 49 ++-- .../unit/test_core/test_complex_formulas.cpp | 2 +- .../test_core/test_core_basic_formulas.cpp | 15 +- libs/utils/include/cynthia/utils.hpp | 31 +++ 10 files changed, 506 insertions(+), 48 deletions(-) create mode 100644 libs/core/include/cynthia/strategies/breadth_first.hpp rename libs/core/include/cynthia/strategies/{dfs.hpp => depth_first.hpp} (74%) create mode 100644 libs/core/src/strategies/breadth_first.cpp rename libs/core/src/strategies/{dfs.cpp => depth_first.cpp} (82%) diff --git a/libs/core/include/cynthia/core.hpp b/libs/core/include/cynthia/core.hpp index 65752a2..8cf6478 100644 --- a/libs/core/include/cynthia/core.hpp +++ b/libs/core/include/cynthia/core.hpp @@ -71,6 +71,16 @@ class Context { static std::map compute_prop_to_id_map(const Closure& closure, const InputOutputPartition& partition); + + template + inline void print_search_debug(const char* fmt, const Arg1& arg1, + const Args&... args) { + logger.debug((std::string(indentation, '\t') + fmt).c_str(), arg1, args...); + }; + + inline void print_search_debug(const char* fmt) { + logger.debug((std::string(indentation, '\t') + fmt).c_str()); + }; }; } // namespace core diff --git a/libs/core/include/cynthia/sddcpp.hpp b/libs/core/include/cynthia/sddcpp.hpp index 55bb059..5d289e2 100644 --- a/libs/core/include/cynthia/sddcpp.hpp +++ b/libs/core/include/cynthia/sddcpp.hpp @@ -28,13 +28,13 @@ namespace cynthia { namespace core { class SddNodeChildrenIterator; -class SddTransitionIterator; class SddNodeWrapper { private: SddNode* raw_{}; SddNodeSize nb_children_ = 0; SddNode** children_ = nullptr; + SddNodeSize id; public: SddNodeWrapper() = default; @@ -46,10 +46,12 @@ class SddNodeWrapper { bool is_decision() const; long node_literal() const; long nb_children() const; + bool at_vtree_root() const; + bool parent_at_vtree_root() const; + SddNodeSize get_id() const; SddNodeChildrenIterator begin() const; + SddNodeChildrenIterator end() const; - SddTransitionIterator transitions_begin() const; - SddTransitionIterator transitions_end() const; }; struct SddNodeChildrenIterator { diff --git a/libs/core/include/cynthia/strategies/breadth_first.hpp b/libs/core/include/cynthia/strategies/breadth_first.hpp new file mode 100644 index 0000000..d7ecf9f --- /dev/null +++ b/libs/core/include/cynthia/strategies/breadth_first.hpp @@ -0,0 +1,190 @@ +#pragma once +/* + * This file is part of Cynthia. + * + * Cynthia is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Cynthia is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Cynthia. If not, see . + */ + +#include +#include + +namespace cynthia { +namespace core { + +constexpr inline size_t infty() { return std::numeric_limits::max(); } + +enum Label { SOLVED = 1, UNKNOWN = 0, FAILED = -1 }; +enum NodeType { + UNDEFINED = 0, + TERMINAL = 1, + AND = 2, + OR = 3, +}; + +enum SddNodeType { + STATE = 0, + ENV_STATE = 1, + SYSTEM_STATE = 2, + SYSTEM_ENV_STATE = 3, +}; + +class node_t; +typedef std::shared_ptr node_ptr; + +struct node_t { +public: + size_t id; + SddNodeWrapper sdd_node; + SddNodeType sdd_node_type; + NodeType type; + Label label; + unsigned long f; + unsigned long f_new; + unsigned long f_old; + + explicit node_t(const SddNodeWrapper& sdd_node, bool is_terminal = false) { + this->sdd_node = sdd_node; + id = sdd_node.get_id(); + sdd_node_type = get_sdd_node_type_(sdd_node); + type = get_node_type_(sdd_node_type); + label = is_terminal ? Label::SOLVED : Label::UNKNOWN; + f = 0; + } + + inline bool solved() const { return label == Label::SOLVED; } + inline bool failed() const { return label == Label::FAILED; } + inline bool is_cost_infinite() const { + return f == std::numeric_limits::max(); + } + inline void set_node_type(NodeType new_node_type) { + if (type != NodeType::UNDEFINED and type != new_node_type) { + throw std::logic_error("type already set"); + } + type = new_node_type; + } + +private: + static inline NodeType get_node_type_(SddNodeType sdd_node_type) { + if (sdd_node_type == SYSTEM_ENV_STATE or sdd_node_type == SYSTEM_STATE) { + return NodeType::OR; + } + if (sdd_node_type == ENV_STATE) { + return NodeType::AND; + } + return NodeType::UNDEFINED; + } + + static inline SddNodeType get_sdd_node_type_(const SddNodeWrapper& wrapper) { + if (!wrapper.is_decision()) { + return STATE; + } else if (!wrapper.at_vtree_root()) { + if (!wrapper.parent_at_vtree_root()) { + return STATE; + } + return ENV_STATE; + } else { + if (!SddNodeWrapper((wrapper.begin()).get_sub()).parent_at_vtree_root()) { + return SYSTEM_STATE; + } + return SYSTEM_ENV_STATE; + } + } +}; + +struct node_comparator { + size_t operator()(node_ptr const& a, node_ptr const& b) const { + return a->id < b->id; + } +}; + +struct graph_t { + std::map id_to_node; + std::map> successors; + std::map> marked_successors; + std::map> marked_predecessors; + std::queue tips; + std::set tip_set; + + inline void add_node(const node_ptr& node) { + id_to_node[node->id] = node; + tips.push(node); + tip_set.insert(node->id); + } + inline void add_successors(size_t node_id, + std::vector node_successors) { + std::sort(node_successors.begin(), node_successors.end()); + successors[node_id] = node_successors; + } + + inline bool is_already_added(size_t node_id) const { + return id_to_node.find(node_id) != id_to_node.end(); + } + inline bool has_next() const { return tips.empty(); } + inline bool is_tip(size_t node_id) const { + return tip_set.find(node_id) != tip_set.end(); + } + inline node_ptr next() { + auto result = tips.front(); + tips.pop(); + tip_set.erase(result->id); + return result; + } + inline std::set get_marked_predecessors(size_t node_id) const { + if (marked_predecessors.find(node_id) == marked_predecessors.end()) { + return {}; + } + return marked_predecessors.at(node_id); + } + inline void mark_arc(const node_ptr& left, const node_ptr& right) { + if (left->type == NodeType::OR) { + auto left_marked_successors = marked_successors[left->id]; + left_marked_successors.clear(); + left_marked_successors.push_back(right->id); + // TODO + } + } +}; + +class BfsContext : public Context { +public: + graph_t graph; + BfsContext(const logic::ltlf_ptr& formula, + const InputOutputPartition& partition) + : Context(formula, partition){}; +}; + +class ForwardBfsSynthesis : public ISynthesis { +public: + ForwardBfsSynthesis(const logic::ltlf_ptr& formula, + const InputOutputPartition& partition) + : context_{formula, partition}, ISynthesis(formula, partition){}; + + bool is_realizable() override; + + bool forward_synthesis_(); + node_ptr get_state_node(const SddNodeWrapper& wrapper); + node_ptr get_env_node(const SddNodeWrapper& wrapper); + std::vector get_successors(node_t& node); + static SddNodeType get_node_type(const SddNodeWrapper& wrapper); + +private: + BfsContext context_; + + void build_revisable(size_t node, std::set& z_set); + void init_open(size_t node, std::set& o_set, + const std::set& z_set); +}; + +} // namespace core +} // namespace cynthia \ No newline at end of file diff --git a/libs/core/include/cynthia/strategies/dfs.hpp b/libs/core/include/cynthia/strategies/depth_first.hpp similarity index 74% rename from libs/core/include/cynthia/strategies/dfs.hpp rename to libs/core/include/cynthia/strategies/depth_first.hpp index 05d409e..2140eef 100644 --- a/libs/core/include/cynthia/strategies/dfs.hpp +++ b/libs/core/include/cynthia/strategies/depth_first.hpp @@ -16,6 +16,8 @@ * along with Cynthia. If not, see . */ +#include + namespace cynthia { namespace core { @@ -32,18 +34,6 @@ class ForwardDfsSynthesis : public ISynthesis { private: Context context_; - template - inline void print_search_debug(const char* fmt, const Arg1& arg1, - const Args&... args) { - context_.logger.debug( - (std::string(context_.indentation, '\t') + fmt).c_str(), arg1, args...); - }; - - inline void print_search_debug(const char* fmt) { - context_.logger.debug( - (std::string(context_.indentation, '\t') + fmt).c_str()); - }; - strategy_t system_move_(const logic::ltlf_ptr& formula, std::set& path); diff --git a/libs/core/src/sddcpp.cpp b/libs/core/src/sddcpp.cpp index cc7c901..487857e 100644 --- a/libs/core/src/sddcpp.cpp +++ b/libs/core/src/sddcpp.cpp @@ -29,6 +29,7 @@ SddNodeWrapper::SddNodeWrapper(SddNode* raw) : raw_{raw} { children_ = sdd_node_elements(raw); nb_children_ = sdd_node_size(raw); } + id = sdd_id(raw); } bool SddNodeWrapper::is_true() const { return sdd_node_is_true(raw_); } @@ -59,5 +60,14 @@ SddNodeChildrenIterator SddNodeWrapper::end() const { long SddNodeWrapper::nb_children() const { return nb_children_; } +bool SddNodeWrapper::at_vtree_root() const { + return raw_->vtree->parent == nullptr; +} +bool SddNodeWrapper::parent_at_vtree_root() const { + return raw_->vtree->parent->parent == nullptr; +} + +SddNodeSize SddNodeWrapper::get_id() const { return id; } + } // namespace core } // namespace cynthia diff --git a/libs/core/src/strategies/breadth_first.cpp b/libs/core/src/strategies/breadth_first.cpp new file mode 100644 index 0000000..3a36ba2 --- /dev/null +++ b/libs/core/src/strategies/breadth_first.cpp @@ -0,0 +1,225 @@ +/* + * This file is part of Cynthia. + * + * Cynthia is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Cynthia is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Cynthia. If not, see . + */ + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +namespace cynthia { +namespace core { + +bool core::ForwardBfsSynthesis::is_realizable() { + bool result = forward_synthesis_(); + return result; +} + +bool ForwardBfsSynthesis::forward_synthesis_() { + auto root_formula = context_.xnf_formula; + bool is_root_terminal = eval(*root_formula); + if (is_root_terminal) + return true; + + auto root_sdd_node_raw = to_sdd(*root_formula, context_); + auto root_sdd_node = SddNodeWrapper(root_sdd_node_raw); + auto root_node = std::make_shared(root_sdd_node); + std::map found; + + context_.graph.add_node(root_node); + root_node->f = 0; + + while (!root_node->solved() and !root_node->is_cost_infinite() and + context_.graph.has_next()) { + node_ptr current_node = context_.graph.next(); + + auto sdd_formula_str = logic::to_string( + *sdd_to_formula(current_node->sdd_node.get_raw(), context_)); + context_.logger.info("Expanding state {}: {}", current_node->id, + sdd_formula_str); + + auto children = get_successors(*current_node); + for (auto& child : children) { + if (!context_.graph.is_already_added(child->id)) { + context_.graph.add_node(child); + child->f = 0; + child->f_new = 0; + found[child->id] = true; + } + } + + context_.logger.info("successors: "); + for (const auto& successor : children) { + auto sdd_formula_str = logic::to_string( + *sdd_to_formula(successor->sdd_node.get_raw(), context_)); + context_.logger.info("\t{}: {}", successor->id, sdd_formula_str); + } + + std::vector children_ids(children.size()); + std::transform(children.begin(), children.end(), children_ids.begin(), + [](const node_ptr& node) { return node->id; }); + context_.graph.add_successors(current_node->id, children_ids); + + auto z_set = std::set(); + build_revisable(current_node->id, z_set); + for (const auto& z_node_id : z_set) { + found[z_node_id] = false; + } + auto o_set = std::set(); + init_open(current_node->id, o_set, z_set); + auto cmp = [](const node_ptr& left, const node_ptr& right) { + return left->f_new >= right->f_new; + }; + std::priority_queue, decltype(cmp)> heap( + cmp); + for (const auto& element_id : o_set) { + heap.push(context_.graph.id_to_node[element_id]); + } + while (!heap.empty()) { + auto current_o_node = heap.top(); + heap.pop(); + if (current_o_node->type == NodeType::OR) { + auto current_o_successors = + context_.graph.successors[current_o_node->id]; + node_ptr o_node_successor_min = + context_.graph.id_to_node[current_o_successors[0]]; + for (const auto& o_node_successor_id : current_o_successors) { + auto o_node_successor = + context_.graph.id_to_node[o_node_successor_id]; + if (current_o_node->f_new == (1 + o_node_successor->f_new) and + (o_node_successor_min->f_new > o_node_successor->f_new or + (o_node_successor_min->f_new == o_node_successor->f_new and + o_node_successor->solved()))) { + o_node_successor_min = o_node_successor; + } + } + } + } + } + + return root_node->solved(); +} + +node_ptr ForwardBfsSynthesis::get_state_node(const SddNodeWrapper& wrapper) { + auto sdd_formula = sdd_to_formula(wrapper.get_raw(), context_); + auto next_state = xnf(*strip_next(*formula)); + auto sdd_next_state = SddNodeWrapper(to_sdd(*next_state, context_)); + bool is_terminal = eval(*sdd_formula); + return std::make_shared(sdd_next_state, is_terminal = is_terminal); +} + +std::vector ForwardBfsSynthesis::get_successors(node_t& node) { + std::vector result; + + if (node.type == NodeType::OR or node.type == NodeType::AND) { + auto child_it = node.sdd_node.begin(); + auto children_end = node.sdd_node.end(); + for (; child_it != children_end; ++child_it) { + node_ptr child; + if (node.type == NodeType::OR) { + child = std::make_shared(SddNodeWrapper(child_it.get_sub())); + } else { // if (node.type == NodeType::AND) + child = get_state_node(SddNodeWrapper(child_it.get_sub())); + } + + child = context_.insert_or_get_node(child); + result.push_back(child); + } + return result; + } + + // node.type == NodeType::TERMINAL + auto next_node = get_state_node(node.sdd_node); + if (next_node->id != node.id) { + node.set_node_type(NodeType::OR); + next_node = context_.insert_or_get_node(next_node); + return {next_node}; + } + // same state -> return no successors + node.set_node_type(NodeType::TERMINAL); + node.label = next_node->solved() ? Label::SOLVED : Label::FAILED; + return result; +} + +void ForwardBfsSynthesis::build_revisable(size_t node_id, + std::set& set) { + for (const auto& predecessor : + context_.graph.get_marked_predecessors(node_id)) { + if (set.find(predecessor) != set.end()) { + set.insert(predecessor); + build_revisable(predecessor, set); + } + } +} + +void ForwardBfsSynthesis::init_open(size_t node_id, std::set& o_set, + const std::set& z_set) { + auto node = context_.graph.id_to_node[node_id]; + auto successors = context_.graph.successors[node_id]; + if (node->type == NodeType::AND and + utils::empty_intersection(successors.begin(), successors.end(), + z_set.begin(), z_set.end())) { + size_t total_cost = 0; + bool is_solved = true; + std::for_each(successors.begin(), successors.end(), + [this, &total_cost, &is_solved](size_t successor_id) { + auto successor = context_.graph.id_to_node[successor_id]; + total_cost += 1 + successor->f; + is_solved = is_solved and successor->solved(); + }); + node->f_new = total_cost; + if (is_solved) + node->label = Label::SOLVED; + o_set.insert(node_id); + if (node->f_new <= node->f) { + return; + } + } else if (node->type == NodeType::OR and + !utils::empty_difference(successors.begin(), successors.end(), + z_set.begin(), z_set.end())) { + std::set difference; + std::set_difference(successors.begin(), successors.end(), z_set.begin(), + z_set.end(), difference.begin()); + auto min_cost = + std::min_element(difference.begin(), difference.end(), + [](const node_ptr& left, const node_ptr& right) { + return left->f < right->f; + }); + node->f_new = *min_cost; + o_set.insert(node->id); + if (node->f_new <= node->f) { + return; + } + } else { + node->f_new = infty(); + } + if (node->f_new > node->f) { + for (const auto& predecessor : + context_.graph.get_marked_predecessors(node->id)) { + if (o_set.find(predecessor) != o_set.end()) { + init_open(node_id, o_set, z_set); + } + } + } +} +} // namespace core +} // namespace cynthia diff --git a/libs/core/src/strategies/dfs.cpp b/libs/core/src/strategies/depth_first.cpp similarity index 82% rename from libs/core/src/strategies/dfs.cpp rename to libs/core/src/strategies/depth_first.cpp index 2068fd8..219d16b 100644 --- a/libs/core/src/strategies/dfs.cpp +++ b/libs/core/src/strategies/depth_first.cpp @@ -17,14 +17,12 @@ #include #include -#include #include #include #include -#include +#include #include #include -#include #include namespace cynthia { @@ -56,9 +54,9 @@ strategy_t ForwardDfsSynthesis::system_move_(const logic::ltlf_ptr& formula, context_.statistics_.visit_node(sdd_formula_id); success_strategy[sdd_formula_id] = sdd_manager_true(context_.manager); failure_strategy[sdd_formula_id] = sdd_manager_false(context_.manager); - this->print_search_debug("State {}", sdd_formula_id); + context_.print_search_debug("State {}", sdd_formula_id); if (eval(*formula)) { - this->print_search_debug("{} accepting!", sdd_formula_id); + context_.print_search_debug("{} accepting!", sdd_formula_id); context_.discovered[sdd_formula_id] = true; context_.indentation -= 1; return success_strategy; @@ -68,17 +66,17 @@ strategy_t ForwardDfsSynthesis::system_move_(const logic::ltlf_ptr& formula, context_.indentation -= 1; bool is_success = context_.discovered[sdd_formula_id]; if (is_success) { - this->print_search_debug("{} already discovered, success", - sdd_formula_id); + context_.print_search_debug("{} already discovered, success", + sdd_formula_id); return success_strategy; } else { - this->print_search_debug("{} already discovered, failure", - sdd_formula_id); + context_.print_search_debug("{} already discovered, failure", + sdd_formula_id); return failure_strategy; } } else if (path.find(sdd_formula_id) != path.end()) { - this->print_search_debug("Already visited state {}, failure", - sdd_formula_id); + context_.print_search_debug("Already visited state {}, failure", + sdd_formula_id); context_.discovered[sdd_formula_id] = false; context_.indentation -= 1; return failure_strategy; @@ -88,7 +86,7 @@ strategy_t ForwardDfsSynthesis::system_move_(const logic::ltlf_ptr& formula, if (!sdd.is_decision()) { auto system_move_str = logic::to_string(*sdd_to_formula(sdd.get_raw(), context_)); - this->print_search_debug("system move (unique): {}", system_move_str); + context_.print_search_debug("system move (unique): {}", system_move_str); auto new_strategy = env_move_(sdd, path); if (!new_strategy.empty()) { path.erase(sdd_formula_id); @@ -96,14 +94,14 @@ strategy_t ForwardDfsSynthesis::system_move_(const logic::ltlf_ptr& formula, context_.indentation -= 1; return success_strategy; } - } else if (sdd.get_raw()->vtree->parent != NULL) { + } else if (!sdd.at_vtree_root()) { // not at the vtree root; it means that system choice is irrelevant - this->print_search_debug("system choice is irrelevant"); + context_.print_search_debug("system choice is irrelevant"); auto env_state_node = sdd; auto new_strategy = env_move_(env_state_node, path); if (!new_strategy.empty()) { - this->print_search_debug("Any system move is a success from state {}!", - sdd_formula_id); + context_.print_search_debug("Any system move is a success from state {}!", + sdd_formula_id); path.erase(sdd_formula_id); // all system moves are OK, since it does not have control context_.discovered[sdd_formula_id] = true; @@ -126,15 +124,16 @@ strategy_t ForwardDfsSynthesis::system_move_(const logic::ltlf_ptr& formula, auto system_move = child_it.get_prime(); auto system_move_str = logic::to_string(*sdd_to_formula(system_move, context_)); - this->print_search_debug("checking system move: {}", system_move_str); + context_.print_search_debug("checking system move: {}", system_move_str); auto env_state_node = SddNodeWrapper(child_it.get_sub()); ++child_it; if (sdd_node_is_false(system_move)) continue; auto new_strategy = env_move_(env_state_node, path); if (!new_strategy.empty()) { - this->print_search_debug("System move {} from state {} is successful", - sdd_formula_id, system_move_str); + context_.print_search_debug( + "System move {} from state {} is successful", sdd_formula_id, + system_move_str); path.erase(sdd_formula_id); new_strategy[sdd_formula_id] = system_move; context_.discovered[sdd_formula_id] = true; @@ -144,7 +143,7 @@ strategy_t ForwardDfsSynthesis::system_move_(const logic::ltlf_ptr& formula, } } - this->print_search_debug("State {} is failure", sdd_formula_id); + context_.print_search_debug("State {} is failure", sdd_formula_id); path.erase(sdd_formula_id); context_.discovered[sdd_formula_id] = false; context_.indentation -= 1; @@ -162,17 +161,17 @@ strategy_t ForwardDfsSynthesis::env_move_(SddNodeWrapper& wrapper, auto next_state_str = logic::to_string(*next_state); auto sdd_next_state = SddNodeWrapper(to_sdd(*next_state, context_)); auto sdd_next_state_id = sdd_id(sdd_next_state.get_raw()); - this->print_search_debug("env move forced to next state {}", - sdd_next_state_id); + context_.print_search_debug("env move forced to next state {}", + sdd_next_state_id); auto strategy = system_move_(next_state, path); context_.indentation -= 1; if (strategy[sdd_next_state_id] == sdd_manager_false(context_.manager)) return strategy_t{}; return strategy; - } else if (wrapper.get_raw()->vtree->parent->parent != NULL) { + } else if (!wrapper.parent_at_vtree_root()) { // parent is not the vtree root; it means that environment choice is // irrelevant - this->print_search_debug("env choice is irrelevant"); + context_.print_search_debug("env choice is irrelevant"); sdd_formula = sdd_to_formula(wrapper.get_raw(), context_); next_state = xnf(*strip_next(*sdd_formula)); auto sdd_next_state = SddNodeWrapper(to_sdd(*next_state, context_)); @@ -194,7 +193,7 @@ strategy_t ForwardDfsSynthesis::env_move_(SddNodeWrapper& wrapper, auto next_state_str = logic::to_string(*next_state); auto sdd_next_state = SddNodeWrapper(to_sdd(*next_state, context_)); auto sdd_next_state_id = sdd_id(sdd_next_state.get_raw()); - this->print_search_debug("env move: {}", env_action_str); + context_.print_search_debug("env move: {}", env_action_str); auto strategy = system_move_(next_state, path); if (strategy[sdd_next_state_id] == sdd_manager_false(context_.manager)) { context_.indentation -= 1; diff --git a/libs/core/tests/unit/test_core/test_complex_formulas.cpp b/libs/core/tests/unit/test_core/test_complex_formulas.cpp index cdb87f5..c5acca5 100644 --- a/libs/core/tests/unit/test_core/test_complex_formulas.cpp +++ b/libs/core/tests/unit/test_core/test_complex_formulas.cpp @@ -18,7 +18,7 @@ #include #include #include -#include +#include #include namespace cynthia { diff --git a/libs/core/tests/unit/test_core/test_core_basic_formulas.cpp b/libs/core/tests/unit/test_core/test_core_basic_formulas.cpp index 3311229..8baf234 100644 --- a/libs/core/tests/unit/test_core/test_core_basic_formulas.cpp +++ b/libs/core/tests/unit/test_core/test_core_basic_formulas.cpp @@ -17,7 +17,8 @@ #include #include -#include +#include +#include namespace cynthia { namespace core { @@ -27,7 +28,7 @@ TEST_CASE("forward synthesis of 'tt'") { logic::Context context; auto partition = InputOutputPartition({"a"}, {"b"}); auto tt = context.make_tt(); - bool result = is_realizable(tt, partition); + bool result = is_realizable(tt, partition); REQUIRE(result); } @@ -35,7 +36,7 @@ TEST_CASE("forward synthesis of 'ff'") { logic::Context context; auto partition = InputOutputPartition({"a"}, {"b"}); auto ff = context.make_ff(); - bool result = is_realizable(ff, partition); + bool result = is_realizable(ff, partition); REQUIRE(!result); } @@ -43,7 +44,7 @@ TEST_CASE("forward synthesis of 'true'") { logic::Context context; auto partition = InputOutputPartition({"a"}, {"b"}); auto true_ = context.make_prop_true(); - bool result = is_realizable(true_, partition); + bool result = is_realizable(true_, partition); REQUIRE(result); } @@ -51,7 +52,7 @@ TEST_CASE("forward synthesis of 'false'") { logic::Context context; auto partition = InputOutputPartition({"a"}, {"b"}); auto false_ = context.make_prop_false(); - bool result = is_realizable(false_, partition); + bool result = is_realizable(false_, partition); REQUIRE(!result); } TEST_CASE("forward synthesis of atom") { @@ -60,12 +61,12 @@ TEST_CASE("forward synthesis of atom") { SECTION("atom controllable") { auto partition = InputOutputPartition({"b"}, {"a"}); - bool result = is_realizable(a, partition); + bool result = is_realizable(a, partition); REQUIRE(result); } SECTION("atom not-controllable") { auto partition = InputOutputPartition({"a"}, {"b"}); - bool result = is_realizable(a, partition); + bool result = is_realizable(a, partition); REQUIRE(!result); } } diff --git a/libs/utils/include/cynthia/utils.hpp b/libs/utils/include/cynthia/utils.hpp index 69d116d..1da2e3f 100644 --- a/libs/utils/include/cynthia/utils.hpp +++ b/libs/utils/include/cynthia/utils.hpp @@ -177,5 +177,36 @@ template inline int ordered_compare(const T& A, const T& B) { return 0; } +template +bool empty_intersection(InputIterator1 first1, InputIterator1 last1, + InputIterator2 first2, InputIterator2 last2) { + auto i = first1; + auto j = first2; + while (i != last1 && j != last2) { + if (*i < *j) + ++i; + else if (*j < *i) + ++j; + else + return false; + } + return true; +} +template +bool empty_difference(InputIterator1 first1, InputIterator1 last1, + InputIterator2 first2, InputIterator2 last2) { + auto i = first1; + auto j = first2; + while (i != last1 && j != last2) { + if (*i < *j) + ++i; + else if (*j < *i) + return false; + else + ++j; + } + return true; +} + } // namespace utils } // namespace cynthia \ No newline at end of file