src/ZF/UNITY/ClientImpl.thy
author paulson
Thu May 29 17:10:00 2003 +0200 (2003-05-29)
changeset 14053 4daa384f4fd7
child 14057 57de6d68389e
permissions -rw-r--r--
Introduction of the theories UNITY/Merge, UNITY/ClientImpl
paulson@14053
     1
(*  Title:      ZF/UNITY/ClientImpl.thy
paulson@14053
     2
    ID:         $Id$
paulson@14053
     3
    Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
paulson@14053
     4
    Copyright   2002  University of Cambridge
paulson@14053
     5
paulson@14053
     6
Distributed Resource Management System:  Client Implementation
paulson@14053
     7
*)
paulson@14053
     8
paulson@14053
     9
paulson@14053
    10
ClientImpl = AllocBase + Guar +
paulson@14053
    11
consts
paulson@14053
    12
  ask :: i (* input history:  tokens requested *)
paulson@14053
    13
  giv :: i (* output history: tokens granted *)
paulson@14053
    14
  rel :: i (* input history: tokens released *)
paulson@14053
    15
  tok :: i (* the number of available tokens *)
paulson@14053
    16
paulson@14053
    17
translations
paulson@14053
    18
  "ask" == "Var(Nil)"
paulson@14053
    19
  "giv" == "Var([0])"
paulson@14053
    20
  "rel" == "Var([1])"
paulson@14053
    21
  "tok" == "Var([2])"
paulson@14053
    22
paulson@14053
    23
rules
paulson@14053
    24
  type_assumes
paulson@14053
    25
  "type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) & 
paulson@14053
    26
   type_of(rel) = list(tokbag) & type_of(tok) = nat"
paulson@14053
    27
  default_val_assumes
paulson@14053
    28
  "default_val(ask) = Nil & default_val(giv)  = Nil & 
paulson@14053
    29
   default_val(rel)  = Nil & default_val(tok)  = 0"
paulson@14053
    30
paulson@14053
    31
paulson@14053
    32
(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
paulson@14053
    33
paulson@14053
    34
constdefs
paulson@14053
    35
 (** Release some client_tokens **)
paulson@14053
    36
  
paulson@14053
    37
  client_rel_act ::i
paulson@14053
    38
    "client_rel_act ==
paulson@14053
    39
     {<s,t>:state*state. EX nrel:nat. nrel = length(s`rel)
paulson@14053
    40
		    &  t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) &
paulson@14053
    41
                  nrel < length(s`giv) &
paulson@14053
    42
                  nth(nrel, s`ask) le nth(nrel, s`giv)}"
paulson@14053
    43
  
paulson@14053
    44
  (** Choose a new token requirement **)
paulson@14053
    45
  (** Including s'=s suppresses fairness, allowing the non-trivial part
paulson@14053
    46
      of the action to be ignored **)
paulson@14053
    47
paulson@14053
    48
  client_tok_act :: i
paulson@14053
    49
 "client_tok_act == {<s,t>:state*state. t=s |
paulson@14053
    50
		 (t = s(tok:=succ(s`tok mod NbT)))}"
paulson@14053
    51
paulson@14053
    52
  client_ask_act :: i
paulson@14053
    53
  "client_ask_act == {<s,t>:state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
paulson@14053
    54
  
paulson@14053
    55
  client_prog :: i
paulson@14053
    56
  "client_prog ==
paulson@14053
    57
   mk_program({s:state. s`tok le NbT & s`giv = Nil &
paulson@14053
    58
	               s`ask = Nil & s`rel = Nil},
paulson@14053
    59
                    {client_rel_act, client_tok_act, client_ask_act},
paulson@14053
    60
                   UN G: preserves(lift(rel)) Int
paulson@14053
    61
			 preserves(lift(ask)) Int
paulson@14053
    62
	                 preserves(lift(tok)).  Acts(G))"
paulson@14053
    63
end