Commit 67c17ef7 authored by Erwan Jahier's avatar Erwan Jahier

lurette 1.9 Tue, 18 Nov 2003 11:17:12 +0100 by jahier

Parent-Version:      1.8
Version-Log:

A lot (too much...) of changes, mainly renaming files, and types, and
functions,
change the interface, move from one module to another, etc.

Bref, a lot of cleanning.

Project-Description: Lurette
parent a3e8a67b
This diff is collapsed.
......@@ -6,47 +6,47 @@
# Where to find libs
INCDIRS = $(HOME)/$(HOST_TYPE)/lib
LIBDIRS = $(HOME)/$(HOST_TYPE)/lib
LIBDIRS = $(HOME)/$(HOST_TYPE)/lib
OCAMLMAKEFILE = $(HOME)/lurette/OcamlMakefile
LURETTE_PATH = $(HOME)/lurette
SOURCES_LURETTE_LIB = $(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/polyDraw.mli \
$(LURETTE_PATH)/source/polyDraw.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/value.mli $(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/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/parse_luc.mli $(LURETTE_PATH)/source/parse_luc.ml \
$(LURETTE_PATH)/source/polyhedron.mli $(LURETTE_PATH)/source/polyhedron.ml \
$(LURETTE_PATH)/source/store.mli $(LURETTE_PATH)/source/store.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/formula_to_bdd.mli \
$(LURETTE_PATH)/source/formula_to_bdd.ml \
$(LURETTE_PATH)/source/bddd.mli \
$(LURETTE_PATH)/source/bddd.ml \
$(LURETTE_PATH)/source/fair_bddd.mli \
$(LURETTE_PATH)/source/fair_bddd.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/automata.mli $(LURETTE_PATH)/source/automata.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
$(LURETTE_PATH)/source/lurette.ml
ALL_SOURCES = $(SOURCES_LURETTE_LIB) $(SOURCES_OCAML)
# SOURCES_LURETTE_LIB = $(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/polyDraw.mli \
# $(LURETTE_PATH)/source/polyDraw.ml \
# $(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
# $(LURETTE_PATH)/source/value.mli $(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/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/parse_luc.mli $(LURETTE_PATH)/source/parse_luc.ml \
# $(LURETTE_PATH)/source/polyhedron.mli $(LURETTE_PATH)/source/polyhedron.ml \
# $(LURETTE_PATH)/source/store.mli $(LURETTE_PATH)/source/store.ml \
# $(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
# $(LURETTE_PATH)/source/formula_to_bdd.mli \
# $(LURETTE_PATH)/source/formula_to_bdd.ml \
# $(LURETTE_PATH)/source/bddd.mli \
# $(LURETTE_PATH)/source/bddd.ml \
# $(LURETTE_PATH)/source/fair_bddd.mli \
# $(LURETTE_PATH)/source/fair_bddd.ml \
# $(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
# $(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
# $(LURETTE_PATH)/source/automata.mli $(LURETTE_PATH)/source/automata.ml \
# $(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
# $(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
# $(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
# $(LURETTE_PATH)/source/lurette.ml
ALL_SOURCES = $(SOURCES) $(SOURCES_OCAML)
ifeq ($(HOST_TYPE),cygwin)
EXE := .exe
......
*********** BUGS
* Quand je tire une solution dans le gras de l'épaisseur,
il faut que je tienne compte des poids des transitions
avec l'option --draw-all-formula
-> idem au sein du polyedre ; oui mais laquelle prendre ?
inside ? n'importe laquelle ?
-> if suffit de refaire en un env_try false 1 0 0 ....
* quand une formule s'avere fausse du point de vue des variables
numeriques, il ne faut pas repartir du haut du graphe, mais backtraker
depuis la branche qui s'avere fausse...
* compilé en mode "assert", lurette se fait tuer par un signal 11
au bout d'une dizaine de pas...
depuis la branche qui s'avere fausse. Sinon, les probabilités induites
par les poids sont un peu contre-intuitives.
* en mode fair, certaine requete aboutisse a qque chose de vraiment
* en mode fair, certaines requetes aboutissent a qque chose de vraiment
pas satisfaisant : pleins de polyhedres intermediaires inutiles
sont calcules, selon l'ordre dans lequel arrivent les contraintes...
......
......@@ -4,8 +4,18 @@
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{ocamldoc}
[2001/12/04 v1.0 ocamldoc support]
\usepackage{color,xcolor,psfig,epsfig,graphics}
\newcommand{\red}{\color{red}}
\newcommand{\blue}[1]{{\color{blue} #1}}
\newcommand{\blued}[1]{{\color{blue2} #1}}
\newcommand{\bluet}[1]{{\color{blue3} #1}}
\newcommand{\green}[1]{{\color{green4} #1}}
\newcommand{\greent}[1]{{\color{green3} #1}}
\newenvironment{ocamldoccode}{%
\color{DarkSlateGrey}
\bgroup
\leftskip\@totalleftmargin
\rightskip\z@skip
......@@ -46,11 +56,13 @@
}
\newenvironment{ocamldocdescription}
{\list{}{\rightmargin0pt \topsep0pt}\raggedright\item\relax}
{ %\color{green3}
\list{}{\rightmargin0pt \topsep0pt}\raggedright\item\relax}
{\endlist\medskip}
\newenvironment{ocamldoccomment}
{\list{}{\leftmargin 2\leftmargini \rightmargin0pt \topsep0pt}\raggedright\item\relax}
{ \color{red}
\list{}{\leftmargin 2\leftmargini \rightmargin0pt \topsep0pt}\raggedright\item\relax}
{\endlist}
\endinput
......
This diff is collapsed.
......@@ -74,7 +74,7 @@ ICFLAGS = \
# XCFLAGS should be the same than the flags with which CUDD has been compiled
# i386-linux
# XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
XCFLAGS = -mcpu=pentiumpro -malign-double -DHAVE_IEEE_754 -DBSD
# sparc-sun
# XCFLAGS = -mcpu=ultrasparc -DHAVE_IEEE_754 -DUNIX100
......
......@@ -100,6 +100,13 @@ clean:
# C part
#-----------------------------------
# COBJS=matrix.o polka.o polka_lexer.o polkag_caml.o polyg_caml.o vectorg_caml.o matrixg_caml.o polkaIO.o polka_parser.o poly.o vector.o
COBJS= polkag_caml.o polyg_caml.o vectorg_caml.o matrixg_caml.o polkaIO.o
libpolka.a: $(COBJS)
ocamlmklib -o polka $(COBJS) -cclib -lcamlidl
libpolkai_caml.a: $(CCFILES_CAML:%=%i_caml.o)
ar rcs $@ $^
libpolkal_caml.a: $(CCFILES_CAML:%=%l_caml.o)
......@@ -143,7 +150,7 @@ libpolkag_caml_prof.a: $(CCFILES_CAML:%=%g_caml_prof.o)
#-----------------------------------
polka.cma: polka_parser.cmo polka_lexer.cmo $(MLFILES:%=%.cmo) polkaIO.cmo
$(OCAMLC) $(MLFLAGS) -a -o $@ $^
$(OCAMLC) $(MLFLAGS) -a -o $@ -custom -cclib -lpolkag_caml $^
polka.cmxa: polka_parser.cmx polka_lexer.cmx $(MLFILES:%=%.cmx) polkaIO.cmx
$(OCAMLOPT) $(MLFLAGS) $(MLOPTFLAGS) -a -o $@ $^
......
#!/bin/sh
# $Id: plot 1.4 Wed, 17 Sep 2003 10:09:24 +0200 jahier $
# $Id: plot 1.5 Tue, 18 Nov 2003 11:17:12 +0100 jahier $
#
# pl: general wrapper script for plotting with gnuplot from shell cmdline
#
......@@ -70,8 +70,9 @@ HOME_RCFILE=$HOME/.plrc
if [ -f $CODE ]; then rm $CODE; fi
cat > $CODE << EOT
# defaults
set data style linespoints
set style data linespoints
set grid
set pointsize 0.1
EOT
# default term setting
......
......@@ -200,7 +200,7 @@ lucky_bc:
make -k bc -f Makefile.lucky OCAMLFLAGS=""
lucky_debug:
make -k dc -f Makefile.lucky OCAMLFLAGS=""
make -k dc -f Makefile.lucky OCAMLFLAGS="" MLONLY=yes
lucky_debug_no_assert:
make -k dc -f Makefile.lucky OCAMLFLAGS="-noassert"
......
......@@ -12,14 +12,17 @@ ifndef OCAMLFLAGS
endif
OCAMLLDFLAGS=-cclib -lpolkag_caml -cclib -lpolkag -cclib $(HOME)/$(HOST_TYPE)/lib/libgmp.a
OCAMLLDFLAGS= \
-cclib -lpolkag_caml \
-cclib -lpolkag \
-cclib $(HOME)/$(HOST_TYPE)/lib/libgmp.a
CC=gcc #g++
#POLKA_CLIB = polkai_caml polkai gmp
POLKA_CLIB =
# POLKA_CLIB = polkag_caml polkag gmp
#POLKA_CLIB = polkag_caml david_polkag_print parme gmpxx
# POLKA_CLIB = polkag_caml david_polkag_print parme gmpxx
LIBS = unix str nums polka cudd
CLIBS = cudd_caml cuddaux cudd $(POLKA_CLIB) camlidl mtr st epd util
......@@ -30,26 +33,65 @@ 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/genlex.ml \
$(LURETTE_PATH)/source/lexeme.ml \
$(LURETTE_PATH)/source/graph.ml \
$(LURETTE_PATH)/source/poly_draw.ml \
$(LURETTE_PATH)/source/prevar.ml \
$(LURETTE_PATH)/source/command_line_luc_exe.ml \
$(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/var.ml \
$(LURETTE_PATH)/source/ne.ml \
$(LURETTE_PATH)/source/exp.ml \
$(LURETTE_PATH)/source/constraint.ml \
$(LURETTE_PATH)/source/lustreExp.ml \
$(LURETTE_PATH)/source/parser.mly \
$(LURETTE_PATH)/source/lexer.mll \
$(LURETTE_PATH)/source/gne.ml \
$(LURETTE_PATH)/source/parse_luc.ml \
$(LURETTE_PATH)/source/polyhedron.ml \
$(LURETTE_PATH)/source/store.ml \
$(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/formula_to_bdd.ml \
$(LURETTE_PATH)/source/bddd.ml \
$(LURETTE_PATH)/source/fair_bddd.ml \
$(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/run_aut.ml \
$(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/lucky.ml \
$(LURETTE_PATH)/source/luc_exe.ml
ifndef MLONLY
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/polyDraw.mli \
$(LURETTE_PATH)/source/polyDraw.ml \
$(LURETTE_PATH)/source/poly_draw.mli \
$(LURETTE_PATH)/source/poly_draw.ml \
$(LURETTE_PATH)/source/prevar.mli \
$(LURETTE_PATH)/source/prevar.ml \
$(LURETTE_PATH)/source/command_line_luc_exe.mli \
$(LURETTE_PATH)/source/command_line_luc_exe.ml \
$(LURETTE_PATH)/source/value.mli \
$(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/var.mli \
$(LURETTE_PATH)/source/var.ml \
$(LURETTE_PATH)/source/ne.mli \
$(LURETTE_PATH)/source/ne.ml \
$(LURETTE_PATH)/source/formula.mli \
$(LURETTE_PATH)/source/formula.ml \
$(LURETTE_PATH)/source/exp.mli \
$(LURETTE_PATH)/source/exp.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/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/parse_luc.mli \
......@@ -70,17 +112,17 @@ SOURCES_OCAML = \
$(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/show_env.mli \
$(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/automata.mli \
$(LURETTE_PATH)/source/automata.ml \
$(LURETTE_PATH)/source/run_aut.mli \
$(LURETTE_PATH)/source/run_aut.ml \
$(LURETTE_PATH)/source/print.mli \
$(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/sim2chro.mli \
$(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli \
$(LURETTE_PATH)/source/env.ml \
$(LURETTE_PATH)/source/lucky.mli \
$(LURETTE_PATH)/source/lucky.ml \
$(LURETTE_PATH)/source/luc_exe.mli \
$(LURETTE_PATH)/source/luc_exe.ml
endif
SOURCES = $(SOURCES_C) \
$(SOURCES_OCAML)
......
......@@ -11,7 +11,7 @@ ifndef OCAMLFLAGS
OCAMLFLAGS := -noassert -unsafe
endif
CC=gcc #g++
CC=gcc
OCAMLLDFLAGS = \
-cclib -lcudd_caml -cclib -lcuddaux -cclib -lcudd \
......@@ -20,7 +20,7 @@ OCAMLLDFLAGS = \
-cclib -lcamlidl -cclib -lmtr -cclib -lst -cclib -lepd -cclib -lutil \
-output-obj
LIBS = str polka
LIBS = str polka cudd
# POLKA_CLIB = polkag_caml polkag gmp
# CLIBS = cudd_caml cuddaux cudd $(POLKA_CLIB) camlidl mtr st epd util
......@@ -33,37 +33,64 @@ 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/polyDraw.mli \
$(LURETTE_PATH)/source/polyDraw.ml \
$(LURETTE_PATH)/source/command_line.mli $(LURETTE_PATH)/source/command_line.ml \
$(LURETTE_PATH)/source/value.mli $(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/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/parse_luc.mli $(LURETTE_PATH)/source/parse_luc.ml \
$(LURETTE_PATH)/source/polyhedron.mli $(LURETTE_PATH)/source/polyhedron.ml \
$(LURETTE_PATH)/source/store.mli $(LURETTE_PATH)/source/store.ml \
$(LURETTE_PATH)/source/env_state.mli $(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/formula_to_bdd.mli \
$(LURETTE_PATH)/source/formula_to_bdd.ml \
$(LURETTE_PATH)/source/bddd.mli \
$(LURETTE_PATH)/source/bddd.ml \
$(LURETTE_PATH)/source/fair_bddd.mli \
$(LURETTE_PATH)/source/fair_bddd.ml \
$(LURETTE_PATH)/source/solver.mli $(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/show_env.mli $(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/automata.mli $(LURETTE_PATH)/source/automata.ml \
$(LURETTE_PATH)/source/print.mli $(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/sim2chro.mli $(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/env.mli $(LURETTE_PATH)/source/env.ml \
$(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/poly_draw.mli \
$(LURETTE_PATH)/source/poly_draw.ml \
$(LURETTE_PATH)/source/prevar.mli \
$(LURETTE_PATH)/source/prevar.ml \
\
$(LURETTE_PATH)/source/command_line.mli \
$(LURETTE_PATH)/source/command_line.ml \
\
$(LURETTE_PATH)/source/value.mli \
$(LURETTE_PATH)/source/value.ml \
$(LURETTE_PATH)/source/var.mli \
$(LURETTE_PATH)/source/var.ml \
$(LURETTE_PATH)/source/ne.mli \
$(LURETTE_PATH)/source/ne.ml \
$(LURETTE_PATH)/source/exp.mli \
$(LURETTE_PATH)/source/exp.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/parse_luc.mli \
$(LURETTE_PATH)/source/parse_luc.ml \
$(LURETTE_PATH)/source/polyhedron.mli \
$(LURETTE_PATH)/source/polyhedron.ml \
$(LURETTE_PATH)/source/store.mli \
$(LURETTE_PATH)/source/store.ml \
$(LURETTE_PATH)/source/env_state.mli \
$(LURETTE_PATH)/source/env_state.ml \
$(LURETTE_PATH)/source/formula_to_bdd.mli \
$(LURETTE_PATH)/source/formula_to_bdd.ml \
$(LURETTE_PATH)/source/bddd.mli \
$(LURETTE_PATH)/source/bddd.ml \
$(LURETTE_PATH)/source/fair_bddd.mli \
$(LURETTE_PATH)/source/fair_bddd.ml \
$(LURETTE_PATH)/source/solver.mli \
$(LURETTE_PATH)/source/solver.ml \
$(LURETTE_PATH)/source/show_env.mli \
$(LURETTE_PATH)/source/show_env.ml \
$(LURETTE_PATH)/source/run_aut.mli \
$(LURETTE_PATH)/source/run_aut.ml \
$(LURETTE_PATH)/source/print.mli \
$(LURETTE_PATH)/source/print.ml \
$(LURETTE_PATH)/source/sim2chro.mli \
$(LURETTE_PATH)/source/sim2chro.ml \
$(LURETTE_PATH)/source/lucky.mli \
$(LURETTE_PATH)/source/lucky.ml \
\
$(LURETTE_PATH)/source/lurette.ml
......
......@@ -22,7 +22,10 @@ SOURCES_OCAML = \
$(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/var.mli \
$(LURETTE_PATH)/source/var.ml \
$(LURETTE_PATH)/source/exp.mli \
$(LURETTE_PATH)/source/exp.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 \
......
(*-----------------------------------------------------------------------
** Copyright (C) 2001, 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: automata.mli
** Author: jahier@imag.fr
*)
type t
(** [Automata.t] is an ADT containing an acyclic sub-automata (ie a
tree) of a ima made of a node and its immediate successors in the
ima. Those [automata] are recomputed at each step and are used to
draw (Several) formula.
More precisely, while building those sub-automata, we not only
consider accessible transitions, we also:
- evaluate formula wrt inputs and pre (by [Solver.formula_to_bdd]);
- check formula (boolean) satisfiability and remove unsatisfiable
transitions;
- evaluate weight expressions and replace them by the result of
their evaluation;
- remove branches guarded by non-recoverable variables (cf
control.mli);
- break eps-loops by removing the last eps transition [*] of the
loop. This can occur if one writes (a * * ). We need to remove it
to avoid that the execution of the ima loops. It is safe to do it
because there is actually another way of producing epsilon,
namely, if the outter loop counter is drawn to 0.
nb 1: the product of ima is *not* done at the beginning and once
for all at the level of ima, but once "local" automata have been
computed and evaluated. The reasons for doing the product there
is because automata product is notoriously highly
exponential. Doing that, we limit the product explosion in two
ways: (1) sub-[automata] are of course much smaller (2) since we
have waited for the time when inputs and pre are known, some more
transitions are removed because then some formula are then known
to be unsatisfiable (well, we currently only check the boolean
satisfiability at that level actually; the numerical part is only
check during the draw of numerical variables).
nb 2: for environments that are run together, we can not draw
formula separately (i.e., we need to explicitly compute the
product) because we need to be able to remember which tuple of
the product leaded to an unsatisfiable formula to make sure that
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.
*)
val get_nodes : t -> Formula.node list
(** get the current nodes of an automata *)
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 get_all_formula: t -> (path * Formula.formula) list
(** get all the formula accessible from the current node *)
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
......@@ -15,11 +15,12 @@
*)
open Util
open Formula
open Exp
open Value
open Constraint
open Store
type var_idx = int
type sol_nb = float
......@@ -66,8 +67,11 @@ let (add_snt_entry : Bdd.t -> sol_nb * sol_nb -> unit) =
let (init_snt : unit -> unit) =
fun _ ->
Hashtbl.add !snt_ref (Bdd.dtrue (Env_state.bdd_manager ())) (1.0, 0.0);
Hashtbl.add !snt_ref (Bdd.dfalse (Env_state.bdd_manager ())) (0.0, 1.0)
let fake_env_in = (Hashtbl.create 0) in
(Hashtbl.add
!snt_ref (Formula_to_bdd.f fake_env_in True) (1.0, 0.0));
(Hashtbl.add
!snt_ref (Formula_to_bdd.f fake_env_in True) (0.0, 1.0))
let (clear_snt: unit -> unit) =
fun _ ->
......@@ -198,14 +202,14 @@ let (build_sol_nb_table: var list -> Bdd.t -> Bdd.t -> unit) =
(****************************************************************************)
let (toss_up_one_var: var_name -> subst) =
let (toss_up_one_var: Var.name -> Var.subst) =
fun var ->
(* *)
let ran = Random.float 1. in
if (ran < 0.5) then (var, B(true)) else (var, B(false))
let (toss_up_one_var_index: var_idx -> subst option) =
let (toss_up_one_var_index: var_idx -> Var.subst option) =
fun var_idx ->
(* if [var_idx] is a index that corresponds to a boolean variable,
this fonction performs a toss and returns a substitution for
......@@ -216,32 +220,32 @@ let (toss_up_one_var_index: var_idx -> subst option) =
appear along a path, we simply ignore it and hence it will not
be added to the store.
*)
let cstr = Env_state.index_to_linear_constraint var_idx in
let cstr = Formula_to_bdd.index_to_linear_constraint var_idx in
match cstr with
Bv(v) -> (
match v.default with
match (Var.default v) with
Some (Formu f) ->
let (bdd, _) = Formula_to_bdd.translate (Env_state.input ()) f in
if Bdd.is_false bdd then Some(v.n, B false)
else if Bdd.is_true bdd then Some(v.n, B true)
let bdd = Formula_to_bdd.f (Env_state.input ()) f in
if Bdd.is_false bdd then Some((Var.name v), B false)
else if Bdd.is_true bdd then Some((Var.name v), B true)
else
(
print_string (
"*** Default values should not depend on " ^
"controllable variables, \nwhich is the case of " ^
(formula_to_string f) ^ ", the default value of " ^
v.n ^ "\n");
(Var.name v) ^ "\n");
exit 1
)
| Some (Expre _) -> assert false
| Some (Numer _) -> assert false
| Some (Liste l) -> assert false
| _ -> Some(toss_up_one_var v.n)
| _ -> Some(toss_up_one_var (Var.name v))
)
| _ -> None
let rec (draw_in_bdd_rec: subst list * Store.t -> Bdd.t -> Bdd.t ->
subst list * Store.t' * Store.p) =
let rec (draw_in_bdd_rec: Var.subst list * Store.t -> Bdd.t -> Bdd.t ->
Var.subst list * Store.t' * Store.p) =
fun (sl, store) bdd comb ->
(** Returns [sl] appended to a draw of all the boolean variables
bigger than the topvar of [bdd] according to the ordering
......@@ -275,7 +279,7 @@ let rec (draw_in_bdd_rec: subst list * Store.t -> Bdd.t -> Bdd.t ->
let _ = assert (not (Bdd.is_false bdd)) in
let _ = assert (sol_number_exists bdd snt) in
let bddvar = Bdd.topvar bdd in
let cstr = (Env_state.index_to_linear_constraint bddvar) in
let cstr = (Formula_to_bdd.index_to_linear_constraint bddvar) in
match cstr with
| Bv(var) ->
draw_in_bdd_rec_bool var (sl, store) bdd comb snt
......@@ -285,8 +289,8 @@ let rec (draw_in_bdd_rec: subst list * Store.t -> Bdd.t -> Bdd.t ->
draw_in_bdd_rec_ineq ineq (sl, store) bdd comb snt
and (draw_in_bdd_rec_bool: var -> subst list * Store.t -> Bdd.t -> Bdd.t -> snt ->
subst list * Store.t' * Store.p) =
and (draw_in_bdd_rec_bool: var -> Var.subst list * Store.t -> Bdd.t -> Bdd.t ->
snt -> Var.subst list * Store.t' * Store.p) =
fun var (sl, store) bdd comb snt ->
let bddvar = Bdd.topvar bdd in
let topvar_comb = Bdd.topvar comb in
......@@ -333,8 +337,8 @@ and (draw_in_bdd_rec_bool: var -> subst list * Store.t -> Bdd.t -> Bdd.t -> snt
(Bdd.dthen bdd), true, n )
in
let (sl1, sl2, new_comb) = (
((var.n, B(bool1))::sl),
((var.n, B(bool2))::sl),
(((Var.name var), B(bool1))::sl),
(((Var.name var), B(bool2))::sl),
(if Bdd.is_true comb then comb else Bdd.dthen comb)
)
in
......@@ -363,8 +367,8 @@ and (draw_in_bdd_rec_bool: var -> subst list * Store.t -> Bdd.t -> Bdd.t -> snt
flush stdout;
assert false
and (draw_in_bdd_rec_ineq: Constraint.ineq -> subst list * Store.t -> Bdd.t ->
Bdd.t -> snt -> subst list * Store.t' * Store.p) =
and (draw_in_bdd_rec_ineq: Constraint.ineq -> Var.subst list * Store.t -> Bdd.t ->
Bdd.t -> snt -> Var.subst list * Store.t' * Store.p) =
fun cstr (sl, store) bdd comb snt ->
(*
When we add to the store an inequality constraint GZ(ne) or
......@@ -421,8 +425,8 @@ and (draw_in_bdd_rec_ineq: Constraint.ineq -> subst list * Store.t -> Bdd.t ->
flush stdout;
assert false
and (draw_in_bdd_rec_eq: Ne.t -> subst list * Store.t -> Bdd.t -> Bdd.t -> snt ->
subst list * Store.t' * Store.p) =
and (draw_in_bdd_rec_eq: Ne.t -> Var.subst list * Store.t -> Bdd.t -> Bdd.t -> snt ->
Var.subst list * Store.t' * Store.p) =
fun ne (sl, store) bdd comb snt ->
(*
We consider 3 stores:
......@@ -532,6 +536,6 @@ and (draw_in_bdd_rec_eq: Ne.t -> subst list * Store.t -> Bdd.t -> Bdd.t -> snt -
(* exported *)
let rec (draw_in_bdd: var list -> Bdd.t -> Bdd.t ->
subst list * Store.t' * Store.p) =
Var.subst list * Store.t' * Store.p) =
fun store bdd comb ->
draw_in_bdd_rec ([], Store.create store) bdd comb
......@@ -13,8 +13,7 @@
type sol_nb = float
val build_sol_nb_table : Formula.var list -> Bdd.t -> Bdd.t -> unit
val build_sol_nb_table : Exp.var list -> Bdd.t -> Bdd.t -> unit
(**
[build_sol_nb_table bdd comb] build a table that associate each to
a [bdd] its solution number in its 2 branches. [comb] is a bdd made
......@@ -22,25 +21,30 @@ val build_sol_nb_table : Formula.var list -> Bdd.t -> Bdd.t -> unit
variable to be generated (which migth not appear in [bdd]).
*)