Skip to content

GitLab

Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

Commit 6f110b29 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.22 Fri, 14 Dec 2001 12:08:57 +0100 by jahier 

Parent-Version:      0.21
Version-Log:

Change the comments layout so that ocamldoc is able to process them nicely.
Project-Description: Lurette
parent 68089bdc
Hide whitespace changes
Inline Side-by-side
Showing with 345 additions and 213 deletions
.lurette.prcs_aux
View file @ 6f110b29
......@@ -2,54 +2,56 @@
;; REALLY bad things.
(Created-By-Prcs-Version 1 3 3)
(test/vrai.h 1120 1006183551 31_vrai.h 1.1)
(doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
(source/env_state.ml 1468 1007648245 51_env_state. 1.3)
(source/graph.ml 2397 1003932490 14_graph.ml 1.2)
(test/tram_env_porte.env 882 1007638809 b/11_tram_env_p 1.2)
(source/util.ml 3552 1007648245 35_util.ml 1.4)
(source/wtree.ml 9181 1007379917 b/1_wtree.ml 1.1)
(source/util.ml 3869 1008328137 35_util.ml 1.5)
(source/wtree.ml 9186 1008328137 b/1_wtree.ml 1.3)
(source/solver.ml 2091 1007651448 39_solver.ml 1.3)
(source/lurette.ml 8309 1007648245 12_lurette.ml 1.12)
(source/solver.mli 707 1007651448 38_solver.mli 1.2)
(source/env.mli 2838 1007379917 15_env.mli 1.5)
(source/solver.mli 742 1008328137 38_solver.mli 1.3)
(source/env.mli 2524 1008328137 15_env.mli 1.7)
(test/vrai.lus 65 1006182545 28_vrai.lus 1.1)
(lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
(test/tram_env_tramway.env 1228 1007638809 b/10_tram_env_t 1.2)
(source/env.ml 8243 1007638809 16_env.ml 1.9)
(source/env.ml 8250 1008328137 16_env.ml 1.10)
(make_lurette 1027 1007398490 27_make_luret 1.5)
(test/vrai_tram.lus 453 1007379917 b/6_vrai_tram. 1.1)
(test/edge.c 1693 1006263320 32_edge.c 1.1)
(lurette.dep.dot 49 1007651448 b/4_lurette.de 1.2)
(doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
(source/parse_env.mli 865 1007638809 40_parse_env. 1.2)
(source/parse_env.mli 939 1008328137 40_parse_env. 1.3)
(ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
(test/edge.h 1052 1006263320 33_edge.h 1.1)
(doc/automata_format 0 1007379917 b/3_automata_f 1.1)
(source/eval.ml 7923 1007638809 49_eval.ml 1.2)
(source/gen_stubs.ml 32119 1007648245 24_generate_l 1.12)
(source/parse_env.ml 6609 1007638809 41_parse_env. 1.2)
(source/gen_stubs.ml 32098 1008255910 24_generate_l 1.13)
(source/parse_env.ml 6537 1008328137 41_parse_env. 1.3)
(interface/TAGS 1956 1007380262 26_TAGS 1.3)
(doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
(source/formula.mli 1663 1007638809 44_formula.ml 1.2)
(doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
(source/formula.mli 1693 1008328137 44_formula.ml 1.3)
(test/tram_env_usager.env 826 1007638809 b/9_tram_env_u 1.2)
(TAGS 9825 1007379917 21_TAGS 1.6)
(source/wtree.mli 2906 1007379917 b/0_wtree.mli 1.1)
(source/env_state.mli 957 1007638809 50_env_state. 1.2)
(source/wtree.mli 2860 1008328137 b/0_wtree.mli 1.3)
(source/env_state.mli 996 1008328137 50_env_state. 1.3)
(interface/sut_idl_stub.ml 338 1006263457 34_sut_idl_st 1.1)
(source/eval.mli 859 1007638809 48_eval.mli 1.2)
(source/eval.mli 1690 1008328137 48_eval.mli 1.3)
(README 0 1002791390 10_README 1.1)
(OcamlMakefile 16039 1007651448 17_OcamlMakef 1.7)
(OcamlMakefile 16584 1008328137 17_OcamlMakef 1.8)
(source/show_env.ml 3303 1007379917 43_show_env.m 1.1)
(test/tram_simple.c 5627 1006433610 37_tram_simpl 1.1)
(doc/synthese 2556 1007379917 b/2_synthese 1.1)
(interface/Makefile 215 1007380262 25_Makefile 1.5)
(source/show_env.mli 848 1007379917 42_show_env.m 1.1)
(interface/Makefile 197 1008255910 25_Makefile 1.6)
(source/show_env.mli 868 1008328137 42_show_env.m 1.2)
(test/tram_simple.h 1746 1006433610 36_tram_simpl 1.1)
(Makefile 1350 1007648245 18_Makefile 1.11)
(Makefile 1393 1008328137 18_Makefile 1.13)
(test/vrai_tram.c 2855 1007379917 b/8_vrai_tram. 1.1)
(source/print.mli 108 1007379917 46_print.mli 1.1)
(source/graph.mli 1305 1003932490 13_graph.mli 1.2)
(source/formula.ml 3115 1007638809 45_formula.ml 1.2)
(source/graph.mli 1340 1008328137 13_graph.mli 1.3)
(source/formula.ml 3109 1008328137 45_formula.ml 1.3)
(test/vrai.c 1405 1006183551 30_vrai.c 1.1)
(source/lurette.mli 370 1007648245 11_lurette.ml 1.8)
(source/print.ml 1098 1007379917 47_print.ml 1.1)
(source/lurette.mli 397 1008328137 11_lurette.ml 1.9)
(source/print.ml 1599 1008328137 47_print.ml 1.2)
(test/vrai_tram.h 2293 1007379917 b/7_vrai_tram. 1.1)
Makefile
View file @ 6f110b29
......@@ -6,22 +6,27 @@ OCAMLMAKEFILE = $(LURETTE_DIR)/OcamlMakefile
-include ./lurette.in
SOURCES = $(SUT) sut_stub.c sut_idl_stub.idl \
$(ORACLE) oracle_stub.c oracle_idl_stub.idl \
lurette_stub.ml \
SOURCES_C = $(SUT) sut_stub.c sut_idl_stub.idl \
$(ORACLE) oracle_stub.c oracle_idl_stub.idl
SOURCES_OCAML = lurette_stub.ml \
$(LURETTE_DIR)/source/util.ml \
$(LURETTE_DIR)/source/graph.mli $(LURETTE_DIR)/source/graph.ml \
$(LURETTE_DIR)/source/formula.mli $(LURETTE_DIR)/source/formula.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/env_state.mli $(LURETTE_DIR)/source/env_state.ml \
$(LURETTE_DIR)/source/sim2chro.mli $(LURETTE_DIR)/source/sim2chro.ml \
$(LURETTE_DIR)/source/eval.mli $(LURETTE_DIR)/source/eval.ml \
$(LURETTE_DIR)/source/solver.mli $(LURETTE_DIR)/source/solver.ml \
$(LURETTE_DIR)/source/wtree.mli $(LURETTE_DIR)/source/wtree.ml \
$(LURETTE_DIR)/source/print.mli $(LURETTE_DIR)/source/print.ml \
$(LURETTE_DIR)/source/parse_env.mli $(LURETTE_DIR)/source/parse_env.ml \
$(LURETTE_DIR)/source/env.mli $(LURETTE_DIR)/source/env.ml \
$(LURETTE_DIR)/source/show_env.mli $(LURETTE_DIR)/source/show_env.ml \
$(LURETTE_DIR)/source/lurette.mli $(LURETTE_DIR)/source/lurette.ml
SOURCES = $(SOURCES_C) \
$(SOURCES_OCAML)
RESULT = lurette
-include $(OCAMLMAKEFILE)
OcamlMakefile
View file @ 6f110b29
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.7 Thu, 06 Dec 2001 16:10:48 +0100 jahier $
# $Id: OcamlMakefile 1.8 Fri, 14 Dec 2001 12:08:57 +0100 jahier $
#
###########################################################################
......@@ -482,20 +482,33 @@ tags:
# Generates the modules dependency graph using ocamldot
# (results in lurette.dep.ps and lurette.depfull.ps). (R1)
dot:
touch $(RESULT).dep.dot ; touch $(RESULT).dep.ps ; \
pushd ../source ; touch $(RESULT).dep.dot ; touch $(RESULT).dep.ps ; \
\rm $(RESULT).dep.ps $(RESULT).dep.dot ; \
touch $(RESULT).depfull.dot ; touch $(RESULT).depfull.ps ; \
\rm $(RESULT).depfull.ps $(RESULT).depfull.dot ; \
ocamldep $(SOURCES) | $(OCAMLDOT) -fullgraph -lr > $(RESULT).depfull.dot ; \
ocamldep $(SOURCES) | $(OCAMLDOT) > $(RESULT).dep.dot ; \
dot -Tps $(RESULT).depfull.dot > $(RESULT).depfull.ps ; \
dot -Tps $(RESULT).dep.dot > $(RESULT).dep.ps
dot -Tps $(RESULT).dep.dot > $(RESULT).dep.ps ; \
cp $(RESULT).dep.ps ../doc ; cp $(RESULT).depfull.ps ../doc ; popd
# (R1)
try:
$(LURETTE_DIR)/make_lurette tram_simple tram_oracle; \
$(LURETTE_DIR)/make_lurette tram_simple vrai_tram; \
./lurette 50 10 10 tram_env_porte.env x tram_env_usager.env tram_env_tramway.env
dochtml:
ocamldoc -t "Lurette implementation description" -html -d ../doc/html -stars \
-keep-code -colorize-code -I ../source/ $(SOURCES_OCAML)
doctex:
ocamldoc -t "Lurette implementation description" -latex -d ../doc -stars \
-keep-code -I ../source/ $(SOURCES_OCAML) ; \
pushd ../doc ; latex doc.tex ; popd
docman:
ocamldoc -t "Lurette implementation description" -man -d ../doc/man -stars \
-keep-code -I ../source/ $(SOURCES_OCAML)
###########################################################################
# LOW LEVEL RULES
......
doc/ocamldoc.hva 0 → 100644
View file @ 6f110b29
\usepackage{alltt}
\newenvironment{ocamldoccode}{\begin{alltt}}{\end{alltt}}
\newenvironment{ocamldocdescription}{\begin{quote}}{\end{quote}}
\newenvironment{ocamldoccomment}{\begin{quote}}{\end{quote}}
\newcommand\textbar{|}
\newcommand\textbackslash{\\}
\newcommand\textasciicircum{\^{}}
\newcommand\sharp{#}
doc/ocamldoc.sty 0 → 100644
View file @ 6f110b29
%% Support macros for LaTeX documentation generated by ocamldoc.
%% This file is in the public domain; do what you want with it.
\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{ocamldoc}
[2001/12/04 v1.0 ocamldoc support]
\newenvironment{ocamldoccode}{%
\bgroup
\leftskip\@totalleftmargin
\rightskip\z@skip
\parindent\z@
\parfillskip\@flushglue
\parskip\z@skip
\noindent\@@par
\@tempswafalse
\def\par{%
\if@tempswa
\leavevmode\null\@@par\penalty\interlinepenalty
\else
\@tempswatrue
\ifhmode\@@par\penalty\interlinepenalty\fi
\fi}
\obeylines
\verbatim@font
\let\org@prime~%
\@noligs
\let\org@dospecials\dospecials
\g@remfrom@specials{\\}
\g@remfrom@specials{\{}
\g@remfrom@specials{\}}
\let\do\@makeother
\dospecials
\let\dospecials\org@dospecials
\frenchspacing\@vobeyspaces
\everypar \expandafter{\the\everypar \unpenalty}}
{\egroup\par}
\def\g@remfrom@specials#1{%
\def\@new@specials{}
\def\@remove##1{%
\ifx##1#1\else
\g@addto@macro\@new@specials{\do ##1}\fi}
\let\do\@remove\dospecials
\let\dospecials\@new@specials
}
\newenvironment{ocamldocdescription}
{\list{}{\rightmargin0pt \topsep0pt}\raggedright\item\relax}
{\endlist\medskip}
\newenvironment{ocamldoccomment}
{\list{}{\leftmargin 2\leftmargini \rightmargin0pt \topsep0pt}\raggedright\item\relax}
{\endlist}
\endinput
lurette.prj
View file @ 6f110b29
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 21)
(Parent-Version lurette 0 20)
(Project-Version lurette 0 22)
(Parent-Version lurette 0 21)
(Version-Log "
Removes a few hard coded paths.
")
Change the comments layout so that ocamldoc is able to process them nicely.")
(New-Version-Log "")
(Checkin-Time "Thu, 13 Dec 2001 16:05:10 +0100")
(Checkin-Time "Fri, 14 Dec 2001 12:08:57 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -18,46 +17,46 @@ Removes a few hard coded paths.
;; Sources files
(source/lurette.mli (lurette/11_lurette.ml 1.8 644))
(source/lurette.mli (lurette/11_lurette.ml 1.9 644))
(source/lurette.ml (lurette/12_lurette.ml 1.12 644))
(source/graph.mli (lurette/13_graph.mli 1.2 644))
(source/graph.mli (lurette/13_graph.mli 1.3 644))
(source/graph.ml (lurette/14_graph.ml 1.2 644))
(source/env.mli (lurette/15_env.mli 1.6 644))
(source/env.ml (lurette/16_env.ml 1.9 644))
(source/env.mli (lurette/15_env.mli 1.7 644))
(source/env.ml (lurette/16_env.ml 1.10 644))
(source/util.ml (lurette/35_util.ml 1.4 644))
(source/util.ml (lurette/35_util.ml 1.5 644))
(source/solver.mli (lurette/38_solver.mli 1.2 644))
(source/solver.mli (lurette/38_solver.mli 1.3 644))
(source/solver.ml (lurette/39_solver.ml 1.3 644))
(source/parse_env.mli (lurette/40_parse_env. 1.2 644))
(source/parse_env.ml (lurette/41_parse_env. 1.2 644))
(source/parse_env.mli (lurette/40_parse_env. 1.3 644))
(source/parse_env.ml (lurette/41_parse_env. 1.3 644))
(source/show_env.mli (lurette/42_show_env.m 1.1 644))
(source/show_env.mli (lurette/42_show_env.m 1.2 644))
(source/show_env.ml (lurette/43_show_env.m 1.1 644))
(source/formula.mli (lurette/44_formula.ml 1.2 644))
(source/formula.ml (lurette/45_formula.ml 1.2 644))
(source/formula.mli (lurette/44_formula.ml 1.3 644))
(source/formula.ml (lurette/45_formula.ml 1.3 644))
(source/print.mli (lurette/46_print.mli 1.1 644))
(source/print.ml (lurette/47_print.ml 1.1 644))
(source/print.ml (lurette/47_print.ml 1.2 644))
(source/eval.mli (lurette/48_eval.mli 1.2 644))
(source/eval.mli (lurette/48_eval.mli 1.3 644))
(source/eval.ml (lurette/49_eval.ml 1.2 644))
(source/env_state.mli (lurette/50_env_state. 1.2 644))
(source/env_state.mli (lurette/50_env_state. 1.3 644))
(source/env_state.ml (lurette/51_env_state. 1.3 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.2 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.2 644))
(source/wtree.mli (lurette/b/0_wtree.mli 1.3 644))
(source/wtree.ml (lurette/b/1_wtree.ml 1.3 644))
(source/gen_stubs.ml (lurette/24_generate_l 1.13 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.7 644))
(Makefile (lurette/18_Makefile 1.12 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.8 644))
(Makefile (lurette/18_Makefile 1.13 644))
(test/Makefile (../Makefile) :symlink)
(interface/Makefile (lurette/25_Makefile 1.6 644))
(make_lurette (lurette/27_make_luret 1.5 744))
......@@ -68,6 +67,8 @@ Removes a few hard coded paths.
(doc/archi.fig (lurette/20_archi.fig 1.1 644))
(doc/synthese (lurette/b/2_synthese 1.1 644))
(doc/automata_format (lurette/b/3_automata_f 1.1 644))
(doc/ocamldoc.sty (lurette/b/12_ocamldoc.s 1.1 644))
(doc/ocamldoc.hva (lurette/b/13_ocamldoc.h 1.1 644))
;; Misc
(README (lurette/10_README 1.1 644))
......@@ -96,7 +97,6 @@ Removes a few hard coded paths.
(test/tram_env_usager.env (lurette/b/9_tram_env_u 1.2 644))
(test/tram_env_tramway.env (lurette/b/10_tram_env_t 1.2 644))
(test/tram_env_porte.env (lurette/b/11_tram_env_p 1.2 644))
)
(Merge-Parents)
(New-Merge-Parents)
source/env.ml
View file @ 6f110b29
......@@ -224,15 +224,15 @@ let (env_try : int -> int -> sut_out -> (node list list * sut_in * env_loc) list
List.map (tuplise_env_outputs) nll_sl_sl_l
(****************************************************************************)
(*****************************************************************************)
let (env_step : node list list -> sut_in -> env_loc -> unit) =
(*
** [env_step node_to output local] modifies the
** environment state by:
** 1 - performing a transition from the current nodes to `nodes_to'
** 2 - updating the memory (using `output' and `local').
*)
(*
** [env_step node_to output local] modifies the
** environment state by:
** 1 - performing a transition from the current nodes to `nodes_to'
** 2 - updating the memory (using `output' and `local').
*)
fun nodes_to output local ->
env_state.current_nodes <- nodes_to ;
env_state.output <- output ;
......
source/env.mli
View file @ 6f110b29
......@@ -6,23 +6,20 @@
**
** File: env.mli
** Main author: jahier@imag.fr
**
** This module simulates the test environement for lurette.
** It assumes that a description of the test environement exists in the
** form of an automata whose arcs are labelled by weighted formula. This
** description is read from an *.env file that has been produced by a
** third party tool, issued from, e.g., a Lutin or a Lustre spec.
**
** This module provides the automata data type, a procedure to read the
** automata from an *.aut file, as well as various procedures to step
** through the automata.
**
** Remark:
** I defined `env_state' as a mutable data type for consistency with
** what occurs in the oracle and in the SUT. Indeed, try and step
** commands modify oracle and SUT internal states via side-effects.
** Making the env_state mutable allows us to do the same for the
** environment.
*)
(**
Simulates the test environment for lurette. It assumes that a
description of the test environement exists in the form of an
automata whose arcs are labelled by weighted formula. This
description is read from an [*.env] file that has been produced by a
third party tool, e.g., a Lutin or a Lustre spec.
Remark: I defined [env_state] as a mutable data type for
consistency with what occurs in the oracle and in the SUT. Indeed,
try and step commands modify oracle and SUT internal states via
side-effects. Making the env_state mutable allows us to do the
same for the environment.
*)
open Graph
......@@ -34,36 +31,37 @@ open Env_state
val read_env_state : string list list -> unit
(*
** Updates the global variable `env_state' using the automata defined
** in the list of list in argument. The idea behind having a list of list
** there is that automata given in inner lists should be run as a product,
** and outter ones should be run in parallel.
** For example, (read_env_state [["foo1"; "foo2"]; ["foo3"]]) means that
** the automata given in `foo1' and `foo2' are run as if their automata
** were multiplied (in the classical sense of the automata product),
** and `foo3' is run in parallel. Of course, `foo3' should not share any
** variables with `foo1' and `foo2' then.
*)
(**
[read_env_state files_ll] updates the global variable
[env_state] using the automata defined in the list of list
[files_ll]. The idea behind having a list of list there is that
automata given in inner lists should be run as a product, and
outer ones should be run in parallel. For example,
[read_env_state [["foo1"; "foo2"]; ["foo3"]]] means that the
automata given in [foo1] and [foo2] are run as if their automata
were multiplied (in the classical sense of the automata product),
and [foo3] is run in parallel. Of course, [foo3] should not share
any variables with [foo1] and [foo2] then.
*)
val env_try : int -> int -> sut_out -> (node list list * sut_in * env_loc) list
(*
** [env_try n p input] returns a list of `n*p' possible outputs of the
** environment with input `input'. This function actually returns a list
** of 3-tuple `node list list * env_out * env_loc' because we need to know
** which arcs produced which outputs later (namely, when performing an
** `env_step').
**
** Also sets (side effect) the environment input values to `input'.
(**
[env_try n p input] returns a list of [n*p] possible outputs of the
environment with input [input]. This function actually returns a list
of 3-tuple [node list list * env_out * env_loc] because we need to know
which arcs produced which outputs later (namely, when performing an
[env_step]).
Also sets (side effect) the environment input values to [input].
*)
val env_step : node list list -> sut_in -> env_loc -> unit
(*
** [env_step node_to output local ] modifies the environment state by:
** 1 - performing a transition from the current_node to `node_to'
** 2 - updating the memory (using `output' and `local').
(**
[env_step node_to output local ] modifies the environment state by:
- performing a transition from the current_node to [node_to],
- updating the memory (using [output] and [local]).
*)
source/env_state.mli
View file @ 6f110b29
......@@ -8,6 +8,8 @@
** Main author: jahier@imag.fr
*)
(** Defines the environment state data type. *)
(****************************************************************************)
open Formula
......@@ -24,16 +26,12 @@ type env_stateT = {
mutable formula_table : Wtree.formula_table ;
mutable wtree_table : Wtree.wtree_table ;
(*
** Used to store the values of variables under a pre
*)
(** Used to store the values of variables under a pre *)
mutable input : env_in ;
mutable output: env_out ;
mutable local : env_loc
}
val env_state : env_stateT
source/eval.mli
View file @ 6f110b29
......@@ -8,28 +8,50 @@
** Main author: jahier@imag.fr
*)
(** Defines functions that evaluate formula or expressions. *)
open Formula
open Lurette_stub
open Wtree
val eval : formula -> sut_out -> formula
(**
[eval f input] returns an evaluated version of the formula f. Input
variables (namely, sut outputs) as well as variables ``under a pre''
(in the environment memory) are replaced by their values. Then,
the formula is simplified; e.g., [true and f] is simplified into [f].
*)
val eval_expr : expr -> sut_out -> expr
(** Ditto for expressions. *)
val eval_wtree_list : sut_out -> wtree list -> node list list
-> formula_table
(**
[eval_wtree_list input wtl nfll] returns a table of formula
appearing in [wtl]; the formula are evaluated
w.r.t. [input]. [nfll] is the list of list of origin nodes
corresponding to the trees in [wtl] (necessary to get formula
associated to pair of nodes from [env_state.formula_table]).
*)
val update_pre: sut_out -> unit
(*
** Computes the values of pre expressions and formula (i.e., updates
** env_state.local).
*)
(**
Computes the values of pre expressions and formula (i.e., updates
[env_state.local]).
*)
val expr_to_atomic: expr -> atomic_expr
(**
Translates expressions into atomic expressions if possible,
fails otherwise
*)
val formula_to_atomic: formula -> atomic_expr
(*
** translates expressions and formula into atomic expressions if possible,
** fails otherwise.
*)
(**
Translates expressions and formula into atomic expressions if possible,
fails otherwise.
*)
source/formula.ml
View file @ 6f110b29
......@@ -6,8 +6,6 @@
**
** File: formula.ml
** Main author: jahier@imag.fr
**
**
*)
(****************************************************************************)
......@@ -67,9 +65,10 @@ type vnf = var_name * (formula * formula)
(****************************************************************************)
(****************************************************************************)
(*
** Pretty prints formula and expressions
*)
(**
Pretty prints formula and expressions
*)
let rec
(formula_eps_to_string: formula_eps -> string) =
fun fe -> match fe with
......
source/formula.mli
View file @ 6f110b29
......@@ -6,10 +6,10 @@
**
** File: formula.mli
** Main author: jahier@imag.fr
**
**
*)
(** Defines the formula types. *)
(****************************************************************************)
open Lurette_stub
......@@ -34,9 +34,9 @@ type formula =
| False
| Bvar of string
| Eq of expr * expr (* = *)
| Ge of expr * expr (* >= *)
| G of expr * expr (* > *)
| Eq of expr * expr (** = *)
| Ge of expr * expr (** >= *)
| G of expr * expr (** > *)
type formula_eps =
| Eps
......@@ -67,13 +67,11 @@ type env_loc = subst list
(****************************************************************************)
(*
** Pretty prints formula and expressions
*)
val formula_eps_to_string : formula_eps -> string
(**
Pretty prints formula and expressions
*)
val formula_eps_to_string : formula_eps -> string
val formula_to_string : formula -> string
val expr_to_string : expr -> string
val arc_info_to_string : arc_info -> string
source/graph.mli
View file @ 6f110b29
......@@ -3,47 +3,48 @@
** This file may only be copied under the terms of the GNU Library General
** Public License
**-----------------------------------------------------------------------
**
** File: graph.mli
** Main author: jahier@imag.fr
**
** Defines a graph data structure as well as various functions
** that operates over it.
*)
(**
Defines a graph data structure as well as various functions
that operates over it.
*)
type ('a, 'b) t
val create: unit -> ('a, 'b) t
(*
** Create an empty graph
*)
(**
Create an empty graph
*)
val add_trans: ('a, 'b) t -> 'a -> 'b -> 'a -> unit
(*
** [add_trans g node_from arc_info node_to] adds a transition from `node_from'
** to `node_to' with arc label `arc_info' to the graph `g'.
*)
(**
[add_trans g node_from arc_info node_to] adds a transition from `node_from'
to `node_to' with arc label `arc_info' to the graph `g'.
*)