From: Marion Guthmuller Date: Thu, 22 Sep 2011 16:12:01 +0000 (+0200) Subject: model-checker : add files for examples X-Git-Tag: exp_20120216~133^2~64 X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/e9b00bd03825b6b1c66e642886328ce6384d9dad model-checker : add files for examples --- diff --git a/examples/msg/mc/automaton2_PROMELA b/examples/msg/mc/automaton2_PROMELA new file mode 100644 index 0000000000..ba1afdadf2 --- /dev/null +++ b/examples/msg/mc/automaton2_PROMELA @@ -0,0 +1,11 @@ +never { /* !G(p->Fq) */ +T0_init : /* init */ + if + :: (1) -> goto T0_init + :: (!q && p) -> goto accept_S2 + fi; +accept_S2 : /* 1 */ + if + :: (!q) -> goto accept_S2 + fi; +} \ No newline at end of file diff --git a/examples/msg/mc/automaton_PROMELA b/examples/msg/mc/automaton_PROMELA new file mode 100644 index 0000000000..2d0a31203d --- /dev/null +++ b/examples/msg/mc/automaton_PROMELA @@ -0,0 +1,28 @@ +never { +T0_init: + if + :: (!d) || (r) -> goto accept_S1 + :: (1) -> goto T1_S4 + :: (1) -> goto T0_S2 + :: (!e) -> goto accept_S3 + fi; +T1_S4: + if + :: (1) -> goto T1_S4 + :: (r) -> goto accept_S1 + fi; +accept_S1: + if + :: (!d) || (r) -> goto accept_S1 + :: (1) -> goto T1_S4 + fi; +T0_S2: + if + :: (1) -> goto T0_S2 + :: (!e) -> goto accept_S3 + fi; +accept_S3: + if + :: (!e) -> goto accept_S3 + fi; +} diff --git a/examples/msg/mc/deploy_mutex2.xml b/examples/msg/mc/deploy_mutex2.xml new file mode 100644 index 0000000000..7ebdbaf581 --- /dev/null +++ b/examples/msg/mc/deploy_mutex2.xml @@ -0,0 +1,43 @@ + + + + + + + + + + + + + + + + + + + diff --git a/examples/msg/mc/example_liveness_with_cycle.c b/examples/msg/mc/example_liveness_with_cycle.c new file mode 100644 index 0000000000..42ef27daa1 --- /dev/null +++ b/examples/msg/mc/example_liveness_with_cycle.c @@ -0,0 +1,148 @@ +/***************** Centralized Mutual Exclusion Algorithm *********************/ +/* This example implements a centralized mutual exclusion algorithm. */ +/* There is no bug on it, it is just provided to test the state space */ +/* reduction of DPOR. */ +/******************************************************************************/ + +#include "msg/msg.h" +#include "mc/mc.h" +#include "xbt/automaton.h" +#include "xbt/automatonparse_promela.h" +#include "example_liveness_with_cycle.h" +#include "y.tab.c" + +#define AMOUNT_OF_CLIENTS 2 +#define CS_PER_PROCESS 1 + +XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages"); + +int p=0; +int q=0; + +int predP(){ + return p; +} + +int predQ(){ + return q; +} + +int coordinator(int argc, char *argv[]) +{ + xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL); // dynamic vector storing requests (which are char*) + int CS_used = 0; // initially the CS is idle + int todo = AMOUNT_OF_CLIENTS * CS_PER_PROCESS; // amount of releases we are expecting + while (todo > 0) { + m_task_t task = NULL; + MSG_task_receive(&task, "coordinator"); + const char *kind = MSG_task_get_name(task); //is it a request or a release? + if (!strcmp(kind, "request")) { // that's a request + char *req = MSG_task_get_data(task); + //XBT_INFO("Req %s", req); + if (CS_used) { // need to push the request in the vector + XBT_INFO("CS already used. Queue the request"); + xbt_dynar_push(requests, &req); + } else { // can serve it immediatly + XBT_INFO("CS idle. Grant immediatly"); + if(strcmp(req, "1") == 0){ + m_task_t answer = MSG_task_create("grant", 0, 1000, NULL); + MSG_task_send(answer, req); + CS_used = 1; + }else{ + m_task_t answer = MSG_task_create("notgrant", 0, 1000, NULL); + MSG_task_send(answer, req); + } + + } + } else { // that's a release. Check if someone was waiting for the lock + if (xbt_dynar_length(requests) > 0) { + XBT_INFO("CS release. Grant to queued requests (queue size: %lu)", + xbt_dynar_length(requests)); + char *req; + if(strcmp(req, "1") == 0){ + xbt_dynar_pop(requests, &req); + MSG_task_send(MSG_task_create("grant", 0, 1000, NULL), req); + todo--; + }else{ + xbt_dynar_pop(requests, &req); + MSG_task_send(MSG_task_create("notgrant", 0, 1000, NULL), req); + todo--; + } + } else { // nobody wants it + XBT_INFO("CS release. resource now idle"); + CS_used = 0; + todo--; + } + } + MSG_task_destroy(task); + } + XBT_INFO("Received all releases, quit now"); + return 0; +} + +int client(int argc, char *argv[]) +{ + int my_pid = MSG_process_get_PID(MSG_process_self()); + // use my pid as name of mailbox to contact me + char *my_mailbox = bprintf("%s", argv[1]); + // request the CS 2 times, sleeping a bit in between + int i; + for (i = 0; i < CS_PER_PROCESS; i++) { + p = 1; + q = 0; + XBT_INFO("Ask the request"); + MSG_task_send(MSG_task_create("request", 0, 1000, my_mailbox), + "coordinator"); + if(strcmp(my_mailbox, "1") == 0){ + p = 1; + q = 0; + } + // wait the answer + m_task_t grant = NULL; + MSG_task_receive(&grant, my_mailbox); + const char *kind = MSG_task_get_name(grant); + if(!strcmp(kind, "grant")){ + if(strcmp(my_mailbox, "2") == 0){ + q = 1; + p = 0; + } + //answers ++; + MSG_task_destroy(grant); + XBT_INFO("got the answer. Sleep a bit and release it"); + MSG_process_sleep(1); + MSG_task_send(MSG_task_create("release", 0, 1000,NULL ), + "coordinator"); + }else{ + MSG_task_destroy(grant); + XBT_INFO("Negative answer"); + MSG_process_sleep(1); + MSG_task_send(MSG_task_create("notrelease", 0, 1000,NULL ), + "coordinator"); + } + + MSG_process_sleep(my_pid); + + } + + //XBT_INFO("Got all the CS I wanted (%s), quit now", my_mailbox); + return 0; +} + +int main(int argc, char *argv[]) +{ + init(); + yyparse(); + automaton = get_automaton(); + xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"p", &predP); + ps = xbt_new_propositional_symbol(automaton,"q", &predQ); + + MSG_global_init(&argc, argv); + MSG_create_environment("../msg_platform.xml"); + MSG_function_register("coordinator", coordinator); + MSG_function_register("client", client); + MSG_launch_application("deploy_mutex2.xml"); + MSG_main_liveness_stateless(automaton); + //MSG_main(); + + return 0; +} diff --git a/examples/msg/mc/example_liveness_with_cycle.h b/examples/msg/mc/example_liveness_with_cycle.h new file mode 100644 index 0000000000..c614af2317 --- /dev/null +++ b/examples/msg/mc/example_liveness_with_cycle.h @@ -0,0 +1,14 @@ +#ifndef _EXAMPLE_LIVENESS_WITH_CYCLE_H +#define _EXAMPLE_LIVENESS_WITH_CYCLE_H + +int yyparse(void); +int yywrap(void); +int yylex(void); + +int predP(void); +int predQ(void); + +int coordinator(int argc, char *argv[]); +int client(int argc, char *argv[]); + +#endif