projects
/
model-checker.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
main, threads: improve comments regarding thread stepping
[model-checker.git]
/
model.cc
diff --git
a/model.cc
b/model.cc
index 98c6e645382bf2bdc32bc75e45e3a90b1de4a3cd..d2e9f5ebecb16ee52c00aa323a16405061a5668b 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-171,8
+171,9
@@
bool ModelChecker::next_execution()
num_executions++;
num_executions++;
- if (isfinalfeasible() || DBG_ENABLED())
- print_summary();
+ bool feasible = isfinalfeasible();
+ if (feasible || DBG_ENABLED())
+ print_summary(feasible);
if ((diverge = model->get_next_backtrack()) == NULL)
return false;
if ((diverge = model->get_next_backtrack()) == NULL)
return false;
@@
-338,7
+339,7
@@
void ModelChecker::check_current_action(void)
if (!already_added)
add_action_to_lists(curr);
if (!already_added)
add_action_to_lists(curr);
- /* Is there a better interface for setting the next thread rather
+ /*
* @todo
Is there a better interface for setting the next thread rather
than this field/convoluted approach? Perhaps like just returning
it or something? */
than this field/convoluted approach? Perhaps like just returning
it or something? */
@@
-352,7
+353,8
@@
void ModelChecker::check_current_action(void)
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
Node *currnode = curr->get_node();
Node *parnode = currnode->get_parent();
- if (!parnode->backtrack_empty()||!currnode->read_from_empty()||!currnode->future_value_empty()||!currnode->promise_empty())
+ if (!parnode->backtrack_empty() || !currnode->read_from_empty() ||
+ !currnode->future_value_empty() || !currnode->promise_empty())
if (!next_backtrack || *curr > *next_backtrack)
next_backtrack = curr;
if (!next_backtrack || *curr > *next_backtrack)
next_backtrack = curr;
@@
-704,7
+706,7
@@
static void print_list(action_list_t *list)
printf("---------------------------------------------------------------------\n");
}
printf("---------------------------------------------------------------------\n");
}
-void ModelChecker::print_summary(
void
)
+void ModelChecker::print_summary(
bool feasible
)
{
printf("\n");
printf("Number of executions: %d\n", num_executions);
{
printf("\n");
printf("Number of executions: %d\n", num_executions);
@@
-712,7
+714,7
@@
void ModelChecker::print_summary(void)
scheduler->print();
scheduler->print();
- if (!
isfinalfeasible()
)
+ if (!
feasible
)
printf("INFEASIBLE EXECUTION!\n");
print_list(action_trace);
printf("\n");
printf("INFEASIBLE EXECUTION!\n");
print_list(action_trace);
printf("\n");