lurette 0.37 Mon, 04 Mar 2002 14:58:15 +0100 by jahier

Parent-Version:      0.36
Version-Log:         Various cosmetic changes in comments.
Project-Description: Lurette

.lurette.prcs_aux

@@ -4,14 +4,14 @@
 (test/usager.env 396 1013445149 b/14_usager.env 1.2)
 (doc/ocamldoc.sty 1380 1008328137 b/12_ocamldoc.s 1.1)
 (source/env_state.ml 2789 1015246213 51_env_state. 1.11)
-(source/graph.ml 2476 1012914629 14_graph.ml 1.3)
-(source/util.ml 9392 1015246213 35_util.ml 1.11)
+(source/graph.ml 1801 1015250295 14_graph.ml 1.4)
+(source/util.ml 9430 1015250295 35_util.ml 1.12)
 (source/wtree.ml 9644 1014051154 b/1_wtree.ml 1.8)
 (source/solver.ml 18003 1015246213 39_solver.ml 1.12)
 (source/command_line.ml 3971 1014048376 b/20_command_li 1.3)
 (source/lurette.ml 11540 1015246213 12_lurette.ml 1.23)
-(source/solver.mli 1041 1015246213 38_solver.mli 1.8)
-(source/env.mli 2506 1013445149 15_env.mli 1.8)
+(source/solver.mli 1059 1015250295 38_solver.mli 1.9)
+(source/env.mli 2389 1015250295 15_env.mli 1.9)
 (lurette.depfull.dot 49 1007651448 b/5_lurette.de 1.2)
 (source/env.ml 8596 1015246213 16_env.ml 1.15)
 (make_lurette 812 1013517738 27_make_luret 1.7)
@@ -20,41 +20,41 @@
 (test/passerelle.env 862 1012914629 b/17_passerelle 1.1)
 (doc/archi.fig 3693 1003928781 20_archi.fig 1.1)
 (source/rnumsolver.ml 5159 1015246213 b/27_rnumsolver 1.1)
-(source/parse_env.mli 939 1008328137 40_parse_env. 1.3)
+(source/parse_env.mli 954 1015250295 40_parse_env. 1.4)
 (ID_EN_VRAC 2184 1002196285 0_ID_EN_VRAC 1.1)
-(source/sim2chro.mli 1421 1014051154 b/23_sim2chro.m 1.2)
+(source/sim2chro.mli 1427 1015250295 b/23_sim2chro.m 1.3)
 (doc/automata_format 0 1007379917 b/3_automata_f 1.1)
 (source/eval.ml 8697 1015246213 49_eval.ml 1.7)
-(source/gen_stubs.ml 32502 1014132434 24_generate_l 1.17)
+(source/gen_stubs.ml 32483 1015250295 24_generate_l 1.18)
 (source/parse_env.ml 9616 1015246213 41_parse_env. 1.5)
 (test/lurette.rif.exp 4746 1015246213 b/22_lurette.ri 1.6)
 (interface/TAGS 1956 1007380262 26_TAGS 1.3)
 (source/sim2chro.ml 2639 1014132434 b/24_sim2chro.m 1.3)
 (doc/Interface_draft 5232 1003928781 19_Interface_ 1.1)
 (doc/ocamldoc.hva 313 1008328137 b/13_ocamldoc.h 1.1)
-(source/formula.mli 2161 1015246213 44_formula.ml 1.6)
+(source/formula.mli 2161 1015250295 44_formula.ml 1.7)
 (source/command_line.mli 1302 1014048376 b/21_command_li 1.3)
 (TAGS 9825 1007379917 21_TAGS 1.6)
-(source/wtree.mli 2964 1013517738 b/0_wtree.mli 1.5)
+(source/wtree.mli 2931 1015250295 b/0_wtree.mli 1.6)
 (test/porte.env 861 1012914629 b/16_porte.env 1.1)
 (source/env_state.mli 3822 1015246213 50_env_state. 1.9)
 (source/rnumsolver.mli 1909 1015246213 b/26_rnumsolver 1.1)
-(source/eval.mli 1682 1015246213 48_eval.mli 1.5)
+(source/eval.mli 1645 1015250295 48_eval.mli 1.6)
 (README 74 1011881677 10_README 1.2)
 (test/ControleurPorte.c 9407 1012914629 b/19_Controleur 1.1)
-(OcamlMakefile 18628 1015246213 17_OcamlMakef 1.18)
+(OcamlMakefile 18580 1015250295 17_OcamlMakef 1.19)
 (test/tram.env 806 1012914629 b/15_tram.env 1.1)
 (source/show_env.ml 2961 1014048376 43_show_env.m 1.3)
 (doc/synthese 2556 1007379917 b/2_synthese 1.1)
 (test/ControleurPorte.h 2306 1012914629 b/18_Controleur 1.1)
 (interface/Makefile 197 1008255910 25_Makefile 1.6)
-(source/show_env.mli 826 1014048376 42_show_env.m 1.4)
+(source/show_env.mli 765 1015250295 42_show_env.m 1.5)
 (test/tram_simple.h 1746 1013519411 b/25_tram_simpl 1.1)
 (Makefile 1776 1015246213 18_Makefile 1.21)
 (test/vrai_tram.c 3060 1012914629 b/8_vrai_tram. 1.2)
 (source/print.mli 597 1014048376 46_print.mli 1.5)
-(source/graph.mli 1499 1014048376 13_graph.mli 1.5)
-(source/formula.ml 4579 1015246213 45_formula.ml 1.7)
-(source/lurette.mli 396 1012914629 11_lurette.ml 1.10)
-(source/print.ml 5534 1015246213 47_print.ml 1.8)
+(source/graph.mli 1493 1015250295 13_graph.mli 1.6)
+(source/formula.ml 4621 1015250295 45_formula.ml 1.8)
+(source/lurette.mli 433 1015250295 11_lurette.ml 1.11)
+(source/print.ml 5524 1015250295 47_print.ml 1.9)
 (test/vrai_tram.h 2468 1012914629 b/7_vrai_tram. 1.2)

OcamlMakefile

@@ -5,7 +5,7 @@
 #                            For updates see:
 #             http://miss.wu-wien.ac.at/~mottl/ocaml_sources
 #
-#        $Id: OcamlMakefile 1.18 Mon, 04 Mar 2002 13:50:13 +0100 jahier $
+#        $Id: OcamlMakefile 1.19 Mon, 04 Mar 2002 14:58:15 +0100 jahier $
 #
 ###########################################################################
 
@@ -537,20 +537,20 @@ ocamlprof:
 
 # Produces an html version of the lurette documentation
 dochtml:
-	ocamldoc -t "Lurette implementation description" -html -d ../doc/html -stars \
+	ocamldoc -t "Lurette modules interfaces" -pp "camlp4o" -html -d ../doc/html -stars \
 	-keep-code -colorize-code -I ../source/ $(SOURCES_OCAML)  \
-	../source/gen_stub.mli ../source/gen_stub.ml
+	../source/gen_stubs.ml
 
 doctex:
-	ocamldoc  -t "Lurette implementation description" -no-stop  -latex -d ../doc -stars \
+	ocamldoc  -t "Lurette modules interfaces" -pp "camlp4o" -no-stop  -latex -d ../doc -stars \
 	-keep-code  -m A -I ../source/ $(SOURCES_OCAML)  \
-	../source/gen_stub.mli ../source/gen_stub.ml ;  \
+	../source/gen_stubs.ml ;  \
 	pushd ../doc ; latex doc.tex ; popd
 
 docman:
-	ocamldoc  -t "Lurette implementation description"  -man -d ../doc/man -stars \
+	ocamldoc  -t "Lurette modules interfaces" -pp "camlp4o"  -man -d ../doc/man -stars \
 	-keep-code -I ../source/ $(SOURCES_OCAML) \
-	../source/gen_stub.mli ../source/gen_stub.ml
+	../source/gen_stubs.ml
 
 ###########################################################################
 # LOW LEVEL RULES

lurette.prj

 ;; -*- Prcs -*-
 (Created-By-Prcs-Version 1 3 3)
 (Project-Description "Lurette")
-(Project-Version lurette 0 36)
-(Parent-Version lurette 0 35)
-(Version-Log " 
-
-Add support to handle numerical contraints. The numerical stuff is
-untested, but the boolean part works as before.
-
-source/rnumsolver.mli:
-source/rnumsolver.ml:
-    New files implementing a numeric solver based on intervals.
-
-source/*.ml:
-    Change the var_type type from a string to a sum type containing
-    the lower and upper bounds of numeric domains. 
-
-    Do not maintain a var_name to index correspondance, but a formula to
-    index one. This is to be able to handle numerical constraint in bdds.
-    This field is not set at init time anymore, but in formula_to_bdd.
-
-    Add <>, <, and <= to the type of formula. 
-
-
-")
+(Project-Version lurette 0 37)
+(Parent-Version lurette 0 36)
+(Version-Log "Various cosmetic changes in comments.")
 (New-Version-Log "")
-(Checkin-Time "Mon, 04 Mar 2002 13:50:13 +0100")
+(Checkin-Time "Mon, 04 Mar 2002 14:58:15 +0100")
 (Checkin-Login jahier)
 (Populate-Ignore ())
 (Project-Keywords)
@@ -36,54 +16,54 @@ source/*.ml:
 
 
 ;; Sources files
-  (source/lurette.mli (lurette/11_lurette.ml 1.10 644))
+  (source/lurette.mli (lurette/11_lurette.ml 1.11 644))
   (source/lurette.ml (lurette/12_lurette.ml 1.23 644))
 
-  (source/graph.mli (lurette/13_graph.mli 1.5 644))
-  (source/graph.ml (lurette/14_graph.ml 1.3 644))
+  (source/graph.mli (lurette/13_graph.mli 1.6 644))
+  (source/graph.ml (lurette/14_graph.ml 1.4 644))
 
-  (source/env.mli (lurette/15_env.mli 1.8 644))
+  (source/env.mli (lurette/15_env.mli 1.9 644))
   (source/env.ml (lurette/16_env.ml 1.15 644))
 
-  (source/util.ml (lurette/35_util.ml 1.11 644))
+  (source/util.ml (lurette/35_util.ml 1.12 644))
 
-  (source/solver.mli (lurette/38_solver.mli 1.8 644))
+  (source/solver.mli (lurette/38_solver.mli 1.9 644))
   (source/solver.ml (lurette/39_solver.ml 1.12 644))
 
   (source/rnumsolver.mli (lurette/b/26_rnumsolver 1.1 644))
   (source/rnumsolver.ml (lurette/b/27_rnumsolver 1.1 644))
 
-  (source/parse_env.mli (lurette/40_parse_env. 1.3 644))
+  (source/parse_env.mli (lurette/40_parse_env. 1.4 644))
   (source/parse_env.ml (lurette/41_parse_env. 1.5 644))
 
-  (source/show_env.mli (lurette/42_show_env.m 1.4 644))
+  (source/show_env.mli (lurette/42_show_env.m 1.5 644))
   (source/show_env.ml (lurette/43_show_env.m 1.3 644))
 
-  (source/formula.mli (lurette/44_formula.ml 1.6 644))
-  (source/formula.ml (lurette/45_formula.ml 1.7 644))
+  (source/formula.mli (lurette/44_formula.ml 1.7 644))
+  (source/formula.ml (lurette/45_formula.ml 1.8 644))
 
   (source/print.mli (lurette/46_print.mli 1.5 644))
-  (source/print.ml (lurette/47_print.ml 1.8 644))
+  (source/print.ml (lurette/47_print.ml 1.9 644))
 
-  (source/eval.mli (lurette/48_eval.mli 1.5 644))
+  (source/eval.mli (lurette/48_eval.mli 1.6 644))
   (source/eval.ml (lurette/49_eval.ml 1.7 644))
 
   (source/env_state.mli (lurette/50_env_state. 1.9 644))
   (source/env_state.ml (lurette/51_env_state. 1.11 644))
 
-  (source/wtree.mli (lurette/b/0_wtree.mli 1.5 644))
+  (source/wtree.mli (lurette/b/0_wtree.mli 1.6 644))
   (source/wtree.ml (lurette/b/1_wtree.ml 1.8 644))
 
-  (source/sim2chro.mli (lurette/b/23_sim2chro.m 1.2 644))
+  (source/sim2chro.mli (lurette/b/23_sim2chro.m 1.3 644))
   (source/sim2chro.ml (lurette/b/24_sim2chro.m 1.3 644))
 
   (source/command_line.ml (lurette/b/20_command_li 1.3 644))
   (source/command_line.mli (lurette/b/21_command_li 1.3 644))
 
-  (source/gen_stubs.ml (lurette/24_generate_l 1.17 644))
+  (source/gen_stubs.ml (lurette/24_generate_l 1.18 644))
 
 ;; Make files
-  (OcamlMakefile (lurette/17_OcamlMakef 1.18 644))
+  (OcamlMakefile (lurette/17_OcamlMakef 1.19 644))
   (Makefile (lurette/18_Makefile 1.21 644))
   (test/Makefile (../Makefile) :symlink)
   (interface/Makefile (lurette/25_Makefile 1.6 644))

source/env.mli

@@ -8,18 +8,15 @@
 ** Main author: jahier@imag.fr
 *)
 
-(** 
-  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.
+(** Environment automata interpreter. Environment automata are
+   labelled by weighted formula. Automata are read from an [*.env]
+   file that has been produced by a third party tool, e.g., a Lutin
+   or a Lustre program.
 
   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.  
+  [try] and [step] commands modify oracle and SUT internal states via
+  side-effects.
 *)
 
 open Graph
@@ -29,18 +26,17 @@ open Env_state
 (*---------------------------------------------------------------------*)
 
 val read_env_state : string list list -> unit
-  (** 
-    [read_env_state files_ll] updates the global variable
+  (** [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.
-  *)
+    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 -> env_in -> (node list list * env_out * env_loc) list
@@ -51,15 +47,25 @@ val env_try : int -> int -> env_in -> (node list list * env_out * env_loc) list
     which arcs produced which outputs later (namely, when performing an 
     [env_step]).
    
-    Also sets (side effect) the environment input values to [input].
+    Also sets (side effect) the environment state input field to [input].
    *)
 
 
 
 val env_step : node list list -> env_out -> env_loc -> unit
   (**
-    [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]).
+    [env_step new_nodes output local] modifies the environment state by:
+    - setting the [env_state] [current_node] field to [new_nodes];
+    - setting the [env_state] [output] and [local] fields to [output] and 
+      [local].
    *)
   
+
+
+
+
+
+
+
+
+

source/eval.mli

@@ -25,31 +25,23 @@ val eval_expr : expr -> env_in -> expr
 
 val eval_wtree_list : env_in -> wtree list -> node list list 
   -> formula_table
-  (** 
-    [eval_wtree_list input wtl nfll] returns a table of formula
+  (** [eval_wtree_list input wtl nfll] returns a table of the 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]).  
-  *)
+    associated to pair of nodes from [env_state.formula_table]).  *)
 
 val update_pre: env_in -> 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
-  *)
+  (** 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 formula into atomic expressions if possible, fails
+    otherwise.  *)
 

source/formula.ml

@@ -50,6 +50,7 @@ type arc = node * node
 
 type arc_info = weigth * formula_eps
 
+(* XXX This is a bad name. Change it ! *)
 type atomic_expr = 
   | Int of int
   | Bool of bool

source/formula.mli

@@ -8,7 +8,7 @@
 ** Main author: jahier@imag.fr
 *)
 
-(** Defines the formula types. *)
+(** Defines the formula data type. *)
 
 (****************************************************************************)
 
@@ -76,9 +76,7 @@ type env_loc = subst list
 
 (****************************************************************************)
 
-(** 
-  Pretty prints formula and expressions 
- *)
+(** Pretty prints formula and expressions. *)
 
 val formula_eps_to_string : formula_eps -> string
 val formula_to_string : formula -> string

source/gen_stubs.ml

@@ -7,29 +7,32 @@
 ** File: generate_lurette_interface.ml
 ** Main author: jahier@imag.fr
 **
-** 
-** Implements a program that takes as input the string "sut"
-** (resp. "oracle") as well as a C header file `<foo>.h' to interface,
-** and which outputs stub files named `lurette_sut.h' and
-** `lurette_sut.c' (resp. `lurette_oracle.h' and `lurette_oracle.c').
-** Those files are used by the lurette Makefile to interface the sut
-** (resp. the oracle).
-** 
-** Note that <foo>.h should follows the poc convention (e.g., generated
-** by a lustre compiler). Namely, it should contain the following pragmas:
-** 
-** //MODULE: <module name> n m 
-**            (* where `n' is the input var number, and `m' the output var one *)
-** //IN:  <C type of the first input var> <a C identifier for the first input var>
-**    .
-**    .
-**    .  
-** //IN:  <C type of the nth input var> <a C identifier for the nth input var>
-** //OUT: <C type of the first output var> <a C identifier for the first output var>
-**    .
-**    .
-**    .
-** //OUT: <C type of the mth output var> <a C identifier for the mth output var>
+*)
+
+(** Generates stubs for calling poc C programs with lurette. It takes as 
+ input the string "sut" (resp. "oracle") as well as a C header file 
+ [<foo>.h] to interface, and outputs stub files named [lurette_sut.h] and
+ [lurette_sut.c] (resp. [lurette_oracle.h] and [lurette_oracle.c]).
+ Those files are used by the lurette Makefile to interface the sut
+ (resp. the oracle).
+ 
+ Note that <foo>.h should follows the poc convention (e.g., generated
+ by a lustre compiler). Namely, it should contain the following pragmas:
+ 
+ //MODULE: <module name> n m 
+            (* where [n] is the input var number, and [m] the output var one *)
+
+ //IN:  <C type of the first input var> <a C identifier for the first input var>
+
+    ...
+      
+ //IN:  <C type of the nth input var> <a C identifier for the nth input var>
+
+ //OUT: <C type of the first output var> <a C identifier for the first output var>
+
+    ...
+    
+ //OUT: <C type of the mth output var> <a C identifier for the mth output var>
 *)
 
 (****************************************************************************)
@@ -64,9 +67,9 @@ type alias = c_type * c_type
 let rec 
   (get_typedef_alias: file -> alias list) =
 (*
-** [get_typedef_alias file] reads `file' (a C header file) and search 
+** [get_typedef_alias file] reads [file] (a C header file) and search 
 ** for typedef C expressions and returns the list of (alias_type, C_type) 
-** found in `file'.
+** found in [file].
 *)
   fun file -> 
     let str = Util.readfile file in  
@@ -113,7 +116,7 @@ let rec (get_vn_and_ct_list: file -> module_name * vn_ct list * vn_ct list) =
 ** poc pragmas have the following shape:
 ** 
 ** //MODULE: <module name> n m 
-**            (* where `n' is the input var number, and `m' the output var one *)
+**            (* where [n] is the input var number, and [m] the output var one *)
 ** //IN:  <C type of the first input var> <a C identifier for the first input var>
 **    .
 **    .
@@ -257,7 +260,7 @@ let _ = assert ((check_var_type
 
 let (generate_stub_c: module_name -> string -> vn_ct list -> vn_ct list -> unit) = 
 (* 
-** [generate_stub_c mod_name str vi vo] generates a file named `<str>_stub.c' 
+** [generate_stub_c mod_name str vi vo] generates a file named [<str>_stub.c] 
 ** that interfaces the sut and the oracle with Lurette.
 *)
   fun mod_name str vi vo ->  
@@ -359,7 +362,7 @@ let (generate_idl : module_name -> sut_or_oracle -> vn_ct list -> vn_ct list
        -> unit) = 
 (* 
 ** [generate_idl mod_name str vi vo] generates an idl file named 
-** `<str>_idl_stub.idl' that camlidl processes to generate stub files that
+** [<str>_idl_stub.idl] that camlidl processes to generate stub files that
 ** will interface C poc files with lurette. 
 *)
   fun mod_name str vi vo ->  
@@ -460,7 +463,7 @@ let (get_ml_type2: file -> vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_c
      in
      let (sptr: int) = 
        (* 
-	** `sptr' should point to the first char of the first 
+	** [sptr] should point to the first char of the first 
 	** type of sut_step. 
 	*)
        try 
@@ -473,7 +476,7 @@ let (get_ml_type2: file -> vn_ct list -> vn_ct list -> vn_ct_mlt_fvn list * vn_c
      in
      let (vtl: string list) = read_type_list sptr [] in
        (* 
-	** `vtl' ougth to contain the list of sut_try types in reverse order,
+	** [vtl] ougth to contain the list of sut_try types in reverse order,
 	** i.e., the output type in the first place, then the last argument
 	** of (the currified version of) sut_try, and so on.
 	*)
@@ -542,9 +545,9 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
 **    - the type of sut inputs (as a tuple containing the sut variables
 **      ordered lexicographically w.r.t. their names)
 **    - the type of sut outputs (in the same manner)
-**    - Defines a version of `sut_try' that takes as argument a tuple 
+**    - Defines a version of [sut_try] that takes as argument a tuple 
 **      instead of a currified list of input values as camlidl provides.
-**    - ditto for `sut_step', `oracle_try', and `oracle_step'
+**    - ditto for [sut_step], [oracle_try], and [oracle_step]
 **    - a list of sut (input and output) variable names and types (so that
 **      we can check later that the environment variable names and types are
 **      consistent with the ones of the sut).
@@ -731,7 +734,7 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
 
 
        (*
-       ** Defines a version of `sut_try' that takes as argument a tuple 
+       ** Defines a version of [sut_try] that takes as argument a tuple 
        ** instead of a currified list of input values as camlidl provides.
        *)
       put "(*****************************************************************) \n";
@@ -749,7 +752,7 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
 
       
        (*
-       ** Ditto for `sut_step'.
+       ** Ditto for [sut_step].
        *)
       put ("let (sut_step: Formula.subst list -> Formula.env_in) = \n") ;
       put "  fun input_sl ->\n    let (" ;
@@ -762,7 +765,7 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
 
 
        (*
-       ** Ditto for `oracle_try'.
+       ** Ditto for [oracle_try].
        *)
       put ("let (oracle_try: Formula.subst list -> Formula.env_in -> bool) = \n") ;
       put "  fun sut_input sut_output -> \n";
@@ -779,7 +782,7 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
       put "\n\n" ;
       
        (*
-       ** Ditto for `oracle_step'.
+       ** Ditto for [oracle_step].
        *)
       put ("let (oracle_step: Formula.subst list -> Formula.env_in -> bool) = \n") ;
       put "  fun sut_input sut_output -> \n";
@@ -823,7 +826,7 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
      
        (*
        ** Defines sut_in_init and sut_out_init that provide fake initial
-       ** values to input and output tuples at ``boot'' time, i.e., when
+       ** values to input and output tuples at [boot] time, i.e., when
        ** lurette starts. 
        *)
      
@@ -836,8 +839,8 @@ let (generate_lurette_stub_file: vn_ct_mlt_fvn list * vn_ct_mlt_fvn list -> unit
 
 let (replace_bool_representation: alias list -> alias list) =
   (*  
-   ** Lustre defines `_boolean' as an `int', but camlidl maps C `boolean'
-   ** to the caml `bool' type. 
+   ** Lustre defines [_boolean] as an [int], but camlidl maps C [boolean]
+   ** to the caml [bool] type. 
    *)
   fun ta -> 
     ("_boolean", "boolean")::(List.remove_assoc "_boolean" ta)

source/graph.ml

@@ -6,15 +6,13 @@
 
 ** File: graph.ml
 ** Main author: jahier@imag.fr
-** 
-** Defines a graph data structure as well as various functions
-** that operate over it.
 *)
 
 (*------------------------------------------------------------------------*)
 
 open Hashtbl
 
+(* exported *)
 type ('a, 'b) t = {
   mutable table : ('a, (('a * 'b) list)) Hashtbl.t ;
   mutable nodes : 'a list ;
@@ -23,10 +21,8 @@ type ('a, 'b) t = {
 
 
   
+(* exported *)
 let (create: unit -> ('a, 'b) t) = 
-(* 
-** Create an empty graph
-*)
   fun () -> 
     {
       table = (Hashtbl.create 1) ;
@@ -34,24 +30,15 @@ let (create: unit -> ('a, 'b) t) =
       trans = []
     }
 
+(* exported *)
 let (get_list_of_target_nodes: ('a, 'b) t -> 'a -> ('a * 'b) list) =
-(* 
-** [get_list_of_target_nodes g node] returns the list of target nodes
-** starting from `node_from' in the graph `g'. Actually, it does not only
-** return a list of nodes but a list of pairs `(node_to, arc_label)' where 
-** `arc_label' is the arc label of the arc from `node_from' to `node_to'. 
-*)
   fun g node ->
     try Hashtbl.find g.table node 
     with Not_found -> []
 
 
+(* exported *)
 let (add_trans: ('a -> 'a -> int) -> ('a, 'b) t -> 'a -> 'b -> 'a -> unit) = 
-(* 
-** [add_trans sort 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'. [sort] is a comparison
-** function used to sort nodes.
-*)
   fun sort g node_from arc_info node_to ->
     let l = g.nodes in
     let l1 = if (List.mem node_from l) then l else (List.append l [node_from]) in
@@ -67,17 +54,13 @@ let (add_trans: ('a -> 'a -> int) -> ('a, 'b) t -> 'a -> 'b -> 'a -> unit) =
 
    
 
+(* exported *)
 let (get_all_nodes: ('a, 'b) t -> 'a list) = 
-(* 
-** [get_all_nodes g] returns the set of nodes of  g
-*)
   fun g -> g.nodes
 
 
+(* exported *)
 let (get_all_trans:  ('a, 'b) t -> ('a * 'b * 'a) list ) = 
-(* 
-** [get_all_trans g] returns the list transitions of the graph g 
-*)
   fun g -> g.trans
 
 

source/graph.mli

@@ -8,9 +8,8 @@
 ** Main author: jahier@imag.fr
 *)
  
-(**
-  Defines a graph data structure as well as various functions
-  that operates over it.
+(** A graph data structure as well as various functions that operates
+  over it.
 *)
 
 
@@ -26,8 +25,8 @@ val create: unit -> ('a, 'b) t
 
 val add_trans: ('a -> 'a -> int) -> ('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'. [sort] is a comparison
+    [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]. [sort] is a comparison
     function used to sort nodes.
   *)
 
@@ -35,18 +34,18 @@ val add_trans: ('a -> 'a -> int) -> ('a, 'b) t -> 'a -> 'b -> 'a -> unit
 val get_list_of_target_nodes: ('a, 'b) t -> 'a -> ('a * 'b) list
   (**
     [get_list_of_target_nodes g node] returns the list of target nodes
-    starting from `node_from' in the graph `g'. Actually, it does not only
-    return a list of nodes but a list of pairs `(node_to, arc_label)' where 
-    `arc_label' is the arc label of the arc from `node_from' to `node_to'. 
+    starting from [node_from] in the graph [g]. Actually, it does not only
+    return a list of nodes but a list of pairs [(node_to, arc_label)] where 
+    [arc_label] is the arc label of the arc from [node_from] to [node_to]. 
   *)