/******************************************************************************
 * File:		umm.m
 * Description:	This is the Murphi implementation of the JMM specified in the 
 *				Uniform Memory Model (UMM) framework. UMM uses a generic  
 *				transition system to specify a formal executable memory model  
 *				in a shared memory system. Test programs can be exhaustively  
 *				excercised against the model for verification. 
 *
 *				The formal JMM specification is described in the paper 
 *				"Specifying Java Thread Semantics Using	a Uniform Memory Model". 
 *				(Available at http://www.cs.utah.edu/~yyang/research/umm.pdf.)
 * 
 * Author:		Yue Yang
 *
 * Date:		Created:		03/01/2002
 *				Last updated:	07/26/2002
 *
 * Usage:		To download and set up the Murphi utility, check 
 *				http://verify.stanford.edu/dill/murphi.html.
 *
 *				To run this program:
 *					1) mu umm.m (this compiles umm.m and generates umm.C)
 *					2) g++ umm.C -I"<path of Murphi3.1/include>" (generates a.exe)
 *					3) run a.exe:
 *					   a -h (to check all options)
 *					   a -tv -ndl(show violation trace, when CFG_SHOW_ALL = False)
 *					   a -ndl (show all interleaving, when CFG_SHOW_ALL = True)
 *
 *				To configure a test:
 *					1) set MyTest to one of the test names defined in TestType_t.
 *					2) set CFG_SHOW_ALL to True (all results) or False (show trace).
 *					3) configure the scope parameters (*_NUM), if necessary.
 *
 *				To add a new test program:
 *					1) add a name in TestType_t for the test case
 *					2) in Startstate, initialize the abstract machine for the test:
 *						a) declare the variable type (default is VAR_NORMAL)
 *						b) use "addDefault" to add the default value for each variable
 *						c) use "add" to set up the local instruction buffer
 *					3) add the desired output messages in Rule "Output final result"
 *					4) add the desired invariant in Invariant "Invariant Test"
 *
 *				To configure the memory model:
 *					- set up MyMemModel from MMType_t (currently only JMM_MP implemented.)
 *					- set CFG_VOLATILE_SC for SC or non-atomic volatile writes.
 *
 * Implementation Comments:	
 *				- GIB size: LABEL_NUM * THREAD_NUM + VAR_NUM is the worst case, could
 *				  be customized per test to reduce the size.
 *				- notRedundant() and alias analysis involves global analysis, 
 *				  currently manually configured via CFG_REDUNDANT_LOCK and CFG_ALIAS.
 *				- This release supports limited computational instructions through
 *				  hardcoding procedure compute().
 * 
 * Copyright:	(c) Yue Yang 2002
 ******************************************************************************/

/**************************************************************************
 *
 * Config Options for test programs
 *
 **************************************************************************/
Type
	/* Different test cases: */
	TestType_t: Enum {
		TEST_PrescientStore,
		TEST_PrescientStore2,
		TEST_WriteAtomicity,
		TEST_VolatileCoherence,
		TEST_Volatile,
		TEST_VolatileBarrier,
		TEST_VolatileWA2,
		TEST_VolatileWA3,
		TEST_VolatileFlag,
		TEST_VolatileSync,
		TEST_Coherence2,
		TEST_EndCon1,	
		TEST_EndCon2,	
		TEST_DoubleCheck,
		TEST_DoubleCheck2,
		TEST_PRAM,	
		TEST_PRAM2,
		TEST_Causality,
		TEST_Causality2,
		TEST_Causal,
		TEST_WAW,			
		TEST_WR,	
		TEST_WA,
		TEST_SC,	
		TEST_PC,
		TEST_RO,				
		TEST_WOS,	
		TEST_Alpha1,
		TEST_Alpha2,
		TEST_Alpha3,
		TEST_Alpha4,
		TEST_Alpha5,
		TEST_Sync1,
		TEST_Sync2, 
		TEST_Sync3,
		TEST_CausalLoop1,
		TEST_CausalLoop2,
		TEST_CausalLoop3,
		TEST_CausalLoop4,
		TEST_Init,
		TEST_Final,
		TEST_Final2
	};

Const
	/* Set MyTest to run a test program. Must choose from TestType_t above. */
	MyTest: TEST_WR;

	/* 
	 * If True: prints out all possible results of the test (but no trace.)
	 * If False: check all invariants, show a violation trace, if existed.
	 */	
	CFG_SHOW_ALL:	True;	

	/* If True: assume A and B are aliased. */
	CFG_ALIAS:		False;	

	/* If True: assume all locks are redundant (thread local or nested) */
	CFG_REDUNDANT_LOCK: False;

	/* 
	 * If True: use SC for volatiles 
	 * If False: allow non-atomic volatile writes.
	 */
	CFG_VOLATILE_SC: True;

/**************************************************************************
 *
 * Config Options for the Abstract Machine
 *
 **************************************************************************/
Const
	/* Scope Parameters */
	THREAD_NUM:		4;		/* max number of threads, NOT including Tinit */
	VAR_NUM:		4;		/* max number of total global variables */
	LOCAL_NUM:		4;		/* max number of local variables */
	VALUE_NUM:		5;		/* data range */
	LABEL_NUM:		7;		/* max number of instructions per thread */
	LOCK_NUM:		2;		/* max number of locks */
	LOCK_CNT_NUM:	1;		/* max recursive lock levels allowed, should > 0
							   if LOCK_NUM != 0 */

	/* 
	 * max number of previous writes to store in GIB 
	 * (default values are initialized in GIB)
	 */	
	GIB_ENT_NUM:		LABEL_NUM * THREAD_NUM + VAR_NUM;	/* worst case */		
	ALL_THREAD_NUM:		THREAD_NUM + 1;						/* add Tinit */

/**************************************************************************
 * Config Options for the memory model
 **************************************************************************/
Type
	/* MM (Memory Model) related instruction opcodes */
	InsType_t: Enum {
		INS_R,			/* read */ 
		INS_W,			/* write */
		INS_L,			/* lock, enter monitor */
		INS_U,			/* unlock, exit monitor */
		INS_F,			/* freeze final fields at the end of constructor */
		INS_C			/* computation instruction applied to local var,
						   not used in the formal spec */
	};

	/* Operation types used in BYPASS matrix */
	OpType_t: Enum {
		OP_Rn,			/* read normal */
		OP_Wn,			/* write normal */
		OP_Lk,			/* lock */
		OP_Un,			/* unlock */	
		OP_Rv,			/* read volatile */
		OP_Wv,			/* write volatile */
		OP_Rf,			/* read final */
		OP_Wf,			/* write final */
		OP_Fz,			/* freeze finals */
		OP_Cp			/* computation */
	};
	
	/* memory models to be implemented */
	MMType_t: Enum {
		JMM_MP
	};

Const
	/* choose which MM to run. Must choose from above MMType_t */
	MyMemModel: JMM_MP;

	/* max num of op types, num of the enum items for OpType_t */
	OP_TYPE_NUM: 10;

/**************************************************************************
 *
 * Internal data structures - don't need to be changed.
 *
 **************************************************************************/
Const
	/* some useful value constants */
	ZERO:		0;
	ONE:		1;
	TWO:		2;
	THREE:		3;
	FOUR:		4;
	DontCare:	0;		

	/* some useful global variable constants */
	A:			0;
	B:			1;
	C:			2;
	D:			3;

	/* some useful local variable constants */
	r1:			0;
	r2:			1;
	r3:			2;
	r4:			3;
	r5:			4;
	r6:			5;

	/* some useful lock constants */
	L1:			0;
	L2:			1;

	/* Useful thread constants */
	Tinit:		0;
	T1:			1;
	T2:			2;
	T3:			3;
	T4:			4;

Type
	/* Useful Types */
	ThreadId_t: 0..ALL_THREAD_NUM - 1;	/* thread id range */
	Var_t: 0..VAR_NUM - 1;				/* variable range */
	Local_t: 0..LOCAL_NUM - 1;			/* local variable range */
	Value_t: 0..VALUE_NUM - 1;			/* data range */
	Label_t: 0..LABEL_NUM - 1;			/* program counter range */
	GibEnt_t: 0..GIB_ENT_NUM - 1;		/* array range for each GIB entry */

	OpTypeNum_t: 0..OP_TYPE_NUM - 1;	/* dimension size for BYPASS table */

	Lock_t: 0..LOCK_NUM;				/* lock range */
	LockCntNum_t: 0..LOCK_CNT_NUM;		/* recursive lock count range, including 0 */

	/* reordering options */
	Order_t: Enum {
		ORDER_no,			/* default: no, program order can't be relaxed */
		ORDER_yes,			/* yes, program order can be relaxed */
		ORDER_diffVar,		/* program order can be relaxed for different addresses */
		ORDER_redundantLock	/* program order can be relaxed if the lock is redundant */
	};

	/* type of a variable */
	VariableType_t: Enum {
		VAR_NORMAL,			/* default: normal variable */
		VAR_VOLATILE,		/* volatile field */
		VAR_FINAL			/* final field */
	};

	/* instruction tuple in thread local buffers */
	Ins_t: Record
		thread:	ThreadId_t;		/* thread id */
		pc: Label_t;			/* program counter */
		op: OpType_t;			/* operation type */
		v: Var_t;				/* global variable, or "address" */
		data: Value_t;			/* data */
		local: Local_t;			/* local variable id */
		useLocal: Boolean;		/* (only for Writes) if write from local var */
		lock: Lock_t;			/* lock to be grabbed or released */
		done: Boolean;			/* if the instruction has been completed */
	End;

	/* Local Variable array entry */	
	LVEnt_t: Record
		data: Value_t;			/* data value of the local var */
		valid: Boolean;			/* if it is valid */
	End;

	/* thread structure */
	Thread_t: Record
		LIB: Array[Label_t] of Ins_t;	/* thread local instruction buffer */
		len: 0..LABEL_NUM;				/* number of total instructions in LIB */
		LV: Array[Local_t] of LVEnt_t;	/* local variables */
	End;

	/* global instruction buffer instruction tuple */
	GibIns_t: Record
		thread:	ThreadId_t;		/* thread id */
		pc: Label_t;			/* program counter */
		op: OpType_t;			/* operation type */
		v: Var_t;				/* global variable, or "address" */
		data: Value_t;			/* data */
		lock: Lock_t;			/* lock to be grabbed or released */
		useNew: Boolean;		/* tag to support non-atomic volatile write */
		time: GibEnt_t;			/* index of this write entry, incremented each
								   time an instruction is appended to GIB. */
	End;
	
	/* Global Instruction Buffer (GIB) entry structure */
	GIB_t: Record
		arr: Array[GibEnt_t] of GibIns_t;	/* to record previous writes for a var */
		len: 0..GIB_ENT_NUM;				/* actural length of the array */
	End;

	/* LOCK array entry */
	LockEnt_t: Record
		count: LockCntNum_t;	
		owner: ThreadId_t;
	End;

/******************************************************************************
 *
 * Global variables of the Abstract Machine.
 * 
 ******************************************************************************/
Var
	/* threads */
	Thread: Array[ThreadId_t] of Thread_t;

	/* global instruction buffer */
	GIB: GIB_t;	

	/* Lock array, to store lock related information */
	LOCK: Array[Lock_t] of LockEnt_t;

	/* array to record var types */
	VarType: Array[Var_t] of VariableType_t;

	/* MM program order rules */
	BYPASS: Array[OpTypeNum_t] of Array[OpTypeNum_t] of Order_t;

/******************************************************************************
 *
 * Functions and Procedures
 *
 ******************************************************************************/

/******************************************************************************
 * inBound()
 * First parameter is a LIB index; Second parameter is the LIB range.
 ******************************************************************************/
Function inBound(i:0..LABEL_NUM - 1; j:0..LABEL_NUM): Boolean;
Begin
	Return (i < j);
End;

/******************************************************************************
 * notComplete(i)
 * Returns True if the local instruction is not completed. 
 ******************************************************************************/
Function notComplete(i: Ins_t): Boolean;
Begin
	Return (i.done = False);
End;

/******************************************************************************
 * isRead(i)
 * Returns True if i is one of the read instructions.
 ******************************************************************************/
Function isRead(i: Ins_t): Boolean;
Begin
	Return (i.op = OP_Rn | i.op = OP_Rf | i.op = OP_Rv);
End;

/******************************************************************************
 * isWrite(i)
 * Returns True if i is one of the write instructions.
 ******************************************************************************/
Function isWrite(i: Ins_t): Boolean;
Begin
	Return (i.op = OP_Wn | i.op = OP_Wf | i.op = OP_Wv);
End;

/******************************************************************************
 * sameThread(t1:ThreadId_t; t2:ThreadId_t)
 *
 * Returns True if thread number equals. 
 ******************************************************************************/
Function sameThread(t1:ThreadId_t; t2:ThreadId_t): Boolean;
Begin
	Return (t1 = t2);
End;

/******************************************************************************
 * sameVar(v1, v2)
 * Returns True if the variables are the same.
 ******************************************************************************/
Function sameVar(v1: Var_t; v2: Var_t): Boolean;
Begin
	Return (v1 = v2 | CFG_ALIAS);
End;

/******************************************************************************
 * lockMatch
 * Returns True if u and l match for synchronization.
 ******************************************************************************/
Function lockMatch(l:GibIns_t; u:GibIns_t): Boolean;
Begin
	Return
	(
		/* matching Unlock/Lock on the same lcok */
		l.op = OP_Lk & u.op = OP_Un & l.lock = u.lock 
		|
		/* matching Write/Read on the same volatile */
		l.op = OP_Rv & u.op = OP_Wv & sameVar(l.v, u.v)
	);
End;

/******************************************************************************
 * synchronized(i1: GibIns_t; i2:GibIns_t): Boolean;
 * Returns True if i1 and i2 are synchronized according to Location Consistency.
 ******************************************************************************/
Function synchronized(i1: GibIns_t; i2:GibIns_t): Boolean;
Begin
	Return
	(
		(Exists l: GibEnt_t Do
			(Exists u: GibEnt_t Do	
				l < GIB.len & u < GIB.len 
				&
				lockMatch(GIB.arr[l], GIB.arr[u]) 
				&
				sameThread(GIB.arr[l].thread, i1.thread) 
				& 
				( sameThread(GIB.arr[u].thread, i2.thread) | 
				sameThread(i2.thread, Tinit) ) 
				&
				i2.time <= GIB.arr[u].time & 
				GIB.arr[u].time < GIB.arr[l].time & 
				GIB.arr[l].time <= i1.time
			End)
		End)
	);
End; /* synchronized */

/******************************************************************************
 * LCOrder(i1: GibIns_t; i2:GibIns_t): Boolean;
 * Returns True if i1 and i2 need to obey the ordering of Location Consistency.
 ******************************************************************************/
Function LCOrder(i1: GibIns_t; i2:GibIns_t): Boolean;
Begin
	Return 
	(
		( sameThread(i1.thread, i2.thread) & i1.pc > i2.pc | 
		!sameThread(i1.thread, Tinit) & sameThread(i2.thread, Tinit) ) 
		|
		synchronized(i1, i2) 
		|
		(Exists k: GibEnt_t Do
			k < GIB.len & GIB.arr[k].time > i2.time & GIB.arr[k].time < i1.time &
			LCOrder(i1, GIB.arr[k]) & LCOrder(GIB.arr[k], i2)
		End) 
	);
End; /* LCOrder */

/******************************************************************************
 * legalNormalWrite(r:Ins_t; w:GibIns_t)
 *
 * Returns True if w is a global Most Recent Predecessor Write of r. 
 ******************************************************************************/
Function legalNormalWrite(r:Ins_t; w:GibIns_t): Boolean;
Var
	tmp: GibIns_t;
Begin
	Assert(r.op = OP_Rn) "legalNormalWrite enter";

	/* set up a tmp read global instruction so that we can call LCOrder */
	tmp.thread := r.thread;
	tmp.pc := r.pc;
	tmp.op := r.op;
	tmp.v := r.v;
	tmp.data := r.data;
	tmp.time := GIB.len;

	Return
	(	
		w.op = OP_Wn & sameVar(w.v, r.v) 
		&
		(sameThread(w.thread, r.thread) -> (w.pc < r.pc))
		&
		!(Exists k: GibEnt_t Do
				k < GIB.len & GIB.arr[k].op = OP_Wn & sameVar(GIB.arr[k].v, r.v) &
				LCOrder(tmp, GIB.arr[k]) & LCOrder(GIB.arr[k], w)
		End) 
	);
End; /* legalNormalWrite */

/******************************************************************************
 * legalOldWrite
 * legalOldWrite and legalNewWrite are used to model non-atomic volatile writes.
 *
 * Returns True if w is a valid old volatile write of r.
 ******************************************************************************/
Function legalOldWrite(r: Ins_t; w: GibIns_t): Boolean;
Begin
	Assert(r.op = OP_Rv) "legalOldWrite enter";

	Return
	(
		w.op = OP_Wv & sameVar(w.v, r.v) &
		!sameThread(r.thread, w.thread) &
		(Exists k1: GibEnt_t Do
			k1 < GIB.len &
			GIB.arr[k1].op = OP_Wv & sameVar(GIB.arr[k1].v, r.v) & 
			GIB.arr[k1].time > w.time  
			&
			!(Exists k2: GibEnt_t Do
				k2 < GIB.len & 
				GIB.arr[k2].op = OP_Wv & sameVar(GIB.arr[k2].v, r.v) &
				GIB.arr[k2].time > w.time & 
				GIB.arr[k2].time != GIB.arr[k1].time 
			End) 
			&
			!(Exists k3: GibEnt_t Do
				k3 < GIB.len & 
				GIB.arr[k3].op = OP_Rv &
				sameThread(GIB.arr[k3].thread, r.thread) & sameVar(GIB.arr[k3].v, r.v) &
				GIB.arr[k3].time > w.time &
				GIB.arr[k3].useNew 
			End)	
			&
			!(Exists k4: GibEnt_t Do
				k4 < GIB.len & 
				sameThread(GIB.arr[k4].thread, GIB.arr[k1].thread) &
				GIB.arr[k4].pc > GIB.arr[k1].pc & 
				GIB.arr[k4].op != OP_Wn
			End)	
		End) 
	);
End;

/******************************************************************************
 * legalNewWrite
 * Returns True if w is a valid new volatile write of r.
 ******************************************************************************/
Function legalNewWrite(r: Ins_t; w: GibIns_t): Boolean;
Begin
	Assert(r.op = OP_Rv ) "legalNewWrite enter";

	Return
	(
		w.op = OP_Wv & sameVar(r.v, w.v)
		&
		!(Exists k: GibEnt_t Do
			k < GIB.len &
			GIB.arr[k].op = OP_Wv &	sameVar(GIB.arr[k].v, r.v) &
			GIB.arr[k].time > w.time 
		End)
	);
End;

/******************************************************************************
 * SCOrder(i1: GibIns_t; i2:GibIns_t): Boolean;
 * Returns True if i1 and i2 need to obey the ordering of Sequential Consistency.
 ******************************************************************************/
Function SCOrder(i1: GibIns_t; i2:GibIns_t): Boolean;
Begin
	Return (i1.time > i2.time);
End; 

/******************************************************************************
 * legalVolatileWrite(r:Ins_t; w:GibIns_t)
 *
 * Returns True if w is a global Most Recent Predecessor Write of r. 
 ******************************************************************************/
Function legalVolatileWrite(r:Ins_t; w:GibIns_t): Boolean;
Var
	tmp: GibIns_t;
Begin
	Assert(r.op = OP_Rv) "legalVolatileWrite enter";

	If !CFG_VOLATILE_SC Then 
		/* allow non-atomic volatile writes */
		Return (legalOldWrite(r, w) | legalNewWrite(r, w));
	Else
		/* SC for volatiles */
		/* set up a tmp read global instruction so that we can call LCOrder */
		tmp.thread := r.thread;
		tmp.pc := r.pc;
		tmp.op := r.op;
		tmp.v := r.v;
		tmp.data := r.data;
		tmp.time := GIB.len;

		Return
		(	
			w.op = OP_Wv & sameVar(w.v, r.v) 
			&
			!(Exists k: GibEnt_t Do
					k < GIB.len & GIB.arr[k].op = OP_Wv & sameVar(GIB.arr[k].v, r.v) &
					SCOrder(tmp, GIB.arr[k]) & SCOrder(GIB.arr[k], w)
			End) 
		);
	End;
End; /* legalVolatileWrite */

/******************************************************************************
 * legalFinalWrite
 * Returns True if w is a valid final write of r.
 ******************************************************************************/
Function legalFinalWrite(r: Ins_t; w: GibIns_t): Boolean;
Begin
	Assert (r.op = OP_Rf) "legalFinalWrite enter";

	Return
	(
		w.op = OP_Wf & sameVar(w.v, r.v) &
		(
			sameThread(w.thread, Tinit) ->
			(
				!(Exists i1: GibEnt_t Do
					i1 < GIB.len & GIB.arr[i1].op = OP_Fz & sameVar(GIB.arr[i1].v, r.v)
				End) 
				&
				!(Exists i2: GibEnt_t Do
					i2 < GIB.len & GIB.arr[i2].op = OP_Wf & sameVar(GIB.arr[i2].v, r.v) &
					sameThread(GIB.arr[i2].thread, r.thread)
				End)
			)
		)
	)
End;

/******************************************************************************
 * localDependent(i, j)
 * Returns True if the ordering between j and i is restricted by local data dependency:
 ******************************************************************************/
Function localDependent(i: Ins_t; j:Ins_t): Boolean;
Begin
	Assert (sameThread(i.thread, j.thread) & i.pc > j.pc) "localDependent enter";

	Return
	(
		sameThread(j.thread, i.thread) & 
		j.local = i.local &
		( isWrite(i) & i.useLocal & isRead(j) |
		isWrite(j) & j.useLocal & isRead(i) |
		isRead(i) & isRead(j) )
	);
End;

/******************************************************************************
 * op2id(op)
 * Convert an operation type op into its corresponding id in BYPASS matrix.
 * This is hardcoded, has to match the sequence.
 ******************************************************************************/
Function op2id(op: OpType_t):OpTypeNum_t;
Begin
	Switch op
		Case OP_Rn:			/* read normal */
			Return 0;
		Case OP_Wn:			/* write normal */
			Return 1;
		Case OP_Lk:			/* lock */
			Return 2;
		Case OP_Un:			/* unlock */	
			Return 3;
		Case OP_Rv:			/* read volatile */
			Return 4;
		Case OP_Wv:			/* write volatile */
			Return 5;
		Case OP_Rf:			/* read final */
			Return 6;
		Case OP_Wf:			/* write final */
			Return 7;
		Case OP_Fz:			/* freeze finals */
			Return 8;
		Case OP_Cp:			/* computation */
			Return 9;
	End;
End;

/******************************************************************************
 * notRedundant
 * Returns True if j is not redundant in terms of synchronization effects.
 * Should involve global analysis. Currently manually configured.
 ******************************************************************************/
Function notRedundant(j: Ins_t):Boolean;
Begin
	Return !CFG_REDUNDANT_LOCK;
End;

/******************************************************************************
 * ready
 * Returns True if i is ready to be issued from the local LIB.
 ******************************************************************************/
Function ready(i: Ins_t):Boolean;
Begin
Alias
	t: Thread[i.thread];
	LIB: t.LIB;
Do
	Return 
	(
		!(Exists j: Label_t Do
			inBound(j, t.len)
			&
			notComplete(LIB[j])
			&
			LIB[j].pc < i.pc		/* out of "program order" */
			&
			(
				localDependent(i, LIB[j])
				|
				BYPASS[op2id(LIB[j].op)][op2id(i.op)] = ORDER_no 
				| 
				(BYPASS[op2id(LIB[j].op)][op2id(i.op)] = ORDER_diffVar & sameVar(LIB[j].v, i.v))
				|
				(BYPASS[op2id(LIB[j].op)][op2id(i.op)] = ORDER_redundantLock & notRedundant(LIB[j]))
			)
		End) 
	);
End;
End; /* ready */

/******************************************************************************
 * appendGIB(w)
 * Append local instruction w to GIB, increment GIB.len.
 ******************************************************************************/
Procedure appendGIB(w: Ins_t);
Begin
	Assert(GIB.len < GIB_ENT_NUM)
		"appendGIB: GIB buffer overflow!";

	GIB.arr[GIB.len].thread := w.thread;
	GIB.arr[GIB.len].pc := w.pc;
	GIB.arr[GIB.len].op := w.op;
	GIB.arr[GIB.len].v := w.v;
	GIB.arr[GIB.len].data := w.data;
	GIB.arr[GIB.len].lock := w.lock;
	GIB.arr[GIB.len].time := GIB.len;

	GIB.arr[GIB.len].useNew := False;

	GIB.len := GIB.len + 1;
End;

/******************************************************************************
 * appendDftGIB(w)
 * Append default write of v to GIB, increment GIB.len.
 ******************************************************************************/
Procedure addDefault(v: Var_t; data: Value_t);
Begin
	Assert(GIB.len < GIB_ENT_NUM)
		"appendGIB: GIB buffer overflow!";

	Switch VarType[v]
		Case VAR_NORMAL:
			GIB.arr[GIB.len].op := OP_Wn;
		Case VAR_VOLATILE:
			GIB.arr[GIB.len].op := OP_Wv;
		Case VAR_FINAL:
			GIB.arr[GIB.len].op := OP_Wf;
	End;

	GIB.arr[GIB.len].thread := Tinit;
	GIB.arr[GIB.len].pc := ZERO;
	GIB.arr[GIB.len].v := v;
	GIB.arr[GIB.len].data := data;
	GIB.arr[GIB.len].lock := DontCare;
	GIB.arr[GIB.len].time := GIB.len;

	GIB.len := GIB.len + 1;
End;

/******************************************************************************
 * add()
 * Add an instruction to the LIB. Increment the current len of that thread.
 * If InsType_t is INS_L or INS_U, parameter v is used for the lock field.
 ******************************************************************************/
Procedure add(	t: ThreadId_t; ins: InsType_t; 
				v: Var_t; data: Value_t; 
				local:Local_t; useLocal: Boolean);
Begin
	Alias
		thread: Thread[t];
		len: thread.len;
		w: thread.LIB[len];
	Do
		Assert(len < LABEL_NUM)
			"add: LIB buffer overflow!";

		Switch ins
			Case INS_R:
				Switch VarType[v]
					Case VAR_NORMAL:
						w.op := OP_Rn;
					Case VAR_VOLATILE:
						w.op := OP_Rv;
					Case VAR_FINAL:
						w.op := OP_Rf;
				End;

			Case INS_W:
				Switch VarType[v]
					Case VAR_NORMAL:
						w.op := OP_Wn;
					Case VAR_VOLATILE:
						w.op := OP_Wv;
					Case VAR_FINAL:
						w.op := OP_Wf;
				End;

			Case INS_L:
				w.op := OP_Lk;
				w.lock := v;

			Case INS_U:
				w.op := OP_Un;
				w.lock := v;

			Case INS_F:
				w.op := OP_Fz;

			Case INS_C:
				w.op := OP_Cp;

		End; /* Switch */

		w.thread := t;
		w.pc := len;
		w.v := v;
		w.data := data;
		w.local := local;
		w.useLocal := useLocal;
		w.done := False;

		len := len + 1;
	End;
End;

/******************************************************************************
 * compute
 *
 * Perform computation on local variables, currently hardcoded per test.
 ******************************************************************************/
Procedure compute(w: Ins_t);
Begin
		Thread[w.thread].LV[w.local].data := Thread[w.thread].LV[w.local].data + 1;
End;

/******************************************************************************
 * AllDone(): Boolean
 ******************************************************************************/
Function AllDone(): Boolean;
Begin
	Return
		(Forall t: ThreadId_t Do
			Forall i: Label_t Do
				inBound(i,Thread[t].len) 
				-> Thread[t].LIB[i].done
			End
		End)
End;

/******************************************************************************
 * initOrder() - MM dependent
 *
 * Set up the thread local reordering rules for each MM.
 ******************************************************************************/
Procedure initOrder();
Begin
	Switch MyMemModel
		Case JMM_MP:

			/*	
			 *	BYPASS (JMM_MP) relaxed
			 *
			 *		Rn	Wn	Lk	Un	Rv	Wv	Rf	Wf	Fz	Cp
			 *	Rn	n	yes	n	n	n	n	n	n	n	n
			 *	Wn	n	yes	n	n	n	n	n	n	n	n
			 *
			 *	Lk	n	rL	n	n	n	n	n	n	n	n
			 *	Un	n	yes	n	n	n	n	n	n	n	n
			 *
			 *	Rv	n	rL	n	n	n	n	n	n	n	n
			 *	Wv	n	yes	n	n	n	n	n	n	n	n
			 *
			 *	Rf	n	yes	n	n	n	n	n	n	n	n
			 *	Wf	n	yes	n	n	n	n	n	n	n	n
			 *
			 *	Fz	n	n	n	n	n	n	n	n	n	n
			 *
			 *	Cp	n	n	n	n	n	n	n	n	n	n
			 */

			/* After init, default value is ORDER_no */
			BYPASS[op2id(OP_Rn)][op2id(OP_Wn)] := ORDER_yes;
			BYPASS[op2id(OP_Wn)][op2id(OP_Wn)] := ORDER_yes;

			BYPASS[op2id(OP_Lk)][op2id(OP_Wn)] := ORDER_redundantLock;
			BYPASS[op2id(OP_Un)][op2id(OP_Wn)] := ORDER_yes ;

			BYPASS[op2id(OP_Rv)][op2id(OP_Wn)] := ORDER_redundantLock ;
			BYPASS[op2id(OP_Wv)][op2id(OP_Wn)] := ORDER_yes ;

			BYPASS[op2id(OP_Rf)][op2id(OP_Wn)] := ORDER_yes ;
			BYPASS[op2id(OP_Wf)][op2id(OP_Wn)] := ORDER_yes ;

			/*	
			 *	BYPASS (JMM_MP) relaxed
			 *
			 *		Rn	Wn	Lk	Un	Rv	Wv	Rf	Wf	Fz	
			 *	Rn	y	d	y	n	y	n	n	n	n
			 *	Wn	d	y	y	n	y	n	n	n	n
			 *
			 *	Lk	n	rL	n	n	n	n	n	n	n
			 *	Un	y	y	n	n	n	n	n	n	n
			 *
			 *	Rv	n	rL	n	n	n	n	n	n	n
			 *	Wv	y	y	n	n	n	n	n	n	n
			 *
			 *	Rf	n	y	n	n	n	n	n	n	n
			 *	Wf	n	y	n	n	n	n	n	n	n
			 *
			 *	Fz	n	n	n	n	n	n	n	n	n
			 */
	End; /* Switch */
End; /* initOrder */


/******************************************************************************
 *
 * Rules for possible actions.
 *
 ******************************************************************************/

/******************************************************************************
 * Event: readNormal
 ******************************************************************************/
Ruleset t:ThreadId_t Do		/* for any thread */
Ruleset i:Label_t Do		/* for any read instruction in LIB */
Ruleset k: GibEnt_t Do		/* for any previous write on the same var in GIB */
Alias 
	thread: Thread[t];
	r: thread.LIB[i];
	LV: thread.LV;
		
	w: GIB.arr[k];
Do
	Rule "Read Normal"
		inBound(i, thread.len)	
		&
		notComplete(r)				
		&
		ready(r) 
		&
		(r.op = OP_Rn)	/* ReadNormal */	
			
		& /* Ok, we found the eligible r */

		k < GIB.len
		& 
		legalNormalWrite(r, w)
	==>
	Begin
		LV[r.local].data := w.data;
		LV[r.local].valid := True;

		r.done := True;		
	End; 
End; /* Alias */
End; /* Ruleset k */	
End; /* Ruleset i */
End; /* Ruleset t */

/******************************************************************************
 * Event: writeNormal
 ******************************************************************************/
Ruleset t:ThreadId_t Do		
Ruleset i:Label_t Do		
Alias 
	w: Thread[t].LIB[i];
	LV: Thread[t].LV;
Do
	Rule "writeNormal"
		inBound(i, Thread[t].len)
		&
		notComplete(w)
		&
		ready(w) 
		&
		w.op = OP_Wn		/* WriteNormal */
	==>
	Begin
		Assert(w.useLocal -> LV[w.local].valid) "Rule writeNormal enter";

		If (w.useLocal) Then
			w.data := LV[w.local].data;
		End;

		appendGIB(w);

		w.done := True;		
	End;
End; /* Alias */
End; /* Ruleset i */
End; /* Ruleset t */

/******************************************************************************
 * Event: lock
 ******************************************************************************/
Ruleset t:ThreadId_t Do		
Ruleset i:Label_t Do		
Alias 
	w: Thread[t].LIB[i];
	lock: w.lock;
Do
	Rule "lock"
		inBound(i, Thread[t].len)
		&
		notComplete(w)
		&
		ready(w) 
		&
		w.op = OP_Lk 	/* Lock */
		&
		(LOCK[lock].count = 0 | LOCK[lock].owner = t)
	==>
	Begin
		Assert(LOCK[lock].count < LOCK_CNT_NUM)
			"lock: lock count overflow.";

		LOCK[lock].count := LOCK[lock].count + 1;
		LOCK[lock].owner := t;

		appendGIB(w);

		w.done := True;		
	End;
End; /* Alias */
End; /* Ruleset i */
End; /* Ruleset t */

/******************************************************************************
 * Event: unlock
 ******************************************************************************/
Ruleset t:ThreadId_t Do		
Ruleset i:Label_t Do		
Alias 
	w: Thread[t].LIB[i];
	lock: w.lock;
Do
	Rule "unlock"
		inBound(i, Thread[t].len)
		&
		notComplete(w)
		&
		ready(w) 
		&
		w.op = OP_Un	/* Unlock */
		&
		(LOCK[lock].count > 0 & LOCK[lock].owner = t)
	==>
	Begin
		LOCK[lock].count := LOCK[lock].count - 1;

		appendGIB(w);

		w.done := True;		
	End;
End; /* Alias */
End; /* Ruleset i */
End; /* Ruleset t */

/******************************************************************************
 * Event: readVolatile
 ******************************************************************************/
Ruleset t:ThreadId_t Do		
Ruleset i:Label_t Do		
Ruleset k:GibEnt_t Do
Alias 
	r: Thread[t].LIB[i];
	LV: Thread[t].LV;
	w: GIB.arr[k];
Do
	Rule "readVolatile"
		inBound(i, Thread[t].len)
		&
		notComplete(r)
		&
		ready(r) 
		&
		(r.op = OP_Rv)		/* ReadVolatile */
		&
		k < GIB.len
		&
		legalVolatileWrite(r, w) /* (legalNewWrite(r, w) | legalOldWrite(r, w)) */
	==>
	Begin
		LV[r.local].data := w.data;
		LV[r.local].valid := True;

		appendGIB(r);

/*
		If(legalNewWrite(r, w)) Then
			GIB.arr[GIB.len - 1].useNew := True;
		End;
*/

		r.done := True;		
	End;
End; /* Alias */
End; /* Ruleset k */
End; /* Ruleset i */
End; /* Ruleset t */

/******************************************************************************
 * Event: writeVolatile
 ******************************************************************************/
Ruleset t:ThreadId_t Do		
Ruleset i:Label_t Do		
Alias 
	w: Thread[t].LIB[i];
	LV: Thread[t].LV;
Do
	Rule "writeVolatile"
		inBound(i, Thread[t].len)
		&
		notComplete(w)
		&
		ready(w) 
		&
		(w.op = OP_Wv)		/* WriteVolatile */
	==>
	Begin
		Assert(w.useLocal ->  LV[w.local].valid) "Rule writeVolatile enter";

		If (w.useLocal = True) Then
			w.data := LV[w.local].data;
		End;

		appendGIB(w);

		w.done := True;		
	End;
End; /* Alias */
End; /* Ruleset i */
End; /* Ruleset t */

/******************************************************************************
 * Event: readFinal
 ******************************************************************************/
Ruleset t:ThreadId_t Do		
Ruleset i:Label_t Do		
Ruleset k:GibEnt_t Do
Alias 
	r: Thread[t].LIB[i];
	v: r.v;
	local: r.local;
	LV: Thread[t].LV;
	w: GIB.arr[k];
Do
	Rule "readFinal"
		inBound(i, Thread[t].len)
		&
		notComplete(r)
		&
		ready(r) 
		&
		(r.op = OP_Rf)		/* ReadFinal */
		&
		k < GIB.len
		&
		legalFinalWrite(r, w)
	==>
	Begin
		LV[local].data := w.data;
		LV[local].valid := True;

		r.done := True;		
	End;
End; /* Alias */
End; /* Ruleset k */
End; /* Ruleset i */
End; /* Ruleset t */

/******************************************************************************
 * Event: writeFinal
 ******************************************************************************/
Ruleset t:ThreadId_t Do		
Ruleset i:Label_t Do		
Alias 
	w: Thread[t].LIB[i];
	v: w.v;
	local: w.local;
	LV: Thread[t].LV;
Do
	Rule "writeFinal"
		inBound(i, Thread[t].len)
		&
		notComplete(w)
		&
		ready(w) 
		&
		w.op = OP_Wf		/* WriteFinal */
	==>
	Begin
		Assert(w.useLocal -> LV[local].valid) "Rule WriteFinal";

		If (w.useLocal) Then
			w.data := LV[local].data;
		End;

		appendGIB(w);		
		w.done := True;		
	End;
End; /* Alias */
End; /* Ruleset i */
End; /* Ruleset t */

/******************************************************************************
 * Event: freeze
 ******************************************************************************/
Ruleset t:ThreadId_t Do		
Ruleset i:Label_t Do		
Alias 
	w: Thread[t].LIB[i];
Do
	Rule "freeze"
		inBound(i, Thread[t].len)
		&
		notComplete(w)
		&
		ready(w) 
		&
		w.op = OP_Fz 		/* Freeze */
	==>
	Begin	
		appendGIB(w);
		w.done := True;		
	End;
End; /* Alias */
End; /* Ruleset i */
End; /* Ruleset t */

/******************************************************************************
 * Event: Computation
 ******************************************************************************/
Ruleset t:ThreadId_t Do		
Ruleset i:Label_t Do		
Alias 
	w: Thread[t].LIB[i];
Do
	Rule "computation"
		inBound(i, Thread[t].len)
		&
		notComplete(w)
		&
		ready(w) 
		&
		w.op = OP_Cp 		/* Computation */
	==>
	Begin	
		compute(w);
		--Put "local:"; --Put Thread[w.thread].LV[w.local].data;
		--Put("\n");
		w.done := True;		
	End;
End; /* Alias */
End; /* Ruleset i */
End; /* Ruleset t */


/******************************************************************************
 * 
 * Test Section
 *
 * The above specification completes implementation of the Abstract Memory Model. 
 * The following test cases will be used to run against the memory model. 
 * Configuration Parameters at the top of the file need to be modified
 * for each test case.
 *  
 * Convention for the tests: 
 * - All variables are assumed to be 0 initially. 
 * - A, B, C, ... are shared varialbes
 * - r1, r2, r3 ... or X, Y, Z ... are local variables.
 *
 ******************************************************************************/

/******************************************************************************
 * Startstate
 ******************************************************************************/
Startstate
Begin
	Clear Thread;
	Clear GIB;
	Clear LOCK;
	Clear VarType;
	Clear BYPASS;

	/* set up BYPASS table for MyMemModel */
	initOrder();

	/* 
	 * 1) setup var type, normal is default, e.g., VarType[A] := VAR_FINAL;
	 * 2) setup default values in GIB using addDefault(A, ZERO);
	 * 3) set up LIB for threads using add(t,ins,v,data,local,useLocal);
	 */

	If(MyTest = TEST_WR) Then						
		/********************************************************************
		 * WR relaxation
		 *-------------------------------------------------------------------
		 * A = 1						B = 1
		 * X = B						Y = A
		 * Finally, X = Y = 0?
		 *-------------------------------------------------------------------
		 * T1:							T2:
		 * W(A, ONE)					W(B, ONE)
		 * R(r1, B)						R(r1, B)	
		 *-------------------------------------------------------------------
		 * Result:
		 * without aliasing, all combinations are possible: 
		 * (0,0), (0,1), (1,0), (1,1).
		 * If aliased: only (1, 1).
		 * For volatile_SC: 01, 10, 11
		 ********************************************************************/
		-- VarType[A] := VAR_VOLATILE;
		-- VarType[B] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_R, B, DontCare, r1, False);

		add(T2, INS_W, B, ONE, DontCare, False);
		add(T2, INS_R, A, DontCare, r1, False);

	Elsif(MyTest = TEST_SC) Then
		/********************************************************************
		 * SC test
		 *-------------------------------------------------------------------
		 * Initially A = B = 2
		 *
		 * T1:							T2:
		 * A = 0;						B = 0;
		 * A = 1;						B = 1;
		 * X = B;						Y = A;
		 *
		 * Finally, exists X = Y = 0?
		 *-------------------------------------------------------------------
		 * Result: 
		 * For normal vars, (X, Y) can be 00, 01, 02, 10, 11, 12, 20, 21, 22
		 * If aliased: 00, 01, 10, 11
		 * For volatiles_NA (non-atomic), 01, 10, 11, 12, 21. can't have 22.
		 * For volatile_SC: 01, 10, 11, 12, 21
		 ********************************************************************/
		-- VarType[A] := VAR_VOLATILE;
		-- VarType[B] := VAR_VOLATILE;

		addDefault(A, TWO);
		addDefault(B, TWO);

		add(T1, INS_W, A, ZERO, DontCare, False);
		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_R, B, DontCare, r1, False);

		add(T2, INS_W, B, ZERO, DontCare, False);
		add(T2, INS_W, B, ONE, DontCare, False);
		add(T2, INS_R, A, DontCare, r1, False);

	Elsif(MyTest = TEST_PC) Then
		/********************************************************************
		 * PC test
		 *-------------------------------------------------------------------
		 * Initially A = B = 2
		 *
		 * T1:							T2:						T3:
		 * A = 0;						X = B;					Y = A;
		 * B = 0;						A = 1;					Z = A;
		 * 
		 *
		 * Finally, exists XYZ = 010?
		 *-------------------------------------------------------------------
		 * Result: 
		 * For normal vars, (X, Y) can be 
		 * 000, 001, 002, 010, 011, 012, 020, 021, 022, 
		 * 200, 201, 202, 210, 211, 212, 220, 221, 222
		 * For volatiles: can't have 010
		 * For volatile_SC: 000, 001, 011, 020, 021, 200, 201, 210, 220, 221, 222
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;
		VarType[B] := VAR_VOLATILE;

		addDefault(A, TWO);
		addDefault(B, TWO);

		add(T1, INS_W, A, ZERO, DontCare, False);
		add(T1, INS_W, B, ZERO, DontCare, False);

		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_W, A, ONE, DontCare, False);

		add(T3, INS_R, A, DontCare, r1, False);
		add(T3, INS_R, A, DontCare, r2, False);

	Elsif(MyTest = TEST_PrescientStore) Then
		/********************************************************************
		 * Presicent Store Test
		 *-------------------------------------------------------------------
		 * T1:							T2:
		 * X = A;						Y = B;
		 * B = 1;						A = 1;
		 *
		 * Finally, exists X = Y = 1?
		 *-------------------------------------------------------------------
		 * Result: (X, Y) can be 00, 01, 10, 11
		 * When aliased: 00, 01, 10, 11
		 * volatile_SC: 00, 01, 10.
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;
		VarType[B] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_R, A, DontCare, r1, False);
		add(T1, INS_W, B, ONE, DontCare, False);

		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_W, A, ONE, DontCare, False);

	Elsif(MyTest = TEST_PrescientStore2) Then
		/********************************************************************
		 * Presicent Store Test
		 *-------------------------------------------------------------------
		 * T1:							T2:
		 * X = A;						Y = B;
		 * B = 1;						A = Y;
		 * can X = 1?
		 *-------------------------------------------------------------------
		 * Result: 00, 01, 11
		 * Aliased: 00, 01, 11
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_R, A, DontCare, r1, False);
		add(T1, INS_W, B, ONE, DontCare, False);

		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_W, A, DontCare, r1, True);

	Elsif (MyTest = TEST_WriteAtomicity) Then					
		/********************************************************************
		 * Not Coherence; Write atomicity.
		 *-------------------------------------------------------------------
		 * T1:							T2:
		 * A = 1;						A = 2;
		 * X = A;						Y = A;
		 * Finally, exists X = 2 & Y = 1?
		 *-------------------------------------------------------------------
		 * It can happen: 11, 12, 21, 22
		 * Aliased: 11, 12, 21, 22
		 * Volatile_SC: 11, 12, 22
		 * Different from CRF!
		 * CRF Result: can't have 21.
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;

		addDefault(A, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_R, A, DontCare, r1, False);

		add(T2, INS_W, A, TWO, DontCare, False);
		add(T2, INS_R, A, DontCare, r1, False);

	Elsif (MyTest = TEST_Coherence2) Then					
		/********************************************************************
		 * Not Coherence
		 *-------------------------------------------------------------------
		 * T1:							T2:
		 * A = 1;						r1 = A;
		 * A = 2;						r2 = A;
		 * Finally, exists r1 = 2 & r2 = 1?
		 *-------------------------------------------------------------------
		 * Result: 
		 * If A is normal, all combinations are possible.
		 * But if A is volatile: 00,01,02,11,12,22
		 ********************************************************************/
		-- VarType[A] := VAR_VOLATILE;

		addDefault(A, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, A, TWO, DontCare, False);

		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);

	Elsif (MyTest = TEST_PRAM) Then					
		/********************************************************************
		 * Not PRAM
		 *-------------------------------------------------------------------
		 * T1:							T2:
		 * A = 1;						r1 = B;
		 * B = 1;						r2 = A;
		 * Finally, exists r1 = 1 & r2 = 0?
		 *-------------------------------------------------------------------
		 * Result: 00, 01, 10, 11.
		 * Aliased: 00, 01, 10, 11.
		 * Volatile_SC: 00, 01, 11.
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;
		VarType[B] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, B, ONE, DontCare, False);

		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);

	Elsif (MyTest = TEST_PRAM2) Then					
		/********************************************************************
		 * Not PRAM
		 *-------------------------------------------------------------------
		 * Initially, A = B = 3;
		 *
		 * T1:							T2:
		 * A = 0;						X = B;
		 * A = 1;						Y = A;
		 * B = 2;
		 * Finally, exists X = 2 & Y = 0?
		 *-------------------------------------------------------------------
		 * Result: 
		 * For normals: 20, 21, 23, 30, 31, 33
		 * For volatiles: 21, 30, 31, 33
		 ********************************************************************/
		--VarType[A] := VAR_VOLATILE;
		--VarType[B] := VAR_VOLATILE;

		addDefault(A, THREE);
		addDefault(B, THREE);

		add(T1, INS_W, A, ZERO, DontCare, False);
		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, B, TWO, DontCare, False);

		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);

	Elsif (MyTest = TEST_RO) Then	
		/********************************************************************
		 * A(CMP, RO)
		 *-------------------------------------------------------------------
		 * A = 1						r1 = A
		 * A = 2						r2 = A
		 *								r3 = A
		 * Finally, r1 = r3 = 1 and r2 = 2?
		 *-------------------------------------------------------------------
		 * Result: all combinations are ok.
		 * Volatile_SC: 000, 001, 002, 011, 012, 022, 111, 112, 122, 222
		 *
		 * Different from CRF!
		 * CRF Result: can't have 121
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;

		addDefault(A, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, A, TWO, DontCare, False);

		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);
		add(T2, INS_R, A, DontCare, r3, False);

	Elsif (MyTest = TEST_WOS) Then	
		/********************************************************************
		 * obeys A(CMP, UPO, WOS) but not A(CMP, UPO, WO)
		 *-------------------------------------------------------------------
		 * A = 1						B = 1
		 * B = 2						A = 2
		 * X = B						Y = A
		 *								
		 * Finally, X = Y = 1?
		 *-------------------------------------------------------------------
		 * Result: 11, 12, 21, 22
		 * If aliased: 11, 12, 21, 22
		 * volatile_SC: 12, 21, 22
		 *
		 * CRF Result: 11 is ok
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;
		VarType[B] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, B, TWO, DontCare, False);
		add(T1, INS_R, B, DontCare, r1, False);

		add(T2, INS_W, B, ONE, DontCare, False);
		add(T2, INS_W, A, TWO, DontCare, False);
		add(T2, INS_R, A, DontCare, r1, False);

	Elsif (MyTest = TEST_Alpha1) Then	
		/********************************************************************
		 * Reads - not possible under Alpha
		 *-------------------------------------------------------------------
		 * A = 1						r1 = A
		 * 								r2 = A
		 * Finally, r1 = 1 & r2 = 0?
		 *-------------------------------------------------------------------
		 * Failed. All combinations are possible: 00, 01, 10, 11
		 * volatile_SC: 00, 01, 11.
		 *
		 * Different from CRF!
		 * CRF Result: 10 is not allowed.
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;

		addDefault(A, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);

		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);

	Elsif (MyTest = TEST_Alpha2) Then	
		/********************************************************************
		 * Reads - not possible under Alpha
		 *-------------------------------------------------------------------
		 * A = 1						A = 2
		 *								r1 = A
		 * 								r2 = A
		 * Finally, r1 = 1 & r2 = 2?
		 *-------------------------------------------------------------------
		 * Failed. 
		 * (r1, r2) can be: 11, 12, 21, 22
		 * Volatile_SC: 11, 21, 22
		 *
		 * Different from CRF!
		 * CRF Result: can't have 12
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;

		addDefault(A, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);

		add(T2, INS_W, A, TWO, DontCare, False);
		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);

	Elsif (MyTest = TEST_Alpha3) Then	
		/********************************************************************
		 * Reads - not possible under Alpha
		 *-------------------------------------------------------------------
		 * A = 1						A = 2							Y = A
		 * X = A														Z = A
		 * Finally, X = 2 & Y = 2 & Z = 1?
		 *-------------------------------------------------------------------
		 * Result: X can't be 0. All other 18 combinations are possible.
		 *
		 * Different from CRF!
		 * CRF Result: can't have 221.
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;

		addDefault(A, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_R, A, DontCare, r1, False);

		add(T2, INS_W, A, TWO, DontCare, False);

		add(T3, INS_R, A, DontCare, r1, False);
		add(T3, INS_R, A, DontCare, r2, False);

	Elsif (MyTest = TEST_Alpha4) Then	
		/********************************************************************
		 * possible under Alpha
		 *-------------------------------------------------------------------
		 * A = 1						r1 = B
		 * B = 1						r2 = A
		 * Finally, r1 = 1 & r2 = 0?
		 *-------------------------------------------------------------------
		 * Result: 00, 01, 10, 11
		 * Failed even under aliasing.
		 *
		 * Different from CRF!
		 * CRF Result:
		 * Violation if no aliasing.
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, B, ONE, DontCare, False);

		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);
	
	Elsif (MyTest = TEST_Alpha5) Then	
		/********************************************************************
		 * Not possible under Alpha
		 *-------------------------------------------------------------------
		 * A = 1						A = 2
		 * X = A						U = A
		 * Y = A						V = A
		 * Finally, X = 1 & Y = 2 & U = 2 & V = 1?
		 *-------------------------------------------------------------------
		 * Result: all combinations with 1 and 2 are ok.
		 * Volatile_SC: 1111, 1121, 1122, 1222, 2222
		 *
		 * Different from CRF!
		 * CRF Result: 1221 not allowed.
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;

		addDefault(A, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_R, A, DontCare, r1, False);
		add(T1, INS_R, A, DontCare, r2, False);

		add(T2, INS_W, A, TWO, DontCare, False);
		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);

	Elsif (MyTest = TEST_Causality) Then					
		/********************************************************************
		 * Causality test
		 *-------------------------------------------------------------------
		 * T1:							T2:							T3:
		 * A = 1;						X = A;						Y = B
		 *								B = 1;						Z = A
		 *
		 * Finally, exists X = 1 & Y = 1 & Z = 0 ?
		 *-------------------------------------------------------------------
		 * If A and B are normal: 000, 001, 010, 011, 100, 101, 110, 111
		 * If A and B are volatiles: 000, 001, 010, 011, 100, 101, 111
		 * Volatiles obey causality!
		 * If aliased and volatile: 000, 001, 011, 100, 101, 111
		 *
		 * CRF Result:
		 * It may happen. Even with aliasing. Since Reconcile A in T3 can go before WriteBack of T1.
		 * With aliasing: state size 228 bytes (up to 541439 states with 120MB); 
		 ********************************************************************/
		--VarType[A] := VAR_VOLATILE;
		--VarType[B] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);

		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_W, B, ONE, DontCare, False);

		add(T3, INS_R, B, DontCare, r1, False);
		add(T3, INS_R, A, DontCare, r2, False);

	Elsif (MyTest = TEST_Causality2) Then					
		/********************************************************************
		 * Causality test
		 *-------------------------------------------------------------------
		 * T1:							T2:							T3:
		 * X = A;						Y = B;						Z = C;
		 * B = 1;						C = 1;						A = 1;
		 *
		 * Finally, exists X = 1 & Y = 1 & Z = 1 ?
		 *-------------------------------------------------------------------
		 * Result: 
		 * If ABC are normal, all combinations are ok
		 * If ABC are volatile: 000, 001, 010, 011, 100, 101, 110 (everything except 111!)
		 * 
		 * CRF Result: 
		 * It may happen. Even with aliasing. Since Reconcile A in T3 can go before WriteBack of T1.
		 * With aliasing: state size 228 bytes (up to 541439 states with 120MB); 
		 * 31526 states; 105447 rules; 12.06 Sec.
		 ********************************************************************/
		--VarType[A] := VAR_VOLATILE;
		--VarType[B] := VAR_VOLATILE;
		--VarType[C] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);
		addDefault(C, ZERO);

		add(T1, INS_R, A, DontCare, r1, False);
		add(T1, INS_W, B, ONE, DontCare, False);

		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_W, C, ONE, DontCare, False);

		add(T3, INS_R, C, DontCare, r1, False);
		add(T3, INS_W, A, ONE, DontCare, False);

	Elsif (MyTest = TEST_EndCon1) Then	
		/********************************************************************
		 * Constructor Test (EndCon is before write of reference)
		 * Detects the pre-mature release of object reference during constructioin.
		 *-------------------------------------------------------------------
		 * Assume A is the reference to a "Point" object and B is the field p.x: 
		 * Initially: A = B = 0;
		 *
		 * T1:		// p = new Point(1);				T2:			// reader thread
		 * B = 1;	// p.x = 1;							r1 = A;		// y = p.x
		 * membar;										membar;
		 * A = 1;	// p = 1;							r2 = B;
		 *
		 * Invariant: never exists a combination such that r1 = 1, r2 = 0;
		 *-------------------------------------------------------------------
		 * Result: 
		 * 10 is allowed.
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_W, B, ONE, DontCare, False);
		add(T1, INS_W, A, ONE, DontCare, False);

		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_R, B, DontCare, r2, False);

		BYPASS[op2id(OP_Wn)][op2id(OP_Wn)] := ORDER_no ;
		BYPASS[op2id(OP_Rn)][op2id(OP_Rn)] := ORDER_no ;
		 
	Elsif (MyTest = TEST_VolatileCoherence) Then
		/********************************************************************
		 * TEST_VolatileCoherence
		 *-------------------------------------------------------------------
		 * Initially: A = B = 0;
		 *
		 * T1:							T2:							T3:
		 * A = 1;						r1 = A;						r1 = A;
		 * A = 2;						r2 = A;						r2 = A;
		 *
		 * Invariant: never exists a combination such that 
		 * r1_T2 = 1, r2_T2 = 2, r1_T3 = 2, r2_T3 = 1;
		 *-------------------------------------------------------------------
		 * Result:
		 * Not Possible.
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;

		addDefault(A, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, A, TWO, DontCare, False);

		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);

		add(T3, INS_R, A, DontCare, r1, False);
		add(T3, INS_R, A, DontCare, r2, False);

	Elsif (MyTest = TEST_VolatileWA2) Then
		/********************************************************************
		 * TEST_VolatileWA2
		 *-------------------------------------------------------------------
		 * Initially: A = B = 0;
		 *
		 * T1:							T2:							T3:
		 * A = 1;						r1 = A;						r1 = A;
		 * B = 1;						r2 = B;						r2 = B;
		 *
		 * Invariant: never exists a combination such that 
		 * r1_T2 = 0, r2_T2 = 1, r1_T3 = 1, r2_T3 = 0;
		 *-------------------------------------------------------------------
		 * SC: All combination: 0000, 0001, 0010, 0011, 0100, 0101, 0111, 0110, 
		 *			1000, 1001, 1010, 1011, 1100, 1101, 1110, 1111.
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;
		VarType[B] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, B, ONE, DontCare, False);

		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_R, B, DontCare, r2, False);

		add(T3, INS_R, A, DontCare, r1, False);
		add(T3, INS_R, B, DontCare, r2, False);

	Elsif (MyTest = TEST_VolatileFlag) Then
		/********************************************************************
		 * TEST_VolatileFlag
		 *-------------------------------------------------------------------
		 * Initially: A = B = C = 0
		 *
		 * T1:							T2:	
		 * A = 1;						r2 = B;
		 * B = 1;						r3 = C;						
		 * C = 1;						r1 = A;					
		 *
		 * Invariant: never exists a combination such that 
		 * r1 = 1, r2 = 0, r3 = 1.
		 *-------------------------------------------------------------------
		 * Result: 000, 100, 101, 110, 111.
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_VOLATILE;
		VarType[C] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);
		addDefault(C, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, B, ONE, DontCare, False);
		add(T1, INS_W, C, ONE, DontCare, False);

		add(T2, INS_R, B, DontCare, r2, False);
		add(T2, INS_R, C, DontCare, r3, False);
		add(T2, INS_R, A, DontCare, r1, False);

	Elsif (MyTest = TEST_VolatileWA3) Then
		/********************************************************************
		 * TEST_VolatileWA3
		 *-------------------------------------------------------------------
		 * Initially: A = B = 0;
		 *
		 * T1:				T2:				T3:				T4:
		 * A = 1;			r1 = B;			B = 1;			r1 = A;
		 *					r2 = A;							r2 = B;
		 *
		 * Invariant: never exists a combination such that 
		 * r1_T2 = 1, r2_T2 = 0, r1_T3 = 1, r2_T3 = 0;
		 *-------------------------------------------------------------------
		 * Result:
		 * SC: no 1110, 1010
		 * NA: All combinations are Possible.
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;
		VarType[B] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);

		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);

		add(T3, INS_W, B, ONE, DontCare, False);

		add(T4, INS_R, A, DontCare, r1, False);
		add(T4, INS_R, B, DontCare, r2, False);

	Elsif (MyTest = TEST_VolatileSync) Then
		/********************************************************************
		 * TEST_VolatileSync
		 *-------------------------------------------------------------------
		 * Initially: A = B = C = 0; B and C are volatiles
		 *
		 * T1:				T2:				T3:				
		 * A = 1;			A = 2;			r1 = B;			
		 * B = 1;			C = 1;			r2 = C;
		 *									r3 = A;	
		 *
		 * If r1 or r2 is not zero, r3 should not be zero.
		 *-------------------------------------------------------------------
		 * Result: no violation
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_VOLATILE;
		VarType[C] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);
		addDefault(C, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, B, ONE, DontCare, False);

		add(T2, INS_W, A, TWO, DontCare, False);
		add(T2, INS_W, C, ONE, DontCare, False);

		add(T3, INS_R, B, DontCare, r1, False);
		add(T3, INS_R, C, DontCare, r2, False);
		add(T3, INS_R, A, DontCare, r3, False);

	Elsif (MyTest = TEST_Init) Then
		/********************************************************************
		 * TEST_Init
		 *-------------------------------------------------------------------
		 * Initially: A = B = 0; 
		 *
		 * T1:				T2:						
		 * Lock l1;			Lock l1,
		 * A = 1;			r1 = A;					
		 * B = 1;			r2 = B;			
		 * Unlock l1;		Unlock l1;					
		 *
		 * If r1=1 and r2=0? 
		 *-------------------------------------------------------------------
		 * Result: 00, 11
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_L, L1, DontCare, DontCare, False);
		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_W, B, ONE, DontCare, False);
		add(T1, INS_U, L1, DontCare, DontCare, False);

		add(T2, INS_L, L1, DontCare, DontCare, False);
		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_R, B, DontCare, r2, False);
		add(T2, INS_U, L1, DontCare, DontCare, False);

	Elsif (MyTest = TEST_Volatile) Then
		/********************************************************************
		 * TEST_Volatile
		 *-------------------------------------------------------------------
		 * Initially: A = B = C = D = 0;
		 *
		 * T1:				T2:				T3:			
		 * C = 1;			D = 1;			r3 = B;
		 * A = 1;			r2 = A;			r4 = A;
		 * r1 = B;			B = 1;			W = A;
		 * A = 0;			V = C;			X = D;
		 * U = D;
		 *
		 * can it have r1=r2=r3=0, r4=1, U=V=W=X=1?
		 *-------------------------------------------------------------------
		 ********************************************************************/
		VarType[A] := VAR_VOLATILE;
		VarType[B] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);
		addDefault(C, ZERO);
		addDefault(D, ZERO);

		add(T1, INS_W, C, ONE, DontCare, False);
		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_R, B, DontCare, r1, False);
		add(T1, INS_W, A, ZERO, DontCare, False);
		add(T1, INS_R, D, DontCare, r2, False);

		add(T2, INS_W, D, ONE, DontCare, False);
		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_W, B, ONE, DontCare, False);
		add(T2, INS_R, C, DontCare, r2, False);

		add(T3, INS_R, B, DontCare, r1, False);
		add(T3, INS_R, A, DontCare, r2, False);
		add(T3, INS_R, A, DontCare, r3, False);
		add(T3, INS_R, D, DontCare, r4, False);


	Elsif (MyTest = TEST_VolatileBarrier) Then
		/********************************************************************
		 * TEST_VolatileBarrier
		 *-------------------------------------------------------------------
		 * Initially: A = B = C = 0; C is volatile
		 *
		 * T1:				T2:						
		 * r1 = A;			r3 = B;			
		 * C = 1;			A = r3;		
		 * r2 = C;						
		 * B = 1;						
		 *
		 * can it have r1=1?
		 *-------------------------------------------------------------------
		 * Result: (r1, r2, r3) can be 010, 011 if CFG_REDUNDANT_LOCK = False
		 * 010, 011, 111 if CFG_REDUNDANT_LOCK = True.
		 ********************************************************************/
		VarType[C] := VAR_VOLATILE;

		addDefault(A, ZERO);
		addDefault(B, ZERO);
		addDefault(C, ZERO);

		add(T1, INS_R, A, DontCare, r1, False);
		add(T1, INS_W, C, ONE, DontCare, False);
		add(T1, INS_R, C, DontCare, r2, False);
		add(T1, INS_W, B, ONE, DontCare, False);

		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_W, A, DontCare, r1, True);


	Elsif (MyTest = TEST_Sync1) Then	
		/********************************************************************
		 * Lock L1;				Lock L2;
		 * A = 1;				B = 1;
		 * Unlock L1;			Unlock L2;			
		 *
		 * Lock L1;				Lock L2;
		 * x = B;				y = A;
		 * Unlock L1;			Unlock L2;
		 *-------------------------------------------------------------------
		 * Result:
		 * All combinations are possilbe 00, 01, 10, 11
		 *
		 * If L2 = L1: 01, 10, 11
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_L, L1, DontCare, DontCare, False);
		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_U, L1, DontCare, DontCare, False);
		add(T1, INS_L, L1, DontCare, DontCare, False);
		add(T1, INS_R, B, DontCare, r1, False);
		add(T1, INS_U, L1, DontCare, DontCare, False);

		add(T2, INS_L, L1, DontCare, DontCare, False);
		add(T2, INS_W, B, ONE, DontCare, False);
		add(T2, INS_U, L1, DontCare, DontCare, False);
		add(T2, INS_L, L1, DontCare, DontCare, False);
		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_U, L1, DontCare, DontCare, False);

	Elsif (MyTest = TEST_Sync2) Then	
		/********************************************************************
		 * Lock L1;				Lock L2;
		 * A = 1;				B = 1;
		 * x = B;				y = A;
		 * Unlock L1;			Unlock L2;
		 *-------------------------------------------------------------------
		 * Result:
		 * All combinations are possilbe 00, 01, 10, 11
		 *
		 * If L2 = L1, only 01, 10
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_L, L1, DontCare, DontCare, False);
		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_R, B, DontCare, r1, False);
		add(T1, INS_U, L1, DontCare, DontCare, False);

		add(T2, INS_L, L1, DontCare, DontCare, False);
		add(T2, INS_W, B, ONE, DontCare, False);
		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_U, L1, DontCare, DontCare, False);

	Elsif (MyTest = TEST_Sync3) Then	
		/********************************************************************
		 * Lock L1;				Lock L1;				Lock L2;
		 * B = 1;				X = B;					Y = A;
		 * Unlock L1;			Unlock L1;				Z = B;
		 *						Lock L2;				Unlock L2;
		 *						A = 1;
		 *						Unlock L2;
		 *
		 * Can X = 1, Y = 1, and Z = 0?
		 *-------------------------------------------------------------------
		 * Result: 000, 001, 010, 011, 100, 101, 111.
		 * Can't have 110.
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_L, L1, DontCare, DontCare, False);
		add(T1, INS_W, B, ONE, DontCare, False);
		add(T1, INS_U, L1, DontCare, DontCare, False);

		add(T2, INS_L, L1, DontCare, DontCare, False);
		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_U, L1, DontCare, DontCare, False);
		add(T2, INS_L, L2, DontCare, DontCare, False);
		add(T2, INS_W, A, ONE, DontCare, False);
		add(T2, INS_U, L2, DontCare, DontCare, False);

		add(T3, INS_L, L2, DontCare, DontCare, False);
		add(T3, INS_R, A, DontCare, r1, False);
		add(T3, INS_R, B, DontCare, r2, False);
		add(T3, INS_U, L2, DontCare, DontCare, False);

	Elsif (MyTest = TEST_Final) Then	
		/********************************************************************
		 * A is final
		 * A = 1;				Y = A;
		 * Freeze A;			
		 * X = A;				
		 *-------------------------------------------------------------------
		 * Result: 10, 11.
		 ********************************************************************/
		VarType[A] := VAR_FINAL;

		addDefault(A, ZERO);

		add(T1, INS_W, A, ONE, DontCare, False);
		add(T1, INS_F, A, DontCare, DontCare, False);
		add(T1, INS_R, A, DontCare, r1, False);

		add(T2, INS_R, A, DontCare, r1, False);

	Elsif (MyTest = TEST_Final2) Then	
		/********************************************************************
		 * A is reference, B is a final field
		 * B = 1;				x = A;
		 * Freeze B;			
		 * A = 1;				y = B;
		 * Can't have x = 1 and y = 0.
		 *-------------------------------------------------------------------
		 * Result: 00, 01, 11. can't have 10.
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_FINAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_W, B, ONE, DontCare, False);
		add(T1, INS_F, B, DontCare, DontCare, False);
		add(T1, INS_W, A, ONE, DontCare, False);

		add(T2, INS_R, A, DontCare, r1, False);
		add(T2, INS_R, B, DontCare, r2, False);

	Elsif (MyTest = TEST_CausalLoop1) Then	
		/********************************************************************
		 * X = A;				Y = B;
		 * B = X;				A = Y;
		 *-------------------------------------------------------------------
		 * Result: 00
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);

		add(T1, INS_R, A, DontCare, r1, False);
		add(T1, INS_W, B, DontCare, r1, True);

		add(T2, INS_R, B, DontCare, r1, False);
		add(T2, INS_W, A, DontCare, r1, True);

	Elsif (MyTest = TEST_CausalLoop2) Then	
		/********************************************************************
		 * A = 1;				X = C;					Z = B;
		 *						Y = A;					C = Z;
		 *						B = Y;
		 *-------------------------------------------------------------------
		 * Can X = 1?
		 * Result:	000, 010, 011 when Read->Read = no;
		 *			000, 010, 011, 111 when Read->Read = yes.
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;
		VarType[C] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);
		addDefault(C, ZERO);
			
		BYPASS[op2id(OP_Rn)][op2id(OP_Rn)] := ORDER_yes ;

		add(T1, INS_W, A, ONE, DontCare, False);

		add(T2, INS_R, C, DontCare, r1, False);
		add(T2, INS_R, A, DontCare, r2, False);
		add(T2, INS_W, B, DontCare, r2, True);

		add(T3, INS_R, B, DontCare, r1, False);
		add(T3, INS_W, C, DontCare, r1, True);

	Elsif (MyTest = TEST_CausalLoop3) Then	
		/********************************************************************
		 * C = 2;			X = C;				Y = A;			Z = B;
		 *					A = X;				B = Y;			A = Z;
		 *-------------------------------------------------------------------
		 * Result:	000, 200, 220, 222
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;
		VarType[C] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);
		addDefault(C, ZERO);
			
		add(T1, INS_W, C, TWO, DontCare, False);

		add(T2, INS_R, C, DontCare, r1, False);
		add(T2, INS_W, A, DontCare, r1, True);

		add(T3, INS_R, A, DontCare, r1, False);
		add(T3, INS_W, B, DontCare, r1, True);

		add(T4, INS_R, B, DontCare, r1, False);
		add(T4, INS_W, A, DontCare, r1, True);


	Elsif (MyTest = TEST_CausalLoop4) Then	
		/********************************************************************
		 * C = 2;			X = C;				Y = A;			Z = B;
		 *					A = X;				Y' = Y + 1;		Z' = Z + 1;
		 *										B = Y';			A = Z';
		 *-------------------------------------------------------------------
		 * Can X = 0, Y = 2, and Z = 3?
		 * Result:	000, 001, 010, 200, 201, 210, 220, 223 
		 ********************************************************************/
		VarType[A] := VAR_NORMAL;
		VarType[B] := VAR_NORMAL;
		VarType[C] := VAR_NORMAL;

		addDefault(A, ZERO);
		addDefault(B, ZERO);
		addDefault(C, ZERO);
			
		add(T1, INS_W, C, TWO, DontCare, False);

		add(T2, INS_R, C, DontCare, r1, False);
		add(T2, INS_W, A, DontCare, r1, True);

		add(T3, INS_R, A, DontCare, r1, False);
		add(T3, INS_C, DontCare, DontCare, r1, False);
		add(T3, INS_W, B, DontCare, r1, True);

		add(T4, INS_R, B, DontCare, r1, False);
		add(T4, INS_C, DontCare, DontCare, r1, False);
		add(T4, INS_W, A, DontCare, r1, True);


	End;
End;

/******************************************************************************
 * Use the rule of final state to output all possible final state results:
 ******************************************************************************/
Rule "Output final result"
	CFG_SHOW_ALL
	&
	AllDone()
==>
Begin
	If (MyTest = TEST_WR) Then
		Put " TEST_WR possible result:\n";
		Put " X:"; Put Thread[T1].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_Init) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_Sync3) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T3].LV[r1].data;
		Put " Z:"; Put Thread[T3].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_CausalLoop1) Then
		Put " X:"; Put Thread[T1].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_CausalLoop2) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r2].data;
		Put " Z:"; Put Thread[T3].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_CausalLoop3 | MyTest = TEST_CausalLoop4) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T3].LV[r1].data;
		Put " Z:"; Put Thread[T4].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_PrescientStore | MyTest = TEST_PrescientStore2) Then
		Put " X:"; Put Thread[T1].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_WriteAtomicity) Then
		Put " X:"; Put Thread[T1].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_SC) Then
		Put " X:"; Put Thread[T1].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_PC) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T3].LV[r1].data;
		Put " Z:"; Put Thread[T3].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_PRAM) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_PRAM2) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_RO) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r2].data;
		Put " Z:"; Put Thread[T2].LV[r3].data;
		Put "\n";
	Elsif (MyTest = TEST_WOS) Then
		Put " X:"; Put Thread[T1].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_Alpha1) Then
		Put " r1:"; Put Thread[T2].LV[r1].data;
		Put " r2:"; Put Thread[T2].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_Alpha2) Then
		Put " r1:"; Put Thread[T2].LV[r1].data;
		Put " r2:"; Put Thread[T2].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_Alpha3) Then
		Put " X:"; Put Thread[T1].LV[r1].data;
		Put " Y:"; Put Thread[T3].LV[r1].data;
		Put " Z:"; Put Thread[T3].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_Alpha4) Then
		Put " r1:"; Put Thread[T2].LV[r1].data;
		Put " r2:"; Put Thread[T2].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_Alpha5) Then
		Put " X:"; Put Thread[T1].LV[r1].data;
		Put " Y:"; Put Thread[T1].LV[r2].data;
		Put " U:"; Put Thread[T2].LV[r1].data;
		Put " V:"; Put Thread[T2].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_Coherence2) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_Causality) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T3].LV[r1].data;
		Put " Z:"; Put Thread[T3].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_Causality2) Then
		Put " X:"; Put Thread[T1].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r1].data;
		Put " Z:"; Put Thread[T3].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_EndCon1) Then
		-- Put " TEST_EndCon1 possible result:\n";
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_VolatileCoherence) Then
		Put " X:"; Put Thread[T2].LV[r1].data;
		Put " Y:"; Put Thread[T2].LV[r2].data;
		Put " X:"; Put Thread[T3].LV[r1].data;
		Put " Y:"; Put Thread[T3].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_VolatileBarrier) Then
		Put " r1:"; Put Thread[T1].LV[r1].data;
		Put " r2:"; Put Thread[T1].LV[r2].data;
		Put " r3:"; Put Thread[T2].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_VolatileWA2) Then
		Put " u:"; Put Thread[T2].LV[r1].data;
		Put " v:"; Put Thread[T2].LV[r2].data;
		Put " x:"; Put Thread[T3].LV[r1].data;
		Put " y:"; Put Thread[T3].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_VolatileWA3) Then
		-- Put " TEST_VolatileWA3 possible result:\n";
		Put " u:"; Put Thread[T2].LV[r1].data;
		Put " v:"; Put Thread[T2].LV[r2].data;
		Put " w:"; Put Thread[T4].LV[r1].data;
		Put " x:"; Put Thread[T4].LV[r2].data;
		Put "\n";
	Elsif (MyTest = TEST_VolatileFlag) Then
		Put " r1:"; Put Thread[T2].LV[r1].data;
		Put " r2:"; Put Thread[T2].LV[r2].data;
		Put " r3:"; Put Thread[T2].LV[r3].data;
		Put "\n";		
	Elsif (MyTest = TEST_VolatileSync) Then
		-- Put " TEST_VolatileWA3 possible result:\n";
		Put " r1:"; Put Thread[T3].LV[r1].data;
		Put " r2:"; Put Thread[T3].LV[r2].data;
		Put " r3:"; Put Thread[T3].LV[r3].data;
		Put " r4:"; Put Thread[T3].LV[r4].data;
		Put "\n";
	Elsif (MyTest = TEST_Sync1) Then
		Put " x:"; Put Thread[T1].LV[r1].data;
		Put " y:"; Put Thread[T2].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_Sync2) Then
		Put " x:"; Put Thread[T1].LV[r1].data;
		Put " y:"; Put Thread[T2].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_Final) Then
		Put " x:"; Put Thread[T1].LV[r1].data;
		Put " y:"; Put Thread[T2].LV[r1].data;
		Put "\n";
	Elsif (MyTest = TEST_Final2) Then
		Put " x:"; Put Thread[T2].LV[r1].data;
		Put " y:"; Put Thread[T2].LV[r2].data;
		Put "\n";

		
	End;
End;

/******************************************************************************
 * Test Invariants
 * Can use invariant to generate a trace leading to the result.
 ******************************************************************************/
Invariant "Invariant Test"
	(!CFG_SHOW_ALL & AllDone())
	-> 
	(MyTest = TEST_WR ->
	!(Thread[T1].LV[r1].data = ZERO & Thread[T2].LV[r1].data = ZERO))
	&
	(MyTest = TEST_PrescientStore ->
	!(Thread[T1].LV[r1].data = ONE & Thread[T2].LV[r1].data = ONE))
	&
	(MyTest = TEST_WriteAtomicity ->
	!(Thread[T1].LV[r1].data = TWO & Thread[T2].LV[r1].data = ONE))
	&
	(MyTest = TEST_SC ->
	!(Thread[T1].LV[r1].data = ZERO & Thread[T2].LV[r1].data = ZERO))
	&
	(MyTest = TEST_Coherence2 ->
	!(Thread[T2].LV[r1].data = TWO & Thread[T2].LV[r2].data = ONE))
	&
	(MyTest = TEST_PRAM ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T2].LV[r2].data = ZERO))
	&
	(MyTest = TEST_PRAM2 ->
	!(Thread[T2].LV[r1].data = TWO & Thread[T2].LV[r2].data = ZERO))
	&
	(MyTest = TEST_RO ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T2].LV[r2].data = TWO &
	  Thread[T2].LV[r3].data = ONE))
	&
	(MyTest = TEST_WOS ->
	!(Thread[T1].LV[r1].data = ONE & Thread[T2].LV[r1].data = ONE ))
	&
	(MyTest = TEST_Alpha1 ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T2].LV[r2].data = ZERO ))
	&
	(MyTest = TEST_Alpha2 ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T2].LV[r2].data = TWO ))
	&
	(MyTest = TEST_Alpha3 ->
	!(Thread[T1].LV[r1].data = TWO & Thread[T3].LV[r1].data = TWO  & 
	  Thread[T3].LV[r2].data = ONE ))
	&
	(MyTest = TEST_Alpha4 ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T2].LV[r2].data = ZERO ))
	&
	(MyTest = TEST_Alpha5 ->
	!(Thread[T1].LV[r1].data = ONE & Thread[T1].LV[r2].data = TWO &
	 Thread[T2].LV[r1].data = TWO & Thread[T2].LV[r2].data = ONE))
	&
	(MyTest = TEST_Causality ->
	!(Thread[T2].LV[r1].data = ONE &
		Thread[T3].LV[r1].data = ONE & Thread[T3].LV[r2].data = ZERO))
	&
	(MyTest = TEST_Causality2 ->
	!(Thread[T1].LV[r1].data = ONE & 
		Thread[T2].LV[r1].data = ONE &
		Thread[T3].LV[r1].data = ONE))
	&
	(MyTest = TEST_EndCon1 ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T2].LV[r2].data = ZERO))
	&
	(MyTest = TEST_VolatileCoherence ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T2].LV[r2].data = TWO &
		Thread[T3].LV[r1].data = TWO & Thread[T3].LV[r2].data = ONE))
	&
	(MyTest = TEST_VolatileWA2 ->
	!(Thread[T2].LV[r1].data = ZERO & Thread[T2].LV[r2].data = ONE &
		Thread[T3].LV[r1].data = ONE & Thread[T3].LV[r2].data = ZERO))
	&
	(MyTest = TEST_VolatileWA3 ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T2].LV[r2].data = ZERO &
		Thread[T4].LV[r1].data = ONE & Thread[T4].LV[r2].data = ZERO))
	&
	(MyTest = TEST_VolatileFlag ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T2].LV[r2].data = ZERO & Thread[T2].LV[r3].data = ONE))
	&
	(MyTest = TEST_VolatileSync ->
	!((Thread[T3].LV[r1].data = ONE | Thread[T3].LV[r2].data = ONE) & Thread[T3].LV[r3].data = ZERO))
	&
	(MyTest = TEST_Sync1 ->
	!(Thread[T1].LV[r1].data = ONE & Thread[T2].LV[r1].data = ONE))
	&
	(MyTest = TEST_Sync2 ->
	!(Thread[T1].LV[r1].data = ZERO & Thread[T2].LV[r1].data = ZERO))
	&
	(MyTest = TEST_Sync3 ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T3].LV[r1].data = ONE & Thread[T3].LV[r2].data = ZERO))
	&
	(MyTest = TEST_Volatile ->
	!(Thread[T1].LV[r1].data = ZERO & Thread[T1].LV[r2].data = ONE &
		Thread[T2].LV[r1].data = ZERO & Thread[T2].LV[r2].data = ONE &
		Thread[T3].LV[r1].data = ZERO & Thread[T3].LV[r2].data = ONE &
		Thread[T3].LV[r3].data = ONE & Thread[T3].LV[r4].data = ONE))
	&
	(MyTest = TEST_Final2 ->
	!(Thread[T2].LV[r1].data = ONE & Thread[T2].LV[r2].data = ZERO))

	;