diff --git a/CMakeLists.txt b/CMakeLists.txt index b3e9334..6bda84c 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -43,7 +43,7 @@ if(PDAAAL_AddressSanitizer) add_compile_options(-fno-omit-frame-pointer -fsanitize=address) endif(PDAAAL_AddressSanitizer) -find_package(Boost 1.70 CONFIG REQUIRED COMPONENTS headers program_options unit_test_framework) +find_package(Boost 1.70 REQUIRED COMPONENTS program_options unit_test_framework) #actual library add_subdirectory(src) diff --git a/src/include/pdaaal/AutomatonPath.h b/src/include/pdaaal/AutomatonPath.h index a56d669..f9771a6 100644 --- a/src/include/pdaaal/AutomatonPath.h +++ b/src/include/pdaaal/AutomatonPath.h @@ -133,6 +133,12 @@ namespace pdaaal { return std::make_pair(*this, *this); } } + void remove_epsilon() { + if (!empty() && std::get<1>(front_edge()) == std::numeric_limits::max()) { + assert(std::get<0>(front_edge()) == std::get<2>(front_edge())); + pop(); + } + } friend bool operator==(const AutomatonPath& l, const AutomatonPath& r) { return l._end == r._end && l._edges == r._edges; diff --git a/src/include/pdaaal/PAutomaton.h b/src/include/pdaaal/PAutomaton.h index 91b7d88..f87dc8a 100644 --- a/src/include/pdaaal/PAutomaton.h +++ b/src/include/pdaaal/PAutomaton.h @@ -1,14 +1,14 @@ -/* +/* * This program 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. - * + * * This program 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 this program. If not, see . */ @@ -17,7 +17,7 @@ * Copyright Morten K. Schou */ -/* +/* * File: PAutomaton.h * Author: Morten K. Schou * diff --git a/src/include/pdaaal/PAutomatonProduct.h b/src/include/pdaaal/PAutomatonProduct.h index db4ec42..1ee1983 100644 --- a/src/include/pdaaal/PAutomatonProduct.h +++ b/src/include/pdaaal/PAutomatonProduct.h @@ -1,14 +1,14 @@ -/* +/* * This program 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. - * + * * This program 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 this program. If not, see . */ @@ -17,7 +17,7 @@ * Copyright Morten K. Schou */ -/* +/* * File: PAutomatonProduct.h * Author: Morten K. Schou * @@ -34,12 +34,20 @@ namespace pdaaal { - template + template class PAutomatonProduct { + public: + using pda_t = _pda_t; + using automaton_t = _automaton_t; + using W = _weight_t; + static constexpr auto trace_info_type = _trace_info_type; + private: using product_automaton_t = internal::PAutomaton; // No explicit abstraction on product automaton - this is covered by _initial and _final. using state_t = typename product_automaton_t::state_t; static constexpr auto epsilon = product_automaton_t::epsilon; using weight_t = typename W::type; + using edge_anno = internal::edge_annotation; + using edge_anno_t = internal::edge_annotation_t; struct queue_elem_comp { bool operator()(const auto& lhs, const auto& rhs) const { return internal::solver_weight::less(rhs, lhs); // Used in a max-heap, so swap arguments to make it a min-heap. @@ -101,11 +109,14 @@ namespace pdaaal { } // This is for the dual_search mode: + template bool add_initial_edge(size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace, const weight_or_bool_t& et_param = default_weight_or_bool()) { - return add_edge(from, label, to, trace, _initial, _final, et_param); + return add_edge(from, label, to, trace, _initial, _final, et_param); } + + template bool add_final_edge(size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace, const weight_or_bool_t& et_param = default_weight_or_bool()) { - return add_edge(from, label, to, trace, _initial, _final, et_param); + return add_edge(from, label, to, trace, _initial, _final, et_param); } automaton_t& automaton() { @@ -131,15 +142,15 @@ namespace pdaaal { return _product; } template - void automaton_to_dot(std::ostream &out) { + void automaton_to_dot(std::ostream &out) const { automaton_to_dot(out, automaton()); } template - void product_automaton_to_dot(std::ostream &out) { + void product_automaton_to_dot(std::ostream &out) const { automaton_to_dot(out, product_automaton()); } template - void automaton_to_dot(std::ostream &out, const aut_t& automaton) { + void automaton_to_dot(std::ostream &out, const aut_t& automaton) const { automaton.template to_dot(out, [this](std::ostream& s, const uint32_t& label){ s << pda().get_symbol(label); }, [this,pda_size=pda().states().size()](std::ostream& s, const size_t& state_id){ @@ -181,7 +192,7 @@ namespace pdaaal { template std::tuple, typename W::type> find_path_shortest() const { - return _product.get_path_shortest([this](size_t s){ return get_original(s); }); + return _product.template get_path_shortest([this](auto s){ return get_original(s); }); } template @@ -206,11 +217,11 @@ namespace pdaaal { } private: - template + template bool add_edge(size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace, const automaton_t& first, const automaton_t& second, // States in first and second automaton corresponds to respectively first and second component of the states in product automaton. [[maybe_unused]] const weight_or_bool_t& et_param) { - static_assert(edge_in_first || needs_back_lookup, "If you insert edge in the second automaton, then you must also enable using _id_fast_lookup_back to keep the relevant information."); + static_assert(edge_in_first || is_dual, "If you insert edge in the second automaton, then you must also enable using _id_fast_lookup_back to keep the relevant information."); const auto& fast_lookup = constexpr_ternary(_id_fast_lookup, _id_fast_lookup_back); std::vector> from_states; if (from < fast_lookup.size()) { // Avoid out-of-bounds. @@ -224,28 +235,34 @@ namespace pdaaal { auto current_to = current.states()[to].get(); queue_type waiting; for (auto [other_from, product_from] : from_states) { // Iterate through reachable 'from-states'. - std::vector other_tos; + std::vector> other_tos; if (label == epsilon) { - other_tos.emplace_back(other_from); + other_tos.emplace_back(other_from, trace); } else { for (const auto& [other_to,other_labels] : other.states()[other_from]->_edges) { - if (other_labels.contains(label)) { - other_tos.emplace_back(other_to); + auto it = other_labels.find(label); + if (it != other_labels.end()) { + if constexpr(W::is_weight && trace_type == Trace_Type::Shortest && is_dual) { + auto w = internal::solver_weight::add(trace.second, it->second.second); + other_tos.emplace_back(other_to, std::make_pair(trace.first, std::move(w))); + } else { + other_tos.emplace_back(other_to, trace); + } } } } - for (auto other_to : other_tos) { - auto [fresh, product_to] = get_product_state(swap_if(current_to, other.states()[other_to].get())); + for (auto&& [other_to,product_trace] : other_tos) { + auto [fresh, product_to] = get_product_state(swap_if(current_to, other.states()[other_to].get())); if (label == epsilon) { - _product.add_epsilon_edge(product_from, product_to, trace); + _product.add_epsilon_edge(product_from, product_to, product_trace); } else { - _product.add_edge(product_from, product_to, label, trace); + _product.add_edge(product_from, product_to, label, product_trace); } if constexpr(W::is_weight && trace_type == Trace_Type::Shortest) { - auto w_opt = _product.make_back_edge_shortest(product_from, label, product_to, trace.second); + auto w_opt = _product.make_back_edge_shortest(product_from, label, product_to, product_trace.second); assert(!fresh || w_opt); // fresh must imply weight change. if constexpr(ET) { - if (!internal::solver_weight::less(et_param, _product.min_accepting_weight())) { + if (_product.has_accepting_state() && !internal::solver_weight::less(et_param, _product.min_accepting_weight())) { return true; // Early termination } } @@ -267,11 +284,11 @@ namespace pdaaal { } } } - return construct_reachable(waiting, first, second, et_param); + return construct_reachable(waiting, first, second, et_param); } // Returns whether an accepting state in the product automaton was reached. - template + template bool construct_reachable(queue_type& waiting, const automaton_t& initial, const automaton_t& final, [[maybe_unused]] const weight_or_bool_t& et_param) { while (!waiting.empty()) { size_t top = waiting.back(); @@ -280,14 +297,14 @@ namespace pdaaal { for (bool flip : std::array{true,false}) { for (const auto& [to,labels] : (flip ? initial : final).states()[flip ? i_from : f_from]->_edges) { if (auto it = labels.find(epsilon); it != labels.end()) { - auto [fresh, product_to] = get_product_state( + auto [fresh, product_to] = get_product_state( initial.states()[(flip ? to : i_from)].get(), final.states()[(flip ? f_from : to)].get()); _product.add_epsilon_edge(top, product_to, it->second); if constexpr(W::is_weight && trace_type == Trace_Type::Shortest) { auto w_opt = _product.make_back_edge_shortest(top, epsilon, product_to, it->second.second); assert(!fresh || w_opt); // fresh must imply weight change. if constexpr(ET) { - if (!internal::solver_weight::less(et_param, _product.min_accepting_weight())) { + if (_product.has_accepting_state() && !internal::solver_weight::less(et_param, _product.min_accepting_weight())) { return true; // Early termination } } @@ -310,9 +327,28 @@ namespace pdaaal { for (const auto& [i_to,i_labels] : initial.states()[i_from]->_edges) { for (const auto& [f_to,f_labels] : final.states()[f_from]->_edges) { std::vector labels; - std::set_intersection(i_labels.begin(), i_labels.end(), f_labels.begin(), f_labels.end(), std::back_inserter(labels)); + if constexpr (is_dual && W::is_weight) { + auto first1 = i_labels.begin(); + auto last1 = i_labels.end(); + auto first2 = f_labels.begin(); + auto last2 = f_labels.end(); + while (first1 != last1 && first2 != last2) { + if (first1->first < first2->first) { + ++first1; + } else { + if (first2->first == first1->first) { + auto w = internal::solver_weight::add(first1->second.second, first2->second.second); + labels.emplace_back(first1->first, std::make_pair(first1->second.first, std::move(w))); + ++first1; // *first1 and *first2 are equivalent. + } + ++first2; + } + } + } else { + std::set_intersection(i_labels.begin(), i_labels.end(), f_labels.begin(), f_labels.end(), std::back_inserter(labels)); + } if (!labels.empty() && labels.size() > (labels.back() == epsilon ? 1 : 0)) { - auto [fresh, to_id] = get_product_state(initial.states()[i_to].get(), final.states()[f_to].get()); + auto [fresh, to_id] = get_product_state(initial.states()[i_to].get(), final.states()[f_to].get()); for (const auto& [label, trace] : labels) { if (label != epsilon) { _product.add_edge(top, to_id, label, trace); @@ -325,7 +361,7 @@ namespace pdaaal { auto w_opt = _product.make_back_edge_shortest(top, min_label_it->first, to_id, min_label_it->second.second); assert(!fresh || w_opt); // fresh must imply weight change. if constexpr(ET) { - if (!internal::solver_weight::less(et_param, _product.min_accepting_weight())) { + if (_product.has_accepting_state() && !internal::solver_weight::less(et_param, _product.min_accepting_weight())) { return true; // Early termination } } @@ -347,7 +383,7 @@ namespace pdaaal { } } if constexpr(W::is_weight && trace_type == Trace_Type::Shortest) { - return !internal::solver_weight::less(et_param, _product.min_accepting_weight()); + return _product.has_accepting_state() && !internal::solver_weight::less(et_param, _product.min_accepting_weight()); } else { return _product.has_accepting_state(); } diff --git a/src/include/pdaaal/Solver.h b/src/include/pdaaal/Solver.h index c8510a6..8ab4ed5 100644 --- a/src/include/pdaaal/Solver.h +++ b/src/include/pdaaal/Solver.h @@ -81,23 +81,71 @@ namespace pdaaal { } } - template + template static bool dual_search_accepts(PAutomatonProduct& instance) { if (instance.template initialize_product()) { return true; } - return dual_search(instance.final_automaton(), instance.initial_automaton(), - [&instance](size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace) -> bool { - return instance.add_final_edge(from, label, to, trace); - }, - [&instance](size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace) -> bool { - return instance.add_initial_edge(from, label, to, trace); + // we could *probably* avoid some dupplication here if the pre/post* algorithms + // were refactored into a streamlined structure wrt shortest/not shortest. + if constexpr (trace_type == Trace_Type::Shortest && W::is_weight) + { + /*typename W::type latest_prestar_queue_weight = W::zero(); + typename W::type latest_poststar_queue_weight = W::zero();*/ + return dual_short_search(instance.final_automaton(), instance.initial_automaton(), + [&instance/*,&latest_prestar_queue_weight,&latest_poststar_queue_weight*/] + (size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace, const auto& et_param) -> bool { + /*latest_prestar_queue_weight = et_param; + auto w = internal::solver_weight::add(latest_poststar_queue_weight, latest_prestar_queue_weight);*/ + return instance.template add_final_edge(from, label, to, trace, /*std::move(w)*/ et_param); + }, + [&instance/*,&latest_prestar_queue_weight,&latest_poststar_queue_weight*/] + (size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace, const auto& et_param) -> bool { + /*latest_poststar_queue_weight = et_param; + auto w = internal::solver_weight::add(latest_poststar_queue_weight, latest_prestar_queue_weight);*/ + return instance.template add_initial_edge(from, label, to, trace, /*std::move(w)*/ et_param); + } + ); + return false; + } + else + { + return dual_search(instance.final_automaton(), instance.initial_automaton(), + [&instance](size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace, const auto&) -> bool { + return instance.add_final_edge(from, label, to, trace); + }, + [&instance](size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace) -> bool { + return instance.add_initial_edge(from, label, to, trace); + } + ); + } + } + + template + static bool dual_short_search(internal::PAutomaton &pre_star_automaton, internal::PAutomaton &post_star_automaton, + const internal::early_termination_fn2& pre_star_early_termination, + const internal::early_termination_fn2& post_star_early_termination) { + internal::PreStarSaturation pre_star(pre_star_automaton, pre_star_early_termination); + internal::PostStarShortestSaturation post_star(post_star_automaton, post_star_early_termination); + if constexpr (ET) { + if (pre_star.found() || post_star.found()) return true; + } + while(!pre_star.workset_empty() && !post_star.workset_empty()) { + post_star.step(); + if constexpr (ET) { + if (post_star.found()) return true; } - ); + pre_star.step(); + if constexpr (ET) { + if (pre_star.found()) return true; + } + } + return pre_star.found() || post_star.found(); } + template static bool dual_search(internal::PAutomaton &pre_star_automaton, internal::PAutomaton &post_star_automaton, - const internal::early_termination_fn& pre_star_early_termination, + const internal::early_termination_fn2& pre_star_early_termination, const internal::early_termination_fn& post_star_early_termination) { internal::PreStarSaturation pre_star(pre_star_automaton, pre_star_early_termination); internal::PostStarSaturation post_star(post_star_automaton, post_star_early_termination); @@ -117,38 +165,51 @@ namespace pdaaal { return pre_star.found() || post_star.found(); } - template + template static bool pre_star_accepts(internal::PAutomaton &automaton, size_t state, const std::vector &stack) { if (stack.size() == 1) { auto s_label = stack[0]; - return automaton.accepts(state, stack) || pre_star(automaton, [&automaton, state, s_label](size_t from, uint32_t label, size_t to, internal::edge_annotation_t) -> bool { + return automaton.accepts(state, stack) || + pre_star(automaton, [&automaton, state, s_label](size_t from, uint32_t label, size_t to, internal::edge_annotation_t, const auto&) -> bool { return from == state && label == s_label && automaton.states()[to]->_accepting; }); } else { - return pre_star(automaton) || automaton.accepts(state, stack); + return pre_star(automaton) || automaton.accepts(state, stack); } } - template + template static bool pre_star_accepts(PAutomatonProduct& instance) { instance.enable_pre_star(); return instance.initialize_product() || - pre_star(instance.automaton(), [&instance](size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace) -> bool { - return instance.add_edge_product(from, label, to, trace); + pre_star(instance.automaton(), [&instance](size_t from, uint32_t label, size_t to, internal::edge_annotation_t trace, const auto& et_param) -> bool { + if constexpr (is_weighted && trace_type == Trace_Type::Shortest) + return instance.template add_edge_product(from, label, to, trace, et_param); + else + return instance.add_edge_product(from, label, to, trace); + }); - } + } - template + template static bool pre_star(internal::PAutomaton &automaton, - const internal::early_termination_fn& early_termination = [](size_t, uint32_t, size_t, internal::edge_annotation_t) -> bool { return false; }) { - internal::PreStarSaturation saturation(automaton, early_termination); + const internal::early_termination_fn2& early_termination = [](size_t, uint32_t, size_t, internal::edge_annotation_t, const auto&) -> bool { return false; }) { + if(!is_weighted && trace_type == Trace_Type::Shortest) + throw std::logic_error("Cannot do shortest-trace pre* for PDA without weights."); // TODO: Consider: W=uin32_t, weight==1 as a default weight. + internal::PreStarSaturation saturation(automaton, early_termination); while(!saturation.workset_empty()) { if constexpr (ET) { - if (saturation.found()) return true; + if (saturation.found()) + { + return true; + } } saturation.step(); } - return saturation.found(); + if(saturation.found()) + return true; + else + return false; } template @@ -211,27 +272,47 @@ namespace pdaaal { // TODO: Implement infinite trace structure. return std::make_pair(return_type{}, weight); } else if constexpr (trace_type == Trace_Type::Shortest) { - auto [automaton_path, weight] = instance.template find_path(); + auto [automaton_path, weight] = instance.template find_path(); return std::make_pair(_get_trace(instance.pda(), instance.automaton(), automaton_path), weight); } else { auto automaton_path = instance.template find_path(); return _get_trace(instance.pda(), instance.automaton(), automaton_path); } } - template + template static auto get_trace_dual_search(const PAutomatonProduct& instance) { - auto paths = instance.template find_path(); - using return_type = decltype(_get_trace(instance.pda(), instance.initial_automaton(), std::declval>())); - if (paths.is_null()) { - return return_type{}; + if constexpr (trace_type == Trace_Type::Shortest && W::is_weight) + { + using return_type = decltype(_get_trace(instance.pda(), instance.initial_automaton(), std::declval>())); + auto [paths, weight] = instance.template find_path(); + if (paths.is_null()) { + return std::make_pair(return_type{}, typename W::type {}); + } + auto [i_path, f_path] = paths.split(); + f_path.remove_epsilon(); // post* may add an epsilon-edge as first. this edge is not in pre* automaton (final_automaton), so remove it from f_path. + auto trace1 = _get_trace(instance.pda(), instance.initial_automaton(), i_path); + auto trace2 = _get_trace(instance.pda(), instance.final_automaton(), f_path); + assert(trace1.back()._pdastate == trace2.front()._pdastate); + assert(trace1.back()._stack.size() == trace2.front()._stack.size()); // Should also check == for contents of stack, but T might not implement ==. + trace1.insert(trace1.end(), trace2.begin() + 1, trace2.end()); + return std::make_pair(trace1, weight); + } + else + { + auto paths = instance.template find_path(); + using return_type = decltype(_get_trace(instance.pda(), instance.initial_automaton(), std::declval>())); + if (paths.is_null()) { + return return_type{}; + } + auto [i_path, f_path] = paths.split(); + f_path.remove_epsilon(); // post* may add an epsilon-edge as first. this edge is not in pre* automaton (final_automaton), so remove it from f_path. + auto trace1 = _get_trace(instance.pda(), instance.initial_automaton(), i_path); + auto trace2 = _get_trace(instance.pda(), instance.final_automaton(), f_path); + assert(trace1.back()._pdastate == trace2.front()._pdastate); + assert(trace1.back()._stack.size() == trace2.front()._stack.size()); // Should also check == for contents of stack, but T might not implement ==. + trace1.insert(trace1.end(), trace2.begin() + 1, trace2.end()); + return trace1; } - auto [i_path, f_path] = paths.split(); - auto trace1 = _get_trace(instance.pda(), instance.initial_automaton(), i_path); - auto trace2 = _get_trace(instance.pda(), instance.final_automaton(), f_path); - assert(trace1.back()._pdastate == trace2.front()._pdastate); - assert(trace1.back()._stack.size() == trace2.front()._stack.size()); // Should also check == for contents of stack, but T might not implement ==. - trace1.insert(trace1.end(), trace2.begin() + 1, trace2.end()); - return trace1; } template static auto get_rule_trace_and_paths(const PAutomatonProduct& instance) { @@ -368,7 +449,7 @@ namespace pdaaal { } // The paths was retrieved from the product automaton. First number is the state in initial_automaton, second number is state in final_automaton. auto [initial_automaton_path, final_automaton_path] = paths.value().split(); - + final_automaton_path.remove_epsilon(); // post* may add an epsilon-edge as first. this edge is not in pre* automaton (final_automaton), so remove it from f_path. auto [trace, initial_stack, initial_path] = _get_trace_stack_path(initial_automaton, std::move(initial_automaton_path)); auto [trace2, final_stack, final_path] = _get_trace_stack_path(final_automaton, std::move(final_automaton_path)); // Concat traces diff --git a/src/include/pdaaal/cegar/CegarPdaFactory.h b/src/include/pdaaal/cegar/CegarPdaFactory.h index 4099f5f..df26957 100644 --- a/src/include/pdaaal/cegar/CegarPdaFactory.h +++ b/src/include/pdaaal/cegar/CegarPdaFactory.h @@ -1,14 +1,14 @@ -/* +/* * This program 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. - * + * * This program 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 this program. If not, see . */ @@ -17,7 +17,7 @@ * Copyright Morten K. Schou */ -/* +/* * File: CegarPdaFactory.h * Author: Morten K. Schou * @@ -457,9 +457,9 @@ namespace pdaaal { bool result; if constexpr (use_pre_star) { - result = Solver::pre_star_accepts(*instance); + result = Solver::pre_star_accepts(*instance); } else if constexpr (use_dual_star) { - result = Solver::dual_search_accepts(*instance); + result = Solver::dual_search_accepts(*instance); } else { result = Solver::post_star_accepts(*instance); } diff --git a/src/include/pdaaal/internal/PAutomaton.h b/src/include/pdaaal/internal/PAutomaton.h index e2320e7..1e765f1 100644 --- a/src/include/pdaaal/internal/PAutomaton.h +++ b/src/include/pdaaal/internal/PAutomaton.h @@ -96,6 +96,10 @@ namespace pdaaal::internal { friend constexpr bool operator!=(const trace_t& l, const trace_t& r) { return !(l == r); } + + friend constexpr bool operator<(const trace_t& l, const trace_t& r) { + return std::tie(l._state, l._rule_id, l._label) < std::tie(r._state, r._rule_id, r._label); + } }; template struct TraceInfo {}; @@ -232,8 +236,25 @@ namespace pdaaal::internal { } } + template + bool has_negative_weights(const C& comp) const { + if constexpr (is_weighted && W::is_signed) + { + for (const auto& from : states()) { + for (const auto& [to,labels] : from->_edges) { + for (const auto& [label,trace] : labels) { + if (comp(trace.second, W::zero())) { + return true; + } + } + } + } + } + return false; + } + [[nodiscard]] const std::vector>& states() const { return _states; } - + [[nodiscard]] const PDA& pda() const { return _pda; } void or_extend(PAutomaton&& other) { @@ -410,11 +431,14 @@ namespace pdaaal::internal { return automaton_path_t(); } - [[nodiscard]] auto find_path_shortest() const { return find_path_shortest([](size_t s){ return s; }); } - template [[nodiscard]] auto find_path_shortest(Fn&& state_map) const { + template + [[nodiscard]] auto find_path_shortest() const { return find_path_shortest([](size_t s){ return s; }); } + + template + [[nodiscard]] auto find_path_shortest(Fn&& state_map) const { using path_state = decltype(std::declval()(std::declval())); static_assert(std::is_convertible_v>); - using automaton_path_t = decltype(AutomatonPath(std::declval())); + using automaton_path_t = decltype(AutomatonPath(std::declval())); if constexpr (is_weighted) { // TODO: Consider unweighted shortest path. // Dijkstra. @@ -443,7 +467,7 @@ namespace pdaaal::internal { search_queue.pop(); if (_states[current.state]->_accepting) { - AutomatonPath automaton_path(state_map(current.state)); + AutomatonPath automaton_path(state_map(current.state)); const queue_elem* p = ¤t; while (p->back_pointer != nullptr) { auto label = p->label; @@ -649,14 +673,17 @@ namespace pdaaal::internal { } } - [[nodiscard]] auto get_path_shortest() const { return get_path_shortest([](size_t s){ return s; }); } - template [[nodiscard]] auto get_path_shortest(Fn&& state_map) const { + template + [[nodiscard]] auto get_path_shortest() const { return get_path_shortest([](size_t s){ return s; }); } + + template [[nodiscard]] + auto get_path_shortest(Fn&& state_map) const { if constexpr (W::is_weight) { - if (_accepting.empty()) return std::make_tuple(AutomatonPath(), solver_weight::max()); + if (_accepting.empty()) return std::make_tuple(AutomatonPath(), solver_weight::max()); auto best_accept_state = *std::min_element(_accepting.begin(), _accepting.end(), [](const auto& a, const auto& b){ return solver_weight::less(a->_best_weight, b->_best_weight); }); - AutomatonPath automaton_path(state_map(best_accept_state->_id)); + AutomatonPath automaton_path(state_map(best_accept_state->_id)); const state_t* p = best_accept_state; while (p->_back_edge_state != std::numeric_limits::max()) { auto label = p->_back_edge_label; diff --git a/src/include/pdaaal/internal/PDA.h b/src/include/pdaaal/internal/PDA.h index 68c6d5c..1f0f8c3 100644 --- a/src/include/pdaaal/internal/PDA.h +++ b/src/include/pdaaal/internal/PDA.h @@ -221,7 +221,20 @@ namespace pdaaal::internal { fut::vector_set _pre_states; explicit state_t(typename PDA::state_t&& other_state) : _rules(std::move(other_state._rules)), _pre_states(std::move(other_state._pre_states)) {} + state_t() = default; + + template + bool has_negative_weight(const C& comp) const { + if constexpr (has_weight && W::is_signed) { + for (const auto& [rule,labels] : _rules) { + if (comp(rule._weight, W::zero())) { + return true; + } + } + } + return false; + } }; public: @@ -233,6 +246,15 @@ namespace pdaaal::internal { auto states_begin() noexcept { return _states.begin(); } auto states_end() noexcept { return _states.end(); } + template + bool has_negative_weight(const C& comp) const { + if constexpr (has_weight && W::is_signed) + for (const auto& s : _states) + if(s.has_negative_weight(comp)) + return true; + return false; + } + [[nodiscard]] virtual size_t number_of_labels() const = 0; const std::vector& states() const { return _states; diff --git a/src/include/pdaaal/internal/PdaSaturation.h b/src/include/pdaaal/internal/PdaSaturation.h index f3fa37c..37a28ca 100644 --- a/src/include/pdaaal/internal/PdaSaturation.h +++ b/src/include/pdaaal/internal/PdaSaturation.h @@ -1,14 +1,14 @@ -/* +/* * This program 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. - * + * * This program 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 this program. If not, see . */ @@ -17,7 +17,7 @@ * Copyright Morten K. Schou */ -/* +/* * File: PdaSaturation.h * Author: Morten K. Schou * @@ -62,91 +62,206 @@ namespace pdaaal::internal { template using early_termination_fn2 = std::function,std::conditional_t const&)>; - template + template class PreStarSaturation { + private: + using weight_t = std::conditional_t; + using solver_weight = min_weight; + + struct weighted_edge_t : public temp_edge_t { // maybe reuse for poststar? + weighted_edge_t(size_t from, uint32_t label, size_t to, weight_t&& weight, trace_t trace) + : temp_edge_t(from, label, to), _weight(std::move(weight)), _trace(trace) {} + weight_t _weight; + trace_t _trace; + }; + + struct weighted_edge_t_comp { + bool operator()(const weighted_edge_t &lhs, const weighted_edge_t &rhs){ + if constexpr (W::is_weight) return solver_weight::less(rhs._weight, lhs._weight); + else return false; + } + }; + + static inline const weight_t& get_weight(const pda_rule_t& rule) { + static const int dummy = 1; + if constexpr(W::is_weight) return rule._weight; + else return dummy; + } + + using trace_info = TraceInfo; using edge_anno = edge_annotation; using edge_anno_t = edge_annotation_t; using p_automaton_t = PAutomaton; + using edge_t = std::conditional_t; + using workset_t = std::conditional_t,weighted_edge_t_comp>, + std::stack + >; + public: - explicit PreStarSaturation(PAutomaton &automaton, const early_termination_fn& early_termination = [](size_t, uint32_t, size_t, edge_anno_t) -> bool { return false; }) + explicit PreStarSaturation(PAutomaton &automaton, const early_termination_fn2& early_termination) : _automaton(automaton), _early_termination(early_termination), _pda_states(_automaton.pda().states()), _n_pda_states(_pda_states.size()), _n_automaton_states(_automaton.states().size()), - _n_pda_labels(_automaton.number_of_labels()), _rel(_n_automaton_states), _delta_prime(_n_automaton_states) { + _n_pda_labels(_automaton.number_of_labels()), _rel(_n_automaton_states), + _delta_prime(_n_automaton_states),_popped(_n_pda_states) { initialize(); }; - private: // This is an implementation of Algorithm 1 (figure 3.3) in: // Schwoon, Stefan. Model-checking pushdown systems. 2002. PhD Thesis. Technische Universität München. // http://www.lsv.fr/Publis/PAPERS/PDF/schwoon-phd02.pdf (page 42) p_automaton_t& _automaton; - const early_termination_fn& _early_termination; + const early_termination_fn2& _early_termination; const std::vector::state_t>& _pda_states; const size_t _n_pda_states; const size_t _n_automaton_states; const size_t _n_pda_labels; - std::stack _workset; + workset_t _workset; std::vector>> _rel; std::vector>> _delta_prime; bool _found = false; + std::vector _minpath; + std::vector _popped; + + bool has_negative_weight() const { + if constexpr (W::is_signed) { + for (const auto& state : _pda_states) + if(state.has_negative_weight(solver_weight::less)) return true; + if(_automaton.has_negative_weights(solver_weight::less)) return true; + } + return false; + } + + void add_pop(size_t state) { + if(state >= _n_pda_states) return; + if(_popped[state]) return; + for (auto pre_state : _pda_states[state]._pre_states) { + const auto& rules = _pda_states[pre_state]._rules; + auto lb = rules.lower_bound(pda_rule_t{state}); + while (lb != rules.end() && lb->first._to == state) { + const auto& [rule, labels] = *lb; + size_t rule_id = lb - rules.begin(); + ++lb; + if(rule._operation == POP) + { + if constexpr (W::is_weight && SHORTEST) + insert_edge_bulk(pre_state, labels, state, p_automaton_t::new_pre_trace(rule_id), rule._weight); + else + insert_edge_bulk(pre_state, labels, state, p_automaton_t::new_pre_trace(rule_id), weight_t{}); + } + } + } + _popped[state] = true; + } void initialize() { + if constexpr (SHORTEST && W::is_weight) { + _minpath.resize(_automaton.states().size()); + std::fill(_minpath.begin(), _minpath.end(), solver_weight::max()); + } + // workset := ->_0 (line 1) for (const auto& from : _automaton.states()) { for (const auto& [to, labels] : from->_edges) { for (const auto& [label, _] : labels) { - _workset.emplace(from->_id, label, to); + if constexpr (W::is_weight && SHORTEST) { + // anything inside the automaton is reachable with weight zero. + _minpath[from->_id] = solver_weight::zero(); + _minpath[to] = solver_weight::zero(); + _workset.emplace(from->_id, label, to, solver_weight::zero(), trace_t()); + } else if constexpr (!SHORTEST) { + _workset.emplace(from->_id, label, to); + } else throw std::logic_error("Shortest traces for void-weights is not supported."); } } + if(from->_accepting) add_pop(from->_id); } + } - // for all --> : workset U= (p, y, p') (line 2) - for (size_t state = 0; state < _n_pda_states; ++state) { - size_t rule_id = 0; - for (const auto& [rule, labels] : _pda_states[state]._rules) { - if (rule._operation == POP) { - insert_edge_bulk(state, labels, rule._to, p_automaton_t::new_pre_trace(rule_id)); + + void insert_edge(size_t from, uint32_t label, size_t to, trace_t trace, [[maybe_unused]] weight_t weight) { + + if constexpr (SHORTEST && W::is_weight) { + auto res = solver_weight::add(weight, _minpath[to]); + assert(res != solver_weight::max()); + assert(weight != solver_weight::max()); + + auto [it, fresh] = _automaton.emplace_edge(from, label, to, std::make_pair(trace, weight)); + if (fresh) { // New edge is not already in edges (rel U workset). + if(solver_weight::less(res, _minpath[from])) _minpath[from] = res; + _workset.emplace(from, label, to, std::move(res), trace); + } else { + if(solver_weight::less(weight, it->second.second)) { + it->second.second = std::move(weight); + _workset.emplace(from, label, to, std::move(res), trace); } - ++rule_id; } - } - } - void insert_edge(size_t from, uint32_t label, size_t to, trace_t trace) { - if (_automaton.emplace_edge(from, label, to, edge_anno::from_trace_info(trace)).second) { // New edge is not already in edges (rel U workset). - _workset.emplace(from, label, to); - if constexpr (ET) { - _found = _found || _early_termination(from, label, to, edge_anno::from_trace_info(trace)); + } else { + if (_automaton.emplace_edge(from, label, to, edge_anno::from_trace_info(trace)).second) { + _workset.emplace(from, label, to); + if constexpr (ET) { + _found = _found || _early_termination(from, label, to, edge_anno::from_trace_info(trace), weight_t{}); + } } } - }; - void insert_edge_bulk(size_t from, const labels_t& labels, size_t to, trace_t trace) { + } + + void insert_edge_bulk(size_t from, const labels_t& labels, size_t to, trace_t trace, weight_t weight) { if (labels.wildcard()) { for (uint32_t i = 0; i < _n_pda_labels; i++) { - insert_edge(from, i, to, trace); + insert_edge(from, i, to, trace, weight); } } else { for (auto label : labels.labels()) { - insert_edge(from, label, to, trace); + insert_edge(from, label, to, trace, weight); } } - }; + } + + weight_t get_pautomata_edge_weight(auto from, auto label, auto to) + { + if constexpr (ET && W::is_weight) + return _automaton.get_edge(from, label, to)->second; + return weight_t{}; + } + public: + void step() { // pop t = (q, y, q') from workset (line 4) auto t = _workset.top(); _workset.pop(); + + [[maybe_unused]] const auto w = get_pautomata_edge_weight(t._from, t._label, t._to); + + if constexpr (SHORTEST && W::is_weight) { + assert(t._weight != solver_weight::max()); + if(!_popped[t._from]) + _minpath[t._from] = t._weight; + if(solver_weight::less(solver_weight::add(w, _minpath[t._to]), t._weight)) + return; + if constexpr (ET) { + _found = _early_termination(t._from, t._label, t._to, std::make_pair(t._trace, w), t._weight) || _found; + } + } // rel = rel U {t} (line 6) (membership test on line 5 is done in insert_edge). _rel[t._from].emplace_back(t._to, t._label); - // (line 7-8 for \Delta') for (const auto& [state, rule_id] : _delta_prime[t._from]) { // Loop over delta_prime (that match with t->from) - if (_pda_states[state]._rules[rule_id].second.contains(t._label)) { - insert_edge(state, t._label, t._to, p_automaton_t::new_pre_trace(rule_id, t._from)); + auto& [rule, labels] = _pda_states[state]._rules[rule_id]; + if (labels.contains(t._label)) { + if constexpr (W::is_weight && SHORTEST) { + auto nw = solver_weight::add(solver_weight::add(rule._weight, _automaton.get_edge(rule._to, rule._op_label, t._from)->second), w); + insert_edge(state, t._label, t._to, p_automaton_t::new_pre_trace(rule_id, t._from), nw); + } else { + insert_edge(state, t._label, t._to, p_automaton_t::new_pre_trace(rule_id, t._from), weight_t{}); + } } } + // Loop over \Delta (filter rules going into q) (line 7 and 9) if (t._from >= _n_pda_states) { return; } for (auto pre_state : _pda_states[t._from]._pre_states) { @@ -158,15 +273,28 @@ namespace pdaaal::internal { ++lb; switch (rule._operation) { case POP: + // check if weight is lower here, maybe? + if (!_popped[t._from]) { + if constexpr (W::is_weight && SHORTEST) + insert_edge_bulk(pre_state, labels, t._from, p_automaton_t::new_pre_trace(rule_id), rule._weight); + else + insert_edge_bulk(pre_state, labels, t._from, p_automaton_t::new_pre_trace(rule_id), weight_t{}); + } break; case SWAP: // (line 7-8 for \Delta) if (rule._op_label == t._label) { - insert_edge_bulk(pre_state, labels, t._to, p_automaton_t::new_pre_trace(rule_id)); + if constexpr (W::is_weight && SHORTEST) + insert_edge_bulk(pre_state, labels, t._to, p_automaton_t::new_pre_trace(rule_id), solver_weight::add(w, rule._weight)); + else + insert_edge_bulk(pre_state, labels, t._to, p_automaton_t::new_pre_trace(rule_id), weight_t{}); } break; case NOOP: // (line 7-8 for \Delta) if (labels.contains(t._label)) { - insert_edge(pre_state, t._label, t._to, p_automaton_t::new_pre_trace(rule_id)); + if constexpr (W::is_weight && SHORTEST) + insert_edge(pre_state, t._label, t._to, p_automaton_t::new_pre_trace(rule_id), solver_weight::add(w, rule._weight)); + else + insert_edge(pre_state, t._label, t._to, p_automaton_t::new_pre_trace(rule_id), weight_t{}); } break; case PUSH: // (line 9) @@ -175,7 +303,11 @@ namespace pdaaal::internal { _delta_prime[t._to].emplace_back(pre_state, rule_id); for (const auto& [to, label] : _rel[t._to]) { // (line 11-12) if (labels.contains(label)) { - insert_edge(pre_state, label, to, p_automaton_t::new_pre_trace(rule_id, t._to)); + if constexpr (W::is_weight && SHORTEST) { + auto nw = solver_weight::add(solver_weight::add(_automaton.get_edge(t._to, label, to)->second, w), rule._weight); + insert_edge(pre_state, label, to, p_automaton_t::new_pre_trace(rule_id, t._to), nw); + } else + insert_edge(pre_state, label, to, p_automaton_t::new_pre_trace(rule_id, t._to), weight_t{}); } } } @@ -185,10 +317,20 @@ namespace pdaaal::internal { } } } + _popped[t._from] = true; + + if constexpr (ET && SHORTEST && W::is_weight) + { + // flush the solution in case we got a trace, but the intersection has no trace shorter than the "longest shortest trace" in the pautomata + if(workset_empty()) + _found = _early_termination(t._from, t._label, t._to, std::make_pair(t._trace, w), solver_weight::max()); + } } + [[nodiscard]] bool workset_empty() const { return _workset.empty(); } + [[nodiscard]] bool found() const { return _found; } @@ -401,22 +543,9 @@ namespace pdaaal::internal { bool has_negative_weight() const { if constexpr (W::is_signed) { - for (const auto& state : _pda_states) { - for (const auto& [rule,labels] : state._rules) { - if (solver_weight::less(rule._weight, W::zero())) { - return true; - } - } - } - for (const auto& from : _automaton.states()) { - for (const auto& [to,labels] : from->_edges) { - for (const auto& [label,trace] : labels) { - if (solver_weight::less(trace.second, W::zero())) { - return true; - } - } - } - } + for (const auto& state : _pda_states) + if(state.has_negative_weight(solver_weight::less)) return true; + if(_automaton.has_negative_weights(solver_weight::less)) return true; } return false; } diff --git a/src/pdaaal-bin/Verifier.h b/src/pdaaal-bin/Verifier.h index a97e59e..8c9cd57 100644 --- a/src/pdaaal-bin/Verifier.h +++ b/src/pdaaal-bin/Verifier.h @@ -1,14 +1,14 @@ -/* +/* * This program 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. - * + * * This program 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 this program. If not, see . */ @@ -17,7 +17,7 @@ * Copyright Morten K. Schou */ -/* +/* * File: Verifier.h * Author: Morten K. Schou * @@ -135,17 +135,29 @@ namespace pdaaal { case 2: { switch (trace_type) { case Trace_Type::None: - result = Solver::pre_star_accepts(instance); + result = Solver::pre_star_accepts(instance); break; case Trace_Type::Any: - result = Solver::pre_star_accepts(instance); + result = Solver::pre_star_accepts(instance); if (result) { trace = Solver::get_trace(instance); } break; case Trace_Type::Shortest: - assert(false); - throw std::runtime_error("Cannot use shortest trace, not implemented for pre* engine."); + if constexpr(pda_t::has_weight) { + result = Solver::pre_star_accepts(instance); + //instance. template product_automaton_to_dot(std::cerr); + //std::cerr << std::endl; + if (result) { + typename pda_t::weight_type weight; + std::tie(trace, weight) = Solver::get_trace(instance); + reachability_time.stop(); // We don't want to include time for output in reachability_time. + json_out.entry("weight", weight); + } + } else { + assert(false); + throw std::runtime_error("Cannot use shortest trace option for unweighted PDA."); + } break; case Trace_Type::Longest: case Trace_Type::ShortestFixedPoint: @@ -158,17 +170,27 @@ namespace pdaaal { case 3: { switch (trace_type) { case Trace_Type::None: - result = Solver::dual_search_accepts(instance); + result = Solver::dual_search_accepts(instance); break; case Trace_Type::Any: - result = Solver::dual_search_accepts(instance); + result = Solver::dual_search_accepts(instance); if (result) { trace = Solver::get_trace_dual_search(instance); } break; case Trace_Type::Shortest: - assert(false); - throw std::runtime_error("Cannot use shortest trace, not implemented for dual* engine."); + if constexpr(pda_t::has_weight) { + result = Solver::dual_search_accepts(instance); + if (result) { + typename pda_t::weight_type weight; + std::tie(trace, weight) = Solver::get_trace_dual_search(instance); + reachability_time.stop(); // We don't want to include time for output in reachability_time + json_out.entry("weight", weight); + } + } else { + assert(false); + throw std::runtime_error("Cannot use shortest trace option for unweighted PDA."); + } break; case Trace_Type::Longest: case Trace_Type::ShortestFixedPoint: diff --git a/test/PAutomaton_test.cpp b/test/PAutomaton_test.cpp index 7baa4f4..8bbfc21 100644 --- a/test/PAutomaton_test.cpp +++ b/test/PAutomaton_test.cpp @@ -82,7 +82,7 @@ BOOST_AUTO_TEST_CASE(UnweightedPreStar) std::vector init_stack{'A', 'A'}; internal::PAutomaton automaton(pda, 0, pda.encode_pre(init_stack)); - Solver::pre_star(automaton); + Solver::pre_star(automaton); std::vector test_stack_reachable{'C', 'B', 'B', 'A'}; BOOST_CHECK_EQUAL(automaton.accepts(2, pda.encode_pre(test_stack_reachable)), true); @@ -158,7 +158,7 @@ BOOST_AUTO_TEST_CASE(WeightedPreStar) std::vector init_stack{'A', 'A'}; internal::PAutomaton automaton(pda, 0, pda.encode_pre(init_stack)); - Solver::pre_star(automaton); + Solver::pre_star(automaton); std::vector test_stack_reachable{'C', 'B', 'B', 'A'}; BOOST_CHECK_EQUAL(automaton.accepts(2, pda.encode_pre(test_stack_reachable)), true); diff --git a/test/ParsingPDAFactory_test.cpp b/test/ParsingPDAFactory_test.cpp index 514e7f1..7df40f8 100644 --- a/test/ParsingPDAFactory_test.cpp +++ b/test/ParsingPDAFactory_test.cpp @@ -1,14 +1,14 @@ -/* +/* * This program 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. - * + * * This program 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 this program. If not, see . */ @@ -17,7 +17,7 @@ * Copyright Morten K. Schou */ -/* +/* * File: ParsingPDAFactory_test.cpp * Author: Morten K. Schou * @@ -460,7 +460,7 @@ A,B auto instance = factory.compile(initial, final); - bool result = Solver::dual_search_accepts(*instance); + bool result = Solver::dual_search_accepts(*instance); BOOST_CHECK(result); auto trace = Solver::get_trace_dual_search(*instance); diff --git a/test/Solver_test.cpp b/test/Solver_test.cpp index 71045f3..14733cf 100644 --- a/test/Solver_test.cpp +++ b/test/Solver_test.cpp @@ -144,8 +144,8 @@ BOOST_AUTO_TEST_CASE(EarlyTerminationPreStar) internal::PAutomaton automaton(pda, 1, pda.encode_pre(init_stack)); std::vector test_stack_reachable{'A'}; - auto result = Solver::pre_star_accepts(automaton, 0, pda.encode_pre(test_stack_reachable)); - BOOST_CHECK_EQUAL(result, true); + auto result = Solver::pre_star_accepts(automaton, 0, pda.encode_pre(test_stack_reachable)); + BOOST_REQUIRE_EQUAL(result, true); auto trace = Solver::get_trace(pda, automaton, 0, test_stack_reachable); BOOST_CHECK_EQUAL(trace.size(), 12); @@ -201,7 +201,7 @@ BOOST_AUTO_TEST_CASE(Pre_0AApop1A) std::vector final_states{1}; PAutomatonProduct instance(pda, initial_nfa, initial_states, final_nfa, final_states); - bool result = Solver::pre_star_accepts(instance); + bool result = Solver::pre_star_accepts(instance); BOOST_CHECK(result); auto trace = Solver::get_trace(instance); BOOST_CHECK_EQUAL(trace.size(), 2); @@ -219,7 +219,7 @@ BOOST_AUTO_TEST_CASE(Pre_0Apop1) std::vector final_states{1}; PAutomatonProduct instance(pda, initial_nfa, initial_states, final_nfa, final_states); - bool result = Solver::pre_star_accepts(instance); + bool result = Solver::pre_star_accepts(instance); BOOST_CHECK(result); auto trace = Solver::get_trace(instance); BOOST_CHECK_EQUAL(trace.size(), 2); @@ -238,7 +238,7 @@ BOOST_AUTO_TEST_CASE(Pre_0AApop0) std::vector final_states{0}; PAutomatonProduct instance(pda, initial_nfa, initial_states, final_nfa, final_states); - bool result = Solver::pre_star_accepts(instance); + bool result = Solver::pre_star_accepts(instance); BOOST_CHECK(result); auto trace = Solver::get_trace(instance); BOOST_CHECK_EQUAL(trace.size(), 3); @@ -258,7 +258,7 @@ BOOST_AUTO_TEST_CASE(Pre_0AApop0A) std::vector final_states{0}; PAutomatonProduct instance(pda, initial_nfa, initial_states, final_nfa, final_states); - bool result = Solver::pre_star_accepts(instance); + bool result = Solver::pre_star_accepts(instance); BOOST_CHECK(result); auto trace = Solver::get_trace(instance); BOOST_CHECK_EQUAL(trace.size(), 3); diff --git a/test/Verification_test.cpp b/test/Verification_test.cpp index ab54423..17a898b 100644 --- a/test/Verification_test.cpp +++ b/test/Verification_test.cpp @@ -1,14 +1,14 @@ -/* +/* * This program 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. - * + * * This program 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 this program. If not, see . */ @@ -17,7 +17,7 @@ * Copyright Morten K. Schou */ -/* +/* * File: Verification_test * Author: Morten K. Schou * @@ -120,22 +120,62 @@ BOOST_AUTO_TEST_CASE(Verification_Test_1) } } })"); - auto pda = PdaJsonParser::parse,true>(pda_stream, std::cerr); - auto initial_p_automaton = PAutomatonParser::parse_string("< [Zero, One] , ([A]?[B])* >", pda); - auto final_p_automaton = PAutomatonParser::parse_string("< [Two] , [B] [B] [B] >", pda); - PAutomatonProduct instance(pda, std::move(initial_p_automaton), std::move(final_p_automaton)); + { + auto pda = PdaJsonParser::parse,true>(pda_stream, std::cerr); + auto initial_p_automaton = PAutomatonParser::parse_string("< [Zero, One] , ([A]?[B])* >", pda); + auto final_p_automaton = PAutomatonParser::parse_string("< [Two] , [B] [B] [B] >", pda); + PAutomatonProduct instance(pda, std::move(initial_p_automaton), std::move(final_p_automaton)); - bool result = Solver::post_star_accepts(instance); + bool result = Solver::post_star_accepts(instance); - BOOST_TEST(result); + BOOST_TEST(result); - auto [trace, weight] = Solver::get_trace(instance); + auto [trace, weight] = Solver::get_trace(instance); - BOOST_CHECK_EQUAL(weight, 1); - BOOST_CHECK_EQUAL(trace.size(), 2); + BOOST_CHECK_EQUAL(weight, 1); + BOOST_CHECK_EQUAL(trace.size(), 2); + + std::cout << "Weight: " << weight << std::endl; + print_trace(trace, pda); + } + pda_stream.seekg(0); + { + auto pda = PdaJsonParser::parse,true>(pda_stream, std::cerr); + auto initial_p_automaton = PAutomatonParser::parse_string("< [Zero, One] , ([A]?[B])* >", pda); + auto final_p_automaton = PAutomatonParser::parse_string("< [Two] , [B] [B] [B] >", pda); + PAutomatonProduct instance(pda, std::move(initial_p_automaton), std::move(final_p_automaton)); + + bool result = Solver::pre_star_accepts(instance); + + BOOST_TEST(result); + + auto [trace, weight] = Solver::get_trace(instance); + + BOOST_CHECK_EQUAL(weight, 1); + BOOST_CHECK_EQUAL(trace.size(), 2); + + std::cout << "Weight: " << weight << std::endl; + print_trace(trace, pda); + } + pda_stream.seekg(0); + { + auto pda = PdaJsonParser::parse,true>(pda_stream, std::cerr); + auto initial_p_automaton = PAutomatonParser::parse_string("< [Zero, One] , ([A]?[B])* >", pda); + auto final_p_automaton = PAutomatonParser::parse_string("< [Two] , [B] [B] [B] >", pda); + PAutomatonProduct instance(pda, std::move(initial_p_automaton), std::move(final_p_automaton)); + + bool result = Solver::dual_search_accepts(instance); - std::cout << "Weight: " << weight << std::endl; - print_trace(trace, pda); + BOOST_TEST(result); + + auto [trace, weight] = Solver::get_trace_dual_search(instance); + + BOOST_CHECK_EQUAL(weight, 1); + BOOST_CHECK_EQUAL(trace.size(), 2); + + std::cout << "Weight: " << weight << std::endl; + print_trace(trace, pda); + } } BOOST_AUTO_TEST_CASE(Verification_negative_weight_test) @@ -894,19 +934,41 @@ BOOST_AUTO_TEST_CASE(Verification_shortest_trace_test) "edges": [[0,"B",3], [3,"A",3], [3,"B",3]] } })"); - auto pda = PdaJsonParser::parse,false>(pda_stream, std::cerr); - auto p_automaton_i = PAutomatonJsonParser::parse(initial_stream, pda); - auto p_automaton_f = PAutomatonJsonParser::parse(final_stream, pda); - PAutomatonProduct instance(pda, std::move(p_automaton_i), std::move(p_automaton_f)); - bool result = Solver::post_star_accepts(instance); - BOOST_TEST(result); - auto [path,weight] = instance.template find_path(); - BOOST_CHECK_EQUAL(weight, 0); - - std::stringstream s; - print_automaton(instance.product_automaton(), pda, s); - s << std::endl; - print_automaton(instance.automaton(), pda, s); - s << std::endl; - BOOST_TEST_MESSAGE(s.str()); + { + auto pda = PdaJsonParser::parse,false>(pda_stream, std::cerr); + auto p_automaton_i = PAutomatonJsonParser::parse(initial_stream, pda); + auto p_automaton_f = PAutomatonJsonParser::parse(final_stream, pda); + PAutomatonProduct instance(pda, std::move(p_automaton_i), std::move(p_automaton_f)); + bool result = Solver::post_star_accepts(instance); + BOOST_TEST(result); + auto [path,weight] = instance.template find_path(); + BOOST_CHECK_EQUAL(weight, 0); + + std::stringstream s; + print_automaton(instance.product_automaton(), pda, s); + s << std::endl; + print_automaton(instance.automaton(), pda, s); + s << std::endl; + BOOST_TEST_MESSAGE(s.str()); + } + initial_stream.seekg(0); + final_stream.seekg(0); + pda_stream.seekg(0); + { + auto pda = PdaJsonParser::parse,false>(pda_stream, std::cerr); + auto p_automaton_i = PAutomatonJsonParser::parse(initial_stream, pda); + auto p_automaton_f = PAutomatonJsonParser::parse(final_stream, pda); + PAutomatonProduct instance(pda, std::move(p_automaton_i), std::move(p_automaton_f)); + bool result = Solver::pre_star_accepts(instance); + BOOST_TEST(result); + auto [path,weight] = instance.template find_path(); + BOOST_CHECK_EQUAL(weight, 0); + + std::stringstream s; + print_automaton(instance.product_automaton(), pda, s); + s << std::endl; + print_automaton(instance.automaton(), pda, s); + s << std::endl; + BOOST_TEST_MESSAGE(s.str()); + } }