author | paulson |
Mon, 01 Mar 1999 18:38:43 +0100 | |
changeset 6295 | 351b3c2b0d83 |
parent 6012 | 1894bfc4aee9 |
child 6800 | 9ee166138311 |
permissions | -rw-r--r-- |
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'). |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5648
diff
changeset
|
32 |
EX nrel. nrel = size (rel s) & |
5636 | 33 |
s' = s (| rel := rel s @ [giv s!nrel] |) & |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5648
diff
changeset
|
34 |
nrel < size (giv s) & |
5636 | 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]|) & |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5648
diff
changeset
|
48 |
size (ask s) = size (rel s))}" |
5636 | 49 |
|
50 |
Cli_prg :: state program |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6012
diff
changeset
|
51 |
"Cli_prg == mk_program ({s. tok s : atMost Max & |
5636 | 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 == |
|
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5648
diff
changeset
|
59 |
{s. size (giv s) <= size (ask s) & |
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5648
diff
changeset
|
60 |
(ALL n: lessThan (size (giv s)). ask s!n <= giv s!n)}" |
5636 | 61 |
|
62 |
end |