equal
deleted
inserted
replaced
9 CompoTraces = CompoScheds + ShortExecutions + |
9 CompoTraces = CompoScheds + ShortExecutions + |
10 |
10 |
11 |
11 |
12 consts |
12 consts |
13 |
13 |
14 mksch ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" |
14 mksch ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" |
15 |
15 par_traces ::"['a trace_module,'a trace_module] => 'a trace_module" |
16 |
16 |
17 defs |
17 defs |
18 |
18 |
19 mksch_def |
19 mksch_def |
20 "mksch A B == (fix`(LAM h tr schA schB. case tr of |
20 "mksch A B == (fix`(LAM h tr schA schB. case tr of |
49 ) |
49 ) |
50 ) |
50 ) |
51 )))" |
51 )))" |
52 |
52 |
53 |
53 |
|
54 par_traces_def |
|
55 "par_traces TracesA TracesB == |
|
56 let trA = fst TracesA; sigA = snd TracesA; |
|
57 trB = fst TracesB; sigB = snd TracesB |
|
58 in |
|
59 ( {tr. Filter (%a.a:actions sigA)`tr : trA} |
|
60 Int {tr. Filter (%a.a:actions sigB)`tr : trB} |
|
61 Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr}, |
|
62 asig_comp sigA sigB)" |
|
63 |
54 rules |
64 rules |
55 |
65 |
56 |
66 |
57 finiteR_mksch |
67 finiteR_mksch |
58 "Finite (mksch A B`tr`x`y) --> Finite tr" |
68 "Finite (mksch A B`tr`x`y) --> Finite tr" |
59 |
69 |
60 |
70 |
61 |
71 |
62 end |
72 end |
63 |
|
64 |
|