Commit 7344d9ba authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.80 Mon, 02 Sep 2002 16:07:51 +0200 by jahier

Parent-Version:      0.79
Version-Log:

source/control.ml:
source/parse_env.ml:
    Add a new ctrl expr (set_between) to let one set the value of a CE var
    in such a way that it is backtracable within an interval. One rational
    is that it let ones code infinite loops that can be exited when
    the formula is false.

Project-Description: Lurette
parent 0f7c0947
......@@ -29,10 +29,10 @@
(test/passerelle.ima 972 1027066799 b/17_passerelle 1.7)
(source/ima_exe.ml 11903 1030614411 b/32_ima_exe.ml 1.16)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/control.ml 4179 1030627155 c/4_control.ml 1.1)
(source/control.ml 4333 1030975671 c/4_control.ml 1.2)
(source/eval.ml 7755 1027066799 49_eval.ml 1.13)
(source/gen_stubs.ml 33359 1030614411 24_generate_l 1.30)
(source/parse_env.ml 22055 1030627155 41_parse_env. 1.21)
(source/parse_env.ml 22235 1030975671 41_parse_env. 1.22)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/automata.mli 3397 1027349504 b/46_automata.m 1.2)
(source/sim2chro.ml 2720 1027943375 b/24_sim2chro.m 1.10)
......@@ -48,13 +48,13 @@
(test/usager.ima 493 1027066799 b/14_usager.env 1.8)
(README 74 1011881677 10_README 1.2)
(test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
(OcamlMakefile 25170 1030627155 17_OcamlMakef 1.36)
(OcamlMakefile 25248 1030975671 17_OcamlMakef 1.37)
(source/command_line_ima_exe.ml 2792 1021651153 b/33_command_li 1.4)
(test/ControleurPorte.rif.exp 4756 1028297733 b/29_Controleur 1.8)
(Makefile.lurette 609 1030614411 b/38_Makefile.l 1.8)
(source/show_env.ml 3603 1030532285 43_show_env.m 1.12)
(source/gne.mli 1079 1027066799 b/36_gne.mli 1.2)
(source/automata.ml 15708 1027349504 b/47_automata.m 1.2)
(source/automata.ml 15814 1030975671 b/47_automata.m 1.3)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(bin/Makefile.lurette_lib 1765 1030525986 c/2_Makefile.l 1.1)
(bin/Makefile.gen_stubs 472 1030532285 b/42_Makefile.g 1.2)
......@@ -69,7 +69,7 @@
(test/heater_float.lus 175 1020068208 b/44_heater_flo 1.1)
(test/vrai_tram.c 3060 1027066799 b/8_vrai_tram. 1.3)
(source/print.mli 773 1027066799 46_print.mli 1.10)
(source/lurettetop.ml 16570 1030614411 c/1_lurettetop 1.3)
(source/lurettetop.ml 18331 1030975671 c/1_lurettetop 1.5)
(test/heater_int.lus 170 1020068208 b/43_heater_int 1.1)
(source/graph.mli 2218 1027066799 13_graph.mli 1.9)
(test/heater_int.rif.exp 860 1028297733 b/28_heater_int 1.6)
......@@ -78,4 +78,4 @@
(source/print.ml 5883 1030532285 47_print.ml 1.18)
(test/vrai_tram.h 2468 1027066799 b/7_vrai_tram. 1.3)
(bin/Makefile.show_ima 1039 1027066799 b/40_Makefile.s 1.4)
(source/control.mli 2978 1030627155 c/3_control.ml 1.1)
(source/control.mli 3202 1030975671 c/3_control.ml 1.2)
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.36 Thu, 29 Aug 2002 15:19:15 +0200 jahier $
# $Id: OcamlMakefile 1.37 Mon, 02 Sep 2002 16:07:51 +0200 jahier $
#
###########################################################################
# Set these variables to the names of the sources to be processed and
......@@ -570,6 +570,9 @@ test3:
test: test1 test2 test3
ls -l test1.res test2.res test3.res
lib:
pushd ~/lurette/bin ; make -f Makefile.lurette_lib OCAMLFLAGS=""; popd
ima:
pushd ~/lurette/bin ; make -k dc -f Makefile.ima_exe OCAMLFLAGS=""; popd
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 79)
(Parent-Version lurette 0 78)
(Project-Version lurette 0 80)
(Parent-Version lurette 0 79)
(Version-Log "
source/lurettetop.ml:
Add a pack command and a --restore option to lurettetop that respectively
save temporarily created files during a session and restore them
later on.
Also clean-up temporarily created files when lurettetop resumes.
source/control.ml:
source/parse_env.ml:
Add a new ctrl expr (set_between) to let one set the value of a CE var
in such a way that it is backtracable within an interval. One rational
is that it let ones code infinite loops that can be exited when
the formula is false.
")
(New-Version-Log "")
(Checkin-Time "Thu, 29 Aug 2002 16:55:47 +0200")
(Checkin-Time "Mon, 02 Sep 2002 16:07:51 +0200")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -53,7 +54,7 @@ source/lurettetop.ml:
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.6 644))
(source/parse_env.mli (lurette/40_parse_env. 1.9 644))
(source/parse_env.ml (lurette/41_parse_env. 1.21 644))
(source/parse_env.ml (lurette/41_parse_env. 1.22 644))
(source/show_env.mli (lurette/42_show_env.m 1.7 644))
(source/show_env.ml (lurette/43_show_env.m 1.12 644))
......@@ -71,7 +72,7 @@ source/lurettetop.ml:
(source/env_state.ml (lurette/51_env_state. 1.25 644))
(source/automata.mli (lurette/b/46_automata.m 1.2 644))
(source/automata.ml (lurette/b/47_automata.m 1.2 644))
(source/automata.ml (lurette/b/47_automata.m 1.3 644))
(source/sim2chro.mli (lurette/b/23_sim2chro.m 1.5 644))
(source/sim2chro.ml (lurette/b/24_sim2chro.m 1.10 644))
......@@ -79,17 +80,17 @@ source/lurettetop.ml:
(source/gne.mli (lurette/b/36_gne.mli 1.2 644))
(source/gne.ml (lurette/b/37_gne.ml 1.2 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.4 644))
(source/lurettetop.ml (lurette/c/1_lurettetop 1.5 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.30 644))
(source/control.mli (lurette/c/3_control.ml 1.1 644))
(source/control.ml (lurette/c/4_control.ml 1.1 644))
(source/control.mli (lurette/c/3_control.ml 1.2 644))
(source/control.ml (lurette/c/4_control.ml 1.2 644))
; little script that sets env vars and starts the lurette build
(make_lurette (lurette/27_make_luret 1.15 755))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.36 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.37 644))
(Makefile.lurette (lurette/b/38_Makefile.l 1.8 644))
(bin/Makefile.show_ima (lurette/b/40_Makefile.s 1.4 644))
......
......@@ -168,6 +168,8 @@ and
)
tnl
and
(* We only keep transitions which weigth is positive and one that
<<could have been>> positive. *)
(is_pos_or_recoverable_var : weight -> Control.state -> bool) =
fun w st ->
match w with
......
......@@ -76,6 +76,11 @@ let (set : string -> int -> state -> state) =
fun id i st ->
StringMap.add id (i, None) st
(* exported *)
let (set_between : string -> int -> int -> int -> state -> state) =
fun id i min max st ->
StringMap.add id (i, Some(min, max)) st
(* exported *)
let (draw_between : string -> int -> int -> state -> state) =
......
......@@ -24,6 +24,11 @@ val compose_state : state -> state -> state
val set : string -> int -> state -> state
(** [set id i st] sets [id] to [i] in [st]. *)
val set_between : string -> int -> int -> int -> state -> state
(** [set id i min max st] sets [id] to [i] in [st], but allow values
between [min] and [max] if no more transition can be made from the
current state. *)
val draw_between : string -> int -> int -> state -> state
(** [loop_between id min max] sets [id] to a value uniformally drawn
between [min] and [max] in [st]. *)
......
......@@ -246,6 +246,7 @@ let rec
| [< 'Genlex.Ident "run" >] -> Run
| [< 'Genlex.Ident "r" >] -> Run
| [< 'Genlex.Ident "show" >] -> Show
| [< 'Genlex.Ident "b" >] -> Build
| [< 'Genlex.Ident "build" >] -> Build
| [< 'Genlex.Ident "clean" >] -> Clean
| [< 'Genlex.Ident "set_sut" ; 'Genlex.Ident str >] -> Sut(str)
......@@ -336,8 +337,8 @@ let (display_cmd : unit -> unit) =
run, r
to start the testing process. Note that the sut and the environment
fields (described below) should be set.
fields (described below) should be set.
quit q, bye
to quit the lurette top level
......
......@@ -365,6 +365,10 @@ and (parse_ctrl_expr: aut_token -> Control.expr) =
[< 'Genlex.Ident "Set" ; 'Genlex.Ident varname ; 'Genlex.Int i
>] ->
(Control.set varname i)
| [< 'Genlex.Ident "Set_between" ; 'Genlex.Ident varname ;
'Genlex.Int i ; 'Genlex.Int min ; 'Genlex.Int max
>] ->
(Control.set_between varname i min max)
| [< 'Genlex.Ident "Draw_between" ; 'Genlex.Ident varname ;
'Genlex.Int min ; 'Genlex.Int max
>] ->
......
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