improve scheduler debugging

diff --git a/model.cc b/model.cc
index bf956804479f3f1e82fe8f04fb273d50ce7c9cbb..773d723e2a6a0db67f1419c0d7276080002bbf11 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -175,6 +175,10 @@ void ModelChecker::print_trace(void)
        printf("---------------------------------------------------------------------\n");
        printf("Total nodes created: %d\n\n", TreeNode::getTotalNodes());
 
+       scheduler->print();
+
+       printf("\nTrace:\n\n");
+
        for (it = action_trace->begin(); it != action_trace->end(); it++) {
                DBG();
                (*it)->print();

diff --git a/schedule.cc b/schedule.cc
index d344fb1acdcf858db73d098b7341a8dae930125f..0f550c41962a5046c6934fe5380d17e0cda39e36 100644 (file)
--- a/schedule.cc
+++ b/schedule.cc
@@ -40,7 +40,7 @@ void Scheduler::print()
                printf("Current thread: %d\n", current->get_id());
        else
                printf("No current thread\n");
-       printf("# Threads in ready list: %ld\n", readyList.size());
+       printf("Num. threads in ready list: %ld\n", readyList.size());
 
        std::list<Thread *>::iterator it;
        for (it = readyList.begin(); it != readyList.end(); it++)