summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlex Auvolat <alex.auvolat@ansys.com>2014-07-24 10:38:52 +0200
committerAlex Auvolat <alex.auvolat@ansys.com>2014-07-24 10:38:52 +0200
commit96c8e33777663aa79e3dc7bbf3860ee250f602d4 (patch)
treec014035e7ab641142159769979095eb6b0faafa7
parent6742003891028d566edf23dc7092c34f6d40255f (diff)
downloadscade-analyzer-96c8e33777663aa79e3dc7bbf3860ee250f602d4.tar.gz
scade-analyzer-96c8e33777663aa79e3dc7bbf3860ee250f602d4.zip
Experiment on dynamic partitionning (guarantee initial partition).
-rw-r--r--abstract/abs_interp_dynpart.ml77
-rw-r--r--doc/readme.pdfbin263955 -> 263736 bytes
-rw-r--r--doc/readme.tm119
3 files changed, 98 insertions, 98 deletions
diff --git a/abstract/abs_interp_dynpart.ml b/abstract/abs_interp_dynpart.ml
index 23df612..2ff950a 100644
--- a/abstract/abs_interp_dynpart.ml
+++ b/abstract/abs_interp_dynpart.ml
@@ -228,48 +228,41 @@ end = struct
loc = Hashtbl.create 2; counter = ref 2; } in
(* add initial disjunction : L/must_reset = tt, L/must_reset ≠ tt *)
- let rstc = BEnumCons(E_EQ, "L/must_reset", EItem bool_true) in
- let rstf = simplify_k [rstc] f in
- let rstf = simplify_k (get_root_true rstf) rstf in
- let nrstc = BEnumCons(E_NE, "L/must_reset", EItem bool_true) in
- let nrstf = simplify_k [nrstc] f in
- let nrstf = simplify_k (get_root_true nrstf) nrstf in
- Hashtbl.add env.loc 0
- {
- id = 0;
- depth = 0;
- def = apply_cl (top env) (conslist_of_f rstc);
- is_init = true;
-
- f = rstf;
- cl = conslist_of_f rstf;
-
- in_c = 0;
- v = bottom env;
-
- out_t = [];
- in_t = [];
- verif_g = [];
- violate_g = [];
- };
- Hashtbl.add env.loc 1
- {
- id = 1;
- depth = 0;
- def = apply_cl (top env) (conslist_of_f nrstc);
- is_init = false;
-
- f = nrstf;
- cl = conslist_of_f nrstf;
-
- in_c = 0;
- v = bottom env;
-
- out_t = [];
- in_t = [];
- verif_g = [];
- violate_g = [];
- };
+ let id = let i = ref 0 in fun () -> (incr i; !i) in
+ let add_loc is_init conds =
+ let cf = simplify_k conds f in
+ let cf = simplify_k (get_root_true cf) cf in
+ let id = id() in
+ Hashtbl.add env.loc id
+ {
+ id;
+ depth = 0;
+ def = apply_cl (top env) (conslist_of_f cf);
+ is_init;
+
+ f = cf;
+ cl = conslist_of_f cf;
+
+ in_c = 0;
+ v = bottom env;
+
+ out_t = [];
+ in_t = [];
+ verif_g = [];
+ violate_g = [];
+ };
+ in
+
+ add_loc true [BEnumCons(E_EQ, "L/must_reset", EItem bool_true)];
+
+ let rec div_g conds = function
+ | [] -> add_loc false conds
+ | (_, _, v)::r ->
+ add_loc false ((BEnumCons(E_NE, v, EItem bool_true))::conds);
+ div_g ((BEnumCons(E_EQ, v, EItem bool_true))::conds) r
+ in
+ div_g [BEnumCons(E_NE, "L/must_reset", EItem bool_true)] env.guarantees;
+
env
diff --git a/doc/readme.pdf b/doc/readme.pdf
index aa680ca..89e5d4e 100644
--- a/doc/readme.pdf
+++ b/doc/readme.pdf
Binary files 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