From f8aacee6ad9be3de387f7c7f9cbdcca83bc01c85 Mon Sep 17 00:00:00 2001 From: ccremers Date: Sun, 25 Jul 2004 15:30:58 +0000 Subject: [PATCH] - Improved some minor stuff regarding synchronisation checking and debugging info. - '--pp=100' switch in debug mode now allows for disabling of synchronising_labels set. --- src/compiler.c | 18 +++++++++++++++--- src/modelchecker.c | 2 +- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/src/compiler.c b/src/compiler.c index 5ece32f..5098df7 100644 --- a/src/compiler.c +++ b/src/compiler.c @@ -1057,6 +1057,15 @@ compute_prec_sets (const System sys) tl_scan = tl_scan->next; } } +#ifdef DEBUG + // Porparam = 100 (weirdness) [x][cc][debug] can turn of the synchronising label sets (override). + if (sys->porparam == 100) + { + termlistDelete (sys->synchronising_labels); + sys->synchronising_labels = NULL; + warning ("Emptied synchronising labels set manually because --pp=100."); + } +#endif // Check for empty stuff //@todo This is for debugging, mainly. if (cl->prec == NULL) @@ -1082,9 +1091,12 @@ compute_prec_sets (const System sys) memFree (prec, size * size * sizeof(int)); #ifdef DEBUG - printf ("Synchronising labels set: "); - termlistPrint (sys->synchronising_labels); - printf ("\n"); + if (DEBUGL(2)) + { + printf ("Synchronising labels set: "); + termlistPrint (sys->synchronising_labels); + printf ("\n"); + } #endif } diff --git a/src/modelchecker.c b/src/modelchecker.c index 0d8984c..a42f024 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -648,7 +648,7 @@ tryChoiceSend (const System sys, const int run, const Roledef rd) /* 1. Simply try */ flag = executeTry (sys, run); /* 2. Postpone if synchonisable */ - if (inTermlist (sys->synchronising_labels, rd->label)) + if (flag && inTermlist (sys->synchronising_labels, rd->label)) { /* This is supposed to be blocked, so we do so */ /* It will possibly be unblocked by a corresponding read event,