* @param i The promise index.
* @return true if the promise should be satisfied by the given model action.
*/
* @param i The promise index.
* @return true if the promise should be satisfied by the given model action.
*/
* Returns whether the promise set is empty.
* @return true if we have explored all promise combinations.
*/
* Returns whether the promise set is empty.
* @return true if we have explored all promise combinations.
*/
* Checks whether the future_values set for this node is empty.
* @return true if the future_values set is empty.
*/
* Checks whether the future_values set for this node is empty.
* @return true if the future_values set is empty.
*/
* Checks whether the readsfrom set for this node is empty.
* @return true if the readsfrom set is empty.
*/
* Checks whether the readsfrom set for this node is empty.
* @return true if the readsfrom set is empty.
*/
{
int thread_id=id_to_int(t->get_id());
return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
}
{
int thread_id=id_to_int(t->get_id());
return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
}
{
int thread_id=id_to_int(tid);
return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
}
{
int thread_id=id_to_int(tid);
return thread_id < num_threads && (enabled_array[thread_id] != THREAD_DISABLED);
}
ASSERT(future_index >= 0 && future_index<((int)future_values.size()));
return future_values[future_index].value;
}
ASSERT(future_index >= 0 && future_index<((int)future_values.size()));
return future_values[future_index].value;
}
ASSERT(future_index >= 0 && future_index<((int)future_values.size()));
return future_values[future_index].expiration;
}
ASSERT(future_index >= 0 && future_index<((int)future_values.size()));
return future_values[future_index].expiration;
}
* @return A write that may break the release sequence. If NULL, that means
* the release sequence should not be broken.
*/
* @return A write that may break the release sequence. If NULL, that means
* the release sequence should not be broken.
*/
{
if (relseq_break_index < (int)relseq_break_writes.size())
return relseq_break_writes[relseq_break_index];
{
if (relseq_break_index < (int)relseq_break_writes.size())
return relseq_break_writes[relseq_break_index];
{
model_print("............................................\n");
model_print("NodeStack printing node_list:\n");
{
model_print("............................................\n");
model_print("NodeStack printing node_list:\n");