pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Tweak model-checking library support

Browse source
This commit is contained in:
Adam Chlipala 2016-02-21 17:00:01 -05:00
parent d677f255c4
commit 65c56a7a2e
2 changed files with 71 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
Frap.v
View file

@ -96,8 +96,11 @@ Ltac first_order := firstorder idtac.
Ltac model_check_done :=
apply MscDone; apply prove_oneStepClosure; simplify; propositional; subst;
repeat match goal with
| [ H : _ |- _ ] => invert H
end; simplify; equality.
| [ H : ?P |- _ ] =>
match type of P with
| Prop => invert H; simplify
end
end; equality.
Ltac singletoner :=
repeat match goal with
@ -110,7 +113,10 @@ Ltac model_check_step :=
repeat (apply oneStepClosure_empty
|| (apply oneStepClosure_split; [ simplify;
repeat match goal with
| [ H : _ |- _ ] => invert H; simplify; try congruence
| [ H : ?P |- _ ] =>
match type of P with
| Prop => invert H; simplify; try congruence
end
end; solve [ singletoner ] | ]))
| simplify ].

63
ModelCheck.v
View file

@ -1,4 +1,7 @@
Require Import Invariant Sets.
Require Import Invariant Relations Sets.
Set Implicit Arguments.
Definition oneStepClosure_current {state} (sys : trsys state)
(invariant1 invariant2 : state -> Prop) :=
@ -95,3 +98,61 @@ Theorem singleton_in_other : forall {A} (x : A) (s1 s2 : set A),
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.
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.