}
// This should be done in GuidedState, or at least interact with it
-void State::execute_next(aid_t next, RemoteApp& app)
+std::shared_ptr<Transition> State::execute_next(aid_t next, RemoteApp& app)
{
// First, warn the guide, so it knows how to build a proper child state
strategy_->execute_next(next, app);
// about a transition AFTER it has executed.
transition_ = just_executed;
- auto executed_transition = std::unique_ptr<Transition>(just_executed);
- actor_state.set_transition(std::move(executed_transition), times_considered);
-
+ const auto executed_transition = std::shared_ptr<Transition>(just_executed);
+ actor_state.set_transition(executed_transition, times_considered);
app.wait_for_requests();
+
+ return executed_transition;
}
} // namespace simgrid::mc
// TODO: Add verbose logging about which event is being explored
- const UnfoldingEvent* e = select_next_unfolding_event(A, enC);
+ UnfoldingEvent* e = select_next_unfolding_event(A, enC);
xbt_assert(e != nullptr, "\n\n****** INVARIANT VIOLATION ******\n"
"UDPOR guarantees that an event will be chosen at each point in\n"
"the search, yet no events were actually chosen\n"
// Explore(C + {e}, D, A \ {e})
// Move the application into stateCe (i.e. `state(C + {e})`) and make note of that state
- move_to_stateCe(stateC, *e);
+ move_to_stateCe(&stateC, e);
state_stack.push_back(record_current_state());
explore(Ce, D, std::move(A), std::move(exC));
return enC;
}
-void UdporChecker::move_to_stateCe(State& state, const UnfoldingEvent& e)
+void UdporChecker::move_to_stateCe(State* state, UnfoldingEvent* e)
{
- const aid_t next_actor = e.get_transition()->aid_;
+ const aid_t next_actor = e->get_transition()->aid_;
// TODO: Add the trace if possible for reporting a bug
xbt_assert(next_actor >= 0, "\n\n****** INVARIANT VIOLATION ******\n"
"one transition of the state of an visited event is enabled, yet no\n"
"state was actually enabled. Please report this as a bug.\n"
"*********************************\n\n");
- state.execute_next(next_actor, get_remote_app());
+ auto latest_transition_by_next_actor = state->execute_next(next_actor, get_remote_app());
+
+ // The transition that is associated with the event was just
+ // executed, so it's possible that the new version of the transition
+ // (i.e. the one after execution) has *more* information than
+ // that which existed *prior* to execution.
+ //
+ //
+ // ------- !!!!! UDPOR INVARIANT !!!!! -------
+ //
+ // At this point, we are leveraging the fact that
+ // UDPOR will not contain more than one copy of any
+ // transition executed by any actor for any
+ // particular step taken by that actor. That is,
+ // if transition `i` of the `j`th actor is contained in the
+ // configuration `C` currently under consideration
+ // by UDPOR, then only one and only one copy exists in `C`
+ //
+ // This means that we can referesh the transitions associated
+ // with each event lazily, i.e. only after we have chosen the
+ // event to continue our execution.
+ e->set_transition(std::move(latest_transition_by_next_actor));
}
void UdporChecker::restore_program_state_with_current_stack()
return next_state;
}
-const UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
+UnfoldingEvent* UdporChecker::select_next_unfolding_event(const EventSet& A, const EventSet& enC)
{
if (enC.empty()) {
throw std::invalid_argument("There are no unfolding events to select. "
}
if (A.empty()) {
- return *(enC.begin());
+ return const_cast<UnfoldingEvent*>(*(enC.begin()));
}
for (const auto& event : A) {
if (enC.contains(event)) {
- return event;
+ return const_cast<UnfoldingEvent*>(event);
}
}
return nullptr;
