#include <assert.h>
-#include "mc_state.h"
-#include "mc_request.h"
-#include "mc_safety.h"
-#include "mc_private.h"
-#include "mc_record.h"
-#include "mc_smx.h"
-#include "mc_client.h"
-#include "mc_exit.h"
+#include "src/mc/mc_state.h"
+#include "src/mc/mc_request.h"
+#include "src/mc/mc_safety.h"
+#include "src/mc/mc_private.h"
+#include "src/mc/mc_record.h"
+#include "src/mc/mc_smx.h"
+#include "src/mc/mc_client.h"
+#include "src/mc/mc_exit.h"
#include "src/xbt/mmalloc/mmprivate.h"
XBT_DEBUG("Initial state");
/* Wait for requests (schedules processes) */
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
/* Get an enabled process and insert it in the interleave set of the initial state */
smx_process_t process;
/** \brief Model-check the application using a DFS exploration
* with DPOR (Dynamic Partial Order Reductions)
*/
-void MC_modelcheck_safety(void)
+int MC_modelcheck_safety(void)
{
MC_modelcheck_safety_init();
/* Answer the request */
MC_simcall_handle(req, value);
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
/* Create the new expanded state */
next_state = MC_state_new();
if(_sg_mc_termination && is_exploration_stack_state(next_state)){
MC_show_non_termination();
- exit(SIMGRID_MC_EXIT_NON_TERMINATION);
+ return SIMGRID_MC_EXIT_NON_TERMINATION;
}
if ((visited_state = is_visited_state(next_state)) == NULL) {
/* Check for deadlocks */
if (MC_deadlock_check()) {
MC_show_deadlock(NULL);
- exit(SIMGRID_MC_EXIT_DEADLOCK);
+ return SIMGRID_MC_EXIT_DEADLOCK;
}
/* Traverse the stack backwards until a state with a non empty interleave
XBT_INFO("No property violation found.");
MC_print_statistics(mc_stats);
- exit(SIMGRID_MC_EXIT_SUCCESS);
+ return SIMGRID_MC_EXIT_SUCCESS;
}
static void MC_modelcheck_safety_init(void)
XBT_INFO("Check non progressive cycles");
else
XBT_INFO("Check a safety property");
- MC_wait_for_requests();
+ mc_model_checker->wait_for_requests();
XBT_DEBUG("Starting the safety algorithm");