nodestack/model: refactor explore_action(), change return semantics
authorBrian Norris <banorris@uci.edu>
Tue, 19 Jun 2012 22:44:13 +0000 (15:44 -0700)
committerBrian Norris <banorris@uci.edu>
Tue, 19 Jun 2012 22:44:13 +0000 (15:44 -0700)
commiteb8e9f61a400856421465d95ac52d9cffed2a491
treef40c0f19bebf8b6f393c1a41908939bedd422e0b
parentd6df701e914b99ba0ca51706a66ab46e138137b6
nodestack/model: refactor explore_action(), change return semantics

ModelChecker would like to know when a new ModelAction is being inserted
into the NodeStack vs. when the new ModelAction should be discarded in
favor of a pre-existing one (due to replay). So I change the semantics of
NodeStack::explore_action() such that it does not always return a
ModelAction; now it returns NULL if the ModelAction was accepted into the
NodeStack, otherwise returning the ModelAction that was already in the
stack.

Now, ModelChecker can choose when to create new clock vectors as well as
other operations (to come) that may be performed only upon *first*
exploration of a new ModelAction.

Additionally, ModelChecker is now responsible for free-ing the ModelAction
if it is not going to be kept in NodeStack.

There should be no change in functionality.
model.cc
nodestack.cc