From: SeongJae Park <sj38.park@xxxxxxxxx>
A sentence is calling 'Fail1:' label as 'Fail:'. Fix it.
Signed-off-by: SeongJae Park <sj38.park@xxxxxxxxx>
---
formal/ppcmem.tex | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/formal/ppcmem.tex b/formal/ppcmem.tex
index 181ca7c6..10526bca 100644
--- a/formal/ppcmem.tex
+++ b/formal/ppcmem.tex
@@ -209,7 +209,7 @@ and \clnref{P1lwz} is equivalent to the C statement \co{r3=x}.
by setting non-zero status in the condition-code register,
which in turn is tested by the \co{bne} instruction.
Because actually modeling the loop would result in state-space
- explosion, we instead branch to the \co{Fail:} label,
+ explosion, we instead branch to the \co{Fail1:} label,
terminating the model with the initial value of~2 in P0's \co{r3}
register, which will not trigger the exists assertion.
--
2.17.1
