+xbt_dynar_t reached_pairs_prop;
+
+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);
+ 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;
+ }
+
+}
+