equal
deleted
inserted
replaced
5 |
5 |
6 *) |
6 *) |
7 |
7 |
8 header{*Common declarations for Chandy and Charpentier's Allocator*} |
8 header{*Common declarations for Chandy and Charpentier's Allocator*} |
9 |
9 |
10 theory AllocBase = Follows + MultisetSum + Guar: |
10 theory AllocBase imports Follows MultisetSum Guar begin |
11 |
11 |
12 consts |
12 consts |
13 tokbag :: i (* tokbags could be multisets...or any ordered type?*) |
13 tokbag :: i (* tokbags could be multisets...or any ordered type?*) |
14 NbT :: i (* Number of tokens in system *) |
14 NbT :: i (* Number of tokens in system *) |
15 Nclients :: i (* Number of clients *) |
15 Nclients :: i (* Number of clients *) |