+ auto* just_executed = mc_model_checker->handle_simcall(next, times_considered, true);
+ xbt_assert(just_executed->type_ == expected_executed_transition->type_,
+ "The transition that was just executed by actor %ld, viz:\n"
+ "%s\n"
+ "is not what was purportedly scheduled to execute, which was:\n"
+ "%s\n",
+ next, just_executed->to_string().c_str(), expected_executed_transition->to_string().c_str());
+
+ // 3. Update the state with the newest information. This means recording
+ // both
+ // 1. what action was last taken from this state (viz. `executed_transition`)
+ // 2. what action actor `next` was able to take given `times_considered`
+ // The latter update is important as *more* information is potentially available
+ // 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);