author | paulson |
Mon, 23 Jun 1997 10:42:03 +0200 | |
changeset 3457 | a8ab7c64817c |
parent 3433 | 2de17c994071 |
child 3521 | bdc51b4c6050 |
permissions | -rw-r--r-- |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
1 |
(* Title: HOLCF/IOA/meta_theory/Deadlock.ML |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
3 |
Author: Olaf Mueller |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
4 |
Copyright 1997 TU Muenchen |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
5 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
6 |
Deadlock freedom of I/O Automata |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
7 |
*) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
8 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
9 |
(******************************************************************************** |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
10 |
input actions may always be added to a schedule |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
11 |
**********************************************************************************) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
12 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
13 |
goal thy "!! sch. [| Filter (%x.x:act A)`sch : schedules A; a:inp A; IOA A; Finite sch|] \ |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
14 |
\ ==> Filter (%x.x:act A)`sch @@ a>>nil : schedules A"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
15 |
by (asm_full_simp_tac (!simpset addsimps [schedules_def,has_schedule_def]) 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
16 |
by (safe_tac set_cs); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
17 |
by (forward_tac [inp_is_act] 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
18 |
by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
19 |
by (pair_tac "ex" 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
20 |
ren "sch s ex" 1; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
21 |
by (subgoal_tac "Finite ex" 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
22 |
by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 2); |
3457 | 23 |
by (rtac (Map2Finite RS iffD1) 2); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
24 |
by (res_inst_tac [("t","Map fst`ex")] subst 2); |
3457 | 25 |
by (assume_tac 2); |
26 |
by (etac FiniteFilter 2); |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
27 |
(* subgoal 1 *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
28 |
by (forward_tac [exists_laststate] 1); |
3457 | 29 |
by (etac allE 1); |
30 |
by (etac exE 1); |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
31 |
(* using input-enabledness *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
32 |
by (asm_full_simp_tac (!simpset addsimps [ioa_def,input_enabled_def]) 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
33 |
by (REPEAT (etac conjE 1)); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
34 |
by (eres_inst_tac [("x","a")] allE 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
35 |
by (Asm_full_simp_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
36 |
by (eres_inst_tac [("x","u")] allE 1); |
3457 | 37 |
by (etac exE 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
38 |
(* instantiate execution *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
39 |
by (res_inst_tac [("x","(s,ex @@ (a,s2)>>nil)")] exI 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
40 |
by (asm_full_simp_tac (!simpset addsimps [filter_act_def,MapConc]) 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
41 |
by (eres_inst_tac [("t","u")] lemma_2_1 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
42 |
by (Asm_full_simp_tac 1); |
3457 | 43 |
by (rtac sym 1); |
44 |
by (assume_tac 1); |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
45 |
qed"scheds_input_enabled"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
46 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
47 |
(******************************************************************************** |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
48 |
Deadlock freedom: component B cannot block an out or int action |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
49 |
of component A in every schedule |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
50 |
Needs compositionality on schedule level, input-enabledness, compatibility |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
51 |
and distributivity of is_exec_frag over @@ |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
52 |
**********************************************************************************) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
53 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
54 |
goal thy "!! sch. [| a : local A; Finite sch; sch : schedules (A||B); \ |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
55 |
\ Filter (%x.x:act A)`(sch @@ a>>nil) : schedules A; compatible A B; IOA B |] \ |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
56 |
\ ==> (sch @@ a>>nil) : schedules (A||B)"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
57 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
58 |
by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1); |
3457 | 59 |
by (rtac conjI 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
60 |
(* a : act (A||B) *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
61 |
by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 2); |
3457 | 62 |
by (rtac disjI1 2); |
63 |
by (etac disjE 2); |
|
64 |
by (etac int_is_act 2); |
|
65 |
by (etac out_is_act 2); |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
66 |
(* Filter B (sch@@[a]) : schedules B *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
67 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
68 |
by (case_tac "a:int A" 1); |
3457 | 69 |
by (dtac intA_is_not_actB 1); |
70 |
by (assume_tac 1); (* --> a~:act B *) |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
71 |
by (Asm_full_simp_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
72 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
73 |
(* case a~:int A , i.e. a:out A *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
74 |
by (case_tac "a~:act B" 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
75 |
by (Asm_full_simp_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
76 |
(* case a:act B *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
77 |
by (Asm_full_simp_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
78 |
by (subgoal_tac "a:out A" 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
79 |
by (Fast_tac 2); |
3457 | 80 |
by (dtac outAactB_is_inpB 1); |
81 |
by (assume_tac 1); |
|
82 |
by (assume_tac 1); |
|
83 |
by (rtac scheds_input_enabled 1); |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
84 |
by (Asm_full_simp_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
85 |
by (REPEAT (atac 1)); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
86 |
qed"IOA_deadlock_free"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
87 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
88 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
89 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
90 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
91 |