From f855402a10148047e449073ae6c32d269275cdf4 Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Sun, 6 Jun 2021 20:32:28 +0200
Subject: m

---
 scheduling/BTLroadmap.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'scheduling/BTLroadmap.md')

diff --git a/scheduling/BTLroadmap.md b/scheduling/BTLroadmap.md
index bfbc1e03..9dd21be9 100644
--- a/scheduling/BTLroadmap.md
+++ b/scheduling/BTLroadmap.md
@@ -393,7 +393,9 @@ exécution symbolique que le bloc `ib1` est simulé par `ib2` modulo
 `TRANSFER` sur l'entrée `pc` se ramène à montrer `ib1[TRANSFER]` avec
 `TRANSFER(pc); ib2` pour la simulation symbolique usuelle.
  
- Ci-dessus `ib1[TRANSFER]` dit qu'on a appliqué `TRANSFER(pc')` sur chacune des sorties `pc'` de `ib1`.
+Ci-dessus `ib1[TRANSFER]` dit qu'on a appliqué `TRANSFER(pc')` sur chacune des sorties `pc'` de `ib1`.
+
+**REM** pour que ce soit correct, il faut sans doute vérifier une condition du style `ok(ib1) => ok(ib1[TRANSFER])`...
 
 ## Support of SSA-optimizations
 
-- 
cgit