From 38f6f42351206cb315c91a8c6e48e54809501d35 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 27 Apr 2005 13:48:00 +0000 Subject: [PATCH] - Fail increases of claims moved to violateClaim; thus, other references were in fact redundant. --- src/claim.c | 4 ---- src/modelchecker.c | 1 - 2 files changed, 5 deletions(-) diff --git a/src/claim.c b/src/claim.c index 4e815b1..ba59acb 100644 --- a/src/claim.c +++ b/src/claim.c @@ -389,8 +389,6 @@ check_claim_nisynch (const System sys, const int i) result = oki_nisynch (sys, i, f, g); if (!result) { - cl->failed = statesIncrease (cl->failed); - #ifdef DEBUG globalError++; warning ("Claim has failed!"); @@ -451,8 +449,6 @@ check_claim_niagree (const System sys, const int i) result = oki_nisynch (sys, i, f, g); if (!result) { - cl->failed = statesIncrease (cl->failed); - #ifdef DEBUG warning ("Claim has failed!"); printf ("To be exact, claim label "); diff --git a/src/modelchecker.c b/src/modelchecker.c index f25c2e4..a467393 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -1387,7 +1387,6 @@ executeTry (const System sys, int run) /* violation */ Termlist tl; - runPoint->claiminfo->failed++; tl = claimViolationDetails (sys, run, runPoint, sys->know); if (violateClaim (sys, sys->step + 1, sys->step, tl)) flag = explorify (sys, run);