X-Git-Url: http://plrg.eecs.uci.edu/git/?p=model-checker.git;a=blobdiff_plain;f=action.h;h=976fd4881c8033c277d3d2b7d27b781a08b693a6;hp=53107ea81762d33ab6a63ef2fa7e69176b379b1c;hb=ece544635301a0410fb98369b732e26ced95329e;hpb=06c0e4f929e94ae837186b50d7d75138bf2d0fd2

diff --git a/action.h b/action.h
index 53107ea..976fd48 100644
--- a/action.h
+++ b/action.h
@@ -1,3 +1,7 @@
+/** @file action.h
+ *  @brief Models actions taken by threads.
+ */
+
 #ifndef __ACTION_H__
 #define __ACTION_H__
 
@@ -21,10 +25,10 @@ typedef enum action_type {
 /* Forward declaration */
 class Node;
 class ClockVector;
+
 /**
  * The ModelAction class encapsulates an atomic action.
  */
-
 class ModelAction {
 public:
 	ModelAction(action_type_t type, memory_order order, void *loc, int value);
@@ -42,11 +46,13 @@ public:
 
 	bool is_read();
 	bool is_write();
+	bool is_rmw();
 	bool is_acquire();
 	bool is_release();
+	bool is_seqcst();
 	bool same_var(ModelAction *act);
 	bool same_thread(ModelAction *act);
-	bool is_dependent(ModelAction *act);
+	bool is_synchronizing(ModelAction *act);
 
 	void create_cv(ModelAction *parent = NULL);
 	void read_from(ModelAction *act);
@@ -73,16 +79,18 @@ private:
 	/** The thread id that performed this action. */
 	thread_id_t tid;
 	
-	/** The value written.  This should probably be something longer. */
+	/** The value read or written (if RMW, then the value written). This
+	 * should probably be something longer. */
 	int value;
 
+	/** A back reference to a Node in NodeStack, if this ModelAction is
+	 * saved on the NodeStack. */
 	Node *node;
 	
 	int seq_number;
 
-	/** The clock vector stored with this action if this action is a
-	 *  store release */
-
+	/** The clock vector stored with this action; only needed if this
+	 * action is a store release? */
 	ClockVector *cv;
 };