*/
void Node::set_promise(unsigned int i) {
if (i >= promises.size())
- promises.resize(i + 1, 0);
- promises[i] = 1;
+ promises.resize(i + 1, PROMISE_IGNORE);
+ promises[i] = PROMISE_UNFULFILLED;
}
/**
* @return true if the promise should be satisfied by the given model action.
*/
bool Node::get_promise(unsigned int i) {
- return (i < promises.size()) && (promises[i] == 2);
+ return (i < promises.size()) && (promises[i] == PROMISE_FULFILLED);
}
/**
*/
bool Node::increment_promise() {
for (unsigned int i = 0; i < promises.size(); i++) {
- if (promises[i] == 1) {
- promises[i] = 2;
+ if (promises[i] == PROMISE_UNFULFILLED) {
+ promises[i] = PROMISE_FULFILLED;
while (i > 0) {
i--;
- if (promises[i] == 2)
- promises[i] = 1;
+ if (promises[i] == PROMISE_FULFILLED)
+ promises[i] = PROMISE_UNFULFILLED;
}
return true;
}
*/
bool Node::promise_empty() {
for (unsigned int i = 0; i < promises.size();i++)
- if (promises[i] == 1)
+ if (promises[i] == PROMISE_UNFULFILLED)
return false;
return true;
}
class ModelAction;
+/**
+ * A flag used for the promise counting/combination problem within a node,
+ * denoting whether a particular Promise is
+ * <ol><li>@b applicable: can be satisfied by this Node's ModelAction and</li>
+ * <li>@b fulfilled: satisfied by this Node's ModelAction under the current
+ * configuration.</li></ol>
+ */
+typedef enum {
+ PROMISE_IGNORE = 0, /**< This promise is inapplicable; ignore it */
+ PROMISE_UNFULFILLED, /**< This promise is applicable but unfulfilled */
+ PROMISE_FULFILLED /**< This promise is applicable and fulfilled */
+} promise_t;
+
/**
* @brief A single node in a NodeStack
*
unsigned int read_from_index;
std::vector< uint64_t, MyAlloc< uint64_t > > future_values;
- std::vector< unsigned int, MyAlloc<unsigned int> > promises;
+ std::vector< promise_t, MyAlloc<promise_t> > promises;
unsigned int future_index;
};