From 96c8e33777663aa79e3dc7bbf3860ee250f602d4 Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Thu, 24 Jul 2014 10:38:52 +0200
Subject: Experiment on dynamic partitionning (guarantee initial partition).

---
 doc/readme.pdf | Bin 263955 -> 263736 bytes
 doc/readme.tm  | 119 ++++++++++++++++++++++++++++++---------------------------
 2 files changed, 63 insertions(+), 56 deletions(-)

(limited to 'doc')

diff --git a/doc/readme.pdf b/doc/readme.pdf
index aa680ca..89e5d4e 100644
Binary files a/doc/readme.pdf and b/doc/readme.pdf differ
diff --git a/doc/readme.tm b/doc/readme.tm
index f21a66c..c6cde6d 100644
--- a/doc/readme.tm
+++ b/doc/readme.tm
@@ -1705,10 +1705,6 @@
   <subsection|Analyse des propriétés des nombres flottants>
 
   <\itemize>
-    <item>Implémenter un domaine d'intervalles permettant de gérer les
-    rationnels en précision arbitraire, ou se brancher sur le module Box
-    d'Apron
-
     <item>Utiliser un opérateur de widening aproprié (cf Astrée)
 
     <item>Implémenter la sémantique des nombres flottants machine (ce qui
@@ -1794,29 +1790,29 @@
     <associate|auto-3|<tuple|2.1|1>>
     <associate|auto-30|<tuple|5.2.3.3|?>>
     <associate|auto-31|<tuple|5.2.5.2|16>>
-    <associate|auto-32|<tuple|5.3|16>>
-    <associate|auto-33|<tuple|5.3.0.3|?>>
-    <associate|auto-34|<tuple|5.3.0.4|?>>
-    <associate|auto-35|<tuple|5.3.0.4.1|?>>
-    <associate|auto-36|<tuple|6|?>>
-    <associate|auto-37|<tuple|6.1|?>>
-    <associate|auto-38|<tuple|6.2|?>>
-    <associate|auto-39|<tuple|6.3|?>>
+    <associate|auto-32|<tuple|5.3|17>>
+    <associate|auto-33|<tuple|5.3.0.3|17>>
+    <associate|auto-34|<tuple|5.3.0.4|17>>
+    <associate|auto-35|<tuple|5.3.0.4.1|17>>
+    <associate|auto-36|<tuple|6|17>>
+    <associate|auto-37|<tuple|6.1|18>>
+    <associate|auto-38|<tuple|6.2|18>>
+    <associate|auto-39|<tuple|6.3|18>>
     <associate|auto-4|<tuple|2.2|2>>
-    <associate|auto-40|<tuple|6.3.1|?>>
-    <associate|auto-41|<tuple|6.3.1.1|?>>
-    <associate|auto-42|<tuple|6.3.1.2|?>>
-    <associate|auto-43|<tuple|6.3.2|?>>
-    <associate|auto-44|<tuple|6.3.2.1|?>>
-    <associate|auto-45|<tuple|6.3.2.2|?>>
-    <associate|auto-46|<tuple|6.3.3|?>>
-    <associate|auto-47|<tuple|6.3.3.1|?>>
-    <associate|auto-48|<tuple|6.3.3.2|?>>
-    <associate|auto-49|<tuple|7|?>>
+    <associate|auto-40|<tuple|6.3.1|18>>
+    <associate|auto-41|<tuple|6.3.1.1|18>>
+    <associate|auto-42|<tuple|6.3.1.2|18>>
+    <associate|auto-43|<tuple|6.3.2|19>>
+    <associate|auto-44|<tuple|6.3.2.1|19>>
+    <associate|auto-45|<tuple|6.3.2.2|19>>
+    <associate|auto-46|<tuple|6.3.3|19>>
+    <associate|auto-47|<tuple|6.3.3.1|19>>
+    <associate|auto-48|<tuple|6.3.3.2|19>>
+    <associate|auto-49|<tuple|7|19>>
     <associate|auto-5|<tuple|2.3|3>>
-    <associate|auto-50|<tuple|7.1|?>>
-    <associate|auto-51|<tuple|7.2|?>>
-    <associate|auto-52|<tuple|<with|mode|<quote|math>|\<bullet\>>|?>>
+    <associate|auto-50|<tuple|7.1|19>>
+    <associate|auto-51|<tuple|7.2|20>>
+    <associate|auto-52|<tuple|<with|mode|<quote|math>|\<bullet\>>|20>>
     <associate|auto-6|<tuple|2.3.1|3>>
     <associate|auto-7|<tuple|2.3.2|3>>
     <associate|auto-8|<tuple|2.3.3|3>>
@@ -1950,77 +1946,88 @@
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
       <no-break><pageref|auto-31><vspace|0.15fn>>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|6<space|2spc>Partitionnement
-      dynamique> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-32><vspace|0.5fn>
+      <with|par-left|<quote|1.5fn>|5.3<space|2spc>Partitionnement dynamique
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-32>>
+
+      <with|par-left|<quote|6fn>|Découpage de base.
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-33><vspace|0.15fn>>
+
+      <with|par-left|<quote|6fn>|Rafinement.
+      <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-34><vspace|0.15fn>>
+
+      Observations. <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
+      <no-break><pageref|auto-35><vspace|0.15fn>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|7<space|2spc>Implémentation>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|6<space|2spc>Implémentation>
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-33><vspace|0.5fn>
+      <no-break><pageref|auto-36><vspace|0.5fn>
 
-      <with|par-left|<quote|1.5fn>|7.1<space|2spc>Parsing et affichage de
+      <with|par-left|<quote|1.5fn>|6.1<space|2spc>Parsing et affichage de
       programmes SCADE <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-34>>
+      <no-break><pageref|auto-37>>
 
-      <with|par-left|<quote|1.5fn>|7.2<space|2spc>Interprète SCADE
+      <with|par-left|<quote|1.5fn>|6.2<space|2spc>Interprète SCADE
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-35>>
+      <no-break><pageref|auto-38>>
 
-      <with|par-left|<quote|1.5fn>|7.3<space|2spc>Analyse statique par
+      <with|par-left|<quote|1.5fn>|6.3<space|2spc>Analyse statique par
       interprétation abstraite <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-36>>
+      <no-break><pageref|auto-39>>
 
-      <with|par-left|<quote|3fn>|7.3.1<space|2spc>Domaine à disjonctions
+      <with|par-left|<quote|3fn>|6.3.1<space|2spc>Domaine à disjonctions
       simples <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-37>>
+      <no-break><pageref|auto-40>>
 
       <with|par-left|<quote|6fn>|Modes d'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-38><vspace|0.15fn>>
+      <no-break><pageref|auto-41><vspace|0.15fn>>
 
       <with|par-left|<quote|6fn>|Options de l'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-39><vspace|0.15fn>>
+      <no-break><pageref|auto-42><vspace|0.15fn>>
 
-      <with|par-left|<quote|3fn>|7.3.2<space|2spc>Domaine à disjonction par
+      <with|par-left|<quote|3fn>|6.3.2<space|2spc>Domaine à disjonction par
       graphe de décision <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-40>>
+      <no-break><pageref|auto-43>>
 
       <with|par-left|<quote|6fn>|Modes d'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-41><vspace|0.15fn>>
+      <no-break><pageref|auto-44><vspace|0.15fn>>
 
       <with|par-left|<quote|6fn>|Options de l'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-42><vspace|0.15fn>>
+      <no-break><pageref|auto-45><vspace|0.15fn>>
 
-      <with|par-left|<quote|3fn>|7.3.3<space|2spc>Analyse par partitionnement
+      <with|par-left|<quote|3fn>|6.3.3<space|2spc>Analyse par partitionnement
       dynamique <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-43>>
+      <no-break><pageref|auto-46>>
 
       <with|par-left|<quote|6fn>|Modes d'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-44><vspace|0.15fn>>
+      <no-break><pageref|auto-47><vspace|0.15fn>>
 
       <with|par-left|<quote|6fn>|Paramètres de l'analyse
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-45><vspace|0.15fn>>
+      <no-break><pageref|auto-48><vspace|0.15fn>>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|8<space|2spc>Prolongements
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|7<space|2spc>Prolongements
       envisageables> <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-46><vspace|0.5fn>
+      <no-break><pageref|auto-49><vspace|0.5fn>
 
-      <with|par-left|<quote|1.5fn>|8.1<space|2spc>Analyse des propriétés des
+      <with|par-left|<quote|1.5fn>|7.1<space|2spc>Analyse des propriétés des
       nombres flottants <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-47>>
+      <no-break><pageref|auto-50>>
 
-      <with|par-left|<quote|1.5fn>|8.2<space|2spc>Analyse de programmes \S
+      <with|par-left|<quote|1.5fn>|7.2<space|2spc>Analyse de programmes \S
       taille réelle \T <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-48>>
+      <no-break><pageref|auto-51>>
 
-      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|9<space|2spc>Références>
+      <vspace*|1fn><with|font-series|<quote|bold>|math-font-series|<quote|bold>|Références>
       <datoms|<macro|x|<repeat|<arg|x>|<with|font-series|medium|<with|font-size|1|<space|0.2fn>.<space|0.2fn>>>>>|<htab|5mm>>
-      <no-break><pageref|auto-49><vspace|0.5fn>
+      <no-break><pageref|auto-52><vspace|0.5fn>
     </associate>
   </collection>
 </auxiliary>
\ No newline at end of file
-- 
cgit v1.2.3