nonDeterministicMachineRunner.h

#pragma once
 
#include <utils/printer.h>
#include <runner/machineRunner.h>
 
#include <deque>
#include <cassert>
 
#define DEBUG 0
 
namespace TuringSim::Runner {
    template<typename LeafType>
    class AlternatingTree {
    public:
        enum class Quantifier {
            Existential,  
            Universal,  
        };
 
        typedef size_t Uid;
 
        void insert(Uid subUid, Quantifier q, std::vector<std::tuple<LeafType, std::optional<bool>>>& newLeaves) {
            leaves.erase(subUid);
            if(q == quantifier) {
                for(size_t i = 0; i < newLeaves.size(); ++i) {
                    leaves.emplace_hint(leaves.end(), nextUid++, std::move(std::get<LeafType>(newLeaves[i])));
                }
                for(size_t i = 0; i < newLeaves.size(); ++i) {
                    if(std::get<std::optional<bool>>(newLeaves[i])) {
                        decide(nextUid - newLeaves.size() + i, *std::get<std::optional<bool>>(newLeaves[i]));
                    }
                }
            }
            else {
                new AlternatingTree(subUid, q, std::move(newLeaves), this);
            }
        }
 
        [[nodiscard]] std::pair<const Uid, LeafType>& pick() {
            return *leaves.begin();
        }
 
        [[nodiscard]] Uid lastLeafUid() {
            return leaves.rbegin()->first;
        }
 
        [[nodiscard]] bool hasLeaves() const {
            return !leaves.empty();
        }
 
        [[nodiscard]] const std::map<Uid, std::shared_ptr<AlternatingTree<LeafType>>>& getSubTrees() {
            return subTrees;
        }
 
        void decide(Uid subUid, bool d) {
            std::tuple<LeafType, bool> decidedLeaf{std::move(leaves[subUid]), std::move(d)};
            decidedLeaves.insert({subUid, decidedLeaf});
            leaves.erase(subUid);
            if(d == (quantifier == Quantifier::Existential)) {
                decision = d;
                if(parent) {
                    auto& [uid, p] = *parent;
                    p->propagate_decide(uid, d);
                }
            }
            else {
                if(leaves.empty() && subTrees.empty()) {
                    decision = d;
                    if(parent) {
                        auto& [uid, p] = *parent;
                        p->propagate_decide(uid, d);
                    }
                }
            }
        }
 
        [[nodiscard]] bool decided() const noexcept {
            return decision.has_value();
        }
 
        [[nodiscard]] std::optional<bool> getDecision() const noexcept {
            return decision;
        }
 
        static std::shared_ptr<AlternatingTree> makeAlternatingTreeRoot(Quantifier quantifier, const std::vector<LeafType>& leaves) {
            AlternatingTree* p = new AlternatingTree(quantifier, leaves);
            return std::shared_ptr<AlternatingTree>(p);
        }
 
        template<typename CharT = char, typename Traits = std::char_traits<CharT>>
        std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> debug() const {
            return debug(0);
        }
 
        template<typename CharT = char, typename Traits = std::char_traits<CharT>>
        static std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> debug(const Quantifier& q) {
            std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> f =
                    [q](std::basic_ostream<CharT, Traits>& os) -> std::basic_ostream<CharT, Traits>& {
                        switch (q) {
                            case Quantifier::Universal:
                                return os << "A";
                            case Quantifier::Existential:
                                return os << "E";
                        }
                    };
            return f;
        }
 
        template<typename CharT = char, typename Traits = std::char_traits<CharT>>
        friend std::basic_ostream<CharT, Traits>& operator<<(std::basic_ostream<CharT, Traits>& os, const AlternatingTree& tree) {
            using Utils::Debug::operator<<;
            return os << tree.debug();
        }
 
        template<typename CharT = char, typename Traits = std::char_traits<CharT>>
        std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> debug(size_t i) const {
            std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> f =
                    [this, i](std::basic_ostream<CharT, Traits>& os) -> std::basic_ostream<CharT, Traits>& {
                        using Utils::Debug::operator<<;
                        std::string indent(i, ' ');
                        os << indent
                           << debug(quantifier)
                           << ", parent: " << Utils::Debug::debug(parent)
                           << ", nextUid: " << nextUid
                           << ", decision: " << Utils::Debug::debug(decision) << std::endl;
 
                        os << indent << "Leaves:" << std::endl;
                        for(const auto& [uid, leaf]: leaves) {
                            os << indent << "  uid: " << uid << std::endl;
                            os << indent << "  leaf: " << std::endl;
                            os << indent << "    " << Utils::Debug::debug(leaf) << std::endl;
                        }
 
                        os << indent << "Decided leaves:" << std::endl;
                        for(const auto& [uid, decided_leaf]: decidedLeaves) {
                            auto& [leaf, decision] = decided_leaf;
                            os << indent << "  uid: " << uid << std::endl;
                            os << indent << "  decision: " << std::boolalpha << decision << std::endl;
                            os << indent << "  leaf: " << std::endl;
                            os << indent << "    " << Utils::Debug::debug(leaf) << std::endl;
                        }
 
                        os << indent << "Sub-trees:" << std::endl;
                        for(const auto& [uid, tree]: subTrees) {
                            os << indent << "  uid: " << uid << std::endl;
                            os << indent << "  tree: " << std::endl;
                            os << tree->debug(i + 4) << std::endl;
                        }
 
                        os << indent << "Decided sub-trees:" << std::endl;
                        for(const auto& [uid, decided_subTree]: decidedSubTrees) {
                            auto& [subTree, decision] = decided_subTree;
                            os << indent << "  uid: " << uid << std::endl;
                            os << indent << "  decision: " << std::boolalpha << decision << std::endl;
                            os << indent << "  sub-tree: " << std::endl;
                            os << subTree->debug(i + 4) << std::endl;
                        }
 
                        return os;
                    };
            return f;
        }
 
        void compact() {
            decidedSubTrees.clear();
            decidedLeaves.clear();
            for(auto& [_uid, subTree]: subTrees) {
                subTree->compact();
            }
        }
 
    private:
        AlternatingTree() = delete;
        AlternatingTree(Quantifier quantifier, const std::vector<LeafType>& leaves) :
                quantifier(quantifier),
                leaves(),
                parent()
        {
            for(const LeafType& leaf: leaves) {
                this->leaves.insert({nextUid++, leaf});
            }
        }
 
        AlternatingTree(Quantifier quantifier, std::vector<LeafType>&& leaves) :
                quantifier(quantifier),
                leaves(),
                parent()
        {
            for(LeafType& leaf: leaves) {
                this->leaves.insert({nextUid++, std::move(leaf)});
            }
        }
 
        AlternatingTree(Uid uid, Quantifier quantifier, std::vector<std::tuple<LeafType, std::optional<bool>>>&& newLeaves, AlternatingTree<LeafType>* parent) :
                quantifier(quantifier),
                leaves(),
                parent({uid, parent})
        {
            for(size_t i = 0; i < newLeaves.size(); ++i) {
                leaves.emplace_hint(leaves.end(), nextUid++, std::move(std::get<LeafType>(newLeaves[i])));
            }
            parent->subTrees[uid] = std::shared_ptr<AlternatingTree>(this);
            for(size_t i = 0; i < newLeaves.size(); ++i) {
                if(std::get<std::optional<bool>>(newLeaves[i])) {
                    decide(nextUid - newLeaves.size() + i, *std::get<std::optional<bool>>(newLeaves[i]));
                }
            }
        }
 
        AlternatingTree(const AlternatingTree& other) :
                quantifier(other.quantifier),
                subTrees(other.subTrees),
                leaves(other.leaves),
                decision(other.decision),
                parent()
        {}
 
        AlternatingTree(AlternatingTree&& other) :
                quantifier(other.quantifier),
                subTrees(std::move(other.subTrees)),
                leaves(std::move(other.leaves)),
                decision(other.decision),
                parent(other.parent)
        {
            if(parent) {
                auto& [uid, p] = *parent;
                p->subTrees[uid] = this;
            }
        }
 
        void propagate_decide(Uid subUid, bool d) {
            decidedSubTrees.insert({subUid, {subTrees[subUid], d}});
            subTrees.erase(subUid);
            if(d == (quantifier == Quantifier::Existential)) {
                decision = d;
                if(parent) {
                    auto& [uid, p] = *parent;
                    p->propagate_decide(uid, d);
                }
            }
            else {
                if(leaves.empty() && subTrees.empty()) {
                    decision = d;
                    if(parent) {
                        auto& [uid, p] = *parent;
                        p->propagate_decide(uid, d);
                    }
                }
            }
        }
 
        Uid nextUid = 0;
        Quantifier quantifier;
        std::map<Uid, std::shared_ptr<AlternatingTree<LeafType>>> subTrees {};
        std::map<Uid, std::tuple<std::shared_ptr<AlternatingTree<LeafType>>, bool>> decidedSubTrees {};
        std::map<Uid, LeafType> leaves;
        std::map<Uid, std::tuple<LeafType, bool>> decidedLeaves;
        std::optional<bool> decision {};
 
        std::optional<std::tuple<Uid, AlternatingTree<LeafType>*>> parent;
    };
 
 
    template<
            typename MachineType,
            typename ListenerType,
            typename ListenerConstructorArgs = typename MachineRunnerArgs<MachineType, ListenerType>::ListenerConstructorArgs
    >
    class NonDeterministicMachineRunner;
 
    template<typename MachineType_, typename ListenerType_, typename... ListenerConstructorArgs>
    class NonDeterministicMachineRunner<
            MachineType_,
            ListenerType_,
            std::tuple<ListenerConstructorArgs...>
    > :
            public MachineRunner<MachineType_, ListenerType_> {
        typedef MachineRunner<MachineType_, ListenerType_> MachineRunner_;
    public:
        using typename MachineRunner_::StateType;
        using typename MachineRunner_::MachineType;
        using typename MachineRunner_::StorageType;
        using typename MachineRunner_::ListenerType;
        using typename MachineRunner_::ListenerIdType;
        using typename MachineRunner_::TransitionType;
        using typename MachineRunner_::ApplyHelperType;
 
        typedef std::integral_constant<bool, !std::is_same_v<ListenerType, void>> IsListened;
        static constexpr bool IsListened_v = IsListened::value;
 
        typedef typename MachineType::IsAccepting IsAccepting;
        static constexpr bool IsAccepting_v = IsAccepting::value;
 
        typedef typename MachineType::IsAlternating IsAlternating;
        static constexpr bool IsAlternating_v = IsAlternating::value;
 
        typedef
        std::conditional_t<
                IsListened_v,
                std::tuple<StateType, StorageType, ListenerIdType>,
                std::tuple<StateType, StorageType>
        > ConfigurationType;
 
        typedef
        std::conditional_t<
                !IsAlternating_v,
                std::tuple<std::vector<ConfigurationType>, std::vector<ConfigurationType>>,
                std::tuple<std::shared_ptr<AlternatingTree<ConfigurationType>>, std::deque<std::weak_ptr<AlternatingTree<ConfigurationType>>>>
        > ConfigurationSetType;
 
        static_assert(std::is_same_v<std::tuple<ListenerConstructorArgs...>, typename MachineRunnerArgs<MachineType, ListenerType>::ListenerConstructorArgs>,
                      "The only allowed value for ListenerConstructorArgs is the default one.");
 
        NonDeterministicMachineRunner(const MachineType& machine, ListenerConstructorArgs... listener) :
                MachineRunner_(machine, listener...),
                configurations(getInitialConfigurations()),
                running(true) {
        }
 
        constexpr NonDeterministicMachineRunner(const NonDeterministicMachineRunner& other) :
                MachineRunner_(other),
                configurations(other.configurations),
                running(other.running)
        {}
 
        constexpr NonDeterministicMachineRunner(NonDeterministicMachineRunner&& other) :
                MachineRunner_(std::move(other)),
                configurations(std::move(other.configurations)),
                running(std::move(other.running))
        {}
 
        constexpr NonDeterministicMachineRunner& operator=(const NonDeterministicMachineRunner& other) {
            if(this != &other) {
                MachineRunner_::operator=(other);
                configurations = other.configurations;
                running = other.running;
            }
            return *this;
        }
 
        constexpr NonDeterministicMachineRunner& operator=(NonDeterministicMachineRunner&& other) {
            if(this != &other) {
                MachineRunner_::operator=(std::move(other));
                configurations = std::move(other.configurations);
                running = std::move(other.running);
            }
            return *this;
        }
 
        virtual ~NonDeterministicMachineRunner() override {}
 
        bool isRunning() const noexcept {
            return running;
        }
 
        const ConfigurationSetType& getConfigurationSet() const {
            return configurations;
        }
 
        virtual void step(size_t nbIter = 1) override {
            for(size_t i = 0; i < nbIter && running; ++i) {
                oneStep();
            }
        }
 
        virtual void exec() override {
            while(running) {
                oneStep();
            }
        }
 
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Winconsistent-missing-override"
 
        virtual bool accept() {
            exec();
            if constexpr (!IsAccepting_v) {
                return true;
            }
            else if constexpr (!IsAlternating_v) {
                for(const auto& haltedConfiguration: std::get<1>(configurations)) {
                    const StateType& state = std::get<0>(haltedConfiguration);
                    const StorageType& memory = std::get<1>(haltedConfiguration);
                    if(MachineRunner_::machine.isAcceptingConfiguration(state, memory)) {
                        return true;
                    }
                }
                return false;
            } else {
                std::shared_ptr<AlternatingTree<ConfigurationType>> tree = std::get<std::shared_ptr<AlternatingTree<ConfigurationType>>>(configurations);
                return *tree->getDecision();
            }
        }
#pragma clang diagnostic pop
 
        template<typename CharT = char, typename Traits = std::char_traits<CharT>>
        std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> debug() const {
            std::function<std::basic_ostream<CharT, Traits>&(std::basic_ostream<CharT, Traits>&)> f =
                    [this](std::basic_ostream<CharT, Traits>& os) -> std::basic_ostream<CharT, Traits>& {
                        using Utils::Debug::operator<<;
                        if constexpr (!IsAlternating_v) {
                            return os << "running: " << std::boolalpha << running << std::endl
                                      << "running configurations: " << Utils::Debug::debug(std::get<0>(configurations)) << std::endl
                                      << "halted configurations: " << Utils::Debug::debug(std::get<1>(configurations)) << std::endl;
                        } else {
                            return os << "running: " << std::boolalpha << running << std::endl
                                      << "configuration tree: " << std::endl << std::get<0>(configurations)->debug(2) << std::endl
                                      << "queue: " << Utils::Debug::debug(std::get<1>(configurations)) << std::endl;
                        }
                    };
            return f;
        }
 
    protected:
        ConfigurationSetType getInitialConfigurations() {
            if constexpr (!IsAlternating_v && IsListened_v) {
                std::vector<std::tuple<StateType, StorageType, ListenerIdType>> initialConfigurations;
                for(const StateType& state: MachineRunner_::machine.getInitialStates()) {
                    initialConfigurations.push_back({state, {}, MachineRunner_::listener.getInitialId()});
                }
                return {initialConfigurations, {}};
            } else if constexpr (!IsAlternating_v && !IsListened_v) {
                std::vector<std::tuple<StateType, StorageType>> initialConfigurations;
                for(const StateType& state: MachineRunner_::machine.getInitialStates()) {
                    initialConfigurations.push_back({state, {}});
                }
                return {initialConfigurations, {}};
            } else if constexpr (IsAlternating_v && IsListened_v) {
                typename AlternatingTree<ConfigurationType>::Quantifier quantifier =
                        MachineRunner_::machine.isInitiallyUniversal() ? AlternatingTree<ConfigurationType>::Quantifier::Universal : AlternatingTree<ConfigurationType>::Quantifier::Existential;
                std::vector<std::tuple<StateType, StorageType, ListenerIdType>> initialConfigurations;
                for(const StateType& state: MachineRunner_::machine.getInitialStates()) {
                    initialConfigurations.push_back({state, {}, MachineRunner_::listener.getInitialId()});
                }
                std::shared_ptr<AlternatingTree<ConfigurationType>> tree = AlternatingTree<ConfigurationType>::makeAlternatingTreeRoot(quantifier, initialConfigurations);
                return {tree, {}};
            } else {
                typename AlternatingTree<ConfigurationType>::Quantifier quantifier =
                        MachineRunner_::machine.isInitiallyUniversal() ? AlternatingTree<ConfigurationType>::Quantifier::Universal : AlternatingTree<ConfigurationType>::Quantifier::Existential;
                std::vector<std::tuple<StateType, StorageType>> initialConfigurations;
                for(const StateType& state: MachineRunner_::machine.getInitialStates()) {
                    initialConfigurations.push_back({state, {}});
                }
                std::shared_ptr<AlternatingTree<ConfigurationType>> tree = AlternatingTree<ConfigurationType>::makeAlternatingTreeRoot(quantifier, initialConfigurations);
                return {tree, {}};
            }
        }
 
        virtual void oneStep() override {
            if (!running) {
                return;
            }
#if DEBUG
            std::cout << "OneStep begin" << std::endl;
#endif
 
            running = false;
 
            if constexpr (!IsAlternating_v) {
                std::vector<ConfigurationType> newConfigurations;
                auto& [runningConfigurations, haltedConfigurations] = configurations;
                if constexpr (IsListened_v) {
                    for(const auto& [currentState, currentMemory, currentId]: runningConfigurations) {
                        typename MachineType::TransitionContainer matchingTransitions =
                                MachineRunner_::machine.getMatchingTransitions(currentState, currentMemory);
 
                        if (matchingTransitions.empty()) {
                            MachineRunner_::listener.registerNoTransition(currentId, currentState, currentMemory);
                            haltedConfigurations.push_back({currentState, currentMemory, currentId});
                        } else {
                            size_t matchingTransitionsRemaining = matchingTransitions.size();
                            for(auto& matchingTransition: matchingTransitions) {
                                StorageType memory = matchingTransitionsRemaining > 1 ? StorageType(currentMemory) : std::move(currentMemory);
                                matchingTransitionsRemaining--;
                                ListenerIdType id = MachineRunner_::listener.registerPreTransition(currentState, memory, currentId);
                                auto& [transition, helper] = matchingTransition;
                                bool currentRunning = true;
                                StateType newState = transition.apply(
                                        currentState,
                                        memory,
                                        std::move(helper),
                                        currentRunning);
                                bool isNewConfigurationRunning = !MachineRunner_::machine.isHaltingConfiguration(newState, memory);
                                MachineRunner_::listener.registerPostTransition(id, currentState, memory, transition, helper, isNewConfigurationRunning);
                                if(isNewConfigurationRunning && currentRunning) {
                                    running = true;
                                    newConfigurations.push_back({newState, memory, id});
                                } else {
                                    haltedConfigurations.push_back({newState, memory, id});
                                }
                            }
                        }
                    }
                } else {
                    for(const auto& [currentState, currentMemory]: runningConfigurations) {
                        typename MachineType::TransitionContainer matchingTransitions =
                                MachineRunner_::machine.getMatchingTransitions(currentState, currentMemory);
 
                        if (matchingTransitions.empty()) {
                            haltedConfigurations.push_back({currentState, currentMemory});
                        } else {
                            size_t matchingTransitionsRemaining = matchingTransitions.size();
                            for(auto& matchingTransition: matchingTransitions) {
                                StorageType memory = matchingTransitionsRemaining > 1 ? StorageType(currentMemory) : std::move(currentMemory);
                                matchingTransitionsRemaining--;
                                auto& [transition, helper] = matchingTransition;
                                bool currentRunning = true;
                                StateType newState = transition.apply(
                                        currentState,
                                        memory,
                                        std::move(helper),
                                        currentRunning);
                                bool isNewConfigurationRunning = !MachineRunner_::machine.isHaltingConfiguration(newState, memory);
                                if(isNewConfigurationRunning && currentRunning) {
                                    running = true;
                                    newConfigurations.push_back({newState, memory});
                                } else {
                                    haltedConfigurations.push_back({newState, memory});
                                }
                            }
                        }
                    }
                }
                runningConfigurations = newConfigurations;
            } else {
                std::deque<std::shared_ptr<AlternatingTree<ConfigurationType>>> toRun;
                std::deque<std::weak_ptr<AlternatingTree<ConfigurationType>>> newToExplore;
 
                auto& [configurationTree, toExplore] = configurations;
 
                if (toExplore.empty()) {
                    toExplore.push_back(configurationTree);
                }
 
                while (!toExplore.empty()) {
                    std::weak_ptr<AlternatingTree<ConfigurationType>> tree_w = toExplore.front();
                    toExplore.pop_front();
                    if (std::shared_ptr<AlternatingTree<ConfigurationType>> tree = tree_w.lock()) {
                        if (tree->decided()) {
                            continue;
                        }
                        if (tree->hasLeaves()) {
                            toRun.push_back(tree);
                            newToExplore.push_back(tree);
                        } else {
                            for(const auto& [_uid, subTree]: tree->getSubTrees()) {
                                toExplore.push_back(subTree);
                            }
                        }
                    }
                }
 
                using Utils::Debug::operator<<;
#if DEBUG
                std::cout << "toRun: " << Utils::Debug::debug(toRun) << std::endl;
                std::cout << "toRun length: " << toRun.size() << std::endl;
#endif
 
                toExplore = newToExplore;
                while(!toRun.empty()) {
#if DEBUG
                    std::cout << "  toRun length remaining: " << toRun.size() << std::endl;
#endif
                    std::shared_ptr<AlternatingTree<ConfigurationType>> tree = toRun.front();
                    toRun.pop_front();
#if DEBUG
                    std::cout << "  tree: " << Utils::Debug::debug(tree) << std::endl;
#endif
                    if(!tree->hasLeaves()) {
                        continue;
                    }
                    size_t lastUid = tree->lastLeafUid();
                    while(tree->hasLeaves() && !tree->decided()) {
                        std::pair<const size_t, ConfigurationType>& leaf = tree->pick();
                        auto& [uid, content] = leaf;
#if DEBUG
                        std::cout << "    picked leaf uid: " << uid << std::endl;
                        std::cout << "    picked leaf content: " << Utils::Debug::debug(content) << std::endl;
#endif
                        if(uid > lastUid) {
#if DEBUG
                            std::cout << "    Too big; uid: " << uid << ", lastUid: " << lastUid << std::endl;
#endif
                            break;
                        }
                        if constexpr(IsListened_v) {
                            auto& [currentState, currentMemory, currentId] = content;
                            Machine::Acceptance::NodeType nodeType = MachineRunner_::machine.isAcceptingConfiguration(currentState, currentMemory);
                            if(std::optional<bool> decision = Machine::Acceptance::toBool(nodeType); decision) {
                                tree->decide(uid, *decision);
                                MachineRunner_::listener.registerNoTransition(currentId, currentState, currentMemory);
                                continue;
                            }
                            typename MachineType::TransitionContainer matchingTransitions =
                                    MachineRunner_::machine.getMatchingTransitions(currentState, currentMemory);
                            if(matchingTransitions.empty()) {
                                bool decision = Machine::Acceptance::decideForEmptySet(nodeType);
                                tree->decide(uid, decision);
                                MachineRunner_::listener.registerNoTransition(currentId, currentState, currentMemory);
                            } else {
                                std::vector<std::tuple<ConfigurationType, std::optional<bool>>> newLeaves;
                                for(auto& matchingTransition: matchingTransitions) {
                                    StorageType memory = currentMemory;
                                    ListenerIdType id = MachineRunner_::listener.registerPreTransition(currentState, memory, currentId);
                                    auto& [transition, helper] = matchingTransition;
                                    bool currentRunning = true;
                                    StateType newState = transition.apply(
                                            currentState,
                                            memory,
                                            std::move(helper),
                                            currentRunning);
                                    bool isNewConfigurationRunning = !MachineRunner_::machine.isHaltingConfiguration(newState, memory);
                                    MachineRunner_::listener.registerPostTransition(id, currentState, memory, transition, helper, isNewConfigurationRunning);
                                    std::optional<bool> decision;
#if DEBUG
                                    std::cout << "      oldState: " << currentState << std::endl;
                                    std::cout << "      newState: " << newState << std::endl;
                                    std::cout << "      terminated: " << std::boolalpha << (!isNewConfigurationRunning || !currentRunning) << std::endl;
#endif
                                    if(!isNewConfigurationRunning || !currentRunning) {
                                        Machine::Acceptance::NodeType acceptance = MachineRunner_::machine.isAcceptingConfiguration(newState, memory);
#if DEBUG
                                        std::cout << "      decision: " << Machine::Acceptance::debug(acceptance) << std::endl;
#endif
                                        decision = Machine::Acceptance::decideForEmptySet(acceptance);
                                    } else {
                                        running = true;
                                    }
#if DEBUG
                                    std::cout << "      decision: " << Utils::Debug::debug(decision) << std::endl;
#endif
                                    newLeaves.push_back({{newState, memory, id}, decision});
                                }
                                typename AlternatingTree<ConfigurationType>::Quantifier quantifier =
                                        (nodeType == Machine::Acceptance::Universal)
                                        ? AlternatingTree<ConfigurationType>::Quantifier::Universal
                                        : AlternatingTree<ConfigurationType>::Quantifier::Existential;
                                tree->insert(uid, quantifier, newLeaves);
                            }
                        } else {
                            auto& [currentState, currentMemory] = content;
                            Machine::Acceptance::NodeType nodeType = MachineRunner_::machine.isAcceptingConfiguration(currentState, currentMemory);
                            if(std::optional<bool> decision = Machine::Acceptance::toBool(nodeType); decision) {
                                tree->decide(uid, *decision);
                                continue;
                            }
                            typename MachineType::TransitionContainer matchingTransitions =
                                    MachineRunner_::machine.getMatchingTransitions(currentState, currentMemory);
                            if(matchingTransitions.empty()) {
                                bool decision = Machine::Acceptance::decideForEmptySet(nodeType);
                                tree->decide(uid, decision);
                            } else {
                                std::vector<std::tuple<ConfigurationType, std::optional<bool>>> newLeaves;
                                for(auto& matchingTransition: matchingTransitions) {
                                    StorageType memory = currentMemory;
                                    auto& [transition, helper] = matchingTransition;
                                    bool currentRunning = true;
                                    StateType newState = transition.apply(
                                            currentState,
                                            memory,
                                            std::move(helper),
                                            currentRunning);
                                    bool isNewConfigurationRunning = !MachineRunner_::machine.isHaltingConfiguration(newState, memory);
                                    std::optional<bool> decision;
#if DEBUG
                                    std::cout << "      oldState: " << currentState << std::endl;
                                    std::cout << "      newState: " << newState << std::endl;
                                    std::cout << "      terminated: " << std::boolalpha << (!isNewConfigurationRunning || !currentRunning) << std::endl;
#endif
                                    if(!isNewConfigurationRunning || !currentRunning) {
                                        Machine::Acceptance::NodeType acceptance = MachineRunner_::machine.isAcceptingConfiguration(newState, memory);
#if DEBUG
                                        std::cout << "      decision: " << Machine::Acceptance::debug(acceptance) << std::endl;
#endif
                                        decision = Machine::Acceptance::decideForEmptySet(acceptance);
                                    } else {
                                        running = true;
                                    }
#if DEBUG
                                    std::cout << "      decision: " << Utils::Debug::debug(decision) << std::endl;
#endif
                                    newLeaves.push_back({{newState, memory}, decision});
                                }
                                typename AlternatingTree<ConfigurationType>::Quantifier quantifier =
                                        (nodeType == Machine::Acceptance::Universal)
                                        ? AlternatingTree<ConfigurationType>::Quantifier::Universal
                                        : AlternatingTree<ConfigurationType>::Quantifier::Existential;
                                tree->insert(uid, quantifier, newLeaves);
                            }
 
                        }
#if DEBUG
                        std::cout << configurationTree->debug(4) << std::endl;
#endif
                    }
                }
            }
#if DEBUG
            std::cout << "OneStep end" << std::endl;
#endif
        }
 
        ConfigurationSetType configurations;
 
        bool running;
    };
}