"off" by default.
extern int _sg_mc_checkpoint;
extern char* _sg_mc_property_file;
extern int _sg_mc_timeout;
+extern int _sg_mc_hash;
extern int _sg_mc_max_depth;
extern int _sg_mc_visited;
extern char* _sg_mc_dot_output_file;
void _mc_cfg_cb_checkpoint(const char *name, int pos);
void _mc_cfg_cb_property(const char *name, int pos);
void _mc_cfg_cb_timeout(const char *name, int pos);
+void _mc_cfg_cb_hash(const char *name, int pos);
void _mc_cfg_cb_max_depth(const char *name, int pos);
void _mc_cfg_cb_visited(const char *name, int pos);
void _mc_cfg_cb_dot_output(const char *name, int pos);
if(_sg_mc_visited > 0 || strcmp(_sg_mc_property_file,"")){
snapshot->stacks = MC_take_snapshot_stacks(&snapshot, snapshot->regions[0]->data);
- if(MC_USE_SNAPSHOT_HASH && snapshot->stacks!=NULL) {
+ if(_sg_mc_hash && snapshot->stacks!=NULL) {
snapshot->hash = mc_hash_processes_state(num_state, snapshot->stacks);
} else {
snapshot->hash = 0;
#endif
int hash_result = 0;
- if(MC_USE_SNAPSHOT_HASH) {
+ if(_sg_mc_hash) {
hash_result = (s1->hash != s2->hash);
if(hash_result) {
XBT_VERB("(%d - %d) Different hash : 0x%" PRIx64 "--0x%" PRIx64, num1, num2, s1->hash, s2->hash);
XBT_VERB("(%d - %d) No difference found", num1, num2);
#endif
-#if defined(MC_DEBUG) && defined(MC_VERBOSE) && MC_USE_SNAPSHOT_HASH
- // * false positive SHOULD be avoided.
- // * There MUST not be any false negative.
+#if defined(MC_DEBUG) && defined(MC_VERBOSE)
+ if(_sg_mc_hash) {
+ // * false positive SHOULD be avoided.
+ // * There MUST not be any false negative.
- XBT_VERB("(%d - %d) State equality hash test is %s %s", num1, num2,
- (hash_result!=0) == (errors!=0) ? "true" : "false",
- !hash_result ? "positive" : "negative");
+ XBT_VERB("(%d - %d) State equality hash test is %s %s", num1, num2,
+ (hash_result!=0) == (errors!=0) ? "true" : "false",
+ !hash_result ? "positive" : "negative");
+ }
#endif
return errors > 0 || hash_result;
int _sg_mc_checkpoint=0;
char* _sg_mc_property_file=NULL;
int _sg_mc_timeout=0;
+int _sg_mc_hash=0;
int _sg_mc_max_depth=1000;
int _sg_mc_visited=0;
char *_sg_mc_dot_output_file = NULL;
_sg_mc_timeout= xbt_cfg_get_boolean(_sg_cfg_set, name);
}
+void _mc_cfg_cb_hash(const char *name, int pos) {
+ if (_sg_cfg_init_status && !_sg_do_model_check) {
+ xbt_die("You are specifying a value to enable/disable the use of global hash to speedup state comparaison, but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
+ }
+ _sg_mc_hash= xbt_cfg_get_boolean(_sg_cfg_set, name);
+}
+
void _mc_cfg_cb_max_depth(const char *name, int pos) {
if (_sg_cfg_init_status && !_sg_do_model_check) {
xbt_die("You are specifying a max depth value after the initialization (through MSG_config?), but model-checking was not activated at config time (through --cfg=model-check:1). This won't work, sorry.");
int SIMIX_pre_mc_compare_snapshots(smx_simcall_t simcall, mc_snapshot_t s1, mc_snapshot_t s2);
void print_comparison_times(void);
-//#define MC_DEBUG 1
+#define MC_DEBUG 1
#define MC_VERBOSE 1
-#define MC_USE_SNAPSHOT_HASH 1
/********************************** DPOR for safety property **************************************/
xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_timeout, NULL);
xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/timeout", "no");
+ /* Enable/disable global hash computation with model-checking */
+ xbt_cfg_register(&_sg_cfg_set, "model-check/hash",
+ "Enable/Disable state hash for state comparison",
+ xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_hash, NULL);
+ xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/hash", "no");
+
/* Set max depth exploration */
xbt_cfg_register(&_sg_cfg_set, "model-check/max_depth",
"Specify the max depth of exploration (default : 1000)",