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
*
const ModelAction * get_read_from();
bool increment_read_from();
bool read_from_empty();
+ int get_read_from_size();
+ const ModelAction * get_read_from_at(int i);
void set_promise(unsigned int i);
bool get_promise(unsigned int i);
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;
};