end_component_decomposition.h

#ifndef PROBFD_PREPROCESSING_END_COMPONENT_DECOMPOSITION_H
#define PROBFD_PREPROCESSING_END_COMPONENT_DECOMPOSITION_H
 
#include "probfd/quotients/quotient_system.h"
 
#include "probfd/storage/per_state_storage.h"
 
#include "probfd/evaluator.h"
#include "probfd/mdp.h"
#include "probfd/type_traits.h"
 
#include <deque>
#include <limits>
#include <memory>
#include <ostream>
#include <vector>
 
// Forward Declarations
namespace utils {
class CountdownTimer;
}
 
namespace probfd::preprocessing {
 
struct ECDStatistics {
    unsigned long long goals = 0;
    unsigned long long terminals = 0;
    unsigned long long selfloops = 0;
 
    unsigned long long sccs1 = 0;
    unsigned long long sccsk = 0;
    unsigned long long sccs1_dead = 0;
    unsigned long long sccsk_dead = 0;
 
    unsigned long long ec1 = 0;
    unsigned long long eck = 0;
 
    unsigned long long ec_transitions = 0;
 
    unsigned long long recursions = 0;
 
    utils::Timer time;
 
    void print(std::ostream& out) const;
};
 
template <typename State, typename Action>
class EndComponentDecomposition {
    using MDPType = MDP<State, Action>;
    using EvaluatorType = Evaluator<State>;
    using QSystem = quotients::QuotientSystem<State, Action>;
 
    struct StateInfo {
        enum { NEW, ONSTACK, CLOSED };
 
        static constexpr uint32_t UNDEF =
            std::numeric_limits<uint32_t>::max() >> 2;
 
        unsigned explored : 1 = 0;
        unsigned expandable_goal : 1 = 0; // non-terminal goal?
        unsigned stackid : 30 = UNDEF;
 
        [[nodiscard]]
        bool onstack() const;
        auto get_status() const;
    };
 
    struct ExpansionInfo {
        // Tarjan's SCC algorithm: stack id and lowlink
        const unsigned stck;
        unsigned lstck;
 
        // whether the transition has non-zero cost or can leave the scc
        bool nz_or_leaves_scc;
 
        // recursive decomposition flag
        // Recursively decompose the SCC if there is a zero-cost transition
        // in it that can leave and remain in the scc.
        bool recurse = false;
 
        std::vector<Action> aops;
        std::vector<std::vector<StateID>> successors;
 
        // Used in decomposition recursion
        ExpansionInfo(
            unsigned stck,
            std::vector<Action> aops,
            std::vector<std::vector<StateID>> successors);
 
        // Used in root iteration
        ExpansionInfo(
            unsigned stck,
            std::vector<Action> aops,
            std::vector<std::vector<StateID>> successors,
            MDPType& mdp);
 
        // Used in decomposition recursion
        bool next_action(std::nullptr_t);
 
        // Used in root iteration
        bool next_action(MDPType& mdp);
 
        bool next_successor();
 
        StateID get_current_successor();
        Action& get_current_action();
    };
 
    struct StackInfo;
 
    const bool expand_goals_;
 
    storage::PerStateStorage<StateInfo> state_infos_;
    std::deque<ExpansionInfo> expansion_queue_;
    std::vector<StackInfo> stack_;
 
    ECDStatistics stats_;
 
public:
    explicit EndComponentDecomposition(bool expand_goals);
 
    std::unique_ptr<QSystem> build_quotient_system(
        MDPType& mdp,
        const EvaluatorType* pruning_function,
        param_type<State> initial_state,
        double max_time = std::numeric_limits<double>::infinity());
 
    void print_statistics(std::ostream& out) const;
 
    [[nodiscard]]
    ECDStatistics get_statistics() const;
 
private:
    // Used in root iteration
    bool push(
        StateID state_id,
        StateInfo& state_info,
        MDPType& mdp,
        const EvaluatorType* pruning_function);
 
    // Used in decomposition recursion
    bool push(StateID state_id, StateInfo& info);
 
    void find_and_decompose_sccs(
        QSystem& sys,
        unsigned limit,
        utils::CountdownTimer& timer,
        auto&... mdp_and_h);
 
    bool push_successor(
        ExpansionInfo& e,
        StackInfo& s,
        utils::CountdownTimer& timer,
        auto&... mdp_and_h);
 
    template <bool RootIteration>
    void scc_found(
        QSystem& sys,
        ExpansionInfo& e,
        StackInfo& s,
        utils::CountdownTimer& timer);
 
    void decompose(QSystem& sys, unsigned start, utils::CountdownTimer& timer);
};
 
} // namespace probfd::preprocessing
 
#define GUARD_INCLUDE_PROBFD_PREPROCESSING_END_COMPONENT_DECOMPOSITION_H
#include "probfd/preprocessing/end_component_decomposition_impl.h"
#undef GUARD_INCLUDE_PROBFD_PREPROCESSING_END_COMPONENT_DECOMPOSITION_H
 
#endif // PROBFD_PREPROCESSING_END_COMPONENT_DECOMPOSITION_H