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,