-/************************** 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);
-
- 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);
- }
+void MC_assert_pair(int prop){
+ if (MC_IS_ENABLED && !prop) {
+ XBT_INFO("**************************");
+ XBT_INFO("*** PROPERTY NOT VALID ***");
+ XBT_INFO("**************************");
+ //XBT_INFO("Counter-example execution trace:");
+ MC_show_snapshot_stack(mc_snapshot_stack);
+ //MC_dump_snapshot_stack(mc_snapshot_stack);
+ MC_print_statistics_pairs(mc_stats_pair);
+ xbt_abort();