equal
deleted
inserted
replaced
5 |
5 |
6 Distributed Resource Management System: the Client |
6 Distributed Resource Management System: the Client |
7 *) |
7 *) |
8 |
8 |
9 Client = Comp + Prefix + |
9 Client = Comp + Prefix + |
10 |
|
11 constdefs (*MOVE higher-up: UNITY.thy or Traces.thy ???*) |
|
12 always :: "'a set => 'a program set" |
|
13 "always A == {F. reachable F <= A}" |
|
14 |
|
15 (*The traditional word for inductive properties. Anyway, INDUCTIVE is |
|
16 reserved!*) |
|
17 invariant :: "'a set => 'a program set" |
|
18 "invariant A == {F. Init F <= A & stable (Acts F) A}" |
|
19 |
|
20 (*Polymorphic in both states and the meaning of <= *) |
|
21 increasing :: "['a => 'b::{ord}] => 'a program set" |
|
22 "increasing f == {F. ALL z. stable (Acts F) {s. z <= f s}}" |
|
23 |
|
24 (*The set of systems that regard "f" as local to F*) |
|
25 localTo :: ['a => 'b, 'a program] => 'a program set (infixl 80) |
|
26 "f localTo F == {G. ALL z. stable (Acts G - Acts F) {s. f s = z}}" |
|
27 |
|
28 |
10 |
29 consts |
11 consts |
30 Max :: nat (*Maximum number of tokens*) |
12 Max :: nat (*Maximum number of tokens*) |
31 |
13 |
32 types |
14 types |