add_executable(example2_liveness_without_cycle automaton.c
automatonparse_promela.c
example2_liveness_without_cycle.c)
+add_executable(example_liveness_with_cycle automaton.c
+automatonparse_promela.c example_liveness_with_cycle.c)
+
+
target_link_libraries(centralized simgrid m )
target_link_libraries(bugged3 simgrid m )
target_link_libraries(random_test simgrid m )
target_link_libraries(example_liveness_without_cycle simgrid m )
-target_link_libraries(example2_liveness_without_cycle simgrid m )
\ No newline at end of file
+target_link_libraries(example2_liveness_without_cycle simgrid m )
+target_link_libraries(example_liveness_with_cycle simgrid m )
val1 = (long) MSG_task_get_data(task1);
XBT_INFO("Received %lu", val1);
- //MC_assert(val1 == 2);
+ MC_assert(val1 == 2);
XBT_INFO("OK");
return 0;
extern xbt_automaton_t automaton;
-int p=1;
+int p=0;
int q=0;
val1 = (long) MSG_task_get_data(task1);
XBT_INFO("Received %lu", val1);
- //MC_assert_pair_stateless(val1 == 2);
+ MC_assert_pair_stateless(val1 == 2);
/*if(val1 == 2)
q = 1;
#include "y.tab.c"
#define AMOUNT_OF_CLIENTS 2
-#define CS_PER_PROCESS 1
+#define CS_PER_PROCESS 2
XBT_LOG_NEW_DEFAULT_CATEGORY(example_liveness_with_cycle, "my log messages");
return q;
}
+
+//xbt_dynar_t listeVars -> { void *ptr; int size (nb octets); } => liste de structures
+//=> parcourir la liste et comparer les contenus de chaque pointeur
+
int coordinator(int argc, char *argv[])
{
xbt_dynar_t requests = xbt_dynar_new(sizeof(char *), NULL); // dynamic vector storing requests (which are char*)
m_task_t answer = MSG_task_create("grant", 0, 1000, NULL);
MSG_task_send(answer, req);
CS_used = 1;
- }else{
+ }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;
+ char *req ;
+ xbt_dynar_pop(requests, &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--;
}
// 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){
+ if(strcmp(my_mailbox, "2") == 0){
p = 1;
q = 0;
}
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);
extern xbt_automaton_t automaton;
-
-int p=1;
int r=1;
-int q=1;
int e=1;
int d=1;
-
-int predP(){
- return p;
-}
-
int predR(){
return r;
}
-int predQ(){
- return q;
-}
-
-
int predD(){
return d;
}
-
int predE(){
return e;
}
//XBT_INFO("r (server) = %d", r);
}
- MC_assert_pair_stateless(atoi(MSG_task_get_name(task)) == 3);
+ //MC_assert_pair_stateless(atoi(MSG_task_get_name(task)) == 3);
XBT_INFO("OK");
return 0;
XBT_INFO("Sent!");
- //r=(r+1)%3;
+ r=(r+1)%2;
//XBT_INFO("r (client) = %d", r);
return 0;
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);
- ps = xbt_new_propositional_symbol(automaton,"r", &predR);
+ xbt_propositional_symbol_t ps = xbt_new_propositional_symbol(automaton,"r", &predR);
ps = xbt_new_propositional_symbol(automaton,"e", &predE);
ps = xbt_new_propositional_symbol(automaton,"d", &predD);
-#ifndef _EXAMPLE_AUTOMATON_H
-#define _EXAMPLE_AUTOMATON_H
+#ifndef _EXAMPLE_LIVENESS_WITHOUT_CYCLE_H
+#define _EXAMPLE_LIVENESS_WITHOUT_CYCLE_H
int yyparse(void);
int yywrap(void);
cursor = 0;
mc_pair_reached_t pair_test;
+ int (*compare_dynar)(const void*; const void*) = propositional_symbols_compare;
xbt_dynar_foreach(reached_pairs, cursor, pair_test){
if(automaton_state_compare(pair_test->automaton_state, pair->automaton_state) == 0){
- if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, propositional_symbols_compare_value) == 0){
+ if(xbt_dynar_compare(pair_test->prop_ato, pair->prop_ato, compare_dynar) == 0){
if(snapshot_compare(pair_test->system_state, pair->system_state) == 0){
MC_UNSET_RAW_MEM;
return 1;
int propositional_symbols_compare_value(const void *s1, const void *s2){
- return (!((int)s1 == (int)s2));
+ return (!(s1 == s2));
}
size_t block_free1, start1, block_free2 , start2, block_busy1, block_busy2 ;
- unsigned int i;
+ size_t i;
void *addr_block1, *addr_block2;
struct mdesc* mdp;
block_busy1 = start1 + mdp1->heapinfo[start1].free.size;
block_busy2 = start2 + mdp2->heapinfo[start2].free.size;
- XBT_DEBUG("Block busy : %d - %d", block_busy1, block_busy2);
+ XBT_DEBUG("Block busy : %Zu - %Zu", block_busy1, block_busy2);
if(mdp1->heapinfo[start1].free.size != mdp2->heapinfo[start2].free.size){ // <=> check block_busy
i=block_busy1 ;
- XBT_DEBUG("Next free : %d", mdp1->heapinfo[start1].free.next);
+ XBT_DEBUG("Next free : %Zu", mdp1->heapinfo[start1].free.next);
while(i<mdp1->heapinfo[start1].free.next){
- XBT_DEBUG("i (block busy) : %d", i);
+ XBT_DEBUG("i (block busy) : %Zu", i);
if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
XBT_DEBUG("Different type of busy block");
XBT_DEBUG("Different size of a large cluster");
return 1;
}else{
- XBT_DEBUG("Blocks %d : %p - %p / Data size : %d (%d blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size );
+ XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu (%Zu blocks)", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE),mdp->heapinfo[i].busy.info.size );
if(memcmp(addr_block1, addr_block2, mdp1->heapinfo[i].busy.info.size * BLOCKSIZE) != 0){
- XBT_DEBUG("Different data in block %d", i);
+ XBT_DEBUG("Different data in block %Zu", i);
return 1;
}
}
return 1;
}else{
if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){
- XBT_DEBUG("Different data in block %d", i);
+ XBT_DEBUG("Different data in block %Zu", i);
return 1;
}
}
return 1;
}else{
- XBT_DEBUG("Index of next busy block : %d - %d", block_busy1, block_busy2);
- XBT_DEBUG("Index of next free cluster : %d", mdp1->heapinfo[block_free1].free.next);
+ XBT_DEBUG("Index of next busy block : %Zu - %Zu", block_busy1, block_busy2);
+ XBT_DEBUG("Index of next free cluster : %Zu", mdp1->heapinfo[block_free1].free.next);
i = block_busy1;
while(i<mdp1->heapinfo[block_free1].free.next){
- XBT_DEBUG("i (block busy) : %d", i);
+ XBT_DEBUG("i (block busy) : %Zu", i);
if(mdp1->heapinfo[i].busy.type != mdp2->heapinfo[i].busy.type){
XBT_DEBUG("Different type of busy block");
XBT_DEBUG("Different size of a large cluster");
return 1;
}else{
- XBT_DEBUG("Blocks %d : %p - %p / Data size : %d", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE));
+ XBT_DEBUG("Blocks %Zu : %p - %p / Data size : %Zu", i, addr_block1, addr_block2, (mdp->heapinfo[i].busy.info.size * BLOCKSIZE));
//XBT_DEBUG("Size of large cluster %d", mdp->heapinfo[i].busy.info.size);
if(memcmp(addr_block1, addr_block2, (mdp1->heapinfo[i].busy.info.size * BLOCKSIZE)) != 0){
- XBT_DEBUG("Different data in block %d", i);
+ XBT_DEBUG("Different data in block %Zu", i);
return 1;
}
}
return 1;
}else{
if(memcmp(addr_block1, addr_block2, BLOCKSIZE) != 0){
- XBT_DEBUG("Different data in fragmented block %d", i);
+ XBT_DEBUG("Different data in fragmented block %Zu", i);
return 1;
}
}