+ xbt_dynar_push(reached_pairs_hash, &pair);
+
+ MC_free_snapshot(sn);
+
+ MC_UNSET_RAW_MEM;
+
+}
+
+
+int visited(xbt_state_t st, int sc){
+
+
+ if(xbt_dynar_is_empty(visited_pairs)){
+
+ return 0;
+
+ }else{
+
+ MC_SET_RAW_MEM;
+
+ mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot_liveness(sn);
+
+ xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
+
+ /* Get values of propositional symbols */
+ unsigned int cursor = 0;
+ xbt_propositional_symbol_t ps = NULL;
+ int res;
+ int_f_void_t f;
+
+ xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
+ f = (int_f_void_t)ps->function;
+ res = (*f)();
+ xbt_dynar_push_as(prop_ato, int, res);
+ }
+
+ cursor = 0;
+ mc_pair_visited_t pair_test = NULL;
+
+ xbt_dynar_foreach(visited_pairs, cursor, pair_test){
+ if(pair_test->search_cycle == sc) {
+ if(automaton_state_compare(pair_test->automaton_state, st) == 0){
+ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+ if(snapshot_compare(pair_test->system_state, sn) == 0){
+
+ MC_free_snapshot(sn);
+ xbt_dynar_reset(prop_ato);
+ xbt_free(prop_ato);
+ MC_UNSET_RAW_MEM;
+
+ return 1;
+
+ }else{
+ XBT_INFO("Different snapshot");
+ }
+ }else{
+ XBT_INFO("Different values of propositional symbols");
+ }
+ }else{
+ XBT_INFO("Different automaton state");
+ }
+ }else{
+ XBT_INFO("Different value of search_cycle");
+ }
+ }
+
+
+ MC_free_snapshot(sn);
+ xbt_dynar_reset(prop_ato);
+ xbt_free(prop_ato);
+ MC_UNSET_RAW_MEM;
+ return 0;
+
+ }
+}
+
+
+int visited_hash(xbt_state_t st, int sc){
+
+
+ if(xbt_dynar_is_empty(visited_pairs_hash)){
+
+ return 0;
+
+ }else{
+
+ MC_SET_RAW_MEM;
+
+ mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot_liveness(sn);
+
+ int j;
+ unsigned int hash_regions[sn->num_reg];
+ for(j=0; j<sn->num_reg; j++){
+ hash_regions[j] = hash_region(sn->regions[j]->data, sn->regions[j]->size);
+ }
+
+
+ /* Get values of propositional symbols */
+ xbt_dynar_t prop_ato = xbt_dynar_new(sizeof(int), NULL);
+ unsigned int cursor = 0;
+ xbt_propositional_symbol_t ps = NULL;
+ int res;
+ int_f_void_t f;
+
+ xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
+ f = (int_f_void_t)ps->function;
+ res = (*f)();
+ xbt_dynar_push_as(prop_ato, int, res);
+ }
+
+ mc_pair_visited_hash_t pair_test = NULL;
+
+ int region_diff = 0;
+ cursor = 0;
+
+ xbt_dynar_foreach(visited_pairs_hash, cursor, pair_test){
+
+ if(pair_test->search_cycle == sc) {
+ if(automaton_state_compare(pair_test->automaton_state, st) == 0){
+ if(propositional_symbols_compare_value(pair_test->prop_ato, prop_ato) == 0){
+ for(j=0 ; j< sn->num_reg ; j++){
+ if(hash_regions[j] != pair_test->hash_regions[j]){
+ region_diff++;
+ }
+ }
+ if(region_diff == 0){
+ MC_free_snapshot(sn);
+ xbt_dynar_reset(prop_ato);
+ xbt_free(prop_ato);
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }else{
+ //XBT_INFO("Different snapshot");
+ }
+ }else{
+ //XBT_INFO("Different values of propositional symbols");
+ }
+ }else{
+ //XBT_INFO("Different automaton state");
+ }
+ }else{
+ //XBT_INFO("Different value of search_cycle");
+ }
+
+ region_diff = 0;
+ }
+
+ MC_free_snapshot(sn);
+ xbt_dynar_reset(prop_ato);
+ xbt_free(prop_ato);
+ MC_UNSET_RAW_MEM;
+ return 0;
+
+ }
+}
+
+void set_pair_visited_hash(xbt_state_t st, int sc){
+
+ MC_SET_RAW_MEM;
+
+ mc_snapshot_t sn = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot_liveness(sn);
+
+ mc_pair_visited_hash_t pair = NULL;
+ pair = xbt_new0(s_mc_pair_visited_hash_t, 1);
+ pair->automaton_state = st;
+ pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+ pair->search_cycle = sc;
+ pair->hash_regions = malloc(sizeof(unsigned int) * sn->num_reg);
+
+ int i;
+
+ for(i=0 ; i< sn->num_reg ; i++){
+ pair->hash_regions[i] = hash_region(sn->regions[i]->data, sn->regions[i]->size);
+ }
+
+ /* Get values of propositional symbols */
+ unsigned int cursor = 0;
+ xbt_propositional_symbol_t ps = NULL;
+ int res;
+ int_f_void_t f;
+
+ xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
+ f = (int_f_void_t)ps->function;
+ res = (*f)();
+ xbt_dynar_push_as(pair->prop_ato, int, res);
+ }
+
+ xbt_dynar_push(visited_pairs_hash, &pair);
+
+ MC_free_snapshot(sn);
+
+ MC_UNSET_RAW_MEM;
+
+}
+
+void set_pair_visited(xbt_state_t st, int sc){
+
+
+ MC_SET_RAW_MEM;
+
+ mc_pair_visited_t pair = NULL;
+ pair = xbt_new0(s_mc_pair_visited_t, 1);
+ pair->automaton_state = st;
+ pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+ pair->search_cycle = sc;
+ pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot_liveness(pair->system_state);
+
+
+ /* Get values of propositional symbols */
+ unsigned int cursor = 0;
+ xbt_propositional_symbol_t ps = NULL;
+ int res;
+ int_f_void_t f;
+
+ xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
+ f = (int_f_void_t)ps->function;
+ res = (*f)();
+ xbt_dynar_push_as(pair->prop_ato, int, res);
+ }
+
+ xbt_dynar_push(visited_pairs, &pair);