Commit c7a6f554 authored by erwan's avatar erwan
Browse files

Allow the division by a constant in constraint.

I'm pretty sure this used to be supported. Why did I remove it?
unfortunately, the ne.ml file was not tracked by git (and by mistake)
at this time.

also, begin to replace lurettetop by rdbg -lurette in tests
parent 1d261ef2
OASISFormat: 0.4 OASISFormat: 0.4
Name: Lutin Name: Lutin
Version: 2.19 Version: 2.20
Authors: Erwan Jahier Authors: Erwan Jahier
Maintainers: erwan.jahier@imag.fr Maintainers: erwan.jahier@imag.fr
License: PROP License: PROP
......
...@@ -563,7 +563,7 @@ illustrated the [[file:local.lut][local.lut]] program: ...@@ -563,7 +563,7 @@ illustrated the [[file:local.lut][local.lut]] program:
#+begin_src sh :tangle sh/local-demo.sh :exports none :noweb yes #+begin_src sh :tangle sh/local-demo.sh :exports none :noweb yes
lutin local.lut -l 100 -o local.rif ; gnuplot-rif local.rif ; rm local.rif rm -f local.rif; lutin local.lut -l 100 -o local.rif && gnuplot-rif local.rif
#+end_src #+end_src
{{{run(./sh/local-demo.sh,lutin local.lut -l 100 -o local.rif ; gnuplot-rif local.rif)}}} {{{run(./sh/local-demo.sh,lutin local.lut -l 100 -o local.rif ; gnuplot-rif local.rif)}}}
...@@ -613,7 +613,7 @@ node bizzare() returns (res: real) = ...@@ -613,7 +613,7 @@ node bizzare() returns (res: real) =
#+begin_src sh :tangle sh/ext-call-demo.sh :exports none :noweb yes #+begin_src sh :tangle sh/ext-call-demo.sh :exports none :noweb yes
rm -f ext-call.rif rm -f ext-call.rif
lutin -L libm.so -l 200 -o ext-call.rif ext-call.lut lutin -L libm.so -l 200 -o ext-call.rif ext-call.lut && \
gnuplot-rif ext-call.rif gnuplot-rif ext-call.rif
#+end_src #+end_src
......
...@@ -797,7 +797,7 @@ html: At first step, the local variable ~target~ is chosen randomly ...@@ -797,7 +797,7 @@ html: At first step, the local variable ~target~ is chosen randomly
html. html.
#+begin_src sh :tangle sh/local-demo.sh :exports none :noweb yes #+begin_src sh :tangle sh/local-demo.sh :exports none :noweb yes
lutin local.lut -l 100 -o local.rif ; gnuplot-rif local.rif ; rm local.rif rm -f local.rif; lutin local.lut -l 100 -o local.rif && gnuplot-rif local.rif
#+end_src #+end_src
{{{run(./sh/local-demo.sh,lutin local.lut -l 100 -o local.rif ; gnuplot-rif local.rif)}}} {{{run(./sh/local-demo.sh,lutin local.lut -l 100 -o local.rif ; gnuplot-rif local.rif)}}}
...@@ -880,7 +880,7 @@ node bizzare() returns (res: real) = ...@@ -880,7 +880,7 @@ node bizzare() returns (res: real) =
#+begin_src sh :tangle sh/ext-call-demo.sh :exports none :noweb yes #+begin_src sh :tangle sh/ext-call-demo.sh :exports none :noweb yes
rm -f ext-call.rif rm -f ext-call.rif
lutin -L libm.so -l 200 -o ext-call.rif ext-call.lut lutin -L libm.so -l 200 -o ext-call.rif ext-call.lut && \
gnuplot-rif ext-call.rif gnuplot-rif ext-call.rif
#+end_src #+end_src
......
export OCAMLOPT=ocamlopt export OCAMLOPT=ocamlopt
LTOP=../../../bin/lurettetop$(EXE) LTOP=lurettetop_exe
LIB= `ocamlfind query -r rdbg-plugin -i-format` \ LIB= `ocamlfind query -r rdbg-plugin -i-format` \
`ocamlfind query -r lutin -i-format` `ocamlfind query -r lutin -i-format`
...@@ -8,7 +8,7 @@ MAIN=rabbit ...@@ -8,7 +8,7 @@ MAIN=rabbit
LURETTETOP=$(LTOP) --precision 2 \ LURETTETOP=$(LTOP) --precision 2 \
--test-length 500 --step-mode Inside --local-var --no-gnuplot --no-sim2chro \ --test-length 500 --step-mode Inside --local-var --no-gnuplot --no-sim2chro \
--do-not-show-step -v 2 --do-not-show-step -v 2
EXPDIR=`$(LTOP) --ocaml-version` EXPDIR=`$(LTOP) --ocaml-version`
$(EXPDIR): $(EXPDIR):
...@@ -32,6 +32,7 @@ test.rif:$(EXPDIR) rabbit.cmxs ...@@ -32,6 +32,7 @@ test.rif:$(EXPDIR) rabbit.cmxs
-rp 'env:lutin:rabbit.lut:-main:rabbit:-seed:34:-L:libm.so:-loc' && \ -rp 'env:lutin:rabbit.lut:-main:rabbit:-seed:34:-L:libm.so:-loc' && \
grep -v "lurette chronogram" test.rif0 | \ grep -v "lurette chronogram" test.rif0 | \
grep -v "lurette Version" | \ grep -v "lurette Version" | \
grep -v "#seed" | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif grep -v "The execution lasted"| sed -e "s/^M//" > test.rif
......
LTOP=../../../bin/lurettetop LTOP=lurettetop_exe
LURETTETOP=$(LTOP) \ LURETTETOP=$(LTOP) \
--test-length 100 --thick-draw 1 \ --test-length 100 --thick-draw 1 \
......
LTOP=../../../../bin/lurettetop
LURETTE=lurette \
LURETTETOP=$(LTOP) --precision 2 \ -sut "lus2lic heater_control.lus -n heater_control" \
-rp "sut:v6:heater_control.lus:heater_control" \ -oracle "lus2lic heater_control.lus -n not_a_sauna" \
-rp "oracle:v6:heater_control.lus:not_a_sauna" \ -env "lutin env.lut -n main -seed 3 -p 2"
-rp "env:lutin:env.lut:-n:main:-seed:3" \
--thick-draw 1 \ EXPDIR=`lurette --ocaml-version`
--draw-inside 0 --draw-edges 0 --draw-vertices 0 --draw-all-vertices \
--step-mode Inside --local-var --no-gnuplot --no-sim2chro \
--do-not-show-step
EXPDIR=`$(LTOP) --ocaml-version`
$(EXPDIR): $(EXPDIR):
[ -d $(EXPDIR) ] || (mkdir -p $(EXPDIR) ; make utest) [ -d $(EXPDIR) ] || (mkdir -p $(EXPDIR) ; make utest)
...@@ -18,7 +13,7 @@ $(EXPDIR): ...@@ -18,7 +13,7 @@ $(EXPDIR):
test.rif: test.rif:
rm -f test.rif .lurette_rc rm -f test.rif .lurette_rc
export GCC="/usr/bin/gcc -fPIC" export GCC="/usr/bin/gcc -fPIC"
$(LURETTETOP) --test-length 2 -go --output test.rif0 env.lut && \ $(LURETTE) --test-length 2 --output test.rif0 && \
grep -v "lurette chronogram" test.rif0 | \ grep -v "lurette chronogram" test.rif0 | \
grep -v "This is lurette Version" test.rif0 | grep -v "#seed " | \ grep -v "This is lurette Version" test.rif0 | grep -v "#seed " | \
grep -v "The execution lasted"| sed -e "s/^M//" > test.rif grep -v "The execution lasted"| sed -e "s/^M//" > test.rif
...@@ -34,16 +29,5 @@ utest: ...@@ -34,16 +29,5 @@ utest:
cp test.rif $(EXPDIR)/test.rif.exp cp test.rif $(EXPDIR)/test.rif.exp
clean: clean:
rm -rf *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp *.dro *_luciole.c test.res rm -rf *.ec *.log *~ .*~ *.o *rif0 *rif Data *.pp_luc *.plot *.gp *.dro *_luciole.c test.res luretteSession*
dontgo:
rm -f test.rif0 .lurette_rc
$(LTOP) --precision 2 \
-rp "sut:v6:heater_control.lus:heater_control" \
-rp "env:lutin:env.lut:-n:main:-seed:3" \
--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 env.lut --output test.rif
...@@ -814,7 +814,7 @@ let rec genpath ...@@ -814,7 +814,7 @@ let rec genpath
let acc = br.br_acc in let acc = br.br_acc in
let cont = br.br_cont in let cont = br.br_cont in
Verbose.exe Verbose.exe
~level:2 ~flag:dbg ~level:3 ~flag:dbg
(fun _ -> (fun _ ->
Printf.fprintf stderr "++REC_GENTRANS:\n" ; Printf.fprintf stderr "++REC_GENTRANS:\n" ;
Printf.fprintf stderr "|> CTRL: %s\n" (string_of_control_state br.br_ctrl); Printf.fprintf stderr "|> CTRL: %s\n" (string_of_control_state br.br_ctrl);
...@@ -1485,7 +1485,7 @@ let rec (genpath_ldbg : ...@@ -1485,7 +1485,7 @@ let rec (genpath_ldbg :
let acc = br.br_acc_ldbg in let acc = br.br_acc_ldbg in
let br_cont = br.br_cont_ldbg in let br_cont = br.br_cont_ldbg in
Verbose.exe Verbose.exe
~level:2 ~flag:dbg ~level:3 ~flag:dbg
(fun _ -> (fun _ ->
Printf.fprintf stderr "++REC_GENTRANS:\n" ; Printf.fprintf stderr "++REC_GENTRANS:\n" ;
Printf.fprintf stderr Printf.fprintf stderr
......
...@@ -273,7 +273,7 @@ let (modulo: t -> t -> t) = ...@@ -273,7 +273,7 @@ let (modulo: t -> t -> t) =
(****************************************************************************) (****************************************************************************)
let (div: t -> t -> t) = let (div_hide: t -> t -> t) =
fun ne1 ne2 -> fun ne1 ne2 ->
if if
is_a_constant ne1 && is_a_constant ne2 is_a_constant ne1 && is_a_constant ne2
...@@ -285,6 +285,33 @@ let (div: t -> t -> t) = ...@@ -285,6 +285,33 @@ let (div: t -> t -> t) =
else else
failwith ("*** arguments of 'div' should be known \n") failwith ("*** arguments of 'div' should be known \n")
let (div: t -> t -> t) =
fun ne1 ne2 ->
if is_a_constant ne2
then
let coeff = mfind "" ne2 in
if num_eq_zero coeff
then (
let ne_str = "("^(to_string ne1) ^ ") / (" ^ (to_string ne2) ^ ")" in
print_string ("\n*** Cannot divide by zero: "^ne_str^"\n");
flush stdout;
exit 2
)
else
( StringMap.fold
(fun vn value acc ->
StringMap.add vn (div_num value coeff) acc
)
ne1
StringMap.empty
)
else
let ne_str = "("^(to_string ne1) ^ ") / (" ^ (to_string ne2) ^ ")" in
print_string ("\n*** Cannot solve non-linear constraints: "^ne_str^"\n");
flush stdout;
exit 2
let (quot: t -> t -> t) = div let (quot: t -> t -> t) = div
(****************************************************************************) (****************************************************************************)
......
let str="2.19" let str="2.20"
let sha="4086b5c" let sha="1d261ef"
Supports Markdown
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