src/HOL/UNITY/Comp/Alloc.thy
changeset 67445 4311845b0412
parent 67443 3abf6a722518
child 67613 ce654b0e6d69
equal deleted inserted replaced
67444:100247708f31 67445:4311845b0412
    45   allocState +
    45   allocState +
    46   client :: "nat => clientState"  \<comment> \<open>states of all clients\<close>
    46   client :: "nat => clientState"  \<comment> \<open>states of all clients\<close>
    47   dummy  :: 'a                    \<comment> \<open>dummy field for new variables\<close>
    47   dummy  :: 'a                    \<comment> \<open>dummy field for new variables\<close>
    48 
    48 
    49 
    49 
    50 \<comment> \<open>* Resource allocation system specification *\<close>
    50 subsubsection \<open>Resource allocation system specification\<close>
    51 
    51 
    52 definition
    52 definition
    53   \<comment> \<open>spec (1)\<close>
    53   \<comment> \<open>spec (1)\<close>
    54   system_safety :: "'a systemState program set"
    54   system_safety :: "'a systemState program set"
    55   where "system_safety =
    55   where "system_safety =
    66 
    66 
    67 definition
    67 definition
    68   system_spec :: "'a systemState program set"
    68   system_spec :: "'a systemState program set"
    69   where "system_spec = system_safety Int system_progress"
    69   where "system_spec = system_safety Int system_progress"
    70 
    70 
    71 \<comment> \<open>* Client specification (required) **\<close>
    71 
       
    72 subsubsection \<open>Client specification (required)\<close>
    72 
    73 
    73 definition
    74 definition
    74   \<comment> \<open>spec (3)\<close>
    75   \<comment> \<open>spec (3)\<close>
    75   client_increasing :: "'a clientState_d program set"
    76   client_increasing :: "'a clientState_d program set"
    76   where "client_increasing = UNIV guarantees  Increasing ask Int Increasing rel"
    77   where "client_increasing = UNIV guarantees  Increasing ask Int Increasing rel"
   103 definition
   104 definition
   104   client_spec :: "'a clientState_d program set"
   105   client_spec :: "'a clientState_d program set"
   105   where "client_spec = client_increasing Int client_bounded Int client_progress
   106   where "client_spec = client_increasing Int client_bounded Int client_progress
   106                     Int client_allowed_acts Int client_preserves"
   107                     Int client_allowed_acts Int client_preserves"
   107 
   108 
   108 \<comment> \<open>* Allocator specification (required) *\<close>
   109 
       
   110 subsubsection \<open>Allocator specification (required)\<close>
   109 
   111 
   110 definition
   112 definition
   111   \<comment> \<open>spec (6)\<close>
   113   \<comment> \<open>spec (6)\<close>
   112   alloc_increasing :: "'a allocState_d program set"
   114   alloc_increasing :: "'a allocState_d program set"
   113   where "alloc_increasing =
   115   where "alloc_increasing =
   166 definition
   168 definition
   167   alloc_spec :: "'a allocState_d program set"
   169   alloc_spec :: "'a allocState_d program set"
   168   where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int
   170   where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int
   169                    alloc_allowed_acts Int alloc_preserves"
   171                    alloc_allowed_acts Int alloc_preserves"
   170 
   172 
   171 \<comment> \<open>* Network specification *\<close>
   173 
       
   174 subsubsection \<open>Network specification\<close>
   172 
   175 
   173 definition
   176 definition
   174   \<comment> \<open>spec (9.1)\<close>
   177   \<comment> \<open>spec (9.1)\<close>
   175   network_ask :: "'a systemState program set"
   178   network_ask :: "'a systemState program set"
   176   where "network_ask = (INT i : lessThan Nclients.
   179   where "network_ask = (INT i : lessThan Nclients.
   216   where "network_spec = network_ask Int network_giv Int
   219   where "network_spec = network_ask Int network_giv Int
   217                      network_rel Int network_allowed_acts Int
   220                      network_rel Int network_allowed_acts Int
   218                      network_preserves"
   221                      network_preserves"
   219 
   222 
   220 
   223 
   221 \<comment> \<open>* State mappings *\<close>
   224 subsubsection \<open>State mappings\<close>
       
   225 
   222 definition
   226 definition
   223   sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
   227   sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
   224   where "sysOfAlloc = (%s. let (cl,xtr) = allocState_d.dummy s
   228   where "sysOfAlloc = (%s. let (cl,xtr) = allocState_d.dummy s
   225                        in (| allocGiv = allocGiv s,
   229                        in (| allocGiv = allocGiv s,
   226                              allocAsk = allocAsk s,
   230                              allocAsk = allocAsk s,