Skip to content

L
lutin
Commit 18e59b0d authored by Erwan Jahier's avatar Erwan Jahier
Browse files
Options

lurette 1.23 Mon, 08 Mar 2004 14:10:38 +0100 by jahier 

Parent-Version:      1.22
Version-Log:

source/*.ml*:
   perform a sed 's/[ ]*$//' on all files to remove
   trailing space.

Project-Description: Lurette
parent ceac869e
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 5314 additions and 4420 deletions
.lurette.prcs_aux
View file @ 18e59b0d
This diff is collapsed.
TODO
View file @ 18e59b0d
......@@ -34,9 +34,6 @@ et je ne suis plus oblig
*********** A faire
* parse_lucky.ml:
XXX parse_lustre_expression : attention au tilde (virer le hack et ragarder ce que ca change)
+ verifier que 2 vars ne sont définies 2 fois dans le meme fichiers
* Ajouter la possibilité de pouvoir rejouer un séquence et de la continuer
......
lurette.prj
View file @ 18e59b0d
This diff is collapsed.
source/bddd.mli
View file @ 18e59b0d
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
** Public License
**-----------------------------------------------------------------------
**
** File: bddd.mli
......
source/command_line.ml
View file @ 18e59b0d
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
** Public License
**-----------------------------------------------------------------------
**
** File: command_line.ml
......@@ -27,13 +27,13 @@ type optionsT = {
mutable oracle : bool
}
type cmd_line_optionT =
type cmd_line_optionT =
Step | NoStep | Help
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
| AllVertices | AllFormula
(* | CuddHeapInit *)
| Seed | Precision | NoOracle | Verbose | ShowStep | Output
| Seed | Precision | NoOracle | Verbose | ShowStep | Output
| ComputeVolume | StepInside | StepEdges | StepVertices
(* Names of the command line options to override the defaults. *)
......@@ -78,14 +78,14 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
("--step-inside", StepInside);
("--step-edges", StepEdges);
("--step-vertices", StepVertices);
(* ("--init-cudd-heap", CuddHeapInit) *)
]
let (option_to_usage: cmd_line_optionT -> string) =
fun opt ->
fun opt ->
match opt with
Step -> "Run lurette step by step.\n"
| NoStep -> "Do not run lurette step by step (Default).\n"
......@@ -110,14 +110,14 @@ let (option_to_usage: cmd_line_optionT -> string) =
| StepEdges -> "Step at edges\n"
| StepVertices -> "Step at vertices\n"
let (group_common_options: (string * cmd_line_optionT) list ->
let (group_common_options: (string * cmd_line_optionT) list ->
(string * cmd_line_optionT) list) =
fun list ->
fun list ->
List.fold_left
(fun acc (str, opt) ->
(fun acc (str, opt) ->
match acc with
(str2, opt2)::tail ->
if
(str2, opt2)::tail ->
if
(opt = opt2)
then
(((str2 ^ "\n\t\t" ^ str), opt)::tail)
......@@ -129,7 +129,7 @@ let (group_common_options: (string * cmd_line_optionT) list ->
list
let usage_options =
List.fold_left
(fun acc (str, opt) ->
(fun acc (str, opt) ->
acc ^ "\n\t\t" ^ str ^ "\n\t\t\t" ^ (option_to_usage opt))
""
(List.rev (group_common_options string_to_option))
......@@ -151,13 +151,13 @@ let usage =
let cmd_line_string_to_int str errmsg =
try
(int_of_string str)
try
(int_of_string str)
with Failure ("int_of_string")
->
->
print_string usage ;
print_string errmsg ;
flush stdout ;
failwith "\n *** Error when calling lurette.\n"
source/command_line.mli
View file @ 18e59b0d
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
** Public License
**-----------------------------------------------------------------------
**
** File: command_line.mli
......@@ -9,7 +9,7 @@
*)
(** Handles everything that is related to command line lurette calls:
printing lurette usage message, handling command line options, etc.
printing lurette usage message, handling command line options, etc.
*)
open Lucky
......@@ -40,16 +40,16 @@ val cmd_line_string_to_int : string -> string -> int
the convertion failed.
*)
type cmd_line_optionT =
type cmd_line_optionT =
Step | NoStep | Help
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
| DisplayLocalVar | NoDisplayLocalVar
| Sim2chro | NoSim2chro
(* | CuddHeapInit *)
| AllVertices | AllFormula
| Seed | Precision | NoOracle | Verbose | ShowStep | Output
| Seed | Precision | NoOracle | Verbose | ShowStep | Output
| ComputeVolume | StepInside | StepEdges | StepVertices
val string_to_option: (string * cmd_line_optionT) list
(** Mapping from options string (e.g., "--no-step") to the cmd_line_optionT
(** Mapping from options string (e.g., "--no-step") to the cmd_line_optionT
type. *)
source/command_line_luc_exe.ml
View file @ 18e59b0d
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
** Public License
**-----------------------------------------------------------------------
**
** File: command_line_luc_exe.ml
......@@ -21,8 +21,8 @@ type optionsT = {
mutable verb : bool
}
type cmd_line_optionT =
StepNb | Seed | Precision | Boot | ShowAut | NoShowAut | Verbose | Locals
type cmd_line_optionT =
StepNb | Seed | Precision | Boot | ShowAut | NoShowAut | Verbose | Locals
| Help | Inside | Edges | Vertices | ComputeVolume
(* Names of the command line options to override the defaults. *)
......@@ -67,7 +67,7 @@ let (string_to_option: (string * cmd_line_optionT) list) = [
]
let (option_to_usage: cmd_line_optionT -> string) =
fun opt ->
fun opt ->
match opt with
Boot -> "The Lucky machine starts generating values.\n"
| ShowAut -> "Run lucky showing the lucky automata.\n"
......@@ -85,14 +85,14 @@ let (option_to_usage: cmd_line_optionT -> string) =
"Compute the polyhedra volume before drawing: more fair, " ^
"but more expensive.\n")
let (group_common_options: (string * cmd_line_optionT) list ->
let (group_common_options: (string * cmd_line_optionT) list ->
(string * cmd_line_optionT) list) =
fun list ->
fun list ->
List.fold_left
(fun acc (str, opt) ->
(fun acc (str, opt) ->
match acc with
(str2, opt2)::tail ->
if
(str2, opt2)::tail ->
if
(opt = opt2)
then
(((str2 ^ ", " ^ str), opt)::tail)
......@@ -102,13 +102,13 @@ let (group_common_options: (string * cmd_line_optionT) list ->
)
[]
list
let usage_options =
List.fold_left
let usage_options =
List.fold_left
(fun acc (str, opt) -> acc ^ "\n " ^ str ^ "\n\t" ^ (option_to_usage opt))
""
(List.rev (group_common_options string_to_option))
let usage =
let usage =
("usage: lucky [options]* (<file.luc>)+ " ^
"\n where `<file.luc> contains a Lucky program. Automata " ^
"\n that share output variables are executed as if they were " ^
......@@ -120,13 +120,13 @@ let usage =
let cmd_line_string_to_int str errmsg =
try
(int_of_string str)
with Failure("int_of_string")
->
try
(int_of_string str)
with Failure("int_of_string")
->
print_string usage ;
print_string errmsg ;
flush stdout ;
failwith "\n *** Error when calling lucky.\n"
source/command_line_luc_exe.mli
View file @ 18e59b0d
(*-----------------------------------------------------------------------
** Copyright (C) - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
** Public License
**-----------------------------------------------------------------------
**
** File: command_line_luc_exe.mli
** Main author: jahier@imag.fr
*)
(** Handles everything that is related to command line calls.
(** Handles everything that is related to command line calls.
*)
......@@ -32,11 +32,11 @@ val cmd_line_string_to_int : string -> string -> int
the convertion failed.
*)
type cmd_line_optionT =
StepNb | Seed | Precision | Boot | ShowAut | NoShowAut | Verbose
type cmd_line_optionT =
StepNb | Seed | Precision | Boot | ShowAut | NoShowAut | Verbose
| Locals | Help | Inside | Edges | Vertices | ComputeVolume
val string_to_option: (string * cmd_line_optionT) list
(** Mapping from options string (e.g., "--with_seed") to the cmd_line_optionT
(** Mapping from options string (e.g., "--with_seed") to the cmd_line_optionT
type. *)
source/constraint.ml
View file @ 18e59b0d
(*-----------------------------------------------------------------------
** Copyright (C) 2002, 2003 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
** Public License
**-----------------------------------------------------------------------
**
** File: constraint.ml
......@@ -10,50 +10,50 @@
(* exported *)
type ineq =
type ineq =
| GZ of Ne.t (** expr > 0 *)
| GeqZ of Ne.t (** expr >= 0 *)
(* exported *)
type t =
type t =
| Bv of Exp.var (** Booleans *)
| EqZ of Ne.t (** expr = 0 *)
| Ineq of ineq (** > or >= *)
(* exported *)
let (ineq_to_string : ineq -> string) =
fun f ->
fun f ->
match f with
| GZ(ne) -> ((Ne.to_string ne) ^ " > 0 ")
| GeqZ(ne) -> ((Ne.to_string ne) ^ " >= 0 ")
(* exported *)
let (to_string : t -> string) =
fun f ->
fun f ->
match f with
| Bv(var) -> (Var.name var)
| Ineq(ineq) -> ineq_to_string ineq
| EqZ(ne) -> ((Ne.to_string ne) ^ " = 0 ")
let (print : t -> unit) =
fun cstr ->
fun cstr ->
Format.print_string (to_string cstr)
let (print_ineq : ineq -> unit) =
fun ineq ->
fun ineq ->
Format.print_string (ineq_to_string ineq)
(* exported *)
let (dimension_ineq : ineq -> int) =
fun cstr ->
fun cstr ->
match cstr with
GZ(ne) -> Ne.dimension ne
| GeqZ(ne) -> Ne.dimension ne
(* exported *)
let (dimension : t -> int) =
fun cstr ->
fun cstr ->
match cstr with
Bv(_) -> 1
| Ineq(ineq) -> dimension_ineq ineq
......@@ -62,14 +62,14 @@ let (dimension : t -> int) =
(* exported *)
let (neg_ineq : ineq -> ineq) =
fun cstr ->
fun cstr ->
match cstr with
GZ(ne) -> GeqZ(Ne.neg_nexpr ne)
| GeqZ(ne) -> GZ(Ne.neg_nexpr ne)
(* exported *)
let (opp_ineq : ineq -> ineq) =
fun cstr ->
fun cstr ->
match cstr with
GZ(ne) -> GZ(Ne.neg_nexpr ne)
| GeqZ(ne) -> GeqZ(Ne.neg_nexpr ne)
......@@ -77,14 +77,14 @@ let (opp_ineq : ineq -> ineq) =
(* exported *)
let (apply_subst_ineq : Ne.subst -> ineq -> ineq) =
fun s cstr ->
fun s cstr ->
match cstr with
GZ(ne) -> GZ(Ne.apply_subst ne s)
| GeqZ(ne) -> GeqZ(Ne.apply_subst ne s)
(* exported *)
let (apply_subst : Ne.subst -> t -> t) =
fun s cstr ->
fun s cstr ->
match cstr with
Bv(_) -> cstr
| Ineq(ineq) -> Ineq(apply_subst_ineq s ineq)
......@@ -92,14 +92,14 @@ let (apply_subst : Ne.subst -> t -> t) =
(* exported *)
let (apply_substl_ineq : Ne.subst list -> ineq -> ineq) =
fun s cstr ->
fun s cstr ->
match cstr with
GZ(ne) -> GZ(Ne.apply_substl s ne)
| GeqZ(ne) -> GeqZ(Ne.apply_substl s ne)
(* exported *)
let (apply_substl : Ne.subst list -> t -> t) =
fun s cstr ->
fun s cstr ->
match cstr with
Bv(_) -> cstr
| Ineq(ineq) -> Ineq(apply_substl_ineq s ineq)
......@@ -108,25 +108,25 @@ let (apply_substl : Ne.subst list -> t -> t) =
(* exported *)
let (eval_ineq : Var.num_subst list -> ineq -> bool) =
fun s ineq ->
fun s ineq ->
match ineq with
GZ(ne) -> Value.num_sup_zero(Ne.eval ne s)
| GeqZ(ne) -> Value.num_supeq_zero(Ne.eval ne s)
(* exported *)
let (get_vars_ineq : ineq -> string list) =
fun ineq ->
fun ineq ->
match ineq with
GZ(ne) -> Ne.get_vars ne
| GeqZ(ne) -> Ne.get_vars ne
(* exported *)
let (get_vars : t -> string list) =
fun cstr ->
fun cstr ->
match cstr with
Bv var -> [(Var.name var)]
| EqZ ne -> Ne.get_vars ne
| Ineq ineq -> get_vars_ineq ineq
source/constraint.mli
View file @ 18e59b0d
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
** Public License
**-----------------------------------------------------------------------
**
** File: constraint.mli
......@@ -14,12 +14,12 @@
(** Normalised linear constraints. *)
(* exported *)
type ineq =
type ineq =
| GZ of Ne.t (** expr > 0 *)
| GeqZ of Ne.t (** expr >= 0 *)
(* exported *)
type t =
type t =
| Bv of Exp.var (** booleans *)
| EqZ of Ne.t (** expr = 0 *)
| Ineq of ineq (** > or >= *)
......@@ -32,7 +32,7 @@ val dimension_ineq : ineq -> int
val get_vars : t -> string list
val get_vars_ineq : ineq -> string list
(** [apply_subst cstr s] applies [s] to [cstr]. Note that the result could
(** [apply_subst cstr s] applies [s] to [cstr]. Note that the result could
have been multiplied by a constant. *)
val apply_subst : Ne.subst -> t -> t
val apply_subst_ineq : Ne.subst -> ineq -> ineq
......
source/control.ml
View file @ 18e59b0d
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
** Public License
**-----------------------------------------------------------------------
**
** File: control.ml
......@@ -26,40 +26,40 @@ end
XXX Normal draw.
*)
type recovery_info
type recovery_info
(* = (int * int) option *)
= Inter of int * int | Never | Always
let (string_of_recov : recovery_info -> string) =
fun r ->
fun r ->
match r with
None -> ""
| Some(min, max) ->
| Some(min, max) ->
(" [" ^ (string_of_int min) ^ ", " ^ (string_of_int max) ^ "]")
(* exported *)
type state = (int * recovery_info) StringMap.t
type state = (int * recovery_info) StringMap.t
(* exported *)
let (compose_state : state -> state -> state) =
fun st1 st2 ->
(StringMap.fold
(StringMap.fold
(fun str v acc -> StringMap.add str v acc)
st1
st1
st2)
(* fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b *)
let (state_size : state -> int) =
fun st ->
fun st ->
StringMap.fold (fun _ _ cpt -> cpt+1) st 0
(* exported *)
let (print_state : state -> unit) =
fun st ->
let (pp: string -> int * recovery_info -> unit) =
fun id (i, recov) ->
let (print_state : state -> unit) =
fun st ->
let (pp: string -> int * recovery_info -> unit) =
fun id (i, recov) ->
output_string stderr ("\t" ^ id ^ " = ");
output_string stderr (string_of_int i);
output_string stderr (" (" ^ (string_of_recov recov) ^ ")\n")
......@@ -70,29 +70,29 @@ let (print_state : state -> unit) =
(* exported *)
let (new_state : unit -> state) =
fun _ ->
fun _ ->
StringMap.empty
(* exported *)
let (set : string -> int -> state -> state) =
fun id i st ->
fun id i st ->
StringMap.add id (i, None) st
(* exported *)
let (set_between : string -> int -> int -> int -> state -> state) =
fun id i min max st ->
StringMap.add id (i, Some(min, max)) st
fun id i min max st ->
StringMap.add id (i, Some(min, max)) st
(* exported *)
let (draw_between : string -> int -> int -> state -> state) =
fun id min max st ->
fun id min max st ->
let draw = min + (Random.int (max - min + 1)) in
StringMap.add id (draw, (Some(min, max))) st
(* exported *)
let (draw_gauss : string -> float -> float -> state -> state) =
fun id m std st ->
fun id m std st ->
let f = Util.gauss_draw m std in
let max_recovering = int_of_float (m +. 100. *. std) in
let min_recovering = int_of_float (m -. 100. *. std) in
......@@ -101,33 +101,33 @@ let (draw_gauss : string -> float -> float -> state -> state) =
(* exported *)
let (dec : string -> state -> state) =
fun id st ->
fun id st ->
assert (StringMap.mem id st);
( match (StringMap.find id st) with
(i, None) ->
(i, None) ->
StringMap.add id (i-1, None) st
| (i, Some(min, max)) ->
| (i, Some(min, max)) ->
StringMap.add id (i-1, Some(min-1, max-1)) st
)
(* exported *)
let (return : string -> state -> int) =
fun id st ->
fun id st ->
try fst (StringMap.find id st)
with _ ->
with _ ->
print_state st;
failwith ("*** " ^ id ^ " is an undefined control expression.\n")
(* exported *)
let (return_comp : string -> state -> int) =
fun id st ->
fun id st ->
if (fst (StringMap.find id st)) > 0 then 0 else 1
(* exported *)
let (is_recoverable : string -> state -> bool) =
fun id st ->
fun id st ->
let (v, r) = StringMap.find id st in
match StringMap.find id st with
match StringMap.find id st with
(_,None) -> false
| (i, Some(min, max)) -> (i<=0 && max >= 1) || (i>0 && min <=0)
......@@ -136,26 +136,26 @@ let (is_recoverable : string -> state -> bool) =
type expr = state -> state
let (compose_expr : expr -> expr -> expr) =
fun e1 e2 ->
fun e1 e2 ->
(fun state -> e2 (e1 state))
type test =
| EqExpr of number * number
| GtExpr of number * number
| GeExpr of number * number
and number =
| VarExpr of string
| IntExpr of int
type test =
| EqExpr of number * number
| GtExpr of number * number
| GeExpr of number * number
and number =
| VarExpr of string
| IntExpr of int
let (ite : test -> expr -> expr -> state -> state) =
fun test e1 e2 st ->
fun test e1 e2 st ->
let number_to_int st n =
match n with
match n with
VarExpr(id) -> return id st
| IntExpr(i) -> i
in
let bool =
let bool =
match test with
EqExpr(n1, n2) -> ((number_to_int st n1) = (number_to_int st n2))
| GtExpr(n1, n2) -> ((number_to_int st n1) > (number_to_int st n2))
......
source/control.mli
View file @ 18e59b0d
(*-----------------------------------------------------------------------
** Copyright (C) 2002 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
** Public License
**-----------------------------------------------------------------------
**
** File: control.mli
......@@ -54,17 +54,17 @@ val is_recoverable : string -> state -> bool
For instance, if [v] has been drawn to 5 after a draw between 2 and
9, it means that all values from 2 to 9 would have been legal
too. Therefore, if:
- a loop is garded by the value of v,
too. Therefore, if:
- a loop is garded by the value of v,
- [v] is bound to 0 at the current step,
- no satisfiable formula can be drawn in the end branch of the
loop,
then, since [v] could have been drawn to a bigger value (7, 8, or 9),
it means that the body of the loop can be tried some more.
Similarly, if:
- [v] is not bound to 0 at the current step, but at least 2 steps
then, since [v] could have been drawn to a bigger value (7, 8, or 9),
it means that the body of the loop can be tried some more.
Similarly, if:
- [v] is not bound to 0 at the current step, but at least 2 steps
have performed
- the formula in the body of the loop is not satisfiable
......@@ -78,22 +78,22 @@ val is_recoverable : string -> state -> bool
type expr = state -> state
(** e.g., [loop_between foo 3 10] is a [expr].
[(return "foo" (loop_between "foo" 3 10)] is a [post_expr].
(** e.g., [loop_between foo 3 10] is a [expr].
[(return "foo" (loop_between "foo" 3 10)] is a [post_expr].
*)
val compose_expr : expr -> expr -> expr
type test =
| EqExpr of number * number
| GtExpr of number * number
| GeExpr of number * number
and number =
| VarExpr of string
| IntExpr of int
type test =
| EqExpr of number * number
| GtExpr of number * number
| GeExpr of number * number
and number =
| VarExpr of string
| IntExpr of int
val ite : test -> expr -> expr -> state -> state
val ite : test -> expr -> expr -> state -> state
(** [ite test e1 e2 st] evaluates [e1] if [test] is true, [e2] otherwise. *)
val state_size : state -> int
source/draw.ml
View file @ 18e59b0d
(*-----------------------------------------------------------------------
** Copyright (C) 2003 - Verimag.
** This file may only be copied under the terms of the GNU Library General
** Public License
** Public License
**-----------------------------------------------------------------------
**
** File: draw.ml
......@@ -15,27 +15,27 @@ open Polyhedron
(* Each point of the polyhedron is defined by the list of its coordinates *)