From 478edbed94011c041ca41f88df7403f6b4356c8a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9lio=20Brun?= <lelio.brun@isae-supaero.fr>
Date: Thu, 23 Sep 2021 16:40:08 +0200
Subject: [PATCH] proper handling of stateless nodes and automata
---
src/backends/C/c_backend_spec.ml | 43 ++++++++++++++++----------
src/checks/stateless.ml | 53 ++++++++++++++++++++++++--------
src/compiler_common.ml | 6 ++--
src/compiler_common.mli | 1 +
src/corelang.ml | 25 ++++++++-------
src/corelang.mli | 2 ++
src/lustre_types.ml | 20 ++++++++++++
src/lustre_types.mli | 2 ++
src/machine_code.ml | 31 ++++++++++++-------
src/machine_code_common.ml | 2 +-
src/optimize_machine.ml | 4 +--
src/printers.ml | 20 ------------
src/spec_common.ml | 5 +--
src/spec_common.mli | 1 +
src/spec_types.ml | 3 +-
src/spec_types.mli | 3 +-
16 files changed, 141 insertions(+), 80 deletions(-)
diff --git a/src/backends/C/c_backend_spec.ml b/src/backends/C/c_backend_spec.ml
index 6839bff3..d2acd9a8 100644
--- a/src/backends/C/c_backend_spec.ml
+++ b/src/backends/C/c_backend_spec.ml
@@ -325,9 +325,8 @@ let pp_memory_pack pp_mem pp_self fmt (mp, mem, self) =
fmt
(mp.mpname.node_id, mem, self)
-let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
+let pp_transition_aux ?i stateless pp_mem_in pp_mem_out pp_var fmt
(name, vars, mem_in, mem_out) =
- let stateless = fst (get_stateless_status m) in
fprintf
fmt
"%s_transition%a(@[<hov>%t%a%t@])"
@@ -341,10 +340,10 @@ let pp_transition_aux ?i m pp_mem_in pp_mem_out pp_var fmt
vars
(fun fmt -> if not stateless then fprintf fmt ",@ %a" pp_mem_out mem_out)
-let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
+let pp_transition stateless pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
pp_transition_aux
?i:t.tindex
- m
+ stateless
pp_mem_in
pp_mem_out
pp_var
@@ -352,7 +351,8 @@ let pp_transition m pp_mem_in pp_mem_out pp_var fmt (t, mem_in, mem_out) =
(t.tname.node_id, t.tvars, mem_in, mem_out)
let pp_transition_aux' ?i m =
- pp_transition_aux ?i m pp_print_string pp_print_string (fun fmt v ->
+ let stateless = fst (get_stateless_status m) in
+ pp_transition_aux ?i stateless pp_print_string pp_print_string (fun fmt v ->
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)
let pp_reset_cleared pp_mem_in pp_mem_out fmt (name, mem_in, mem_out) =
@@ -434,7 +434,7 @@ module PrintSpec = struct
fun test_output fmt e -> pp_expr ~test_output m mem_out fmt e
in
match p with
- | Transition (f, inst, i, vars, r, mems, insts) ->
+ | Transition (stateless, f, inst, i, vars, r, mems, insts) ->
let pp_mem_in, pp_mem_out =
match inst with
| None ->
@@ -449,7 +449,7 @@ module PrintSpec = struct
in
pp_transition_aux
?i
- m
+ stateless
pp_mem_in
pp_mem_out
(pp_expr test_output)
@@ -686,10 +686,11 @@ let pp_transition_def m fmt t =
let name = t.tname.node_id in
let mem_in = mk_mem_in m in
let mem_out = mk_mem_out m in
+ let stateless = fst (get_stateless_status m) in
pp_acsl
(pp_predicate
(pp_transition
- m
+ stateless
(pp_machine_decl' ~ghost:true)
(pp_machine_decl' ~ghost:true)
(pp_local m))
@@ -717,6 +718,7 @@ let pp_transition_footprint_lemma m fmt t =
let name = t.tname.node_id in
let mem_in = mk_mem_in m in
let mem_out = mk_mem_out m in
+ let stateless = fst (get_stateless_status m) in
let mems =
ISet.(
diff (of_list (List.map (fun v -> v.var_id) m.mmemory)) t.tmem_footprint)
@@ -740,6 +742,7 @@ let pp_transition_footprint_lemma m fmt t =
?mems
?insts
?i:t.tindex
+ stateless
name
(vdecls_to_vals t.tvars)
in
@@ -1057,8 +1060,8 @@ module SrcMod = struct
| e -> e
let rename_predicate n = function
- | Transition (f, inst, i, es, r, mf, mif) ->
- Transition (f, inst, i, List.map (rename_expression n) es, r, mf, mif)
+ | Transition (s, f, inst, i, es, r, mf, mif) ->
+ Transition (s, f, inst, i, List.map (rename_expression n) es, r, mf, mif)
| p -> p
let rec rename_formula n = function
@@ -1109,6 +1112,8 @@ module SrcMod = struct
let mem = mk_mem m in
let inputs = m.mstep.step_inputs in
let outputs = m.mstep.step_outputs in
+ let stateless = fst (get_stateless_status m) in
+ let stateless_c = fst (get_stateless_status m_c) in
let l = List.init (k - 1) (fun n -> n + 1) in
pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut
(fun fmt n ->
@@ -1121,13 +1126,13 @@ module SrcMod = struct
| 0 ->
pp_init pp_print_string fmt (name, rename 0 mem)
| n ->
- pp_transition_aux m pp_print_string pp_print_string pp_var_decl
+ pp_transition_aux stateless pp_print_string pp_print_string pp_var_decl
fmt
(name,
List.map (rename_var_decl n) (inputs @ outputs),
rename (n - 1) mem,
rename n mem)))
- (pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl))
+ (pp_transition_aux stateless_c pp_print_string pp_print_string pp_var_decl))
(pp_contract m)
in
pp_predicate
@@ -1168,6 +1173,8 @@ module SrcMod = struct
let mem = mk_mem m in
let inputs = m.mstep.step_inputs in
let outputs = m.mstep.step_outputs in
+ let stateless = fst (get_stateless_status m) in
+ let stateless_c = fst (get_stateless_status m_c) in
let l = List.init k (fun n -> n + 1) in
let pp =
pp_implies
@@ -1178,8 +1185,8 @@ module SrcMod = struct
let c_inputs = List.map (fun v -> false, rename_var_decl n v) m_c.mstep.step_inputs in
let c_outputs = List.map (fun v -> true, rename_var_decl n v) m_c.mstep.step_outputs in
pp_and
- (pp_transition_aux m pp_print_string pp_print_string pp_var_decl)
- (pp_transition_aux m_c pp_print_string pp_print_string pp)
+ (pp_transition_aux stateless pp_print_string pp_print_string pp_var_decl)
+ (pp_transition_aux stateless_c pp_print_string pp_print_string pp)
fmt
((name,
List.map (rename_var_decl n) (inputs @ outputs),
@@ -1253,6 +1260,7 @@ module SrcMod = struct
let mem_out = mk_mem_out m in
let inputs = m.mstep.step_inputs in
let outputs = m.mstep.step_outputs in
+ let stateless_c = fst (get_stateless_status m_c) in
let l = List.init k (fun n -> n + 1) in
pp_axiomatic
(fun fmt () -> fprintf fmt "%s_k_Induction" name)
@@ -1280,7 +1288,7 @@ module SrcMod = struct
(pp_comma_list pp_var_decl)
fmt
(n, mem_in, mem_out)))
- (pp_transition_aux m_c pp_print_string pp_print_string pp_var_decl))
+ (pp_transition_aux stateless_c pp_print_string pp_print_string pp_var_decl))
(pp_contract m)))))
fmt
((),
@@ -1326,6 +1334,7 @@ module SrcMod = struct
in
let inputs = m.mstep.step_inputs in
let outputs = m.mstep.step_outputs in
+ let stateless = fst (get_stateless_status m) in
let pp_if_outputs pp =
if outputs = [] then pp_print_nothing else pp
in
@@ -1358,7 +1367,7 @@ module SrcMod = struct
pp_spec_vars fmt ();
pp_acsl_cut
(fun fmt () ->
- if fst (get_stateless_status m) then
+ if stateless then
fprintf
fmt
"%a@,%a@,%a@,%a@,%a@,%a"
@@ -1388,7 +1397,7 @@ module SrcMod = struct
(pp_ensures (pp_memory_pack_aux pp_ptr pp_print_string))
(name, mem, self)
(pp_ensures
- (pp_transition_aux m (pp_old pp_ptr) pp_ptr (fun fmt v ->
+ (pp_transition_aux stateless (pp_old pp_ptr) pp_ptr (fun fmt v ->
(if is_output m v then pp_ptr_decl else pp_var_decl) fmt v)))
(name, inputs @ outputs, mem, mem)
pp_spec
diff --git a/src/checks/stateless.ml b/src/checks/stateless.ml
index 6f163714..80d67e03 100644
--- a/src/checks/stateless.ml
+++ b/src/checks/stateless.ml
@@ -62,6 +62,9 @@ let rec check_expr expr =
i);
check_expr e' && reset_opt && stateless_node
+and check_eexpr e =
+ check_expr e.eexpr_qfexpr
+
and compute_node nd =
(* returns true iff the node is stateless.*)
let eqs, aut = get_node_eqs nd in
@@ -69,21 +72,47 @@ and compute_node nd =
&& (* A node containinig an automaton will be stateful *)
List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
+and compute_contract nd =
+ let c = node_as_contract nd in
+ let eqs, aut = get_contract_eqs c in
+ aut = []
+ && (* A node containinig an automaton will be stateful *)
+ List.for_all (fun eq -> check_expr eq.eq_rhs) eqs
+ &&
+ List.for_all check_eexpr c.assume
+ &&
+ List.for_all check_eexpr c.guarantees
+
+and compute_node_or_contract nd =
+ match nd.node_spec, nd.node_iscontract with
+ | None, false
+ | Some (NodeSpec _), false
+ | Some (Contract _), false ->
+ compute_node nd
+ | Some (Contract _), true ->
+ compute_contract nd
+ | _ ->
+ assert false
+
and check_node td =
match td.top_decl_desc with
- | Node nd -> (
- match nd.node_stateless with
- | None ->
- let stateless = compute_node nd in
- nd.node_stateless <- Some stateless;
- if nd.node_dec_stateless && not stateless then
- raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id))
- else (
+ | Node nd ->
+ begin match nd.node_stateless with
+ | None ->
+ let stateless = compute_node_or_contract nd in
+ nd.node_stateless <- Some stateless;
+ if stateless
+ then (if not nd.node_dec_stateless
+ then Log.report ~level:2 (fun fmt ->
+ Format.fprintf fmt "%s: node -> function@;" nd.node_id))
+ else if nd.node_dec_stateless
+ then raise (Error (td.top_decl_loc, Stateful_kwd nd.node_id));
nd.node_dec_stateless <- stateless;
- stateless)
- | Some stl ->
- stl)
- | ImportedNode nd ->
+ stateless
+ | Some stl ->
+ stl
+ end
+| ImportedNode nd ->
if nd.nodei_prototype = Some "C" && not nd.nodei_stateless then
raise (Error (td.top_decl_loc, Stateful_ext_C nd.nodei_id));
nd.nodei_stateless
diff --git a/src/compiler_common.ml b/src/compiler_common.ml
index 2c087aef..91d5b00f 100644
--- a/src/compiler_common.ml
+++ b/src/compiler_common.ml
@@ -72,8 +72,9 @@ let expand_automata decls =
let check_stateless_decls decls =
Log.report ~level:1 (fun fmt ->
- fprintf fmt "@ .. checking stateless/stateful status@ ");
- try Stateless.check_prog decls
+ fprintf fmt "@ @[<v 2>.. checking stateless/stateful status@ ");
+ try (Stateless.check_prog decls;
+ Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ "))
with Stateless.Error (loc, err) as exc ->
eprintf
"Stateless status error: %a%a@."
@@ -426,3 +427,4 @@ let update_vdecl_parents_prog prog =
| _ ->
())
prog
+
diff --git a/src/compiler_common.mli b/src/compiler_common.mli
index 5b686c31..9aa99565 100644
--- a/src/compiler_common.mli
+++ b/src/compiler_common.mli
@@ -28,3 +28,4 @@ val clock_decls : Clocks.t Env.t -> program_t -> Clocks.t Env.t
val create_dest_dir : unit -> unit
val track_exception : unit -> unit
+
diff --git a/src/corelang.ml b/src/corelang.ml
index 32a0f891..4b78ff1f 100644
--- a/src/corelang.ml
+++ b/src/corelang.ml
@@ -765,18 +765,18 @@ let get_node_var id node =
node.node_id; *)
raise Not_found
+let get_eqs stmts =
+ List.fold_right
+ (fun stmt (res_eq, res_aut) ->
+ match stmt with
+ | Eq eq ->
+ eq :: res_eq, res_aut
+ | Aut aut ->
+ res_eq, aut :: res_aut)
+ stmts
+ ([], [])
+
let get_node_eqs =
- let get_eqs stmts =
- List.fold_right
- (fun stmt (res_eq, res_aut) ->
- match stmt with
- | Eq eq ->
- eq :: res_eq, res_aut
- | Aut aut ->
- res_eq, aut :: res_aut)
- stmts
- ([], [])
- in
let table_eqs = Hashtbl.create 23 in
fun nd ->
try
@@ -787,6 +787,9 @@ let get_node_eqs =
Hashtbl.replace table_eqs nd.node_id (nd.node_stmts, res);
res
+let get_contract_eqs c =
+ get_eqs c.stmts
+
let get_node_eq id node =
let eqs, _ = get_node_eqs node in
try List.find (fun eq -> List.mem id eq.eq_lhs) eqs
diff --git a/src/corelang.mli b/src/corelang.mli
index aa5af920..3500c8e1 100644
--- a/src/corelang.mli
+++ b/src/corelang.mli
@@ -156,6 +156,8 @@ val get_node_var : ident -> node_desc -> var_decl
val get_node_eqs : node_desc -> eq list * automata_desc list
+val get_contract_eqs : contract_desc -> eq list * automata_desc list
+
val get_node_eq : ident -> node_desc -> eq
val get_node_interface : node_desc -> imported_node_desc
diff --git a/src/lustre_types.ml b/src/lustre_types.ml
index 4ca126ce..a9aad140 100644
--- a/src/lustre_types.ml
+++ b/src/lustre_types.ml
@@ -246,6 +246,26 @@ let tag_true = "true"
let tag_false = "false"
+(* Project the contract node as a pure contract: local memories are pushed back
+ in the contract definition. Should mainly be used to print it *)
+let node_as_contract nd =
+ match nd.node_spec with
+ | None | Some (NodeSpec _) ->
+ raise (Invalid_argument "Not a contract")
+ | Some (Contract c) ->
+ (* While a processed contract shall have no locals, sttms nor consts, an
+ unprocessed one could. So we conservatively merge elements, to enable
+ printing unprocessed contracts *)
+ let consts, locals =
+ List.partition (fun v -> v.var_dec_const) nd.node_locals
+ in
+ {
+ c with
+ consts = consts @ c.consts;
+ locals = locals @ c.locals;
+ stmts = nd.node_stmts @ c.stmts;
+ }
+
(* Local Variables: *)
(* compile-command:"make -C .." *)
(* End: *)
diff --git a/src/lustre_types.mli b/src/lustre_types.mli
index aa030847..7cfdbfa3 100644
--- a/src/lustre_types.mli
+++ b/src/lustre_types.mli
@@ -233,3 +233,5 @@ type spec_types =
val tag_true : label
val tag_false : label
+
+val node_as_contract: node_desc -> contract_desc
diff --git a/src/machine_code.ml b/src/machine_code.ml
index 0d757dd3..7e9f43ba 100644
--- a/src/machine_code.ml
+++ b/src/machine_code.ml
@@ -239,6 +239,7 @@ let reset_instance env i r c =
None, []
let translate_eq env ctx nd inputs locals outputs i eq =
+ let stateless = fst (get_stateless_status_node nd) in
let id = nd.node_id in
let translate_expr = translate_expr env in
let translate_act = translate_act env in
@@ -257,6 +258,7 @@ let translate_eq env ctx nd inputs locals outputs i eq =
[
mk_transition
~i:(i - 1)
+ stateless
id
(vdecls_to_vals (inputs @ locals_pi @ outputs_pi));
a;
@@ -276,6 +278,7 @@ let translate_eq env ctx nd inputs locals outputs i eq =
@ [
mk_transition
~i
+ stateless
id
(vdecls_to_vals (inputs @ locals_i @ outputs_i));
];
@@ -306,7 +309,7 @@ let translate_eq env ctx nd inputs locals outputs i eq =
ctl
(MStep ([ var_x ], inst, [ c1; c2 ]))
(mk_memory_pack ~inst (node_name td))
- (mk_transition ~inst (node_name td) [ vdecl_to_val var_x ])
+ (mk_transition ~inst false (node_name td) [ vdecl_to_val var_x ])
{ ctx with j = IMap.add inst (td, []) ctx.j }
in
{ ctx with si = mkinstr (MSetReset inst) :: ctx.si }
@@ -339,7 +342,7 @@ let translate_eq env ctx nd inputs locals outputs i eq =
let vl = List.map translate_expr el in
let node_f = node_from_name f in
let call_f = node_f, NodeDep.filter_static_inputs (node_inputs node_f) el in
- let inst = new_instance node_f eq.eq_rhs.expr_tag in
+ let i = new_instance node_f eq.eq_rhs.expr_tag in
let env_cks =
List.fold_right
(fun arg cks -> arg.expr_clock :: cks)
@@ -349,17 +352,20 @@ let translate_eq env ctx nd inputs locals outputs i eq =
let call_ck =
Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks)
in
- let r, reset_inst = reset_instance inst r call_ck in
+ let r, reset_inst = reset_instance i r call_ck in
+ let stateless = Stateless.check_node node_f in
+ let inst = if stateless then None else Some i in
+ let mp = if stateless then True else mk_memory_pack ?inst (node_name node_f) in
let ctx =
ctl
~ck:call_ck
- (MStep (var_p, inst, vl))
- (mk_memory_pack ~inst (node_name node_f))
- (mk_transition ?r ~inst (node_name node_f) (vl @ vdecls_to_vals var_p))
+ (MStep (var_p, i, vl))
+ mp
+ (mk_transition ?r ?inst stateless (node_name node_f) (vl @ vdecls_to_vals var_p))
{
ctx with
- j = IMap.add inst call_f ctx.j;
- s = (if Stateless.check_node node_f then [] else reset_inst) @ ctx.s;
+ j = IMap.add i call_f ctx.j;
+ s = (if stateless then [] else reset_inst) @ ctx.s;
}
in
(*Clocks.new_var true in Clock_calculus.unify_imported_clock (Some call_ck)
@@ -369,8 +375,8 @@ let translate_eq env ctx nd inputs locals outputs i eq =
{
ctx with
si =
- (if Stateless.check_node node_f then ctx.si
- else mkinstr (MSetReset inst) :: ctx.si);
+ (if stateless then ctx.si
+ else mkinstr (MSetReset i) :: ctx.si);
}
| [ x ], _ ->
begin try
@@ -495,8 +501,10 @@ let transition_0 nd =
}
let transition_toplevel nd i =
+ let stateless = fst (get_stateless_status_node nd) in
let tr =
mk_transition
+ stateless
nd.node_id
~i
(vdecls_to_vals (nd.node_inputs @ nd.node_outputs))
@@ -541,6 +549,7 @@ let translate_spec env = function
NodeSpec s
let translate_decl nd sch =
+ let stateless = fst (get_stateless_status_node nd) in
(* Format.eprintf "Translating node %s@." nd.node_id; *)
(* Extracting eqs, variables .. *)
let eqs, auts = get_node_eqs nd in
@@ -621,7 +630,7 @@ let translate_decl nd sch =
~instr_spec:
((if fst (get_stateless_status_node nd) then []
else [ mk_memory_pack ~i:0 nd.node_id ])
- @ [ mk_transition ~i:0 nd.node_id (vdecls_to_vals nd.node_inputs) ])
+ @ [ mk_transition ~i:0 stateless nd.node_id (vdecls_to_vals nd.node_inputs) ])
MClearReset
in
let mnode_spec = Utils.option_map (translate_spec env) nd.node_spec in
diff --git a/src/machine_code_common.ml b/src/machine_code_common.ml
index 0ea7a177..922f3b79 100644
--- a/src/machine_code_common.ml
+++ b/src/machine_code_common.ml
@@ -59,7 +59,7 @@ module PrintSpec = struct
fun fmt e -> pp_expr m fmt e
in
match p with
- | Transition (f, inst, i, vars, _r, _mems, _insts) ->
+ | Transition (_, f, inst, i, vars, _r, _mems, _insts) ->
fprintf
fmt
"Transition_%a<%a>%a%a"
diff --git a/src/optimize_machine.ml b/src/optimize_machine.ml
index f9d32b40..cc42e739 100644
--- a/src/optimize_machine.ml
+++ b/src/optimize_machine.ml
@@ -644,9 +644,9 @@ let expr_spec_replace :
e
let predicate_spec_replace fvar = function
- | Transition (f, inst, i, vars, r, mems, insts) ->
+ | Transition (s, f, inst, i, vars, r, mems, insts) ->
Transition
- (f, inst, i, List.map (expr_spec_replace fvar) vars, r, mems, insts)
+ (s, f, inst, i, List.map (expr_spec_replace fvar) vars, r, mems, insts)
| p ->
p
diff --git a/src/printers.ml b/src/printers.ml
index 15bae926..5d3a818c 100644
--- a/src/printers.ml
+++ b/src/printers.ml
@@ -538,26 +538,6 @@ let pp_spec fmt spec =
import.outputs))
spec.imports
-(* Project the contract node as a pure contract: local memories are pushed back
- in the contract definition. Should mainly be used to print it *)
-let node_as_contract nd =
- match nd.node_spec with
- | None | Some (NodeSpec _) ->
- raise (Invalid_argument "Not a contract")
- | Some (Contract c) ->
- (* While a processed contract shall have no locals, sttms nor consts, an
- unprocessed one could. So we conservatively merge elements, to enable
- printing unprocessed contracts *)
- let consts, locals =
- List.partition (fun v -> v.var_dec_const) nd.node_locals
- in
- {
- c with
- consts = consts @ c.consts;
- locals = locals @ c.locals;
- stmts = nd.node_stmts @ c.stmts;
- }
-
(* Printing top contract as comments in regular output and as contract in kind2 *)
let pp_contract fmt nd =
let c = node_as_contract nd in
diff --git a/src/spec_common.ml b/src/spec_common.ml
index 85e4edbb..bdae2bcf 100644
--- a/src/spec_common.ml
+++ b/src/spec_common.ml
@@ -79,12 +79,13 @@ let vals vs = List.map (fun v -> Val v) vs
let mk_pred_call pred = Predicate pred
-let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst id vars
+let mk_transition ?(mems = ISet.empty) ?(insts = IMap.empty) ?r ?i ?inst stateless id vars
=
let tr =
mk_pred_call
(Transition
- ( id,
+ ( stateless,
+ id,
inst,
i,
vals vars,
diff --git a/src/spec_common.mli b/src/spec_common.mli
index df43a864..d2ac2230 100644
--- a/src/spec_common.mli
+++ b/src/spec_common.mli
@@ -16,6 +16,7 @@ val mk_transition :
?r:'a ->
?i:int ->
?inst:ident ->
+ bool ->
ident ->
'a list ->
'a formula_t
diff --git a/src/spec_types.ml b/src/spec_types.ml
index 8eb61540..7d2324a3 100644
--- a/src/spec_types.ml
+++ b/src/spec_types.ml
@@ -24,7 +24,8 @@ let type_of_l_value : type a. (a, left_v) expression_t -> Types.t = function
type 'a predicate_t =
| Transition :
- ident (* node name *)
+ bool (* stateless *)
+ * ident (* node name *)
* ident option
(* instance *)
* int option
diff --git a/src/spec_types.mli b/src/spec_types.mli
index 5edb4568..f7ab12cb 100644
--- a/src/spec_types.mli
+++ b/src/spec_types.mli
@@ -17,7 +17,8 @@ val type_of_l_value : ('a, left_v) expression_t -> Types.t
type 'a predicate_t =
| Transition :
- ident (* node name *)
+ bool (* stateless *)
+ * ident (* node name *)
* ident option
(* instance *)
* int option
--
GitLab