- char *hash = malloc(sizeof(char)*160) ;
- xbt_sha((char *)&pair, hash);
- xbt_dynar_push(reached_pairs, &hash);
+
+ mc_pair_reached_t pair = NULL;
+ pair = xbt_new0(s_mc_pair_reached_t, 1);
+ pair->automaton_state = a->current_state;
+ pair->prop_ato = xbt_dynar_new(sizeof(int), NULL);
+ pair->system_state = xbt_new0(s_mc_snapshot_t, 1);
+ MC_take_snapshot(pair->system_state);
+
+ /* 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(pair->prop_ato, &res);
+ }
+
+ cursor = 0;
+ mc_pair_reached_t pair_test;
+
+ xbt_dynar_foreach(reached_pairs, cursor, pair_test){
+ if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
+ if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, propositional_symbols_compare_value) == 0){
+ if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }
+ }
+ }
+ }
+