A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
better to use a function that exists than dealing with the underlying
[simgrid.git]
/
src
/
mc
/
mc_liveness.c
diff --git
a/src/mc/mc_liveness.c
b/src/mc/mc_liveness.c
index
f875704
..
678d417
100644
(file)
--- a/
src/mc/mc_liveness.c
+++ b/
src/mc/mc_liveness.c
@@
-274,7
+274,8
@@
void MC_ddfs_init(void){
successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
/* Save the initial state */
successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
/* Save the initial state */
- initial_snapshot_liveness = MC_take_snapshot_liveness();
+ initial_state_liveness = xbt_new0(s_mc_global_t, 1);
+ initial_state_liveness->initial_snapshot = MC_take_snapshot_liveness();
MC_UNSET_RAW_MEM;
MC_UNSET_RAW_MEM;
@@
-290,7
+291,7
@@
void MC_ddfs_init(void){
MC_UNSET_RAW_MEM;
if(cursor != 0){
MC_UNSET_RAW_MEM;
if(cursor != 0){
- MC_restore_snapshot(initial_s
napshot_liveness
);
+ MC_restore_snapshot(initial_s
tate_liveness->initial_snapshot
);
MC_UNSET_RAW_MEM;
}
MC_UNSET_RAW_MEM;
}
@@
-307,7
+308,7
@@
void MC_ddfs_init(void){
set_pair_reached(state);
if(cursor != 0){
set_pair_reached(state);
if(cursor != 0){
- MC_restore_snapshot(initial_s
napshot_liveness
);
+ MC_restore_snapshot(initial_s
tate_liveness->initial_snapshot
);
MC_UNSET_RAW_MEM;
}
MC_UNSET_RAW_MEM;
}
@@
-344,7
+345,7
@@
void MC_ddfs(int search_cycle){
_mc_property_automaton->current_state = current_pair->automaton_state;
_mc_property_automaton->current_state = current_pair->automaton_state;
- XBT_
INFO
("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
+ XBT_
DEBUG
("********************* ( Depth = %d, search_cycle = %d )", xbt_fifo_size(mc_stack_liveness), search_cycle);
mc_stats_pair->visited_pairs++;
mc_stats_pair->visited_pairs++;
@@
-371,7
+372,7
@@
void MC_ddfs(int search_cycle){
/* Debug information */
req_str = MC_request_to_string(req, value);
/* Debug information */
req_str = MC_request_to_string(req, value);
- XBT_
INFO
("Execute: %s", req_str);
+ XBT_
DEBUG
("Execute: %s", req_str);
xbt_free(req_str);
MC_state_set_executed_request(current_pair->graph_state, req, value);
xbt_free(req_str);
MC_state_set_executed_request(current_pair->graph_state, req, value);
@@
-451,9
+452,9
@@
void MC_ddfs(int search_cycle){
}else{
}else{
- XBT_
INFO
("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
+ XBT_
DEBUG
("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
- XBT_
INFO
("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ XBT_
DEBUG
("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
MC_SET_RAW_MEM;
xbt_fifo_unshift(mc_stack_liveness, pair_succ);
MC_SET_RAW_MEM;
xbt_fifo_unshift(mc_stack_liveness, pair_succ);
@@
-477,13
+478,13
@@
void MC_ddfs(int search_cycle){
if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
if(((pair_succ->automaton_state->type == 1) || (pair_succ->automaton_state->type == 2))){
- XBT_
INFO
("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
+ XBT_
DEBUG
("Next pair (depth =%d) -> Acceptance pair (%s)", xbt_fifo_size(mc_stack_liveness) + 1, pair_succ->automaton_state->id);
set_pair_reached(pair_succ->automaton_state);
search_cycle = 1;
set_pair_reached(pair_succ->automaton_state);
search_cycle = 1;
- XBT_
INFO
("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
+ XBT_
DEBUG
("Reached pairs : %lu", xbt_dynar_length(reached_pairs));
}
}
@@
-504,7
+505,7
@@
void MC_ddfs(int search_cycle){
}
if(MC_state_interleave_size(current_pair->graph_state) > 0){
}
if(MC_state_interleave_size(current_pair->graph_state) > 0){
- XBT_
INFO
("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
+ XBT_
DEBUG
("Backtracking to depth %d", xbt_fifo_size(mc_stack_liveness));
MC_replay_liveness(mc_stack_liveness, 0);
}
}
MC_replay_liveness(mc_stack_liveness, 0);
}
}
@@
-514,14
+515,14
@@
void MC_ddfs(int search_cycle){
}else{
}else{
- XBT_
INFO
("Max depth reached");
+ XBT_
DEBUG
("Max depth reached");
}
if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
}
if(xbt_fifo_size(mc_stack_liveness) == MAX_DEPTH_LIVENESS ){
- XBT_
INFO
("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
+ XBT_
DEBUG
("Pair (depth = %d) shifted in stack, maximum depth reached", xbt_fifo_size(mc_stack_liveness) );
}else{
}else{
- XBT_
INFO
("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
+ XBT_
DEBUG
("Pair (depth = %d) shifted in stack", xbt_fifo_size(mc_stack_liveness) );
}
}