Add note about resetting `times_considered`

Resetting `times_considered` after multiple
serializations of a particular transition are performed
to give the checker all exections of an actor
that can perform multiple actions. There was concern
that this value would have to be "reset" to the
original value after the serialization, since the latter
modifies the simcall's observer's internal state.

However, no reset is actually needed as each
SIMCALL_EXECUTE message that the checker sends to the
application-side comes equipped with the latest
`times_considered`, and thus preparation will be
performed correctly before execution.

diff --git a/src/mc/remote/AppSide.cpp b/src/mc/remote/AppSide.cpp
index 3adb9b9..80e4c52 100644 (file)
--- a/src/mc/remote/AppSide.cpp
+++ b/src/mc/remote/AppSide.cpp
@@ -209,11 +209,12 @@ void AppSide::handle_actors_status() const
                    "The serialized transition is too large for the buffer. Please fix the code.");
         strncpy(probe.buffer.data(), str.c_str(), probe.buffer.size() - 1);
         probe.buffer.back() = '\0';
-
-        // TODO: Do we need to reset `times_considered` for each actor's
-        // simcall observer here to the "original" value? We may need to
-        // add a method to handle this
       }
+      // NOTE: We do NOT need to reset `times_considered` for each actor's
+      // simcall observer here to the "original" value (i.e. the value BEFORE
+      // multiple prepare() calls were made for serialization purposes) since
+      // each SIMCALL_EXECUTE provides a `times_considered` to be used to prepare
+      // the transition before execution.
     }
 
     size_t size = probes.size() * sizeof(s_mc_message_simcall_probe_one_t);