andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Improved some minor stuff regarding synchronisation checking and

Browse Source 
debugging info.
- '--pp=100' switch in debug mode now allows for disabling of
  synchronising_labels set.
This commit is contained in:
ccremers 2004-07-25 15:30:58 +00:00
parent db52ec77e6
commit f8aacee6ad
2 changed files with 16 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
src/compiler.c
View File

@ -1057,6 +1057,15 @@ compute_prec_sets (const System sys)
tl_scan = tl_scan->next; 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 // Check for empty stuff
//@todo This is for debugging, mainly. //@todo This is for debugging, mainly.
if (cl->prec == NULL) if (cl->prec == NULL)
@ -1082,9 +1091,12 @@ compute_prec_sets (const System sys)
memFree (prec, size * size * sizeof(int)); memFree (prec, size * size * sizeof(int));
#ifdef DEBUG #ifdef DEBUG
if (DEBUGL(2))
{
printf ("Synchronising labels set: "); printf ("Synchronising labels set: ");
termlistPrint (sys->synchronising_labels); termlistPrint (sys->synchronising_labels);
printf ("\n"); printf ("\n");
}
#endif #endif
} }

2
src/modelchecker.c
View File

@ -648,7 +648,7 @@ tryChoiceSend (const System sys, const int run, const Roledef rd)
/* 1. Simply try */ /* 1. Simply try */
flag = executeTry (sys, run); flag = executeTry (sys, run);
/* 2. Postpone if synchonisable */ /* 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 */ /* This is supposed to be blocked, so we do so */
/* It will possibly be unblocked by a corresponding read event, /* It will possibly be unblocked by a corresponding read event,