--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/UNITY/ClientImpl.thy Thu May 29 17:10:00 2003 +0200
@@ -0,0 +1,63 @@
+(* Title: ZF/UNITY/ClientImpl.thy
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2002 University of Cambridge
+
+Distributed Resource Management System: Client Implementation
+*)
+
+
+ClientImpl = AllocBase + Guar +
+consts
+ ask :: i (* input history: tokens requested *)
+ giv :: i (* output history: tokens granted *)
+ rel :: i (* input history: tokens released *)
+ tok :: i (* the number of available tokens *)
+
+translations
+ "ask" == "Var(Nil)"
+ "giv" == "Var([0])"
+ "rel" == "Var([1])"
+ "tok" == "Var([2])"
+
+rules
+ type_assumes
+ "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) &
+ type_of(rel) = list(tokbag) & type_of(tok) = nat"
+ default_val_assumes
+ "default_val(ask) = Nil & default_val(giv) = Nil &
+ default_val(rel) = Nil & default_val(tok) = 0"
+
+
+(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
+
+constdefs
+ (** Release some client_tokens **)
+
+ client_rel_act ::i
+ "client_rel_act ==
+ {<s,t>:state*state. EX nrel:nat. nrel = length(s`rel)
+ & t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
+ nrel < length(s`giv) &
+ nth(nrel, s`ask) le nth(nrel, s`giv)}"
+
+ (** Choose a new token requirement **)
+ (** Including s'=s suppresses fairness, allowing the non-trivial part
+ of the action to be ignored **)
+
+ client_tok_act :: i
+ "client_tok_act == {<s,t>:state*state. t=s |
+ (t = s(tok:=succ(s`tok mod NbT)))}"
+
+ client_ask_act :: i
+ "client_ask_act == {<s,t>:state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
+
+ client_prog :: i
+ "client_prog ==
+ mk_program({s:state. s`tok le NbT & s`giv = Nil &
+ s`ask = Nil & s`rel = Nil},
+ {client_rel_act, client_tok_act, client_ask_act},
+ UN G: preserves(lift(rel)) Int
+ preserves(lift(ask)) Int
+ preserves(lift(tok)). Acts(G))"
+end
\ No newline at end of file