Logo AND Algorithmique Numérique Distribuée

Public GIT Repository
model-checker : new examples (with tesh) for verification of liveness properties...
[simgrid.git] / examples / msg / mc / electric_fence.c
1 /* Copyright (c) 2013. The SimGrid Team.
2  * All rights reserved.                                                     */
3
4 /* This program is free software; you can redistribute it and/or modify it
5  * under the terms of the license (GNU LGPL) which comes with this package. */
6
7
8 /******************** Non-deterministic message ordering  *********************/
9 /* This example implements one process which receives messages from two other */
10 /* processes. There is no bug on it, it is just provided to test the soundness*/ 
11 /* of the state space reduction with DPOR, if the maximum depth (defined with */
12 /* --cfg=model-check/max_depth:) is reached.                                  */
13 /******************************************************************************/
14
15 #include <msg/msg.h>
16 #include <simgrid/modelchecker.h>
17
18 #define N 2
19
20 XBT_LOG_NEW_DEFAULT_CATEGORY(electric_fence, "Example to check the soundness of DPOR");
21
22 int server(int argc, char *argv[]);
23 int client(int argc, char *argv[]);
24
25 int server(int argc, char *argv[])
26 {
27   msg_task_t task1 = NULL, task2 = NULL;
28   msg_comm_t comm_received1 = NULL, comm_received2 = NULL;
29
30   comm_received1 = MSG_task_irecv(&task1, "mymailbox");
31   comm_received2 = MSG_task_irecv(&task2, "mymailbox");
32
33   MSG_comm_wait(comm_received1, -1);
34   MSG_comm_wait(comm_received2, -1);
35
36   XBT_INFO("OK");
37   return 0;
38 }
39
40 int client(int argc, char *argv[])
41 {
42
43   msg_task_t task = MSG_task_create(argv[1], 0, 10000, NULL);
44
45   MSG_task_send(task, "mymailbox");
46   
47   XBT_INFO("Sent!");
48   return 0;
49 }
50
51 int main(int argc, char *argv[])
52 {
53
54   MSG_init(&argc, argv);
55
56   MSG_create_environment("platform.xml");
57
58   MSG_function_register("server", server);
59
60   MSG_function_register("client", client);
61
62   MSG_launch_application("deploy_electric_fence.xml");
63
64   MSG_main();
65
66   return 0;
67
68 }