* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/VisitedState.hpp"
+#include "src/mc/explo/Exploration.hpp"
#include "src/mc/mc_private.hpp"
#include <unistd.h>
#include <sys/wait.h>
#include <memory>
#include <boost/range/algorithm.hpp>
-#include "src/mc/api.hpp"
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_VisitedState, mc, "Logging specific to state equality detection mechanisms");
XBT_DEBUG("Snapshot %p of visited state %ld (exploration stack state %ld)", new_state->system_state.get(),
new_state->num, graph_state->get_num());
- auto [range_begin, range_end] = boost::range::equal_range(states_, new_state.get(), Api::get().compare_pair());
+ auto [range_begin, range_end] =
+ boost::range::equal_range(states_, new_state.get(), compare_pair_by_actor_count_and_used_heap());
if (compare_snapshots)
for (auto i = range_begin; i != range_end; ++i) {
+++ /dev/null
-/* Copyright (c) 2020-2022. The SimGrid Team. All rights reserved. */
-
-/* This program is free software; you can redistribute it and/or modify it
- * under the terms of the license (GNU LGPL) which comes with this package. */
-
-#ifndef SIMGRID_MC_API_HPP
-#define SIMGRID_MC_API_HPP
-
-#include <memory>
-#include <vector>
-
-#include "simgrid/forward.h"
-#include "src/mc/api/RemoteApp.hpp"
-#include "src/mc/api/State.hpp"
-#include "src/mc/mc_forward.hpp"
-#include "src/mc/mc_record.hpp"
-#include "xbt/automaton.hpp"
-#include "xbt/base.h"
-
-namespace simgrid::mc {
-
-/*
-** This class aimes to implement FACADE APIs for simgrid. The FACADE layer sits between the CheckerSide
-** (Unfolding_Checker, DPOR, ...) layer and the
-** AppSide layer. The goal is to drill down into the entagled details in the CheckerSide layer and break down the
-** detailes in a way that the CheckerSide eventually
-** be capable to acquire the required information through the FACADE layer rather than the direct access to the AppSide.
-*/
-
-class Api {
-private:
- Api() = default;
-
- struct DerefAndCompareByActorsCountAndUsedHeap {
- template <class X, class Y> bool operator()(X const& a, Y const& b) const
- {
- return std::make_pair(a->actor_count_, a->heap_bytes_used) < std::make_pair(b->actor_count_, b->heap_bytes_used);
- }
- };
-
-public:
- static Api& get()
- {
- static Api api;
- return api;
- }
-
- // AUTOMATION APIs
- inline DerefAndCompareByActorsCountAndUsedHeap compare_pair() const
- {
- return DerefAndCompareByActorsCountAndUsedHeap();
- }
-};
-
-} // namespace simgrid::mc
-
-#endif
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/api/State.hpp"
-#include "src/mc/api.hpp"
#include "src/mc/mc_config.hpp"
#include <boost/range/algorithm.hpp>
#ifndef SIMGRID_MC_CHECKER_HPP
#define SIMGRID_MC_CHECKER_HPP
-#include "src/mc/api.hpp"
+#include "simgrid/forward.h"
+#include "src/mc/api/RemoteApp.hpp"
+#include "src/mc/mc_record.hpp"
+#include <xbt/Extendable.hpp>
#include <memory>
XBT_PUBLIC Exploration* create_communication_determinism_checker(const std::vector<char*>& args);
XBT_PUBLIC Exploration* create_udpor_checker(const std::vector<char*>& args);
+// FIXME: kill this template and use lambdas in boost::range_equal
+struct DerefAndCompareByActorsCountAndUsedHeap {
+ template <class X, class Y> bool operator()(X const& a, Y const& b) const
+ {
+ return std::make_pair(a->actor_count_, a->heap_bytes_used) < std::make_pair(b->actor_count_, b->heap_bytes_used);
+ }
+};
+static inline DerefAndCompareByActorsCountAndUsedHeap compare_pair_by_actor_count_and_used_heap()
+{
+ return DerefAndCompareByActorsCountAndUsedHeap();
+}
+
} // namespace simgrid::mc
#endif
auto new_pair =
std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_);
- auto [res_begin, res_end] = boost::range::equal_range(acceptance_pairs_, new_pair.get(), Api::get().compare_pair());
+ auto [res_begin, res_end] =
+ boost::range::equal_range(acceptance_pairs_, new_pair.get(), compare_pair_by_actor_count_and_used_heap());
if (pair->search_cycle)
for (auto i = res_begin; i != res_end; ++i) {
std::make_shared<VisitedPair>(pair->num, pair->prop_state_, pair->atomic_propositions, pair->app_state_);
auto [range_begin, range_end] =
- boost::range::equal_range(visited_pairs_, visited_pair.get(), Api::get().compare_pair());
+ boost::range::equal_range(visited_pairs_, visited_pair.get(), compare_pair_by_actor_count_and_used_heap());
for (auto i = range_begin; i != range_end; ++i) {
const VisitedPair* pair_test = i->get();
src/mc/ModelChecker.hpp
src/mc/VisitedState.cpp
src/mc/VisitedState.hpp
- src/mc/api.hpp
src/mc/api/ActorState.hpp
src/mc/api/State.cpp
src/mc/api/State.hpp