+}
+
+int visited(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t s, int sc){
+
+
+ if(xbt_fifo_size(visited_pairs) == 0){
+
+ return 0;
+
+ }else{
+
+ MC_SET_RAW_MEM;
+
+ 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;
+ xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+ int (*f)() = ps->function;
+ int res = (*f)();
+ xbt_dynar_push_as(prop_ato, int, res);
+ }
+
+
+
+ int i=0;
+ xbt_fifo_item_t item = xbt_fifo_get_first_item(visited_pairs);
+ mc_pair_visited_t pair_test = NULL;
+
+ while(i < xbt_fifo_size(visited_pairs)){
+
+ pair_test = (mc_pair_visited_t) xbt_fifo_get_item_content(item);
+
+ 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(s, pair_test->system_state) == 0){
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }
+ }
+ }
+ }
+
+ item = xbt_fifo_get_next_item(item);
+
+ i++;
+
+ }
+
+ MC_UNSET_RAW_MEM;
+ return 0;
+
+ }
+}
+
+void set_pair_visited(xbt_automaton_t a, xbt_state_t st, mc_snapshot_t sn, 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->system_state = sn;
+ pair->search_cycle = sc;
+
+ /* Get values of propositional symbols */
+ unsigned int cursor = 0;
+ xbt_propositional_symbol_t ps = NULL;
+ xbt_dynar_foreach(a->propositional_symbols, cursor, ps){
+ int (*f)() = ps->function;
+ int res = (*f)();
+ xbt_dynar_push_as(pair->prop_ato, int, res);
+ }
+
+ xbt_fifo_unshift(visited_pairs, pair);
+
+ MC_UNSET_RAW_MEM;
+
+
