Commit 4aed6dc3 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.1 Mon, 08 Sep 2003 16:02:09 +0200 by jahier

Parent-Version:      0.143
Version-Log:

Major change in the lucky syntax.

Also add structured types (in lucky only, for the time being).

Project-Description: Lurette
parent 2b40538c
This diff is collapsed.
*********** BUGS
:-)
* ZZZ une contrainte du style "0<x<100 and x<>2" va tirer "1" une fois sur 2 !!!
car "x<>2" est traduit en "x<2 or x>2" et le choix sur le or est effectué de
facon équitable ...
En particulier, je ne peux donc pas representer des enum par des entiers...
=> Solution on remonte du bdd le nombre de solutions entieres presentes
a chaque feuille.
pour cela, je dois changer un peu de philosophie (cf solver.ml).
Avant:
1- calcul du nombre de solutions d'un point de vue Booleen
2- tirage dans le bdd tenant compte des poids obtenu en (1)
en verifiant au fur et a mesure les contraintes numeriques
faciles, a savoir celles de dimensions 1
3- une fois aux feuilles, s'il reste des contraintes de dimensions > 1,
faire appel à Polka.
Apres:
1- calcul du nombre de solutions d'un point de vue Booleen ET
des variables numériques de dimension 1.
2- tirage dans le bdd tenant compte des poids obtenu en (1)
3- comme avant
en d'autre termes, je fais la vérif de satisfiabilité des intervalles
lors du calcul du nombre de solutions, et pas lors du tirage dans le bdd.
*********** A faire maintenant
* install: gnuplot-rif n'est pas dans le path
* Nouvelle syntaxe pour lucky
*********** A faire maintenant
* renommer les scripts et les executables comme suit:
- les noeuds sont des string
- les formules ont la syntaxe lustre
- syntaxe concrete :
xlurette -> xlurette_exe
xlurette.sh -> xlurette
les declarations de types:
et ainsi de suite ...
typedef {
Ident : TypeExp ;
ex_array : bool ^ 3 ;
ex_struct : {a:bool; b: float} ;
ex_enum : (bleu, blanc, rouge) ;
}
* rajouter un jeu de test testant les types structures ainsi que la
nouvelle syntaxe (gestions des poids dynamique, etc.)
les declarations de variables:
inputs { -- (resp output, locals)
Ident : type [-Flag = Exp ]* ;
* Integrer la possibilité d'utiliser des types structurés avec lurette et scade
v : float -min 1 -max 10 -default 5 ;
u : bool -alias (v > 6) ;
}
* Faire un lustre2lucky comme TP avec Yussef
Exp = Feuille | ( Arbre )
* Faire l'elimination des DAGS, ie,
finir la fonction duplicate_graph_from_node automata.ml
Flag = -min | -max | -default | -alias
* faire un passage sur map vs rev_map
Les noeuds :
InitialNode ::=
initial { Ident }
* documenter les options ~default, ~alias, etc.
Nodes ::=
nodes {
Ident : <stable | transient> [-NodeFlag = Value]* ;
}
* Signaler les approximations faites (en dimension > 1)
- volumes des polyhedres pas calculés (=> pb d'equité)
- pour le choix des entiers, on travaille dans les reels,
puis on tronque (truncate) => l'entier tiré n'est alors parfois
meme pas solution des contraintes !!!
N.B. pour l'instant pas de NodeFlag
* dire dans la doc que on ne peut avoir qu'au plus une transition sortante
avec un poids infini (ca n'a pas un sens bien clair et on peut toujours
faire autrement). Dire aussi que 2 transitions ne peuvent a la fois avoir
meme origine et arrivée.
Les transitions :
Transitions ::=
transitions {
Ident -> Ident [-TransFlag = Exp]* ;
ex_etat1 -> ex_etat2 -weight 3 -formula (x >= 4)
}
* ajouter les options --product-mode {multiply | arbiter}
qui disent comment on multiplie 2 automates (cf papier)
* env_state devrait etre un objet ...
(1) Portage pour scade, esterel ...
-> structure, tableau, types structures, etc.
(1) Portage Reluc
......@@ -146,8 +162,6 @@ Les transitions :
* Ecrire une batterie de test plus sérieuse !
* Ecrire un papier qui explique la transformation en automate.
* Réfléchir à une version d'un tireur sans bdd ou les choix seraient
effectués pendant le parcours de la formule (pas d'équité, mais bon) +
......
inputs = (Heat_on , bool),
outputs = (U,float),
locals = (Dudt ,float),
pre = (pre(1,U),float); (pre(1, Dudt), float) ,
ctrl_expr = ,
start_node = 0,
arcs_nb = 0,
nodes_nb = 0,
arcs =
From 0 To 1 With 1:(&& (= U 17.5) (= Dudt 0.1)) ;
From 1 To 1 With
1:
( && (= U pre(1,U) + pre(1, Dudt))
&& ( > Dudt (IfThenElseNum Heat_on 0. (- 5.)))
( < Dudt (IfThenElseNum Heat_on 2. 0.) )
) .
inputs {
Heat_on %this_a_label:this is a pragma%
%this_is_another_label: "and this is another pragma"%
: bool
}
outputs {
U:real ~min 1. ~max 60
}
locals {
Dudt %scr:15,2,16,2% %foo:bar%
: float ~min -100. ~max 100.
}
start_node { 0 }
nodes {
}
transitions {
0 -> %titi: transition pragma %
1 ~cond ((U = 17.0) and (Dudt = 0.0)) ;
1 -> 1 ~cond
%toto:this is a formula pragma%
-- %titi: this is an other one %
((U = pre(U) + pre(Dudt)) and
(Dudt > (if Heat_on then 0.0 else -5.0))
and
( (1.0 * Dudt + 0.0) < (if Heat_on then 2.0 else 0.0)))
}
......@@ -1326,13 +1326,13 @@ let toolbar8 = GButton.toolbar
()
in
let sim2chro = toolbar8#insert_button
~text: "sim2chro"
~text: "View with sim2chro"
~icon:(GMisc.pixmap (GDraw.pixmap_from_xpm ~file:((Unix.getenv "PIXMAP_DIR") ^ "chrono.xpm") ()) ())#coerce
()
in
let _ = tooltips#set_tip ~text:"Call sim2chro with the selected file" sim2chro#coerce in
let button39 = toolbar8#insert_button
~text: "gnuplot "
~text: "View with gnuplot "
~icon:(GMisc.pixmap (GDraw.pixmap_from_xpm ~file:((Unix.getenv "PIXMAP_DIR") ^ "gnuplot-rif.xpm") ()) ())#coerce
()
in
......@@ -1343,6 +1343,11 @@ let delete_rif_button = toolbar8#insert_button
()
in
let _ = tooltips#set_tip ~text:"Delete selected file" delete_rif_button#coerce in
let edit_rif = toolbar8#insert_button
~text: "Edit "
~icon:(GMisc.pixmap (GDraw.pixmap_from_xpm ~file:((Unix.getenv "PIXMAP_DIR") ^ "open.xpm") ()) ())#coerce
()
in
let label27 = GMisc.label
~text: "This page does not work yet, sorry"
~packing:(vbox15#pack ~padding:0
......@@ -1535,6 +1540,7 @@ method toolbar8 = toolbar8
method sim2chro = sim2chro
method button39 = button39
method delete_rif_button = delete_rif_button
method edit_rif = edit_rif
method label27 = label27
method time_diagrams_label = time_diagrams_label
initializer callbacks#set_xlurette self;
......@@ -2209,25 +2215,6 @@ let extra_includedirs_label = GMisc.label
~line_wrap:false
()
in
let extra_cfiles_entry = GEdit.entry
~packing:(table7#attach ~left:1
~top:0
~right:2
~bottom:1
~xpadding:0
~ypadding:0
~expand:`X
~shrink:`NONE
~fill:`X
)
~width:400
~max_length:0
~visibility:true
~editable:true
()
in
let _ = GtkBase.Widget.set_can_focus extra_cfiles_entry#as_widget true in
let _ = tooltips#set_tip ~text:"Set the EXTRA_CFILES environment variable. May be necessary if the sut or the oracle uses external C files " extra_cfiles_entry#coerce in
let extra_libs_entry = GEdit.entry
~packing:(table7#attach ~left:1
~top:1
......@@ -2374,6 +2361,25 @@ let button66 = toolbar19#insert_button
()
in
let _ = tooltips#set_tip ~text:"Browse for a directory" button66#coerce in
let extra_cfiles_entry = GEdit.entry
~packing:(table7#attach ~left:1
~top:0
~right:2
~bottom:1
~xpadding:0
~ypadding:0
~expand:`X
~shrink:`NONE
~fill:`X
)
~width:400
~max_length:0
~visibility:true
~editable:true
()
in
let _ = GtkBase.Widget.set_can_focus extra_cfiles_entry#as_widget true in
let _ = tooltips#set_tip ~text:"Set the EXTRA_CFILES environment variable. May be necessary if the sut or the oracle uses external C files " extra_cfiles_entry#coerce in
let vbox22 = GPack.vbox
~spacing:0
~homogeneous:true
......@@ -2440,7 +2446,6 @@ method extra_cfiles_label = extra_cfiles_label
method extra_libs_label = extra_libs_label
method extra_libdirs_label = extra_libdirs_label
method extra_includedirs_label = extra_includedirs_label
method extra_cfiles_entry = extra_cfiles_entry
method extra_libs_entry = extra_libs_entry
method extra_libdirs_entry = extra_libdirs_entry
method extra_includedirs_entry = extra_includedirs_entry
......@@ -2452,6 +2457,7 @@ method toolbar18 = toolbar18
method button65 = button65
method toolbar19 = toolbar19
method button66 = button66
method extra_cfiles_entry = extra_cfiles_entry
method vbox22 = vbox22
method vbox23 = vbox23
method hbox20 = hbox20
......
This diff is collapsed.
This diff is collapsed.
matrix.cmi: vector.cmi
poly.cmi: matrix.cmi vector.cmi
polka.cmo: polka.cmi
polka.cmx: polka.cmi
vector.cmo: polka.cmi polka_lexer.cmi polka_parser.cmi vector.cmi
vector.cmx: polka.cmx polka_lexer.cmi polka_parser.cmx vector.cmi
matrix.cmo: polka.cmi vector.cmi matrix.cmi
matrix.cmx: polka.cmx vector.cmx matrix.cmi
poly.cmo: matrix.cmi vector.cmi poly.cmi
poly.cmx: matrix.cmx vector.cmx poly.cmi
polka_parser.cmo: polka.cmi polka_parser.cmi
polka_parser.cmx: polka.cmx polka_parser.cmi
polka_parser.cmi: polka.cmi
polka_lexer.cmi: polka_parser.cmi
polkaIO.cmo: matrix.cmi polka.cmi poly.cmi vector.cmi polkaIO.cmi
polkaIO.cmx: matrix.cmx polka.cmx poly.cmx vector.cmx polkaIO.cmi
polkaIO.cmi: matrix.cmi poly.cmi vector.cmi
......@@ -60,8 +60,8 @@ SCADE_OS_NAME=@SCADE_OS_NAME@
LINKER= cc
STRIP= strip
CFLAGS= #-xO3 -Xc -DSIM
CFLAGS_0= #-Xc -DSIM
CFLAGS= -O2 -DSIM #-xO3 -Xc -DSIM
CFLAGS_0= -O -DSIM #-Xc -DSIM
MEMORIES=$(SCADE_INSTALL_DIR)/lib/memories.c
......
......@@ -274,9 +274,9 @@ mv $LURETTEPATH/share/lucky_init.csh $LURETTEPATH/$HOST_TYPE/lucky_init.csh
case "$HOST_TYPE" in
cygwin)
mv $LURETTEPATH/share/lurettetop.bat $LURETTEPATH/$HOST_TYPE/bin
mv $LURETTEPATH/share/xlurette.bat $LURETTEPATH/$HOST_TYPE/bin
mv $LURETTEPATH/share/lucky.bat $LURETTEPATH/$HOST_TYPE/bin
cp $LURETTEPATH/share/lurettetop.bat $LURETTEPATH/$HOST_TYPE/bin
cp $LURETTEPATH/share/xlurette.bat $LURETTEPATH/$HOST_TYPE/bin
cp $LURETTEPATH/share/lucky.bat $LURETTEPATH/$HOST_TYPE/bin
;;
esac
......@@ -284,9 +284,11 @@ esac
chmod a+x lurettetop.sh
chmod a+x xlurette.sh
chmod a+x lucky.sh
mv $LURETTEPATH/share/lurettetop.sh $LURETTEPATH/$HOST_TYPE/bin
mv $LURETTEPATH/share/xlurette.sh $LURETTEPATH/$HOST_TYPE/bin
mv $LURETTEPATH/share/lucky.sh $LURETTEPATH/$HOST_TYPE/bin
cp $LURETTEPATH/share/lurettetop.sh $LURETTEPATH/$HOST_TYPE/bin
cp $LURETTEPATH/share/xlurette.sh $LURETTEPATH/$HOST_TYPE/bin
cp $LURETTEPATH/share/lucky.sh $LURETTEPATH/$HOST_TYPE/bin
cp $LURETTEPATH/share/gnuplot-rif $LURETTEPATH/$HOST_TYPE/bin
cp $LURETTEPATH/share/plot $LURETTEPATH/$HOST_TYPE/bin
echo
echo " Installation terminated."
......
......@@ -19,8 +19,8 @@ if test -f $FILE ;
rm -f $FILE.gp $FILE.plot
echo "#@set data style steps" > $FILE.gp
echo "#@t=1" >> $FILE.gp
# echo "#@set data style steps" > $FILE.gp
echo "#@t=1" > $FILE.gp
echo "#@f=0" >> $FILE.gp
sed -e 's/:bool/ | /g' $FILE \
......
......@@ -19,17 +19,16 @@
"Regular expression used by Font-lock mode.")
(setq lucky-font-lock-keywords
'(
;;("*$" . font-lock-comment-face)
'(("--.*$" . font-lock-comment-face)
("\\<\\(weight\\|max\\|min\\|default\\|cond\\|max\\|With\\)\\>" . font-lock-string-face)
("\\<\\(weight\\|max\\|min\\|default\\|alias\\|init\\|cond\\|max\\|With\\)\\>" . font-lock-string-face)
("\\<\\(IfThenElse\\|IfThenElseNum\\|Dec\\|Return_not_sig\\|Return_sig\\|Draw_between\\|Draw_gauss\\|Set\\|Set_between\\|+\\|*\\|-\\|/\\|mod\\)\\>"
. font-lock-keyword-face)
("[][;,()|{}@^!:#*=<>&/%+~?---]\\.?\\|\\.\\." . font-lock-function-name-face)
("\\<\\(true\\|and\\|or\\|if\\|then\\|else\\|pre\\|and\\|and\\|||\\|not\\|false\\|eps\\|!\\)\\>" . font-lock-reference-face)
("\\<\\(bool\\|int\\|real\\|float\\)\\(\\^.+\\)?\\>" . font-lock-variable-name-face)
("\\(\\<\\(inputs\\|outputs\\|alias_def\\|start_node\\|alias\\|locals\\|transitions\\|start_node\\|transient\\|stable\\|arcs_nb\\|nodes_nb\\|=\\)\\>\\|->\\)" .
("\\(\\<\\(inputs\\|outputs\\|typedef\\|alias_def\\|start_node\\|nodes\\|locals\\|transitions\\|start_node\\|transient\\|stable\\|arcs_nb\\|nodes_nb\\|=\\)\\>\\|->\\)" .
font-lock-function-name-face)))
......
......@@ -6,8 +6,8 @@
setenv LURETTE_PATH @LURETTEPATH@
setenv PIXMAP_DIR @PIXMAP_DIR@
set path=(@LURETTEPATH@/@HOST_TYPE@/bin $path)
set PATH=(@LURETTEPATH@/@HOST_TYPE@/bin $PATH)
set path=(@LURETTEPATH@/@HOST_TYPE@/bin @LURETTEPATH@/share $path)
set PATH=(@LURETTEPATH@/@HOST_TYPE@/bin @LURETTEPATH@/share $PATH)
setenv PS_VIEWER @GV@
setenv DOT @LURETTEPATH@/@HOST_TYPE@/bin/dot
......
......@@ -7,8 +7,8 @@ set LURETTE_PATH=@LURETTEPATH@
set PIXMAP_DIR=@PIXMAP_DIR@
set path=@LURETTEPATH@/@HOST_TYPE@/bin:$path
set PATH=@LURETTEPATH@/@HOST_TYPE@/bin:$PATH
set path=@LURETTEPATH@/@HOST_TYPE@/bin:@LURETTEPATH@/share:$path
set PATH=@LURETTEPATH@/@HOST_TYPE@/bin:@LURETTEPATH@/share:$PATH
set PS_VIEWER=@GV@
set DOT=@LURETTEPATH@/@HOST_TYPE@/bin/dot
......
......@@ -140,6 +140,11 @@ libnc:
rm -f liblurette_lib_nc.a
make liblurette_lib_nc.a
libnc_no_clean:
make nc -f Makefile.lurette_lib OCAMLFLAGS="-noassert -unsafe"
rm -f liblurette_lib_nc.a
make liblurette_lib_nc.a
libbc:
rm -f lurette_lib.o
make bc -f Makefile.lurette_lib OCAMLFLAGS=""
......@@ -230,6 +235,9 @@ stubs_assert:
gen_lut:
make -k nc -f Makefile.gen_fake_lutin OCAMLFLAGS="-noassert -unsafe"
gen_luc:
make -k nc -f Makefile.gen_fake_lucky OCAMLFLAGS="-noassert -unsafe"
gen_lut_assert:
make -k nc -f Makefile.gen_fake_lutin OCAMLFLAGS=""
mv gen_fake_lutin gen_fake_lutin_assert
......@@ -237,21 +245,22 @@ gen_lut_assert:
xlurette:
cd $(HOME)/lurette/ihm/xlurette; \
make opt ; cp xlurette ../../$(HOST_TYPE)/bin
make opt ; cp xlurette$(EXE) ../../$(HOST_TYPE)/bin
all_assert: lucky_assert ltop_assert show_assert stubs_assert gen_lut_assert
all: libnc lucky ltop show stubs gen_lut xlurette
all: libnc lucky ltop show stubs gen_lut gen_luc xlurette
clean_exe:
rm -i gen_stubs lucky lurettetop lurette_lib.* gen_fake_lutin show_luc
rm -i gen_stubs lucky lurettetop lurette_lib.* gen_fake_lucky gen_fake_lutin show_luc
clean:
make -k clean -f Makefile.gen_stubs ; \
make -k clean -f Makefile.lucky ; \
make -k clean -f Makefile.lurettetop ; \
make -k clean -f Makefile.lurette_lib ; \
make -k clean -f Makefile.gen_fake_lutin ; \
make -k clean -f Makefile.gen_fake_lucky ; \
make -k clean -f Makefile.show_luc
......@@ -259,6 +268,7 @@ clean:
cp:
cp gen_stubs$(EXE) $(BIN_INSTALL_DIR) ; \
cp gen_fake_lutin$(EXE) $(BIN_INSTALL_DIR) ; \
cp gen_fake_lucky$(EXE) $(BIN_INSTALL_DIR) ; \
cp lucky$(EXE) $(BIN_INSTALL_DIR) ; \
cp show_luc$(EXE) $(BIN_INSTALL_DIR) ; \
cp lurettetop$(EXE) $(BIN_INSTALL_DIR) ; \
......
#
-include ../Makefile.common.source
SOURCES = $(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/gen_stubs_common.mli \
$(LURETTE_PATH)/source/gen_stubs_common.ml \
$(LURETTE_PATH)/source/parse_c_scade.mli \
$(LURETTE_PATH)/source/parse_c_scade.ml \
$(LURETTE_PATH)/source/parse_poc.mli \
$(LURETTE_PATH)/source/parse_poc.ml \
$(LURETTE_PATH)/source/gen_fake_lucky.ml
RESULT = gen_fake_lucky
LIBS = str unix
-include $(OCAMLMAKEFILE)
......@@ -30,6 +30,8 @@ USE_CAMLP4 = yes
SOURCES_OCAML = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/genlex.mli $(LURETTE_PATH)/source/genlex.ml \
$(LURETTE_PATH)/source/lexeme.mli $(LURETTE_PATH)/source/lexeme.ml \
$(LURETTE_PATH)/source/graph.mli \
$(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/prevar.mli \
......@@ -40,16 +42,16 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/ne.mli \
$(LURETTE_PATH)/source/ne.ml \
$(LURETTE_PATH)/source/constraint.mli \
$(LURETTE_PATH)/source/constraint.ml \
$(LURETTE_PATH)/source/formula.mli \
$(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/constraint.mli \
$(LURETTE_PATH)/source/constraint.ml \
$(LURETTE_PATH)/source/lustreExp.mli $(LURETTE_PATH)/source/lustreExp.ml \
$(LURETTE_PATH)/source/parser.mly $(LURETTE_PATH)/source/lexer.mll \
$(LURETTE_PATH)/source/gne.mli \
$(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/control.mli \
$(LURETTE_PATH)/source/control.ml \
$(LURETTE_PATH)/source/parse_env.mli \
$(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/parse_luc.mli \
$(LURETTE_PATH)/source/parse_luc.ml \
$(LURETTE_PATH)/source/polyhedron.mli \
$(LURETTE_PATH)/source/polyhedron.ml \
$(LURETTE_PATH)/source/draw.mli \
......
......@@ -34,6 +34,8 @@ SOURCES_C = ocaml2c.idl call_lurette_main.c
SOURCES = $(SOURCES_C) \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/genlex.mli $(LURETTE_PATH)/source/genlex.ml \
$(LURETTE_PATH)/source/lexeme.mli $(LURETTE_PATH)/source/lexeme.ml \
$(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
......@@ -41,9 +43,10 @@ SOURCES = $(SOURCES_C) \
$(LURETTE_PATH)/source/ne.mli $(LURETTE_PATH)/source/ne.ml \
$(LURETTE_PATH)/source/constraint.mli $(LURETTE_PATH)/source/constraint.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/lustreExp.mli $(LURETTE_PATH)/source/lustreExp.ml \
$(LURETTE_PATH)/source/parser.mly $(LURETTE_PATH)/source/lexer.mll \
$(LURETTE_PATH)/source/gne.mli $(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/control.mli $(LURETTE_PATH)/source/control.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/parse_luc.mli $(LURETTE_PATH)/source/parse_luc.ml \
$(LURETTE_PATH)/source/polyhedron.mli $(LURETTE_PATH)/source/polyhedron.ml \
$(LURETTE_PATH)/source/draw.mli $(LURETTE_PATH)/source/draw.ml \
$(LURETTE_PATH)/source/store.mli $(LURETTE_PATH)/source/store.ml \
......
......@@ -13,7 +13,9 @@ endif
USE_CAMLP4 = yes
SOURCES = $(LURETTE_PATH)/source/util.ml $(LURETTE_PATH)/source/lurettetop.ml
SOURCES = \
$(LURETTE_PATH)/source/genlex.mli $(LURETTE_PATH)/source/genlex.ml \
$(LURETTE_PATH)/source/util.ml $(LURETTE_PATH)/source/lurettetop.ml
RESULT = lurettetop
......
......@@ -17,12 +17,16 @@ USE_CAMLP4 = yes
SOURCES_OCAML = \
$(LURETTE_PATH)/source/util.ml \
$(LURETTE_PATH)/source/genlex.mli $(LURETTE_PATH)/source/genlex.ml \
$(LURETTE_PATH)/source/lexeme.mli $(LURETTE_PATH)/source/lexeme.ml \
$(LURETTE_PATH)/source/prevar.mli $(LURETTE_PATH)/source/prevar.ml \
$(LURETTE_PATH)/source/value.mli $(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/graph.mli $(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/formula.mli $(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/control.mli $(LURETTE_PATH)/source/control.ml \
$(LURETTE_PATH)/source/parse_env.mli $(LURETTE_PATH)/source/parse_env.ml \
$(LURETTE_PATH)/source/lustreExp.mli $(LURETTE_PATH)/source/lustreExp.ml \
$(LURETTE_PATH)/source/parser.mly $(LURETTE_PATH)/source/lexer.mll \
$(LURETTE_PATH)/source/parse_luc.mli $(LURETTE_PATH)/source/parse_luc.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/show_luc.ml
......
This diff is collapsed.
......@@ -55,28 +55,32 @@ type t
they won't be drawn again.
*)
type path
(* information associated to a formula which tells along which path
in the automata the formula has been obtained *)
val get : Formula.node list list -> t list
(**
[get nll] computes the sub-automata of the global ima made of the
accessible nodes from nodes in [nll]. [automata] obtained from
inner lists of nodes are multiplied. During that product, we check
that formula conjunctions are still (booleanly) satisfiable.
that formula conjunctions are still (Booleanly) satisfiable.
*)
val get_nodes : t -> Formula.node list
(** get the current nodes of an automata *)
val choose_n_formula : int -> t ->
(Formula.node list * Formula.formula * Control.state) list
(** [choose_n_formula n a] draws a list of triple made of a formula,
its corresponding target node, and a post-cond control expression
label list to evaluate if this formula is elected to perform the
step. [n] is the number of formula that should be drawn.
val choose_n_formula : int -> t -> (path * Formula.formula) list
(** [choose_n_formula n a] draws a list of pair made of a formula,
and its corresponding path.
[n] is the number of formula that should be drawn in [a].
*)
val remove_formula : t -> Formula.formula -> t
(** [remove_formula a f] removes all transitions labelled by [f] in
[a] (needed when f is unsatisfiable for numerical reasons). Also
removes epsilon transitions that lead to path that ends up without
a formula, which is likely to happen when we remove transitions
lebbeled with formula.
val remove_formula : t -> path -> t
(** [remove_formula a path] removes from [a] transitions so that
[path] is no more a path of [a]. This means that we remove the
last transition of [path] as well as transitions that would not
lead to a stable node (which can happen when we remove a transition).
*)
val get_top_path : path -> Formula.node list
......@@ -8,6 +8,7 @@
** Main author: jahier@imag.fr
*)
open Formula
(* exported *)
type ineq =
......@@ -16,7 +17,7 @@ type ineq =
(* exported *)
type t =
| Bv of string (** booleans *)
| Bv of Formula.var (** Booleans *)
| EqZ of Ne.t (** expr = 0 *)