Add ModelCheck

This commit is contained in:
Adam Chlipala 2016-02-21 12:16:31 -05:00
parent 4d54fe8857
commit fd45f9d71a
5 changed files with 139 additions and 3 deletions

41
Frap.v
View file

@ -1,5 +1,5 @@
Require Import String Arith Omega Program Sets Relations Map Var Invariant Bool.
Export String Arith Sets Relations Map Var Invariant Bool.
Require Import String Arith Omega Program Sets Relations Map Var Invariant Bool ModelCheck.
Export String Arith Sets Relations Map Var Invariant Bool ModelCheck.
Require Import List.
Export List ListNotations.
Open Scope string_scope.
@ -89,3 +89,40 @@ Export Frap.Map.
Ltac maps_equal := Frap.Map.M.maps_equal; simplify.
Ltac first_order := firstorder idtac.
(** * Model checking *)
Ltac model_check_done :=
apply MscDone; apply prove_oneStepClosure; simplify; propositional; subst;
repeat match goal with
| [ 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; try congruence
end; solve [ singletoner ] | ]))
| simplify ].
Ltac model_check_steps1 := model_check_done || model_check_step.
Ltac model_check_steps := repeat model_check_steps1.
Ltac model_check_finish := simplify; propositional; subst; simplify; equality.
Ltac model_check_infer :=
apply multiStepClosure_ok; simplify; model_check_steps.
Ltac model_check_find_invariant :=
simplify; eapply invariant_weaken; [ model_check_infer | ]; cbv beta in *.
Ltac model_check := model_check_find_invariant; model_check_finish.

97
ModelCheck.v Normal file
View file

@ -0,0 +1,97 @@
Require Import Invariant Sets.
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.
Theorem oneStepClosure_done : forall state (sys : trsys state) (invariant : state -> Prop),
(forall st, sys.(Initial) st -> invariant st)
-> oneStepClosure sys invariant invariant
-> invariantFor sys invariant.
Proof.
unfold oneStepClosure, oneStepClosure_current, oneStepClosure_new.
intuition eauto using invariant_induction.
Qed.
Inductive multiStepClosure {state} (sys : trsys state)
: (state -> Prop) -> (state -> Prop) -> Prop :=
| MscDone : forall inv,
oneStepClosure sys inv inv
-> multiStepClosure sys inv inv
| MscStep : forall inv inv' inv'',
oneStepClosure sys inv inv'
-> multiStepClosure sys inv' inv''
-> multiStepClosure sys inv inv''.
Lemma multiStepClosure_ok' : forall state (sys : trsys state) (inv inv' : state -> Prop),
multiStepClosure sys inv inv'
-> (forall st, sys.(Initial) st -> inv st)
-> invariantFor sys inv'.
Proof.
induction 1; simpl; intuition eauto using oneStepClosure_done.
unfold oneStepClosure, oneStepClosure_current in *.
intuition eauto.
Qed.
Theorem multiStepClosure_ok : forall state (sys : trsys state) (inv : state -> Prop),
multiStepClosure sys sys.(Initial) inv
-> invariantFor sys inv.
Proof.
eauto using multiStepClosure_ok'.
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)) ({st} \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,
({x} \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.

View file

@ -103,7 +103,7 @@ Proof.
apply IHmultiStepClosure.
simplify.
unfold oneStepClosure, oneStepClosure_current in *. (* <-- *)
unfold oneStepClosure, oneStepClosure_current in *.
propositional.
apply H3.
apply H1.

View file

@ -9,3 +9,4 @@ Just run `make` here to build everything, including the book `frap.pdf` and the
* Chapter 2: `BasicSyntax.v`
* Chapter 3: `Interpreters.v`
* Chapter 4: `TransitionSystems.v`
* Chapter 5: `ModelChecking.v`

View file

@ -4,6 +4,7 @@ Var.v
Sets.v
Relations.v
Invariant.v
ModelCheck.v
Frap.v
BasicSyntax_template.v
BasicSyntax.v