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
model-checker : fix dpor
[simgrid.git]
/
src
/
mc
/
mc_dpor.c
diff --git
a/src/mc/mc_dpor.c
b/src/mc/mc_dpor.c
index
1768a12
..
c52988b
100644
(file)
--- a/
src/mc/mc_dpor.c
+++ b/
src/mc/mc_dpor.c
@@
-28,7
+28,7
@@
static void visited_state_free_voidp(void *s){
static int is_visited_state(){
if(_sg_mc_visited == 0)
static int is_visited_state(){
if(_sg_mc_visited == 0)
- return
0
;
+ return
-1
;
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
int raw_mem_set = (mmalloc_get_current_heap() == raw_heap);
@@
-50,7
+50,7
@@
static int is_visited_state(){
if(raw_mem_set)
MC_SET_RAW_MEM;
if(raw_mem_set)
MC_SET_RAW_MEM;
- return
0
;
+ return
-1
;
}else{
}else{
@@
-85,7
+85,7
@@
static int is_visited_state(){
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
- return
1
;
+ return
state_test->num
;
}else{
/* Search another state with same number of bytes used */
previous_cursor = cursor - 1;
}else{
/* Search another state with same number of bytes used */
previous_cursor = cursor - 1;
@@
-102,7
+102,7
@@
static int is_visited_state(){
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
- return
1
;
+ return
state_test->num
;
}
previous_cursor--;
}
}
previous_cursor--;
}
@@
-120,7
+120,7
@@
static int is_visited_state(){
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
MC_SET_RAW_MEM;
else
MC_UNSET_RAW_MEM;
- return
1
;
+ return
state_test->num
;
}
next_cursor++;
}
}
next_cursor++;
}
@@
-154,7
+154,7
@@
static int is_visited_state(){
if(raw_mem_set)
MC_SET_RAW_MEM;
if(raw_mem_set)
MC_SET_RAW_MEM;
- return
0
;
+ return
-1
;
}
}
}
}
@@
-222,6
+222,7
@@
void MC_dpor(void)
xbt_fifo_item_t item = NULL;
int pos, i, interleave_size;
int interleave_proc[simix_process_maxpid];
xbt_fifo_item_t item = NULL;
int pos, i, interleave_size;
int interleave_proc[simix_process_maxpid];
+ int visited_state;
while (xbt_fifo_size(mc_stack_safety) > 0) {
while (xbt_fifo_size(mc_stack_safety) > 0) {
@@
-248,6
+249,8
@@
void MC_dpor(void)
XBT_DEBUG("Execute: %s", req_str);
xbt_free(req_str);
}
XBT_DEBUG("Execute: %s", req_str);
xbt_free(req_str);
}
+
+ req_str = MC_request_get_dot_output(req, value);
MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
@@
-295,7
+298,7
@@
void MC_dpor(void)
next_state = MC_state_new();
next_state = MC_state_new();
- if(
!is_visited_state()
){
+ if(
(visited_state = is_visited_state()) == -1
){
/* Get an enabled process and insert it in the interleave set of the next state */
xbt_swag_foreach(process, simix_global->process_list){
/* Get an enabled process and insert it in the interleave set of the next state */
xbt_swag_foreach(process, simix_global->process_list){
@@
-309,11
+312,23
@@
void MC_dpor(void)
next_state->system_state = MC_take_snapshot();
}
next_state->system_state = MC_take_snapshot();
}
+ if(dot_output != NULL)
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
+
+ }else{
+
+ if(dot_output != NULL)
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, visited_state, req_str);
+
}
}
+
+
xbt_fifo_unshift(mc_stack_safety, next_state);
MC_UNSET_RAW_MEM;
xbt_fifo_unshift(mc_stack_safety, next_state);
MC_UNSET_RAW_MEM;
+ xbt_free(req_str);
+
/* Let's loop again */
/* The interleave set is empty or the maximum depth is reached, let's back-track */
/* Let's loop again */
/* The interleave set is empty or the maximum depth is reached, let's back-track */