src/HOL/UNITY/Comp/Alloc.thy
author nipkow
Thu, 22 Jul 2004 17:37:31 +0200
changeset 15074 277b3a4da341
parent 11786 51ce34ef5113
child 17310 1322ed8e0ee4
permissions -rw-r--r--
Modified \<Sum> syntax a little.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Alloc
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     2
    ID:         $Id$
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     5
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     6
Specification of Chandy and Charpentier's Allocator
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     7
*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     8
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
     9
Alloc = AllocBase + PPROD +
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    10
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    11
(** State definitions.  OUTPUT variables are locals **)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    12
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    13
record clientState =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    14
  giv :: nat list   (*client's INPUT history:  tokens GRANTED*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    15
  ask :: nat list   (*client's OUTPUT history: tokens REQUESTED*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    16
  rel :: nat list   (*client's OUTPUT history: tokens RELEASED*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    17
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    18
record 'a clientState_d =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    19
  clientState +
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    20
  dummy :: 'a       (*dummy field for new variables*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    21
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    22
constdefs
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    23
  (*DUPLICATED FROM Client.thy, but with "tok" removed*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    24
  (*Maybe want a special theory section to declare such maps*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    25
  non_dummy :: 'a clientState_d => clientState
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    26
    "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    27
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    28
  (*Renaming map to put a Client into the standard form*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    29
  client_map :: "'a clientState_d => clientState*'a"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    30
    "client_map == funPair non_dummy dummy"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    31
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    32
  
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    33
record allocState =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    34
  allocGiv :: nat => nat list   (*OUTPUT history: source of "giv" for i*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    35
  allocAsk :: nat => nat list   (*INPUT: allocator's copy of "ask" for i*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    36
  allocRel :: nat => nat list   (*INPUT: allocator's copy of "rel" for i*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    37
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    38
record 'a allocState_d =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    39
  allocState +
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    40
  dummy    :: 'a                (*dummy field for new variables*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    41
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    42
record 'a systemState =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    43
  allocState +
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    44
  client :: nat => clientState  (*states of all clients*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    45
  dummy  :: 'a                  (*dummy field for new variables*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    46
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    47
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    48
constdefs
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    49
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    50
(** Resource allocation system specification **)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    51
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    52
  (*spec (1)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    53
  system_safety :: 'a systemState program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    54
    "system_safety ==
15074
277b3a4da341 Modified \<Sum> syntax a little.
nipkow
parents: 11786
diff changeset
    55
     Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s)
277b3a4da341 Modified \<Sum> syntax a little.
nipkow
parents: 11786
diff changeset
    56
     <= NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    57
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    58
  (*spec (2)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    59
  system_progress :: 'a systemState program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    60
    "system_progress == INT i : lessThan Nclients.
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    61
			INT h. 
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    62
			  {s. h <= (ask o sub i o client)s} LeadsTo
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    63
			  {s. h pfixLe (giv o sub i o client) s}"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    64
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    65
  system_spec :: 'a systemState program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    66
    "system_spec == system_safety Int system_progress"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    67
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    68
(** Client specification (required) ***)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    69
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    70
  (*spec (3)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    71
  client_increasing :: 'a clientState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    72
    "client_increasing ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    73
         UNIV guarantees  Increasing ask Int Increasing rel"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    74
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    75
  (*spec (4)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    76
  client_bounded :: 'a clientState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    77
    "client_bounded ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    78
         UNIV guarantees  Always {s. ALL elt : set (ask s). elt <= NbT}"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    79
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    80
  (*spec (5)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    81
  client_progress :: 'a clientState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    82
    "client_progress ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    83
	 Increasing giv  guarantees
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    84
	 (INT h. {s. h <= giv s & h pfixGe ask s}
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    85
		 LeadsTo {s. tokens h <= (tokens o rel) s})"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    86
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    87
  (*spec: preserves part*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    88
  client_preserves :: 'a clientState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    89
    "client_preserves == preserves giv Int preserves clientState_d.dummy"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    90
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    91
  (*environmental constraints*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    92
  client_allowed_acts :: 'a clientState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    93
    "client_allowed_acts ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    94
       {F. AllowedActs F =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    95
	    insert Id (UNION (preserves (funPair rel ask)) Acts)}"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    96
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    97
  client_spec :: 'a clientState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    98
    "client_spec == client_increasing Int client_bounded Int client_progress
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
    99
                    Int client_allowed_acts Int client_preserves"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   100
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   101
(** Allocator specification (required) ***)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   102
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   103
  (*spec (6)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   104
  alloc_increasing :: 'a allocState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   105
    "alloc_increasing ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   106
	 UNIV  guarantees
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   107
	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   108
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   109
  (*spec (7)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   110
  alloc_safety :: 'a allocState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   111
    "alloc_safety ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   112
	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   113
         guarantees
15074
277b3a4da341 Modified \<Sum> syntax a little.
nipkow
parents: 11786
diff changeset
   114
	 Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s)
277b3a4da341 Modified \<Sum> syntax a little.
nipkow
parents: 11786
diff changeset
   115
         <= NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
11194
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   116
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   117
  (*spec (8)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   118
  alloc_progress :: 'a allocState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   119
    "alloc_progress ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   120
	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   121
	                             Increasing (sub i o allocRel))
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   122
         Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   123
         Always {s. ALL i<Nclients.
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   124
		     ALL elt : set ((sub i o allocAsk) s). elt <= NbT}
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   125
         Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   126
         (INT i : lessThan Nclients. 
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   127
	  INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   128
		 LeadsTo
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   129
	         {s. tokens h <= (tokens o sub i o allocRel)s})
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   130
         guarantees
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   131
	     (INT i : lessThan Nclients.
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   132
	      INT h. {s. h <= (sub i o allocAsk) s}
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   133
	             LeadsTo
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   134
	             {s. h pfixLe (sub i o allocGiv) s})"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   135
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   136
  (*NOTE: to follow the original paper, the formula above should have had
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   137
	INT h. {s. h i <= (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   138
	       LeadsTo
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   139
	       {s. tokens h i <= (tokens o sub i o allocRel)s})
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   140
    thus h should have been a function variable.  However, only h i is ever
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   141
    looked at.*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   142
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   143
  (*spec: preserves part*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   144
  alloc_preserves :: 'a allocState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   145
    "alloc_preserves == preserves allocRel Int preserves allocAsk Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   146
                        preserves allocState_d.dummy"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   147
  
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   148
  (*environmental constraints*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   149
  alloc_allowed_acts :: 'a allocState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   150
    "alloc_allowed_acts ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   151
       {F. AllowedActs F =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   152
	    insert Id (UNION (preserves allocGiv) Acts)}"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   153
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   154
  alloc_spec :: 'a allocState_d program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   155
    "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   156
                   alloc_allowed_acts Int alloc_preserves"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   157
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   158
(** Network specification ***)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   159
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   160
  (*spec (9.1)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   161
  network_ask :: 'a systemState program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   162
    "network_ask == INT i : lessThan Nclients.
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   163
			Increasing (ask o sub i o client)  guarantees
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   164
			((sub i o allocAsk) Fols (ask o sub i o client))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   165
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   166
  (*spec (9.2)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   167
  network_giv :: 'a systemState program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   168
    "network_giv == INT i : lessThan Nclients.
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   169
			Increasing (sub i o allocGiv)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   170
			guarantees
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   171
			((giv o sub i o client) Fols (sub i o allocGiv))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   172
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   173
  (*spec (9.3)*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   174
  network_rel :: 'a systemState program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   175
    "network_rel == INT i : lessThan Nclients.
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   176
			Increasing (rel o sub i o client)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   177
			guarantees
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   178
			((sub i o allocRel) Fols (rel o sub i o client))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   179
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   180
  (*spec: preserves part*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   181
  network_preserves :: 'a systemState program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   182
    "network_preserves ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   183
       preserves allocGiv  Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   184
       (INT i : lessThan Nclients. preserves (rel o sub i o client)  Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   185
                                   preserves (ask o sub i o client))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   186
  
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   187
  (*environmental constraints*)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   188
  network_allowed_acts :: 'a systemState program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   189
    "network_allowed_acts ==
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   190
       {F. AllowedActs F =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   191
           insert Id
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   192
	    (UNION (preserves allocRel Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   193
		    (INT i: lessThan Nclients. preserves(giv o sub i o client)))
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   194
		  Acts)}"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   195
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   196
  network_spec :: 'a systemState program set
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   197
    "network_spec == network_ask Int network_giv Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   198
                     network_rel Int network_allowed_acts Int
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   199
                     network_preserves"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   200
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   201
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   202
(** State mappings **)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   203
  sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   204
    "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   205
                       in (| allocGiv = allocGiv s,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   206
			     allocAsk = allocAsk s,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   207
			     allocRel = allocRel s,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   208
			     client   = cl,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   209
			     dummy    = xtr|)"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   210
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   211
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   212
  sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   213
    "sysOfClient == %(cl,al). (| allocGiv = allocGiv al,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   214
			         allocAsk = allocAsk al,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   215
			         allocRel = allocRel al,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   216
			         client   = cl,
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   217
			         systemState.dummy = allocState_d.dummy al|)"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   218
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   219
consts 
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   220
    Alloc   :: 'a allocState_d program
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   221
    Client  :: 'a clientState_d program
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   222
    Network :: 'a systemState program
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   223
    System  :: 'a systemState program
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   224
  
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   225
rules
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   226
    Alloc   "Alloc   : alloc_spec"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   227
    Client  "Client  : client_spec"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   228
    Network "Network : network_spec"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   229
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   230
defs
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   231
    System_def
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   232
      "System == rename sysOfAlloc Alloc Join Network Join
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   233
                 (rename sysOfClient
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   234
		  (plam x: lessThan Nclients. rename client_map Client))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   235
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   236
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   237
(**
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   238
locale System =
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   239
  fixes 
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   240
    Alloc   :: 'a allocState_d program
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   241
    Client  :: 'a clientState_d program
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   242
    Network :: 'a systemState program
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   243
    System  :: 'a systemState program
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   244
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   245
  assumes
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   246
    Alloc   "Alloc   : alloc_spec"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   247
    Client  "Client  : client_spec"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   248
    Network "Network : network_spec"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   249
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   250
  defines
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   251
    System_def
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   252
      "System == rename sysOfAlloc Alloc
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   253
                 Join
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   254
                 Network
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   255
                 Join
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   256
                 (rename sysOfClient
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   257
		  (plam x: lessThan Nclients. rename client_map Client))"
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   258
**)
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   259
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   260
ea13ff5a26d1 reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
paulson
parents:
diff changeset
   261
end