-/******************************** 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)
-{
- unsigned int iter;
- surf_action_t action = NULL;
- surf_model_t model = NULL;
- smx_action_t smx_action = NULL;
-
- /* Execute all the actions in every model */
- xbt_dynar_foreach(model_list, iter, model){
- while ((action = xbt_swag_extract(model->states.running_action_set))){
- /* FIXME: timeouts are not calculated correctly */
- if(NOW >= action->max_duration){
- surf_action_state_set(action, SURF_ACTION_DONE);
- smx_action = action->data;
- 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);
-
- /* Copy the transfered data of the completed network actions */
- /* FIXME: be carefull it might not be an action of the network model */
- if(smx_action && smx_action->data != NULL)
- SIMIX_network_copy_data((smx_comm_t)smx_action->data);
-
- if(smx_action)
- SIMIX_action_signal_all(smx_action);
- }
- }
- /*FIXME: check if this is always empty or not */
- while ((action = xbt_swag_extract(model->states.failed_action_set))) {
- smx_action = action->data;
- DEBUG4("Resource [%s] (%d): Executing FAILED action \"%s\" (%p)",
- model->name, xbt_swag_size(model->states.running_action_set),
- smx_action->name, smx_action);
- if (smx_action)
- SIMIX_action_signal_all(smx_action);
- }
- }
- /* That's it, now go one step deeper into the model-checking process! */
- NOW += 0.5; /* FIXME: Check time increases*/
-}
-
-/****************************** Statistics ************************************/