+int visited(xbt_state_t st){
+
+ if(_sg_mc_visited == 0)
+ return 0;
+
+ int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
+
+ MC_SET_RAW_MEM;
+
+ mc_pair_visited_t new_pair = NULL;
+ new_pair = xbt_new0(s_mc_pair_visited_t, 1);
+ new_pair->automaton_state = st;
+ new_pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+ new_pair->system_state = MC_take_snapshot();
+
+ /* Get values of propositional symbols */
+ int res;
+ int_f_void_t f;
+ unsigned int cursor = 0;
+ xbt_propositional_symbol_t ps = NULL;
+ xbt_dynar_foreach(_mc_property_automaton->propositional_symbols, cursor, ps){
+ f = (int_f_void_t)ps->function;
+ res = (*f)();
+ xbt_dynar_push_as(new_pair->prop_ato, int, res);
+ }
+
+ MC_UNSET_RAW_MEM;
+
+ if(xbt_dynar_is_empty(visited_pairs)){
+
+ MC_SET_RAW_MEM;
+ /* New pair visited */
+ xbt_dynar_push(visited_pairs, &new_pair);
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+ return 0;
+
+ }else{
+
+ MC_SET_RAW_MEM;
+
+ cursor = 0;
+ mc_pair_visited_t pair_test = NULL;
+
+ xbt_dynar_foreach(visited_pairs, cursor, pair_test){
+ if(XBT_LOG_ISENABLED(mc_liveness, xbt_log_priority_debug))
+ XBT_DEBUG("****** Pair visited #%d ******", cursor + 1);
+ if(automaton_state_compare(pair_test->automaton_state, st) == 0){
+ if(propositional_symbols_compare_value(pair_test->prop_ato, new_pair->prop_ato) == 0){
+ if(snapshot_compare(new_pair->system_state, pair_test->system_state) == 0){
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+ else
+ MC_UNSET_RAW_MEM;
+
+ return 1;
+ }
+ }else{
+ XBT_DEBUG("Different values of propositional symbols");
+ }
+ }else{
+ XBT_DEBUG("Different automaton state");
+ }
+ }
+
+ if(xbt_dynar_length(visited_pairs) == _sg_mc_visited){
+ xbt_dynar_remove_at(visited_pairs, 0, NULL);
+ }
+
+ /* New pair visited */
+ xbt_dynar_push(visited_pairs, &new_pair);
+
+ MC_UNSET_RAW_MEM;
+
+ if(raw_mem_set)
+ MC_SET_RAW_MEM;
+
+ return 0;
+
+ }
+}
+