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

lurette 0.51 Wed, 27 Mar 2002 17:46:03 +0100 by jahier

Parent-Version:      0.50
Version-Log:

Change the way pre are translated in the .env file. Now
instead of writting "_pre2toto", one writes "pre(2,toto)".

But internally, it is handled the same way as before (i.e., the first
thing I do when parsing the env file is to transform "pre(2,toto)"
into "_pre2toto" (it makes the hangling of pre vars much more
homogeneous with the way the other vars are handled.

Also fix a bug where it was not possible to have a pre on input
vars because the update_pre was failing to proceed quietly  whenever
one of its var was not computable because its pre does have a value.
Also give an appropriate error message whenever the user wrongly
use a pre on a var that can not be computed.

Project-Description: Lurette
parent c699a9b3
......@@ -5,7 +5,7 @@
# For updates see:
# http://miss.wu-wien.ac.at/~mottl/ocaml_sources
#
# $Id: OcamlMakefile 1.22 Thu, 14 Mar 2002 18:45:50 +0100 jahier $
# $Id: OcamlMakefile 1.23 Wed, 27 Mar 2002 17:46:03 +0100 jahier $
#
###########################################################################
......@@ -97,13 +97,13 @@ NCRESULT := $(addsuffix $(NCSUFFIX), $(RESULT))
TOPRESULT := $(addsuffix $(TOPSUFFIX), $(RESULT))
ifndef OCAMLC
OCAMLC := ocamlc
OCAMLC := ocamlc.opt
endif
export OCAMLC
ifndef OCAMLOPT
OCAMLOPT := ocamlopt
OCAMLOPT := ocamlopt.opt
endif
export OCAMLOPT
......@@ -139,7 +139,7 @@ endif
export OTAGS
ifndef OCAMLLEX
OCAMLLEX := ocamllex
OCAMLLEX := ocamllex.opt
endif
export OCAMLLEX
......@@ -561,9 +561,11 @@ ocamlprof:
# Produces an html version of the lurette documentation
dochtml:
ocamldoc -t "Lurette modules interfaces" -pp "camlp4o" -html -d ../doc/html -stars \
ocamldoc -t "Lurette modules interfaces" -pp "camlp4o" \
-g ~/incoming/ocamldoc-pre4/odoc_fhtml.cmo \
-d ../doc/html -stars \
-keep-code -colorize-code -I ../source/ $(SOURCES_OCAML) \
../source/gen_stubs.ml
../source/gen_stubs.ml
doctex:
ocamldoc -t "Lurette modules interfaces" -pp "camlp4o" -no-stop -latex -d ../doc -stars \
......
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 50)
(Parent-Version lurette 0 49)
(Project-Version lurette 0 51)
(Parent-Version lurette 0 50)
(Version-Log "
Add the possibility to put pragmas in the .env files.
Change the way pre are translated in the .env file. Now
instead of writting \"_pre2toto\", one writes \"pre(2,toto)\".
But internally, it is handled the same way as before (i.e., the first
thing I do when parsing the env file is to transform \"pre(2,toto)\"
into \"_pre2toto\" (it makes the hangling of pre vars much more
homogeneous with the way the other vars are handled.
Also fix a bug where it was not possible to have a pre on input
vars because the update_pre was failing to proceed quietly whenever
one of its var was not computable because its pre does have a value.
Also give an appropriate error message whenever the user wrongly
use a pre on a var that can not be computed.
")
(New-Version-Log "")
(Checkin-Time "Wed, 27 Mar 2002 13:36:39 +0100")
(Checkin-Time "Wed, 27 Mar 2002 17:46:03 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -19,14 +32,14 @@ Add the possibility to put pragmas in the .env files.
;; Sources files for ima_exe
(source/ima_exe.mli (lurette/b/31_ima_exe.ml 1.1 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.2 644))
(source/ima_exe.ml (lurette/b/32_ima_exe.ml 1.3 644))
(source/command_line_ima_exe.ml (lurette/b/33_command_li 1.2 644))
(source/command_line_ima_exe.mli (lurette/b/34_command_li 1.1 644))
;; Sources files for lurette only
(source/lurette.mli (lurette/11_lurette.ml 1.12 644))
(source/lurette.ml (lurette/12_lurette.ml 1.29 644))
(source/lurette.ml (lurette/12_lurette.ml 1.30 644))
(source/command_line.ml (lurette/b/20_command_li 1.4 644))
(source/command_line.mli (lurette/b/21_command_li 1.4 644))
......@@ -36,18 +49,18 @@ Add the possibility to put pragmas in the .env files.
(source/graph.ml (lurette/14_graph.ml 1.5 644))
(source/env.mli (lurette/15_env.mli 1.10 644))
(source/env.ml (lurette/16_env.ml 1.20 644))
(source/env.ml (lurette/16_env.ml 1.21 644))
(source/util.ml (lurette/35_util.ml 1.15 644))
(source/solver.mli (lurette/38_solver.mli 1.10 644))
(source/solver.ml (lurette/39_solver.ml 1.17 644))
(source/solver.ml (lurette/39_solver.ml 1.18 644))
(source/rnumsolver.mli (lurette/b/26_rnumsolver 1.2 644))
(source/rnumsolver.ml (lurette/b/27_rnumsolver 1.4 644))
(source/parse_env.mli (lurette/40_parse_env. 1.6 644))
(source/parse_env.ml (lurette/41_parse_env. 1.12 644))
(source/parse_env.ml (lurette/41_parse_env. 1.13 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))
......@@ -73,7 +86,7 @@ Add the possibility to put pragmas in the .env files.
(source/gen_stubs.ml (lurette/24_generate_l 1.20 644))
;; Make files
(OcamlMakefile (lurette/17_OcamlMakef 1.22 644))
(OcamlMakefile (lurette/17_OcamlMakef 1.23 644))
(Makefile (lurette/18_Makefile 1.24 644))
(interface/Makefile (lurette/25_Makefile 1.6 644))
(test/Makefile_ima_exe (lurette/b/35_Makefile_i 1.2 644))
......
......@@ -308,20 +308,33 @@ let _ = assert ((get_pre_var "_pre1toto") = "toto")
(* exported *)
let (update_pre: env_in -> env_out -> env_loc -> unit) =
fun input output local ->
let (update_one_pre_var : var_name -> subst) =
let (maybe_update_one_pre_var : var_name -> subst option) =
fun pre_vn ->
let vn = get_pre_var pre_vn in
let pre_value =
try Hashtbl.find input vn
try
let pre_value =
try Hashtbl.find input vn
with Not_found ->
try List.assoc vn output
with Not_found ->
List.assoc vn local
in
Some((pre_vn, pre_value))
with Not_found ->
try List.assoc vn output
with Not_found ->
try List.assoc vn local
with Not_found -> assert false
in
(pre_vn, pre_value)
(* At the second step, input vars migth still not be avaible if
the env starts generate outputs. *)
None
in
env_state.pre <- List.map (update_one_pre_var) env_state.pre_var_names
let maybe_pre = List.map (maybe_update_one_pre_var) env_state.pre_var_names in
env_state.pre <-
List.fold_left
(fun acc ms ->
match ms with
Some(s) -> (s::acc)
| None -> acc
)
[]
maybe_pre
......
......@@ -222,9 +222,10 @@ and
main_loop t =
let _ = print_string ("\n# step " ^ (string_of_int t) ^ ":\n"); flush stdout in
let previous_nodes = env_state.current_nodes in
let input = read_rif_input (Env_state.in_env_unsorted ()) in
let previous_nodes = env_state.current_nodes in
let nll_out_loc_list = Env.env_try 1 1 input in
......
......@@ -314,7 +314,11 @@ and
(* Performs the steps *)
let _ = Lurette_stub.sut_step input in
let _ = if (options.oracle) then Lurette_stub.oracle_step input new_sut_output else true in
let _ =
if (options.oracle)
then Lurette_stub.oracle_step input new_sut_output
else true
in
Env.env_step nll input loc ;
let str =
......
......@@ -129,7 +129,7 @@ let rec (parse_automata: aut_token -> read_automata) =
[< 'Genlex.Ident "inputs"; 'Genlex.Kwd "="; li = parse_list_var ;
'Genlex.Ident "outputs"; 'Genlex.Kwd "="; lo = parse_list_genvar ;
'Genlex.Ident "locals"; 'Genlex.Kwd "="; ll = parse_list_genvar ;
'Genlex.Ident "pre"; 'Genlex.Kwd "="; lpre = parse_list_var ;
'Genlex.Ident "pre"; 'Genlex.Kwd "="; lpre = parse_list_prevar ;
'Genlex.Ident "start_node"; 'Genlex.Kwd "="; 'Genlex.Int node_id ;
'Genlex.Kwd "," ;
'Genlex.Ident "arcs"; 'Genlex.Kwd "="; la = parse_list_arc
......@@ -141,6 +141,33 @@ let rec (parse_automata: aut_token -> read_automata) =
raise e
and (parse_list_var: aut_token -> vnt list) =
fun tok ->
let tok_list = Stream.npeek 10 tok in
try
parse_list (parse_var) tok
with e ->
print_err_msg tok_list "parse_list_var" ;
raise e
and (parse_var: aut_token -> vnt) =
fun tok ->
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
[< 'Genlex.Kwd "("; 'Genlex.Ident var;
prag_var = parse_pragma_list ;
'Genlex.Kwd ","; 'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
->
( match typ with
"bool" -> (var, BoolT)
| "float" -> (var, FloatT(-.max_float, max_float))
| "int" -> (var, IntT(min_int, max_int))
| str -> failwith ("*** Bad type in .env: " ^ str )
)
with e ->
print_err_msg tok_list "parse_var" ;
raise e
and (parse_list_genvar: aut_token -> vnt list) =
fun tok ->
let tok_list = Stream.npeek 10 tok in
......@@ -202,31 +229,33 @@ and (parse_type_more: string -> string -> aut_token -> vnt) =
raise e
and (parse_list_var: aut_token -> vnt list) =
and (parse_list_prevar: aut_token -> vnt list) =
fun tok ->
let tok_list = Stream.npeek 10 tok in
try
parse_list (parse_var) tok
parse_list (parse_prevar) tok
with e ->
print_err_msg tok_list "parse_list_var" ;
print_err_msg tok_list "parse_list_prevar" ;
raise e
and (parse_var: aut_token -> vnt) =
and (parse_prevar: aut_token -> vnt) =
fun tok ->
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
[< 'Genlex.Kwd "("; 'Genlex.Ident var;
prag_var = parse_pragma_list ;
'Genlex.Kwd ","; 'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
[< 'Genlex.Kwd "("; 'Genlex.Ident "pre"; 'Genlex.Kwd "(";
'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident var;
'Genlex.Kwd ")"; pl = parse_pragma_list ;
'Genlex.Kwd ","; 'Genlex.Ident typ ; 'Genlex.Kwd ")" >]
->
let pre_var = ("_pre" ^ (string_of_int i) ^ var) in
( match typ with
"bool" -> (var, BoolT)
| "float" -> (var, FloatT(-.max_float, max_float))
| "int" -> (var, IntT(min_int, max_int))
"bool" -> (pre_var, BoolT)
| "float" -> (pre_var, FloatT(-.max_float, max_float))
| "int" -> (pre_var, IntT(min_int, max_int))
| str -> failwith ("*** Bad type in .env: " ^ str )
)
with e ->
print_err_msg tok_list "parse_var" ;
print_err_msg tok_list "parse_prevar" ;
raise e
and (parse_list_arc: vnt list -> aut_token -> read_arc list) =
......@@ -292,11 +321,18 @@ and (parse_formula: vnt list -> aut_token -> formula) =
f = parse_more_formula True vars >] -> f
| [< 'Genlex.Kwd "false" ; pl = parse_pragma_list ;
f = parse_more_formula False vars >] -> f
| [< 'Genlex.Ident id ; pl = parse_pragma_list ;
| [< 'Genlex.Ident "pre"; 'Genlex.Kwd "("; 'Genlex.Int i ;
'Genlex.Kwd "," ; 'Genlex.Ident id; 'Genlex.Kwd ")";
pl = parse_pragma_list ;
f = parse_expr_or_bool_ident ("_pre" ^ (string_of_int i) ^ id) vars
>] -> f
| [< 'Genlex.Ident id ;
pl = parse_pragma_list ;
f1 = parse_expr_or_bool_ident id vars;
f = parse_more_formula f1 vars >] -> f
| [< e1 = parse_expr vars ; f1 = parse_expr_right e1 vars ;
f = parse_more_formula f1 vars >] -> f
| [< e1 = parse_expr vars ; f = parse_expr_right e1 vars
>] -> f
with e ->
print_err_msg tok_list "parse_formula" ;
raise e
......@@ -328,8 +364,10 @@ and (parse_more_formula: formula -> vnt list -> aut_token -> formula) =
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
[< 'Genlex.Kwd "||"; pl = parse_pragma_list ; f2 = parse_formula vars >] -> Or(f1, f2)
| [< 'Genlex.Kwd "&&"; pl = parse_pragma_list ; f2 = parse_formula vars >] -> And(f1, f2)
[< 'Genlex.Kwd "||"; pl = parse_pragma_list ;
f2 = parse_formula vars >] -> Or(f1, f2)
| [< 'Genlex.Kwd "&&"; pl = parse_pragma_list ;
f2 = parse_formula vars >] -> And(f1, f2)
| [< >] -> f1
with e ->
print_err_msg tok_list "parse_more_formula" ;
......@@ -387,7 +425,21 @@ and (parse_more_mults: expr -> vnt list -> aut_token -> expr) =
and (parse_simple: vnt list -> aut_token -> expr) =
fun vars tok ->
match tok with parser
[< 'Genlex.Ident s ; pl = parse_pragma_list >] ->
| [< 'Genlex.Ident "pre"; 'Genlex.Kwd "(";
'Genlex.Int i ; 'Genlex.Kwd "," ; 'Genlex.Ident id;
'Genlex.Kwd ")"; pl = parse_pragma_list >] ->
let s = ("_pre" ^ (string_of_int i) ^ id) in
let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in
let var =
match vt with
BoolT -> assert false
| IntT(_,_) -> Ivar(s)
| FloatT(_,_) -> Fvar(s)
in
var
| [< 'Genlex.Ident s ; pl = parse_pragma_list >] ->
let (_, vt) = List.find (fun (vn,vt) -> vn = s) vars in
let var =
match vt with
......@@ -396,7 +448,8 @@ and (parse_simple: vnt list -> aut_token -> expr) =
| FloatT(_,_) -> Fvar(s)
in
var
| [< 'Genlex.Int i; pl = parse_pragma_list >] -> Ival(i)
| [< 'Genlex.Int i; pl = parse_pragma_list >] -> Ival(i)
| [< 'Genlex.Float f; pl = parse_pragma_list >] -> Fval(f)
| [< 'Genlex.Kwd "IfThenElseExpr"; pl = parse_pragma_list ;
f1 = parse_formula vars;
......
......@@ -97,8 +97,15 @@ let rec (formula_to_bdd : env_in -> formula -> Bdd.t * bool) =
print_string (vn ^ " is not a boolean!\n");
assert false
| None ->
(Bdd.ithvar env_state.bdd_manager
(Env_state.atomic_formula_to_index (Bv(vn))), false)
if List.mem vn env_state.pre_var_names
then failwith
("*** " ^ vn ^ " is unknown at this stage.\n "
^ "*** Make sure you have not used "
^ "a pre on a output var at the 1st step, \n "
^ "*** or a pre on a input var at the second step in "
^ "your formula in the environment.\n ")
else (Bdd.ithvar env_state.bdd_manager
(Env_state.atomic_formula_to_index (Bv(vn))), false)
)
| Eq(e1, e2) ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment