Hi,
On Fri, 2 Apr 2021 19:05:04 +0300 Aleksei Pleshakov <qro...@gmail.com> wrote: > Currently I am trying to understand what particular KLEE execution > statistics are important for me to know Depends on what you're doing. As a user you are probably interested in coverage (ICov), as a developer in the stats you try to optimise (e.g. solving time, coverage, cache hits). > so could you please elaborate on the meaning of "active states"? I > assume that is about ExectionState object, and active state means > being processed in the engine at the moment. So does the option > MaxStates stand for the number of forks that are analyzed > simultaneously? "Active states" is the number of states that are handled at some point in time during execution. (This does not include states that were already terminated.) When you dump the corresponding sqlite file (run.stats) you get the time stamps and the number of states at that time. You can also visualise the data in Grafana (see docs). The last row for run.stats is usually written after terminating all states, hence the "States" statistic is empty when using klee-stats. "AvgStates" is the average value of the corresponding column (NumStates) and "MaxStates", similarly, the maximum value of that column. Be careful when using those statistics, some benchmarks start with hundreds of thousands of states but degrade to a single one due to memory pressure. You might miss such cases just by looking at avg/max. > Also, could you please hint me what wrt and wall time are? wrt - "with respect to" wall time - execution time of KLEE (wall clock time, opposed to user/system time etc.) > And would you mind what time does Tfork measure? This is roughly the time spent in KLEE's branch/fork functions and includes things as checking path feasibility, attaching constraints and maintaining the process tree. It is not the time spent forking STP ;). Kind regards, Frank _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev