+/**
+ * @brief Synchronizes two actions
+ *
+ * When A synchronizes with B (or A --sw-> B), B inherits A's clock vector.
+ * This function performs the synchronization as well as providing other hooks
+ * for other checks along with synchronization.
+ *
+ * @param first The left-hand side of the synchronizes-with relation
+ * @param second The right-hand side of the synchronizes-with relation
+ * @return True if the synchronization was successful (i.e., was consistent
+ * with the execution order); false otherwise
+ */
+bool ModelChecker::synchronize(const ModelAction *first, ModelAction *second)
+{
+ if (*second < *first) {
+ set_bad_synchronization();
+ return false;
+ }
+ check_promises(first->get_tid(), second->get_cv(), first->get_cv());
+ return second->synchronize_with(first);
+}
+