/*
 * 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.
 * 
 */

#line 1 "proc.m"
-----------------------------------------------------------------------------
--							Cause a read or write
-----------------------------------------------------------------------------


Ruleset v : Value Do	-- write a non-det. selected new value
Ruleset n : NODE Do	-- any node
Ruleset a : ID Do	-- any address

Alias 
    Acc : Nodes[n].AccCtrl[a];
    mem : Nodes[n].Dram[a];
Do

	Rule "Load a value"
		(!Nodes[n].Blocked) & 
		(!Nodes[n].PPBlocked) &
		(HomeMap[a] != n) &
		Space_in_Network(n) 
	==>
	Begin
		cur_node := n;
		Msg_setNoValue (RD_FAULT, a, cur_node, false, cur_msg);  -- should it need to enqueue
	    	cur_id := a;
		Switch (Acc)
		    Case Blk_Invalid:
			Nodes[n].Blocked := true;
                        Assert(!(Isundefined(cur_node))) "Undefined cur_node in RD_FAULT";
			DispatchState(mem.State, RD_FAULT, a, mem, 
				HomeMap[a]);
		Endswitch; -- switch
	End; -- rule


	Rule "Overwrite a value"
		(!Nodes[n].Blocked) & 
		(!Nodes[n].PPBlocked) &
		(HomeMap[a] != n) &
		Space_in_Network(n) 
	==>
	Begin
	    cur_node := n;

	    Switch (Acc)
		Case Blk_Invalid:
		    Nodes[n].Blocked := true;
		    Msg_setNoValue (OW_FAULT, a, cur_node, false, cur_msg);
	    	    cur_id := a;
	    	    Assert(!(Isundefined(cur_node))) "Undefined cur_node in OW_FAULT";
		    DispatchState(mem.State, OW_FAULT, a, mem, HomeMap[a]);

		    Msg_setNoValue (WR_Done, a, cur_node, false, cur_msg);
	    	    cur_id := a;
	    	    Assert(!(Isundefined(cur_node))) "Undefined cur_node in WR_Done";
		    mem.Data := v;
		    DispatchState(mem.State, WR_Done,  a, mem, HomeMap[a]);
		Case Blk_ReadOnly:
		    Nodes[n].Blocked := true;
		    Msg_setNoValue (OW_FAULT, a, cur_node, false, cur_msg);
	    	    cur_id := a;
	    	    Assert(!(Isundefined(cur_node))) "Undefined cur_node in OW_FAULT";
		    DispatchState(mem.State, OW_FAULT, a, mem, HomeMap[a]);

		    Msg_setNoValue (WR_Done, a, cur_node, false, cur_msg);
	    	    cur_id := a;
	    	    Assert(!(Isundefined(cur_node))) "Undefined cur_node in WR_Done";
		    mem.Data := v;
		    DispatchState(mem.State, WR_Done,  a, mem, HomeMap[a]);
		Else
                    mem.Data := v;  	-- change value
	    Endswitch; -- switch
	End;

	Rule "Store a value"
		(!Nodes[n].Blocked) & 
		(!Nodes[n].PPBlocked) &
		(HomeMap[a] != n) &
		Space_in_Network(n) 
	==>
	Begin
	    cur_node := n;
	    Switch (Acc)
		Case Blk_Invalid:
		    Nodes[n].Blocked := true;
		    Msg_set(WR_FAULT, a, v, cur_node, false, cur_msg);  -- should it need to enqueue
		    cur_id := a;
		    Assert(!(Isundefined(cur_node))) "Undefined cur_node in WR_FAULT";
		    DispatchState(mem.State, WR_FAULT, a, mem, HomeMap[a]);

		    Msg_setNoValue (WR_Done, a, cur_node, false, cur_msg);
	    	    cur_id := a;
	    	    Assert(!(Isundefined(cur_node))) "Undefined cur_node in WR_Done";
		    mem.Data := v;
		    DispatchState(mem.State, WR_Done,  a, mem, HomeMap[a]);
		Case Blk_ReadOnly:
		    Nodes[n].Blocked := true;
		    Msg_set(WR_RO_FAULT, a, v, cur_node, false, cur_msg);  -- should it need to enqueue
		    cur_id := a;
                    Assert(!(Isundefined(cur_node))) "Undefined cur_node in WR_RO_FAULT";
		    DispatchState(mem.State, WR_RO_FAULT, a, mem, HomeMap[a]);

		    Msg_setNoValue (WR_Done, a, cur_node, false, cur_msg);
	    	    cur_id := a;
	    	    Assert(!(Isundefined(cur_node))) "Undefined cur_node in WR_Done";
		    mem.Data := v;
		    DispatchState(mem.State, WR_Done,     a, mem, HomeMap[a]);
		Else
                    mem.Data := v;  	-- change value
	    Endswitch; -- switch
	End;

End; -- aliases
End; -- ruleset a
End; -- ruleset n
End; -- ruleset v
