From 7c0507a900e706ca00c5d6fe7a1fd196433a00f6 Mon Sep 17 00:00:00 2001 From: ccremers Date: Wed, 27 Apr 2005 11:43:47 +0000 Subject: [PATCH] - Fixed bug where claim fails were not counted in the modelchecker, as reported bij GH. Attacks were indicated, though, so this only caused problems for users using --summary and not looking at the "attack: L:?" field. --- src/modelchecker.c | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/modelchecker.c b/src/modelchecker.c index 135917d..f25c2e4 100644 --- a/src/modelchecker.c +++ b/src/modelchecker.c @@ -1233,12 +1233,15 @@ int violateClaim (const System sys, int length, int claimev, Termlist reqt) { int flag; + Claimlist clinfo; /* default = no adaption of pruning, continue search */ flag = 1; /* Count the violations */ sys->failed = statesIncrease (sys->failed); + clinfo = sys->traceEvent[claimev]->claiminfo; + clinfo->failed = statesIncrease (clinfo->failed); // note: for modelchecking secrecy, this can lead to more fails (at further events in branches of the tree) than claim encounters /* mark the path in the state graph? */ if (sys->output == STATESPACE)