-
Notifications
You must be signed in to change notification settings - Fork 82
/
ModelCheck.v
182 lines (155 loc) · 5.56 KB
/
ModelCheck.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
Require Import Invariant Relations Sets Classical.
Set Implicit Arguments.
Definition oneStepClosure_current {state} (sys : trsys state)
(invariant1 invariant2 : state -> Prop) :=
forall st, invariant1 st
-> invariant2 st.
Definition oneStepClosure_new {state} (sys : trsys state)
(invariant1 invariant2 : state -> Prop) :=
forall st st', invariant1 st
-> sys.(Step) st st'
-> invariant2 st'.
Definition oneStepClosure {state} (sys : trsys state)
(invariant1 invariant2 : state -> Prop) :=
oneStepClosure_current sys invariant1 invariant2
/\ oneStepClosure_new sys invariant1 invariant2.
Theorem prove_oneStepClosure : forall state (sys : trsys state) (inv1 inv2 : state -> Prop),
(forall st, inv1 st -> inv2 st)
-> (forall st st', inv1 st -> sys.(Step) st st' -> inv2 st')
-> oneStepClosure sys inv1 inv2.
Proof.
unfold oneStepClosure; tauto.
Qed.
Inductive multiStepClosure {state} (sys : trsys state)
: (state -> Prop) -> (state -> Prop) -> (state -> Prop) -> Prop :=
| MscDone : forall inv,
multiStepClosure sys inv (constant nil) inv
| MscStep : forall inv worklist inv' inv'',
oneStepClosure sys worklist inv'
-> multiStepClosure sys (inv \cup inv') (inv' \setminus inv) inv''
-> multiStepClosure sys inv worklist inv''.
Lemma adding_irrelevant : forall A (s : A) inv inv',
s \in (inv \cup inv') \setminus (inv' \setminus inv)
-> s \in inv.
Proof.
sets idtac.
destruct (classic (inv s)); tauto.
Qed.
Lemma multiStepClosure_ok' : forall state (sys : trsys state) (inv worklist inv' : state -> Prop),
multiStepClosure sys inv worklist inv'
-> (forall st, sys.(Initial) st -> inv st)
-> worklist \subseteq inv
-> (forall s, s \in inv \setminus worklist
-> forall s', sys.(Step) s s'
-> s' \in inv)
-> invariantFor sys inv'.
Proof.
induction 1; simpl; intuition.
apply invariant_induction; simpl; intuition.
eapply H1.
red.
unfold minus.
split; eauto.
assumption.
apply IHmultiStepClosure; clear IHmultiStepClosure.
intuition.
apply H1 in H4.
sets idtac.
sets idtac.
intuition.
apply adding_irrelevant in H4.
destruct (classic (s \in worklist)).
destruct H.
red in H7.
eapply H7 in H6.
right; eassumption.
assumption.
left.
eapply H3.
2: eassumption.
sets idtac.
Qed.
Theorem multiStepClosure_ok : forall state (sys : trsys state) (inv : state -> Prop),
multiStepClosure sys sys.(Initial) sys.(Initial) inv
-> invariantFor sys inv.
Proof.
intros; eapply multiStepClosure_ok'; eauto; sets idtac.
Qed.
Theorem oneStepClosure_empty : forall state (sys : trsys state),
oneStepClosure sys (constant nil) (constant nil).
Proof.
unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new; intuition.
Qed.
Theorem oneStepClosure_split : forall state (sys : trsys state) st sts (inv1 inv2 : state -> Prop),
(forall st', sys.(Step) st st' -> inv1 st')
-> oneStepClosure sys (constant sts) inv2
-> oneStepClosure sys (constant (st :: sts)) (constant (st :: nil) \cup inv1 \cup inv2).
Proof.
unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new; intuition.
inversion H0; subst.
unfold union; simpl; tauto.
unfold union; simpl; eauto.
unfold union in *; simpl in *.
intuition (subst; eauto).
Qed.
Theorem singleton_in : forall {A} (x : A) rest,
(constant (x :: nil) \cup rest) x.
Proof.
unfold union; simpl; auto.
Qed.
Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A),
s2 x
-> (s1 \cup s2) x.
Proof.
unfold union; simpl; auto.
Qed.
(** * Abstraction *)
Inductive simulates state1 state2 (R : state1 -> state2 -> Prop)
(sys1 : trsys state1) (sys2 : trsys state2) : Prop :=
| Simulates :
(forall st1, sys1.(Initial) st1
-> exists st2, R st1 st2
/\ sys2.(Initial) st2)
-> (forall st1 st2, R st1 st2
-> forall st1', sys1.(Step) st1 st1'
-> exists st2', R st1' st2'
/\ sys2.(Step) st2 st2')
-> simulates R sys1 sys2.
Inductive invariantViaSimulation state1 state2 (R : state1 -> state2 -> Prop)
(inv2 : state2 -> Prop)
: state1 -> Prop :=
| InvariantViaSimulation : forall st1 st2, R st1 st2
-> inv2 st2
-> invariantViaSimulation R inv2 st1.
Lemma invariant_simulates' : forall state1 state2 (R : state1 -> state2 -> Prop)
(sys1 : trsys state1) (sys2 : trsys state2),
(forall st1 st2, R st1 st2
-> forall st1', sys1.(Step) st1 st1'
-> exists st2', R st1' st2'
/\ sys2.(Step) st2 st2')
-> forall st1 st1', sys1.(Step)^* st1 st1'
-> forall st2, R st1 st2
-> exists st2', R st1' st2'
/\ sys2.(Step)^* st2 st2'.
Proof.
induction 2; simpl; intuition eauto.
eapply H in H2.
firstorder.
apply IHtrc in H2.
firstorder; eauto.
eauto.
Qed.
Local Hint Constructors invariantViaSimulation : core.
Theorem invariant_simulates : forall state1 state2 (R : state1 -> state2 -> Prop)
(sys1 : trsys state1) (sys2 : trsys state2) (inv2 : state2 -> Prop),
simulates R sys1 sys2
-> invariantFor sys2 inv2
-> invariantFor sys1 (invariantViaSimulation R inv2).
Proof.
inversion_clear 1; intros.
unfold invariantFor; intros.
apply H0 in H2.
firstorder.
apply invariant_simulates' with (sys2 := sys2) (R := R) (st2 := x) in H3; auto.
firstorder; eauto.
Qed.