/*
 * Copyright (c) 1996 by Satish Chandra, Brad Richards, Mark D. Hill, 
 * James R. Larus, and David A. Wood.
 *
 * Teapot is distributed under the following conditions:
 * 
 *     You may make copies of Teapot for your own use and modify those copies.
 * 
 *     All copies of Teapot must retain our names and copyright notice.
 * 
 *     You may not sell Teapot or distributed Teapot in conjunction with a
 *     commercial product or service without the expressed written consent of
 *     the copyright holders.
 * 
 * THIS SOFTWARE IS PROVIDED ``AS IS'' AND WITHOUT ANY EXPRESS OR IMPLIED
 * WARRANTIES, INCLUDING, WITHOUT LIMITATION, THE IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.
 * 
 */

---------------------- Constant definitions -----------------------------

Const
	NodeCount:  3;				-- number of nodes in the system
	AddrCount:  1;				-- # of addresses in the system
	ReorderMax: 1;				-- how much reordering allowed?

	ValueCount: 1;				-- maximum value of any variable
	-- ChanMax:	NodeCount+AddrCount;	-- enough?
	-- ChanMax:	NodeCount+AddrCount+1;
	ChanMax:	NodeCount+AddrCount+2;
	QueueMax:	ChanMax;		-- enough?
	#include "Generated/const.h"
	NULL: 0;

------------------------ Type definitions -------------------------------

Type

	NodeRangeType:	0..NodeCount-1;
	AddrRangeType:	0..AddrCount-1;
	
	NODE:			Scalarset (NodeCount); 
	-- NODE:			NodeRangeType;
	ID:			Scalarset (AddrCount);
	Value:			Scalarset (ValueCount);
	CTRTYPE:		0..(AddrCount*ChanMax+1);

	INTEGER:		0..NodeCount;

	BOOLEAN:		boolean;
	BitType:		boolean;


	MSG: 
		enum{
		    #include "Generated/msgs.h"
		};
	
	Message:
		Record
			MType: 	MSG;
			Addr:	ID;
			Value:	Value;
#ifdef RACEDET
			RdBit:	BitType;
			WrBit:	BitType;
#endif
		End;

	AccStateType: 
		enum {
			Blk_Invalid,
			Blk_ReadOnly,
			Blk_Writable
    		};

	AccessType: 
		enum {
			READ,
			WRITE
    		};

	STATE: 
		enum {
		    #include "Generated/states.h"
		};

        SHARER_LIST:
                Record
                        Sh  : Array [INTEGER] of NODE; -- this is one bigger, but to fool murph i types
                        Cnt : INTEGER;
                End;

        SHARER_LIST_ITOR:
                Record
                        Num : INTEGER;
                        Sh  : Array [INTEGER] of NODE;
                        Cur : INTEGER;
                End;

#ifdef UPDATE
        WRITER_LIST: Array [NODE] of BitType; 
#endif


	CONT : 0..ContMax;

	TAG_CHG:
		enum {
			TPPI_Blk_Invalidate,
			TPPI_Blk_Validate_RW,
			TPPI_Blk_Validate_RO,
			TPPI_Blk_Downgrade_RO,
			TPPI_Blk_Upgrade_RW,
			TPPI_Blk_No_Tag_Change
		};

	QueueElemType:
		Record
			Msg:	Message;
			Src:	NODE;
		End;

	QueueType:
		Record
			Count:	0..QueueMax;
			Elems:	Array [0..QueueMax-1] of QueueElemType;
		End;

	INFO:
		Record
			State:	STATE;
			Data:	Value;
			Bitvec:	SHARER_LIST;
			NumSharers: INTEGER;
			Owner:  NODE;
			ID0:	ID;
			CONT0:	CONT;
			NODE1:  NODE;
			Queue:	QueueType;
#ifdef RACEDET
			RdBit:  BitType;
			WrBit:  BitType;
			AuxRdBit:  BitType;
			AuxWrBit:  BitType;
#endif	
    	End;

	TNodeType: -- Typhoon, T-Zero, blah
		Record
			Blocked:	boolean;
			PPBlocked:	boolean;
			AccCtrl:	Array [ID] of AccStateType;
			Dram:		Array [ID] of INFO;
			MsgCtr:		CTRTYPE;
			AtBarrier:	BOOLEAN;
		End;

	NetSlotType:
		Record
			Count:	0..ChanMax;
			Messages: Array [0..ChanMax-1] of Message;
			Ages:    Array [0..ChanMax-1] of CTRTYPE;
		End;

	STRING: 		0..1; 
	
	FuncType: 		0..FuncMax;

	ContSlot:
		Record
			Func: FuncType;
			ID0: ID;
			NODE0: NODE;
			NODE1: NODE;
			CONT0: CONT;
			SHARER_LIST_ITOR0: SHARER_LIST_ITOR;
		End;

	ContPoolType:
		Record
			pos: 0..ContMax;
			slots: Array [0..ContMax-1] of ContSlot;
		End;

	HistoryType:
		Record
			writer:  NODE;				-- current
			writers: Array [NODE] of BOOLEAN;	-- past
			readers: Array [NODE] of BOOLEAN;
		End;

	RaceType: 
		enum {
			RW,	
			WR,
			WW,
			None
    		};

	RaceRec:
		Record
			race: 	  RaceType;
			procs:	  Array [0..1] of NODE;
			pending:  Array [0..1] of BOOLEAN;
		End;
	

-----------------------------------------------------------------------------
--                       Variable declarations
-----------------------------------------------------------------------------

Var

	old_idx: 0..ChanMax-1;

	Network: Array [NODE] of Array [NODE] of NetSlotType;
	
	Nodes: Array [NODE] of TNodeType;

	HomeMap: Array[ID] of NODE;

	ContPools: Array[NODE] of Array [ID] of ContPoolType;

	cur_node: NODE;
	
	cur_msg: Message;

	cur_id : ID;

	History: Array [ID] of HistoryType;

	ProtocolRace: 	Array [ID] of RaceType;

	PendingOp: 	Array [NODE] of AccessType;

	#include "Generated/conts.h"


-----------------------------------------------------------------------------
--                      Utilities
----------------------------------------------------------------------------

#include "Generated/trans.h"

Function Msg_To_Str(m: MSG):STRING;
Begin
	return 1;
End;

Procedure skip();
Begin
End;

#define TRACE_HANDLER(a,b,c,d)		skip()
#define TRACE_Q(a,b,c,d)			skip()
#define msg_ptr						cur_msg.MType
#define BlkAlign(va)		va

#include "bitvec.m"		
#include "nw.m"		
#include "transfer.m"	
#include "queue.m"		
#include "cont.m"
#include "info.m"
#include "race_support.m"

-- During the Resume, we must check that both Murfi and the protocol
-- agree as to the presence or absence of a data race.  

Procedure Thread_Resume(id:ID);
Begin
	Assert(id = cur_id);
	Nodes[cur_node].Blocked := false;
	CheckForRace(cur_id, cur_node);
End;

#include "Generated/hdlrs.m"	
#include "barrier.m"	
#include "queue2.m"	
#include "pp.m"			
#include "proc.m"		

-----------------------------------------------------------------------------
--                       Start state and Invariants
-----------------------------------------------------------------------------

Ruleset v: Value Do
Ruleset p: NODE  Do
	
	Startstate
	Begin
		For a : ID do
			HomeMap[a] := p;
			Undefine History[a].writer;
			For i : NODE Do
			    History[a].readers[i] := False;
			    History[a].writers[i] := False;
			Endfor;
			ProtocolRace[a] := None;
		Endfor;

		For n : NODE do
		
			cur_node := n;
			Undefine old_idx;
			Undefine cur_msg;

			Nodes[n].Blocked := false;
			Nodes[n].PPBlocked := false;
			Undefine Nodes[n].MsgCtr;
			-- Undefine Nodes[n].RaceIdx;
			Nodes[n].AtBarrier := false;
			Undefine PendingOp[n];
	
			For va : ID do
	
			    	cur_id := va;
				ContPools[n][va].pos := 0;
				Undefine ContPools[n][va].slots;
				InitConstConts();

				If (HomeMap[va] = n)
				Then
					Nodes[n].AccCtrl[va] := Blk_Invalid;
					Nodes[n].Dram[va].State:=Home_inv_None;
					Nodes[n].Dram[va].Data := v;

					BV_Clear(Nodes[n].Dram[va].Bitvec);
					Nodes[n].Dram[va].NumSharers := 0;

					Undefine Nodes[n].Dram[va].Owner;
					Undefine Nodes[n].Dram[va].ID0;
					Undefine Nodes[n].Dram[va].CONT0;
					Undefine Nodes[n].Dram[va].NODE1;
					Undefine Nodes[n].Dram[va].NODE1;
					Nodes[n].Dram[va].Queue.Count := 0;
					Undefine Nodes[n].Dram[va].Queue.Elems;
#ifdef RACEDET
					Nodes[n].Dram[va].RdBit := False;
					Nodes[n].Dram[va].WrBit := False;
					Nodes[n].Dram[va].AuxRdBit := False;
					Nodes[n].Dram[va].AuxWrBit := False;
#endif
				Else
					Nodes[n].AccCtrl[va] := Blk_Invalid;
					Nodes[n].Dram[va].State:=Cache_inv_INV;
					Undefine Nodes[n].Dram[va].Data;
					BV_Undefine(Nodes[n].Dram[va].Bitvec);
					Undefine Nodes[n].Dram[va].NumSharers;

					Undefine Nodes[n].Dram[va].Owner;
					Undefine Nodes[n].Dram[va].ID0;
					Undefine Nodes[n].Dram[va].CONT0;
					Undefine Nodes[n].Dram[va].NODE1;
					Nodes[n].Dram[va].Queue.Count := 0;
					Undefine Nodes[n].Dram[va].Queue.Elems;
#ifdef RACEDET
					Nodes[n].Dram[va].RdBit := False;
					Nodes[n].Dram[va].WrBit := False;
					Nodes[n].Dram[va].AuxRdBit := False;
					Nodes[n].Dram[va].AuxWrBit := False;
#endif
				Endif;
			Endfor; -- va
		Endfor; -- n

		For src : NODE do
			For dst : NODE do
				Network[src][dst].Count := 0;
				Undefine Network[src][dst].Ages;
				Undefine Network[src][dst].Messages;
			Endfor; --dst
		Endfor; --src

	End; -- startstate

End; -- ruleset p
End; -- ruleset v

-----------------------------------------------------------------------------
--                         Invariant rules
-----------------------------------------------------------------------------
#include "invariant.m"
