CycleGraph::checkForCycles() is a cheap function; it only checks a flag status.
So we don't need to make code more complicated just to avoid calling this
function.
Effectively a revert of:
commit
7cee72d776ddfbf585038f3cad3df799e353cc11
- bool feasible = isfinalfeasible();
- if (feasible || DBG_ENABLED())
- print_summary(feasible);
+ if (isfinalfeasible() || DBG_ENABLED())
+ print_summary();
if ((diverge = model->get_next_backtrack()) == NULL)
return false;
if ((diverge = model->get_next_backtrack()) == NULL)
return false;
printf("---------------------------------------------------------------------\n");
}
printf("---------------------------------------------------------------------\n");
}
-void ModelChecker::print_summary(bool feasible)
+void ModelChecker::print_summary()
{
printf("\n");
printf("Number of executions: %d\n", num_executions);
{
printf("\n");
printf("Number of executions: %d\n", num_executions);
+ if (!isfinalfeasible())
printf("INFEASIBLE EXECUTION!\n");
print_list(action_trace);
printf("\n");
printf("INFEASIBLE EXECUTION!\n");
print_list(action_trace);
printf("\n");
void check_current_action(void);
void check_current_action(void);
- /**
- * Prints an execution summary with trace information.
- * @param feasible Formats outputting according to whether or not the
- * current trace is feasible. Defaults to feasible = true.
- */
- void print_summary(bool feasible = true);
+ /** Prints an execution summary with trace information. */
+ void print_summary();
Thread * schedule_next_thread();
Thread * schedule_next_thread();