+
+ if(MC_state_interleave_size(current_state->graph_state)){
+ MC_restore_snapshot(current_state->system_state);
+ xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
+ XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));
+ MC_UNSET_RAW_MEM;
+ break;
+ }
+ }
+
+ MC_UNSET_RAW_MEM;
+
+ }
+ }
+ MC_UNSET_RAW_MEM;
+ return;
+}
+
+
+
+/************ DPOR 2 (invisible and independant transitions) ************/
+
+xbt_dynar_t reached_pairs_prop;
+xbt_dynar_t visible_transitions;
+xbt_dynar_t enabled_processes;
+
+mc_prop_ato_t new_proposition(char* id, int value){
+ mc_prop_ato_t prop = NULL;
+ prop = xbt_new0(s_mc_prop_ato_t, 1);
+ prop->id = strdup(id);
+ prop->value = value;
+ return prop;
+}
+
+mc_pair_prop_t new_pair_prop(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st){
+ mc_pair_prop_t pair = NULL;
+ pair = xbt_new0(s_mc_pair_prop_t, 1);
+ pair->system_state = sn;
+ pair->automaton_state = st;
+ pair->graph_state = sg;
+ pair->propositions = xbt_dynar_new(sizeof(mc_prop_ato_t), NULL);
+ pair->fully_expanded = 0;
+ pair->interleave = 0;
+ mc_stats_pair->expanded_pairs++;
+ return pair;
+}
+
+int reached_prop(mc_pair_prop_t pair){
+
+ char* hash_reached = malloc(sizeof(char)*160);
+ unsigned int c= 0;
+
+ MC_SET_RAW_MEM;
+ char *hash = malloc(sizeof(char)*160);
+ xbt_sha((char *)&pair, hash);
+ xbt_dynar_foreach(reached_pairs_prop, c, hash_reached){
+ if(strcmp(hash, hash_reached) == 0){
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }
+ }
+
+ MC_UNSET_RAW_MEM;
+ return 0;
+}
+
+void set_pair_prop_reached(mc_pair_prop_t pair){
+
+ if(reached_prop(pair) == 0){
+ MC_SET_RAW_MEM;
+ char *hash = malloc(sizeof(char)*160) ;
+ xbt_sha((char *)&pair, hash);
+ xbt_dynar_push(reached_pairs_prop, &hash);
+ MC_UNSET_RAW_MEM;
+ }
+
+}
+
+int invisible(mc_pair_prop_t p, mc_pair_prop_t np){
+ mc_prop_ato_t prop1;
+ mc_prop_ato_t prop2;
+ int i;
+ for(i=0;i<xbt_dynar_length(p->propositions); i++){
+ prop1 = xbt_dynar_get_as(p->propositions, i, mc_prop_ato_t);
+ prop2 = xbt_dynar_get_as(np->propositions, i, mc_prop_ato_t);
+ //XBT_DEBUG("test invisible : prop 1 = %s : %d / prop 2 = %s : %d", prop1->id, prop1->value, prop2->id, prop2->value);
+ if(prop1->value != prop2->value)
+ return 0;
+ }
+ return 1;
+
+}
+
+void set_fully_expanded(mc_pair_prop_t pair){
+ pair->fully_expanded = 1;
+}
+
+void MC_dpor2_init(xbt_automaton_t a)
+{
+ mc_pair_prop_t initial_pair = NULL;
+ mc_state_t initial_graph_state = NULL;
+ mc_snapshot_t initial_system_state = NULL;
+ xbt_state_t initial_automaton_state = NULL;
+
+
+ MC_SET_RAW_MEM;
+ initial_graph_state = MC_state_new();
+ MC_UNSET_RAW_MEM;
+
+ /* Wait for requests (schedules processes) */
+ MC_wait_for_requests();
+
+ unsigned int cursor = 0;
+ unsigned int cursor2 = 0;
+ xbt_state_t automaton_state = NULL;
+ int res;
+ xbt_transition_t transition_succ;
+
+ xbt_dynar_foreach(a->states, cursor, automaton_state){
+ if(automaton_state->type == -1){
+ xbt_dynar_foreach(automaton_state->out, cursor2, transition_succ){
+ res = MC_automaton_evaluate_label(a, transition_succ->label);
+ if((res == 1) || (res == 2)){
+ initial_automaton_state = transition_succ->dst;
+ break;
+ }
+ }
+ }
+
+ if(initial_automaton_state != NULL)
+ break;
+ }
+
+ if(initial_automaton_state == NULL){
+ cursor = 0;
+ xbt_dynar_foreach(a->states, cursor, automaton_state){
+ if(automaton_state->type == -1){
+ initial_automaton_state = automaton_state;
+ break;
+ }
+ }
+ }
+
+ reached_pairs_prop = xbt_dynar_new(sizeof(char *), NULL);
+ visible_transitions = xbt_dynar_new(sizeof(s_smx_req_t), NULL);
+ enabled_processes = xbt_dynar_new(sizeof(smx_process_t), NULL);
+
+ MC_SET_RAW_MEM;
+ initial_system_state = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot(initial_system_state);
+ initial_pair = new_pair_prop(initial_system_state, initial_graph_state, initial_automaton_state);
+ cursor = 0;
+ xbt_propositional_symbol_t ps;
+ xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+ int (*f)() = ps->function;
+ int val = (*f)();
+ mc_prop_ato_t pa = new_proposition(ps->pred, val);
+ xbt_dynar_push(initial_pair->propositions, &pa);
+ }
+ xbt_fifo_unshift(mc_stack_liveness_stateful, initial_pair);
+ MC_UNSET_RAW_MEM;
+
+
+ XBT_DEBUG("**************************************************");
+ XBT_DEBUG("Initial pair");
+
+ MC_dpor2(a, 0);
+
+}
+
+
+void MC_dpor2(xbt_automaton_t a, int search_cycle)
+{
+ char *req_str;
+ int value;
+ smx_req_t req = NULL, prev_req = NULL;
+ mc_state_t next_graph_state = NULL;
+ mc_snapshot_t next_system_state = NULL;
+ xbt_state_t next_automaton_state = NULL;
+ xbt_transition_t transition_succ;
+ unsigned int cursor;
+ int res;
+ mc_pair_prop_t pair = NULL, next_pair = NULL, prev_pair = NULL;
+ smx_process_t process = NULL;
+ xbt_fifo_item_t item = NULL;
+ int d;
+
+
+ while (xbt_fifo_size(mc_stack_liveness_stateful) > 0) {
+
+ /* Get current pair */
+ pair = (mc_pair_prop_t)
+ xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
+
+ XBT_DEBUG("**************************************************");
+ XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)",
+ xbt_fifo_size(mc_stack_liveness_stateful), pair, MC_state_interleave_size(pair->graph_state));
+
+ if(MC_state_interleave_size(pair->graph_state) == 0){
+
+ xbt_dynar_reset(enabled_processes);
+
+ MC_SET_RAW_MEM;
+
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ xbt_dynar_push(enabled_processes, &process);
+ //XBT_DEBUG("Process : pid=%lu",process->pid);
+ }
+ }
+
+ //XBT_DEBUG("Enabled processes before pop : %lu", xbt_dynar_length(enabled_processes));
+
+ //XBT_DEBUG("Processes already interleaved : %d", pair->interleave);
+
+ if(xbt_dynar_length(enabled_processes) > 0){
+ for(d=0;d<pair->interleave;d++){
+ xbt_dynar_shift(enabled_processes, NULL);
+ }
+ }
+
+ //XBT_DEBUG("Enabled processes after pop : %lu", xbt_dynar_length(enabled_processes));
+
+ if(pair->fully_expanded == 0){
+ if(xbt_dynar_length(enabled_processes) > 0){
+ MC_state_interleave_process(pair->graph_state, xbt_dynar_get_as(enabled_processes, 0, smx_process_t));
+ //XBT_DEBUG("Interleave process");
+ }
+ }
+
+ MC_UNSET_RAW_MEM;
+
+ }
+
+
+ /* Update statistics */
+ mc_stats_pair->visited_pairs++;
+ //sleep(1);
+
+ /*cursor = 0;
+ mc_prop_ato_t pato;
+ xbt_dynar_foreach(pair->propositions, cursor, pato){
+ XBT_DEBUG("%s : %d", pato->id, pato->value);
+ }*/
+
+ /* Test acceptance pair and acceptance cycle*/
+
+ if(pair->automaton_state->type == 1){
+ if(search_cycle == 0){
+ set_pair_prop_reached(pair);
+ XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", pair->graph_state, pair->automaton_state, pair->automaton_state->id);
+ }else{
+ if(reached_prop(pair) == 1){
+ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+ XBT_INFO("| ACCEPTANCE CYCLE |");
+ XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
+ XBT_INFO("Counter-example that violates formula :");
+ MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
+ MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
+ MC_print_statistics_pairs(mc_stats_pair);
+ exit(0);
+ }
+ }
+ }
+
+ /* If there are processes to interleave and the maximum depth has not been reached
+ then perform one step of the exploration algorithm */
+ if (xbt_fifo_size(mc_stack_liveness_stateful) < MAX_DEPTH &&
+ (req = MC_state_get_request(pair->graph_state, &value))) {
+
+ /* Debug information */
+ if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
+ req_str = MC_request_to_string(req, value);
+ XBT_DEBUG("Execute: %s", req_str);
+ xbt_free(req_str);
+ }
+
+ MC_state_set_executed_request(pair->graph_state, req, value);
+ //mc_stats_pairs->executed_transitions++;
+
+ /* Answer the request */
+ SIMIX_request_pre(req, value); /* After this call req is no longer usefull */
+
+ /* Wait for requests (schedules processes) */
+ MC_wait_for_requests();
+
+ /* Create the new expanded state */
+ MC_SET_RAW_MEM;
+
+ pair->interleave++;
+ //XBT_DEBUG("Process interleaved in pair %p : %u", pair, MC_state_interleave_size(pair->graph_state));
+ //xbt_dynar_pop(enabled_processes, NULL);
+
+ next_graph_state = MC_state_new();
+
+ next_system_state = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot(next_system_state);
+ MC_UNSET_RAW_MEM;
+
+ cursor = 0;
+ xbt_dynar_foreach(pair->automaton_state->out, cursor, transition_succ){
+ res = MC_automaton_evaluate_label(a, transition_succ->label);
+ if((res == 1) || (res == 2)){ // enabled transition in automaton
+ next_automaton_state = transition_succ->dst;
+ break;
+ }
