Benjamin_Loison/Synchronous_reactive_systems
1
0
Fork 0
Code Issues 7 Pull Requests Packages Projects Releases Wiki Activity

[automaton] support for multiple output conditions

Browse Source
This commit is contained in:
sofamaniac 2023-01-05 18:31:12 +01:00
parent 094f403f5f
commit b2aa8bc6d5
5 changed files with 34 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/ast.ml
View File

@ -55,7 +55,7 @@ and t_equation = t_varlist * t_expression
and t_eqlist = t_equation list
and t_state = | State of ident * t_eqlist * t_expression * ident
and t_state = | State of ident * t_eqlist * (t_expression list) * (ident list)
and t_automaton = t_state * t_state list

13
src/lustre_pp.ml
View File

@ -153,14 +153,21 @@ let rec pp_automata fmt: t_automaton list -> unit = function
pp_translist trans
pp_automata tail
and pp_nexts fmt: t_expression list * string list -> unit = function
| [], [] -> ()
| e::exprs, n::nexts ->
Format.fprintf fmt "if %a then %s else %a"
pp_expression e
n
pp_nexts (exprs, nexts)
and pp_translist fmt: t_state list -> unit = function
| [] -> ()
| State(name, eqs, cond, next)::q ->
Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \t\t\tthen %s\n%a"
Format.fprintf fmt "\t\t\t|%s -> do\n%a\n\t\t\tdone until %a \n%a"
name
pp_equations eqs
pp_expression cond
next
pp_nexts (cond, next)
pp_translist q
let pp_node fmt node =

12
src/parser.mly
View File

@ -436,9 +436,10 @@ ident_comma_list:
transition:
| CASE IDENT BO_arrow DO equations DONE {
State($2, $5, EConst([TBool], CBool(true)), $2) }
| CASE IDENT BO_arrow DO equations UNTIL expr THEN IDENT {
State($2, $5, $7, $9)}
State($2, $5, [EConst([TBool], CBool(true))], [$2]) }
| CASE IDENT BO_arrow DO equations UNTIL next_list {
let (exprs, outs) = $7 in
State($2, $5, exprs, outs)}
;
transition_list:
@ -446,3 +447,8 @@ transition_list:
| transition transition_list { $1 :: $2 }
| /* empty */ {raise(MyParsingError("Empty automaton", current_location()))}
;
next_list:
| expr THEN IDENT { [$1], [$3] }
| next_list ELSE IF expr THEN IDENT { let (exprs, outs) = $1 in $4::exprs, $6::outs }
;

8
src/passes.ml
View File

@ -852,13 +852,18 @@ let automaton_translation debug automaton =
in
List.map aux eqlist
in
let rec next_construct exprs nexts = match exprs, nexts with
| [], [] -> EConst([TInt], CInt(1))
| e::exprs, n::nexts -> ETriOp([TInt], TOp_if, e, EConst([TInt], CInt(find_state n)), next_construct exprs nexts)
| _, _ -> failwith "Automata translation: next construct: should not happen"
in
let state_translation state =
match state with
| State( name, equations, expr, next ) ->
let b = create_branch_name name in
let eqs = translate_eqlist equations name in
let bool_expr = EComp([TBool], COp_eq, EVar([TInt], to_var automat_name TInt), EConst([TInt], CInt(find_state name))) in
let next_expr = EWhen([TInt], ETriOp([TInt], TOp_if, expr, EConst([TInt], CInt(find_state next)), EConst([TInt], CInt(1))), EVar([TBool], to_var (get_branch_bool name) TBool)) in
let next_expr = EWhen([TInt], next_construct expr next, EVar([TBool], to_var (get_branch_bool name) TBool)) in
(([TBool], [to_var b TBool]), bool_expr)::(([TInt], [to_var (create_next_var name) TInt]), next_expr)::eqs
in
let rec iter_states states =
@ -900,6 +905,7 @@ let automaton_translation debug automaton =
|RVar(_)::q -> TReal::build_type q
|[] -> []
in
let init, states = automaton in
init_state_translation states 1;
let transition_eq = (([TInt], [IVar(automat_name)]), EBinOp([TInt], BOp_arrow, EConst([TInt], CInt(1)), EMonOp([TInt], MOp_pre, merge_state states))) in

5
tests/automaton.node
View File

@ -15,7 +15,8 @@ node auto (i: int) returns (o : int);
var x, y:int;
let
automaton
| Incr -> do (o,x) = (0 fby o + 1, 2); done
| Decr -> do (o,x) = diagonal_int(0 fby o); done
| Incr -> do (o,x) = (0 fby o + 1, 2); until x > 0 then Decr else if x = o then Done
| Decr -> do (o,x) = diagonal_int(0 fby o); until x < o then Incr
| Done -> do o = pre o; done
tel