projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
f559a99
)
model: add "# redundant" stat
author
Brian Norris
<banorris@uci.edu>
Sat, 17 Nov 2012 08:01:18 +0000
(
00:01
-0800)
committer
Brian Norris
<banorris@uci.edu>
Sat, 17 Nov 2012 08:01:18 +0000
(
00:01
-0800)
model.cc
patch
|
blob
|
history
model.h
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index eb5cd347e0442d60cdd35fea377afe189cea2177..df06760893018d5bc1756cd89df263c6ed117cc6 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-401,12
+401,15
@@
void ModelChecker::record_stats()
stats.num_buggy_executions++;
else if (is_complete_execution())
stats.num_complete++;
stats.num_buggy_executions++;
else if (is_complete_execution())
stats.num_complete++;
+ else
+ stats.num_redundant++;
}
/** @brief Print execution stats */
void ModelChecker::print_stats() const
{
model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
}
/** @brief Print execution stats */
void ModelChecker::print_stats() const
{
model_print("Number of complete, bug-free executions: %d\n", stats.num_complete);
+ model_print("Number of redundant executions: %d\n", stats.num_redundant);
model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
model_print("Total executions: %d\n", stats.num_total);
model_print("Number of buggy executions: %d\n", stats.num_buggy_executions);
model_print("Number of infeasible executions: %d\n", stats.num_infeasible);
model_print("Total executions: %d\n", stats.num_total);
diff --git
a/model.h
b/model.h
index 0d27d5a305d1830b75ac3519e294816f85bc88de..15516e267cfbb9b7c8947ed8d550926e59de8a98 100644
(file)
--- a/
model.h
+++ b/
model.h
@@
-58,6
+58,7
@@
struct execution_stats {
int num_infeasible; /**< @brief Number of infeasible executions */
int num_buggy_executions; /** @brief Number of buggy executions */
int num_complete; /**< @brief Number of feasible, non-buggy, complete executions */
int num_infeasible; /**< @brief Number of infeasible executions */
int num_buggy_executions; /** @brief Number of buggy executions */
int num_complete; /**< @brief Number of feasible, non-buggy, complete executions */
+ int num_redundant; /**< @brief Number of redundant, aborted executions */
};
struct PendingFutureValue {
};
struct PendingFutureValue {