-
-/**
- * \brief Schedules all the process that are ready to run
- * As a side effect it performs some clean-up required by SIMIX
- */
-void MC_schedule_enabled_processes(void)
-{
- smx_process_t process;
-
- //SIMIX_process_empty_trash();
-
- /* Schedule every process that is ready to run due to an finished action */
- while ((process = xbt_swag_extract(simix_global->process_to_run))) {
- DEBUG2("Scheduling %s on %s", process->name, process->smx_host->name);
- SIMIX_process_schedule(process);
- }
-}
-
-/******************************** States **************************************/
-
-/**
- * \brief Creates a state data structure used by the exploration algorithm
- */
-mc_state_t MC_state_new(void)
-{
- mc_state_t state = NULL;
-
- state = xbt_new0(s_mc_state_t, 1);
- state->transitions = xbt_setset_new_set(mc_setset);
- state->enabled_transitions = xbt_setset_new_set(mc_setset);
- state->interleave = xbt_setset_new_set(mc_setset);
- state->done = xbt_setset_new_set(mc_setset);
- state->executed_transition = NULL;
-
- mc_stats->expanded_states++;
-
- return state;
-}
-/**
- * \brief Deletes a state data structure
- * \param trans The state to be deleted
- */
-void MC_state_delete(mc_state_t state)
-{
- /*if(state->executed_transition)
- MC_transition_delete(state->executed_transition);*/
- xbt_setset_destroy_set(state->transitions);
- xbt_setset_destroy_set(state->enabled_transitions);
- xbt_setset_destroy_set(state->interleave);
- xbt_setset_destroy_set(state->done);
-
- xbt_free(state);
-}
-
-/************************** SURF Emulation ************************************/
-
-/* Dirty hack, we manipulate surf's clock to simplify the integration of the
- model-checker */
-extern double NOW;
-
-/**
- * \brief Executes all the actions at every model
- */
-void MC_execute_surf_actions(void)