+/******************** Non-deterministic message ordering *********************/
+/* Server assumes a fixed order in the reception of messages from its clients */
+/* which is incorrect because the message ordering is non-deterministic */
+/******************************************************************************/
+
#include <msg/msg.h>
#include <mc/modelchecker.h>
#define N 3
+/******************** Non-deterministic message ordering *********************/
+/* Server assumes a fixed order in the reception of messages from its clients */
+/* which is incorrect because the message ordering is non-deterministic */
+/******************************************************************************/
+
#include <msg/msg.h>
#include <mc/modelchecker.h>
#define N 3
-/* Centralized Mutual Exclusion Algorithm
- *
- * This constitutes the answer to the exercice 2 of the practical
- * lab on implementing mutual exclusion algorithms with SimGrid.
- *
- * YOU SHOULD TRY IMPLEMENTING IT YOURSELF BEFORE READING THE SOLUTION.
- */
+/***************** Centralized Mutual Exclusion Algorithm *********************/
+/* This example implements a centralized mutual exclusion algorithm. */
+/* There is no bug on it, it is just provided to test the state space */
+/* reduction of DPOR. */
+/******************************************************************************/
#include "msg/msg.h"
-#define AMOUNT_OF_CLIENTS 5
+#define AMOUNT_OF_CLIENTS 4
#define CS_PER_PROCESS 2
XBT_LOG_NEW_DEFAULT_CATEGORY(centralized, "my log messages");
<process host="Geoff" function="client" />
- <process host="Disney" function="client" />
+<!-- <process host="Disney" function="client" />
-<!-- <process host="iRMX" function="client" />
+ <process host="iRMX" function="client" />
<process host="McGee" function="client" />
DEBUG5("Resource [%s] (%d): Executing RUNNING action \"%s\" (%p) MaxDuration %lf",
model->name, xbt_swag_size(model->states.running_action_set),
smx_action->name, smx_action, action->max_duration);
-
+
if(smx_action)
SIMIX_action_signal_all(smx_action);
}