Commit 7733868b authored by Erwan Jahier's avatar Erwan Jahier

Take the -m option into account by lutin when used with --2c-4luciole.

parent 7f9e1c37
......@@ -30,6 +30,7 @@ camlidl-*
*.hide
*.zip
*.rif
*.rif0
*.rif~
objs
*.plot
......@@ -183,3 +184,8 @@ cross-win32
doc/lutin-man/touch.tex
linux
mymakefile
*_exe
*.lut.tex
examples/lutin/catherine
examples/lutin/simplice
examples/lutin/chaouki
\ No newline at end of file
......@@ -68,7 +68,7 @@ ifeq ($(HOSTTYPE),cygwin)
CC=gcc
GCC=gcc
GPP=g++
CFLAGS=-g -O2 -fpic
CFLAGS=-g -O2 -fpic -DPOLKA_NUM=3
SYNCHRONE_DIR=//ARPONT/www-verimag/DIST-TOOLS/SYNCHRONE
......@@ -104,7 +104,7 @@ ifeq ($(HOSTTYPE),cross-win32)
AR=/usr/bin/i586-mingw32msvc-ar
AS=/usr/bin/i586-mingw32msvc-as
export EXE=.exe
CFLAGS=-g -O2 -fpic -DWIN32
CFLAGS=-g -O2 -fpic -DWIN32 -DPOLKA_NUM=3
DWIN32 =
OCAMLOPT=/usr/i586-mingw32msvc/bin/ocamlopt
......@@ -123,7 +123,7 @@ ifeq ($(HOSTTYPE),win32)
GPP=g++
RANLIB=ranlib
CFLAGS=
CFLAGS=-DPOLKA_NUM=3
AR=ar
AS=as
EXE := .exe
......
node n (i:bool) returns(x: real) =
loop ~5: 1 { i and x=42. }
\ No newline at end of file
......@@ -5,10 +5,8 @@ LIB=../../../$(HOSTTYPE)/lib
MAIN=rabbit
NEW_LURETTETOP=$(LTOP) --precision 2 \
--test-length 5000 --thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-sim2chro \
--do-not-show-step
--test-length 5000 --step-mode Inside --local-var --no-sim2chro \
--do-not-show-step -v 2
......@@ -22,7 +20,7 @@ clean:
test: rabbit.cmxs
rm -f test.rif0 .lurette_rc
$(NEW_LURETTETOP) -go --output test.rif0 \
$(NEW_LURETTETOP) -go --output test.rif0 -seed 3306566 \
-rp "sut:ocaml:rabbit.cmxs:" \
-rp 'env:lutin:rabbit.lut:-main:rabbit:-L:libm.so:-loc' && \
grep -v "lurette chronogram" test.rif0 | \
......
include "ud.lut"
--------------------------------------------------------------------------------
--
--
-- --------------------------------------
-- | |
-- | |
-- | ----------------- |
-- | | p1 | p2 | |
-- | | | | |
-- | | | | |
-- | |--------c--------| |
-- | | | | |
-- | | | | |
-- | | p4 | p3| |
-- | ----------------- |
-- | |
-- | |
-- | |
-- | |
-- | |
-- --------------------------------------
--
-- c is moving in the big square (the graphics window).
-- p1, p2, p3, p4 are moving in the 4 small squares (depends on c)
node obstacle(x_min, x_max, y_min, y_max : real)
returns (p1x, p1y, p2x, p2y, p3x, p3y, p4x, p4y : real) =
exist cx, cy : real in
let cote_x = (x_max-x_min) / 4.0 in
let cote_y = (y_max-y_min) / 4.0 in
let eps = 10.0 in
run cx := up_and_down(x_min + cote_x/2.0 , x_max-cote_x/2.0, eps) in
run cy := up_and_down(y_min + cote_y/2.0 , y_max-cote_y/2.0, eps) in
assert
-- each pi remains inside one of the small squares
between(p1x, cx - cote_x, cx) and
between(p1y, cy - cote_y, cy) and
between(p2x, cx, cx + cote_x) and
between(p2y, cy - cote_y, cy) and
between(p3x, cx, cx + cote_x) and
between(p3y, cy, cy + cote_y) and
between(p4x, cx - cote_x, cx) and
between(p4y, cy, cy + cote_y)
in
true fby loop {
-- each pi does not move too fast
between(p1x, pre p1x - eps, pre p1x + eps) and
between(p1y, pre p1y - eps, pre p1y + eps) and
between(p2x, pre p2x - eps, pre p2x + eps) and
between(p2y, pre p2y - eps, pre p2y + eps) and
between(p3x, pre p3x - eps, pre p3x + eps) and
between(p3y, pre p3y - eps, pre p3y + eps) and
between(p4x, pre p4x - eps, pre p4x + eps) and
between(p4y, pre p4y - eps, pre p4y + eps)
}
let cross_product(ux,uy,vx,vy:real) : real = (ux*vy-uy*vx)
-- we look at the sign (of the z-axis) of p1p4 ^ p1p (cross product), etc.
let is_inside(px,py,p1x,p1y,p2x,p2y,p3x,p3y,p4x,p4y : real) : bool =
let p1p_x = px-p1x in
let p1p_y = py-p1y in
let p2p_x = px-p2x in
let p2p_y = py-p2y in
let p3p_x = px-p3x in
let p3p_y = py-p3y in
let p4p_x = px-p4x in
let p4p_y = py-p4y in
let p2p1_x = p1x-p2x in
let p2p1_y = p1y-p2y in
let p1p4_x = p4x-p1x in
let p1p4_y = p4y-p1y in
let p4p3_x = p3x-p4x in
let p4p3_y = p3y-p4y in
let p3p2_x = p2x-p3x in
let p3p2_y = p2y-p3y in
cross_product(p2p1_x, p2p1_y, p2p_x, p2p_y) < 0.0 and -- p2p1 ^ p2p < 0
cross_product(p1p4_x, p1p4_y, p1p_x, p1p_y) < 0.0 and -- p1p4 ^ p1p < 0
cross_product(p4p3_x, p4p3_y, p4p_x, p4p_y) < 0.0 and -- p4p3 ^ p4p < 0
cross_product(p3p2_x, p3p2_y, p3p_x, p3p_y) < 0.0 -- p3p2 ^ p3p < 0
include "ud.lut"
include "moving-obstacle.lut"
node rabbit_speed (low, high:real) returns (Speed: real) =
exist Delta, SpeedLow, SpeedHigh: real in
let draw_params() =
between(Delta, 0.5, 1.0) and
between(SpeedLow, 0.0, low) and between(SpeedHigh, 1.0, high)
in
let keep_params() =
Delta = pre Delta and SpeedLow = pre SpeedLow and
SpeedHigh = pre SpeedHigh
in
{
&> loop { draw_params() fby loop ~100: 10 { keep_params() } }
&> Speed = 1.0 fby
run Speed := up_and_down(pre SpeedLow, pre SpeedHigh, pre Delta)
}
extern sin(x: real) : real
extern cos(x: real) : real
-- extern printint(i:int):unit
exception Pb
node rabbit (x_min, x_max, y_min, y_max : real)
returns(x, y, p1x, p1y, p2x, p2y, p3x, p3y, p4x, p4y: real ; freeze:bool) =
exist Speed, Alpha, Beta : real in
let keep_position() = (x = pre x and y = pre y) in
let draw_params() = between(Alpha, -3.14, 3.14) and between(Beta, -0.3, 0.3)
in
-- The beginning
run Speed := rabbit_speed(5.0, 50.0) in
run p1x,p1y, p2x,p2y, p3x,p3y, p4x,p4y := obstacle(x_min, x_max, y_min, y_max) in
let line() =
x = (pre x + Speed * cos(pre Alpha)) and
y = (pre y + Speed * sin(pre Alpha)) and
Alpha = pre Alpha and
-- And he always avoids the obstacle
not is_inside(x,y,p1x,p1y,p2x,p2y,p3x,p3y,p4x,p4y)
in
let escape () =
try
between(x, pre x - 21.0, pre x + 21.) and
between(y, pre y - 21.0, pre y + 21.) and
not is_inside(x,y,p1x,p1y,p2x,p2y,p3x,p3y,p4x,p4y)
do raise Pb
in
let curve() =
x = (pre x + Speed * cos(pre Alpha)) and
y = (pre y + Speed * sin(pre Alpha)) and
Alpha = pre Alpha - Beta and Beta = pre Beta and
not is_inside(x,y,p1x,p1y,p2x,p2y,p3x,p3y,p4x,p4y)
in
assert
-- The rabbit always remains in its playground
between(x, x_min, x_max) and
between(y, y_min, y_max)
in
assert (freeze = is_inside(x,y,p1x,p1y,p2x,p2y,p3x,p3y,p4x,p4y)) in
draw_params() fby
try loop {
-- try
{ draw_params() &> escape() } fby
-- { draw_params() and keep_position() } fby
{
| loop [0,20] line() -- forward straigth ahead for a while
| loop [0,20] curve() -- forward by turning for a while
}
-- do escape()
-- nb: if it is inside the obstacle, it keeps its position until it can move
}
......@@ -11,21 +11,18 @@ let draw x y =
open Data
let get_float var sol =
match (
try List.assoc var sol with Not_found -> assert false
) with (F f) -> f | _ ->
Printf.printf "*********************\n";
match (try List.assoc var sol with Not_found -> assert false)
with (F f) -> f | _ ->
Printf.printf "*** error when parsing float\n";
flush stdout;
assert false
let det ((p1x,p1y),(p2x,p2y),(p3x,p3y),(p4x,p4y)) =
((p2x-.p1x)*.(p4y-.p3y)-.(p2y-.p1y)*.(p4x-.p3x))
let poly_mem = ref [|(0,0)|]
let get_bool var sol =
match (try List.assoc var sol with Not_found -> assert false)
with (B b) -> b | _ ->
Printf.printf "*** error when parsing bool\n";
flush stdout;
assert false
(**************************************************************************)
......@@ -40,7 +37,6 @@ let _ =
let init _ = ()
type var_type = string
let (inputs :(string * string) list) = [
......@@ -53,7 +49,9 @@ let (inputs :(string * string) list) = [
"p3x", "real";
"p3y", "real";
"p4x", "real";
"p4y", "real"]
"p4y", "real";
"freeze", "bool"
]
let mems_i = []
......@@ -68,7 +66,35 @@ let (outputs :(string * string) list) =
"y_min", "real"; "y_max", "real"
]
let cross_product(ux,uy,vx,vy) = (ux*.vy-.uy*.vx);;
let image = ref (Graphics.get_image 0 0 (Graphics.size_x ()) (Graphics.size_y ()))
let cross_product(ux,uy,vx,vy) = (ux*.vy-.uy*.vx)
let is_inside(px,py,p1x,p1y,p2x,p2y,p3x,p3y,p4x,p4y) =
let p1p_x = px-.p1x in
let p1p_y = py-.p1y in
let p2p_x = px-.p2x in
let p2p_y = py-.p2y in
let p3p_x = px-.p3x in
let p3p_y = py-.p3y in
let p4p_x = px-.p4x in
let p4p_y = py-.p4y in
let p2p1_x = p1x-.p2x in
let p2p1_y = p1y-.p2y in
let p1p4_x = p4x-.p1x in
let p1p4_y = p4y-.p1y in
let p4p3_x = p3x-.p4x in
let p4p3_y = p3y-.p4y in
let p3p2_x = p2x-.p3x in
let p3p2_y = p2y-.p3y in
cross_product(p2p1_x, p2p1_y, p2p_x, p2p_y) < 0.0 &&
cross_product(p1p4_x, p1p4_y, p1p_x, p1p_y) < 0.0 &&
cross_product(p4p3_x, p4p3_y, p4p_x, p4p_y) < 0.0 &&
cross_product(p3p2_x, p3p2_y, p3p_x, p3p_y) < 0.0
let (step : Data.subst list -> Data.subst list)=
fun rabbit_outs ->
let x_min = (F (float_of_int 0))
......@@ -89,7 +115,15 @@ let (step : Data.subst list -> Data.subst list)=
and p2y = get_float "p2y" rabbit_outs
and p3y = get_float "p3y" rabbit_outs
and p4y = get_float "p4y" rabbit_outs
and freeze = get_bool "freeze" rabbit_outs
in
if
(is_inside(x,y,p1x,p1y,p2x,p2y,p3x,p3y,p4x,p4y))
then
(
ignore (Graphics.read_key ())
);
let p1xI = truncate p1x
and p1yI = truncate p1y
and p2xI = truncate p2x
......@@ -98,21 +132,23 @@ let (step : Data.subst list -> Data.subst list)=
and p3yI = truncate p3y
and p4xI = truncate p4x
and p4yI = truncate p4y
in
in
let point_list = [(p1xI,p1yI);(p2xI,p2yI);(p3xI,p3yI);(p4xI,p4yI)] in
let poly = Array.of_list point_list in
if
poly <> !poly_mem
then
(
Graphics.draw_poly poly;
Graphics.set_color (Graphics.rgb 255 255 255);
Graphics.draw_poly !poly_mem;
Graphics.set_color (Graphics.rgb 0 0 0);
poly_mem := poly;
);
Graphics.draw_image !image 0 0;
draw x y;
image := Graphics.get_image 0 0 (Graphics.size_x ()) (Graphics.size_y ());
if freeze then (
Graphics.set_color (Graphics.rgb 255 0 100);
Graphics.fill_poly poly
)
else (
Graphics.set_color (Graphics.rgb 0 0 0);
Graphics.draw_poly poly
);
bounds
......
../up_and_down/ud.lut
\ No newline at end of file
include "lib.lut"
node mainR () returns (x : real) =
exist px : real in
let minR = 0. in
let maxR= 100. in
let deltaR= 5. in
betweenR(x, minR, maxR) fby
betweenR(x, minR, maxR) fby
assert px = pre x in
loop {
up_and_downR(x, px, minR, maxR, deltaR)
}
----------------------------------------------------------------------------------------------
let up_and_downI(x, px : int ref; min, max, delta : int) =
if
(pre x < min) or ( (pre x < max) and (pre px <= pre x))
then
betweenI(x, pre x, pre x + delta)
else
betweenI(x, pre x - delta, pre x)
node mainI () returns (i : int) =
exist pi : int in
let minI = 0 in
let maxI = 100 in
let deltaI = 5 in
betweenI(i, minI, maxI) fby
betweenI(i, minI, maxI) fby
assert pi = pre i in
loop {
up_and_downI(i, pi, minI, maxI, deltaI)
}
node xxx (i:int) returns (j:int ; x: real [4.; 6.0] = 0.0) =
-- assert (i > -1000000 and i < 1000000) in
loop { i=j }
--------------------------------------------------------
node main () returns (i: int; x : real) =
exist pi : int in
exist px : real in
let minI = 0 in
let maxI= 100 in
let deltaI= 5 in
let minR = 0. in
let maxR= 100. in
let deltaR= 5. in
-- let pi = pre i in
betweenI(i, minI, maxI) and betweenR(x, minR, maxR) fby
betweenI(i, minI, maxI) and betweenR(x, minR, maxR) fby
assert pi = pre i in
assert px = pre x in
loop {
up_and_downR(x, px, minR, maxR, deltaR) and
up_and_downI(i, pi, minI, maxI, deltaI)
}
......@@ -60,7 +60,7 @@ utest:
clean:
rm -rf *.h *.c *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp heater_control not_a_sauna*
rm -rf *.h *.c *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp heater_control not_a_sauna* *.cov
......
......@@ -821,6 +821,9 @@ Dynamic allocation of an internal structure
assert (option.env <> []);
put (List.hd option.env);
List.iter (fun x -> put (" " ^ x)) (List.tl option.env);
(match option.main_node with
| None -> ()
| Some mn -> put ("::"^mn));
putln "\");";
putln " return ctx;";
......@@ -868,6 +871,9 @@ Reset procedure
assert (option.env <> []);
put (List.hd option.env);
List.iter (fun x -> put (" " ^ x)) (List.tl option.env);
(match option.main_node with
| None -> ()
| Some mn -> put ("::"^mn));
putln "\");";
putln "}";
......@@ -945,7 +951,7 @@ open Prog
let (main : unit -> unit) =
fun _ ->
let env_list = option.env in
let state = LucProg.make_state option.pp env_list in
let state = LucProg.make_state option.pp env_list option.main_node in
let _ = assert (env_list <> []) in
let fn = build_file_name env_list in
let _ =
......@@ -961,11 +967,7 @@ let (main : unit -> unit) =
| Nop -> ()
| Lustre -> gen_files_for_lustre ()
| Luciole ->
let var_to_vn_ct v =
(Var.name v,
Type.to_cstring (Var.typ v)
)
in
let var_to_vn_ct v = (Var.name v, Type.to_cstring (Var.typ v)) in
Luciole.gen_stubs false fn
(List.map var_to_vn_ct state.s.in_vars)
(List.map var_to_vn_ct state.s.out_vars)
......
......@@ -83,37 +83,37 @@ let rec (main : unit -> 'a) =
( try Arg.parse speclist (fun _ -> ()) usage
with
Failure(e) ->
print_string e;
flush stdout ;
flush stderr ;
exit 2
Failure(e) ->
print_string e;
flush stdout ;
flush stderr ;
exit 2
);
try
if flag.env = "" then (
print_string "*** Bad usage: you ougth to specify a lucky file in input (-env).\n";
Arg.usage speclist usage;
flush stdout ;
flush stderr ;
exit 2
print_string "*** Bad usage: you ougth to specify a lucky file in input (-env).\n";
Arg.usage speclist usage;
flush stdout ;
flush stderr ;
exit 2
);
if flag.sut_header = "" then (
print_string "*** Bad usage: you ougth to specify a c header file in input (-sut-header).\n";
Arg.usage speclist usage;
flush stdout ;
flush stderr ;
exit 2
print_string "*** Bad usage: you ougth to specify a c header file in input (-sut-header).\n";
Arg.usage speclist usage;
flush stdout ;
flush stderr ;
exit 2
);
let _ =
Util.generate_up_and_down_macro "."
in
let state = LucProg.make_state flag.pp [flag.env] in
let state = LucProg.make_state flag.pp [flag.env] None in
let var_to_vn_ct v =
(Var.name v,
Type.to_cstring_bis (Var.typ v)
)
(Var.name v,
Type.to_cstring_bis (Var.typ v)
)
in
let (typedef, sut_inputs, sut_outputs) = Parse_poc.get_vn_and_ct_list flag.sut_header in
let type_to_string (vn,t) =
......@@ -125,21 +125,21 @@ let rec (main : unit -> 'a) =
let env_inputs = List.map var_to_vn_ct state.s.Prog.in_vars in
(* luciole I/O
luciole outs = env in \ sut outs
luciole in = (env outs U sut outs) \ luciole outs
luciole outs = env in \ sut outs
luciole in = (env outs U sut outs) \ luciole outs
*)
let luciole_outputs = List.rev_append
(List.filter (fun v -> not (List.mem v sut_outputs)) env_inputs)
(List.filter (fun v -> not (List.mem v env_outputs)) sut_inputs)
in
in
let luciole_inputs =
List.filter (fun v -> not (List.mem v luciole_outputs)) (List.rev_append env_outputs sut_outputs)
in
let luciole_outputs = List.sort compare luciole_outputs in
let luciole_inputs = List.sort compare luciole_inputs in
let sut_str = Filename.basename (Filename.chop_extension flag.sut_header) in
Luciole.gen_stubs true sut_str luciole_outputs luciole_inputs
Luciole.gen_stubs true sut_str luciole_outputs luciole_inputs
with e ->
Arg.usage speclist usage;
......
......@@ -115,7 +115,7 @@ let (make : string -> string -> lucky_process) =
Formula_to_bdd.clear_all ()
in
let pp_opt = if pp = "" then None else Some pp in
let state0 = LucProg.make_state pp_opt [file] in
let state0 = LucProg.make_state pp_opt [file] None in
let init_state_dyn = state0.d in
let init_state = {
d = init_state_dyn ;
......
......@@ -44,15 +44,15 @@ open Prog
exception MakeError
let (make : ?seed:(int) -> ?fair:(bool) -> ?pp:(string) -> ?verbose:(int) ->
?precision:(int) -> string list -> state) =
?precision:(int) -> ?main:(string option) -> string list -> state) =
fun ?(seed = (random_seed ())) ?(fair = false) ?(pp = "")
?(verbose = 0) ?(precision = 2) files ->
?(verbose = 0) ?(precision = 2) ?(main=None) files ->
try
let _ = Formula_to_bdd.clear_all () in
let pp_opt = if pp = "" then None else Some pp in
let state0 = LucProg.make_state pp_opt files in
let state0 = LucProg.make_state pp_opt files main in
let init_state_dyn = { state0.d with verbose = verbose } in
let init_state = {
d = init_state_dyn ;
......
(** Time-stamp: <modified the 12/07/2011 (at 17:39) by Erwan Jahier> *)
(** Time-stamp: <modified the 08/08/2011 (at 17:05) by Erwan Jahier> *)
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
......@@ -38,7 +38,8 @@ val make :
?pp:(string) -> (** in order to use a preprocessor before parsing *)
?verbose:(int) ->
?precision:(int) -> (** to change the precision used to perform numeric computations *)
string list -> (** list of ".luc" file names *)
?main:(string option) -> (** main node name (for .lut files) *)
string list -> (** list of ".luc" or ".lut" file names *)
state
(** To indicate whether the point used to perform the step is
......
let make seed fair pp verbose precision files =
Luc4ocaml.make ~seed:seed ~fair:fair ~pp:pp ~verbose:verbose ~precision:precision files
let make seed fair pp verbose precision files mn_opt =
Luc4ocaml.make ~seed:seed ~fair:fair ~pp:pp ~verbose:verbose ~precision:precision files ~main:mn_opt
let step mode = Luc4ocaml.step ~mode:mode
......
......@@ -6,7 +6,8 @@ val make :
string -> (* in order to use a preprocessor before parsing *)
int -> (* verbose *)
int -> (* precision of the numeric computations *)
string list -> (* list of ".luc" file names *)
string list -> (* list of ".luc" or ".lut" file names *)
string option -> (* main node name (for .lut files) *)
state (* initial state of the machine *)
val step : step_mode -> state -> inputs -> state * solution
......
......@@ -803,8 +803,8 @@ let (make : string option -> string list -> Prog.t) =
prog
(* exported *)
let rec (make_state : string option -> string list -> Prog.state) =
fun pp_opt files ->
let rec (make_state : string option -> string list -> string option -> Prog.state) =
fun pp_opt files mn_opt ->
let lutfile_opt =
match files with
| file::rest ->
......@@ -814,10 +814,23 @@ let rec (make_state : string option -> string list -> Prog.state) =
if (Util.get_extension file <> ".lut") then
failwith (file ^ ": a .lut file is expected\n")
else
Some (file::rest,main)
(match mn_opt with
| None -> Some (file::rest,main)
| Some mn ->
Printf.eprintf "Warning: main node is specified twice. ";
Printf.eprintf "I will ignore %s and use %s\n" main mn;
flush stderr;
Some (file::rest,mn)
)
| file::files->
if Util.get_extension file = ".lut" then (
Some (file::rest,"main")
match mn_opt with
| None ->
Printf.eprintf "Warning: no main node is specified. ";
Printf.eprintf "I will us