author | paulson |
Sat, 23 Sep 2000 16:02:01 +0200 | |
changeset 10064 | 1a77667b21ef |
parent 9403 | aad13b59b8d9 |
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 |
||
8931 | 9 |
Client = Rename + AllocBase + |
5636 | 10 |
|
11 |
types |
|
12 |
tokbag = nat (*tokbags could be multisets...or any ordered type?*) |
|
13 |
||
14 |
record state = |
|
15 |
giv :: tokbag list (*input history: tokens granted*) |
|
16 |
ask :: tokbag list (*output history: tokens requested*) |
|
17 |
rel :: tokbag list (*output history: tokens released*) |
|
18 |
tok :: tokbag (*current token request*) |
|
19 |
||
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8931
diff
changeset
|
20 |
record 'a state_d = |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
21 |
state + |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8931
diff
changeset
|
22 |
dummy :: 'a (*new variables*) |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
23 |
|
5636 | 24 |
|
25 |
(*Array indexing is translated to list indexing as A[n] == A!(n-1). *) |
|
26 |
||
27 |
constdefs |
|
28 |
||
29 |
(** Release some tokens **) |
|
30 |
||
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8931
diff
changeset
|
31 |
rel_act :: "('a state_d * 'a state_d) set" |
5636 | 32 |
"rel_act == {(s,s'). |
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5648
diff
changeset
|
33 |
EX nrel. nrel = size (rel s) & |
5636 | 34 |
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
|
35 |
nrel < size (giv s) & |
5636 | 36 |
ask s!nrel <= giv s!nrel}" |
37 |
||
38 |
(** Choose a new token requirement **) |
|
39 |
||
40 |
(** Including s'=s suppresses fairness, allowing the non-trivial part |
|
41 |
of the action to be ignored **) |
|
42 |
||
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8931
diff
changeset
|
43 |
tok_act :: "('a state_d * 'a state_d) set" |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
44 |
"tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}" |
8216 | 45 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8931
diff
changeset
|
46 |
ask_act :: "('a state_d * 'a state_d) set" |
5636 | 47 |
"ask_act == {(s,s'). s'=s | |
8216 | 48 |
(s' = s (|ask := ask s @ [tok s]|))}" |
5636 | 49 |
|
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8931
diff
changeset
|
50 |
Client :: 'a state_d program |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
51 |
"Client == |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
52 |
mk_program ({s. tok s : atMost NbT & |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
53 |
giv s = [] & ask s = [] & rel s = []}, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
54 |
{rel_act, tok_act, ask_act}, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
55 |
UN G: preserves rel Int preserves ask Int preserves tok. |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9403
diff
changeset
|
56 |
Acts G)" |
5636 | 57 |
|
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
58 |
(*Maybe want a special theory section to declare such maps*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8931
diff
changeset
|
59 |
non_dummy :: 'a state_d => state |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8931
diff
changeset
|
60 |
"non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)" |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
61 |
|
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
62 |
(*Renaming map to put a Client into the standard form*) |
9403
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8931
diff
changeset
|
63 |
client_map :: "'a state_d => state*'a" |
aad13b59b8d9
much tidying in connection with the 2nd UNITY paper
paulson
parents:
8931
diff
changeset
|
64 |
"client_map == funPair non_dummy dummy" |
8251
9be357df93d4
New treatment of "guarantees" with polymorphic components and bijections.
paulson
parents:
8216
diff
changeset
|
65 |
|
5636 | 66 |
end |