#ifndef SIMGRID_MC_LIVENESS_CHECKER_HPP
#define SIMGRID_MC_LIVENESS_CHECKER_HPP
-#include <stdint.h>
+#include <cstddef>
+
+#include <string>
+#include <list>
#include <simgrid_config.h>
#include <xbt/base.h>
-#include <xbt/fifo.h>
#include <xbt/dynar.h>
#include <xbt/automaton.h>
#include <xbt/memory.hpp>
simgrid::mc::State* graph_state = nullptr; /* System state included */
xbt_automaton_state_t automaton_state = nullptr;
simgrid::xbt::unique_ptr<s_xbt_dynar_t> atomic_propositions;
- size_t heap_bytes_used = 0;
+ std::size_t heap_bytes_used = 0;
int nb_processes = 0;
int acceptance_removed = 0;
int visited_removed = 0;
simgrid::mc::VisitedPair* insertAcceptancePair(simgrid::mc::Pair* pair);
int insertVisitedPair(simgrid::mc::VisitedPair* visited_pair, simgrid::mc::Pair* pair);
void showAcceptanceCycle(std::size_t depth);
- void replay(xbt_fifo_t stack);
+ void replay();
void removeAcceptancePair(int pair_num);
+public: // (non-static wannabe) fields
+ static xbt_dynar_t acceptance_pairs;
+ static std::list<Pair*> liveness_stack;
};
}