public:
void copy_from(const Strategy* strategy) override
{
- const BasicStrategy* cast_strategy = dynamic_cast<BasicStrategy const*>(strategy);
+ const auto* cast_strategy = dynamic_cast<BasicStrategy const*>(strategy);
xbt_assert(cast_strategy != nullptr);
depth_ = cast_strategy->depth_ - 1;
xbt_assert(depth_ > 0, "The exploration reached a depth greater than %d. We will stop here to prevent weird interaction with DFSExplorer. If you want to change that behaviour, you should augment the size of the search by using --cfg=model-check/max-depth:", _sg_mc_max_depth.get());
public:
void copy_from(const Strategy* strategy) override
{
- const MaxMatchComm* cast_strategy = dynamic_cast<MaxMatchComm const*>(strategy);
+ const auto* cast_strategy = dynamic_cast<MaxMatchComm const*>(strategy);
xbt_assert(cast_strategy != nullptr);
for (auto& [id, val] : cast_strategy->mailbox_)
mailbox_[id] = val;
public:
void copy_from(const Strategy* strategy) override
{
- const MinMatchComm* cast_strategy = dynamic_cast<MinMatchComm const*>(strategy);
- xbt_assert(cast_strategy != nullptr);
- for (auto& [id, val] : cast_strategy->mailbox_)
- mailbox_[id] = val;
- if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_RECV)
- mailbox_[cast_strategy->last_mailbox_]--;
- if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_SEND)
- mailbox_[cast_strategy->last_mailbox_]++;
-
- for (auto const& [_, val] : mailbox_)
- value_of_state_ -= std::abs(val);
- xbt_assert(value_of_state_ > 0, "MinMatchComm value shouldn't reach 0");
+ const auto* cast_strategy = dynamic_cast<MinMatchComm const*>(strategy);
+ xbt_assert(cast_strategy != nullptr);
+ for (auto& [id, val] : cast_strategy->mailbox_)
+ mailbox_[id] = val;
+ if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_RECV)
+ mailbox_[cast_strategy->last_mailbox_]--;
+ if (cast_strategy->last_transition_ == Transition::Type::COMM_ASYNC_SEND)
+ mailbox_[cast_strategy->last_mailbox_]++;
+
+ for (auto const& [_, val] : mailbox_)
+ value_of_state_ -= std::abs(val);
+ xbt_assert(value_of_state_ > 0, "MinMatchComm value shouldn't reach 0");
}
MinMatchComm() = default;
~MinMatchComm() override = default;
using Handler = std::function<bool(const Execution&, Execution::EventHandle, const Transition*)>;
using HandlerMap = std::unordered_map<Action, Handler>;
- const static HandlerMap handlers =
- HandlerMap{{Action::ACTOR_JOIN, &ReversibleRaceCalculator::is_race_reversible_ActorJoin},
- {Action::BARRIER_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock},
- {Action::BARRIER_WAIT, &ReversibleRaceCalculator::is_race_reversible_BarrierWait},
- {Action::COMM_ASYNC_SEND, &ReversibleRaceCalculator::is_race_reversible_CommSend},
- {Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv},
- {Action::COMM_TEST, &ReversibleRaceCalculator::is_race_reversible_CommTest},
- {Action::COMM_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait},
- {Action::MUTEX_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock},
- {Action::MUTEX_TEST, &ReversibleRaceCalculator::is_race_reversible_MutexTest},
- {Action::MUTEX_TRYLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexTrylock},
- {Action::MUTEX_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexUnlock},
- {Action::MUTEX_WAIT, &ReversibleRaceCalculator::is_race_reversible_MutexWait},
- {Action::OBJECT_ACCESS, &ReversibleRaceCalculator::is_race_reversible_ObjectAccess},
- {Action::RANDOM, &ReversibleRaceCalculator::is_race_reversible_Random},
- {Action::SEM_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_SemAsyncLock},
- {Action::SEM_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_SemUnlock},
- {Action::SEM_WAIT, &ReversibleRaceCalculator::is_race_reversible_SemWait},
- {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny},
- {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}};
+ const static HandlerMap handlers = {
+ {Action::ACTOR_JOIN, &ReversibleRaceCalculator::is_race_reversible_ActorJoin},
+ {Action::BARRIER_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_BarrierAsyncLock},
+ {Action::BARRIER_WAIT, &ReversibleRaceCalculator::is_race_reversible_BarrierWait},
+ {Action::COMM_ASYNC_SEND, &ReversibleRaceCalculator::is_race_reversible_CommSend},
+ {Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv},
+ {Action::COMM_TEST, &ReversibleRaceCalculator::is_race_reversible_CommTest},
+ {Action::COMM_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait},
+ {Action::MUTEX_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_MutexAsyncLock},
+ {Action::MUTEX_TEST, &ReversibleRaceCalculator::is_race_reversible_MutexTest},
+ {Action::MUTEX_TRYLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexTrylock},
+ {Action::MUTEX_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_MutexUnlock},
+ {Action::MUTEX_WAIT, &ReversibleRaceCalculator::is_race_reversible_MutexWait},
+ {Action::OBJECT_ACCESS, &ReversibleRaceCalculator::is_race_reversible_ObjectAccess},
+ {Action::RANDOM, &ReversibleRaceCalculator::is_race_reversible_Random},
+ {Action::SEM_ASYNC_LOCK, &ReversibleRaceCalculator::is_race_reversible_SemAsyncLock},
+ {Action::SEM_UNLOCK, &ReversibleRaceCalculator::is_race_reversible_SemUnlock},
+ {Action::SEM_WAIT, &ReversibleRaceCalculator::is_race_reversible_SemWait},
+ {Action::TESTANY, &ReversibleRaceCalculator::is_race_reversible_TestAny},
+ {Action::WAITANY, &ReversibleRaceCalculator::is_race_reversible_WaitAny}};
const auto* e2_action = E.get_transition_for_handle(e2);
if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) {
// we know that the prior set `S` covered the entire history of C and
// was maximal. Subsequent sets will miss events earlier in the
// topological ordering that appear in `S`
- EventSet minimally_reproducible_events = EventSet();
+ EventSet minimally_reproducible_events;
for (const auto& maximal_set : maximal_subsets_iterator_wrapper<Configuration>(*this)) {
if (maximal_set.size() > minimally_reproducible_events.size()) {
SECTION("Forward direction")
{
- auto ordered_events = C.get_topologically_sorted_events();
- const EventSet ordered_event_set = EventSet(std::move(ordered_events));
+ auto ordered_events = C.get_topologically_sorted_events();
+ const auto ordered_event_set = EventSet(std::move(ordered_events));
REQUIRE(events_seen == ordered_event_set);
}
SECTION("Reverse direction")
{
- auto ordered_events = C.get_topologically_sorted_events_of_reverse_graph();
- const EventSet ordered_event_set = EventSet(std::move(ordered_events));
+ auto ordered_events = C.get_topologically_sorted_events_of_reverse_graph();
+ const auto ordered_event_set = EventSet(std::move(ordered_events));
REQUIRE(events_seen == ordered_event_set);
}
}
using Handler = std::function<EventSet(const Configuration&, Unfolding*, const std::shared_ptr<Transition>)>;
using HandlerMap = std::unordered_map<Action, Handler>;
- const static HandlerMap handlers =
- HandlerMap{{Action::COMM_ASYNC_RECV, &ExtensionSetCalculator::partially_extend_CommRecv},
- {Action::COMM_ASYNC_SEND, &ExtensionSetCalculator::partially_extend_CommSend},
- {Action::COMM_WAIT, &ExtensionSetCalculator::partially_extend_CommWait},
- {Action::COMM_TEST, &ExtensionSetCalculator::partially_extend_CommTest},
- {Action::MUTEX_ASYNC_LOCK, &ExtensionSetCalculator::partially_extend_MutexAsyncLock},
- {Action::MUTEX_UNLOCK, &ExtensionSetCalculator::partially_extend_MutexUnlock},
- {Action::MUTEX_WAIT, &ExtensionSetCalculator::partially_extend_MutexWait},
- {Action::MUTEX_TEST, &ExtensionSetCalculator::partially_extend_MutexTest},
- {Action::ACTOR_JOIN, &ExtensionSetCalculator::partially_extend_ActorJoin}};
+ const static HandlerMap handlers = {
+ {Action::COMM_ASYNC_RECV, &ExtensionSetCalculator::partially_extend_CommRecv},
+ {Action::COMM_ASYNC_SEND, &ExtensionSetCalculator::partially_extend_CommSend},
+ {Action::COMM_WAIT, &ExtensionSetCalculator::partially_extend_CommWait},
+ {Action::COMM_TEST, &ExtensionSetCalculator::partially_extend_CommTest},
+ {Action::MUTEX_ASYNC_LOCK, &ExtensionSetCalculator::partially_extend_MutexAsyncLock},
+ {Action::MUTEX_UNLOCK, &ExtensionSetCalculator::partially_extend_MutexUnlock},
+ {Action::MUTEX_WAIT, &ExtensionSetCalculator::partially_extend_MutexWait},
+ {Action::MUTEX_TEST, &ExtensionSetCalculator::partially_extend_MutexTest},
+ {Action::ACTOR_JOIN, &ExtensionSetCalculator::partially_extend_ActorJoin}};
if (const auto handler = handlers.find(action->type_); handler != handlers.end()) {
return handler->second(C, U, std::move(action));
// `WaitAny()` is always disabled in `config(K)`; hence, it
// is independent of any transition in `config(K)` (according
// to formal definition of independence)
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ const auto K = EventSet({e, pre_event_a_C.value_or(e)});
const auto config_K = History(K);
if (not config_K.contains(e_issuer)) {
continue;
// `WaitAny()` is always disabled in `config(K)`; hence, it
// is independent of any transition in `config(K)` (according
// to formal definition of independence)
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ const auto K = EventSet({e, pre_event_a_C.value_or(e)});
const auto config_K = History(K);
if (not config_K.contains(e_issuer)) {
continue;
// `CommTest()` is always disabled in `config(K)`; hence, it
// is independent of any transition in `config(K)` (according
// to formal definition of independence)
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ const auto K = EventSet({e, pre_event_a_C.value_or(e)});
const auto config_K = History(K);
if (not config_K.contains(e_issuer)) {
continue;
// `WaitAny()` is always disabled in `config(K)`; hence, it
// is independent of any transition in `config(K)` (according
// to formal definition of independence)
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ const auto K = EventSet({e, pre_event_a_C.value_or(e)});
const auto config_K = History(K);
if (not config_K.contains(e_issuer)) {
continue;
// Check for other locks on the same mutex
if (const auto* e_mutex = dynamic_cast<const MutexTransition*>(e->get_transition());
e_mutex->type_ == Transition::Type::MUTEX_ASYNC_LOCK && mutex_lock->get_mutex() == e_mutex->get_mutex()) {
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ const auto K = EventSet({e, pre_event_a_C.value_or(e)});
exC.insert(U->discover_event(std::move(K), mutex_lock));
}
}
// This entails getting information about
// the relative position of the mutex in the queue, which
// again means we need more context...
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ const auto K = EventSet({e, pre_event_a_C.value_or(e)});
exC.insert(U->discover_event(std::move(K), mutex_unlock));
}
}
// This entails getting information about
// the relative position of the mutex in the queue, which
// again means we need more context...
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ const auto K = EventSet({e, pre_event_a_C.value_or(e)});
exC.insert(U->discover_event(std::move(K), mutex_wait));
}
}
// This entails getting information about
// the relative position of the mutex in the queue, which
// again means we need more context...
- const EventSet K = EventSet({e, pre_event_a_C.value_or(e)});
+ const auto K = EventSet({e, pre_event_a_C.value_or(e)});
exC.insert(U->discover_event(std::move(K), mutex_test));
}
}
bool equal(const maximal_subsets_iterator& other) const { return current_maximal_set == other.current_maximal_set; }
const EventSet& dereference() const
{
- static const EventSet empty_set = EventSet();
+ static const EventSet empty_set;
if (current_maximal_set.has_value()) {
return current_maximal_set.value();
}
SECTION("Each element of each subset is distinct and appears half of the time in all subsets iteration")
{
// Each element is expected to be found in half of the sets
- const unsigned k = static_cast<unsigned>(example_vec.size());
+ const auto k = static_cast<unsigned>(example_vec.size());
const int expected_count = integer_power(2, k - 1);
std::unordered_map<int, int> element_counts(k);
