int main(int argc, char *argv[])
{
-
+
MSG_global_init(&argc, argv);
MSG_create_environment("platform.xml");
MSG_launch_application("deploy_bugged1.xml");
MSG_main_stateful();
-
+
MSG_clean();
-
+
return 0;
-}
+}
\ No newline at end of file
--- /dev/null
+/******************** Non-deterministic message ordering *********************/
+/* Server assumes a fixed order in the reception of messages from its clients */
+/* which is incorrect because the message ordering is non-deterministic */
+/******************************************************************************/
+
+#include <msg/msg.h>
+#include <mc/modelchecker.h>
+#define N 3
+
+XBT_LOG_NEW_DEFAULT_CATEGORY(example, "this example");
+
+int server(int argc, char *argv[]);
+int client(int argc, char *argv[]);
+
+int server(int argc, char *argv[])
+{
+ m_task_t task1, task2;
+ long val1, val2;
+
+ MSG_task_receive(&task1, "mymailbox");
+ val1 = (long) MSG_task_get_data(task1);
+ MSG_task_destroy(task1);
+ task1 = NULL;
+ XBT_INFO("Received %lu", val1);
+
+ MSG_task_receive(&task2, "mymailbox");
+ val2 = (long) MSG_task_get_data(task2);
+ MSG_task_destroy(task2);
+ task2 = NULL;
+ XBT_INFO("Received %lu", val2);
+
+ MC_assert_stateful(min(val1, val2) == 1);
+
+ MSG_task_receive(&task1, "mymailbox");
+ val1 = (long) MSG_task_get_data(task1);
+ MSG_task_destroy(task1);
+ XBT_INFO("Received %lu", val1);
+
+ MSG_task_receive(&task2, "mymailbox");
+ val2 = (long) MSG_task_get_data(task2);
+ MSG_task_destroy(task2);
+ XBT_INFO("Received %lu", val2);
+
+ XBT_INFO("OK");
+ return 0;
+}
+
+int client(int argc, char *argv[])
+{
+ m_task_t task1 =
+ MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
+ m_task_t task2 =
+ MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
+
+ XBT_INFO("Send %d!", atoi(argv[1]));
+ MSG_task_send(task1, "mymailbox");
+
+ XBT_INFO("Send %d!", atoi(argv[1]));
+ MSG_task_send(task2, "mymailbox");
+
+ return 0;
+}
+
+int main(int argc, char *argv[])
+{
+ MSG_global_init(&argc, argv);
+
+ MSG_create_environment("platform.xml");
+
+ MSG_function_register("server", server);
+
+ MSG_function_register("client", client);
+
+ MSG_launch_application("deploy_bugged2.xml");
+
+ MSG_main_stateful();
+
+ return 0;
+}
//XBT_INFO("r (server) = %d", r);
}
- MC_assert_pair(atoi(MSG_task_get_name(task)) == 3);
+ MC_assert_pair_stateful(atoi(MSG_task_get_name(task)) == 3);
XBT_INFO("OK");
return 0;
//XBT_INFO("r=%d", r);
- MSG_main_with_automaton(automaton);
+ MSG_main_liveness_stateful(automaton);
MSG_clean();
XBT_PUBLIC(void) MC_assert(int);
XBT_PUBLIC(void) MC_assert_stateful(int);
-XBT_PUBLIC(void) MC_assert_pair(int);
+XBT_PUBLIC(void) MC_assert_pair_stateful(int);
+XBT_PUBLIC(void) MC_assert_pair_stateless(int);
XBT_PUBLIC(int) MC_random(int min, int max);
XBT_PUBLIC(int) MSG_get_channel_number(void);
XBT_PUBLIC(MSG_error_t) MSG_main(void);
XBT_PUBLIC(MSG_error_t) MSG_main_stateful(void);
-XBT_PUBLIC(MSG_error_t) MSG_main_with_automaton(xbt_automaton_t a);
+XBT_PUBLIC(MSG_error_t) MSG_main_liveness_stateful(xbt_automaton_t a);
+XBT_PUBLIC(MSG_error_t) MSG_main_liveness_stateless(xbt_automaton_t a);
XBT_PUBLIC(MSG_error_t) MSG_clean(void);
XBT_PUBLIC(void) MSG_function_register(const char *name,
xbt_main_func_t code);
SG_BEGIN_DECL()
/********************************* Global *************************************/
-XBT_PUBLIC(void) MC_init(void);
-XBT_PUBLIC(void) MC_init_stateful(void);
-XBT_PUBLIC(void) MC_init_with_automaton(xbt_automaton_t a);
+XBT_PUBLIC(void) MC_init_safety_stateless(void);
+XBT_PUBLIC(void) MC_init_safety_stateful(void);
+XBT_PUBLIC(void) MC_init_liveness_stateful(xbt_automaton_t a);
+XBT_PUBLIC(void) MC_init_liveness_stateless(xbt_automaton_t a);
XBT_PUBLIC(void) MC_exit(void);
+XBT_PUBLIC(void) MC_exit_liveness(void);
XBT_PUBLIC(void) MC_assert(int);
XBT_PUBLIC(void) MC_assert_stateful(int);
-XBT_PUBLIC(void) MC_assert_pair(int);
+XBT_PUBLIC(void) MC_assert_pair_stateful(int);
+XBT_PUBLIC(void) MC_assert_pair_stateless(int);
XBT_PUBLIC(void) MC_modelcheck(void);
XBT_PUBLIC(void) MC_modelcheck_stateful(void);
-XBT_PUBLIC(void) MC_modelcheck_with_automaton(xbt_automaton_t a);
+XBT_PUBLIC(void) MC_modelcheck_liveness_stateful(xbt_automaton_t a);
+XBT_PUBLIC(void) MC_modelcheck_liveness_stateless(xbt_automaton_t a);
XBT_PUBLIC(int) MC_random(int, int);
XBT_PUBLIC(void) MC_process_clock_add(smx_process_t, double);
XBT_PUBLIC(double) MC_process_clock_get(smx_process_t);
/* Create the initial state and push it into the exploration stack */
MC_SET_RAW_MEM;
initial_state = MC_state_new();
- xbt_fifo_unshift(mc_stack, initial_state);
+ xbt_fifo_unshift(mc_stack_safety_stateless, initial_state);
MC_UNSET_RAW_MEM;
XBT_DEBUG("**************************************************");
smx_process_t process = NULL;
xbt_fifo_item_t item = NULL;
- while (xbt_fifo_size(mc_stack) > 0) {
+ while (xbt_fifo_size(mc_stack_safety_stateless) > 0) {
/* Get current state */
state = (mc_state_t)
- xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack));
+ xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateless));
XBT_DEBUG("**************************************************");
XBT_DEBUG("Exploration depth=%d (state=%p)(%u interleave)",
- xbt_fifo_size(mc_stack), state,
+ xbt_fifo_size(mc_stack_safety_stateless), state,
MC_state_interleave_size(state));
/* Update statistics */
/* If there are processes to interleave and the maximum depth has not been reached
then perform one step of the exploration algorithm */
- if (xbt_fifo_size(mc_stack) < MAX_DEPTH &&
+ if (xbt_fifo_size(mc_stack_safety_stateless) < MAX_DEPTH &&
(req = MC_state_get_request(state, &value))) {
/* Debug information */
/* Create the new expanded state */
MC_SET_RAW_MEM;
next_state = MC_state_new();
- xbt_fifo_unshift(mc_stack, next_state);
+ xbt_fifo_unshift(mc_stack_safety_stateless, next_state);
/* Get an enabled process and insert it in the interleave set of the next state */
xbt_swag_foreach(process, simix_global->process_list){
/* Trash the current state, no longer needed */
MC_SET_RAW_MEM;
- xbt_fifo_shift(mc_stack);
+ xbt_fifo_shift(mc_stack_safety_stateless);
MC_state_delete(state);
MC_UNSET_RAW_MEM;
(from it's predecesor state), depends on any other previous request
executed before it. If it does then add it to the interleave set of the
state that executed that previous request. */
- while ((state = xbt_fifo_shift(mc_stack)) != NULL) {
+ while ((state = xbt_fifo_shift(mc_stack_safety_stateless)) != NULL) {
req = MC_state_get_internal_request(state);
- xbt_fifo_foreach(mc_stack, item, prev_state, mc_state_t) {
+ xbt_fifo_foreach(mc_stack_safety_stateless, item, prev_state, mc_state_t) {
if(MC_request_depend(req, MC_state_get_internal_request(prev_state))){
if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
XBT_DEBUG("Dependent Transitions:");
}
if (MC_state_interleave_size(state)) {
/* We found a back-tracking point, let's loop */
- xbt_fifo_unshift(mc_stack, state);
- XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack));
+ xbt_fifo_unshift(mc_stack_safety_stateless, state);
+ XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateless));
MC_UNSET_RAW_MEM;
- MC_replay(mc_stack);
+ MC_replay(mc_stack_safety_stateless);
break;
} else {
MC_state_delete(state);
}
-/********************* DPOR without replay *********************/
+/********************* DPOR stateful *********************/
mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs){
mc_state_ws_t sws = NULL;
MC_take_snapshot(initial_system_snapshot);
initial_state = new_state_ws(initial_system_snapshot, initial_graph_state);
- xbt_fifo_unshift(mc_snapshot_stack, initial_state);
+ xbt_fifo_unshift(mc_stack_safety_stateful, initial_state);
MC_UNSET_RAW_MEM;
smx_process_t process = NULL;
- if(xbt_fifo_size(mc_snapshot_stack) == 0)
+ if(xbt_fifo_size(mc_stack_safety_stateful) == 0)
return;
int value;
mc_state_ws_t prev_state;
mc_state_ws_t next_state;
- while(xbt_fifo_size(mc_snapshot_stack) > 0){
+ while(xbt_fifo_size(mc_stack_safety_stateful) > 0){
- current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+ current_state = (mc_state_ws_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_safety_stateful));
XBT_DEBUG("**************************************************");
- XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_snapshot_stack),current_state, MC_state_interleave_size(current_state->graph_state));
+ XBT_DEBUG("Depth : %d, State : %p , %u interleave", xbt_fifo_size(mc_stack_safety_stateful),current_state, MC_state_interleave_size(current_state->graph_state));
mc_stats->visited_states++;
-
+ if(mc_stats->expanded_states>1100)
+ exit(0);
+ //sleep(1);
- if((xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
+ if((xbt_fifo_size(mc_stack_safety_stateful) < MAX_DEPTH) && (req = MC_state_get_request(current_state->graph_state, &value))){
/* Debug information */
if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
req_str = MC_request_to_string(req, value);
- XBT_DEBUG("Execute: %s", req_str);
+ //XBT_INFO("Visited states = %lu",mc_stats->visited_states );
+ XBT_DEBUG("Execute: %s",req_str);
xbt_free(req_str);
}
MC_take_snapshot(next_snapshot);
next_state = new_state_ws(next_snapshot, next_graph_state);
- xbt_fifo_unshift(mc_snapshot_stack, next_state);
+ xbt_fifo_unshift(mc_stack_safety_stateful, next_state);
MC_UNSET_RAW_MEM;
/* Trash the current state, no longer needed */
MC_SET_RAW_MEM;
- xbt_fifo_shift(mc_snapshot_stack);
+ xbt_fifo_shift(mc_stack_safety_stateful);
MC_UNSET_RAW_MEM;
/* Check for deadlocks */
}
MC_SET_RAW_MEM;
- while((current_state = xbt_fifo_shift(mc_snapshot_stack)) != NULL){
+ while((current_state = xbt_fifo_shift(mc_stack_safety_stateful)) != NULL){
req = MC_state_get_internal_request(current_state->graph_state);
- xbt_fifo_foreach(mc_snapshot_stack, item, prev_state, mc_state_ws_t) {
+ xbt_fifo_foreach(mc_stack_safety_stateful, item, prev_state, mc_state_ws_t) {
if(MC_request_depend(req, MC_state_get_internal_request(prev_state->graph_state))){
if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
XBT_DEBUG("Dependent Transitions:");
if(MC_state_interleave_size(current_state->graph_state)){
MC_restore_snapshot(current_state->system_state);
- xbt_fifo_unshift(mc_snapshot_stack, current_state);
- XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
+ xbt_fifo_unshift(mc_stack_safety_stateful, current_state);
+ XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_safety_stateful));
MC_UNSET_RAW_MEM;
break;
}
}
}
- if(xbt_fifo_size(mc_snapshot_stack) > 0)
+ if(initial_automaton_state != NULL)
break;
}
- if(xbt_fifo_size(mc_snapshot_stack) == 0){
+ if(initial_automaton_state == NULL){
cursor = 0;
xbt_dynar_foreach(a->states, cursor, automaton_state){
if(automaton_state->type == -1){
mc_prop_ato_t pa = new_proposition(ps->pred, val);
xbt_dynar_push(initial_pair->propositions, &pa);
}
- xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
+ xbt_fifo_unshift(mc_stack_liveness_stateful, initial_pair);
MC_UNSET_RAW_MEM;
int d;
- while (xbt_fifo_size(mc_snapshot_stack) > 0) {
+ while (xbt_fifo_size(mc_stack_liveness_stateful) > 0) {
/* Get current pair */
pair = (mc_pair_prop_t)
- xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+ xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
XBT_DEBUG("**************************************************");
XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)",
- xbt_fifo_size(mc_snapshot_stack), pair, MC_state_interleave_size(pair->graph_state));
+ xbt_fifo_size(mc_stack_liveness_stateful), pair, MC_state_interleave_size(pair->graph_state));
if(MC_state_interleave_size(pair->graph_state) == 0){
XBT_INFO("| ACCEPTANCE CYCLE |");
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("Counter-example that violates formula :");
- MC_show_snapshot_stack(mc_snapshot_stack);
- MC_dump_snapshot_stack(mc_snapshot_stack);
+ MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
+ MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
MC_print_statistics_pairs(mc_stats_pair);
exit(0);
}
/* If there are processes to interleave and the maximum depth has not been reached
then perform one step of the exploration algorithm */
- if (xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH &&
+ if (xbt_fifo_size(mc_stack_liveness_stateful) < MAX_DEPTH &&
(req = MC_state_get_request(pair->graph_state, &value))) {
/* Debug information */
xbt_dynar_push(next_pair->propositions, &pa);
//XBT_DEBUG("%s : %d", pa->id, pa->value);
}
- xbt_fifo_unshift(mc_snapshot_stack, next_pair);
+ xbt_fifo_unshift(mc_stack_liveness_stateful, next_pair);
cursor = 0;
if((invisible(pair, next_pair) == 0) && (pair->fully_expanded == 0)){
/* Trash the current state, no longer needed */
MC_SET_RAW_MEM;
- xbt_fifo_shift(mc_snapshot_stack);
+ xbt_fifo_shift(mc_stack_liveness_stateful);
//MC_state_delete(state);
MC_UNSET_RAW_MEM;
(from it's predecesor state), depends on any other previous request
executed before it. If it does then add it to the interleave set of the
state that executed that previous request. */
- while ((pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL) {
+ while ((pair = xbt_fifo_shift(mc_stack_liveness_stateful)) != NULL) {
req = MC_state_get_internal_request(pair->graph_state);
- xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pair_prop_t) {
+ xbt_fifo_foreach(mc_stack_liveness_stateful, item, prev_pair, mc_pair_prop_t) {
if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
XBT_DEBUG("Dependent Transitions:");
if (MC_state_interleave_size(pair->graph_state) > 0) {
/* We found a back-tracking point, let's loop */
MC_restore_snapshot(pair->system_state);
- xbt_fifo_unshift(mc_snapshot_stack, pair);
- XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
+ xbt_fifo_unshift(mc_stack_liveness_stateful, pair);
+ XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_liveness_stateful));
MC_UNSET_RAW_MEM;
break;
} else {
mc_prop_ato_t pa = new_proposition(ps->pred, val);
xbt_dynar_push(initial_pair->propositions, &pa);
}
- xbt_fifo_unshift(mc_snapshot_stack, initial_pair);
+ xbt_fifo_unshift(mc_stack_liveness_stateful, initial_pair);
MC_UNSET_RAW_MEM;
int d;
- while (xbt_fifo_size(mc_snapshot_stack) > 0) {
+ while (xbt_fifo_size(mc_stack_liveness_stateful) > 0) {
/* Get current pair */
pair = (mc_pair_prop_col_t)
- xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+ xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
XBT_DEBUG("**************************************************");
XBT_DEBUG("Exploration depth=%d (pair=%p) (%d interleave)",
- xbt_fifo_size(mc_snapshot_stack), pair, MC_state_interleave_size(pair->graph_state));
+ xbt_fifo_size(mc_stack_liveness_stateful), pair, MC_state_interleave_size(pair->graph_state));
if(MC_state_interleave_size(pair->graph_state) == 0){
XBT_INFO("| ACCEPTANCE CYCLE |");
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("Counter-example that violates formula :");
- MC_show_snapshot_stack(mc_snapshot_stack);
- MC_dump_snapshot_stack(mc_snapshot_stack);
+ MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
+ MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
MC_print_statistics_pairs(mc_stats_pair);
exit(0);
}
/* If there are processes to interleave and the maximum depth has not been reached
then perform one step of the exploration algorithm */
- if (xbt_fifo_size(mc_snapshot_stack) < MAX_DEPTH &&
+ if (xbt_fifo_size(mc_stack_liveness_stateful) < MAX_DEPTH &&
(req = MC_state_get_request(pair->graph_state, &value))) {
set_pair_prop_col_visited(pair, search_cycle);
mc_prop_ato_t pa = new_proposition(ps->pred, val);
xbt_dynar_push(next_pair->propositions, &pa);
}
- xbt_fifo_unshift(mc_snapshot_stack, next_pair);
+ xbt_fifo_unshift(mc_stack_liveness_stateful, next_pair);
cursor = 0;
if((invisible_col(pair, next_pair) == 0) && (pair->fully_expanded == 0)){
/* Trash the current state, no longer needed */
MC_SET_RAW_MEM;
- xbt_fifo_shift(mc_snapshot_stack);
+ xbt_fifo_shift(mc_stack_liveness_stateful);
//MC_state_delete(state);
MC_UNSET_RAW_MEM;
(from it's predecesor state), depends on any other previous request
executed before it. If it does then add it to the interleave set of the
state that executed that previous request. */
- while ((pair = xbt_fifo_shift(mc_snapshot_stack)) != NULL) {
+ while ((pair = xbt_fifo_shift(mc_stack_liveness_stateful)) != NULL) {
req = MC_state_get_internal_request(pair->graph_state);
- xbt_fifo_foreach(mc_snapshot_stack, item, prev_pair, mc_pair_prop_col_t) {
+ xbt_fifo_foreach(mc_stack_liveness_stateful, item, prev_pair, mc_pair_prop_col_t) {
if(MC_request_depend(req, MC_state_get_internal_request(prev_pair->graph_state))){
if(XBT_LOG_ISENABLED(mc_dpor, xbt_log_priority_debug)){
XBT_DEBUG("Dependent Transitions:");
if (MC_state_interleave_size(pair->graph_state) > 0) {
/* We found a back-tracking point, let's loop */
MC_restore_snapshot(pair->system_state);
- xbt_fifo_unshift(mc_snapshot_stack, pair);
- XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_snapshot_stack));
+ xbt_fifo_unshift(mc_stack_liveness_stateful, pair);
+ XBT_DEBUG("Back-tracking to depth %d", xbt_fifo_size(mc_stack_liveness_stateful));
MC_UNSET_RAW_MEM;
break;
} else {
#include <unistd.h>
#include <sys/types.h>
#include <sys/wait.h>
+#include <sys/time.h>
#include "../surf/surf_private.h"
#include "../simix/private.h"
"Logging specific to MC (global)");
/* MC global data structures */
-mc_snapshot_t initial_snapshot = NULL;
-xbt_fifo_t mc_stack = NULL;
-mc_stats_t mc_stats = NULL;
-mc_stats_pair_t mc_stats_pair = NULL;
+
mc_state_t mc_current_state = NULL;
char mc_replay_mode = FALSE;
double *mc_time = NULL;
-xbt_fifo_t mc_snapshot_stack = NULL;
+mc_snapshot_t initial_snapshot = NULL;
+
+/* Safety */
+
+xbt_fifo_t mc_stack_safety_stateful = NULL;
+xbt_fifo_t mc_stack_safety_stateless = NULL;
+mc_stats_t mc_stats = NULL;
+
+/* Liveness */
+
+xbt_fifo_t mc_stack_liveness_stateful = NULL;
+mc_stats_pair_t mc_stats_pair = NULL;
+xbt_fifo_t mc_stack_liveness_stateless = NULL;
+
/**
* \brief Initialize the model-checker data structures
*/
-void MC_init(void)
+void MC_init_safety_stateless(void)
{
+
/* Check if MC is already initialized */
if (initial_snapshot)
return;
mc_stats->state_size = 1;
/* Create exploration stack */
- mc_stack = xbt_fifo_new();
+ mc_stack_safety_stateless = xbt_fifo_new();
MC_UNSET_RAW_MEM;
MC_UNSET_RAW_MEM;
}
-void MC_init_stateful(void){
+void MC_init_safety_stateful(void){
+
/* Check if MC is already initialized */
if (initial_snapshot)
mc_stats->state_size = 1;
/* Create exploration stack */
- mc_snapshot_stack = xbt_fifo_new();
+ mc_stack_safety_stateful = xbt_fifo_new();
MC_UNSET_RAW_MEM;
}
-void MC_init_with_automaton(xbt_automaton_t a){
+void MC_init_liveness_stateful(xbt_automaton_t a){
XBT_DEBUG("Start init mc");
/* Initialize statistics */
mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
mc_stats = xbt_new0(s_mc_stats_t, 1);
- //mc_stats_pair->pair_size = 1;
XBT_DEBUG("Creating snapshot_stack");
/* Create exploration stack */
- mc_snapshot_stack = xbt_fifo_new();
+ mc_stack_liveness_stateful = xbt_fifo_new();
MC_UNSET_RAW_MEM;
- //MC_vddfs_with_restore_snapshot_init(a);
- //MC_ddfs_with_restore_snapshot_init(a);
- MC_dpor2_init(a);
+ //MC_vddfs_stateful_init(a);
+ MC_ddfs_stateful_init(a);
+ //MC_dpor2_init(a);
//MC_dpor3_init(a);
}
+void MC_init_liveness_stateless(xbt_automaton_t a){
+
+ XBT_DEBUG("Start init mc");
+
+ mc_time = xbt_new0(double, simix_process_maxpid);
+
+ /* Initialize the data structures that must be persistent across every
+ iteration of the model-checker (in RAW memory) */
+
+ MC_SET_RAW_MEM;
+
+ /* Initialize statistics */
+ mc_stats_pair = xbt_new0(s_mc_stats_pair_t, 1);
+
+ XBT_DEBUG("Creating snapshot_stack");
+
+ /* Create exploration stack */
+ mc_stack_liveness_stateless = xbt_fifo_new();
+
+ MC_UNSET_RAW_MEM;
+
+ MC_ddfs_stateless_init(a);
+}
+
void MC_modelcheck(void)
{
- MC_init();
+ MC_init_safety_stateless();
MC_dpor();
MC_exit();
}
void MC_modelcheck_stateful(void)
{
- MC_init_stateful();
+ MC_init_safety_stateful();
MC_dpor_stateful();
MC_exit();
}
-void MC_modelcheck_with_automaton(xbt_automaton_t a){
- MC_init_with_automaton(a);
- MC_exit_with_automaton();
+void MC_modelcheck_liveness_stateful(xbt_automaton_t a){
+ MC_init_liveness_stateful(a);
+ MC_exit_liveness();
+}
+
+void MC_modelcheck_liveness_stateless(xbt_automaton_t a){
+ MC_init_liveness_stateless(a);
+ MC_exit_liveness();
}
-void MC_exit_with_automaton(void)
+void MC_exit_liveness(void)
{
MC_print_statistics_pairs(mc_stats_pair);
xbt_free(mc_time);
MC_memory_exit();
}
+
void MC_exit(void)
{
MC_print_statistics(mc_stats);
* execution trace
* \param stack The stack to dump
*/
-void MC_dump_stack(xbt_fifo_t stack)
+void MC_dump_stack_safety_stateless(xbt_fifo_t stack)
{
mc_state_t state;
- MC_show_stack(stack);
+ MC_show_stack_safety_stateless(stack);
MC_SET_RAW_MEM;
while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
}
-void MC_show_stack(xbt_fifo_t stack)
+void MC_show_stack_safety_stateless(xbt_fifo_t stack)
{
int value;
mc_state_t state;
XBT_INFO("%s", req_str);
xbt_free(req_str);*/
XBT_INFO("Counter-example execution trace:");
- MC_dump_stack(mc_stack);
+ MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
}
void MC_show_deadlock_stateful(smx_req_t req)
XBT_INFO("%s", req_str);
xbt_free(req_str);*/
XBT_INFO("Counter-example execution trace:");
- MC_show_stack_stateful(mc_snapshot_stack);
+ MC_show_stack_safety_stateful(mc_stack_safety_stateful);
}
-void MC_dump_stack_stateful(xbt_fifo_t stack)
+void MC_dump_stack_safety_stateful(xbt_fifo_t stack)
{
//mc_state_ws_t state;
- MC_show_stack_stateful(stack);
+ MC_show_stack_safety_stateful(stack);
/*MC_SET_RAW_MEM;
while ((state = (mc_state_t) xbt_fifo_pop(stack)) != NULL)
}
-void MC_show_stack_stateful(xbt_fifo_t stack)
+void MC_show_stack_safety_stateful(xbt_fifo_t stack)
{
int value;
mc_state_ws_t state;
}
}
+void MC_show_stack_liveness_stateful(xbt_fifo_t stack){
+ int value;
+ mc_pair_t pair;
+ xbt_fifo_item_t item;
+ smx_req_t req;
+ char *req_str = NULL;
+
+ for (item = xbt_fifo_get_last_item(stack);
+ (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
+ : (NULL)); item = xbt_fifo_get_prev_item(item)) {
+ req = MC_state_get_executed_request(pair->graph_state, &value);
+ if(req){
+ req_str = MC_request_to_string(req, value);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
+ }
+ }
+}
+
+void MC_dump_stack_liveness_stateful(xbt_fifo_t stack){
+ mc_pair_t pair;
+
+ MC_SET_RAW_MEM;
+ while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
+ MC_pair_delete(pair);
+ MC_UNSET_RAW_MEM;
+}
+
+void MC_show_stack_liveness_stateless(xbt_fifo_t stack){
+ int value;
+ mc_pair_stateless_t pair;
+ xbt_fifo_item_t item;
+ smx_req_t req;
+ char *req_str = NULL;
+
+ for (item = xbt_fifo_get_last_item(stack);
+ (item ? (pair = (mc_pair_stateless_t) (xbt_fifo_get_item_content(item)))
+ : (NULL)); item = xbt_fifo_get_prev_item(item)) {
+ req = MC_state_get_executed_request(pair->graph_state, &value);
+ if(req){
+ req_str = MC_request_to_string(req, value);
+ XBT_INFO("%s", req_str);
+ xbt_free(req_str);
+ }
+ }
+}
+
+void MC_dump_stack_liveness_stateless(xbt_fifo_t stack){
+ mc_pair_stateless_t pair;
+
+ MC_SET_RAW_MEM;
+ while ((pair = (mc_pair_stateless_t) xbt_fifo_pop(stack)) != NULL)
+ MC_pair_stateless_delete(pair);
+ MC_UNSET_RAW_MEM;
+}
+
+
void MC_print_statistics(mc_stats_t stats)
{
XBT_INFO("State space size ~= %lu", stats->state_size);
XBT_INFO("*** PROPERTY NOT VALID ***");
XBT_INFO("**************************");
XBT_INFO("Counter-example execution trace:");
- MC_dump_stack(mc_stack);
+ MC_dump_stack_safety_stateless(mc_stack_safety_stateless);
MC_print_statistics(mc_stats);
xbt_abort();
}
XBT_INFO("*** PROPERTY NOT VALID ***");
XBT_INFO("**************************");
XBT_INFO("Counter-example execution trace:");
- MC_dump_stack_stateful(mc_snapshot_stack);
+ MC_dump_stack_safety_stateful(mc_stack_safety_stateful);
MC_print_statistics(mc_stats);
xbt_abort();
}
}
-void MC_assert_pair(int prop){
+void MC_assert_pair_stateful(int prop){
+ if (MC_IS_ENABLED && !prop) {
+ XBT_INFO("**************************");
+ XBT_INFO("*** PROPERTY NOT VALID ***");
+ XBT_INFO("**************************");
+ //XBT_INFO("Counter-example execution trace:");
+ MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
+ //MC_dump_snapshot_stack(mc_snapshot_stack);
+ MC_print_statistics_pairs(mc_stats_pair);
+ xbt_abort();
+ }
+}
+
+void MC_assert_pair_stateless(int prop){
if (MC_IS_ENABLED && !prop) {
XBT_INFO("**************************");
XBT_INFO("*** PROPERTY NOT VALID ***");
XBT_INFO("**************************");
//XBT_INFO("Counter-example execution trace:");
- MC_show_snapshot_stack(mc_snapshot_stack);
+ MC_show_stack_liveness_stateless(mc_stack_liveness_stateless);
//MC_dump_snapshot_stack(mc_snapshot_stack);
MC_print_statistics_pairs(mc_stats_pair);
xbt_abort();
}
-void MC_show_snapshot_stack(xbt_fifo_t stack){
- int value;
- mc_pair_t pair;
- xbt_fifo_item_t item;
- smx_req_t req;
- char *req_str = NULL;
-
- for (item = xbt_fifo_get_last_item(stack);
- (item ? (pair = (mc_pair_t) (xbt_fifo_get_item_content(item)))
- : (NULL)); item = xbt_fifo_get_prev_item(item)) {
- req = MC_state_get_executed_request(pair->graph_state, &value);
- if(req){
- req_str = MC_request_to_string(req, value);
- XBT_INFO("%s", req_str);
- xbt_free(req_str);
- }
- }
-}
-
-void MC_dump_snapshot_stack(xbt_fifo_t stack){
- mc_pair_t pair;
-
- MC_SET_RAW_MEM;
- while ((pair = (mc_pair_t) xbt_fifo_pop(stack)) != NULL)
- MC_pair_delete(pair);
- MC_UNSET_RAW_MEM;
-}
-
void MC_pair_delete(mc_pair_t pair){
xbt_free(pair->graph_state->proc_status);
xbt_free(pair->graph_state);
}
-void MC_vddfs_with_restore_snapshot_init(xbt_automaton_t a){
+void MC_vddfs_stateful_init(xbt_automaton_t a){
XBT_DEBUG("**************************************************");
- XBT_DEBUG("Double-DFS with visited state and restore snapshot init");
+ XBT_DEBUG("Double-DFS stateful with visited state init");
XBT_DEBUG("**************************************************");
mc_pair_t mc_initial_pair;
xbt_dynar_foreach(successors, cursor, pair_succ){
MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+ xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
set_pair_visited(pair_succ, 0);
MC_UNSET_RAW_MEM;
if(cursor == 0){
- MC_vddfs_with_restore_snapshot(a, 0, 0);
+ MC_vddfs_stateful(a, 0, 0);
}else{
- MC_vddfs_with_restore_snapshot(a, 0, 1);
+ MC_vddfs_stateful(a, 0, 1);
}
}
}
-void MC_vddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
+void MC_vddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
smx_process_t process = NULL;
- if(xbt_fifo_size(mc_snapshot_stack) == 0)
+ if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
return;
if(restore == 1){
- MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
+ MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
MC_UNSET_RAW_MEM;
}
/* Get current state */
- mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+ mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
if(restore==1){
xbt_swag_foreach(process, simix_global->process_list){
XBT_INFO("| ACCEPTANCE CYCLE |");
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("Counter-example that violates formula :");
- MC_show_snapshot_stack(mc_snapshot_stack);
- MC_dump_snapshot_stack(mc_snapshot_stack);
+ MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
+ MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
MC_print_statistics_pairs(mc_stats_pair);
exit(0);
}
mc_stats_pair->executed_transitions++;
MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+ xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
set_pair_visited(pair_succ, search_cycle);
MC_UNSET_RAW_MEM;
- MC_vddfs_with_restore_snapshot(a, search_cycle, 0);
+ MC_vddfs_stateful(a, search_cycle, 0);
if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
set_pair_reached(current_pair);
XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
- MC_vddfs_with_restore_snapshot(a, 1, 1);
+ MC_vddfs_stateful(a, 1, 1);
}
}else{
MC_SET_RAW_MEM;
- xbt_fifo_shift(mc_snapshot_stack);
+ xbt_fifo_shift(mc_stack_liveness_stateful);
XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
MC_UNSET_RAW_MEM;
-/********************* Double-DFS without visited state *******************/
+/********************* Double-DFS stateful without visited state *******************/
-void MC_ddfs_with_restore_snapshot_init(xbt_automaton_t a){
+void MC_ddfs_stateful_init(xbt_automaton_t a){
XBT_DEBUG("**************************************************");
- XBT_DEBUG("Double-DFS without visited state and with restore snapshot init");
+ XBT_DEBUG("Double-DFS stateful without visited state init");
XBT_DEBUG("**************************************************");
mc_pair_t mc_initial_pair;
xbt_dynar_foreach(successors, cursor, pair_succ){
MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+ xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
MC_UNSET_RAW_MEM;
if(cursor == 0){
- MC_ddfs_with_restore_snapshot(a, 0, 0);
+ MC_ddfs_stateful(a, 0, 0);
}else{
- MC_ddfs_with_restore_snapshot(a, 0, 1);
+ MC_ddfs_stateful(a, 0, 1);
}
}
}
-void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore){
+void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore){
smx_process_t process = NULL;
- if(xbt_fifo_size(mc_snapshot_stack) == 0)
+ if(xbt_fifo_size(mc_stack_liveness_stateful) == 0)
return;
if(restore == 1){
- MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack)))->system_state);
+ MC_restore_snapshot(((mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful)))->system_state);
MC_UNSET_RAW_MEM;
}
/* Get current state */
- mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_snapshot_stack));
+ mc_pair_t current_pair = (mc_pair_t)xbt_fifo_get_item_content(xbt_fifo_get_first_item(mc_stack_liveness_stateful));
if(restore==1){
xbt_swag_foreach(process, simix_global->process_list){
XBT_INFO("| ACCEPTANCE CYCLE |");
XBT_INFO("*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*-*");
XBT_INFO("Counter-example that violates formula :");
- MC_show_snapshot_stack(mc_snapshot_stack);
- MC_dump_snapshot_stack(mc_snapshot_stack);
+ MC_show_stack_liveness_stateful(mc_stack_liveness_stateful);
+ MC_dump_stack_liveness_stateful(mc_stack_liveness_stateful);
MC_print_statistics_pairs(mc_stats_pair);
exit(0);
}
mc_stats_pair->executed_transitions++;
MC_SET_RAW_MEM;
- xbt_fifo_unshift(mc_snapshot_stack, pair_succ);
+ xbt_fifo_unshift(mc_stack_liveness_stateful, pair_succ);
MC_UNSET_RAW_MEM;
- MC_ddfs_with_restore_snapshot(a, search_cycle, 0);
+ MC_ddfs_stateful(a, search_cycle, 0);
if((search_cycle == 0) && (current_pair->automaton_state->type == 1)){
set_pair_reached(current_pair);
XBT_DEBUG("Acceptance pair : graph=%p, automaton=%p(%s)", current_pair->graph_state, current_pair->automaton_state, current_pair->automaton_state->id);
- MC_ddfs_with_restore_snapshot(a, 1, 1);
+ MC_ddfs_stateful(a, 1, 1);
}
}
MC_SET_RAW_MEM;
- xbt_fifo_shift(mc_snapshot_stack);
+ xbt_fifo_shift(mc_stack_liveness_stateful);
XBT_DEBUG("Pair (graph=%p, automaton =%p) shifted in snapshot_stack", current_pair->graph_state, current_pair->automaton_state);
MC_UNSET_RAW_MEM;
}
+
+
+/********************* Double-DFS stateless *******************/
+
+void MC_pair_stateless_delete(mc_pair_stateless_t pair){
+ xbt_free(pair->graph_state->proc_status);
+ xbt_free(pair->graph_state);
+ //xbt_free(pair->automaton_state); -> FIXME : à implémenter
+ xbt_free(pair);
+}
+
+mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st){
+ mc_pair_stateless_t p = NULL;
+ p = xbt_new0(s_mc_pair_stateless_t, 1);
+ p->automaton_state = st;
+ p->graph_state = sg;
+ mc_stats_pair->expanded_pairs++;
+ return p;
+}
+
+
+int reached_stateless(mc_pair_stateless_t pair){
+
+ char* hash_reached = malloc(sizeof(char)*160);
+ unsigned int c= 0;
+
+ MC_SET_RAW_MEM;
+ char *hash = malloc(sizeof(char)*160);
+ xbt_sha((char *)&pair, hash);
+ xbt_dynar_foreach(reached_pairs, c, hash_reached){
+ if(strcmp(hash, hash_reached) == 0){
+ MC_UNSET_RAW_MEM;
+ return 1;
+ }
+ }
+
+ MC_UNSET_RAW_MEM;
+ return 0;
+}
+
+void set_pair_stateless_reached(mc_pair_stateless_t pair){
+
+ if(reached_stateless(pair) == 0){
+ MC_SET_RAW_MEM;
+ char *hash = malloc(sizeof(char)*160) ;
+ xbt_sha((char *)&pair, hash);
+ xbt_dynar_push(reached_pairs, &hash);
+ MC_UNSET_RAW_MEM;
+ }
+
+}
+
+
+void MC_ddfs_stateless_init(xbt_automaton_t a){
+
+ XBT_DEBUG("**************************************************");
+ XBT_DEBUG("Double-DFS without visited state and with restore snapshot init");
+ XBT_DEBUG("**************************************************");
+
+ mc_pair_stateless_t mc_initial_pair;
+ mc_state_t initial_graph_state;
+ smx_process_t process;
+
+ MC_wait_for_requests();
+
+ MC_SET_RAW_MEM;
+
+ initial_graph_state = MC_state_pair_new();
+ xbt_swag_foreach(process, simix_global->process_list){
+ if(MC_process_is_enabled(process)){
+ MC_state_interleave_process(initial_graph_state, process);
+ }
+ }
+
+ reached_pairs = xbt_dynar_new(sizeof(char *), NULL);
+
+ MC_UNSET_RAW_MEM;
+
+ /* regarder dans l'automate toutes les transitions activables grâce à l'état initial du système
+ -> donnera les états initiaux de la propriété consistants avec l'état initial du système */
+
+ unsigned int cursor = 0;
+ unsigned int cursor2 = 0;
+ xbt_state_t state = NULL;
+ int res;
+ xbt_transition_t transition_succ;
+ xbt_dynar_t successors = xbt_dynar_new(sizeof(mc_pair_stateless_t), NULL);
+ mc_pair_stateless_t pair_succ;
+
+ xbt_dynar_foreach(a->states, cursor, state){
+ if(state->type == -1){
+ xbt_dynar_foreach(state->out, cursor2, transition_succ){
+ res = MC_automaton_evaluate_label(a, transition_succ->label);
+
+ if((res == 1) || (res == 2)){
+
+ MC_SET_RAW_MEM;
+
+ mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
+ xbt_dynar_push(successors, &mc_initial_pair);
+
+ MC_UNSET_RAW_MEM;
+
+ }
+ }
+ }
+ }
+
+ cursor = 0;
+
+ if(xbt_dynar_length(successors) == 0){
+ xbt_dynar_foreach(a->states, cursor, state){
+ if(state->type == -1){
+ MC_SET_RAW_MEM;
+
+ mc_initial_pair = new_pair_stateless(initial_graph_state, transition_succ->dst);
+ xbt_dynar_push(successors, &mc_initial_pair);
+
+ MC_UNSET_RAW_MEM;
+ }
+ }
+ }
+
+ cursor = 0;
+ xbt_dynar_foreach(successors, cursor, pair_succ){
+ MC_SET_RAW_MEM;
+
+ xbt_fifo_unshift(mc_stack_liveness_stateless, pair_succ);
+
+ MC_UNSET_RAW_MEM;
+
+ if(cursor == 0){
+ MC_ddfs_stateless(a, 0, 0);
+ }else{
+ MC_ddfs_stateless(a, 0, 1);
+ }
+ }
+}
+
+
+void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int restore){
+
+
+}
+
void MC_wait_for_requests(void);
void MC_get_enabled_processes();
void MC_show_deadlock(smx_req_t req);
-void MC_show_stack(xbt_fifo_t stack);
-void MC_dump_stack(xbt_fifo_t stack);
void MC_show_deadlock_stateful(smx_req_t req);
-void MC_show_stack_stateful(xbt_fifo_t stack);
-void MC_dump_stack_stateful(xbt_fifo_t stack);
+void MC_show_stack_safety_stateless(xbt_fifo_t stack);
+void MC_dump_stack_safety_stateless(xbt_fifo_t stack);
+void MC_show_stack_safety_stateful(xbt_fifo_t stack);
+void MC_dump_stack_safety_stateful(xbt_fifo_t stack);
/********************************* Requests ***********************************/
int MC_request_depend(smx_req_t req1, smx_req_t req2);
multi-request like waitany ) */
} s_mc_state_t, *mc_state_t;
-extern xbt_fifo_t mc_stack;
+extern xbt_fifo_t mc_stack_safety_stateless;
mc_state_t MC_state_new(void);
void MC_state_delete(mc_state_t state);
memory_map_t get_memory_map(void);
-/********************************** DFS for liveness property**************************************/
+/********************************** Double-DFS for liveness property**************************************/
typedef struct s_mc_pair{
mc_snapshot_t system_state;
int num;
}s_mc_pair_t, *mc_pair_t;
-extern xbt_fifo_t mc_snapshot_stack;
+extern xbt_fifo_t mc_stack_liveness_stateful;
int MC_automaton_evaluate_label(xbt_automaton_t a, xbt_exp_label_t l);
mc_pair_t new_pair(mc_snapshot_t sn, mc_state_t sg, xbt_state_t st);
int reached(mc_pair_t p);
void set_pair_reached(mc_pair_t p);
-void MC_show_snapshot_stack(xbt_fifo_t stack);
-void MC_dump_snapshot_stack(xbt_fifo_t stack);
+void MC_show_stack_liveness_stateful(xbt_fifo_t stack);
+void MC_dump_stack_liveness_stateful(xbt_fifo_t stack);
void MC_pair_delete(mc_pair_t pair);
-void MC_exit_with_automaton(void);
+void MC_exit_liveness(void);
mc_state_t MC_state_pair_new(void);
-/* **** Double-DFS without visited state **** */
+/* **** Double-DFS stateful without visited state **** */
-void MC_ddfs_with_restore_snapshot_init(xbt_automaton_t a);
-void MC_ddfs_with_restore_snapshot(xbt_automaton_t a, int search_cycle, int restore);
+void MC_ddfs_stateful_init(xbt_automaton_t a);
+void MC_ddfs_stateful(xbt_automaton_t a, int search_cycle, int restore);
-/* **** Double-DFS with visited state **** */
+/* **** Double-DFS stateful with visited state **** */
typedef struct s_mc_visited_pair{
mc_pair_t pair;
int search_cycle;
}s_mc_visited_pair_t, *mc_visited_pair_t;
-void MC_vddfs_with_restore_snapshot_init(xbt_automaton_t a);
-void MC_vddfs_with_restore_snapshot(xbt_automaton_t automaton, int search_cycle, int restore);
+void MC_vddfs_stateful_init(xbt_automaton_t a);
+void MC_vddfs_stateful(xbt_automaton_t automaton, int search_cycle, int restore);
void set_pair_visited(mc_pair_t p, int search_cycle);
int visited(mc_pair_t p, int search_cycle);
+/* **** Double-DFS stateless **** */
+
+typedef struct s_mc_pair_stateless{
+ mc_state_t graph_state;
+ xbt_state_t automaton_state;
+}s_mc_pair_stateless_t, *mc_pair_stateless_t;
+
+extern xbt_fifo_t mc_stack_liveness_stateless;
+
+mc_pair_stateless_t new_pair_stateless(mc_state_t sg, xbt_state_t st);
+void MC_ddfs_stateless_init(xbt_automaton_t a);
+void MC_ddfs_stateless(xbt_automaton_t a, int search_cycle, int restore);
+int reached_stateless(mc_pair_stateless_t p);
+void set_pair_stateless_reached(mc_pair_stateless_t p);
+void MC_show_stack_liveness_stateless(xbt_fifo_t stack);
+void MC_dump_stack_liveness_stateless(xbt_fifo_t stack);
+void MC_pair_stateless_delete(mc_pair_stateless_t pair);
/* **** DPOR Cristian stateful **** */
mc_state_t graph_state;
}s_mc_state_ws_t, *mc_state_ws_t;
+extern xbt_fifo_t mc_stack_safety_stateful;
+
void MC_init_stateful(void);
void MC_modelcheck_stateful(void);
mc_state_ws_t new_state_ws(mc_snapshot_t s, mc_state_t gs);
return MSG_OK;
}
-MSG_error_t MSG_main_with_automaton(xbt_automaton_t a)
+MSG_error_t MSG_main_liveness_stateful(xbt_automaton_t a)
{
/* Clean IO before the run */
fflush(stdout);
fflush(stderr);
if (MC_IS_ENABLED) {
- MC_modelcheck_with_automaton(a);
+ MC_modelcheck_liveness_stateful(a);
+ }
+ else {
+ SIMIX_run();
+ }
+ return MSG_OK;
+}
+
+MSG_error_t MSG_main_liveness_stateless(xbt_automaton_t a)
+{
+ /* Clean IO before the run */
+ fflush(stdout);
+ fflush(stderr);
+
+ if (MC_IS_ENABLED) {
+ MC_modelcheck_liveness_stateless(a);
}
else {
SIMIX_run();