12 datatype ('a)act = S('a) | R('a) |
12 datatype ('a)act = S('a) | R('a) |
13 |
13 |
14 |
14 |
15 consts |
15 consts |
16 |
16 |
17 ch_asig :: "'a act signature" |
17 ch_asig :: 'a act signature |
18 ch_trans :: "('a act, 'a list)transition set" |
18 ch_trans :: ('a act, 'a list)transition set |
19 ch_ioa :: "('a act, 'a list)ioa" |
19 ch_ioa :: ('a act, 'a list)ioa |
20 |
20 |
21 rsch_actions :: "'m action => bool act option" |
21 rsch_actions :: 'm action => bool act option |
22 srch_actions :: "'m action =>(bool * 'm) act option" |
22 srch_actions :: "'m action =>(bool * 'm) act option" |
23 |
23 |
24 srch_asig, |
24 srch_asig, |
25 rsch_asig :: "'m action signature" |
25 rsch_asig :: 'm action signature |
26 |
26 |
27 srch_trans :: "('m action, 'm packet list)transition set" |
27 srch_trans :: ('m action, 'm packet list)transition set |
28 rsch_trans :: "('m action, bool list)transition set" |
28 rsch_trans :: ('m action, bool list)transition set |
29 |
29 |
30 srch_ioa :: "('m action, 'm packet list)ioa" |
30 srch_ioa :: ('m action, 'm packet list)ioa |
31 rsch_ioa :: "('m action, bool list)ioa" |
31 rsch_ioa :: ('m action, bool list)ioa |
32 |
32 |
33 |
33 |
34 defs |
34 defs |
35 |
35 |
36 srch_asig_def "srch_asig == asig_of(srch_ioa)" |
36 srch_asig_def "srch_asig == asig_of(srch_ioa)" |