From ddacd030e6dfd2ef0a844574d1ee0a9b05ee413b Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Sun, 20 Feb 2022 12:02:38 -0500 Subject: [PATCH] Revising for Tuesday's lecture --- ModelChecking.v | 4 ++-- ModelChecking_template.v | 4 ++-- frap_book.tex | 2 -- 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/ModelChecking.v b/ModelChecking.v index 9367b4b..b510c6f 100644 --- a/ModelChecking.v +++ b/ModelChecking.v @@ -290,7 +290,7 @@ Qed. * states. Here is a definition of some tactics to do the work. * BEGIN CODE THAT WILL NOT BE EXPLAINED IN DETAIL! *) -Hint Rewrite fact_init_is. +Local Hint Rewrite fact_init_is. Ltac model_check_done := apply MscDone; apply prove_oneStepClosure; simplify; propositional; subst; @@ -607,7 +607,7 @@ Qed. (* We ask Coq to remember this lemma as a hint, which will be used by the * model-checking tactics that we refrain from explaining in detail. *) -Hint Rewrite add2_init_is. +Local Hint Rewrite add2_init_is. (* Now, let's verify the original system. *) Theorem add2_ok : diff --git a/ModelChecking_template.v b/ModelChecking_template.v index f4d91e9..2610d80 100644 --- a/ModelChecking_template.v +++ b/ModelChecking_template.v @@ -238,7 +238,7 @@ Qed. (* BEGIN CODE THAT WILL NOT BE EXPLAINED IN DETAIL! *) -Hint Rewrite fact_init_is. +Local Hint Rewrite fact_init_is. Ltac model_check_done := apply MscDone; apply prove_oneStepClosure; simplify; propositional; subst; @@ -508,7 +508,7 @@ Qed. (* We ask Coq to remember this lemma as a hint, which will be used by the * model-checking tactics that we refrain from explaining in detail. *) -Hint Rewrite add2_init_is. +Local Hint Rewrite add2_init_is. (* Now, let's verify the original system. *) Theorem add2_ok : diff --git a/frap_book.tex b/frap_book.tex index 409c69b..6941d00 100644 --- a/frap_book.tex +++ b/frap_book.tex @@ -1782,14 +1782,12 @@ For our purposes, the key pay-off from this connection is that we may translate We can apply this theorem to the two example programs from earlier in the section, now imagining that we run two parallel-thread copies of each program, using last chapter's approach to modeling threads with transition systems. The concrete system can be represented with thread-local states $\{\mathsf{Read}\} \cup \{\mathsf{Write}(n) \mid n \in \mathbb N\}$ and the abstract system with $\{\mathsf{BRead}\} \cup \{\mathsf{BWrite}(b) \mid b \in \mathbb B\}$, for the Booleans $\mathbb B$. We define compatibility between local states. - $$\infer{\mathsf{Read} \sim \mathsf{BRead}}{} \quad \infer{\mathsf{Write}(n) \sim \mathsf{BWrite}(b)}{ n \; \textrm{even} \Leftrightarrow b = \mathsf{true} }$$ We also define the overall state simulation relation $R$, which also covers state shared by threads. - $$\infer{(n, (\ell_1, \ell_2)) \; R \; (b, (\ell'_1, \ell'_2))}{ (n \; \textrm{even} \Leftrightarrow b = \mathsf{true}) & \ell_1 \sim \ell'_1