1 (* Title: ZF/UNITY/ClientImpl.thy |
1 (* Title: ZF/UNITY/ClientImpl.thy |
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
2 Author: Sidi O Ehmety, Cambridge University Computer Laboratory |
4 Copyright 2002 University of Cambridge |
3 Copyright 2002 University of Cambridge |
5 |
4 |
6 Distributed Resource Management System: Client Implementation |
5 Distributed Resource Management System: Client Implementation. |
7 *) |
6 *) |
8 |
7 |
9 theory ClientImpl imports AllocBase Guar begin |
8 theory ClientImpl imports AllocBase Guar begin |
10 |
9 |
11 abbreviation "ask == Var(Nil)" (* input history: tokens requested *) |
10 abbreviation "ask == Var(Nil)" (* input history: tokens requested *) |
36 (** Choose a new token requirement **) |
35 (** Choose a new token requirement **) |
37 (** Including t=s suppresses fairness, allowing the non-trivial part |
36 (** Including t=s suppresses fairness, allowing the non-trivial part |
38 of the action to be ignored **) |
37 of the action to be ignored **) |
39 definition |
38 definition |
40 "client_tok_act == {<s,t> \<in> state*state. t=s | |
39 "client_tok_act == {<s,t> \<in> state*state. t=s | |
41 t = s(tok:=succ(s`tok mod NbT))}" |
40 t = s(tok:=succ(s`tok mod NbT))}" |
42 |
41 |
43 definition |
42 definition |
44 "client_ask_act == {<s,t> \<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}" |
43 "client_ask_act == {<s,t> \<in> state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}" |
45 |
44 |
46 definition |
45 definition |
47 "client_prog == |
46 "client_prog == |
48 mk_program({s \<in> state. s`tok \<le> NbT & s`giv = Nil & |
47 mk_program({s \<in> state. s`tok \<le> NbT & s`giv = Nil & |
49 s`ask = Nil & s`rel = Nil}, |
48 s`ask = Nil & s`rel = Nil}, |
50 {client_rel_act, client_tok_act, client_ask_act}, |
49 {client_rel_act, client_tok_act, client_ask_act}, |
51 \<Union>G \<in> preserves(lift(rel)) Int |
50 \<Union>G \<in> preserves(lift(rel)) Int |
52 preserves(lift(ask)) Int |
51 preserves(lift(ask)) Int |
53 preserves(lift(tok)). Acts(G))" |
52 preserves(lift(tok)). Acts(G))" |
54 |
53 |
55 |
54 |
56 declare type_assumes [simp] default_val_assumes [simp] |
55 declare type_assumes [simp] default_val_assumes [simp] |
57 (* This part should be automated *) |
56 (* This part should be automated *) |
58 |
57 |