diff --git a/src/pdaaal/CegarPdaFactory.h b/src/pdaaal/CegarPdaFactory.h index 2eb186b..f003e66 100644 --- a/src/pdaaal/CegarPdaFactory.h +++ b/src/pdaaal/CegarPdaFactory.h @@ -126,6 +126,7 @@ namespace pdaaal { CegarPdaReconstruction(const solver_instance_t& instance, const NFA& initial_headers, const NFA& final_headers) : _instance(instance), _initial_nfa(initial_headers), _final_nfa(final_headers) {}; + template std::variant @@ -137,7 +138,7 @@ namespace pdaaal { size_t init_state; std::vector> trace; std::vector initial_path, final_path; - std::tie(init_state, trace, _initial_abstract_stack, _final_abstract_stack, initial_path, final_path) = Solver::get_rule_trace_and_paths(_instance); + std::tie(init_state, trace, _initial_abstract_stack, _final_abstract_stack, initial_path, final_path) = Solver::get_rule_trace_and_paths(_instance); assert(init_state != std::numeric_limits::max()); // Assume that a trace exists (otherwise don't call this function!) auto build_nfa_path = [](const automaton_t& automaton, const std::vector& path) -> std::vector { @@ -448,7 +449,7 @@ namespace pdaaal { using refinement_t = typename Reconstruction::refinement_t; using header_refinement_t = typename Reconstruction::header_refinement_t; public: - template + template std::optional cegar_solve(Factory&& factory, const NFA& initial_headers, const NFA& final_headers) { while(true) { auto instance = factory.compile(initial_headers, final_headers); @@ -456,6 +457,8 @@ namespace pdaaal { bool result; if constexpr (use_pre_star) { result = Solver::pre_star_accepts(instance); + } else if constexpr (use_dual_star) { + result = Solver::dual_search_accepts(instance); } else { result = Solver::post_star_accepts(instance); } @@ -465,7 +468,7 @@ namespace pdaaal { Reconstruction reconstruction(factory, instance, initial_headers, final_headers); - auto res = reconstruction.reconstruct_trace(); + auto res = reconstruction.template reconstruct_trace(); if (std::holds_alternative(res)) { return std::get(res); diff --git a/src/pdaaal/Solver.h b/src/pdaaal/Solver.h index c8d090b..e9a5ceb 100644 --- a/src/pdaaal/Solver.h +++ b/src/pdaaal/Solver.h @@ -33,10 +33,8 @@ namespace pdaaal { - - class Solver { - private: - static constexpr auto epsilon = std::numeric_limits::max(); + namespace details { + constexpr auto epsilon = std::numeric_limits::max(); struct temp_edge_t { size_t _from = std::numeric_limits::max(); @@ -74,61 +72,71 @@ namespace pdaaal { }; template - using early_termination_fn = std::function trace)>; - - public: - - template - static bool pre_star_accepts(PAutomaton &automaton, size_t state, const std::vector &stack) { - if (stack.size() == 1) { - auto s_label = stack[0]; - return pre_star(automaton, [&automaton, state, s_label](size_t from, uint32_t label, size_t to, trace_ptr trace) -> bool { - return from == state && label == s_label && automaton.states()[to]->_accepting; - }); - } else { - return pre_star(automaton) || automaton.accepts(state, stack); - } - } - - template - static bool pre_star_accepts(SolverInstance_impl& instance) { - instance.enable_pre_star(); - return instance.initialize_product() || - pre_star(instance.automaton(), [&instance](size_t from, uint32_t label, size_t to, trace_ptr trace) -> bool { - return instance.add_edge_product(from, label, to, trace); - }); - } + using early_termination_fn = std::function)>; template - static bool pre_star(PAutomaton &automaton, const early_termination_fn& early_termination = [](size_t f, uint32_t l, size_t t, trace_ptr trace) -> bool { return false; }) { + class PreStarSaturation { + public: + explicit PreStarSaturation(PAutomaton &automaton, const early_termination_fn& early_termination = [](size_t f, uint32_t l, size_t t, trace_ptr trace) -> bool { return false; }) + : _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) { + 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) - const auto& pda_states = automaton.pda().states(); - const auto n_pda_states = pda_states.size(); - const auto n_automaton_states = automaton.states().size(); - std::unordered_set edges; - std::stack workset; - std::vector>> rel(n_automaton_states); + PAutomaton& _automaton; + const early_termination_fn& _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::unordered_set _edges; + std::stack _workset; + std::vector>> _rel; + std::vector>> _delta_prime; + bool _found = false; + + void initialize() { + // workset := ->_0 (line 1) + for (const auto &from : _automaton.states()) { + for (const auto &[to,labels] : from->_edges) { + for (const auto &[label,_] : labels) { + insert_edge(from->_id, label, to, nullptr); + } + } + } - bool found = false; - const auto insert_edge = [&found, &early_termination, &edges, &workset, &automaton](size_t from, uint32_t label, size_t to, const trace_t *trace) { - auto res = edges.emplace(from, label, to); + // 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, _automaton.new_pre_trace(rule_id)); + } + ++rule_id; + } + } + } + void insert_edge(size_t from, uint32_t label, size_t to, const trace_t *trace) { + auto res = _edges.emplace(from, label, to); if (res.second) { // New edge is not already in edges (rel U workset). - workset.emplace(from, label, to); + _workset.emplace(from, label, to); if (trace != nullptr) { // Don't add existing edges if constexpr (ET) { - found = found || early_termination(from, label, to, trace_ptr_from(trace)); + _found = _found || _early_termination(from, label, to, trace_ptr_from(trace)); } - automaton.add_edge(from, to, label, trace_ptr_from(trace)); + _automaton.add_edge(from, to, label, trace_ptr_from(trace)); } } }; - const auto n_pda_labels = automaton.number_of_labels(); - const auto insert_edge_bulk = [&insert_edge, n_pda_labels](size_t from, const labels_t &precondition, size_t to, const trace_t *trace) { + void insert_edge_bulk(size_t from, const labels_t &precondition, size_t to, const trace_t *trace) { if (precondition.wildcard()) { - for (uint32_t i = 0; i < n_pda_labels; i++) { + for (uint32_t i = 0; i < _n_pda_labels; i++) { insert_edge(from, i, to, trace); } } else { @@ -138,55 +146,26 @@ namespace pdaaal { } }; - // workset := ->_0 (line 1) - for (const auto &from : automaton.states()) { - for (const auto &[to,labels] : from->_edges) { - for (const auto &[label,_] : labels) { - insert_edge(from->_id, label, to, nullptr); - } - } - } - - // 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, automaton.new_pre_trace(rule_id)); - } - ++rule_id; - } - } - - // delta_prime[q] = [p,rule_id] where states[p]._rules[rule_id]._labels.contains(y) for each p, rule_id - // corresponds to --> (the y is the same, since we only have PUSH and not arbitrary --> , i.e. y==y2) - std::vector>> delta_prime(n_automaton_states); - - while (!workset.empty()) { // (line 3) - if constexpr (ET) { - if (found) { - return true; - } - } - + public: + void step() { // pop t = (q, y, q') from workset (line 4) - auto t = workset.top(); - workset.pop(); + auto t = _workset.top(); + _workset.pop(); // 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); + _rel[t._from].emplace_back(t._to, t._label); // (line 7-8 for \Delta') - for (auto pair : delta_prime[t._from]) { // Loop over delta_prime (that match with t->from) + for (auto pair : _delta_prime[t._from]) { // Loop over delta_prime (that match with t->from) auto state = pair.first; auto rule_id = pair.second; - if (pda_states[state]._rules[rule_id].second.contains(t._label)) { - insert_edge(state, t._label, t._to, automaton.new_pre_trace(rule_id, t._from)); + if (_pda_states[state]._rules[rule_id].second.contains(t._label)) { + insert_edge(state, t._label, t._to, _automaton.new_pre_trace(rule_id, t._from)); } } // Loop over \Delta (filter rules going into q) (line 7 and 9) - if (t._from >= n_pda_states) { continue; } - for (auto pre_state : pda_states[t._from]._pre_states) { - const auto &rules = pda_states[pre_state]._rules; + if (t._from >= _n_pda_states) { return; } + for (auto pre_state : _pda_states[t._from]._pre_states) { + const auto &rules = _pda_states[pre_state]._rules; auto lb = rules.lower_bound(details::rule_t{t._from}); while (lb != rules.end() && lb->first._to == t._from) { const auto &[rule, labels] = *lb; @@ -197,22 +176,22 @@ namespace pdaaal { break; case SWAP: // (line 7-8 for \Delta) if (rule._op_label == t._label) { - insert_edge_bulk(pre_state, labels, t._to, automaton.new_pre_trace(rule_id)); + insert_edge_bulk(pre_state, labels, t._to, _automaton.new_pre_trace(rule_id)); } break; case NOOP: // (line 7-8 for \Delta) if (labels.contains(t._label)) { - insert_edge(pre_state, t._label, t._to, automaton.new_pre_trace(rule_id)); + insert_edge(pre_state, t._label, t._to, _automaton.new_pre_trace(rule_id)); } break; case PUSH: // (line 9) if (rule._op_label == t._label) { // (line 10) - delta_prime[t._to].emplace_back(pre_state, rule_id); + _delta_prime[t._to].emplace_back(pre_state, rule_id); const trace_t *trace = nullptr; - for (auto rel_rule : rel[t._to]) { // (line 11-12) + for (auto rel_rule : _rel[t._to]) { // (line 11-12) if (labels.contains(rel_rule.second)) { - trace = trace == nullptr ? automaton.new_pre_trace(rule_id, t._to) : trace; + trace = trace == nullptr ? _automaton.new_pre_trace(rule_id, t._to) : trace; insert_edge(pre_state, rel_rule.second, rel_rule.first, trace); } } @@ -224,94 +203,158 @@ namespace pdaaal { } } } - return found; - } - - template - static bool post_star_accepts(PAutomaton &automaton, size_t state, const std::vector &stack) { - if (stack.size() == 1) { - auto s_label = stack[0]; - return post_star(automaton, [&automaton, state, s_label](size_t from, uint32_t label, size_t to, trace_ptr trace) -> bool { - return from == state && label == s_label && automaton.states()[to]->_accepting; - }); - } else { - return post_star(automaton) || automaton.accepts(state, stack); + [[nodiscard]] bool workset_empty() const { + return _workset.empty(); } - } + [[nodiscard]] bool found() const { + return _found; + } + }; - template - static bool post_star_accepts(SolverInstance_impl& instance) { - return instance.initialize_product() || - post_star(instance.automaton(), [&instance](size_t from, uint32_t label, size_t to, trace_ptr trace) -> bool { - return instance.add_edge_product(from, label, to, trace); - }); - } + template + class PostStarSaturation { + public: + explicit PostStarSaturation(PAutomaton &automaton, const early_termination_fn& early_termination = [](size_t f, uint32_t l, size_t t, trace_ptr trace) -> bool { return false; }) + : _automaton(automaton), _early_termination(early_termination), _pda_states(_automaton.pda().states()), + _n_pda_states(_pda_states.size()), _n_Q(_automaton.states().size()) { + initialize(); + }; - template - static auto get_trace(const SolverInstance& instance) { - static_assert(trace_type != Trace_Type::None, "If you want a trace, don't ask for none."); - if constexpr (trace_type == Trace_Type::Shortest) { - auto [path, stack, weight] = instance.template find_path(); - return std::make_pair(_get_trace(instance.pda(), instance.automaton(), path, stack), weight); - } else { - auto [path, stack] = instance.template find_path(); - return _get_trace(instance.pda(), instance.automaton(), path, stack); - } - } - template - static auto get_rule_trace_and_paths(const AbstractionSolverInstance& instance) { - static_assert(trace_type != Trace_Type::None, "If you want a trace, don't ask for none."); - if constexpr (trace_type == Trace_Type::Shortest) { - auto [paths, stack, weight] = instance.template find_path(); - return std::make_pair(_get_rule_trace_and_paths(instance.automaton(), paths, stack), weight); - } else { - auto [paths, stack] = instance.template find_path(); - return _get_rule_trace_and_paths(instance.automaton(), paths, stack); - } - } + private: + // This is an implementation of Algorithm 2 (figure 3.4) 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 48) - template - static bool post_star(PAutomaton &automaton, const early_termination_fn& early_termination = [](size_t f, uint32_t l, size_t t, trace_ptr trace) -> bool { return false; }) { - static_assert(is_weighted || trace_type != Trace_Type::Shortest, "Cannot do shortest-trace post* for PDA without weights."); // TODO: Consider: W=uin32_t, weight==1 as a default weight. - if constexpr (is_weighted && trace_type == Trace_Type::Shortest) { - return post_star_shortest(automaton, early_termination); - } else if constexpr (trace_type == Trace_Type::Any) { - return post_star_any(automaton, early_termination); - } else if constexpr (trace_type == Trace_Type::None) { - return post_star_any(automaton, early_termination); // TODO: Implement faster no-trace option. + PAutomaton& _automaton; + const early_termination_fn& _early_termination; + const std::vector::state_t>& _pda_states; + const size_t _n_pda_states; + const size_t _n_Q; + std::unordered_map, size_t, boost::hash>> _q_prime{}; + + size_t _n_automaton_states{}; + std::unordered_set _edges; + std::queue _workset; + std::vector>> _rel1; // faster access for lookup _from -> (_to, _label) + std::vector> _rel2; // faster access for lookup _to -> _from (when _label is uint32_t::max) + + bool _found = false; + + void initialize() { + // for -> do (line 3) + // Q' U= {q_p'y1} (line 4) + for (auto &state : _pda_states) { + for (auto &[rule, labels] : state._rules) { + if (rule._operation == PUSH) { + auto res = _q_prime.emplace(std::make_pair(rule._to, rule._op_label), _automaton.next_state_id()); + if (res.second) { + _automaton.add_state(false, false); + } + } + } + } + _n_automaton_states = _automaton.states().size(); + _rel1.resize(_n_automaton_states); + _rel2.resize(_n_automaton_states - _n_Q); + + // workset := ->_0 intersect (P x Gamma x Q) (line 1) + // rel := ->_0 \ workset (line 2) + for (const auto &from : _automaton.states()) { + for (const auto &[to,labels] : from->_edges) { + assert(!labels.contains(epsilon)); // PostStar algorithm assumes no epsilon transitions in the NFA. + for (const auto &[label,_] : labels) { + insert_edge(from->_id, label, to, nullptr, from->_id >= _n_pda_states); + } + } + } } - } + void insert_edge(size_t from, uint32_t label, size_t to, const trace_t *trace, bool direct_to_rel = false) { + auto res = _edges.emplace(from, label, to); + if (res.second) { // New edge is not already in edges (rel U workset). + if (direct_to_rel) { + _rel1[from].emplace_back(to, label); + if (label == epsilon && to >= _n_Q) { + _rel2[to - _n_Q].push_back(from); + } + } else { + _workset.emplace(from, label, to); + } + if (trace != nullptr) { // Don't add existing edges + if (label == epsilon) { + _automaton.add_epsilon_edge(from, to, trace_ptr_from(trace)); + } else { + _automaton.add_edge(from, to, label, trace_ptr_from(trace)); + } + } + if constexpr (ET) { + _found = _found || _early_termination(from, label, to, trace_ptr_from(trace)); + } + } + }; - template - static auto get_trace(const TypedPDA& pda, const PAutomaton& automaton, size_t state, const std::vector& stack) { - static_assert(trace_type != Trace_Type::None, "If you want a trace, don't ask for none."); - auto stack_native = pda.encode_pre(stack); - if constexpr (trace_type == Trace_Type::Shortest) { - auto [path, weight] = automaton.template accept_path(state, stack_native); - return std::make_pair(_get_trace(pda, automaton, path, stack_native), weight); - } else { - auto path = automaton.template accept_path(state, stack_native); - return _get_trace(pda, automaton, path, stack_native); + public: + void step() { + // pop t = (q, y, q') from workset (line 6) + temp_edge_t t; + t = _workset.front(); + _workset.pop(); + // rel = rel U {t} (line 8) (membership test on line 7 is done in insert_edge). + _rel1[t._from].emplace_back(t._to, t._label); + if (t._label == epsilon && t._to >= _n_Q) { + _rel2[t._to - _n_Q].push_back(t._from); + } + + // if y != epsilon (line 9) + if (t._label != epsilon) { + const auto &rules = _pda_states[t._from]._rules; + for (size_t rule_id = 0; rule_id < rules.size(); ++rule_id) { + const auto &[rule,labels] = rules[rule_id]; + if (!labels.contains(t._label)) { continue; } + auto trace = _automaton.new_post_trace(t._from, rule_id, t._label); + switch (rule._operation) { + case POP: // (line 10-11) + insert_edge(rule._to, epsilon, t._to, trace, false); + break; + case SWAP: // (line 12-13) + insert_edge(rule._to, rule._op_label, t._to, trace, false); + break; + case NOOP: + insert_edge(rule._to, t._label, t._to, trace, false); + break; + case PUSH: // (line 14) + assert(_q_prime.find(std::make_pair(rule._to, rule._op_label)) != std::end(_q_prime)); + size_t q_new = _q_prime[std::make_pair(rule._to, rule._op_label)]; + insert_edge(rule._to, rule._op_label, q_new, trace, false); // (line 15) + insert_edge(q_new, t._label, t._to, trace, true); // (line 16) + if (!_rel2[q_new - _n_Q].empty()) { + auto trace_q_new = _automaton.new_post_trace(q_new); + for (auto f : _rel2[q_new - _n_Q]) { // (line 17) + insert_edge(f, t._label, t._to, trace_q_new, false); // (line 18) + } + } + break; + } + } + } else { + if (!_rel1[t._to].empty()) { + auto trace = _automaton.new_post_trace(t._to); + for (auto e : _rel1[t._to]) { // (line 20) + insert_edge(t._from, e.second, e.first, trace, false); // (line 21) + } + } + } } - } - template >> - static auto get_trace(const TypedPDA& pda, const PAutomaton& automaton, size_t state, const std::vector& stack_native) { - static_assert(trace_type != Trace_Type::None, "If you want a trace, don't ask for none."); - if constexpr (trace_type == Trace_Type::Shortest) { - auto [path, weight] = automaton.template accept_path(state, stack_native); - return std::make_pair(_get_trace(pda, automaton, path, stack_native),weight); - } else { - auto path = automaton.template accept_path(state, stack_native); - return _get_trace(pda, automaton, path, stack_native); + [[nodiscard]] bool workset_empty() const { + return _workset.empty(); } - } + [[nodiscard]] bool found() const { + return _found; + } + }; - private: template> - static bool post_star_shortest(PAutomaton &automaton, const early_termination_fn& early_termination) { + class PostStarShortestSaturation { static_assert(is_weighted); - const A add; - const C less; struct weight_edge_trace { W weight; @@ -326,37 +369,6 @@ namespace pdaaal { return less(rhs.weight, lhs.weight); // Used in a max-heap, so swap arguments to make it a min-heap. } }; - - // This is an implementation of Algorithm 2 (figure 3.4) 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 48) - const auto & pda_states = automaton.pda().states(); - const auto n_pda_states = pda_states.size(); - const auto n_Q = automaton.states().size(); - - // for -> do - // Q' U= {q_p'y1} - std::unordered_map, size_t, boost::hash>> q_prime{}; - for (const auto &state : pda_states) { - for (const auto &[rule,labels] : state._rules) { - if (rule._operation == PUSH) { - auto res = q_prime.emplace(std::make_pair(rule._to, rule._op_label), automaton.next_state_id()); - if (res.second) { - automaton.add_state(false, false); - } - } - } - } - const auto n_automata_states = automaton.states().size(); - std::vector minpath(n_automata_states - n_Q); - for (size_t i = 0; i < minpath.size(); ++i) { - minpath[i] = pdaaal::max()(); - } - - std::unordered_map, temp_edge_hasher> edge_weights; - std::priority_queue, weight_edge_trace_comp> workset; - std::vector>> rel1(n_Q); // faster access for lookup _from -> (_to, _label) - std::vector> rel2(n_automata_states - n_Q); // faster access for lookup _to -> _from (when _label is uint32_t::max) struct rel3_elem { uint32_t _label; size_t _to; @@ -374,101 +386,143 @@ namespace pdaaal { return !(*this == other); } }; - std::vector> rel3(n_automata_states - n_Q); - const auto update_edge_ = [&edge_weights](size_t from, uint32_t label, size_t to, W edge_weight, W workset_weight) -> std::pair { - auto res = edge_weights.emplace(temp_edge_t{from, label, to}, std::make_pair(edge_weight, workset_weight)); + public: + PostStarShortestSaturation(PAutomaton &automaton, const early_termination_fn& early_termination) + : _automaton(automaton), _early_termination(early_termination), _pda_states(_automaton.pda().states()), + _n_pda_states(_pda_states.size()), _n_Q(_automaton.states().size()) { + initialize(); + }; + + private: + const A _add{}; + const C _less{}; + PAutomaton& _automaton; + const early_termination_fn& _early_termination; + const std::vector::state_t>& _pda_states; + const size_t _n_pda_states; + const size_t _n_Q; + std::unordered_map, size_t, boost::hash>> _q_prime{}; + + size_t _n_automaton_states{}; + std::vector _minpath; + + std::unordered_map, temp_edge_hasher> _edge_weights; + std::priority_queue, weight_edge_trace_comp> _workset; + std::vector>> _rel1; // faster access for lookup _from -> (_to, _label) + std::vector> _rel2; // faster access for lookup _to -> _from (when _label is uint32_t::max) + std::vector> _rel3; + + bool _found = false; + + void initialize() { + // for -> do + // Q' U= {q_p'y1} + for (const auto &state : _pda_states) { + for (const auto &[rule,labels] : state._rules) { + if (rule._operation == PUSH) { + auto res = _q_prime.emplace(std::make_pair(rule._to, rule._op_label), _automaton.next_state_id()); + if (res.second) { + _automaton.add_state(false, false); + } + } + } + } + _n_automaton_states = _automaton.states().size(); + _minpath.resize(_n_automaton_states - _n_Q); + for (size_t i = 0; i < _minpath.size(); ++i) { + _minpath[i] = pdaaal::max()(); + } + + _rel1.resize(_n_Q); + _rel2.resize(_n_automaton_states - _n_Q); + _rel3.resize(_n_automaton_states - _n_Q); + + // workset := ->_0 intersect (P x Gamma x Q) + // rel := ->_0 \ workset + for (auto &from : _automaton.states()) { + for (auto &[to,labels] : from->_edges) { + assert(!labels.contains(epsilon)); // PostStar algorithm assumes no epsilon transitions in the NFA. + for (auto &[label,trace] : labels) { + temp_edge_t temp_edge{from->_id, label, to}; + _edge_weights.emplace(temp_edge, std::make_pair(zero()(), zero()())); + if (from->_id < _n_pda_states) { + _workset.emplace(zero()(), temp_edge, nullptr); + } else { + insert_rel(from->_id, label, to); + if constexpr (ET) { + _found = _found || _early_termination(from->_id, label, to, trace); + } + } + } + } + } + } + + std::pair update_edge_(size_t from, uint32_t label, size_t to, W edge_weight, W workset_weight) { + auto res = _edge_weights.emplace(temp_edge_t{from, label, to}, std::make_pair(edge_weight, workset_weight)); if (!res.second) { - C less; auto result = std::make_pair(false, false); - if (less(edge_weight, (*res.first).second.first)) { + if (_less(edge_weight, (*res.first).second.first)) { (*res.first).second.first = edge_weight; result.first = true; } - if (less(workset_weight, (*res.first).second.second)) { + if (_less(workset_weight, (*res.first).second.second)) { (*res.first).second.second = workset_weight; result.second = true; } return result; } return std::make_pair(res.second, res.second); - }; - const auto update_edge = [n_Q, &minpath, &workset, &update_edge_, &add](size_t from, uint32_t label, size_t to, W edge_weight, const trace_t* trace) { - auto workset_weight = to < n_Q ? edge_weight : add(minpath[to - n_Q], edge_weight); + } + void update_edge(size_t from, uint32_t label, size_t to, W edge_weight, const trace_t* trace) { + auto workset_weight = to < _n_Q ? edge_weight : _add(_minpath[to - _n_Q], edge_weight); if (update_edge_(from, label, to, edge_weight, workset_weight).second) { - workset.emplace(workset_weight, temp_edge_t{from, label, to}, trace); + _workset.emplace(workset_weight, temp_edge_t{from, label, to}, trace); } - }; - const auto get_weight = [&edge_weights](size_t from, uint32_t label, size_t to) -> W { - return (*edge_weights.find(temp_edge_t{from, label, to})).second.first; - }; - - bool found = false; - - // Adds to rel. - const auto insert_rel = [&rel1, &rel2, n_Q](size_t from, uint32_t label, size_t to){ - rel1[from].emplace_back(to, label); - if (label == epsilon && to >= n_Q) { - rel2[to - n_Q].push_back(from); - } - }; - - // workset := ->_0 intersect (P x Gamma x Q) - // rel := ->_0 \ workset - for (auto &from : automaton.states()) { - for (auto &[to,labels] : from->_edges) { - assert(!labels.contains(epsilon)); // PostStar algorithm assumes no epsilon transitions in the NFA. - for (auto &[label,trace] : labels) { - temp_edge_t temp_edge{from->_id, label, to}; - edge_weights.emplace(temp_edge, std::make_pair(zero()(), zero()())); - if (from->_id < n_pda_states) { - workset.emplace(zero()(), temp_edge, nullptr); - } else { - insert_rel(from->_id, label, to); - if constexpr (ET) { - found = found || early_termination(from->_id, label, to, trace); - } - } - } + } + W get_weight(size_t from, uint32_t label, size_t to) const { + return (*_edge_weights.find(temp_edge_t{from, label, to})).second.first; + } + void insert_rel(size_t from, uint32_t label, size_t to) { // Adds to rel. + _rel1[from].emplace_back(to, label); + if (label == epsilon && to >= _n_Q) { + _rel2[to - _n_Q].push_back(from); } } - while (!workset.empty()) { - if constexpr (ET) { - if (found) { - break; - } - } + public: + void step() { // pop t = (q, y, q') from workset - auto elem = workset.top(); - workset.pop(); + auto elem = _workset.top(); + _workset.pop(); auto t = elem.edge; - auto weights = (*edge_weights.find(t)).second; - if (less(weights.second, elem.weight)) { - continue; // Same edge with a smaller weight was already processed. + auto weights = (*_edge_weights.find(t)).second; + if (_less(weights.second, elem.weight)) { + return; // Same edge with a smaller weight was already processed. } auto t_weight = weights.first; // rel = rel U {t} insert_rel(t._from, t._label, t._to); if (t._label == epsilon) { - automaton.add_epsilon_edge(t._from, t._to, std::make_pair(elem.trace, t_weight)); + _automaton.add_epsilon_edge(t._from, t._to, std::make_pair(elem.trace, t_weight)); } else { - automaton.add_edge(t._from, t._to, t._label, std::make_pair(elem.trace, t_weight)); + _automaton.add_edge(t._from, t._to, t._label, std::make_pair(elem.trace, t_weight)); } if constexpr (ET) { - found = found || early_termination(t._from, t._label, t._to, std::make_pair(elem.trace, t_weight)); + _found = _found || _early_termination(t._from, t._label, t._to, std::make_pair(elem.trace, t_weight)); } // if y != epsilon if (t._label != epsilon) { - const auto &rules = pda_states[t._from]._rules; + const auto &rules = _pda_states[t._from]._rules; for (size_t rule_id = 0; rule_id < rules.size(); ++rule_id) { const auto &[rule,labels] = rules[rule_id]; if (!labels.contains(t._label)) { continue; } - auto trace = automaton.new_post_trace(t._from, rule_id, t._label); - auto wd = add(elem.weight, rule._weight); - auto wb = add(t_weight, rule._weight); + auto trace = _automaton.new_post_trace(t._from, rule_id, t._label); + auto wd = _add(elem.weight, rule._weight); + auto wb = _add(t_weight, rule._weight); if (rule._operation != PUSH) { uint32_t label = 0; switch(rule._operation) { @@ -487,191 +541,350 @@ namespace pdaaal { } update_edge(rule._to, label, t._to, wb, trace); } else { // rule._operation == PUSH - assert(q_prime.find(std::make_pair(rule._to, rule._op_label)) != std::end(q_prime)); - size_t q_new = q_prime[std::make_pair(rule._to, rule._op_label)]; + assert(_q_prime.find(std::make_pair(rule._to, rule._op_label)) != std::end(_q_prime)); + size_t q_new = _q_prime[std::make_pair(rule._to, rule._op_label)]; auto add_to_workset = update_edge_(rule._to, rule._op_label, q_new, zero()(), wd).second; auto was_updated = update_edge_(q_new, t._label, t._to, wb, zero()()).first; if (was_updated) { rel3_elem new_elem{t._label, t._to, trace, wb}; - auto &relq = rel3[q_new - n_Q]; + auto &relq = _rel3[q_new - _n_Q]; auto lb = std::lower_bound(relq.begin(), relq.end(), new_elem); if (lb == std::end(relq) || *lb != new_elem) { relq.insert(lb, new_elem); - } else if (less(wb, lb->_weight)) { + } else if (_less(wb, lb->_weight)) { *lb = new_elem; } } - if (less(wd, minpath[q_new - n_Q])) { - minpath[q_new - n_Q] = wd; + if (_less(wd, _minpath[q_new - _n_Q])) { + _minpath[q_new - _n_Q] = wd; if (add_to_workset) { - workset.emplace(wd, temp_edge_t{rule._to, rule._op_label, q_new}, trace); + _workset.emplace(wd, temp_edge_t{rule._to, rule._op_label, q_new}, trace); } } else if (was_updated) { - if (!rel2[q_new - n_Q].empty()) { - auto trace_q_new = automaton.new_post_trace(q_new); - for (auto f : rel2[q_new - n_Q]) { - update_edge(f, t._label, t._to, add(get_weight(f, epsilon, q_new), wb), trace_q_new); + if (!_rel2[q_new - _n_Q].empty()) { + auto trace_q_new = _automaton.new_post_trace(q_new); + for (auto f : _rel2[q_new - _n_Q]) { + update_edge(f, t._label, t._to, _add(get_weight(f, epsilon, q_new), wb), trace_q_new); } } } } } } else { - if (t._to < n_Q) { - if (!rel1[t._to].empty()) { - auto trace = automaton.new_post_trace(t._to); - for (auto e : rel1[t._to]) { - assert(e.first >= n_pda_states); - update_edge(t._from, e.second, e.first, add(get_weight(t._to, e.second, e.first), t_weight), trace); + if (t._to < _n_Q) { + if (!_rel1[t._to].empty()) { + auto trace = _automaton.new_post_trace(t._to); + for (auto e : _rel1[t._to]) { + assert(e.first >= _n_pda_states); + update_edge(t._from, e.second, e.first, _add(get_weight(t._to, e.second, e.first), t_weight), trace); } } } else { - if (!rel3[t._to - n_Q].empty()) { - auto trace = automaton.new_post_trace(t._to); - for (auto &e : rel3[t._to - n_Q]) { - update_edge(t._from, e._label, e._to, add(get_weight(t._to, e._label, e._to), t_weight), trace); + if (!_rel3[t._to - _n_Q].empty()) { + auto trace = _automaton.new_post_trace(t._to); + for (auto &e : _rel3[t._to - _n_Q]) { + update_edge(t._from, e._label, e._to, _add(get_weight(t._to, e._label, e._to), t_weight), trace); } } } } } - - for (size_t i = n_Q; i < n_automata_states; ++i) { - for (auto &e : rel3[i - n_Q]) { - assert(e._label != epsilon); - automaton.add_edge(i, e._to, e._label, std::make_pair(e._trace, e._weight)); - if constexpr (ET) { - found = found || early_termination(i, e._label, e._to, std::make_pair(e._trace, e._weight)); + void finalize() { + for (size_t i = _n_Q; i < _n_automaton_states; ++i) { + for (auto &e : _rel3[i - _n_Q]) { + assert(e._label != epsilon); + _automaton.add_edge(i, e._to, e._label, std::make_pair(e._trace, e._weight)); + if constexpr (ET) { + _found = _found || _early_termination(i, e._label, e._to, std::make_pair(e._trace, e._weight)); + } } } } - return found; - } + [[nodiscard]] bool workset_empty() const { + return _workset.empty(); + } + [[nodiscard]] bool found() const { + return _found; + } + }; - template - static bool post_star_any(PAutomaton &automaton, const early_termination_fn& early_termination) { - // This is an implementation of Algorithm 2 (figure 3.4) 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 48) - const auto & pda_states = automaton.pda().states(); - const auto n_pda_states = pda_states.size(); - const auto n_Q = automaton.states().size(); - - // for -> do (line 3) - // Q' U= {q_p'y1} (line 4) - std::unordered_map, size_t, boost::hash>> q_prime{}; - for (auto &state : pda_states) { - for (auto &[rule, labels] : state._rules) { - if (rule._operation == PUSH) { - auto res = q_prime.emplace(std::make_pair(rule._to, rule._op_label), automaton.next_state_id()); - if (res.second) { - automaton.add_state(false, false); + template + class TraceBack { + using rule_t = user_rule_t; + public: + TraceBack(const PAutomaton& automaton, std::deque>&& edges) + : _automaton(automaton), _edges(std::move(edges)) { }; + private: + const PAutomaton& _automaton; + std::deque> _edges; + bool _post = false; + public: + [[nodiscard]] bool post() const { return _post; } + [[nodiscard]] const std::deque>& edges() const { return _edges; } + std::optional next() { + while(true) { // In case of post_epsilon_trace, keep going until a rule is found or we are done. + auto[from, label, to] = _edges.back(); + const trace_t* trace_label = _automaton.get_trace_label(from, label, to); + if (trace_label == nullptr) return std::nullopt; // Done + _edges.pop_back(); + + if (trace_label->is_pre_trace()) { + // pre* trace + const auto &[rule, labels] = _automaton.pda().states()[from]._rules[trace_label->_rule_id]; + switch (rule._operation) { + case POP: + break; + case SWAP: + _edges.emplace_back(rule._to, rule._op_label, to); + break; + case NOOP: + _edges.emplace_back(rule._to, label, to); + break; + case PUSH: + _edges.emplace_back(trace_label->_state, label, to); + _edges.emplace_back(rule._to, rule._op_label, trace_label->_state); + break; } + return rule_t(from, label, rule); + } else if (trace_label->is_post_epsilon_trace()) { + // Intermediate post* trace + // Current edge is the result of merging with an epsilon edge. + // Reconstruct epsilon edge and the other edge. + _edges.emplace_back(trace_label->_state, label, to); + _edges.emplace_back(from, std::numeric_limits::max(), trace_label->_state); + + } else { // post* trace + _post = true; + const auto &[rule, labels] = _automaton.pda().states()[trace_label->_state]._rules[trace_label->_rule_id]; + switch (rule._operation) { + case POP: + case SWAP: + case NOOP: + _edges.emplace_back(trace_label->_state, trace_label->_label, to); + break; + case PUSH: + auto[from2, label2, to2] = _edges.back(); + _edges.pop_back(); + trace_label = _automaton.get_trace_label(from2, label2, to2); + assert(trace_label != nullptr); + _edges.emplace_back(trace_label->_state, trace_label->_label, to2); + break; + } + assert(from == rule._to); + return rule_t(trace_label->_state, trace_label->_label, rule); } } } - const auto n_automata_states = automaton.states().size(); + }; - std::unordered_set edges; - std::queue workset; - std::vector>> rel1(n_automata_states); // faster access for lookup _from -> (_to, _label) - std::vector> rel2(n_automata_states - n_Q); // faster access for lookup _to -> _from (when _label is uint32_t::max) + } - bool found = false; - const auto insert_edge = [&found, &early_termination, &edges, &workset, &rel1, &rel2, &automaton, n_Q] - (size_t from, uint32_t label, size_t to, const trace_t *trace, bool direct_to_rel = false) { - auto res = edges.emplace(from, label, to); - if (res.second) { // New edge is not already in edges (rel U workset). - if (direct_to_rel) { - rel1[from].emplace_back(to, label); - if (label == epsilon && to >= n_Q) { - rel2[to - n_Q].push_back(from); - } - } else { - workset.emplace(from, label, to); - } - if (trace != nullptr) { // Don't add existing edges - if (label == epsilon) { - automaton.add_epsilon_edge(from, to, trace_ptr_from(trace)); - } else { - automaton.add_edge(from, to, label, trace_ptr_from(trace)); - } - } - if constexpr (ET) { - found = found || early_termination(from, label, to, trace_ptr_from(trace)); - } + class Solver { + public: + template + static bool dual_search_accepts(SolverInstance_impl& 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, trace_ptr trace) -> bool { + return instance.add_final_edge(from, label, to, trace); + }, + [&instance](size_t from, uint32_t label, size_t to, trace_ptr trace) -> bool { + return instance.add_initial_edge(from, label, to, trace); } - }; - - // workset := ->_0 intersect (P x Gamma x Q) (line 1) - // rel := ->_0 \ workset (line 2) - for (const auto &from : automaton.states()) { - for (const auto &[to,labels] : from->_edges) { - assert(!labels.contains(epsilon)); // PostStar algorithm assumes no epsilon transitions in the NFA. - for (const auto &[label,_] : labels) { - insert_edge(from->_id, label, to, nullptr, from->_id >= n_pda_states); - } + ); + } + template + static bool dual_search(PAutomaton &pre_star_automaton, PAutomaton &post_star_automaton, + const details::early_termination_fn& pre_star_early_termination, + const details::early_termination_fn& post_star_early_termination) { + details::PreStarSaturation pre_star(pre_star_automaton, pre_star_early_termination); + details::PostStarSaturation 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 pre_star_accepts(PAutomaton &automaton, size_t state, const std::vector &stack) { + if (stack.size() == 1) { + auto s_label = stack[0]; + return pre_star(automaton, [&automaton, state, s_label](size_t from, uint32_t label, size_t to, trace_ptr trace) -> bool { + return from == state && label == s_label && automaton.states()[to]->_accepting; + }); + } else { + return pre_star(automaton) || automaton.accepts(state, stack); } + } - while (!workset.empty()) { // (line 5) + template + static bool pre_star_accepts(SolverInstance_impl& instance) { + instance.enable_pre_star(); + return instance.initialize_product() || + pre_star(instance.automaton(), [&instance](size_t from, uint32_t label, size_t to, trace_ptr trace) -> bool { + return instance.add_edge_product(from, label, to, trace); + }); + } + + template + static bool pre_star(PAutomaton &automaton, + const details::early_termination_fn& early_termination = [](size_t f, uint32_t l, size_t t, trace_ptr trace) -> bool { return false; }) { + details::PreStarSaturation saturation(automaton, early_termination); + while(!saturation.workset_empty()) { if constexpr (ET) { - if (found) { - return true; - } + if (saturation.found()) return true; } + saturation.step(); + } + return saturation.found(); + } - // pop t = (q, y, q') from workset (line 6) - temp_edge_t t; - t = workset.front(); - workset.pop(); - // rel = rel U {t} (line 8) (membership test on line 7 is done in insert_edge). - rel1[t._from].emplace_back(t._to, t._label); - if (t._label == epsilon && t._to >= n_Q) { - rel2[t._to - n_Q].push_back(t._from); + template + static bool post_star_accepts(PAutomaton &automaton, size_t state, const std::vector &stack) { + if (stack.size() == 1) { + auto s_label = stack[0]; + return post_star(automaton, [&automaton, state, s_label](size_t from, uint32_t label, size_t to, trace_ptr trace) -> bool { + return from == state && label == s_label && automaton.states()[to]->_accepting; + }); + } else { + return post_star(automaton) || automaton.accepts(state, stack); + } + } + + template + static bool post_star_accepts(SolverInstance_impl& instance) { + return instance.initialize_product() || + post_star(instance.automaton(), [&instance](size_t from, uint32_t label, size_t to, trace_ptr trace) -> bool { + return instance.add_edge_product(from, label, to, trace); + }); + } + + template + static bool post_star(PAutomaton &automaton, + const details::early_termination_fn& early_termination = [](size_t f, uint32_t l, size_t t, trace_ptr trace) -> bool { return false; }) { + static_assert(is_weighted || trace_type != Trace_Type::Shortest, "Cannot do shortest-trace post* for PDA without weights."); // TODO: Consider: W=uin32_t, weight==1 as a default weight. + if constexpr (is_weighted && trace_type == Trace_Type::Shortest) { + return post_star_shortest(automaton, early_termination); + } else if constexpr (trace_type == Trace_Type::Any) { + return post_star_any(automaton, early_termination); + } else if constexpr (trace_type == Trace_Type::None) { + return post_star_any(automaton, early_termination); // TODO: Implement faster no-trace option. + } + } + + template + static bool pre_star_accepts_no_ET(SolverInstance_impl& instance) { + instance.enable_pre_star(); + pre_star(instance.automaton()); + return instance.initialize_product(); + } + template + static bool post_star_accepts_no_ET(SolverInstance_impl& instance) { + post_star(instance.automaton()); + return instance.initialize_product(); + } + + template + static auto get_trace(const SolverInstance& instance) { + static_assert(trace_type != Trace_Type::None, "If you want a trace, don't ask for none."); + if constexpr (trace_type == Trace_Type::Shortest) { + auto [path, stack, weight] = instance.template find_path(); + return std::make_pair(_get_trace(instance.pda(), instance.automaton(), path, stack), weight); + } else { + auto [path, stack] = instance.template find_path(); + return _get_trace(instance.pda(), instance.automaton(), path, stack); + } + } + template + static auto get_trace_dual_search(const SolverInstance& instance) { + auto [paths, stack] = instance.template find_path(); + std::vector i_path, f_path; + for (const auto& [i_state, f_state] : paths) { + i_path.emplace_back(i_state); + f_path.emplace_back(f_state); + } + auto trace1 = _get_trace(instance.pda(), instance.initial_automaton(), i_path, stack); + auto trace2 = _get_trace(instance.pda(), instance.final_automaton(), f_path, stack); + 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 AbstractionSolverInstance& instance) { + static_assert(trace_type != Trace_Type::None, "If you want a trace, don't ask for none."); + if constexpr (trace_type == Trace_Type::Shortest) { + auto[paths, stack, weight] = instance.template find_path(); + return std::make_pair(_get_rule_trace_and_paths(instance.automaton(), paths, stack), weight); + } else if constexpr(use_dual) { + auto[paths, stack] = instance.template find_path(); + return _get_rule_trace_and_paths(instance.initial_automaton(), instance.final_automaton(), paths, stack); + } else { + auto[paths, stack] = instance.template find_path(); + return _get_rule_trace_and_paths(instance.automaton(), paths, stack); + } + } + + template + static auto get_trace(const TypedPDA& pda, const PAutomaton& automaton, size_t state, const std::vector& stack) { + static_assert(trace_type != Trace_Type::None, "If you want a trace, don't ask for none."); + auto stack_native = pda.encode_pre(stack); + if constexpr (trace_type == Trace_Type::Shortest) { + auto [path, weight] = automaton.template accept_path(state, stack_native); + return std::make_pair(_get_trace(pda, automaton, path, stack_native), weight); + } else { + auto path = automaton.template accept_path(state, stack_native); + return _get_trace(pda, automaton, path, stack_native); + } + } + template >> + static auto get_trace(const TypedPDA& pda, const PAutomaton& automaton, size_t state, const std::vector& stack_native) { + static_assert(trace_type != Trace_Type::None, "If you want a trace, don't ask for none."); + if constexpr (trace_type == Trace_Type::Shortest) { + auto [path, weight] = automaton.template accept_path(state, stack_native); + return std::make_pair(_get_trace(pda, automaton, path, stack_native),weight); + } else { + auto path = automaton.template accept_path(state, stack_native); + return _get_trace(pda, automaton, path, stack_native); + } + } + + private: + template + static bool post_star_any(PAutomaton &automaton, const details::early_termination_fn& early_termination) { + details::PostStarSaturation saturation(automaton, early_termination); + while(!saturation.workset_empty()) { + if constexpr (ET) { + if (saturation.found()) return true; } + saturation.step(); + } + return saturation.found(); + } - // if y != epsilon (line 9) - if (t._label != epsilon) { - const auto &rules = pda_states[t._from]._rules; - for (size_t rule_id = 0; rule_id < rules.size(); ++rule_id) { - const auto &[rule,labels] = rules[rule_id]; - if (!labels.contains(t._label)) { continue; } - auto trace = automaton.new_post_trace(t._from, rule_id, t._label); - switch (rule._operation) { - case POP: // (line 10-11) - insert_edge(rule._to, epsilon, t._to, trace, false); - break; - case SWAP: // (line 12-13) - insert_edge(rule._to, rule._op_label, t._to, trace, false); - break; - case NOOP: - insert_edge(rule._to, t._label, t._to, trace, false); - break; - case PUSH: // (line 14) - assert(q_prime.find(std::make_pair(rule._to, rule._op_label)) != std::end(q_prime)); - size_t q_new = q_prime[std::make_pair(rule._to, rule._op_label)]; - insert_edge(rule._to, rule._op_label, q_new, trace, false); // (line 15) - insert_edge(q_new, t._label, t._to, trace, true); // (line 16) - if (!rel2[q_new - n_Q].empty()) { - auto trace_q_new = automaton.new_post_trace(q_new); - for (auto f : rel2[q_new - n_Q]) { // (line 17) - insert_edge(f, t._label, t._to, trace_q_new, false); // (line 18) - } - } - break; - } - } - } else { - if (!rel1[t._to].empty()) { - auto trace = automaton.new_post_trace(t._to); - for (auto e : rel1[t._to]) { // (line 20) - insert_edge(t._from, e.second, e.first, trace, false); // (line 21) - } - } + template> + static bool post_star_shortest(PAutomaton &automaton, const details::early_termination_fn& early_termination) { + details::PostStarShortestSaturation saturation(automaton, early_termination); + while(!saturation.workset_empty()) { + if constexpr (ET) { + if (saturation.found()) break; } + saturation.step(); } - return found; + saturation.finalize(); + return saturation.found(); } template @@ -698,63 +911,13 @@ namespace pdaaal { return result; }; - bool post = false; - std::vector trace; trace.push_back(decode_edges(edges)); - while (true) { - auto [from, label, to] = edges.back(); - edges.pop_back(); - const trace_t *trace_label = automaton.get_trace_label(from, label, to); - if (trace_label == nullptr) break; - - if (trace_label->is_pre_trace()) { - // pre* trace - const auto &[rule,labels] = automaton.pda().states()[from]._rules[trace_label->_rule_id]; - switch (rule._operation) { - case POP: - break; - case SWAP: - edges.emplace_back(rule._to, rule._op_label, to); - break; - case NOOP: - edges.emplace_back(rule._to, label, to); - break; - case PUSH: - edges.emplace_back(trace_label->_state, label, to); - edges.emplace_back(rule._to, rule._op_label, trace_label->_state); - break; - } - trace.push_back(decode_edges(edges)); - - } else if (trace_label->is_post_epsilon_trace()) { - // Intermediate post* trace - // Current edge is the result of merging with an epsilon edge. - // Reconstruct epsilon edge and the other edge. - edges.emplace_back(trace_label->_state, label, to); - edges.emplace_back(from, std::numeric_limits::max(), trace_label->_state); - - } else { - // post* trace - const auto &[rule, labels] = automaton.pda().states()[trace_label->_state]._rules[trace_label->_rule_id]; - switch (rule._operation) { - case POP: - case SWAP: - case NOOP: - edges.emplace_back(trace_label->_state, trace_label->_label, to); - break; - case PUSH: - auto [from2, label2, to2] = edges.back(); - edges.pop_back(); - auto trace_label2 = automaton.get_trace_label(from2, label2, to2); - edges.emplace_back(trace_label2->_state, trace_label2->_label, to2); - break; - } - trace.push_back(decode_edges(edges)); - post = true; - } + details::TraceBack tb(automaton, std::move(edges)); + while (tb.next()) { + trace.push_back(decode_edges(tb.edges())); } - if (post) { + if (tb.post()) { std::reverse(trace.begin(), trace.end()); } return trace; @@ -790,81 +953,89 @@ namespace pdaaal { edges.emplace_back(paths[i - 1].first, stack[i - 1], paths[i].first); } - bool post = false; - + details::TraceBack tb(automaton, std::move(edges)); std::vector trace; - while (true) { - auto [from, label, to] = edges.back(); - const trace_t *trace_label = automaton.get_trace_label(from, label, to); - if (trace_label == nullptr) break; - edges.pop_back(); - - if (trace_label->is_pre_trace()) { - // pre* trace - const auto &[rule,labels] = automaton.pda().states()[from]._rules[trace_label->_rule_id]; - switch (rule._operation) { - case POP: - break; - case SWAP: - edges.emplace_back(rule._to, rule._op_label, to); - break; - case NOOP: - edges.emplace_back(rule._to, label, to); - break; - case PUSH: - edges.emplace_back(trace_label->_state, label, to); - edges.emplace_back(rule._to, rule._op_label, trace_label->_state); - break; - } - trace.emplace_back(from, label, rule); - } else if (trace_label->is_post_epsilon_trace()) { - // Intermediate post* trace - // Current edge is the result of merging with an epsilon edge. - // Reconstruct epsilon edge and the other edge. - edges.emplace_back(trace_label->_state, label, to); - edges.emplace_back(from, std::numeric_limits::max(), trace_label->_state); - - } else { // post* trace - post = true; - const auto &[rule, labels] = automaton.pda().states()[trace_label->_state]._rules[trace_label->_rule_id]; - switch (rule._operation) { - case POP: - case SWAP: - case NOOP: - edges.emplace_back(trace_label->_state, trace_label->_label, to); - break; - case PUSH: - auto [from2, label2, to2] = edges.back(); - edges.pop_back(); - trace_label = automaton.get_trace_label(from2, label2, to2); - assert(trace_label != nullptr); - edges.emplace_back(trace_label->_state, trace_label->_label, to2); - break; - } - assert(from == rule._to); - trace.emplace_back(trace_label->_state, trace_label->_label, rule); - } + while (auto rule = tb.next()) { + trace.emplace_back(rule.value()); } // Get accepting path of initial stack (and the initial stack itself - for post*) std::vector start_stack; - start_stack.reserve(edges.size()); + start_stack.reserve(tb.edges().size()); std::vector start_path; - start_path.reserve(edges.size() + 1); - start_path.push_back(std::get<0>(edges.back())); - for (auto it = edges.crbegin(); it != edges.crend(); ++it) { + start_path.reserve(tb.edges().size() + 1); + start_path.push_back(std::get<0>(tb.edges().back())); + for (auto it = tb.edges().crbegin(); it != tb.edges().crend(); ++it) { start_path.push_back(std::get<2>(*it)); start_stack.push_back(std::get<1>(*it)); } - if (post) { // post* was used + if (tb.post()) { // post* was used std::reverse(trace.begin(), trace.end()); return std::make_tuple(trace[0].from(), trace, start_stack, stack, start_path, goal_path); } else { // pre* was used return std::make_tuple(paths[0].first, trace, stack, start_stack, goal_path, start_path); } } + + template + static std::tuple< + size_t, // Initial state. (State is size_t::max if no trace exists.) + std::vector>, // Sequence of rules applied to the initial configuration to reach the final configuration. + std::vector, // Initial stack + std::vector, // Final stack + std::vector, // Path in initial PAutomaton (accepting initial stack) + std::vector // Path in final PAutomaton (accepting final stack) (independent of whether pre* or post* was used) + > _get_rule_trace_and_paths(const PAutomaton& initial_automaton, const PAutomaton& final_automaton, + const std::vector>& paths, // The paths as retrieved from the product automaton. First number is the state in initial_automaton, second number is state in final_automaton. + const std::vector& stack) { + using rule_t = user_rule_t; + + if (paths.empty()) { + return std::make_tuple(std::numeric_limits::max(), std::vector(), std::vector(), std::vector(), std::vector(), std::vector()); + } + assert(stack.size() + 1 == paths.size()); + // Build up stack of edges in the PAutomaton. Each PDA rule corresponds to changing some of the top edges. + std::deque> initial_edges; + for (size_t i = stack.size(); i > 0; --i) { + initial_edges.emplace_back(paths[i - 1].first, stack[i - 1], paths[i].first); + } + auto [trace, initial_stack, initial_path] = _get_trace_stack_path(initial_automaton, std::move(initial_edges)); + + std::deque> final_edges; + for (size_t i = stack.size(); i > 0; --i) { + final_edges.emplace_back(paths[i - 1].second, stack[i - 1], paths[i].second); + } + auto [trace2, final_stack, final_path] = _get_trace_stack_path(final_automaton, std::move(final_edges)); + // Concat traces + trace.insert(trace.end(), trace2.begin(), trace2.end()); + return std::make_tuple(trace[0].from(), trace, initial_stack, final_stack, initial_path, final_path); + } + + template + static std::tuple>, std::vector, std::vector> + _get_trace_stack_path(const PAutomaton& automaton, std::deque>&& edges) { + std::vector> trace; + details::TraceBack tb(automaton, std::move(edges)); + while(auto rule = tb.next()) { + trace.emplace_back(rule.value()); + } + if (tb.post()) { + std::reverse(trace.begin(), trace.end()); + } + + // Get accepting path of initial stack (and the initial stack itself - for post*) + std::vector stack; stack.reserve(tb.edges().size()); + std::vector path; path.reserve(tb.edges().size() + 1); + path.push_back(std::get<0>(tb.edges().back())); + for (auto it = tb.edges().crbegin(); it != tb.edges().crend(); ++it) { + path.push_back(std::get<2>(*it)); + stack.push_back(std::get<1>(*it)); + } + return {trace, stack, path}; + } }; + } #endif //PDAAAL_SOLVER_H diff --git a/src/pdaaal/SolverInstance.h b/src/pdaaal/SolverInstance.h index 2135b95..d98e60e 100644 --- a/src/pdaaal/SolverInstance.h +++ b/src/pdaaal/SolverInstance.h @@ -46,12 +46,13 @@ namespace pdaaal { _product(_pda, intersect_vector(initial_states, final_states), initial_nfa.empty_accept() && final_nfa.empty_accept()) { }; // Returns whether an accepting state in the product automaton was reached. + template bool initialize_product() { std::vector ids(_product.states().size()); std::iota (ids.begin(), ids.end(), 0); // Fill with 0,1,...,size-1; - return construct_reachable(ids, - _swap_initial_final ? _final : _initial, - _swap_initial_final ? _initial : _final); + return construct_reachable(ids, + _swap_initial_final ? _final : _initial, + _swap_initial_final ? _initial : _final); } // Returns whether an accepting state in the product automaton was reached. @@ -84,6 +85,59 @@ namespace pdaaal { return construct_reachable(waiting, initial, final); } + // This is for the dual_search mode: + bool add_initial_edge(size_t from, uint32_t label, size_t to, trace_ptr trace) { + std::vector> from_states; + if (from < _id_fast_lookup.size()) { // Avoid out-of-bounds. + from_states = _id_fast_lookup[from]; // Copy here, since loop-body might alter _id_fast_lookup[from]. + } + if (from < _pda_size) { + from_states.emplace_back(from, from); // Initial states are not stored in _id_fast_lookup. + } + std::vector waiting; + for (auto [final_from, product_from] : from_states) { // Iterate through reachable 'from-states'. + for (const auto& [final_to,final_labels] : _final.states()[final_from]->_edges) { + if (final_labels.contains(label)) { + auto [fresh, product_to] = get_product_state(_initial.states()[to].get(), _final.states()[final_to].get()); + _product.add_edge(product_from, product_to, label, trace); + if (_product.has_accepting_state()) { + return true; // Early termination + } + if (fresh) { + waiting.push_back(product_to); // If the 'to-state' is new (was not previously reachable), we need to continue constructing from there. + } + } + } + } + return construct_reachable(waiting, _initial, _final); + } + bool add_final_edge(size_t from, uint32_t label, size_t to, trace_ptr trace) { + std::vector> from_states; + if (from < _id_fast_lookup_back.size()) { // Avoid out-of-bounds. + from_states = _id_fast_lookup_back[from]; // Copy here, since loop-body might alter _id_fast_lookup[from]. + } + if (from < _pda_size) { + from_states.emplace_back(from, from); // Initial states are not stored in _id_fast_lookup. + } + std::vector waiting; + for (auto [initial_from, product_from] : from_states) { // Iterate through reachable 'from-states'. + for (const auto& [initial_to,initial_labels] : _initial.states()[initial_from]->_edges) { + if (initial_labels.contains(label)) { + auto [fresh, product_to] = get_product_state(_initial.states()[initial_to].get(), _final.states()[to].get()); + _product.add_edge(product_from, product_to, label, trace); + if (_product.has_accepting_state()) { + return true; // Early termination + } + if (fresh) { + waiting.push_back(product_to); // If the 'to-state' is new (was not previously reachable), we need to continue constructing from there. + } + } + } + } + return construct_reachable(waiting, _initial, _final); + } + + automaton_t& automaton() { return _swap_initial_final ? _final : _initial; } @@ -91,9 +145,15 @@ namespace pdaaal { return _swap_initial_final ? _final : _initial; } + automaton_t& initial_automaton() { + return _initial; + } const automaton_t& initial_automaton() const { return _initial; } + automaton_t& final_automaton() { + return _final; + } const automaton_t& final_automaton() const { return _final; } @@ -250,6 +310,7 @@ namespace pdaaal { private: // Returns whether an accepting state in the product automaton was reached. + template bool construct_reachable(std::vector& waiting, const automaton_t& initial, const automaton_t& final) { while (!waiting.empty()) { size_t top = waiting.back(); @@ -260,7 +321,7 @@ namespace pdaaal { std::vector labels; std::set_intersection(i_labels.begin(), i_labels.end(), f_labels.begin(), f_labels.end(), std::back_inserter(labels)); if (!labels.empty()) { - 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) { _product.add_edge(top, to_id, label, trace); } @@ -302,6 +363,7 @@ namespace pdaaal { _id_map.unpack(id - _pda_size, &res); return res; } + template std::pair get_product_state(const state_t* a, const state_t* b) { if (a->_id == b->_id && a->_id < _pda_size) { return std::make_pair(false, a->_id); @@ -314,6 +376,12 @@ namespace pdaaal { _id_fast_lookup.resize(a->_id + 1); } _id_fast_lookup[a->_id].emplace_back(b->_id, state_id); + if constexpr(needs_back_lookup) { + if (b->_id >= _id_fast_lookup_back.size()) { + _id_fast_lookup_back.resize(b->_id + 1); + } + _id_fast_lookup_back[b->_id].emplace_back(a->_id, state_id); + } return std::make_pair(true, state_id); } else { return std::make_pair(false ,id + _pda_size); @@ -328,7 +396,8 @@ namespace pdaaal { product_automaton_t _product; bool _swap_initial_final = false; ptrie::set_stable _id_map; - std::vector>> _id_fast_lookup; + std::vector>> _id_fast_lookup; // maps initial_state -> (final_state, product_state) + std::vector>> _id_fast_lookup_back; // maps final_state -> (initial_state, product_state) Only used in dual_search }; template diff --git a/test/ParsingPDAFactory_test.cpp b/test/ParsingPDAFactory_test.cpp index 41b7fd4..dbd37cd 100644 --- a/test/ParsingPDAFactory_test.cpp +++ b/test/ParsingPDAFactory_test.cpp @@ -424,3 +424,95 @@ A,B,C BOOST_CHECK(std::all_of(trace.begin(), trace.end(), [](const auto& trace_state){ return trace_state._stack.back() == "C"; })); print_trace(trace); } + + +BOOST_AUTO_TEST_CASE(DualSearch_Test) +{ + std::istringstream i_stream(R"( +# You can make a comment like this + +# Labels +A,B +# Initial states +0 +# Accepting states +0 +# Rules +0 A -> 2 B +0 B -> 0 A +0 A -> 1 - +1 B -> 2 +B +2 B -> 0 - + +# POP rules use - +# PUSH rules use +LABEL +# SWAP rules use LABEL +)"); + auto factory = ParsingPDAFactory<>::create(i_stream); + + // initial stack: [A,B] + NFA initial(std::unordered_set{"A"}); + NFA temp(std::unordered_set{"B"}); + initial.concat(std::move(temp)); + // final stack: [A] + NFA final(std::unordered_set{"A"}); + // Yeah, a small regex -> NFA parser could be nice here... + + auto instance = factory.compile(initial, final); + + bool result = Solver::dual_search_accepts(instance); + BOOST_CHECK(result); + + auto trace = Solver::get_trace_dual_search(instance); + BOOST_CHECK_GE(trace.size(), 4); + BOOST_CHECK_LE(trace.size(), 5); + + print_trace(trace); +} + +BOOST_AUTO_TEST_CASE(Complete_CEGAR_dualsearch_Full_Abstraction_Test) +{ + std::istringstream i_stream(R"( +# Labels +A,B,C +# Initial states +0 +# Accepting states +0 +# Rules +0 A -> 2 B +0 B -> 0 A +0 A -> 1 - +1 B -> 2 +B +2 B -> 0 - + +# POP rules use - +# PUSH rules use +LABEL +# SWAP rules use LABEL +)"); + auto factory = ParsingCegarPdaFactory<>::create(i_stream, + [](const auto& label){ return 0; }, // All labels map to 0. + [](const auto& s){ return 0; }); // All states map to 0. + + // initial stack: [A,B,C] + NFA initial(std::unordered_set{"A"}); + NFA temp1(std::unordered_set{"B"}); + NFA temp2(std::unordered_set{"C"}); + initial.concat(std::move(temp1)); + initial.concat(std::move(temp2)); + // final stack: [A,C] + NFA final(std::unordered_set{"A"}); + NFA temp3(std::unordered_set{"C"}); + final.concat(std::move(temp3)); + // Yeah, a small regex -> NFA parser could be nice here... + + CEGAR,ParsingCegarPdaReconstruction<>> cegar; + auto res = cegar.cegar_solve(std::move(factory), initial, final); + BOOST_CHECK(res.has_value()); + auto trace = res.value(); + + BOOST_CHECK_GE(trace.size(), 4); + BOOST_CHECK_LE(trace.size(), 5); + BOOST_CHECK(std::all_of(trace.begin(), trace.end(), [](const auto& trace_state){ return trace_state._stack.back() == "C"; })); + print_trace(trace); +} \ No newline at end of file