return values;
}
+/** \brief Find a suitable subrange of candidate duplicates for a given state
+ *
+ * See mc_dpor.c with a similar (same?) function.
+ */
static int get_search_interval(xbt_dynar_t all_pairs, mc_visited_pair_t pair, int *min, int *max){
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
index = get_search_interval(acceptance_pairs, pair, &min, &max);
if(min != -1 && max != -1){ // Acceptance pair with same number of processes and same heap bytes used exists
+
+ // Parallell implementation
/*res = xbt_parmap_mc_apply(parmap, snapshot_compare, xbt_dynar_get_ptr(acceptance_pairs, min), (max-min)+1, pair);
if(res != -1){
if(!raw_mem_set)
MC_UNSET_RAW_MEM;
return ((mc_pair_t)xbt_dynar_get_as(acceptance_pairs, (min+res)-1, mc_pair_t))->num;
}*/
+
cursor = min;
while(cursor <= max){
pair_test = (mc_visited_pair_t)xbt_dynar_get_as(acceptance_pairs, cursor, mc_visited_pair_t);
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
- fprintf(stderr, "Search acceptance pair %d\n", pair_num);
-
MC_SET_RAW_MEM;
unsigned int cursor = 0;
MC_UNSET_RAW_MEM;
}
+/** \brief Checks whether a given state has already been visited by the algorithm.
+ *
+ */
static int is_visited_pair(mc_visited_pair_t pair, int pair_num, xbt_automaton_state_t automaton_state, xbt_dynar_t atomic_propositions){
if(_sg_mc_visited == 0)
mc_pair_t next_pair = NULL;
xbt_dynar_t prop_values = NULL;
- int new_pair = 0;
mc_visited_pair_t reached_pair = NULL;
+ int counter_example_depth = 0;
if(xbt_fifo_size(mc_stack_liveness) < _sg_mc_max_depth){
if((current_pair->automaton_state->type == 1) || (current_pair->automaton_state->type == 2)){
if((reached_pair = is_reached_acceptance_pair(current_pair->num, current_pair->automaton_state, current_pair->atomic_propositions)) == NULL){
+ counter_example_depth = xbt_fifo_size(mc_stack_liveness);
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("| ACCEPTANCE CYCLE |");
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
MC_show_stack_liveness(mc_stack_liveness);
MC_dump_stack_liveness(mc_stack_liveness);
MC_print_statistics(mc_stats);
+ XBT_INFO("Counter-example depth : %d", counter_example_depth);
xbt_abort();
}
MC_SET_RAW_MEM;
prop_values = get_atomic_propositions_values();
MC_UNSET_RAW_MEM;
+
+ int new_pair = 0;
/* Evaluate enabled transition according to atomic propositions values */
cursor= 0;