13 definition |
13 definition |
14 is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
14 is_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
15 "is_simulation R C A = |
15 "is_simulation R C A = |
16 ((!s:starts_of C. R``{s} Int starts_of A ~= {}) & |
16 ((!s:starts_of C. R``{s} Int starts_of A ~= {}) & |
17 (!s s' t a. reachable C s & |
17 (!s s' t a. reachable C s & |
18 s -a--C-> t & |
18 s \<midarrow>a\<midarrow>C\<rightarrow> t & |
19 (s,s') : R |
19 (s,s') : R |
20 --> (? t' ex. (t,t'):R & move A ex s' a t')))" |
20 --> (? t' ex. (t,t'):R & move A ex s' a t')))" |
21 |
21 |
22 definition |
22 definition |
23 is_backward_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
23 is_backward_simulation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
24 "is_backward_simulation R C A = |
24 "is_backward_simulation R C A = |
25 ((!s:starts_of C. R``{s} <= starts_of A) & |
25 ((!s:starts_of C. R``{s} <= starts_of A) & |
26 (!s t t' a. reachable C s & |
26 (!s t t' a. reachable C s & |
27 s -a--C-> t & |
27 s \<midarrow>a\<midarrow>C\<rightarrow> t & |
28 (t,t') : R |
28 (t,t') : R |
29 --> (? ex s'. (s,s'):R & move A ex s' a t')))" |
29 --> (? ex s'. (s,s'):R & move A ex s' a t')))" |
30 |
30 |
31 definition |
31 definition |
32 is_forw_back_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
32 is_forw_back_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
33 "is_forw_back_simulation R C A = |
33 "is_forw_back_simulation R C A = |
34 ((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) & |
34 ((!s:starts_of C. ? S'. (s,S'):R & S'<= starts_of A) & |
35 (!s S' t a. reachable C s & |
35 (!s S' t a. reachable C s & |
36 s -a--C-> t & |
36 s \<midarrow>a\<midarrow>C\<rightarrow> t & |
37 (s,S') : R |
37 (s,S') : R |
38 --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))" |
38 --> (? T'. (t,T'):R & (! t':T'. ? s':S'. ? ex. move A ex s' a t'))))" |
39 |
39 |
40 definition |
40 definition |
41 is_back_forw_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
41 is_back_forw_simulation :: "[('s1 * 's2 set)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
42 "is_back_forw_simulation R C A = |
42 "is_back_forw_simulation R C A = |
43 ((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) & |
43 ((!s:starts_of C. ! S'. (s,S'):R --> S' Int starts_of A ~={}) & |
44 (!s t T' a. reachable C s & |
44 (!s t T' a. reachable C s & |
45 s -a--C-> t & |
45 s \<midarrow>a\<midarrow>C\<rightarrow> t & |
46 (t,T') : R |
46 (t,T') : R |
47 --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))" |
47 --> (? S'. (s,S'):R & (! s':S'. ? t':T'. ? ex. move A ex s' a t'))))" |
48 |
48 |
49 definition |
49 definition |
50 is_history_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |
50 is_history_relation :: "[('s1 * 's2)set,('a,'s1)ioa,('a,'s2)ioa] => bool" where |