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

- Fail increases of claims moved to violateClaim; thus, other references

Browse Source 
were in fact redundant.
This commit is contained in:
ccremers 2005-04-27 13:48:00 +00:00
parent 7c0507a900
commit 38f6f42351
2 changed files with 0 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/claim.c
View File

@ -389,8 +389,6 @@ check_claim_nisynch (const System sys, const int i)
result = oki_nisynch (sys, i, f, g); result = oki_nisynch (sys, i, f, g);
if (!result) if (!result)
{ {
cl->failed = statesIncrease (cl->failed);
#ifdef DEBUG #ifdef DEBUG
globalError++; globalError++;
warning ("Claim has failed!"); warning ("Claim has failed!");
@ -451,8 +449,6 @@ check_claim_niagree (const System sys, const int i)
result = oki_nisynch (sys, i, f, g); result = oki_nisynch (sys, i, f, g);
if (!result) if (!result)
{ {
cl->failed = statesIncrease (cl->failed);
#ifdef DEBUG #ifdef DEBUG
warning ("Claim has failed!"); warning ("Claim has failed!");
printf ("To be exact, claim label "); printf ("To be exact, claim label ");

1
src/modelchecker.c
View File

@ -1387,7 +1387,6 @@ executeTry (const System sys, int run)
/* violation */ /* violation */
Termlist tl; Termlist tl;
runPoint->claiminfo->failed++;
tl = claimViolationDetails (sys, run, runPoint, sys->know); tl = claimViolationDetails (sys, run, runPoint, sys->know);
if (violateClaim (sys, sys->step + 1, sys->step, tl)) if (violateClaim (sys, sys->step + 1, sys->step, tl))
flag = explorify (sys, run); flag = explorify (sys, run);