diff options
| -rw-r--r-- | scheduling/BTLroadmap.md | 4 |
1 files changed, 3 insertions, 1 deletions
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 |