equal
deleted
inserted
replaced
48 Deadlock freedom: component B cannot block an out or int action |
48 Deadlock freedom: component B cannot block an out or int action |
49 of component A in every schedule. |
49 of component A in every schedule. |
50 Needs compositionality on schedule level, input-enabledness, compatibility |
50 Needs compositionality on schedule level, input-enabledness, compatibility |
51 and distributivity of is_exec_frag over @@ |
51 and distributivity of is_exec_frag over @@ |
52 **********************************************************************************) |
52 **********************************************************************************) |
53 Delsplits [expand_if]; |
53 Delsplits [split_if]; |
54 goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \ |
54 goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \ |
55 \ Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \ |
55 \ Filter (%x. x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \ |
56 \ ==> (sch @@ a>>nil) : schedules (A||B)"; |
56 \ ==> (sch @@ a>>nil) : schedules (A||B)"; |
57 |
57 |
58 by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,locals_def]) 1); |
58 by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,locals_def]) 1); |
81 by (rtac scheds_input_enabled 1); |
81 by (rtac scheds_input_enabled 1); |
82 by (Asm_full_simp_tac 1); |
82 by (Asm_full_simp_tac 1); |
83 by (REPEAT (atac 1)); |
83 by (REPEAT (atac 1)); |
84 qed"IOA_deadlock_free"; |
84 qed"IOA_deadlock_free"; |
85 |
85 |
86 Addsplits [expand_if]; |
86 Addsplits [split_if]; |
87 |
87 |
88 |
88 |
89 |
89 |
90 |
90 |