|
4776
|
1 |
Traces = UNITY +
|
|
|
2 |
|
|
|
3 |
consts traces :: "['a set, ('a * 'a)set set] => 'a list set"
|
|
|
4 |
|
|
|
5 |
inductive "traces Init Acts"
|
|
|
6 |
intrs
|
|
|
7 |
(*Initial trace is empty*)
|
|
|
8 |
Init "s: Init ==> [s] : traces Init Acts"
|
|
|
9 |
|
|
|
10 |
Acts "[| act: Acts; s#evs : traces Init Acts; (s,s'): act |]
|
|
|
11 |
==> s'#s#evs : traces Init Acts"
|
|
|
12 |
|
|
|
13 |
|
|
|
14 |
consts reachable :: "['a set, ('a * 'a)set set] => 'a set"
|
|
|
15 |
|
|
|
16 |
inductive "reachable Init Acts"
|
|
|
17 |
intrs
|
|
|
18 |
(*Initial trace is empty*)
|
|
|
19 |
Init "s: Init ==> s : reachable Init Acts"
|
|
|
20 |
|
|
|
21 |
Acts "[| act: Acts; s : reachable Init Acts; (s,s'): act |]
|
|
|
22 |
==> s' : reachable Init Acts"
|
|
|
23 |
|
|
|
24 |
end
|