Commit 78e1cbf1 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

Some work on examples (use run, enhance the code, etc.)

parent fc42ba62
......@@ -380,8 +380,8 @@ LUTIN_FILES = \
$(OBJDIR)/autoGen.mli \
$(OBJDIR)/auto2Lucky.ml \
$(OBJDIR)/auto2Lucky.mli \
$(OBJDIR)/lutProg.mli \
$(OBJDIR)/lutProg.ml
$(OBJDIR)/lutProg.mli \
$(OBJDIR)/lutProg.ml
OCAMLMAKEFILE = $(LURETTE_PATH)/OcamlMakefile
......
export OCAMLOPT=ocamlopt
LTOP=../../../$(HOSTTYPE)/bin/lurettetop
LIB=../../../$(HOSTTYPE)/lib
MAIN=rabbit
CMXA_LIB = unix.cmxa str.cmxa bdd.cmxa polka.cmxa luc4ocaml.cmxa
CMA_LIB=luc4ocaml.cma
LUC4OCAML_INSTALL_DIR = -I ../../../$(HOSTTYPE)/lib
# LUC4OCAML_INSTALL_DIR = -I +lucky
NEW_LURETTETOP=$(LTOP) --precision 2 \
--test-length 500 --thick-draw 1 \
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-sim2chro --seed 3 \
--do-not-show-step
ifeq ($(HOSTTYPE),win32)
LD_ARCH=-DWIN32
endif
ifeq ($(HOSTTYPE),cygwin)
LD_ARCH=-DWIN32
endif
ifeq ($(HOSTTYPE),mac)
LD_ARCH=-DMAC
endif
%.cmxs: %.ml
ocamlopt -shared -o $*.cmxs -I $(LIB) graphics.cmxa ocamlRM.cmx rif_base.cmx $*.ml
$(MAIN).opt:$(MAIN).ml
ocamlopt.opt -cc g++ -cclib -lgmp $(LUC4OCAML_INSTALL_DIR) graphics.cmxa $(CMXA_LIB) $(MAIN).ml -o $(MAIN).opt
$(MAIN):$(MAIN).ml
ocamlc.opt $(LUC4OCAML_INSTALL_DIR) graphics.cma $(CMA_LIB) $(MAIN).ml -o $(MAIN)
demo: $(MAIN).opt
time ./$(MAIN).opt 50000 0.001 line
demo2: $(MAIN).opt
time ./$(MAIN).opt 10000 0.0 line
clean:
rm -f *.top *.cmi *.cmo *.cmx *.o *.cma *.cmxa *.a *.cmi *.cmo *.cmi *.cmx *.o *~ $(MAIN) $(MAIN).opt *~ *.pp_luc
test: clean $(MAIN).opt
./$(MAIN).opt 1000 0.0 test | grep -v "The random engine is initialized with the seed"
rm -f test.res && diff -B -u -i $(MAIN).out.exp $(MAIN).out > test.res && \
rm -rf *.ec *.cm* *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp $(MAIN).opt
test: rabbit.cmxs
rm -f test.rif0 .lurette_rc
$(NEW_LURETTETOP) -go --output test.rif0 \
-rp "sut:ocaml:rabbit.cmxs:" \
-rp "env:lutin:rabbit.lut:rabbit" && \
grep -v "lurette chronogram" test.rif0 | \
grep -v "lurette Version" | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif &&\
rm -f test.res && diff -u -i test.rif.exp test.rif > test.res
[ ! -s test.res ] && make clean
utest:
cp $(MAIN).out $(MAIN).out.exp
......
--------------------------------------------------------------------------------
let between(x, min, max : real) : bool = ((min < x) and (x < max))
let up_and_down(x, px : real ref; min, max, delta : real) =
if
(pre x < min) or ( (pre x < max) and (pre px <= pre x))
then
between(x, pre x, pre x + delta)
else
between(x, pre x - delta, pre x)
--------------------------------------------------------------------------------
system rabbit_speed () returns (Speed: real) =
exist Delta : real in
exist SpeedLow: real in
exist SpeedHigh: real in
exist pSpeed: real in
exist draw_params : bool in
exist compute_speed : bool in
let DeltaMin = 0.5 in
let DeltaMax = 1.0 in
let SpeedLowMin = 0.0 in
let SpeedLowMax = 5.0 in
let SpeedHighMin = 1.0 in
let SpeedHighMax = 20.0 in
pSpeed = 0.0 and Speed = 0.0
fby
assert pSpeed = pre Speed in
assert draw_params =
-- Choosing New values for parameters
(
DeltaMin < Delta and Delta < DeltaMax and
SpeedLowMin < SpeedLow and SpeedLow < SpeedLowMax and
SpeedHighMin < SpeedHigh and SpeedHigh < SpeedHighMax and
Speed = pre Speed
)
in
assert compute_speed =
(
SpeedLow = pre SpeedLow and
SpeedHigh = pre SpeedHigh and
Delta = pre Delta and
up_and_down(Speed, pSpeed, pre SpeedLow, pre SpeedHigh, pre Delta)
)
in
loop {
draw_params fby loop ~1000: 100 { compute_speed }
}
--------------------------------------------------------------------------------
-- XXX
--extern sin (x : real) : real : "libm.so"
--extern cos (x : real) : real : "libm.so"
let sin( x : real) : real = 0.5
let cos (x : real) : real = 0.5
system rabbit_dir (Speed, x_min, x_max, y_min, y_max : real)
returns(x, y: real) =
exist Alpha : real in
exist Beta : real in
exist draw_params : bool in
exist line : bool in
exist curve : bool in
let pi = 3.14 in
x = 250.0 and y = 250.0
fby
assert draw_params =
(
-3.14 < Alpha and Alpha <= 3.14 and
-0.3 < Beta and Beta <= 0.3 and
x = pre x and y = pre y
)
in
assert line =
(
x_min < x and x < x_max and
y_min < y and y < y_max and
x = (pre x + Speed * cos(pre Alpha)) and
y = (pre y + Speed * sin(pre Alpha)) and
Alpha = pre Alpha
)
in
assert curve =
(
x_min < x and x < x_max and
y_min < y and y < y_max and
x = (pre x + Speed * cos(pre Alpha)) and
y = (pre y + Speed * sin(pre Alpha)) and
Alpha = pre Alpha - Beta and
Beta = pre Beta
)
in
loop {
draw_params fby {
loop ~1000: 100 { line }
-- | loop ~1000: 100 { curve }
}
}
--------------------------------------------------------------------------------
--
--
-- --------------------------------------
-- | |
-- | |
-- | ----------------- |
-- | | 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)
system moving_obstacle3 (x_min, x_max, y_min, y_max : real)
returns (p1x, p1y, p2x, p2y, p3x, p3y, p4x, p4y : real) =
exist cx, cy, pcx, pcy : real in
let eps = 1.0 in
let cote_x = (x_max-x_min) / 6.0 in
let cote_y = (y_max-y_min) / 6.0 in
-- initial values
p1x = 249.0 and p1y = 249.0 and
p2x = 249.0 and p2y = 256.0 and
p3x = 256.0 and p3y = 256.0 and
p4x = 256.0 and p4y = 249.0 and
cx = 250.0 and cy = 250.0 and
pcx = 250.0 and pcy = 250.0
fby
assert pcx = pre cx in
assert pcy = pre cy in
loop{
-- each pi remains inside one of the small squares
pcx - cote_x < p1x and p1x < pcx and
pcy - cote_y < p1y and p1y < pcy and
pcx < p2x and p2x < pcx + cote_x and
pcy - cote_y < p2y and p2y < pcy and
pcx < p3x and p3x < pcx + cote_x and
pcy < p3y and p3y < pcy + cote_y and
pcx - cote_x < p4x and p4x < pcx and
pcy < p4y and p4y < pcy +cote_y and
-- 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 p1x - eps, pre p2x + eps) and
between(p2y, pre p1y - eps, pre p2y + eps) and
between(p3x, pre p1x - eps, pre p3x + eps) and
between(p3y, pre p1y - eps, pre p3y + eps) and
between(p4x, pre p1x - eps, pre p4x + eps) and
between(p4y, pre p1y - eps, pre p4y + eps) and
-- The center of the big square is moving, but inside the big square
up_and_down(cx, pcx, x_min + cote_x , x_max-cote_x, 3.0) and
up_and_down(cy, pcy, y_min + cote_y , y_max-cote_y, 2.0) and
true
}
system louis (b : bool)
returns (y, z : real) =
exist cx : real in
loop {
y = 0.0 and z = 0.0 and not b |>
{
loop {
y = 42.0
&>
z = 3.0
}
}
}
(*
--------------------------------------
| |
| |
| ----------------- |
| | 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)
*)
let between(x, min, max : real) : bool =
((min < x) and (x < max))
let up_and_down(x, px : real ref; min, max, delta : real) =
if (pre x < min) or (
(pre x < max) and (pre px <= pre x)
) then (
between(x, pre x, pre x + delta)
) else (
between(x, pre x - delta, pre x)
)
system moving_obstacle3 (
x_min : real;
x_max : real;
y_min : real;
y_max : real
) returns (
p1x : real;
p1y : real;
p2x : real;
p2y : real;
p3x : real;
p3y : real;
p4x : real;
p4y : real
) =
exist cx : real in
exist cy : real in
exist pcx : real in
exist pcy : real in
let eps = 1.0 in
let cote_x = (x_max-x_min) / 6.0 in
let cote_y = (y_max-y_min) / 6.0 in
-- initial values
p1x = 249.0 and p1y = 249.0 and
p2x = 249.0 and p2y = 256.0 and
p3x = 256.0 and p3y = 256.0 and
p4x = 256.0 and p4y = 249.0 and
cx = 250.0 and cy = 250.0 and
pcx = 250.0 and pcy = 250.0
fby
assert pcx = pre cx in
assert pcy = pre cy in
loop{
-- each pi remains inside one of the small squares
pcx - cote_x < p1x and p1x < pcx and
pcy - cote_y < p1y and p1y < pcy and
pcx < p2x and p2x < pcx + cote_x and
pcy - cote_y < p2y and p2y < pcy and
pcx < p3x and p3x < pcx + cote_x and
pcy < p3y and p3y < pcy + cote_y and
pcx - cote_x < p4x and p4x < pcx and
pcy < p4y and p4y < pcy +cote_y and
-- 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 p1x - eps, pre p2x + eps) and
between(p2y, pre p1y - eps, pre p2y + eps) and
between(p3x, pre p1x - eps, pre p3x + eps) and
between(p3y, pre p1y - eps, pre p3y + eps) and
between(p4x, pre p1x - eps, pre p4x + eps) and
between(p4y, pre p1y - eps, pre p4y + eps) and
-- The center of the big square is moving, but inside the big square
up_and_down(cx, pcx, x_min + cote_x , x_max-cote_x, 3.0) and
up_and_down(cy, pcy, y_min + cote_y , y_max-cote_y, 2.0) and
true
}
\ No newline at end of file
system rabbit
inputs {}
outputs {
Speed : float ~init 0.0
}
locals {
-- should be an input
stress : bool ~alias false;
Delta : float;
DeltaMin : float ~ alias 0.5;
DeltaMax : float ~ alias 1.0;
SpeedLow : float;
SpeedLowMin : float ~ alias 0.0;
SpeedLowMax : float ~ alias 5.0;
SpeedHigh : float;
SpeedHighMin : float ~ alias 1.0;
SpeedHighMax : float ~ alias 20.0;
Cpt : int;
}
nodes {
init : stable;
drawing : transient;
running : stable;
}
start_node { init }
transitions {
init -> drawing;
drawing -> running
~cond
-- Drawing the slope (Delta), the lower, and the upper bound of the speed
DeltaMin < Delta and Delta < DeltaMax and
SpeedLowMin < SpeedLow and SpeedLow < SpeedLowMax and
SpeedHighMin < SpeedHigh and SpeedHigh < SpeedHighMax and
Speed = pre Speed and Cpt = 0 ;
running -> running
~weight 1000 - (pre Cpt)
~cond
SpeedLow = pre SpeedLow and
SpeedHigh = pre SpeedHigh and
Delta = pre Delta and
up_and_down(Speed, pre SpeedLow, pre SpeedHigh, pre Delta) and
Cpt = pre(Cpt) + 1 ;
running -> drawing
~weight 10
~cond Speed = pre Speed;
}
(*
Demonstrate the use of Lutin from Ocaml.
Confere the Makefile for building and use.
*)
open Luc4ocaml
let _ =
if (Array.length Sys.argv <> 4) then
(
print_string "usage: rabbit <step nb> <step delay> <line|dot>
where
<step nb> is the number of steps to perform
<step delay> is a delay to introduce between each step (otherwise,
the rabbit is to quick and one can not see
that its speed is varying)
<line|dot> is to indicate whether to use lines or dots to draw
the rabbit trajectory.
e.g.: rabbit 10000 0.0 line
then type 'g' to go to the next demo.
\n";
exit 1
)
(**************************************************************************)
(* Utilities *)
let draw x y =
if Sys.argv.(3) = "dot" then
Graphics.plot (truncate x) (truncate y)
else
(* if Sys.argv.(3) = "dot" then *)
(* Graphics.plot (truncate x) (truncate y) *)
(* else *)
Graphics.lineto (truncate x) (truncate y)
let get_float var sol =
try
match (List.assoc var sol) with F f -> f | _ -> assert false
with Not_found ->
open Rif_base
let get_float var sol =
match (
try List.assoc var sol with Not_found -> assert false
) with (F f) -> f | _ ->
Printf.printf "*********************\n";
flush stdout;
assert false
let det ((p1x,p1y),(p2x,p2y),(p3x,p3y),(p4x,p4y)) =
((p2x-.p1x)*.(p4y-.p3y)-.(p2y-.p1y)*.(p4x-.p3x))
(**************************************************************************)
(* Main loop for demo 1 and 2 *)
let rec main_loop rs rd i delay =
(* Get the size of the Graphics window *)
let x_min = F (float_of_int 0)
and x_max = F (float_of_int (Graphics.size_x ()))
and y_min = F (float_of_int 0)
and y_max = F (float_of_int (Graphics.size_y ()))
in
let bounds = [("x_min", x_min);("x_max",x_max);("y_min",y_min);("y_max",y_max)] in
(* Performing the steps *)
let (rs', (speed, _rs_locals)) = Luc4ocaml.step rs [] in
let (rd', (dir, _rd_locals)) = Luc4ocaml.step rd (bounds@speed) in
(* Drawing the new point onto the Graphics window *)
let x = get_float "x" dir in
let y = get_float "y" dir in
if Graphics.key_pressed () && (Graphics.read_key () = 'g') then () else
(
if delay <> "0.0" then ignore (Sys.command ("sleep " ^ delay));
draw x y;
if i > 0 then main_loop rs' rd' (i-1) delay
)
let poly_mem = ref [|(0,0)|]
(**************************************************************************)
(* Main loop for demo 3 and 4 *)
let oc = open_out "toto"
let rec main_loop_obstacle rs rd ro i delay =
(* Get the size of the Graphics window *)
let x_min = F (float_of_int 0)
and x_max = F (float_of_int (Graphics.size_x ()))
and y_min = F (float_of_int 0)
and y_max = F (float_of_int (Graphics.size_y ())) in
let bounds = [("x_min", x_min);("x_max",x_max);("y_min",y_min);("y_max",y_max)] in
(* Performing the steps *)
let (rs', (speed, _)) = Luc4ocaml.step rs [] in
let (ro', (obstacle_points, _)) = Luc4ocaml.step ro (bounds) in
let (rd', (dir, _)) = Luc4ocaml.step rd (bounds@speed@obstacle_points) in
(* Drawing the new point onto the Graphics window *)
let x = get_float "x" dir
and y = get_float "y" dir
and p1x = get_float "_p1x" obstacle_points
and p2x = get_float "_p2x" obstacle_points
and p3x = get_float "_p3x" obstacle_points
and p4x = get_float "_p4x" obstacle_points
and p1y = get_float "_p1y" obstacle_points
and p2y = get_float "_p2y" obstacle_points
and p3y = get_float "_p3y" obstacle_points
and p4y = get_float "_p4y" obstacle_points
in
let p1xI = truncate p1x
and p1yI = truncate p1y
and p2xI = truncate p2x