equal
deleted
inserted
replaced
9 RefMappings = Traces + |
9 RefMappings = Traces + |
10 |
10 |
11 default term |
11 default term |
12 |
12 |
13 consts |
13 consts |
14 laststate ::"('a,'s)execution => 's" |
14 |
15 move ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" |
15 move ::"[('a,'s)ioa,('a,'s)pairs,'s,'a,'s] => bool" |
16 is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |
16 is_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |
17 is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |
17 is_weak_ref_map ::"[('s1=>'s2),('a,'s1)ioa,('a,'s2)ioa] => bool" |
18 |
18 |
|
19 |
19 defs |
20 defs |
20 |
21 |
21 laststate_def |
|
22 "laststate ex == case Last`(snd ex) of |
|
23 Undef => fst ex |
|
24 | Def at => snd at" |
|
25 |
22 |
26 move_def |
23 move_def |
27 "move ioa ex s a t == |
24 "move ioa ex s a t == |
28 (is_exec_frag ioa (s,ex) & Finite ex & |
25 (is_exec_frag ioa (s,ex) & Finite ex & |
29 laststate (s,ex)=t & |
26 laststate (s,ex)=t & |
43 s -a--C-> t |
40 s -a--C-> t |
44 --> (if a:ext(C) |
41 --> (if a:ext(C) |
45 then (f s) -a--A-> (f t) |
42 then (f s) -a--A-> (f t) |
46 else (f s)=(f t)))" |
43 else (f s)=(f t)))" |
47 |
44 |
|
45 |
48 end |
46 end |