Commit 89aedffe authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.45 Mon, 22 Sep 2008 18:20:01 +0200 by jahier

Parent-Version:      1.44
Version-Log:

Fix an embarassing bug in the integer solver (in dimension 1).

Project-Description: Lurette
parent b6379be0
This diff is collapsed.
......@@ -9,6 +9,11 @@ source: gen_version
cd install; autoconf; cd ..
./RUN_ME
clean:
cd polka; make clean; cd ..
cd GBDDML; make clean; cd ..
cd source; make clean; cd ..
VERSION:=$(shell prcs info --sort date ./lurette.prj | tail -n 1 | awk '{printf "%s\n", $$2}')
......@@ -16,6 +21,12 @@ VERSION:=$(shell prcs info --sort date ./lurette.prj | tail -n 1 | awk '{printf
gen_version:
rm -f source/version.ml
echo "let str=\"$(VERSION)\"" > source/version.ml
rm VERSION
date +VERSION_DATE=%d-%m-%y > VERSION
echo "VERSION=$(VERSION)" >> VERSION
echo "export VERSION" >> VERSION
echo "export VERSION_DATE" >> VERSION
ci:
......
......@@ -5,14 +5,13 @@
# For updates see:
# http://www.oefai.at/~markus/ocaml_sources
#
# $Id: OcamlMakefile 1.55 Tue, 06 Jun 2006 14:26:40 +0200 jahier $
# $Id: OcamlMakefile 1.56 Mon, 22 Sep 2008 18:20:01 +0200 jahier $
#
###########################################################################
# Set these variables to the names of the sources to be processed and
# the result variable. Order matters during linkage!
-include ./Makefile.common.source
......
......@@ -5,14 +5,26 @@ programs from Ocaml.
*************************************************************************
* INSTALLATION
* INSTALLATION of the libraries
Just copy the files of the ./lib directory wherever it is convenient for you.
For example, in the
For example, in the directory:
`ocamlc -where`/lucky
directory (that you have to create before)
Perform a « mkdir `ocamlc -where`/lucky » if necessary.
*************************************************************************
* binaries
The bin directory contains two standalone executables:
- luc4ocaml.top, an Objective Caml toplevel that contains the luc4ocaml lib
preloaded at start-up (try './luc4ocaml.top -I `ocamlc -where`/lucky').
- luc2c: an experimental tool that generates C file wrappers that makes it
possible to Call Lucky programs from C (cf examples/lucky/C/Makefile).
*************************************************************************
......@@ -31,7 +43,7 @@ Confere also the following directories to find examples:
*************************************************************************
* Building files
Thoses example directories contain Makefile that illustrate how programs
Thoses example directories contain Makefiles that illustrate how programs
should be compiled. Basically one needs to:
(1) import the following ocaml librairies(*):
......
V1.45 (22/09/2008)
* Fix an embarassing bug in the integer solver (in dimension 1).
V1.44 (4/12/2007)
* Better error messages and a few minor improvements
V1.43 (8/12/2006)
* Add a luc2c tool, which generates C stub files to call lucky
......
......@@ -49,10 +49,14 @@ Bien sur, il manipule 10000 variables au lieu de 1000, mais tout de m
*********** A faire
* luc2c reclame un HOST_TYPE (ne devrait pas. sinon, l'encapsuler dans un script)
par ailleurs, luc2c --scade povoque un « failure "tl" error » avec un exemple
de david Lesens.
* Luc4ocaml : rajouter un get_vertices
* verifier que les ~init secomportent correctement en cas de produit d'automate
* verifier que les ~init se comportent correctement en cas de produit d'automate
* les env_state.d.memory devraient etre des Value.t VarMap.t plutot
que des Var.subst list !!
......
VERSION_DATE=01-02-07
VERSION=unstable.3
VERSION_DATE=26-02-08
VERSION=1.44
export VERSION
export VERSION_DATE
......@@ -12,13 +12,13 @@ window.ml: window.rml
window: window.ml
$(OCAMLC) -o window \
-I `$(RMLC) -where` -I ../lib \
luc4ocaml.cma rml_interpreter.cma \
luc4ocaml.cma rmllib.cma \
window.ml
window.opt: window.ml
$(OCAMLOPT) -o window \
-I `$(RMLC) -where` -I +lucky -I ../lib \
$(LUC4OCAML_CMXA) rml_interpreter.cmxa \
$(LUC4OCAML_CMXA) rmllib.cmxa \
window.ml
......
......@@ -570,21 +570,3 @@ let
if val then pre(cpt) + 1 else 0 ;
m = (cpt >= n) ;
tel
......@@ -12,7 +12,7 @@ locals {
cpt : int ;
invariant : bool ~alias (cpt = pre cpt + 1)
and ( T = pre T + (if Heat_on then eps else -eps));
and ( T = (if Heat_on then eps else -eps) + pre T);
new_T1 : bool ~alias T1 = T + eps1 ;
new_T2 : bool ~alias T2 = T + eps2 ;
......
This diff is collapsed.
......@@ -437,7 +437,7 @@ lucky_bc:
lucky_debug:
mv *.mli hide_mli
make -k dc -f Makefile.lucky OCAMLFLAGS="" MLONLY=yes
make -k dc -f Makefile.lucky OCAMLFLAGS="" MLONLY=yes || mv hide_mli/*.mli .
mv hide_mli/*.mli .
lucky_debug2:
......
......@@ -39,7 +39,6 @@ CLIBS = camlidl $(CLIBS_WIN32) bdd_stubs
USE_CAMLP4 = yes
HERE=$(LURETTE_PATH)/source/
HERE=./
......@@ -164,7 +163,11 @@ SOURCES_OCAML := \
$(HERE)/rif.mli \
$(HERE)/rif.ml \
$(HERE)/luc_exe.mli \
$(HERE)/luc_exe.ml
$(HERE)/luc_exe.ml \
./luc4ocaml.mli \
./luc4ocaml.ml \
./luc4ocaml_nolbl.mli \
./luc4ocaml_nolbl.ml
endif
......@@ -174,16 +177,16 @@ RESULT = lucky
-include $(OCAMLMAKEFILE)
pack :
# for distributing the sources...
src :
rm -rf lucky-src
mkdir lucky-src
mkdir lucky-src/source
mkdir lucky-src/examples
cp -rf ../examples/lucky examples
cp -rf ../GBDDML lucky-src/
cp -rf ../polka lucky-src/
cp $(SOURCES_OCAML) lucky-src/source
cp ../Makefile.common.source lucky-src
cp ../OcamlMakefile lucky-src
cp Makefile.lucky lucky-src/source
cp ../OcamlMakefile.orig lucky-src/OcamlMakefile
cp Makefile.lucky.src lucky-src/source/Makefile
tar cvfz lucky-src-$(VERSION).tgz lucky-src
\ No newline at end of file
......@@ -6,7 +6,7 @@ else
VERSION = $(shell prcs info --sort=date ../lurette.prj | tail -n 1 | awk '{printf "%s\n", $$2}')
endif
VERSION=1.43
#VERSION=1.43
ver:
echo version=$(VERSION)
......@@ -226,7 +226,6 @@ draw-rel:
cp -rf ../examples/luckyDraw /tmp/$(DRAW_RELEASE_NAME)/examples/
cp -rf $(SYNCHRONE_LURETTE_DIR)/doc/luckydraw /tmp/$(DRAW_RELEASE_NAME)/doc/ || true
mkdir /tmp/$(DRAW_RELEASE_NAME)/lib
mkdir /tmp/$(DRAW_RELEASE_NAME)/bin
\
cp ../README-luckyDraw /tmp/$(DRAW_RELEASE_NAME)/
cp -rf $(LURETTE_PATH)/$(HOSTTYPE)/lib/*polka*a /tmp/$(DRAW_RELEASE_NAME)/lib
......
......@@ -27,6 +27,7 @@ type optionsT = {
type cmd_line_optionT =
StepNb | Seed | Precision | Boot | ShowAut | NoShowAut | Verbose | Locals
| Help | Inside | Edges | Vertices | ComputeVolume | Oracle | PP | Reactive
| Version
(* Names of the command line options to override the defaults. *)
let (string_to_option: (string * cmd_line_optionT) list) = [
......@@ -73,6 +74,9 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
("--reactive", Reactive);
("--version", Version);
("-version", Version);
("--help", Help);
("-help", Help);
("-h", Help)
......@@ -93,6 +97,7 @@ let (option_to_usage: cmd_line_optionT -> string) =
| Locals -> "Shows local variables.\n"
| Help -> "Display this message.\n"
| Verbose -> "Set on a verbose mode.\n"
| Version -> "Display the version number.\n"
| Oracle -> "Launch an oracle (replace blank by '+', e.g., --oracle ecexe+f.ec).\n"
| PP -> "Pipe lucky file(s) through a preprocessor (e.g., cpp).\n"
| Reactive -> "Set on a reactive mode, in which, when no transition is possible, the previous values are returned.\n"
......
......@@ -38,7 +38,7 @@ val cmd_line_string_to_int : string -> string -> int
type cmd_line_optionT =
StepNb | Seed | Precision | Boot | ShowAut | NoShowAut | Verbose
| Locals | Help | Inside | Edges | Vertices | ComputeVolume | Oracle | PP | Reactive
| Version
val string_to_option: (string * cmd_line_optionT) list
(** Mapping from options string (e.g., "--with_seed") to the cmd_line_optionT
......
......@@ -58,7 +58,7 @@ let rec (get_subst_from_solved_system : t' ->
let s =
match (Ne.find "" ne) with
Some(cst) -> (vn, Value.quot_num cst v)
| None -> (vn, Value.diff_num v v)
| None -> (vn, Value.diff_num v v) (* return 0 *)
in
let new_tail =
(* We reinject the binding obtained in s into the remaining
......@@ -67,8 +67,8 @@ let rec (get_subst_from_solved_system : t' ->
(fun (x, ne) -> (x,(Ne.apply_simple_subst ne s)))
tail
in
s::(get_subst_from_solved_system store new_tail)
s::(get_subst_from_solved_system store new_tail)
let (deduce_remaining_vars : (string * Value.num) list ->
t' -> (string * Value.num) list) =
......
......@@ -109,7 +109,7 @@ let rec (lookup: Var.env_in -> Env_state.t -> Exp.var -> Value.t option) =
Ditto for the linear_constraint <-> bdd index tables.
The reason for that is that, formula that depends on pre or input
are not likely to appear twice if they contains numiric values.
are not likely to appear twice if they contains numeric values.
For Boolean, well, I could leave them in the global table.
*)
......@@ -435,7 +435,7 @@ and
let gne1 = (expr_to_gne e1 input state)
and gne2 = (expr_to_gne e2 input state)
in
Gne.quot gne1 gne2
Gne.div gne1 gne2
| Mod(e1, e2) ->
let gne1 = (expr_to_gne e1 input state)
......
......@@ -26,11 +26,18 @@ type t
val add : t -> t -> t
val diff : t -> t -> t
val mult : t -> t -> t
val quot : t -> t -> t
val modulo : t -> t -> t
val div : t -> t -> t
val opposite : t -> t
(* The same as div, except that is raises an internal error if
the second arg does not divide the first.
For internal use only.
*)
val quot : t -> t -> t
(** [empty ()] returns an empty gne.t *)
val empty : unit -> t
......
......@@ -101,6 +101,7 @@ and
n+2
| Locals -> options.locals <- true ; (n+1)
| Help -> print_string Command_line_luc_exe.usage; exit 0
| Version -> exit 0
| Inside -> options.draw_mode <- Lucky.StepInside ; (n+1)
| Edges -> options.draw_mode <- Lucky.StepEdges ; (n+1)
| Vertices -> options.draw_mode <- Lucky.StepVertices ; (n+1)
......
......@@ -213,9 +213,9 @@ let ite_i c n1 n2 =
let sum_i n1 n2 = Exp.Sum (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let diff_i n1 n2 = Exp.Diff (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let prod_i n1 n2 = Exp.Prod (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let quot_i n1 n2 = Exp.Quot (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let mod_i n1 n2 = Exp.Mod (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let div_i n1 n2 = Exp.Div (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let quot_i = div_i
let uminus_i n1 = Exp.Uminus (fst n1), (snd n1)
......@@ -245,7 +245,8 @@ let ite_f c n1 n2 =
let sum_f n1 n2 = Exp.Sum (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let diff_f n1 n2 = Exp.Diff (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let prod_f n1 n2 = Exp.Prod (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let quot_f n1 n2 = Exp.Quot (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let div_f n1 n2 = Exp.Div (fst n1, fst n2), Util.merge (snd n1) (snd n2)
let quot_f = div_f
let uminus_f n1 = Exp.Uminus (fst n1), (snd n1)
......
(** Time-stamp: <modified the 11/12/2006 (at 15:25) by Erwan Jahier> *)
(** Time-stamp: <modified the 22/09/2008 (at 14:37) by Erwan Jahier> *)
(*
** File: luckyDraw.mli
** Author: jahier@imag.fr
......@@ -79,9 +79,9 @@ val ite_i : bool_expr -> int_expr -> int_expr -> int_expr
val sum_i : int_expr -> int_expr -> int_expr
val diff_i : int_expr -> int_expr -> int_expr
val prod_i : int_expr -> int_expr -> int_expr
val quot_i : int_expr -> int_expr -> int_expr
val mod_i : int_expr -> int_expr -> int_expr
val div_i : int_expr -> int_expr -> int_expr
val quot_i : int_expr -> int_expr -> int_expr
val uminus_i : int_expr -> int_expr
......@@ -102,6 +102,7 @@ val ite_f : bool_expr -> float_expr -> float_expr -> float_expr
val sum_f : float_expr -> float_expr -> float_expr
val diff_f : float_expr -> float_expr -> float_expr
val prod_f : float_expr -> float_expr -> float_expr
val div_f : float_expr -> float_expr -> float_expr
val quot_f : float_expr -> float_expr -> float_expr
val uminus_f : float_expr -> float_expr
......
......@@ -32,7 +32,6 @@ type t =
| Le_sum of Lexeme.t * t * t
| Le_diff of Lexeme.t * t * t
| Le_prod of Lexeme.t * t * t
| Le_quot of Lexeme.t * t * t
| Le_mod of Lexeme.t * t * t
| Le_div of Lexeme.t * t * t
| Le_and of Lexeme.t * t * t
......@@ -79,7 +78,6 @@ let (le_to_string : t -> string) =
| Le_sum(lex , _ , _) -> lex.str
| Le_diff(lex , _ , _) -> lex.str
| Le_prod(lex , _ , _) -> lex.str
| Le_quot(lex , _ , _) -> lex.str
| Le_mod(lex , _ , _) -> lex.str
| Le_div(lex , _ , _) -> lex.str
| Le_and(lex , _ , _) -> lex.str
......@@ -471,11 +469,6 @@ let rec (do_type : my_in_channel -> Exp.var_tbl -> vut -> typedef list ->
(fun e1 e2 -> Numer(Prod(e1, e2))) true
" numeric expression expected")
| Le_quot(sinfo, le1, le2) ->
(do_type_num_op2 ic sinfo varl vutl tdl ftbl le1 le2
(fun e1 e2 -> Numer(Quot(e1, e2))) true
" numeric expression expected")
| Le_mod(sinfo, le1, le2) -> (
let (varl2, fel, t) =
do_type_num_op2 ic sinfo varl vutl tdl ftbl le1 le2
......@@ -490,19 +483,10 @@ let rec (do_type : my_in_channel -> Exp.var_tbl -> vut -> typedef list ->
(varl2, fel, t)
)
| Le_div(sinfo, le1, le2) -> (
let (varl2, fel, t) =
do_type_num_op2 ic sinfo varl vutl tdl ftbl le1 le2
(fun e1 e2 -> Numer(Div(e1, e2))) true
" integer expression expected"
in
if
t <> IntT
then
( uncompatible_type ic sinfo t IntT ; exit 2)
else
(varl2, fel, t)
)
| Le_div(sinfo, le1, le2) ->
(do_type_num_op2 ic sinfo varl vutl tdl ftbl le1 le2
(fun e1 e2 -> Numer(Div(e1, e2))) true
" numeric expression expected")
| Le_sup(sinfo, le1, le2) ->
(do_type_num_op2 ic sinfo varl vutl tdl ftbl le1 le2
......@@ -1278,16 +1262,6 @@ let rec (infer_type_do : t -> itype -> var list ->
| _ -> assert false
)
| Le_quot(sinfo, le1, le2) ->
check_type sinfo N typ;
let (e1, it1, acc1) = infer_type_do le1 typ acc in
let (e2, it2, acc2) = infer_type_do le2 it1 acc1 in
(
match e1,e2 with
Numer e1', Numer e2' -> Numer(Quot(e1', e2')), it2, acc2
| _ -> assert false
)
| Le_mod(sinfo, le1, le2) ->
check_type sinfo I typ;
let (e1, _,acc1) = infer_type_do le1 I acc in
......
......@@ -28,7 +28,6 @@ type t =
| Le_sum of Lexeme.t * t * t
| Le_diff of Lexeme.t * t * t
| Le_prod of Lexeme.t * t * t
| Le_quot of Lexeme.t * t * t
| Le_mod of Lexeme.t * t * t
| Le_div of Lexeme.t * t * t
| Le_and of Lexeme.t * t * t
......
......@@ -33,6 +33,51 @@ type t = Value.num StringMap.t
type subst = (string * Value.num) * t
(****************************************************************************)
(* exported *)
let (to_string_gen : (Value.num -> string) -> string -> t -> string) =
fun nv_to_string plus ne ->
let str =
(StringMap.fold
(fun vn v acc ->
if
vn = ""
then
let v_str = nv_to_string v in
match v_str with
"" -> "+1" ^ acc
| "-" -> "-1" ^ acc
| _ -> (v_str ^ acc)
else
(acc^plus ^ (nv_to_string v ) ^ "" ^ ((Prevar.format vn)))
)
ne
""
)
in
Str.global_replace (Str.regexp "+ -") "-" str
(* exported *)
let (to_string : t -> string) =
fun ne ->
to_string_gen (num_value_to_string) " + " ne
(* exported *)
let (print : t -> unit) =
fun ne ->
print_string (to_string ne)
(* exported *)
let (substl_to_string : subst list -> string) =
fun sl ->
(List.fold_left
(fun acc ((vn, a), ne) ->
(acc ^ " " ^ (Value.num_value_to_string a) ^ "." ^ vn ^
" -> " ^ to_string ne ^ "\n")
)
""
sl
)
(****************************************************************************)
......@@ -219,17 +264,6 @@ let (quot: t -> t -> t) =
else
failwith "*** The second argument of '/' should be bound (otherwise, the constraint is not linear).\n"
let _ = assert (
let ne1 = StringMap.add "" (I(1)) (StringMap.add "toto" (I(2)) StringMap.empty) in
let ne2 = StringMap.add "" (I(2)) StringMap.empty in
let ne_res = StringMap.add "" (I(0)) (StringMap.add "toto" (I(1)) StringMap.empty) in
let ne_cal = quot ne1 ne2 in
((StringMap.find "toto" ne_res) = (StringMap.find "toto" ne_cal))
&&
((StringMap.find "" ne_res) = (StringMap.find "" ne_cal))
)
(****************************************************************************)
......@@ -252,6 +286,17 @@ let (div: t -> t -> t) =
else
failwith "*** the second argument of 'div should be bound (otherwise, the constraint is not linear). \n"
let _ = assert (
let ne1 = StringMap.add "" (I(1)) (StringMap.add "toto" (I(2)) StringMap.empty) in
let ne2 = StringMap.add "" (I(2)) StringMap.empty in
let ne_res = StringMap.add "" (I(0)) (StringMap.add "toto" (I(1)) StringMap.empty) in
let ne_cal = div ne1 ne2 in
((StringMap.find "toto" ne_res) = (StringMap.find "toto" ne_cal))
&&
((StringMap.find "" ne_res) = (StringMap.find "" ne_cal))
)
(****************************************************************************)
......@@ -282,22 +327,103 @@ let (neg_nexpr : t -> t) =
fun ne ->
StringMap.map (fun x -> match x with I(i) -> I(-i) | F(f) -> F(-.f)) ne
type split_res =
| Split of string * Value.num * t
(* i.e., for expressions over floats, or for simple integer expressions *)
| No_solution (* e.g., "2.x + 3 = 0" have no solution for integers *)
| Dont_know (* e.g., "a.x + b.y = 0", for which it is difficult to
find a substition for integers *)
let split_res_to_string = function
| Split(str,v,ne) ->
"(" ^ str ^ ", " ^ (Value.num_value_to_string v)^ ", " ^ (to_string ne) ^ ")"
| No_solution -> "no solution"
| Dont_know -> "???"
(* exported *)
let (split : t -> (string * Value.num) option * t) =
let (split_old : t -> split_res) =
fun ne ->
let f = fun var num_val acc ->
match acc with
None, ne ->
if
var = ""
then
if var = "" then
None, StringMap.add var num_val ne
else
Some(var, num_val), ne
| Some(v, nv), ne -> Some(v, nv), (StringMap.add var num_val ne)
in
StringMap.fold f ne (None, StringMap.empty)
in (
match StringMap.fold f ne (None, StringMap.empty) with
| None,_ -> No_solution
| Some(v,c), ne -> Split(v,c,ne)
)
let (split : t -> split_res) =
fun ne ->
(* let res2 = split2 ne in *)
let list_to_ne =
List.fold_left (fun acc (c,v) -> StringMap.add v c acc) StringMap.empty
in
let divide c1 c2 =
match (c1,c2) with
| I i1, I i2 -> (i2/i1)*i1 = i2
| _ ,_ -> true
in
let cl = List.rev (StringMap.fold (fun v c acc -> (c,v)::acc) ne []) in
let res =
match cl with
| []
| [_,_] ->
print_string "The impossible occured!\n"; flush stdout;
assert false (* dim > 0 *)
| (F f_cst,"")::(F f, v)::rest
| (F f, v)::(F f_cst,"")::rest
-> (* for floats, no soucis... *)
(* a.x+b*)
let ne_rest = list_to_ne ((F f_cst, "")::rest) in
Split(v, F f, ne_rest)
(* For integers, let's be careful *)
| (c,v)::(c0, "")::[]
| (c0, "")::(c,v)::[] ->
(* c.v = 0 => c = 0 *)
let ne_rest = list_to_ne [(c0, "")] in
if divide c c0 then Split (v, c, ne_rest) else No_solution
| _ -> (
try (* we search if one of the coef divide all the others *)
let (c,v) =
List.find
(fun (c,v) ->
v<>"" && List.for_all (fun (c',v') -> divide c c') cl
)
cl
in
let _, rest = List.partition (fun x -> x=(c,v)) cl in
let ne_rest = list_to_ne rest in
Split(v,c, ne_rest)
with
(* if no coef divide all the other, we dont know what to do.
That will be handled later by polka.
*)