1 (* Title: HOL/UNITY/Client.thy |
1 (* Title: HOL/UNITY/Comp/Client.thy |
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
3 Copyright 1998 University of Cambridge |
5 *) |
4 *) |
6 |
5 |
7 header{*Distributed Resource Management System: the Client*} |
6 header{*Distributed Resource Management System: the Client*} |
8 |
7 |
9 theory Client imports Rename AllocBase begin |
8 theory Client imports Rename AllocBase begin |
10 |
9 |
11 types |
10 types |
12 tokbag = nat --{*tokbags could be multisets...or any ordered type?*} |
11 tokbag = nat --{*tokbags could be multisets...or any ordered type?*} |
13 |
12 |
14 record state = |
13 record state = |
15 giv :: "tokbag list" --{*input history: tokens granted*} |
14 giv :: "tokbag list" --{*input history: tokens granted*} |
16 ask :: "tokbag list" --{*output history: tokens requested*} |
15 ask :: "tokbag list" --{*output history: tokens requested*} |
17 rel :: "tokbag list" --{*output history: tokens released*} |
16 rel :: "tokbag list" --{*output history: tokens released*} |
18 tok :: tokbag --{*current token request*} |
17 tok :: tokbag --{*current token request*} |
19 |
18 |
20 record 'a state_d = |
19 record 'a state_d = |
21 state + |
20 state + |
22 dummy :: 'a --{*new variables*} |
21 dummy :: 'a --{*new variables*} |
23 |
22 |
28 |
27 |
29 (** Release some tokens **) |
28 (** Release some tokens **) |
30 |
29 |
31 rel_act :: "('a state_d * 'a state_d) set" |
30 rel_act :: "('a state_d * 'a state_d) set" |
32 "rel_act == {(s,s'). |
31 "rel_act == {(s,s'). |
33 \<exists>nrel. nrel = size (rel s) & |
32 \<exists>nrel. nrel = size (rel s) & |
34 s' = s (| rel := rel s @ [giv s!nrel] |) & |
33 s' = s (| rel := rel s @ [giv s!nrel] |) & |
35 nrel < size (giv s) & |
34 nrel < size (giv s) & |
36 ask s!nrel \<le> giv s!nrel}" |
35 ask s!nrel \<le> giv s!nrel}" |
37 |
36 |
38 (** Choose a new token requirement **) |
37 (** Choose a new token requirement **) |
39 |
38 |
40 (** Including s'=s suppresses fairness, allowing the non-trivial part |
39 (** Including s'=s suppresses fairness, allowing the non-trivial part |
41 of the action to be ignored **) |
40 of the action to be ignored **) |
43 tok_act :: "('a state_d * 'a state_d) set" |
42 tok_act :: "('a state_d * 'a state_d) set" |
44 "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" |
43 "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" |
45 |
44 |
46 ask_act :: "('a state_d * 'a state_d) set" |
45 ask_act :: "('a state_d * 'a state_d) set" |
47 "ask_act == {(s,s'). s'=s | |
46 "ask_act == {(s,s'). s'=s | |
48 (s' = s (|ask := ask s @ [tok s]|))}" |
47 (s' = s (|ask := ask s @ [tok s]|))}" |
49 |
48 |
50 Client :: "'a state_d program" |
49 Client :: "'a state_d program" |
51 "Client == |
50 "Client == |
52 mk_total_program |
51 mk_total_program |
53 ({s. tok s \<in> atMost NbT & |
52 ({s. tok s \<in> atMost NbT & |
54 giv s = [] & ask s = [] & rel s = []}, |
53 giv s = [] & ask s = [] & rel s = []}, |
55 {rel_act, tok_act, ask_act}, |
54 {rel_act, tok_act, ask_act}, |
56 \<Union>G \<in> preserves rel Int preserves ask Int preserves tok. |
55 \<Union>G \<in> preserves rel Int preserves ask Int preserves tok. |
57 Acts G)" |
56 Acts G)" |
58 |
57 |
59 (*Maybe want a special theory section to declare such maps*) |
58 (*Maybe want a special theory section to declare such maps*) |
60 non_dummy :: "'a state_d => state" |
59 non_dummy :: "'a state_d => state" |
61 "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)" |
60 "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)" |
62 |
61 |