1 /**************** Shared buffer between asynchronous receives *****************/
2 /* Server process assumes that the data from the second communication comm2 */
3 /* will overwrite the one from the first communication, because of the order */
4 /* of the wait calls. This is not true because data copy can be triggered by */
5 /* a call to wait on the other end of the communication (client). */
6 /* NOTE that the communications use different mailboxes, but they share the */
7 /* same buffer for reception (task1). */
8 /******************************************************************************/
10 #include "xbt/automaton.h"
11 #include "xbt/automatonparse_promela.h"
12 #include "example2_liveness_without_cycle.h"
18 XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "Example liveness with cycle");
20 extern xbt_automaton_t automaton;
37 int server(int argc, char *argv[]);
38 int client(int argc, char *argv[]);
40 int server(int argc, char *argv[])
44 msg_comm_t comm1, comm2;
46 comm1 = MSG_task_irecv(&task1, "mymailbox1");
47 comm2 = MSG_task_irecv(&task1, "mymailbox2");
48 MSG_comm_wait(comm1, -1);
49 MSG_comm_wait(comm2, -1);
51 val1 = (long) MSG_task_get_data(task1);
52 XBT_INFO("Received %lu", val1);
54 MC_assert_pair_stateless(val1 == 2);
61 //XBT_INFO("q (server) = %d", q);
68 int client(int argc, char *argv[])
73 MSG_task_create("task", 0, 10000, (void *) atol(argv[1]));
75 mbox = bprintf("mymailbox%s", argv[1]);
77 XBT_INFO("Send %d!", atoi(argv[1]));
78 comm = MSG_task_isend(task1, mbox);
80 MSG_comm_wait(comm, -1);
87 int main(int argc, char *argv[])
92 automaton = get_automaton();
93 xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP);
94 ps = xbt_new_propositional_symbol(automaton,"q", &predQ);
96 //display_automaton();
98 MSG_global_init(&argc, argv);
100 MSG_create_environment("platform.xml");
102 MSG_function_register("server", server);
104 MSG_function_register("client", client);
106 MSG_launch_application("deploy_bugged3.xml");
108 MSG_main_liveness_stateless(automaton);