Commit 94d83c01 authored by Erwan Jahier's avatar Erwan Jahier
Browse files

lurette 0.49 Tue, 26 Mar 2002 16:22:45 +0100 by jahier

Parent-Version:      0.48
Version-Log:

Clean up a little bit the ima format to make it sipler to parse
and to avoid reducing  the naming space as much as possible.

Project-Description: Lurette
parent 1c7769db
;; -*- Prcs -*-
(Created-By-Prcs-Version 1 3 3)
(Project-Description "Lurette")
(Project-Version lurette 0 48)
(Parent-Version lurette 0 47)
(Project-Version lurette 0 49)
(Parent-Version lurette 0 48)
(Version-Log "
Add support for (boolean and numeric) if-then-else.
Remove the eval.ml module as the replacement of pre and input
vars is now done in Solver.formula_to_bdd.
Add a new module gne.ml that provides a garded normal expressions
data structure that is used to handle if-then-elses.
Also introduce a new field to env_state called bdd_tbl_global which
is used to cache the result of formula_to_bdd for bdds that do not
depend on pre nor input vars. The field bdd_tbl which cache the other
reults is now cleared at each step because it is useless to store results
that depends on pre and inputs.
Clean up a little bit the ima format to make it sipler to parse
and to avoid reducing the naming space as much as possible.
")
(New-Version-Log "")
(Checkin-Time "Fri, 22 Mar 2002 14:29:17 +0100")
(Checkin-Time "Tue, 26 Mar 2002 16:22:45 +0100")
(Checkin-Login jahier)
(Populate-Ignore ())
(Project-Keywords)
......@@ -60,7 +49,7 @@ that depends on pre and inputs.
(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.10 644))
(source/parse_env.ml (lurette/41_parse_env. 1.11 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))
......@@ -111,10 +100,10 @@ that depends on pre and inputs.
;; Various files used for testing purposes
(test/usager.env (lurette/b/14_usager.env 1.4 644))
(test/tram.env (lurette/b/15_tram.env 1.3 644))
(test/porte.env (lurette/b/16_porte.env 1.3 644))
(test/passerelle.env (lurette/b/17_passerelle 1.3 644))
(test/usager.env (lurette/b/14_usager.env 1.5 644))
(test/tram.env (lurette/b/15_tram.env 1.4 644))
(test/porte.env (lurette/b/16_porte.env 1.4 644))
(test/passerelle.env (lurette/b/17_passerelle 1.4 644))
(test/ControleurPorte.h (lurette/b/18_Controleur 1.1 644))
(test/ControleurPorte.c (lurette/b/19_Controleur 1.1 644))
......
......@@ -11,6 +11,8 @@
open Formula
let debug_parsing = true
type read_arc = Arc of node * arc_info * node
......@@ -23,9 +25,10 @@ type read_automata = Automata of
* read_arc list (* Transition list *)
(* Keywords of the automata format *)
let lexer = Genlex.make_lexer ["["; "]"; "("; ")"; ","; ":"; ";";
"And"; "Or"; "Not"; "true"; "false";
"="; ">"; ">="; "<"; "<="; "IfThenElse";"IfThenElseB";
let lexer = Genlex.make_lexer ["("; ")"; ","; ";"; ".";
"&&"; "||"; "!"; "true"; "false";
"IfThenElseExpr";"IfThenElse";
"="; ">"; ">="; "<"; "<=";
"+"; "-"; "*"; "/"; "mod"; "%"]
type aut_token = Genlex.token Stream.t
......@@ -43,9 +46,6 @@ let print_genlex_token =
in
print_string "\n\t"
(* false by default because it produces outputs even if everything is fine *)
let debug_parsing = false
let print_err_msg tok_list func =
if debug_parsing then
begin
......@@ -65,9 +65,10 @@ let rec
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
[< vnt = parse ; tail = (parse_list_var_tail (parse)) >]
| [< 'Genlex.Kwd "," >] -> [] (* empty list *)
| [< 'Genlex.Kwd "." >] -> [] (* empty list *)
| [< vnt = parse ; tail = (parse_list_var_tail (parse)) >]
-> vnt :: tail
| [< >] -> [] (* empty list *)
with e ->
print_err_msg tok_list "parse_list";
raise e
......@@ -76,10 +77,11 @@ and (parse_list_var_tail: (aut_token -> 'a) -> aut_token -> 'a list) =
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
| [< 'Genlex.Kwd ",">] -> [] (* end of the list *)
| [< 'Genlex.Kwd ".">] -> [] (* end of the list *)
| [< 'Genlex.Kwd ";" ; a = parse ;
tail = (parse_list_var_tail (parse)) >]
-> a :: tail
| [< >] -> [] (* end of the list *)
with e ->
print_err_msg tok_list "parse_list_var_tail";
raise e
......@@ -91,29 +93,14 @@ let rec (parse_automata: aut_token -> read_automata) =
let tok_list = Stream.npeek 20 tok in
try
match tok with parser
[< 'Genlex.Ident "start"; 'Genlex.Ident "node"; 'Genlex.Kwd "=";
'Genlex.Int node_id ; 'Genlex.Kwd "," ;
'Genlex.Ident "input"; 'Genlex.Ident "vars"; 'Genlex.Kwd "=";
'Genlex.Kwd "[" ; li = parse_list_var ; 'Genlex.Kwd "]" ;
'Genlex.Kwd "," ;
'Genlex.Ident "output"; 'Genlex.Ident "vars"; 'Genlex.Kwd "=";
'Genlex.Kwd "[" ; lo = parse_list_genvar ; 'Genlex.Kwd "]" ;
[< '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 "start_node"; 'Genlex.Kwd "="; 'Genlex.Int node_id ;
'Genlex.Kwd "," ;
'Genlex.Ident "local"; 'Genlex.Ident "vars"; 'Genlex.Kwd "=";
'Genlex.Kwd "[" ; ll = parse_list_genvar ; 'Genlex.Kwd "]" ;
'Genlex.Kwd "," ;
'Genlex.Ident "pre"; 'Genlex.Ident "vars"; 'Genlex.Kwd "=";
'Genlex.Kwd "[" ; lpre = parse_list_var ; 'Genlex.Kwd "]" ;
'Genlex.Kwd "," ;
'Genlex.Ident "arcs"; 'Genlex.Kwd "=";
'Genlex.Kwd "[" ;
la = parse_list_arc (List.append li (List.append lo (List.append ll lpre))) ;
'Genlex.Kwd "]"
'Genlex.Ident "arcs"; 'Genlex.Kwd "="; la = parse_list_arc
(List.append li (List.append lo (List.append ll lpre)))
>]
-> Automata(node_id, li, lo, ll, lpre, la)
with e ->
......@@ -220,9 +207,9 @@ and (parse_arc: vnt list -> aut_token -> read_arc) =
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
[< 'Genlex.Kwd "("; 'Genlex.Int node_from ;
'Genlex.Kwd ","; arc_info = parse_arc_info vars;
'Genlex.Kwd "," ; 'Genlex.Int node_to ; 'Genlex.Kwd ")"; >]
[< 'Genlex.Ident "From"; 'Genlex.Int node_from ;
'Genlex.Ident "To"; 'Genlex.Int node_to ;
'Genlex.Ident "With"; arc_info = parse_arc_info vars >]
-> Arc(node_from, arc_info, node_to)
with e ->
print_err_msg tok_list "parse_arc" ;
......@@ -232,7 +219,7 @@ and (parse_arc_info: vnt list -> aut_token -> arc_info) =
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
[< 'Genlex.Int weigth ; 'Genlex.Kwd ":"; expr = parse_formula_eps vars >]
[< 'Genlex.Int weigth ; 'Genlex.Ident ":"; expr = parse_formula_eps vars >]
-> (weigth, expr)
with e ->
print_err_msg tok_list "parse_arc_info" ;
......@@ -243,7 +230,8 @@ and (parse_formula_eps: vnt list -> aut_token -> formula_eps) =
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
[< 'Genlex.Ident "eps" >] -> Eps
| [< 'Genlex.Ident "eps" >] -> Eps
| [< 'Genlex.Ident "("; 'Genlex.Ident "eps"; 'Genlex.Ident ")" >] -> Eps
| [< f = parse_formula vars >] -> Form(f)
with e ->
print_err_msg tok_list "parse_formula_eps" ;
......@@ -254,9 +242,9 @@ and (parse_formula: vnt list -> aut_token -> formula) =
let tok_list = Stream.npeek 10 tok in
try
match tok with parser
[< 'Genlex.Kwd "Not"; f1 = parse_formula vars;
[< 'Genlex.Kwd "!"; f1 = parse_formula vars;
f = parse_more_formula (Not(f1)) vars >] -> f
| [< 'Genlex.Kwd "IfThenElseB"; f1 = parse_formula vars; f2 = parse_formula vars;
| [< 'Genlex.Kwd "IfThenElse"; f1 = parse_formula vars; f2 = parse_formula vars;
f3 = parse_formula vars >] -> IteB(f1, f2, f3)
| [< 'Genlex.Kwd "("; f1 = parse_formula vars ; 'Genlex.Kwd ")" ;
f = parse_more_formula f1 vars >] -> f
......@@ -297,8 +285,8 @@ 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 "Or"; f2 = parse_formula vars >] -> Or(f1, f2)
| [< 'Genlex.Kwd "And"; f2 = parse_formula vars >] -> And(f1, f2)
[< 'Genlex.Kwd "||"; f2 = parse_formula vars >] -> Or(f1, f2)
| [< 'Genlex.Kwd "&&"; f2 = parse_formula vars >] -> And(f1, f2)
| [< >] -> f1
with e ->
print_err_msg tok_list "parse_more_formula" ;
......@@ -362,7 +350,7 @@ and (parse_simple: vnt list -> aut_token -> expr) =
var
| [< 'Genlex.Int i >] -> Ival(i)
| [< 'Genlex.Float f >] -> Fval(f)
| [< 'Genlex.Kwd "IfThenElse"; f1 = parse_formula vars; e2 = parse_expr vars;
| [< 'Genlex.Kwd "IfThenElseExpr"; f1 = parse_formula vars; e2 = parse_expr vars;
e3 = parse_expr vars >] -> Ite(f1, e2, e3)
| [< 'Genlex.Kwd "("; e = parse_expr vars; 'Genlex.Kwd ")" >] -> e
(* La passerelle *)
start node = 0,
input vars = [
inputs =
(baisser_pass,bool);
(rentrer_pass,bool);
(ouvrir_porte,bool);
(fermer_porte,bool);
(porte_et_pass_ok,bool)
],
output vars = [
(porte_et_pass_ok,bool),
outputs =
(pass_baissee,bool);
(pass_rentree,bool)
],
local vars = [],
pre vars = [],
arcs = [
(0, 1: Not pass_rentree And Not pass_baissee,1) ;
(1, 1: eps,2);
(2, 1: eps,3);
(3, 1: Not pass_baissee And Not pass_rentree And Not baisser_pass And Not rentrer_pass,2);
(2, 1: eps,4);
(4, 1: eps,5);
(5, 1: eps,6);
(6, 1: Not pass_baissee And Not pass_rentree And baisser_pass,5);
(5, 1: eps,7);
(7, 1: Not pass_rentree And pass_baissee,1);
(4, 1: eps,8);
(8, 1: eps,9);
(9, 1: Not pass_baissee And Not pass_rentree And rentrer_pass,8);
(8, 1: eps,10);
(10, 1: pass_rentree And Not pass_baissee,1)
]
(pass_rentree,bool),
locals = ,
pre = ,
start_node = 0,
arcs =
From 0 To 1 With 1: (! pass_rentree && ! pass_baissee );
From 1 To 2 With 1: eps;
From 2 To 3 With 1: eps;
From 3 To 2 With 1: (! pass_baissee && ! pass_rentree && ! baisser_pass && ! rentrer_pass);
From 2 To 4 With 1: eps;
From 4 To 5 With 1: eps;
From 5 To 6 With 1: eps;
From 6 To 5 With 1: (! pass_baissee && ! pass_rentree && baisser_pass);
From 5 To 7 With 1: eps;
From 7 To 1 With 1: (! pass_rentree && pass_baissee);
From 4 To 8 With 1: eps;
From 8 To 9 With 1: eps;
From 9 To 8 With 1: (! pass_baissee && ! pass_rentree && rentrer_pass);
From 8 To 10 With 1: eps;
From 10 To 1 With 1: (pass_rentree && ! pass_baissee)
.
(* La porte *)
start node = 0,
input vars = [(baisser_pass,bool);(rentrer_pass,bool);(ouvrir_porte,bool);
(fermer_porte,bool);(porte_et_pass_ok,bool)],
output vars = [(porte_ouverte,bool);(porte_fermee,bool)],
local vars = [],
pre vars = [],
arcs = [
(0, 1 : Not porte_fermee And Not porte_ouverte,1);
(1, 1 : eps,2);
(2, 1 : eps,3);
(3, 1 : Not porte_ouverte And Not porte_fermee And Not ouvrir_porte And Not fermer_porte,2);
(2, 1 : eps,4);
(4, 1 : eps,5);
(5, 1 : eps,6);
(6, 1 : Not porte_ouverte And Not porte_fermee And ouvrir_porte,5);
(5, 1 : eps,7);
(7, 1 : Not porte_fermee And porte_ouverte,1);
(4, 1 : eps,8);
(8, 1 : eps,9);
(9, 1 : Not porte_ouverte And Not porte_fermee And fermer_porte,8);
(8, 1 : eps,10);
(10,1 : porte_fermee And Not porte_ouverte,1)
]
inputs = (baisser_pass,bool);
(rentrer_pass,bool);
(ouvrir_porte,bool);
(fermer_porte,bool);
(porte_et_pass_ok,bool),
outputs = (porte_ouverte,bool);
(porte_fermee,bool),
locals = ,
pre = ,
start_node = 0,
arcs =
From 0 To 1 With 1 : ! porte_fermee && ! porte_ouverte ;
From 1 To 2 With 1 : eps ;
From 2 To 3 With 1 : eps ;
From 3 To 2 With 1 : ! porte_ouverte && ! porte_fermee && ! ouvrir_porte && ! fermer_porte ;
From 2 To 4 With 1 : eps ;
From 4 To 5 With 1 : eps ;
From 5 To 6 With 1 : eps ;
From 6 To 5 With 1 : ! porte_ouverte && ! porte_fermee && ouvrir_porte ;
From 5 To 7 With 1 : eps ;
From 7 To 1 With 1 : ! porte_fermee && porte_ouverte ;
From 4 To 8 With 1 : eps ;
From 8 To 9 With 1 : eps ;
From 9 To 8 With 1 : ! porte_ouverte && ! porte_fermee && fermer_porte ;
From 8 To 10 With 1 : eps ;
From 10 To 1 With 1 : porte_fermee && ! porte_ouverte
.
(* Le Tram *)
start node = 0,
input vars = [(baisser_pass,bool);
inputs = (baisser_pass,bool);
(rentrer_pass,bool);
(ouvrir_porte,bool);
(fermer_porte,bool);
(porte_et_pass_ok,bool)
],
output vars = [(en_marche,bool);
,
outputs = (en_marche,bool);
(debut_ramassage,bool);
(fin_ramassage,bool)
],
local vars = [],
pre vars = [],
arcs = [
(0,1:eps,1);
(1,1:eps,2);
(2,1:en_marche And Not debut_ramassage And Not fin_ramassage,1);
(1,1:eps,3);
(3,1:Not fin_ramassage And debut_ramassage And Not en_marche,4);
(4,1:eps,5);
(5,1:Not fin_ramassage And Not debut_ramassage And Not en_marche,4);
(4,1:eps,6);
(6,1:fin_ramassage And Not debut_ramassage And Not en_marche,7);
(7,1:eps,8);
(8,1:Not fin_ramassage And Not debut_ramassage And Not en_marche And Not porte_et_pass_ok,7);
(7,1:eps,9);
(9,1:Not fin_ramassage And Not debut_ramassage And en_marche And porte_et_pass_ok,0)
]
,
locals = ,
pre = ,
start_node = 0,
arcs =
From 0 To 1 With 1:eps;
From 1 To 2 With 1:eps;
From 2 To 1 With 1:(en_marche && ! debut_ramassage && ! fin_ramassage);
From 1 To 3 With 1:eps;
From 3 To 4 With 1:(! fin_ramassage && debut_ramassage && ! en_marche);
From 4 To 5 With 1:eps;
From 5 To 4 With 1:(! fin_ramassage && ! debut_ramassage && ! en_marche);
From 4 To 6 With 1:eps;
From 6 To 7 With 1:(fin_ramassage && ! debut_ramassage && ! en_marche);
From 7 To 8 With 1:eps;
From 8 To 7 With 1:(! fin_ramassage && ! debut_ramassage && ! en_marche && ! porte_et_pass_ok);
From 7 To 9 With 1:eps;
From 9 To 0 With 1:(! fin_ramassage && ! debut_ramassage && en_marche && porte_et_pass_ok)
.
(* Les usagers *)
start node = 0,
input vars = [(baisser_pass,bool);(rentrer_pass,bool);(ouvrir_porte,bool);
(fermer_porte,bool);(porte_et_pass_ok,bool)],
output vars = [(demande_pass,bool);(demande_porte,bool)],
local vars = [],
pre vars = [],
arcs = [
(0, 1: eps,1);
(1, 1: eps,2);
(2, 1: demande_porte Or demande_pass,0);
(1, 1: eps,3);
(3, 1: (Not demande_porte) Or (Not demande_pass),0)
]
inputs = (baisser_pass,bool);(rentrer_pass,bool);(ouvrir_porte,bool);
(fermer_porte,bool);(porte_et_pass_ok,bool),
outputs = (demande_pass,bool);(demande_porte,bool),
locals = ,
pre = ,
start_node = 0,
arcs =
From 0 To 1 With 1: eps;
From 1 To 2 With 1: eps;
From 2 To 0 With 1: demande_porte || demande_pass;
From 1 To 3 With 1: eps ;
From 3 To 0 With 1: (! demande_porte) || (! demande_pass)
.
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