5636
|
1 |
(* Title: HOL/UNITY/Client.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5 |
|
|
6 |
Distributed Resource Management System: the Client
|
|
7 |
*)
|
|
8 |
|
|
9 |
Client = Comp + Prefix +
|
|
10 |
|
|
11 |
consts
|
|
12 |
Max :: nat (*Maximum number of tokens*)
|
|
13 |
|
|
14 |
types
|
|
15 |
tokbag = nat (*tokbags could be multisets...or any ordered type?*)
|
|
16 |
|
|
17 |
record state =
|
|
18 |
giv :: tokbag list (*input history: tokens granted*)
|
|
19 |
ask :: tokbag list (*output history: tokens requested*)
|
|
20 |
rel :: tokbag list (*output history: tokens released*)
|
|
21 |
tok :: tokbag (*current token request*)
|
|
22 |
|
|
23 |
|
|
24 |
(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
|
|
25 |
|
|
26 |
constdefs
|
|
27 |
|
|
28 |
(** Release some tokens **)
|
|
29 |
|
|
30 |
rel_act :: "(state*state) set"
|
|
31 |
"rel_act == {(s,s').
|
|
32 |
EX nrel. nrel = length (rel s) &
|
|
33 |
s' = s (| rel := rel s @ [giv s!nrel] |) &
|
|
34 |
nrel < length (giv s) &
|
|
35 |
ask s!nrel <= giv s!nrel}"
|
|
36 |
|
|
37 |
(** Choose a new token requirement **)
|
|
38 |
|
|
39 |
(** Including s'=s suppresses fairness, allowing the non-trivial part
|
|
40 |
of the action to be ignored **)
|
|
41 |
|
|
42 |
tok_act :: "(state*state) set"
|
|
43 |
"tok_act == {(s,s'). s'=s | (EX t: atMost Max. s' = s (|tok := t|))}"
|
|
44 |
|
|
45 |
ask_act :: "(state*state) set"
|
|
46 |
"ask_act == {(s,s'). s'=s |
|
|
47 |
(s' = s (|ask := ask s @ [tok s]|) &
|
|
48 |
length (ask s) = length (rel s))}"
|
|
49 |
|
|
50 |
Cli_prg :: state program
|
|
51 |
"Cli_prg == mk_program ({s. tok s : atMost Max &
|
|
52 |
giv s = [] &
|
|
53 |
ask s = [] &
|
|
54 |
rel s = []},
|
|
55 |
{rel_act, tok_act, ask_act})"
|
|
56 |
|
|
57 |
giv_meets_ask :: state set
|
|
58 |
"giv_meets_ask ==
|
|
59 |
{s. length (giv s) <= length (ask s) &
|
|
60 |
(ALL n: lessThan (length (giv s)). ask s!n <= giv s!n)}"
|
|
61 |
|
|
62 |
end
|