3 * @brief Provides structures for queueing ModelChecker actions to be taken
6 #ifndef __WORKQUEUE_H__
7 #define __WORKQUEUE_H__
10 #include "stl-model.h"
15 WORK_NONE = 0, /**< No work to be done */
16 WORK_CHECK_CURR_ACTION, /**< Check the current action; used for the
17 first action of the work loop */
18 WORK_CHECK_RELEASE_SEQ, /**< Check if any pending release sequences
20 WORK_CHECK_MO_EDGES, /**< Check if new mo_graph edges can be added */
25 class WorkQueueEntry {
27 /** @brief Type of work queue entry */
31 * @brief Object affected
32 * @see CheckRelSeqWorkEntry
37 * @brief The ModelAction to work on
38 * @see MOEdgeWorkEntry
44 * @brief Work: perform initial promise, mo_graph checks on the current action
46 * This WorkQueueEntry performs the normal, first-pass checks for a ModelAction
47 * that is currently being explored. The current ModelAction (@a action) is the
48 * only relevant parameter to this entry.
50 class CheckCurrWorkEntry : public WorkQueueEntry {
53 * @brief Constructor for a "check current action" work entry
54 * @param curr The current action
56 CheckCurrWorkEntry(ModelAction *curr) {
57 type = WORK_CHECK_CURR_ACTION;
64 * @brief Work: check an object location for resolved release sequences
66 * This WorkQueueEntry checks synchronization and the mo_graph for resolution
67 * of any release sequences. The object @a location is the only relevant
68 * parameter to this entry.
70 class CheckRelSeqWorkEntry : public WorkQueueEntry {
73 * @brief Constructor for a "check release sequences" work entry
74 * @param l The location which must be checked for release sequences
76 CheckRelSeqWorkEntry(void *l) {
77 type = WORK_CHECK_RELEASE_SEQ;
84 * @brief Work: check a ModelAction for new mo_graph edges
86 * This WorkQueueEntry checks for new mo_graph edges for a particular
87 * ModelAction (e.g., that was just generated or that updated its
88 * synchronization). The ModelAction @a action is the only relevant parameter
91 class MOEdgeWorkEntry : public WorkQueueEntry {
94 * @brief Constructor for a mo_edge work entry
95 * @param updated The ModelAction which was updated, triggering this work
97 MOEdgeWorkEntry(ModelAction *updated) {
98 type = WORK_CHECK_MO_EDGES;
104 /** @brief typedef for the work queue type */
105 typedef ModelList<WorkQueueEntry> work_queue_t;
107 #endif /* __WORKQUEUE_H__ */