nodestack.h

   1 /** @file nodestack.h
   2  *  @brief Stack of operations for use in backtracking.
   3  */
   4
   5 #ifndef __NODESTACK_H__
   6 #define __NODESTACK_H__
   7
   8 #include <cstddef>
   9 #include <inttypes.h>
  10
  11 #include "mymemory.h"
  12 #include "schedule.h"
  13 #include "stl-model.h"
  14 #include "classlist.h"
  15
  16 /**
  17  * @brief A single node in a NodeStack
  18  *
  19  * Represents a single node in the NodeStack. Each Node is associated with up
  20  * to one action and up to one parent node. A node holds information
  21  * regarding the last action performed (the "associated action"), the thread
  22  * choices that have been explored (explored_children) and should be explored
  23  * (backtrack), and the actions that the last action may read from.
  24  */
  25 class Node {
  26 public:
  27         Node(ModelAction *act);
  28         ~Node();
  29
  30         ModelAction * get_action() const { return action; }
  31         void set_uninit_action(ModelAction *act) { uninit_action = act; }
  32         ModelAction * get_uninit_action() const { return uninit_action; }
  33         void print() const;
  34
  35         SNAPSHOTALLOC
  36 private:
  37         ModelAction * const action;
  38
  39         /** @brief ATOMIC_UNINIT action which was created at this Node */
  40         ModelAction *uninit_action;
  41 };
  42
  43 typedef SnapVector<Node *> node_list_t;
  44
  45 /**
  46  * @brief A stack of nodes
  47  *
  48  * Holds a Node linked-list that can be used for holding backtracking,
  49  * may-read-from, and replay information. It is used primarily as a
  50  * stack-like structure, in that backtracking points and replay nodes are
  51  * only removed from the top (most recent).
  52  */
  53 class NodeStack {
  54 public:
  55         NodeStack();
  56         ~NodeStack();
  57
  58         void register_engine(const ModelExecution *exec);
  59         ModelAction * explore_action(ModelAction *act);
  60         Node * get_head() const;
  61         Node * get_next() const;
  62         void reset_execution();
  63         void full_reset();
  64         void print() const;
  65
  66         SNAPSHOTALLOC
  67 private:
  68         node_list_t node_list;
  69         const struct model_params * get_params() const;
  70
  71         /** @brief The model-checker execution object */
  72         const ModelExecution *execution;
  73
  74         /**
  75          * @brief the index position of the current head Node
  76          *
  77          * This index is relative to node_list. The index should point to the
  78          * current head Node. It is negative when the list is empty.
  79          */
  80         int head_idx;
  81 };
  82
  83 #endif  /* __NODESTACK_H__ */