Skip to content

GitLab

Commit 9d1241f6 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.40 Thu, 07 Mar 2002 16:26:47 +0100 by jahier 

Parent-Version:      0.39
Version-Log:

Change the naming convention of prevars. Now, _pretoto is noted
_pre1toto, and _pre_pre_pretoto is noted _pre3toto.

Also fix a bug in the default initialization of ranges : min_float
is the smallest positive float, not the smallet one !!

Project-Description: Lurette
parent 4579cc26
Hide whitespace changes
Inline Side-by-side
.lurette.prcs_aux
View file @ 9d1241f6
......@@ -5,29 +5,29 @@
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 2871 1015504587 51_env_state. 1.13)
(source/graph.ml 1801 1015250295 14_graph.ml 1.4)
(source/util.ml 9430 1015250295 35_util.ml 1.12)
(source/util.ml 10405 1015514807 35_util.ml 1.13)
(source/wtree.ml 9644 1014051154 b/1_wtree.ml 1.8)
(source/solver.ml 14080 1015504587 39_solver.ml 1.14)
(source/solver.ml 14068 1015514807 39_solver.ml 1.15)
(source/command_line.ml 3971 1014048376 b/20_command_li 1.3)
(source/lurette.ml 11363 1015504587 12_lurette.ml 1.25)
(source/solver.mli 1059 1015250295 38_solver.mli 1.9)
(source/env.mli 2389 1015250295 15_env.mli 1.9)
(test/heater_float.rif.exp 1577 1015408234 b/30_heater_flo 1.1)
(test/heater_float.rif.exp 1461 1015514807 b/30_heater_flo 1.2)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(source/env.ml 8395 1015408234 16_env.ml 1.16)
(source/env.ml 9370 1015514807 16_env.ml 1.17)
(make_lurette 812 1013517738 27_make_luret 1.7)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(test/passerelle.env 866 1015408234 b/17_passerelle 1.2)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/rnumsolver.ml 7434 1015408234 b/27_rnumsolver 1.2)
(source/rnumsolver.ml 7438 1015514807 b/27_rnumsolver 1.3)
(source/parse_env.mli 905 1015408234 40_parse_env. 1.5)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(source/sim2chro.mli 1427 1015250295 b/23_sim2chro.m 1.3)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7990 1015504587 49_eval.ml 1.9)
(source/eval.ml 8273 1015514807 49_eval.ml 1.10)
(source/gen_stubs.ml 33424 1015408234 24_generate_l 1.19)
(source/parse_env.ml 9431 1015408234 41_parse_env. 1.6)
(source/parse_env.ml 9431 1015514807 41_parse_env. 1.7)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(source/sim2chro.ml 2669 1015408234 b/24_sim2chro.m 1.4)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
......@@ -51,7 +51,7 @@
(interface/Makefile 197 1008255910 25_Makefile 1.6)
(source/show_env.mli 765 1015250295 42_show_env.m 1.5)
(test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
(Makefile 1756 1015504587 18_Makefile 1.22)
(Makefile 1758 1015514807 18_Makefile 1.23)
(test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
(source/print.mli 597 1014048376 46_print.mli 1.5)
(source/graph.mli 1493 1015250295 13_graph.mli 1.6)
......
Makefile
View file @ 9d1241f6
......@@ -2,7 +2,7 @@ LURETTE_DIR = ..
OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
OCAMLFLAGS = -noassert -unsafe
# OCAMLFLAGS = -noassert -unsafe
OCAMLNCFLAGS = -inline 10
-include ./lurette.in
......
lurette.prj
View file @ 9d1241f6
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 39)
(Parent-Version lurette 0 38)
(Version-Log "
Use the new cudd interface based on camlidl (mlcuddidl).
(Project-Version lurette 0 40)
(Parent-Version lurette 0 39)
(Version-Log "
Change the naming convention of prevars. Now, _pretoto is noted
_pre1toto, and _pre_pre_pretoto is noted _pre3toto.
Also fix a bug in the default initialization of ranges : min_float
is the smallest positive float, not the smallet one !!
Now, bdds do not leaks anymore. Remove debugging stuff that was used
to track that problem.
")
(New-Version-Log "")
(Checkin-Time "Thu, 07 Mar 2002 13:36:27 +0100")
(Checkin-Time "Thu, 07 Mar 2002 16:26:47 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -29,18 +31,18 @@ to track that problem.
(source/graph.ml (lurette/14_graph.ml 1.4 644))
(source/env.mli (lurette/15_env.mli 1.9 644))
(source/env.ml (lurette/16_env.ml 1.16 644))
(source/env.ml (lurette/16_env.ml 1.17 644))
(source/util.ml (lurette/35_util.ml 1.12 644))
(source/util.ml (lurette/35_util.ml 1.13 644))
(source/solver.mli (lurette/38_solver.mli 1.9 644))
(source/solver.ml (lurette/39_solver.ml 1.14 644))
(source/solver.ml (lurette/39_solver.ml 1.15 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.1 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.2 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.3 644))
(source/parse_env.mli (lurette/40_parse_env. 1.5 644))
(source/parse_env.ml (lurette/41_parse_env. 1.6 644))
(source/parse_env.ml (lurette/41_parse_env. 1.7 644))
(source/show_env.mli (lurette/42_show_env.m 1.5 644))
(source/show_env.ml (lurette/43_show_env.m 1.3 644))
......@@ -52,7 +54,7 @@ to track that problem.
(source/print.ml (lurette/47_print.ml 1.10 644))
(source/eval.mli (lurette/48_eval.mli 1.7 644))
(source/eval.ml (lurette/49_eval.ml 1.9 644))
(source/eval.ml (lurette/49_eval.ml 1.10 644))
(source/env_state.mli (lurette/50_env_state. 1.11 644))
(source/env_state.ml (lurette/51_env_state. 1.13 644))
......@@ -70,7 +72,7 @@ to track that problem.
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.20 644))
(Makefile (lurette/18_Makefile 1.22 644))
(Makefile (lurette/18_Makefile 1.23 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.7 744))
......@@ -109,7 +111,7 @@ to track that problem.
(test/heater_int.rif.exp (lurette/b/28_heater_int 1.1 644))
(test/ControleurPorte.rif.exp (lurette/b/29_Controleur 1.1 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.1 644))
(test/heater_float.rif.exp (lurette/b/30_heater_flo 1.2 644))
)
......
source/env.ml
View file @ 9d1241f6
......@@ -19,8 +19,33 @@ open Env_state
(****************************************************************************)
(****************************************************************************)
(* read_env_state *)
let rec (add_missing_pre: string list -> string list) =
(* Even if the automata contains "_pre3toto", we need to store
"_pre2toto", and "_pre1toto". Thefore we add them here to the
list of pre vars declared in the automata thanks to this
function. *)
fun vnl ->
List.fold_left (add_missing_pre_acc) [] vnl
and
(add_missing_pre_acc: string list -> string -> string list) =
fun acc pren_vn ->
let (n, vn) = Util.split_pre_var_string pren_vn in
let rec (build_list_pre : string list -> int -> string -> string list) =
fun acc i str ->
let prei_str = ("_pre" ^ (string_of_int i) ^ str) in
if i = 1
then prei_str::acc
else build_list_pre (prei_str::acc) (i-1) str
in
Util.merge (build_list_pre [] n vn) acc
let _ = assert ( (add_missing_pre ["_pre3toto"; "_pre2titi"; "_pre2toto"])
= ["_pre2titi"; "_pre1titi"; "_pre3toto"; "_pre2toto"; "_pre1toto"] )
(* Exported *)
let (read_env_state_one_file : string -> node) =
fun file ->
(** Returns the initial node of the automata defined in
......@@ -38,8 +63,9 @@ let (read_env_state_one_file : string -> node) =
flush stdout;
raise e
in
let (list_pre_vn, _) = List.split list_pre in
let (list_pre_vn0, _) = List.split list_pre in
let list_pre_vn = add_missing_pre list_pre_vn0 in
(* Sets the [graph] field of [env_state]. *)
let node_nb = (List.length (Graph.get_all_nodes env_state.graph)) in
let (add_arc: Parse_env.read_arc -> unit) =
......
source/eval.ml
View file @ 9d1241f6
......@@ -255,12 +255,23 @@ let (formula_to_atomic: formula -> atomic_expr) = function
| False -> Bool(false)
| _ -> assert false
let (get_pre_var: var_name -> var_name) =
fun pre_n_vn ->
let (n, vn) = Util.split_pre_var_string pre_n_vn in
if (n-1) <> 0
then ("_pre" ^ (string_of_int (n-1)) ^ vn)
else vn
let _ = assert ((get_pre_var "_pre3toto") = "_pre2toto")
let _ = assert ((get_pre_var "_pre1toto") = "toto")
(* exported *)
let (update_pre: env_in -> env_out -> env_loc -> unit) =
fun input output local ->
let (update_one_pre_var : var_name -> subst) =
fun pre_vn ->
let vn = String.sub pre_vn 4 ((String.length pre_vn) -4) in
let vn = get_pre_var pre_vn in
let pre_value =
try Hashtbl.find input vn
with Not_found ->
......
source/parse_env.ml
View file @ 9d1241f6
......@@ -138,7 +138,7 @@ and (parse_var: aut_token -> vnt) =
( match typ with
"bool" -> (var, BoolT)
(* XXX Rajouter dans le format un moyen de prciser ces bornes *)
| "float" -> (var, FloatT(-.min_float, max_float))
| "float" -> (var, FloatT(-.max_float, max_float))
| "int" -> (var, IntT(-min_int, max_int))
| str -> failwith ("*** Bad type in .env: " ^ str )
)
......
source/rnumsolver.ml
View file @ 9d1241f6
......@@ -58,7 +58,7 @@ type nac =
| NSupEqI of int (** >= *)
| NInfEqI of int (** <= *)
let eps = min_float
let eps = epsilon_float
let (normalise : nc -> Formula.vn * nac) =
fun nc ->
......
source/solver.ml
View file @ 9d1241f6
......@@ -341,9 +341,7 @@ let rec (draw_in_bdd: subst list * Rnumsolver.store -> Bdd.t -> Bdd.t ->
)
else
raise No_numeric_solution
let (draw : vn list -> vnt list -> Bdd.t -> Bdd.t -> subst list * subst list) =
fun bool_vars_to_gen num_vnt_to_gen comb bdd ->
......
source/util.ml
View file @ 9d1241f6
......@@ -197,7 +197,30 @@ let (gv: string -> unit) =
then print_string " Can't call gv; is gv in your path?\n\n"
else ();;
(** [split_pre_var_string pren_vn] returns the int [n] and the string
[vn] if pren_varname is a string that begins with "_pre", followed
by a string representing [n], and ended var [vn] (fails
otherwise). *)
let rec (split_pre_var_string: string -> int * string) =
fun pren_vn ->
let n_vn = String.sub pren_vn 4 ((String.length pren_vn) - 4) in
try split_pre_var_string_acc "" n_vn
with Failure _ -> failwith ("*** Bad format of pre var. It should be of " ^
"the form, e.g., \"_pre32toto\", which is not" ^
" the case of \"" ^ pren_vn ^ "\"\n")
and (split_pre_var_string_acc: string -> string -> int * string) =
fun n_str str ->
let i_str = String.sub str 0 1 in
try
let _ = int_of_string i_str in
split_pre_var_string_acc
(n_str ^ i_str)
(String.sub str 1 ((String.length str) - 1))
with Failure _ ->
((int_of_string n_str), str)
let _ = assert ((split_pre_var_string "_pre44toto") = (44, "toto"))
(****************************************************************************)
......
test/heater_float.rif.exp
View file @ 9d1241f6
......@@ -23,46 +23,46 @@ Dudt:real
#step 8
21.0630719827 #outs t 0.499651978894
#step 9
21.5627239616 #outs f -1.18684266315e-308
21.5627239616 #outs f -2.66697363463
#step 10
21.5627239616 #outs f -3.29123862314e-309
18.895750327 #outs f -0.739579634752
#step 11
21.5627239616 #outs f -1.07307852997e-308
18.1561706922 #outs f -2.41133238312
#step 12
21.5627239616 #outs f -2.11299236317e-308
15.7448383091 #outs f -4.7481398316
#step 13
21.5627239616 #outs f -1.86731856158e-308
10.9966984775 #outs f -4.19608219844
#step 14
21.5627239616 #outs f -1.0546711157e-308
6.80061627908 #outs t 1.05201248789
#step 15
21.5627239616 #outs f -7.4310793236e-309
7.85262876697 #outs t 1.33205998577
#step 16
21.5627239616 #outs f -2.15243263731e-308
9.18468875274 #outs t 0.0652933123238
#step 17
21.5627239616 #outs f -4.46105597619e-309
9.24998206506 #outs t 1.59901951487
#step 18
21.5627239616 #outs f -8.31314176801e-309
10.8490015799 #outs t 1.25277610573
#step 19
21.5627239616 #outs f -9.90891000234e-309
12.1017776857 #outs t 1.10934102574
#step 20
21.5627239616 #outs f -1.35971396293e-308
13.2111187114 #outs t 0.777825771733
#step 21
21.5627239616 #outs f -2.02309075907e-308
13.9889444831 #outs t 0.181551815608
#step 22
21.5627239616 #outs f -1.25081348333e-308
14.1704962987 #outs t 0.875710594009
#step 23
21.5627239616 #outs f -8.17829663712e-309
15.0462068927 #outs t 1.26489661403
#step 24
21.5627239616 #outs f -7.57329185879e-309
16.3111035068 #outs t 1.31927726086
#step 25
21.5627239616 #outs f -7.2098280436e-310
17.6303807676 #outs t 1.93519470811
#step 26
21.5627239616 #outs f -1.50174376539e-308
19.5655754757 #outs t 0.650162771318
#step 27
21.5627239616 #outs f -9.95324653024e-309
20.2157382471 #outs t 1.10535585215
#step 28
21.5627239616 #outs f -1.20246699858e-308
21.3210940992 #outs f -2.70208333531
#step 29
21.5627239616 #outs f -4.63147086824e-310
18.6190107639 #outs f -0.104074542302
#step 30
21.5627239616 #outs f -1.38285127784e-308
18.5149362216 #outs f -3.1074278109
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment