projects
/
model-checker.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
81ea453
)
model: rearrange conditionals, fixup take_step()
author
Brian Norris
<banorris@uci.edu>
Wed, 3 Oct 2012 21:50:30 +0000
(14:50 -0700)
committer
Brian Norris
<banorris@uci.edu>
Wed, 3 Oct 2012 21:57:20 +0000
(14:57 -0700)
model.cc
patch
|
blob
|
history
diff --git
a/model.cc
b/model.cc
index 39a7c2170f59fb0ac9b3a7d2160ecb80027283ff..8b7201f1b88c4edf98475e0ebeadc7ecd6fd6f32 100644
(file)
--- a/
model.cc
+++ b/
model.cc
@@
-1756,7
+1756,7
@@
bool ModelChecker::take_step() {
if (has_asserted())
return false;
if (has_asserted())
return false;
- Thread *
curr = thread_current();
+ Thread *curr = thread_current();
if (curr) {
if (curr->get_state() == THREAD_READY) {
ASSERT(priv->current_action);
if (curr) {
if (curr->get_state() == THREAD_READY) {
ASSERT(priv->current_action);
@@
-1770,22
+1770,22
@@
bool ModelChecker::take_step() {
ASSERT(false);
}
}
ASSERT(false);
}
}
- Thread *
next = scheduler->next_thread(priv->nextThread);
+ Thread *next = scheduler->next_thread(priv->nextThread);
/* Infeasible -> don't take any more steps */
if (!isfeasible())
return false;
/* Infeasible -> don't take any more steps */
if (!isfeasible())
return false;
- if (next)
- next->set_state(THREAD_RUNNING);
DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
/* next == NULL -> don't take any more steps */
if (!next)
return false;
DEBUG("(%d, %d)\n", curr ? curr->get_id() : -1, next ? next->get_id() : -1);
/* next == NULL -> don't take any more steps */
if (!next)
return false;
- if ( next->get_pending() != NULL ) {
- //restart a pending action
+ next->set_state(THREAD_RUNNING);
+
+ if (next->get_pending() != NULL) {
+ /* restart a pending action */
set_current_action(next->get_pending());
next->set_pending(NULL);
next->set_state(THREAD_READY);
set_current_action(next->get_pending());
next->set_pending(NULL);
next->set_state(THREAD_READY);