/* do liveness model-checking */
xbt_cfg_register(&_sg_cfg_set, "model-check/property",
"Specify the name of the file containing the property. It must be the result of the ltl2ba program.",
- xbt_cfgelm_string, 0, 1, _mc_cfg_cb_property, NULL);
+ xbt_cfgelm_string, 1, 1, _mc_cfg_cb_property, NULL);
xbt_cfg_setdefault_string(_sg_cfg_set, "model-check/property", "");
- xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_comms_determinism, NULL);
+ /* do communications determinism model-checking */
+ xbt_cfg_register(&_sg_cfg_set, "model-check/communications_determinism",
+ "Enable/disable the detection of determinism in the communications schemes",
- xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_send_determinism, NULL);
++ xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_comms_determinism, NULL);
+ xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/communications_determinism", "no");
+
+ /* do send determinism model-checking */
+ xbt_cfg_register(&_sg_cfg_set, "model-check/send_determinism",
+ "Enable/disable the detection of send-determinism in the communications schemes",
++ xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_send_determinism, NULL);
+ xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/send_determinism", "no");
+
/* Specify the kind of model-checking reduction */
xbt_cfg_register(&_sg_cfg_set, "model-check/reduction",
"Specify the kind of exploration reduction (either none or DPOR)",
/* Enable/disable timeout for wait requests with model-checking */
xbt_cfg_register(&_sg_cfg_set, "model-check/timeout",
"Enable/Disable timeout for wait requests",
- xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_timeout, NULL);
+ xbt_cfgelm_boolean, 1, 1, _mc_cfg_cb_timeout, NULL);
xbt_cfg_setdefault_boolean(_sg_cfg_set, "model-check/timeout", "no");
- xbt_cfgelm_boolean, 0, 1, _mc_cfg_cb_hash, NULL);
+ /* 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, 1, 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)",
int i, j;
- heaplimit = ((struct mdesc *)heap1)->heaplimit;
+ state->heaplimit = ((struct mdesc *)heap1)->heaplimit;
- s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize;
- state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - getpagesize();
++ state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize;
- heapbase1 = (char *)heap1 + BLOCKSIZE;
- heapbase2 = (char *)heap2 + BLOCKSIZE;
+ state->heapbase1 = (char *)heap1 + BLOCKSIZE;
+ state->heapbase2 = (char *)heap2 + BLOCKSIZE;
- heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)((struct mdesc *)heap1)->heapinfo - (char *)s_heap)));
- heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)((struct mdesc *)heap2)->heapinfo - (char *)s_heap)));
+ state->heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)((struct mdesc *)heap1)->heapinfo - (char *)state->s_heap)));
+ state->heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)((struct mdesc *)heap2)->heapinfo - (char *)state->s_heap)));
- heapsize1 = heap1->heapsize;
- heapsize2 = heap2->heapsize;
+ state->heapsize1 = heap1->heapsize;
+ state->heapsize2 = heap2->heapsize;
- to_ignore1 = i1;
- to_ignore2 = i2;
+ state->to_ignore1 = i1;
+ state-> to_ignore2 = i2;
- equals_to1 = malloc(heaplimit * sizeof(heap_area_t *));
- types1 = malloc(heaplimit * sizeof(type_name *));
- for(i=0; i<=heaplimit; i++){
- equals_to1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(heap_area_t));
- types1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(type_name));
+ state->equals_to1 = malloc(state->heaplimit * sizeof(heap_area_t *));
+ state->types1 = malloc(state->heaplimit * sizeof(type_name *));
+ for(i=0; i<=state->heaplimit; i++){
+ state->equals_to1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(heap_area_t));
+ state->types1[i] = malloc(MAX_FRAGMENT_PER_BLOCK * sizeof(type_name));
for(j=0; j<MAX_FRAGMENT_PER_BLOCK; j++){
- equals_to1[i][j] = NULL;
- types1[i][j] = NULL;
+ state->equals_to1[i][j] = NULL;
+ state->types1[i][j] = NULL;
}
}
}
/* Heap information */
- heaplimit = ((struct mdesc *)heap1)->heaplimit;
+ state->heaplimit = ((struct mdesc *)heap1)->heaplimit;
- s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize;
- state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - getpagesize();
++ state->s_heap = (char *)mmalloc_get_current_heap() - STD_HEAP_SIZE - xbt_pagesize;
- heapbase1 = (char *)heap1 + BLOCKSIZE;
- heapbase2 = (char *)heap2 + BLOCKSIZE;
+ state->heapbase1 = (char *)heap1 + BLOCKSIZE;
+ state->heapbase2 = (char *)heap2 + BLOCKSIZE;
- heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)heap1->heapinfo - (char *)s_heap)));
- heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)heap2->heapinfo - (char *)s_heap)));
+ state->heapinfo1 = (malloc_info *)((char *)heap1 + ((uintptr_t)((char *)heap1->heapinfo - (char *)state->s_heap)));
+ state->heapinfo2 = (malloc_info *)((char *)heap2 + ((uintptr_t)((char *)heap2->heapinfo - (char *)state->s_heap)));
- heapsize1 = heap1->heapsize;
- heapsize2 = heap2->heapsize;
+ state->heapsize1 = heap1->heapsize;
+ state->heapsize2 = heap2->heapsize;
/* Start comparison */
size_t i, j, k;