src/HOL/UNITY/Comp/Alloc.thy
changeset 15074 277b3a4da341
parent 11786 51ce34ef5113
child 17310 1322ed8e0ee4
equal deleted inserted replaced
15073:279c2daaf517 15074:277b3a4da341
    50 (** Resource allocation system specification **)
    50 (** Resource allocation system specification **)
    51 
    51 
    52   (*spec (1)*)
    52   (*spec (1)*)
    53   system_safety :: 'a systemState program set
    53   system_safety :: 'a systemState program set
    54     "system_safety ==
    54     "system_safety ==
    55      Always {s. (\\<Sum>i: lessThan Nclients. (tokens o giv o sub i o client)s)
    55      Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s)
    56      <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
    56      <= NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
    57 
    57 
    58   (*spec (2)*)
    58   (*spec (2)*)
    59   system_progress :: 'a systemState program set
    59   system_progress :: 'a systemState program set
    60     "system_progress == INT i : lessThan Nclients.
    60     "system_progress == INT i : lessThan Nclients.
    61 			INT h. 
    61 			INT h. 
   109   (*spec (7)*)
   109   (*spec (7)*)
   110   alloc_safety :: 'a allocState_d program set
   110   alloc_safety :: 'a allocState_d program set
   111     "alloc_safety ==
   111     "alloc_safety ==
   112 	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
   112 	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
   113          guarantees
   113          guarantees
   114 	 Always {s. (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocGiv)s)
   114 	 Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s)
   115          <= NbT + (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
   115          <= NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
   116 
   116 
   117   (*spec (8)*)
   117   (*spec (8)*)
   118   alloc_progress :: 'a allocState_d program set
   118   alloc_progress :: 'a allocState_d program set
   119     "alloc_progress ==
   119     "alloc_progress ==
   120 	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
   120 	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int