X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/blobdiff_plain/40334ce6fe520b2fa7d1e240716e4f34a5fdc74e..ea66702ca647cf2e57f4680aa88f8e0eda6011bc:/examples/msg/mc/bugged1_liveness.c diff --git a/examples/msg/mc/bugged1_liveness.c b/examples/msg/mc/bugged1_liveness.c index b463bf9981..47107f0fca 100644 --- a/examples/msg/mc/bugged1_liveness.c +++ b/examples/msg/mc/bugged1_liveness.c @@ -1,14 +1,13 @@ -/* Copyright (c) 2012-2014. The SimGrid Team. - * All rights reserved. */ +/* Copyright (c) 2012-2017. The SimGrid Team. All rights reserved. */ /* This program is free software; you can redistribute it and/or modify it * under the terms of the license (GNU LGPL) which comes with this package. */ -/***************** Centralized Mutual Exclusion Algorithm *********************/ -/* This example implements a centralized mutual exclusion algorithm. */ -/* Bug : CS requests of client 1 not satisfied */ -/* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok) */ -/******************************************************************************/ +/***************** Centralized Mutual Exclusion Algorithm *******************/ +/* This example implements a centralized mutual exclusion algorithm. */ +/* Bug : CS requests of client 1 not satisfied */ +/* LTL property checked : G(r->F(cs)); (r=request of CS, cs=CS ok) */ +/****************************************************************************/ #ifdef GARBAGE_STACK #include @@ -18,7 +17,6 @@ #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"); @@ -37,10 +35,11 @@ static void garbage_stack(void) { } #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; + int CS_used = 0; + msg_task_t task = NULL; + msg_task_t answer = NULL; xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL); char *req; @@ -61,7 +60,7 @@ int coordinator(int argc, char *argv[]) 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); @@ -81,16 +80,16 @@ int coordinator(int argc, char *argv[]) kind = NULL; req = NULL; } - 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()); char *my_mailbox = xbt_strdup(argv[1]); - msg_task_t grant = NULL, release = NULL; + msg_task_t grant = NULL; + msg_task_t release = NULL; while(1){ XBT_INFO("Ask the request"); @@ -125,7 +124,7 @@ int client(int argc, char *argv[]) release = NULL; MSG_process_sleep(my_pid); - + if(strcmp(my_mailbox, "1") == 0){ cs=0; r=0; @@ -133,7 +132,6 @@ int client(int argc, char *argv[]) } } - return 0; } @@ -141,7 +139,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 - // zeros and unitialized variables will contain 0. This call will place + // zeros and uninitialized variables will contain 0. This call will place // random byes in the stack of the callee: garbage_stack(); #endif @@ -151,19 +149,15 @@ static int raw_client(int argc, char *argv[]) int main(int argc, char *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); - const char* platform_file = options[0]; - const char* application_file = options[1]; - - MSG_create_environment(platform_file); + MSG_create_environment(argv[1]); MSG_function_register("coordinator", coordinator); MSG_function_register("client", raw_client); - MSG_launch_application(application_file); + MSG_launch_application(argv[2]); MSG_main();