A
lgorithmique
N
umérique
D
istribuée
Public GIT Repository
projects
/
simgrid.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
steal a bunch of easy commits and please sonar
[simgrid.git]
/
examples
/
msg
/
mc
/
bugged1_liveness.c
diff --git
a/examples/msg/mc/bugged1_liveness.c
b/examples/msg/mc/bugged1_liveness.c
index
50ad0ae
..
fda0554
100644
(file)
--- a/
examples/msg/mc/bugged1_liveness.c
+++ b/
examples/msg/mc/bugged1_liveness.c
@@
-1,4
+1,4
@@
-/* Copyright (c) 2012-201
4
. The SimGrid Team.
+/* Copyright (c) 2012-201
5
. The SimGrid Team.
* All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
* All rights reserved. */
/* This program is free software; you can redistribute it and/or modify it
@@
-18,7
+18,6
@@
#include "simgrid/msg.h"
#include "mc/mc.h"
#include "simgrid/msg.h"
#include "mc/mc.h"
-#include "xbt/automaton.h"
#include "bugged1_liveness.h"
XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
#include "bugged1_liveness.h"
XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
@@
-26,14
+25,6
@@
XBT_LOG_NEW_DEFAULT_CATEGORY(bugged1_liveness, "my log messages");
int r=0;
int cs=0;
int r=0;
int cs=0;
-int predR(){
- return r;
-}
-
-int predCS(){
- return cs;
-}
-
#ifdef GARBAGE_STACK
/** Do not use a clean stack */
static void garbage_stack(void) {
#ifdef GARBAGE_STACK
/** Do not use a clean stack */
static void garbage_stack(void) {
@@
-45,9
+36,8
@@
static void garbage_stack(void) {
}
#endif
}
#endif
-int coordinator(int argc, char *argv[])
+
static
int coordinator(int argc, char *argv[])
{
{
-
int CS_used = 0;
msg_task_t task = NULL, answer = NULL;
xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
int CS_used = 0;
msg_task_t task = NULL, answer = NULL;
xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL);
@@
-70,7
+60,7
@@
int coordinator(int argc, char *argv[])
answer = NULL;
}
}
answer = NULL;
}
}
- } else {
+ } else {
if (!xbt_dynar_is_empty(requests)) {
XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
xbt_dynar_shift(requests, &req);
if (!xbt_dynar_is_empty(requests)) {
XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", xbt_dynar_length(requests));
xbt_dynar_shift(requests, &req);
@@
-90,11
+80,10
@@
int coordinator(int argc, char *argv[])
kind = NULL;
req = NULL;
}
kind = NULL;
req = NULL;
}
-
return 0;
}
return 0;
}
-int client(int argc, char *argv[])
+
static
int client(int argc, char *argv[])
{
int my_pid = MSG_process_get_PID(MSG_process_self());
{
int my_pid = MSG_process_get_PID(MSG_process_self());
@@
-134,7
+123,7
@@
int client(int argc, char *argv[])
release = NULL;
MSG_process_sleep(my_pid);
release = NULL;
MSG_process_sleep(my_pid);
-
+
if(strcmp(my_mailbox, "1") == 0){
cs=0;
r=0;
if(strcmp(my_mailbox, "1") == 0){
cs=0;
r=0;
@@
-142,7
+131,6
@@
int client(int argc, char *argv[])
}
}
}
}
-
return 0;
}
return 0;
}
@@
-150,7
+138,7
@@
static int raw_client(int argc, char *argv[])
{
#ifdef GARBAGE_STACK
// At this point the stack of the callee (client) is probably filled with
{
#ifdef GARBAGE_STACK
// At this point the stack of the callee (client) is probably filled with
- // zeros and unitialized variables will contain 0. This call will place
+ // zeros and uni
ni
tialized variables will contain 0. This call will place
// random byes in the stack of the callee:
garbage_stack();
#endif
// random byes in the stack of the callee:
garbage_stack();
#endif
@@
-159,22
+147,17
@@
static int raw_client(int argc, char *argv[])
int main(int argc, char *argv[])
{
int main(int argc, char *argv[])
{
-
MSG_init(&argc, argv);
MSG_init(&argc, argv);
- char **options = &argv[1];
+ MC_automaton_new_propositional_symbol_pointer("r", &r);
+ MC_automaton_new_propositional_symbol_pointer("cs", &cs);
- MSG_config("model-check/property","promela_bugged1_liveness");
- MC_automaton_new_propositional_symbol("r", &predR);
- MC_automaton_new_propositional_symbol("cs", &predCS);
+ MSG_create_environment(argv[1]);
- const char* platform_file = options[0];
- const char* application_file = options[1];
-
- MSG_create_environment(platform_file);
MSG_function_register("coordinator", coordinator);
MSG_function_register("client", raw_client);
MSG_function_register("coordinator", coordinator);
MSG_function_register("client", raw_client);
- MSG_launch_application(application_file);
+ MSG_launch_application(argv[2]);
+
MSG_main();
return 0;
MSG_main();
return 0;