Some heftier ModelChecking examples

This commit is contained in:
Adam Chlipala 2016-02-14 19:23:26 -05:00
parent eb50f67c2a
commit c129d8447e
3 changed files with 110 additions and 25 deletions

2
Frap.v
View file

@ -43,7 +43,7 @@ Ltac invert0 e := invert e; fail.
Ltac invert1 e := invert0 e || (invert e; []).
Ltac invert2 e := invert1 e || (invert e; [|]).
Ltac simplify := repeat progress (simpl in *; intros; try autorewrite with core in *);
Ltac simplify := repeat progress (simpl in *; intros; try autorewrite with core in *; repeat unifyTails);
repeat (removeDups || doSubtract).
Ltac propositional := intuition idtac.

View file

@ -146,13 +146,24 @@ Proof.
constructor.
Qed.
Theorem singleton_in : forall {A} (x : A),
{x} x.
Theorem singleton_in : forall {A} (x : A) rest,
({x} \cup rest) x.
Proof.
simplify.
left.
simplify.
equality.
Qed.
Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A),
s2 x
-> (s1 \cup s2) x.
Proof.
simplify.
right.
assumption.
Qed.
Theorem factorial_ok_2 :
invariantFor (factorial_sys 2) (fact_correct 2).
Proof.
@ -213,13 +224,19 @@ Ltac model_check_done :=
| [ H : _ |- _ ] => invert H
end; simplify; equality.
Ltac singletoner :=
repeat match goal with
| _ => apply singleton_in
| [ |- (_ \cup _) _ ] => apply singleton_in_other
end.
Ltac model_check_step :=
eapply MscStep; [
repeat ((apply oneStepClosure_empty; simplify)
|| (apply oneStepClosure_split; [ simplify;
repeat match goal with
| [ H : _ |- _ ] => invert H
end; apply singleton_in | ]))
end; solve [ singletoner ] | ]))
| simplify ].
Ltac model_check_steps1 := model_check_done || model_check_step.
@ -246,8 +263,8 @@ Proof.
model_check.
Qed.
Theorem factorial_ok_4 :
invariantFor (factorial_sys 4) (fact_correct 4).
Theorem factorial_ok_5 :
invariantFor (factorial_sys 5) (fact_correct 5).
Proof.
model_check.
Qed.
@ -255,21 +272,6 @@ Qed.
(** * Getting smarter about not exploring from the same state twice *)
(*Theorem oneStepClosure_new_done : forall state (sys : trsys state) (invariant : state -> Prop),
(forall st, sys.(Initial) st -> invariant st)
-> oneStepClosure_new sys invariant invariant
-> invariantFor sys invariant.
Proof.
unfold oneStepClosure_new.
propositional.
apply invariant_induction.
assumption.
simplify.
eapply H2.
eassumption.
assumption.
Qed.*)
Inductive multiStepClosure_smarter {state} (sys : trsys state)
: (state -> Prop) -> (state -> Prop) -> (state -> Prop) -> Prop :=
| MscsDone : forall inv worklist,
@ -383,21 +385,23 @@ Ltac smodel_check_done :=
Ltac smodel_check_step :=
eapply MscsStep; [
repeat ((apply oneStepClosure_new_empty; simplify)
repeat ((apply oneStepClosure_new_empty; solve [ simplify ])
|| (apply oneStepClosure_new_split; [ simplify;
repeat match goal with
| [ H : _ |- _ ] => invert H
end; apply singleton_in | ]))
end; solve [ singletoner ] | ]))
| simplify ].
Ltac smodel_check_steps1 := smodel_check_done || smodel_check_step.
Ltac smodel_check_steps := repeat smodel_check_steps1.
Ltac smodel_check_find_invariant :=
Ltac smodel_check_setup :=
simplify; eapply invariantFor_weaken; [
apply multiStepClosure_smarter_ok; simplify; smodel_check_steps
apply multiStepClosure_smarter_ok; simplify
| ].
Ltac smodel_check_find_invariant := smodel_check_setup; [ smodel_check_steps | ].
Ltac smodel_check := smodel_check_find_invariant; model_check_finish.
Theorem factorial_ok_2_smarter_snazzy :
@ -417,3 +421,73 @@ Theorem factorial_ok_5_smarter_snazzy :
Proof.
smodel_check.
Qed.
(** * Back to the multithreaded example from last time *)
Theorem increment2_init_is :
parallel1 increment_init increment_init = { {| Shared := {| Global := 0; Locked := false |};
Private := (Lock, Lock) |} }.
Proof.
simplify.
apply sets_equal; simplify.
propositional.
invert H.
invert H2.
invert H4.
equality.
rewrite <- H0.
constructor.
constructor.
constructor.
Qed.
Hint Rewrite increment2_init_is.
(*Theorem increment2_ok :
invariantFor increment2_sys increment2_right_answer.
Proof.
unfold increment2_right_answer.
smodel_check.
Qed.*)
Definition increment3_sys := parallel increment_sys increment2_sys.
Definition increment3_right_answer
(s : threaded_state inc_state (increment_program * (increment_program * increment_program))) :=
s.(Private) = (Done, (Done, Done))
-> s.(Shared).(Global) = 3.
Theorem increment3_init_is :
parallel1 increment_init (parallel1 increment_init increment_init)
= { {| Shared := {| Global := 0; Locked := false |};
Private := (Lock, (Lock, Lock)) |} }.
Proof.
simplify.
apply sets_equal; simplify.
propositional.
invert H.
invert H2.
invert H4.
equality.
invert H.
rewrite <- H0.
constructor.
constructor.
constructor.
constructor.
Qed.
Hint Rewrite increment3_init_is.
Theorem increment3_ok :
invariantFor increment3_sys increment3_right_answer.
Proof.
unfold increment3_right_answer.
smodel_check_find_invariant.
model_check_finish.
Qed.

11
Sets.v
View file

@ -238,3 +238,14 @@ Ltac doSubtract :=
|| (apply DsKeep; [ simpl; intuition congruence | ])
|| (apply DsDrop; [ simpl; intuition congruence | ]))
end.
(** Undetermined set variables in fixed points should be turned into the empty set. *)
Ltac unifyTails :=
match goal with
| [ |- context[_ \cup ?x] ] => is_evar x;
match type of x with
| set ?A => unify x (constant (@nil A))
| ?A -> Prop => unify x (constant (@nil A))
end
end.