pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-09-19 19:57:13 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix up ModelChecking to track a change in TransitionSystems

Browse source
This commit is contained in:
Adam Chlipala 2018-03-04 18:46:12 -05:00
parent a501f5e1ec
commit b0ad93e6a4
2 changed files with 26 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

26
ModelChecking.v
View file

@ -582,7 +582,7 @@ Inductive add2_R : threaded_state nat (add2_thread * add2_thread)
(* Let's also recharacterize the initial states via a singleton set. *)
Theorem add2_init_is :
parallel1 add2_binit add2_binit = { {| Shared := true; Private := (BRead, BRead) |} }.
parallel_init add2_binit add2_binit = { {| Shared := true; Private := (BRead, BRead) |} }.
Proof.
simplify.
apply sets_equal; simplify.
@ -1054,7 +1054,7 @@ Qed.
* intimidating statement and a much more interesting proof, whose details we
* nonetheless won't comment on in text. It may make sense to skip past the
* next two lemma statements to the main theorem [withInterference_parallel]. *)
Lemma withInterference_parallel1 : forall shared private1 private2
Lemma withInterference_parallel_init : forall shared private1 private2
(invs : shared -> Prop)
(sys1 : trsys (threaded_state shared private1))
(sys2 : trsys (threaded_state shared private2))
@ -1149,11 +1149,11 @@ Proof.
constructor.
Qed.
Lemma withInterference_parallel2 : forall shared private1 private2
(invs : shared -> Prop)
(sys1 : trsys (threaded_state shared private1))
(sys2 : trsys (threaded_state shared private2))
st st',
Lemma withInterference_parallel_step : forall shared private1 private2
(invs : shared -> Prop)
(sys1 : trsys (threaded_state shared private1))
(sys2 : trsys (threaded_state shared private2))
st st',
(withInterference invs (parallel sys1 sys2)).(Step)^* st st'
-> forall st1 st2,
(forall st1', (withInterference invs sys1).(Step)^* st1 st1' -> invs st1'.(Shared))
@ -1268,9 +1268,9 @@ Proof.
assert ((withInterference invs sys1).(Step)^*
{| Shared := sh; Private := pr1 |}
{| Shared := s'.(Shared); Private := fst s'.(Private) |}).
apply withInterference_parallel1 with (sys2 := sys2)
(st := {| Shared := sh; Private := (pr1, pr2) |})
(st2 := {| Shared := sh; Private := pr2 |});
apply withInterference_parallel_init with (sys2 := sys2)
(st := {| Shared := sh; Private := (pr1, pr2) |})
(st2 := {| Shared := sh; Private := pr2 |});
simplify; propositional.
apply H in H1; propositional.
apply H0 in H1; propositional.
@ -1280,9 +1280,9 @@ Proof.
assert ((withInterference invs sys2).(Step)^*
{| Shared := sh; Private := pr2 |}
{| Shared := s'.(Shared); Private := snd s'.(Private) |}).
apply withInterference_parallel2 with (sys1 := sys1)
(st := {| Shared := sh; Private := (pr1, pr2) |})
(st1 := {| Shared := sh; Private := pr1 |});
apply withInterference_parallel_step with (sys1 := sys1)
(st := {| Shared := sh; Private := (pr1, pr2) |})
(st1 := {| Shared := sh; Private := pr1 |});
simplify; propositional.
apply H in H5; propositional.
apply H0 in H5; propositional.

26
ModelChecking_template.v
View file

@ -466,7 +466,7 @@ Inductive add2_R : threaded_state nat (add2_thread * add2_thread)
(* Let's also recharacterize the initial states via a singleton set. *)
Theorem add2_init_is :
parallel1 add2_binit add2_binit = { {| Shared := true; Private := (BRead, BRead) |} }.
parallel_init add2_binit add2_binit = { {| Shared := true; Private := (BRead, BRead) |} }.
Proof.
simplify.
apply sets_equal; simplify.
@ -925,7 +925,7 @@ Proof.
equality.
Qed.
Lemma withInterference_parallel1 : forall shared private1 private2
Lemma withInterference_parallel_init : forall shared private1 private2
(invs : shared -> Prop)
(sys1 : trsys (threaded_state shared private1))
(sys2 : trsys (threaded_state shared private2))
@ -1020,11 +1020,11 @@ Proof.
constructor.
Qed.
Lemma withInterference_parallel2 : forall shared private1 private2
(invs : shared -> Prop)
(sys1 : trsys (threaded_state shared private1))
(sys2 : trsys (threaded_state shared private2))
st st',
Lemma withInterference_parallel_step : forall shared private1 private2
(invs : shared -> Prop)
(sys1 : trsys (threaded_state shared private1))
(sys2 : trsys (threaded_state shared private2))
st st',
(withInterference invs (parallel sys1 sys2)).(Step)^* st st'
-> forall st1 st2,
(forall st1', (withInterference invs sys1).(Step)^* st1 st1' -> invs st1'.(Shared))
@ -1133,9 +1133,9 @@ Proof.
assert ((withInterference invs sys1).(Step)^*
{| Shared := sh; Private := pr1 |}
{| Shared := s'.(Shared); Private := fst s'.(Private) |}).
apply withInterference_parallel1 with (sys2 := sys2)
(st := {| Shared := sh; Private := (pr1, pr2) |})
(st2 := {| Shared := sh; Private := pr2 |});
apply withInterference_parallel_init with (sys2 := sys2)
(st := {| Shared := sh; Private := (pr1, pr2) |})
(st2 := {| Shared := sh; Private := pr2 |});
simplify; propositional.
apply H in H1; propositional.
apply H0 in H1; propositional.
@ -1145,9 +1145,9 @@ Proof.
assert ((withInterference invs sys2).(Step)^*
{| Shared := sh; Private := pr2 |}
{| Shared := s'.(Shared); Private := snd s'.(Private) |}).
apply withInterference_parallel2 with (sys1 := sys1)
(st := {| Shared := sh; Private := (pr1, pr2) |})
(st1 := {| Shared := sh; Private := pr1 |});
apply withInterference_parallel_step with (sys1 := sys1)
(st := {| Shared := sh; Private := (pr1, pr2) |})
(st1 := {| Shared := sh; Private := pr1 |});
simplify; propositional.
apply H in H5; propositional.
apply H0 in H5; propositional.