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 : New public functions to take a snapshot and compare two snapshots...
[simgrid.git]
/
src
/
mc
/
mc_request.c
diff --git
a/src/mc/mc_request.c
b/src/mc/mc_request.c
index
3d89d84
..
50c7cd2
100644
(file)
--- a/
src/mc/mc_request.c
+++ b/
src/mc/mc_request.c
@@
-11,11
+11,10
@@
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc,
static char* pointer_to_string(void* pointer);
static char* buff_size_to_string(size_t size);
static char* pointer_to_string(void* pointer);
static char* buff_size_to_string(size_t size);
-int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2)
-{
- if(_surf_do_model_check == 2)
+int MC_request_depend(smx_simcall_t r1, smx_simcall_t r2) {
+ if(mc_reduce_kind == e_mc_reduce_none)
return TRUE;
return TRUE;
-
+
if (r1->issuer == r2->issuer)
return FALSE;
if (r1->issuer == r2->issuer)
return FALSE;
@@
-240,6
+239,16
@@
char *MC_request_to_string(smx_simcall_t req, int value)
}
break;
}
break;
+ case SIMCALL_MC_SNAPSHOT:
+ type = xbt_strdup("MC_SNAPSHOT");
+ args = '\0';
+ break;
+
+ case SIMCALL_MC_COMPARE_SNAPSHOTS:
+ type = xbt_strdup("MC_COMPARE_SNAPSHOTS");
+ args = '\0';
+ break;
+
default:
THROW_UNIMPLEMENTED;
}
default:
THROW_UNIMPLEMENTED;
}
@@
-272,7
+281,9
@@
int MC_request_is_visible(smx_simcall_t req)
|| req->call == SIMCALL_COMM_WAIT
|| req->call == SIMCALL_COMM_WAITANY
|| req->call == SIMCALL_COMM_TEST
|| req->call == SIMCALL_COMM_WAIT
|| req->call == SIMCALL_COMM_WAITANY
|| req->call == SIMCALL_COMM_TEST
- || req->call == SIMCALL_COMM_TESTANY;
+ || req->call == SIMCALL_COMM_TESTANY
+ || req->call == SIMCALL_MC_SNAPSHOT
+ || req->call == SIMCALL_MC_COMPARE_SNAPSHOTS;
}
int MC_request_is_enabled(smx_simcall_t req)
}
int MC_request_is_enabled(smx_simcall_t req)