From 7fcc03cc7282fba480a3cfc998e85f62182da4ad Mon Sep 17 00:00:00 2001
From: Valentin Perrelle <valentin.perrelle@cea.fr>
Date: Fri, 31 Jul 2020 19:59:49 +0200
Subject: [PATCH] [Aorai] move metavariable assignements from conditions to
transitions
- Use the same field "actions" for parsed and typed transitions
- Rename confusing types in Promelaast
- Reorganized Promelaoutput to mirror the naming convention
---
src/plugins/aorai/aorai_dataflow.ml | 6 +-
src/plugins/aorai/aorai_graph.ml | 4 +-
src/plugins/aorai/aorai_graph.mli | 3 +-
src/plugins/aorai/aorai_metavariables.ml | 14 +-
src/plugins/aorai/aorai_register.ml | 4 +-
src/plugins/aorai/aorai_utils.ml | 45 +-
src/plugins/aorai/aorai_utils.mli | 4 +-
src/plugins/aorai/aorai_visitors.ml | 4 +-
src/plugins/aorai/data_for_aorai.ml | 238 +++++-----
src/plugins/aorai/data_for_aorai.mli | 13 +-
src/plugins/aorai/logic_simplification.ml | 15 +-
src/plugins/aorai/logic_simplification.mli | 4 +-
src/plugins/aorai/promelaast.mli | 44 +-
src/plugins/aorai/promelaoutput.ml | 414 +++++++++---------
src/plugins/aorai/promelaoutput.mli | 56 +--
src/plugins/aorai/promelaparser.mly | 8 +-
src/plugins/aorai/promelaparser_withexps.mly | 8 +-
.../aorai/tests/ya/metavariables-right.ya | 4 +-
.../aorai/tests/ya/metavariables-wrong.ya | 2 +-
src/plugins/aorai/tests/ya/stack.ya | 8 +-
src/plugins/aorai/yaparser.mly | 31 +-
21 files changed, 473 insertions(+), 456 deletions(-)
diff --git a/src/plugins/aorai/aorai_dataflow.ml b/src/plugins/aorai/aorai_dataflow.ml
index f6315b5ce50..0662bf5764d 100644
--- a/src/plugins/aorai/aorai_dataflow.ml
+++ b/src/plugins/aorai/aorai_dataflow.ml
@@ -276,8 +276,7 @@ let make_start_transition ?(is_main=false) kf init_states =
let my_trans = Path_analysis.get_transitions_of_state state auto in
let treat_one_trans acc trans =
if is_crossable trans kf then begin
- let (_,action) = trans.cross in
- let bindings = actions_to_range action in
+ let bindings = actions_to_range trans.actions in
let fst_set =
Data_for_aorai.Aorai_state.Set.singleton trans.stop
in
@@ -309,8 +308,7 @@ let make_return_transition kf state =
let last = Data_for_aorai.Aorai_state.Set.singleton state in
let treat_one_trans acc trans =
if Aorai_utils.isCrossable trans kf Promelaast.Return then begin
- let (_,action) = trans.cross in
- let my_bindings = actions_to_range action in
+ let my_bindings = actions_to_range trans.actions in
let new_bindings = compose_actions bindings (last, last, my_bindings) in
add_or_merge trans.stop new_bindings acc
end else acc
diff --git a/src/plugins/aorai/aorai_graph.ml b/src/plugins/aorai/aorai_graph.ml
index a72aca27e95..77f78d8950a 100644
--- a/src/plugins/aorai/aorai_graph.ml
+++ b/src/plugins/aorai/aorai_graph.ml
@@ -26,7 +26,7 @@
open Promelaast
type state = Promelaast.state
-type transition = (typed_condition * action) trans
+type transition = Promelaast.typed_trans
module Vertex =
struct
@@ -46,7 +46,7 @@ struct
let compare x y = Pervasives.compare x.numt y.numt
let default = {
numt = -1; start = Vertex.default; stop = Vertex.default;
- cross = TTrue,[]
+ cross = TTrue; actions = []
}
end
diff --git a/src/plugins/aorai/aorai_graph.mli b/src/plugins/aorai/aorai_graph.mli
index 4823c41789d..8735c3cc1e7 100644
--- a/src/plugins/aorai/aorai_graph.mli
+++ b/src/plugins/aorai/aorai_graph.mli
@@ -24,8 +24,7 @@
(**************************************************************************)
type state = Promelaast.state
-type transition =
- (Promelaast.typed_condition * Promelaast.action) Promelaast.trans
+type transition = Promelaast.typed_trans
type edge = state * transition * state
include Graph.Sig.I
diff --git a/src/plugins/aorai/aorai_metavariables.ml b/src/plugins/aorai/aorai_metavariables.ml
index 9ce8aac82a0..6c77e04c43a 100644
--- a/src/plugins/aorai/aorai_metavariables.ml
+++ b/src/plugins/aorai/aorai_metavariables.ml
@@ -90,10 +90,9 @@ struct
Format.pp_print_string fmt st.Promelaast.name
let pretty_trans fmt tr =
- let cond,act = tr.cross in
- Promelaoutput.print_condition fmt cond;
- if act <> [] then
- Format.fprintf fmt "{@[%a@]}" Promelaoutput.print_action act
+ Promelaoutput.Typed.print_condition fmt tr.cross;
+ if tr.actions <> [] then
+ Format.fprintf fmt "{@[%a@]}" Promelaoutput.Typed.print_actionl tr.actions
let pretty_set fmt set =
let l = Set.elements set in
@@ -115,18 +114,17 @@ struct
let analyze ((src,tr,dst) as edge) = function
| Bottom -> Bottom
| InitializedSet initialized ->
- let cond,act = tr.cross in
(* Check that the condition uses only initialized variables *)
- let used = used_metavariables cond in
+ let used = used_metavariables tr.cross in
let diff = Set.diff used initialized in
if not (Set.is_empty diff) then
alarm edge diff;
(* Add variables initialized by the condition *)
- let add_initialized set = function
+ let add set = function
| Copy_value ((TVar({lv_origin = Some vi}),_),_) -> Set.add vi set
| _ -> set
in
- let initialized' = List.fold_left add_initialized initialized act in
+ let initialized' = List.fold_left add initialized tr.actions in
Aorai_option.debug ~dkey "%a {%a} -> %a {%a}"
pretty_state src pretty_set initialized
pretty_state dst pretty_set initialized';
diff --git a/src/plugins/aorai/aorai_register.ml b/src/plugins/aorai/aorai_register.ml
index 1ad1b145e78..14c35b7f0e6 100644
--- a/src/plugins/aorai/aorai_register.ml
+++ b/src/plugins/aorai/aorai_register.ml
@@ -48,7 +48,7 @@ let convert_ltl_exprs t =
POr(c1,c2) -> POr (convert_cond c1, convert_cond c2)
| PAnd(c1,c2) -> PAnd(convert_cond c1, convert_cond c2)
| PNot c -> PNot (convert_cond c)
- | PCall _ | PReturn _ | PTrue | PFalse | PAssign _ -> cond
+ | PCall _ | PReturn _ | PTrue | PFalse -> cond
| PRel(Neq,PVar x,PCst _) ->
(try
let (rel,t1,t2) = Hashtbl.find ltl_to_promela x in PRel(rel,t1,t2)
@@ -259,7 +259,7 @@ let output () =
(* Dot file *)
if (Aorai_option.Dot.get()) then
begin
- Promelaoutput.output_dot_automata (Data_for_aorai.getAutomata ())
+ Promelaoutput.Typed.output_dot_automata (Data_for_aorai.getAutomata ())
(!dot_file:>string);
printverb "Generating dot file : done\n"
end;
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 5daa862d825..c192b4c348e 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -66,8 +66,7 @@ let isCrossable tr func st =
| TFalse -> False
| TRel _ -> Undefined
in
- let cond,_ = tr.cross in
- let res = isCross cond <> False in
+ let res = isCross tr.cross <> False in
Aorai_option.debug ~level:2 "Function %a %s-state, \
transition %s -> %s is%s possible" Kernel_function.pretty func
(if st=Call then "pre" else "post")
@@ -307,8 +306,7 @@ let isCrossableAtInit tr func =
| TRel(rel,t1,t2) -> eval_rel_at_init rel t1 t2
in
- let (cond,_) = tr.cross in
- match isCross cond with
+ match isCross tr.cross with
| Bool3.True | Bool3.Undefined -> true
| Bool3.False -> false
@@ -557,7 +555,7 @@ let mk_behavior_call generated_kf kf bhv =
(* Translate the cross condition of an automaton edge to an expression.
Used in mk_stmt. This might generate calls to auxiliary functions, to
take into account a guard that uses a function behavior. *)
-let crosscond_to_exp generated_kf curr_f curr_status loc (cond,_) res =
+let crosscond_to_exp generated_kf curr_f curr_status loc cond res =
let check_current_event f status =
Kernel_function.equal curr_f f && curr_status = status
in
@@ -1059,10 +1057,10 @@ let mk_deterministic_lemma () =
let subst = Cil_datatype.Logic_var.Hashtbl.create 5 in
let subst_res = Kernel_function.Hashtbl.create 5 in
let guard1 =
- pred_of_condition subst subst_res label (fst trans1.cross)
+ pred_of_condition subst subst_res label trans1.cross
in
let guard2 =
- pred_of_condition subst subst_res label (fst trans2.cross)
+ pred_of_condition subst subst_res label trans2.cross
in
let pred = Logic_const.pnot (Logic_const.pand (guard1, guard2)) in
let quants =
@@ -1288,7 +1286,7 @@ let action_assigns trans =
add_if_needed caux (Logic_const.tvar aux) empty
| _ -> empty
in
- let _,res = List.fold_left treat_one_action empty_pebble (snd trans.cross) in
+ let _,res = List.fold_left treat_one_action empty_pebble trans.actions in
Writes res
let get_reachable_trans state st auto current_state =
@@ -1354,7 +1352,7 @@ let force_transition loc f st current_state =
*)
let add_one_trans (has_crossable_trans, crossable_non_reject) trans =
let has_crossable_trans =
- Logic_simplification.tor has_crossable_trans (fst trans.cross)
+ Logic_simplification.tor has_crossable_trans trans.cross
in
let crossable_non_reject =
crossable_non_reject ||
@@ -1428,7 +1426,7 @@ let partition_action trans =
*)
in
let treat_one_trans acc tr =
- List.fold_left (treat_one_action tr.start) acc (snd tr.cross)
+ List.fold_left (treat_one_action tr.start) acc tr.actions
in
List.fold_left treat_one_trans Cil_datatype.Term_lval.Map.empty trans
@@ -1530,7 +1528,8 @@ let add_behavior_pebble_actions ~loc f st behaviors state trans =
let set = Data_for_aorai.pebble_set_at set Logic_const.here_label in
let treat_action guard res action =
match action with
- | Copy_value _ | Counter_incr _ | Counter_init _ -> res
+ | Copy_value _ | Counter_incr _ | Counter_init _ ->
+ res
| Pebble_init (_,_,v) ->
let a = Cil_const.make_logic_var_quant aux.lv_name aux.lv_type in
let guard = rename_pred aux a guard in
@@ -1558,9 +1557,9 @@ let add_behavior_pebble_actions ~loc f st behaviors state trans =
:: res
in
let treat_one_trans acc tr =
- let guard = crosscond_to_pred (fst tr.cross) f st in
+ let guard = crosscond_to_pred tr.cross f st in
let guard = Logic_const.pold guard in
- List.fold_left (treat_action guard) acc (snd tr.cross)
+ List.fold_left (treat_action guard) acc tr.actions
in
let res = List.fold_left treat_one_trans [] trans in
let res = Logic_const.term (Tunion res) set.term_type in
@@ -1639,8 +1638,7 @@ let mk_unchanged_aux_vars trans =
| Pebble_init _ | Pebble_move _ -> acc
in
let add_one_trans acc tr =
- let (_,actions) = tr.cross in
- List.fold_left add_one_action acc actions
+ List.fold_left add_one_action acc tr.actions
in
let my_aux_vars = List.fold_left add_one_trans my_aux_vars trans in
let treat_lval lv acc =
@@ -1672,15 +1670,14 @@ let mk_behavior ~loc auto kf e status state =
List.fold_left
(fun (in_guard, out_guard, all_assigns, action_bhvs) trans ->
Aorai_option.debug "examining transition %d" trans.numt;
- let (cond,actions) = trans.cross in
Aorai_option.debug "transition %d is active" trans.numt;
- let guard = crosscond_to_pred cond kf e in
+ let guard = crosscond_to_pred trans.cross kf e in
let my_in_guard,my_out_guard =
match state.multi_state with
| None -> guard, Logic_const.pnot ~loc guard
| Some (_,aux) ->
let set =
- find_pebble_origin Logic_const.here_label actions
+ find_pebble_origin Logic_const.here_label trans.actions
in
pebble_guard ~loc set aux guard,
pebble_guard_neg ~loc set aux guard
@@ -1689,7 +1686,7 @@ let mk_behavior ~loc auto kf e status state =
Logic_const.pand ~loc (out_guard, my_out_guard)
in
let in_guard, all_assigns, action_bhvs =
- match actions with
+ match trans.actions with
| [] ->
(Logic_const.por ~loc (in_guard,my_in_guard),
all_assigns,
@@ -1721,7 +1718,7 @@ let mk_behavior ~loc auto kf e status state =
| Some (_,aux) ->
let set =
find_pebble_origin
- Logic_const.pre_label actions
+ Logic_const.pre_label trans.actions
in
acc @
List.map
@@ -1732,7 +1729,7 @@ let mk_behavior ~loc auto kf e status state =
posts
in
let post_cond =
- List.fold_left treat_one_action [post_cond] actions
+ List.fold_left treat_one_action [post_cond] trans.actions
in
let assigns = action_assigns trans in
let all_assigns = concat_assigns assigns all_assigns in
@@ -1879,7 +1876,7 @@ let auto_func_behaviors loc f st state =
global_behavior :: (List.rev behaviors)
-let act_convert loc (_,act) res =
+let act_convert loc act res =
let treat_one_act =
function
| Counter_init t_lval ->
@@ -1929,7 +1926,7 @@ let mk_stmt generated_kf loc (states, tr) f fst status ((st,_) as state) res =
Cil_datatype.Varinfo.Set.union tr_funcs new_funcs,
Cil.mkBinOp loc LAnd (is_state_exp trans.start loc) exp
::exp_from_trans,
- act_convert loc trans.cross res :: stmt_from_action))
+ act_convert loc trans.actions res :: stmt_from_action))
useful_trans
([],[],Cil_datatype.Varinfo.Set.empty, [], [])
in
@@ -2079,7 +2076,7 @@ let auto_func_block generated_kf loc f st status res =
let get_preds_wrt_params_reachable_states state f status =
let auto = Data_for_aorai.getGraph () in
- let treat_one_trans acc tr = Logic_simplification.tor acc (fst tr.cross) in
+ let treat_one_trans acc tr = Logic_simplification.tor acc tr.cross in
let find_trans state prev tr =
Path_analysis.get_edges prev state auto @ tr
in
diff --git a/src/plugins/aorai/aorai_utils.mli b/src/plugins/aorai/aorai_utils.mli
index 47d4bb47275..0bc659364f4 100644
--- a/src/plugins/aorai/aorai_utils.mli
+++ b/src/plugins/aorai/aorai_utils.mli
@@ -32,12 +32,12 @@ open Promelaast
*)
val isCrossable:
- (typed_condition * action) trans -> kernel_function -> funcStatus -> bool
+ typed_trans -> kernel_function -> funcStatus -> bool
(** Given a transition and the main entry point it returns if
the cross condition can be satisfied at the beginning of the program. *)
val isCrossableAtInit:
- (typed_condition * action) trans -> kernel_function -> bool
+ typed_trans -> kernel_function -> bool
(** This function rewrites a cross condition into an ACSL expression.
Moreover, by giving current operation name and its status (call or
diff --git a/src/plugins/aorai/aorai_visitors.ml b/src/plugins/aorai/aorai_visitors.ml
index ad68e06ec7a..486c67733ed 100644
--- a/src/plugins/aorai/aorai_visitors.ml
+++ b/src/plugins/aorai/aorai_visitors.ml
@@ -382,7 +382,7 @@ let possible_start kf (start,int) =
let trans = Path_analysis.get_edges start int auto in
let treat_one_trans cond tr =
Logic_const.por
- (cond, Aorai_utils.crosscond_to_pred (fst tr.cross) kf Promelaast.Call)
+ (cond, Aorai_utils.crosscond_to_pred tr.cross kf Promelaast.Call)
in
let cond = List.fold_left treat_one_trans Logic_const.pfalse trans in
Logic_const.pand (Aorai_utils.is_state_pred start, cond)
@@ -409,7 +409,7 @@ let neg_trans kf trans =
List.fold_left
(fun cond tr ->
Logic_simplification.tand
- cond (Logic_simplification.tnot (fst tr.cross)))
+ cond (Logic_simplification.tnot tr.cross))
cond trans)
TTrue same_start
in
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 56f2d69b042..54f5d8c0e25 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -57,19 +57,18 @@ module Aorai_typed_trans =
Datatype.Make_with_collections(
struct
let name = "Aorai_typed_trans"
- type t =
- (Promelaast.typed_condition * Promelaast.action) Promelaast.trans
+ type t = Promelaast.typed_trans
let structural_descr = Structural_descr.t_abstract
let reprs = [ { numt = -1; start = List.hd (Aorai_state.reprs);
stop = List.hd (Aorai_state.reprs);
- cross = (TTrue,[]); } ]
+ cross = TTrue; actions=[]; } ]
let equal x y = Datatype.Int.equal x.numt y.numt
let hash x = x.numt
let rehash = Datatype.identity
let compare x y = Datatype.Int.compare x.numt y.numt
let copy = Datatype.identity
let internal_pretty_code = Datatype.undefined
- let pretty = Promelaoutput.print_transition
+ let pretty = Promelaoutput.Typed.print_transition
let varname _ = assert false
let mem_project = Datatype.never_any_project
end)
@@ -354,8 +353,8 @@ let new_state name =
let new_intermediate_state () = new_state "aorai_intermediate_state"
-let new_trans start stop cond =
- { start = start; stop = stop; cross = cond; numt = TransIndex.next () }
+let new_trans start stop cross actions =
+ { start; stop; cross; actions; numt = TransIndex.next () }
let check_states s =
let {states;trans} = getAutomata() in
@@ -410,25 +409,23 @@ let is_single elt =
the entire automaton is processed by adding direct transitions from the
starting state to the children of the end state.
*)
-type eps_trans =
- Normal of typed_condition * action
- | Epsilon of typed_condition * action
-
-let print_epsilon_trans fmt = function
- | Normal (c,a) ->
- Format.fprintf fmt "%a%a"
- Promelaoutput.print_condition c
- Promelaoutput.print_action a
- | Epsilon (c,a) ->
- Format.fprintf fmt "epsilon-trans:@\n%a%a"
- Promelaoutput.print_condition c
- Promelaoutput.print_action a
+type 'a eps = Normal of 'a | Epsilon of 'a
+
+let print_eps f fmt = function
+ | Normal x -> f fmt x
+ | Epsilon x -> Format.fprintf fmt "epsilon-trans:@\n%a" f x
+
+let print_eps_trans fmt tr =
+ Format.fprintf fmt "%s -> %s:@[%a%a@]"
+ tr.start.name tr.stop.name
+ (print_eps Promelaoutput.Typed.print_condition) tr.cross
+ Promelaoutput.Typed.print_actionl tr.actions
type current_event =
| ECall of
kernel_function
* Cil_types.logic_var Cil_datatype.Varinfo.Hashtbl.t
- * eps_trans Promelaast.trans
+ * (typed_condition eps,typed_action) Promelaast.trans
| EReturn of kernel_function
| ECOR of kernel_function
| ENone (* None found yet *)
@@ -553,11 +550,11 @@ let memo_aux_variable tr counter used_prms vi =
let my_lvar = Cil.cvar_to_lvar my_var in
Cil_datatype.Varinfo.Hashtbl.add used_prms vi my_lvar;
(match tr.cross with
- | Normal (cond,action) ->
+ | Normal _ ->
let st = Extlib.opt_map (fun _ -> tr.stop) counter in
let loc = get_bindings st my_lvar in
let copy = Copy_value (loc,Logic_const.tvar (Cil.cvar_to_lvar vi)) in
- tr.cross <- Normal(cond,copy::action)
+ tr.actions <- copy :: tr.actions
| Epsilon _ ->
Aorai_option.fatal "Epsilon transition used as Call event"
);
@@ -896,36 +893,27 @@ let type_cond needs_pebble metaenv env tr cond =
let current = if needs_pebble then Some tr.stop else None in
let rec aux pos env =
function
- | PAssign (s, e) ->
- if not pos then
- Aorai_option.abort
- "Metavariable assignment cannot be done under a negation";
- let vi = find_metavar s metaenv in
- let env, e, c = type_expr metaenv env ~tr ?current e in
- let assign = Copy_value ((TVar (Cil.cvar_to_lvar vi), TNoOffset), e) in
- (* TODO: check type assignability *)
- env, c, [assign]
| PRel(rel,e1,e2) ->
let env, e1, c1 = type_expr metaenv env ~tr ?current e1 in
let env, e2, c2 = type_expr metaenv env ~tr ?current e2 in
let call_cond = if pos then tand c1 c2 else tor (tnot c1) (tnot c2) in
let rel = TRel(Logic_typing.type_rel rel,e1,e2) in
let cond = if pos then tand call_cond rel else tor call_cond rel in
- env, cond, []
- | PTrue -> env, TTrue, []
- | PFalse -> env, TFalse, []
+ env, cond
+ | PTrue -> env, TTrue
+ | PFalse -> env, TFalse
| POr(c1,c2) ->
- let env1, c1, a1 = aux pos env c1 in
- let env2, c2, a2 = aux pos env c2 in
+ let env1, c1 = aux pos env c1 in
+ let env2, c2 = aux pos env c2 in
let env, c = merge_current_event env1 env2 c1 c2 in
- env, c, a1 @ a2
+ env, c
| PAnd(c1,c2) ->
- let env, c1, a1 = aux pos env c1 in
- let env, c2, a2 = aux pos env c2 in
- env, TAnd (c1,c2), a1 @ a2
+ let env, c1 = aux pos env c1 in
+ let env, c2 = aux pos env c2 in
+ env, TAnd (c1,c2)
| PNot c ->
- let env, c, a = aux (not pos) env c in
- env, TNot c, a
+ let env, c = aux (not pos) env c in
+ env, TNot c
| PCall (s,b) ->
let kf =
try Globals.Functions.find_by_name s
@@ -946,9 +934,9 @@ let type_cond needs_pebble metaenv env tr cond =
(ECall (kf, Cil_datatype.Varinfo.Hashtbl.create 3, tr)) env
(TCall (kf,b))
in
- env, c, []
+ env, c
else
- env, TCall (kf,b), []
+ env, TCall (kf,b)
| PReturn s ->
let kf =
try
@@ -957,9 +945,9 @@ let type_cond needs_pebble metaenv env tr cond =
in
if pos then
let env,c = add_current_event (EReturn kf) env (TReturn kf) in
- env, c, []
+ env, c
else
- env, TReturn kf, []
+ env, TReturn kf
in
aux true (ENone::env) cond
@@ -1029,7 +1017,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
| _ -> new_intermediate_state ()
in
Aorai_option.debug "Examining single elt:@\n%s -> %s:@[%a@]"
- curr_start.name my_end.name Promelaoutput.print_seq_elt elt;
+ curr_start.name my_end.name Promelaoutput.Parsed.print_seq_elt elt;
let guard_exit_loop env current counter =
if is_opt then TTrue
else
@@ -1070,9 +1058,9 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
[] -> my_end
| _ -> new_intermediate_state ()
in
- let trans_start = new_trans curr_start seq_start (Normal (TTrue,[]))
+ let trans_start = new_trans curr_start seq_start (Normal TTrue) []
in
- let inner_env, cond, act =
+ let inner_env, cond =
type_cond needs_pebble metaenv env trans_start cond
in
let (env,states, seq_transitions, seq_end) =
@@ -1089,8 +1077,8 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
let states = add_if_needed states curr_start in
let transitions = trans_start :: seq_transitions in
(match trans_start.cross with
- | Normal (conds,action) ->
- trans_start.cross <- Normal (tand cond conds,action @ act)
+ | Normal conds ->
+ trans_start.cross <- Normal (tand cond conds)
| Epsilon _ ->
Aorai_option.fatal
"Transition guard translated as epsilon transition");
@@ -1121,7 +1109,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
let auto = (inner_states,inner_trans) in
if at_most_one then begin
(* Just adds an epsilon transition from start to end *)
- let opt = new_trans curr_start oth_start (Epsilon (TTrue,[])) in
+ let opt = new_trans curr_start oth_start (Epsilon TTrue) [] in
env, states, opt::trans, curr_start, curr_end
end
else if has_loop then begin
@@ -1159,19 +1147,12 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
List.fold_left
(fun acc tr ->
let init_action = Counter_init (make_counter tr.stop) in
- let init_cross =
- match tr.cross with
- | Normal (cond, actions) ->
- Normal(cond, init_action :: actions)
- | Epsilon(cond, actions) ->
- Epsilon(cond, init_action :: actions)
- in
- Aorai_option.debug "New init trans %s -> %s: %a"
- st.name tr.stop.name
- print_epsilon_trans init_cross;
+ let init_actions = init_action :: tr.actions in
let init_trans =
- new_trans st tr.stop init_cross
+ new_trans st tr.stop tr.cross init_actions
in
+ Aorai_option.debug "New init trans %a"
+ print_eps_trans init_trans;
if at_most_one then init_trans :: acc
else begin
let st =
@@ -1183,24 +1164,22 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
(make_counter_term curr_start)
else TTrue
in
- let loop_action =
- if needs_counter then begin
+ let loop_actions =
+ if needs_counter then
let counter = make_counter curr_start in
- [ Counter_incr counter ]
- end else []
+ Counter_incr counter :: tr.actions
+ else tr.actions
in
let loop_cross =
match tr.cross with
- | Normal(cond, actions) ->
- Normal(tand loop_cond cond, loop_action @ actions)
- | Epsilon(cond, actions) ->
- Epsilon(tand loop_cond cond, loop_action @ actions)
+ | Normal cond -> Normal (tand loop_cond cond)
+ | Epsilon cond -> Epsilon (tand loop_cond cond)
in
- Aorai_option.debug "New loop trans %s -> %s: %a"
- inner_end.name tr.stop.name
- print_epsilon_trans loop_cross;
let loop_trans =
- new_trans inner_end tr.stop loop_cross in
+ new_trans inner_end tr.stop loop_cross loop_actions
+ in
+ Aorai_option.debug "New loop trans %a"
+ print_eps_trans loop_trans;
init_trans :: loop_trans :: acc
end)
oth_trans trans
@@ -1220,7 +1199,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
in
TRel (Cil_types.Req, t, Logic_const.tinteger ~loc 0)
in
- let no_seq = new_trans st oth_start (Epsilon (zero_cond,[])) in
+ let no_seq = new_trans st oth_start (Epsilon zero_cond) [] in
no_seq :: loop_trans
end else loop_trans
in
@@ -1236,11 +1215,10 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
guard_exit_loop env st (make_counter_term curr_end)
else TTrue
in
- let min_cond = Epsilon (min_cond,[]) in
- Aorai_option.debug "New exit trans %s -> %s: %a"
- inner_end.name oth_start.name
- print_epsilon_trans min_cond;
- let exit_trans = new_trans inner_end oth_start min_cond in
+ let min_cond = Epsilon min_cond in
+ let exit_trans = new_trans inner_end oth_start min_cond [] in
+ Aorai_option.debug "New exit trans %a"
+ print_eps_trans exit_trans;
let trans = exit_trans :: trans @ oth_trans in
states, trans
end else begin
@@ -1256,7 +1234,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
List.fold_left
(fun acc tr ->
match tr.cross with
- | Normal (cond,_) | Epsilon (cond,_) ->
+ | Normal cond | Epsilon cond ->
let cond = change_bound_var tr.stop st cond in
tor acc cond)
TFalse trans
@@ -1268,7 +1246,7 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
| _ ->
let reject = get_reject_state () in
let states = add_if_needed states reject in
- let trans = new_trans st reject (Normal(cond,[])) :: trans
+ let trans = new_trans st reject (Normal cond) [] :: trans
in states, trans @ oth_trans
)
end
@@ -1284,6 +1262,13 @@ let rec type_seq default_state tr metaenv env needs_pebble curr_start curr_end s
end else
env, states, trans, curr_start, curr_end
+let type_action metaenv env = function
+| Metavar_assign (s, e) ->
+ let vi = find_metavar s metaenv in
+ let _, e, _ = type_expr metaenv env e in
+ (* TODO: check type assignability *)
+ Copy_value ((TVar (Cil.cvar_to_lvar vi), TNoOffset), e)
+
let single_path (states,transitions as auto) tr =
Aorai_option.Deterministic.get () ||
(let init = Path_analysis.get_init_states auto in
@@ -1311,15 +1296,26 @@ let type_trans auto metaenv env tr =
in
Aorai_option.debug
"Analyzing transition %s -> %s: %a (needs pebble: %B)"
- tr.start.name tr.stop.name Promelaoutput.print_parsed tr.cross needs_pebble;
+ tr.start.name tr.stop.name
+ Promelaoutput.Parsed.print_guard
+ tr.cross needs_pebble;
match tr.cross with
| Seq seq ->
let default_state = find_otherwise_trans auto tr.start in
let has_default_state = Extlib.has_some default_state in
- let _,states, transitions,_,_ =
+ let env,states, transitions,_,_ =
type_seq has_default_state tr metaenv env needs_pebble tr.start tr.stop seq
in
- let (states, transitions) =
+ (* Insert metavariable assignments for transitions to tr.stop *)
+ let meta_actions = List.map (type_action metaenv env) tr.actions in
+ let add_meta_actions t =
+ if Aorai_state.equal t.stop tr.stop then
+ { t with actions = t.actions @ meta_actions }
+ else
+ t
+ in
+ let transitions = List.map add_meta_actions transitions in
+ let transitions =
if List.exists (fun st -> st.multi_state <> None) states then begin
(* We have introduced some multi-state somewhere, we have to introduce
pebbles and propagate them from state to state. *)
@@ -1334,26 +1330,25 @@ let type_trans auto metaenv env tr =
(fun trans ->
match trans.cross with
| Epsilon _ -> trans
- | Normal(cond,actions) ->
+ | Normal _ ->
let (dest,d_aux) = memo_multi_state tr.stop in
let actions =
if tr.start.nums <> start.nums then begin
let src,s_aux = memo_multi_state tr.start in
- Pebble_move(dest,d_aux,src,s_aux) :: actions
+ Pebble_move(dest,d_aux,src,s_aux) :: trans.actions
end else begin
let v = Cil.cvar_to_lvar count in
let incr = Counter_incr (TVar v, TNoOffset) in
let init = Pebble_init (dest, d_aux, v) in
- init::incr::actions
+ init::incr::trans.actions
end
in
- { trans with
- cross = Normal(cond, actions) })
+ { trans with actions })
transitions
in
- states, transitions
+ transitions
end else
- states, transitions
+ transitions
in
(* For each intermediate state, add a transition
to either the default state or a rejection state (in which we will
@@ -1368,8 +1363,8 @@ let type_trans auto metaenv env tr =
in
Aorai_option.debug "Resulting transitions:@\n%a"
(Pretty_utils.pp_list ~sep:"@\n"
- (fun fmt tr -> Format.fprintf fmt "%s -> %s:@[%a@]"
- tr.start.name tr.stop.name print_epsilon_trans tr.cross))
+ (fun fmt tr -> Format.fprintf fmt "%a"
+ print_eps_trans tr))
transitions;
states, transitions, needs_default
| Otherwise -> [],[], false (* treated directly by type_seq *)
@@ -1382,8 +1377,7 @@ let add_reject_trans auto intermediate_states =
let cond =
List.fold_left
(fun acc tr ->
- let cond,_ = tr.cross in
- let cond = change_bound_var tr.stop st cond in
+ let cond = change_bound_var tr.stop st tr.cross in
tor cond acc)
TFalse my_trans
in
@@ -1393,35 +1387,38 @@ let add_reject_trans auto intermediate_states =
| _ ->
Aorai_option.debug
"Adding default transition %s -> %s: %a"
- st.name reject_state.name Promelaoutput.print_condition cond;
- states, new_trans st reject_state (cond,[]) :: trans
+ st.name reject_state.name Promelaoutput.Typed.print_condition cond;
+ states, new_trans st reject_state cond [] :: trans
in
List.fold_left treat_one_state auto intermediate_states
let propagate_epsilon_transitions (states, _ as auto) =
- let rec transitive_closure start (conds,actions) known_states curr =
+ let rec transitive_closure start conds actions known_states curr =
let known_states = curr :: known_states in
let trans = Path_analysis.get_transitions_of_state curr auto in
List.fold_left
(fun acc tr ->
match tr.cross with
- | Epsilon (cond,my_actions) ->
+ | Epsilon cond ->
Aorai_option.debug "Treating epsilon trans %s -> %s"
curr.name tr.stop.name;
if List.exists (fun st -> st.nums = tr.stop.nums) known_states
then acc
else
transitive_closure
- start (tand cond conds, my_actions @ actions)
+ start (tand cond conds) (tr.actions @ actions)
known_states tr.stop @ acc
- | Normal (cond, action) ->
+ | Normal cond ->
Aorai_option.debug "Adding transition %s -> %s from epsilon trans"
start.name tr.stop.name;
- new_trans start tr.stop (tand cond conds,action @ actions) ::acc)
+ let tr =
+ new_trans start tr.stop (tand cond conds) (tr.actions @ actions)
+ in
+ tr :: acc)
[] trans
in
let treat_one_state acc st =
- acc @ transitive_closure st (TTrue,[]) [] st
+ acc @ transitive_closure st TTrue [] [] st
in
let trans = List.fold_left treat_one_state [] states in
(states, trans)
@@ -1435,26 +1432,26 @@ let add_default_trans (states, transitions as auto) otherwise =
let cond =
List.fold_left
(fun acc c ->
- let (cond,_) = c.cross in
+ let cond = c.cross in
Aorai_option.debug "considering trans %s -> %s: %a"
- c.start.name c.stop.name Promelaoutput.print_condition cond;
+ c.start.name c.stop.name Promelaoutput.Typed.print_condition cond;
let neg = tnot cond in
Aorai_option.debug "negation: %a"
- Promelaoutput.print_condition neg;
+ Promelaoutput.Typed.print_condition neg;
Aorai_option.debug "acc: %a"
- Promelaoutput.print_condition acc;
+ Promelaoutput.Typed.print_condition acc;
let res = tand acc (tnot cond) in
Aorai_option.debug "partial result: %a"
- Promelaoutput.print_condition res;
+ Promelaoutput.Typed.print_condition res;
res
)
TTrue
my_trans
in
Aorai_option.debug "resulting transition: %a"
- Promelaoutput.print_condition cond;
+ Promelaoutput.Typed.print_condition cond;
let cond,_ = Logic_simplification.simplifyCond cond in
- let new_trans = new_trans st tr.stop (cond,[]) in
+ let new_trans = new_trans st tr.stop cond [] in
new_trans::acc
in
let transitions = List.fold_left add_one_trans transitions otherwise in
@@ -1474,11 +1471,7 @@ let type_cond_auto auto =
"Considering parsed transition %s -> %s" tr.start.name tr.stop.name;
Aorai_option.debug
"Resulting transitions:@\n%a@\nEnd of transitions"
- (Pretty_utils.pp_list ~sep:"@\n"
- (fun fmt tr ->
- Format.fprintf fmt "%s -> %s: %a"
- tr.start.name tr.stop.name print_epsilon_trans tr.cross))
- trans;
+ (Pretty_utils.pp_list ~sep:"@\n" print_eps_trans) trans;
let add_reject =
if needs_reject then
(List.filter
@@ -1504,20 +1497,19 @@ let type_cond_auto auto =
let states, trans =
match Reject_state.get_option () with
| Some state ->
- (states, (new_trans state state (TTrue,[])):: transitions)
+ (states, new_trans state state TTrue [] :: transitions)
| None -> auto
in
let auto = { original_auto with states ; trans } in
if Aorai_option.debug_atleast 1 then
- Promelaoutput.output_dot_automata auto "aorai_debug_typed.dot";
+ Promelaoutput.Typed.output_dot_automata auto "aorai_debug_typed.dot";
let (_,trans) =
List.fold_left
(fun (i,l as acc) t ->
- let cond, action = t.cross in
- let cond = fst (Logic_simplification.simplifyCond cond)
+ let cond = fst (Logic_simplification.simplifyCond t.cross)
in match cond with
TFalse -> acc
- | _ -> (i+1,{ t with cross = (cond,action); numt = i } :: l))
+ | _ -> (i+1,{ t with cross = cond; numt = i } :: l))
(0,[]) trans
in
let _, states =
@@ -1562,7 +1554,7 @@ let setAutomata auto =
automata:=Some auto;
check_states "typed automata";
if Aorai_option.debug_atleast 1 then
- Promelaoutput.output_dot_automata auto "aorai_debug_reduced.dot";
+ Promelaoutput.Typed.output_dot_automata auto "aorai_debug_reduced.dot";
if (Array.length !cond_of_parametrizedTransitions) <
(getNumberOfTransitions ())
then
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index 2d440c0e0e8..8c7ed586075 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/src/plugins/aorai/data_for_aorai.mli
@@ -42,10 +42,8 @@ exception Empty_automaton
module Aorai_state: Datatype.S_with_collections with type t = Promelaast.state
-module Aorai_typed_trans:
- Datatype.S_with_collections
- with
- type t = (Promelaast.typed_condition * Promelaast.action) Promelaast.trans
+module Aorai_typed_trans:
+ Datatype.S_with_collections with type t = Promelaast.typed_trans
(** Initializes some tables according to data from Cil AST. *)
val setCData : unit -> unit
@@ -201,13 +199,13 @@ val buch_sync : string
val new_state: string -> state
-val new_trans: state -> state -> 'a -> 'a trans
+val new_trans: state -> state -> 'c -> 'a list -> ('c,'a) trans
(** Return the buchi automata as stored after parsing *)
val getAutomata : unit -> Promelaast.typed_automaton
(** Return only the graph part of the automata *)
-val getGraph : unit -> state list * (typed_condition * action) trans list
+val getGraph : unit -> state list * typed_trans list
(** Type-checks the parsed automaton and stores the result.
This might introduce new global variables in case of sequences.
@@ -249,8 +247,7 @@ val is_reject_state: state -> bool
(** returns the transition having the corresponding id.
@raise Not_found if this is not the case.
*)
-val getTransition:
- int -> (Promelaast.typed_condition * Promelaast.action) Promelaast.trans
+val getTransition: int -> Promelaast.typed_trans
(* ************************************************************************* *)
(**{b Variables information} Usually it seems very useful to access to varinfo
diff --git a/src/plugins/aorai/logic_simplification.ml b/src/plugins/aorai/logic_simplification.ml
index 88de692c01c..9bf174dd1ae 100644
--- a/src/plugins/aorai/logic_simplification.ml
+++ b/src/plugins/aorai/logic_simplification.ml
@@ -28,7 +28,7 @@ open Promelaast
let pretty_clause fmt l =
Format.fprintf fmt "@[<2>[%a@]]@\n"
- (Pretty_utils.pp_list ~sep:",@ " Promelaoutput.print_condition) l
+ (Pretty_utils.pp_list ~sep:",@ " Promelaoutput.Typed.print_condition) l
let pretty_dnf fmt l =
Format.fprintf fmt "@[<2>[%a@]]@\n"
@@ -360,7 +360,7 @@ let simplClause clause dnf =
*)
let simplifyCond condition =
Aorai_option.debug
- "initial condition: %a" Promelaoutput.print_condition condition;
+ "initial condition: %a" Promelaoutput.Typed.print_condition condition;
(* Step 1 : Condition is translate into Disjunctive Normal Form *)
let res1 = condToDNF condition in
Aorai_option.debug "initial dnf: %a" pretty_dnf res1;
@@ -394,14 +394,9 @@ let simplifyTrans transl =
let (crossCond , pcond ) = simplifyCond (tr.cross) in
(* pcond stands for parametrized condition :
disjunction of conjunctions of parametrized call/return *)
- let tr'={ start = tr.start ;
- stop = tr.stop ;
- cross = crossCond ;
- numt = tr.numt
- }
- in
+ let tr'= { tr with cross = crossCond } in
Aorai_option.debug "condition is %a, dnf is %a"
- Promelaoutput.print_condition crossCond pretty_dnf pcond;
+ Promelaoutput.Typed.print_condition crossCond pretty_dnf pcond;
if tr'.cross <> TFalse then (tr'::ltr,pcond::lpcond) else (ltr,lpcond)
)
([],[])
@@ -437,7 +432,7 @@ let simplifyDNFwrtCtx dnf kf1 status =
in
let res = tors (List.map simplCNFwrtCtx dnf) in
Aorai_option.debug
- "After simplification: %a" Promelaoutput.print_condition res; res
+ "After simplification: %a" Promelaoutput.Typed.print_condition res; res
(*
Tests :
diff --git a/src/plugins/aorai/logic_simplification.mli b/src/plugins/aorai/logic_simplification.mli
index 80956533bb6..6c58727222e 100644
--- a/src/plugins/aorai/logic_simplification.mli
+++ b/src/plugins/aorai/logic_simplification.mli
@@ -45,8 +45,8 @@ val simplifyCond:
simplifyCond done on each cross condition. Uncrossable transition are
removed. *)
val simplifyTrans:
- Promelaast.typed_condition Promelaast.trans list ->
- (Promelaast.typed_condition Promelaast.trans list)*
+ Promelaast.typed_trans list ->
+ (Promelaast.typed_trans list)*
(Promelaast.typed_condition list list list)
val dnfToCond :
diff --git a/src/plugins/aorai/promelaast.mli b/src/plugins/aorai/promelaast.mli
index 3f7ac668c9f..518a203b36d 100644
--- a/src/plugins/aorai/promelaast.mli
+++ b/src/plugins/aorai/promelaast.mli
@@ -47,7 +47,6 @@ type condition =
| PCall of string * string option
(** Call might be done in a given behavior *)
| PReturn of string
- | PAssign of string * expression
and seq_elt =
{ condition: condition option;
@@ -62,7 +61,10 @@ and sequence = seq_elt list
otherwise keyword. A single condition is expressed with a singleton
having an empty nested sequence and min_rep and max_rep being equal to one.
*)
-type parsed_condition = Seq of sequence | Otherwise
+type guard = Seq of sequence | Otherwise
+
+type action =
+ | Metavar_assign of string * expression
type typed_condition =
| TOr of typed_condition * typed_condition (** Logical OR *)
@@ -80,7 +82,11 @@ type typed_condition =
tied to the corresponding value.
*)
-type single_action =
+(** Additional actions to perform when crossing a transition.
+ There is at most one Pebble_* action for each transition, and
+ each transition leading to a state with multi-state has such an action.
+ *)
+type typed_action =
| Counter_init of Cil_types.term_lval
| Counter_incr of Cil_types.term_lval
| Pebble_init of
@@ -96,14 +102,9 @@ type single_action =
moves pebbles from [old_set] to [new_set], governed by the
corresponding aux variables. *)
| Copy_value of Cil_types.term_lval * Cil_types.term
- (** copy the current value of the given term into the given location
- so that it can be accessed by a later state. *)
+ (** copy the current value of the given term into the given location
+ so that it can be accessed by a later state. *)
-(** Additional actions to perform when crossing a transition.
- There is at most one Pebble_* action for each transition, and
- each transition leading to a state with multi-state has such an action.
- *)
-type action = single_action list
(** Internal representation of a State from the Buchi automata. *)
type state =
@@ -125,23 +126,28 @@ type state =
}
(** Internal representation of a transition from the Buchi automata. *)
-type 'condition trans =
- { start : state ; (** Starting state of the transition *)
- stop : state ; (** Ending state of the transition *)
- mutable cross : 'condition ; (** Cross condition of the transition *)
- mutable numt : int (** Numerical ID of the transition *)
+type ('c,'a) trans =
+ { start : state ; (** Starting state of the transition *)
+ stop : state ; (** Ending state of the transition *)
+ mutable cross : 'c; (** Cross condition of the transition *)
+ mutable actions : 'a list; (** Actions to execute while crossing *)
+ mutable numt : int (** Numerical ID of the transition *)
}
+type parsed_trans = (guard, action) trans
+
+type typed_trans = (typed_condition, typed_action) trans
+
(** Internal representation of a Buchi automata : a list of states and a list of transitions.*)
-type 'condition automaton = {
+type ('c,'a) automaton = {
states: state list;
- trans: ('condition trans) list;
+ trans: (('c,'a) trans) list;
metavariables: Cil_types.varinfo Datatype.String.Map.t;
}
-type parsed_automaton = parsed_condition automaton
+type parsed_automaton = (guard, action) automaton
-type typed_automaton = (typed_condition * action) automaton
+type typed_automaton = (typed_condition, typed_action) automaton
(** An operation can have two status: currently calling or returning. *)
type funcStatus =
diff --git a/src/plugins/aorai/promelaoutput.ml b/src/plugins/aorai/promelaoutput.ml
index 85afe95f6ed..0eaf37ee308 100644
--- a/src/plugins/aorai/promelaoutput.ml
+++ b/src/plugins/aorai/promelaoutput.ml
@@ -30,139 +30,8 @@ open Promelaast
open Bool3
open Format
-let string_of_unop = function
- | Uminus -> "-"
- | Ustar -> "*"
- | Uamp -> "&"
- | Ubw_not -> "~"
-
-let rec print_parsed_expression fmt = function
- | PVar s -> Format.fprintf fmt "%s" s
- | PPrm (f,s) -> Format.fprintf fmt "%s().%s" f s
- | PMetavar s -> Format.fprintf fmt "$%s" s
- | PCst (IntConstant s) -> Format.fprintf fmt "%s" s
- | PCst (FloatConstant s) -> Format.fprintf fmt "%s" s
- | PCst (StringConstant s) -> Format.fprintf fmt "%S" s
- | PCst (WStringConstant s) -> Format.fprintf fmt "%S" s
- | PBinop(bop,e1,e2) ->
- Format.fprintf fmt "(@[%a@])@ %a@ (@[%a@])"
- print_parsed_expression e1 Printer.pp_binop (Logic_typing.type_binop bop)
- print_parsed_expression e2
- | PUnop(uop,e) -> Format.fprintf fmt "%s@;(@[%a@])"
- (string_of_unop uop)
- print_parsed_expression e
- | PArrget(e1,e2) -> Format.fprintf fmt "%a@;[@(%a@]]"
- print_parsed_expression e1 print_parsed_expression e2
- | PField(e,s) -> Format.fprintf fmt "%a.%s" print_parsed_expression e s
- | PArrow(e,s) -> Format.fprintf fmt "%a->%s" print_parsed_expression e s
-
-let rec print_parsed_condition fmt = function
- | PRel(rel,e1,e2) ->
- Format.fprintf fmt "%a %a@ %a"
- print_parsed_expression e1
- Printer.pp_relation (Logic_typing.type_rel rel)
- print_parsed_expression e2
- | PTrue -> Format.pp_print_string fmt "true"
- | PFalse -> Format.pp_print_string fmt "false"
- | POr(e1,e2) -> Format.fprintf fmt "(@[%a@])@ or@ (@[%a@])"
- print_parsed_condition e1 print_parsed_condition e2
- | PAnd(e1,e2) -> Format.fprintf fmt "(@[%a@])@ and@ (@[%a@])"
- print_parsed_condition e1 print_parsed_condition e2
- | PNot c -> Format.fprintf fmt "not(@[%a@])"
- print_parsed_condition c
- | PCall (s,None) -> Format.fprintf fmt "CALL(%s)" s
- | PCall (s, Some b) -> Format.fprintf fmt "CALL(%s::%s)" s b
- | PReturn s -> Format.fprintf fmt "RETURN(%s)" s
- | PAssign (s, e) -> Format.fprintf fmt " %s := %a " s print_parsed_expression e
-
-let rec print_seq_elt fmt elt =
- Format.fprintf fmt "(%a%a){@[%a,%a@]}"
- (Pretty_utils.pp_opt print_parsed_condition) elt.condition
- print_sequence elt.nested
- (Pretty_utils.pp_opt print_parsed_expression) elt.min_rep
- (Pretty_utils.pp_opt print_parsed_expression) elt.max_rep
-
-and print_sequence fmt l =
- Pretty_utils.pp_list ~pre:"[@[" ~sep:";@ " ~suf:"@]]" print_seq_elt fmt l
-
-let print_parsed fmt = function
- | Seq l -> print_sequence fmt l
- | Otherwise -> Format.pp_print_string fmt "Otherwise"
-
-let rec print_condition fmt = function
- | TCall (kf,None) ->
- Format.fprintf fmt "Call(%a)" Kernel_function.pretty kf
- | TCall (kf, Some b) ->
- Format.fprintf fmt "Call(%a::%s)"
- Kernel_function.pretty kf b.Cil_types.b_name
- | TReturn kf ->
- Format.fprintf fmt "Return(%a)" Kernel_function.pretty kf
- | TOr (c1,c2) ->
- Format.fprintf fmt "@[<hov>(@[<2>%a@])@]@ or@ @[<hov>(@[<2>%a@])@]"
- print_condition c1 print_condition c2
- | TAnd (c1,c2) ->
- Format.fprintf fmt "@[<hov>(@[<2>%a@])@]@ and@ @[<hov>(@[<2>%a@])@]"
- print_condition c1 print_condition c2
- | TNot c ->
- Format.fprintf fmt "@[<hov 4>@[<hov 5>not(%a@])@]" print_condition c
- | TTrue -> Format.pp_print_string fmt "True"
- | TFalse -> Format.pp_print_string fmt "False"
- | TRel(rel,exp1,exp2) ->
- (* \result will be printed as such, not as f().return *)
- Format.fprintf fmt "@[(%a)@]@ %a@ @[(%a)@]"
- Printer.pp_term exp1
- Printer.pp_relation rel
- Printer.pp_term exp2
-
-let print_one_action fmt = function
- | Counter_init lv ->
- Format.fprintf fmt "@[%a <- 1@]" Printer.pp_term_lval lv
- | Counter_incr lv ->
- Format.fprintf fmt "@[%a <- @[%a@ +@ 1@]@]"
- Printer.pp_term_lval lv Printer.pp_term_lval lv
- | Pebble_init (set,_,v) ->
- Format.fprintf fmt "@[%a <- {@[ %a @]}@]"
- Printer.pp_logic_var set.l_var_info Printer.pp_logic_var v
- | Pebble_move(s1,_,s2,_) ->
- Format.fprintf fmt "@[%a <- %a@]"
- Printer.pp_logic_var s1.l_var_info
- Printer.pp_logic_var s2.l_var_info
- | Copy_value(lv,v) ->
- Format.fprintf fmt "@[%a <- %a@]" Printer.pp_term_lval lv Printer.pp_term v
-
-let print_action fmt l =
- Pretty_utils.pp_list ~sep:"@\n" print_one_action fmt l
-
-(* Use well-parenthesized combination of escape_newline/normal_newline*)
-let escape_newline fmt =
- let funcs = Format.pp_get_formatter_out_functions fmt () in
- let has_printed = ref false in
- let out_newline () =
- if !has_printed then funcs.Format.out_string " \\\n" 0 3
- else funcs.Format.out_newline ()
- in
- let out_string s b l =
- if String.contains (String.sub s b l) '"' then
- has_printed:=not !has_printed;
- funcs.Format.out_string s b l
- in
- Format.pp_set_formatter_out_functions fmt
- { funcs with Format.out_newline; out_string };
- funcs
-
-let print_full_transition fmt (cond,action) =
- Format.fprintf fmt "%a@\n%a" print_condition cond print_action action
-
-let trans_label num = "tr"^string_of_int(num)
-
-let print_trans fmt trans =
- Format.fprintf fmt
- "@[<2>%s:@ %a@]"
- (trans_label trans.numt) print_full_transition trans.cross
+type 'a printer = Format.formatter -> 'a -> unit
-let state_label num = "st"^string_of_int(num)
-let print_state_label fmt st =
- Format.fprintf fmt "@[<2>%s:@ %s@]" (state_label st.nums) st.name
let print_bool3 fmt b =
Format.pp_print_string fmt
@@ -171,14 +40,6 @@ let print_bool3 fmt b =
| False -> "False"
| Undefined -> "Undef")
-let print_transition fmt tr =
- Format.fprintf fmt "@[<2>{@ %d:@ %s@ {%a}@ %s@]}"
- tr.numt tr.start.name print_full_transition tr.cross tr.stop.name
-
-let print_transitionl fmt trl =
- Format.fprintf fmt "@[<2>Transitions:@\n%a@]"
- (Pretty_utils.pp_list ~sep:"@\n" ~suf:"@\n" print_transition) trl
-
let print_state fmt st =
Format.fprintf fmt "@[<2>%s@ (acc=%a;@ init=%a;@ num=%d)@]"
st.name print_bool3 st.acceptation print_bool3 st.init st.nums
@@ -187,64 +48,223 @@ let print_statel fmt stl =
Format.fprintf fmt "@[<2>States:@\n%a@]"
(Pretty_utils.pp_list ~sep:"@\n" ~suf:"@\n" print_state) stl
-let print_raw_automata fmt auto =
- Format.fprintf fmt "@[<2>Automaton:@\n%a%a@]"
- print_statel auto.states print_transitionl auto.trans
-
-let dot_state out st =
- let shape =
- if st.init = Bool3.True && st.acceptation=Bool3.True then "doubleoctagon"
- else if st.acceptation=Bool3.True then "octagon"
- else if st.init=Bool3.True then "doublecircle"
- else "circle"
- in
- Format.fprintf out "\"%a\" [shape = %s];@\n" print_state_label st shape
-
-let dot_trans out tr =
- let print_label fmt tr =
- if DotSeparatedLabels.get () then
- Format.pp_print_int fmt tr.numt
- else print_trans fmt tr
- in
- Format.fprintf
- out
- "\"%a\"@ ->@ \"%a\"@ [label = @[\"%a\"@]];@\n"
- print_state_label tr.start
- print_state_label tr.stop
- print_label tr
-
-let output_dot_automata {states ; trans} fichier =
- let cout = open_out fichier in
- let fmt = formatter_of_out_channel cout in
- let output_functions = escape_newline fmt in
- let one_line_comment s =
- let l = String.length s in
- let fill = if l >= 75 then 0 else 75 - l in
- let spaces = String.make fill ' ' in
- Format.fprintf fmt "@[/* %s%s*/@\n@]" s spaces
- in
- one_line_comment "File generated by Aorai LTL2ACSL Plug-in";
- one_line_comment "";
- one_line_comment "Usage of dot files '.dot' :";
- one_line_comment " dot <MyFile.dot> -T<DesiredType> > <OutputFile>";
- one_line_comment "";
- one_line_comment " Allowed types : canon,dot,xdot,fig,gd,gd2,";
- one_line_comment " gif,hpgl,imap,cmap,ismap,jpg,jpeg,mif,mp,pcl,pic,plain,";
- one_line_comment " plain-ext,png,ps,ps2,svg,svgz,vrml,vtx,wbmp";
- one_line_comment "";
- one_line_comment " Example with postscript file :";
- one_line_comment " dot property.dot -Tps > property.ps";
- Format.fprintf fmt "@[<2>@\ndigraph %s {@\n@\n%a@\n%a@\n%t}@\n@]"
- (Filename.chop_extension (Filename.basename fichier))
- (Pretty_utils.pp_list dot_state) states
- (Pretty_utils.pp_list dot_trans) trans
- (fun fmt ->
+let state_label num = "st"^string_of_int(num)
+let print_state_label fmt st =
+ Format.fprintf fmt "@[<2>%s:@ %s@]" (state_label st.nums) st.name
+
+
+module Parsed =
+struct
+ let string_of_unop = function
+ | Uminus -> "-"
+ | Ustar -> "*"
+ | Uamp -> "&"
+ | Ubw_not -> "~"
+
+ let rec print_expression fmt = function
+ | PVar s -> Format.fprintf fmt "%s" s
+ | PPrm (f,s) -> Format.fprintf fmt "%s().%s" f s
+ | PMetavar s -> Format.fprintf fmt "$%s" s
+ | PCst (IntConstant s) -> Format.fprintf fmt "%s" s
+ | PCst (FloatConstant s) -> Format.fprintf fmt "%s" s
+ | PCst (StringConstant s) -> Format.fprintf fmt "%S" s
+ | PCst (WStringConstant s) -> Format.fprintf fmt "%S" s
+ | PBinop(bop,e1,e2) ->
+ Format.fprintf fmt "(@[%a@])@ %a@ (@[%a@])"
+ print_expression e1 Printer.pp_binop (Logic_typing.type_binop bop)
+ print_expression e2
+ | PUnop(uop,e) -> Format.fprintf fmt "%s@;(@[%a@])"
+ (string_of_unop uop)
+ print_expression e
+ | PArrget(e1,e2) -> Format.fprintf fmt "%a@;[@(%a@]]"
+ print_expression e1 print_expression e2
+ | PField(e,s) -> Format.fprintf fmt "%a.%s" print_expression e s
+ | PArrow(e,s) -> Format.fprintf fmt "%a->%s" print_expression e s
+
+ let rec print_condition fmt = function
+ | PRel(rel,e1,e2) ->
+ Format.fprintf fmt "%a %a@ %a"
+ print_expression e1
+ Printer.pp_relation (Logic_typing.type_rel rel)
+ print_expression e2
+ | PTrue -> Format.pp_print_string fmt "true"
+ | PFalse -> Format.pp_print_string fmt "false"
+ | POr(e1,e2) -> Format.fprintf fmt "(@[%a@])@ or@ (@[%a@])"
+ print_condition e1 print_condition e2
+ | PAnd(e1,e2) -> Format.fprintf fmt "(@[%a@])@ and@ (@[%a@])"
+ print_condition e1 print_condition e2
+ | PNot c -> Format.fprintf fmt "not(@[%a@])"
+ print_condition c
+ | PCall (s,None) -> Format.fprintf fmt "CALL(%s)" s
+ | PCall (s, Some b) -> Format.fprintf fmt "CALL(%s::%s)" s b
+ | PReturn s -> Format.fprintf fmt "RETURN(%s)" s
+
+ let rec print_seq_elt fmt elt =
+ Format.fprintf fmt "(%a%a){@[%a,%a@]}"
+ (Pretty_utils.pp_opt print_condition) elt.condition
+ print_sequence elt.nested
+ (Pretty_utils.pp_opt print_expression) elt.min_rep
+ (Pretty_utils.pp_opt print_expression) elt.max_rep
+
+ and print_sequence fmt l =
+ Pretty_utils.pp_list ~pre:"[@[" ~sep:";@ " ~suf:"@]]" print_seq_elt fmt l
+
+ let print_guard fmt = function
+ | Seq l -> print_sequence fmt l
+ | Otherwise -> Format.pp_print_string fmt "Otherwise"
+
+ let print_action fmt = function
+ | Metavar_assign (s, e) ->
+ Format.fprintf fmt "@[$%s := %a@]" s print_expression e
+
+ let print_actionl fmt l =
+ Pretty_utils.pp_list ~sep:"@\n" print_action fmt l
+end
+
+
+module Typed =
+struct
+ let rec print_condition fmt = function
+ | TCall (kf,None) ->
+ Format.fprintf fmt "Call(%a)" Kernel_function.pretty kf
+ | TCall (kf, Some b) ->
+ Format.fprintf fmt "Call(%a::%s)"
+ Kernel_function.pretty kf b.Cil_types.b_name
+ | TReturn kf ->
+ Format.fprintf fmt "Return(%a)" Kernel_function.pretty kf
+ | TOr (c1,c2) ->
+ Format.fprintf fmt "@[<hov>(@[<2>%a@])@]@ or@ @[<hov>(@[<2>%a@])@]"
+ print_condition c1 print_condition c2
+ | TAnd (c1,c2) ->
+ Format.fprintf fmt "@[<hov>(@[<2>%a@])@]@ and@ @[<hov>(@[<2>%a@])@]"
+ print_condition c1 print_condition c2
+ | TNot c ->
+ Format.fprintf fmt "@[<hov 4>@[<hov 5>not(%a@])@]" print_condition c
+ | TTrue -> Format.pp_print_string fmt "True"
+ | TFalse -> Format.pp_print_string fmt "False"
+ | TRel(rel,exp1,exp2) ->
+ (* \result will be printed as such, not as f().return *)
+ Format.fprintf fmt "@[(%a)@]@ %a@ @[(%a)@]"
+ Printer.pp_term exp1
+ Printer.pp_relation rel
+ Printer.pp_term exp2
+
+ let print_action fmt = function
+ | Counter_init lv ->
+ Format.fprintf fmt "@[%a <- 1@]" Printer.pp_term_lval lv
+ | Counter_incr lv ->
+ Format.fprintf fmt "@[%a <- @[%a@ +@ 1@]@]"
+ Printer.pp_term_lval lv Printer.pp_term_lval lv
+ | Pebble_init (set,_,v) ->
+ Format.fprintf fmt "@[%a <- {@[ %a @]}@]"
+ Printer.pp_logic_var set.l_var_info Printer.pp_logic_var v
+ | Pebble_move(s1,_,s2,_) ->
+ Format.fprintf fmt "@[%a <- %a@]"
+ Printer.pp_logic_var s1.l_var_info
+ Printer.pp_logic_var s2.l_var_info
+ | Copy_value(lv,v) ->
+ Format.fprintf fmt "@[%a <- %a@]" Printer.pp_term_lval lv Printer.pp_term v
+
+ let print_actionl fmt l =
+ Pretty_utils.pp_list ~sep:"@\n" print_action fmt l
+
+ (* Use well-parenthesized combination of escape_newline/normal_newline*)
+ let escape_newline fmt =
+ let funcs = Format.pp_get_formatter_out_functions fmt () in
+ let has_printed = ref false in
+ let out_newline () =
+ if !has_printed then funcs.Format.out_string " \\\n" 0 3
+ else funcs.Format.out_newline ()
+ in
+ let out_string s b l =
+ if String.contains (String.sub s b l) '"' then
+ has_printed:=not !has_printed;
+ funcs.Format.out_string s b l
+ in
+ Format.pp_set_formatter_out_functions fmt
+ { funcs with Format.out_newline; out_string };
+ funcs
+
+ let trans_label num = "tr"^string_of_int(num)
+
+ let print_trans fmt trans =
+ Format.fprintf fmt
+ "@[<2>%s:@ %a@\n%a@]"
+ (trans_label trans.numt)
+ print_condition trans.cross
+ print_actionl trans.actions
+
+ let print_transition fmt tr =
+ Format.fprintf fmt "@[<2>{@ %d:@ %s@ {%a@\n%a}@ %s@]}"
+ tr.numt
+ tr.start.name
+ print_condition tr.cross
+ print_actionl tr.actions
+ tr.stop.name
+
+ let print_transitionl fmt trl =
+ Format.fprintf fmt "@[<2>Transitions:@\n%a@]"
+ (Pretty_utils.pp_list ~sep:"@\n" ~suf:"@\n" print_transition) trl
+
+ let print_automata fmt auto =
+ Format.fprintf fmt "@[<2>Automaton:@\n%a%a@]"
+ print_statel auto.states print_transitionl auto.trans
+
+ let dot_state out st =
+ let shape =
+ if st.init = Bool3.True && st.acceptation=Bool3.True then "doubleoctagon"
+ else if st.acceptation=Bool3.True then "octagon"
+ else if st.init=Bool3.True then "doublecircle"
+ else "circle"
+ in
+ Format.fprintf out "\"%a\" [shape = %s];@\n" print_state_label st shape
+
+ let dot_trans out tr =
+ let print_label fmt tr =
if DotSeparatedLabels.get () then
- (Format.fprintf fmt
- "/* guards of transitions */@\ncomment=\"%a\";@\n"
- (Pretty_utils.pp_list ~sep:"@\n" print_trans) trans));
- Format.pp_set_formatter_out_functions fmt output_functions;
- close_out cout
+ Format.pp_print_int fmt tr.numt
+ else print_trans fmt tr
+ in
+ Format.fprintf
+ out
+ "\"%a\"@ ->@ \"%a\"@ [label = @[\"%a\"@]];@\n"
+ print_state_label tr.start
+ print_state_label tr.stop
+ print_label tr
+
+ let output_dot_automata {states ; trans} fichier =
+ let cout = open_out fichier in
+ let fmt = formatter_of_out_channel cout in
+ let output_functions = escape_newline fmt in
+ let one_line_comment s =
+ let l = String.length s in
+ let fill = if l >= 75 then 0 else 75 - l in
+ let spaces = String.make fill ' ' in
+ Format.fprintf fmt "@[/* %s%s*/@\n@]" s spaces
+ in
+ one_line_comment "File generated by Aorai LTL2ACSL Plug-in";
+ one_line_comment "";
+ one_line_comment "Usage of dot files '.dot' :";
+ one_line_comment " dot <MyFile.dot> -T<DesiredType> > <OutputFile>";
+ one_line_comment "";
+ one_line_comment " Allowed types : canon,dot,xdot,fig,gd,gd2,";
+ one_line_comment " gif,hpgl,imap,cmap,ismap,jpg,jpeg,mif,mp,pcl,pic,plain,";
+ one_line_comment " plain-ext,png,ps,ps2,svg,svgz,vrml,vtx,wbmp";
+ one_line_comment "";
+ one_line_comment " Example with postscript file :";
+ one_line_comment " dot property.dot -Tps > property.ps";
+ Format.fprintf fmt "@[<2>@\ndigraph %s {@\n@\n%a@\n%a@\n%t}@\n@]"
+ (Filename.chop_extension (Filename.basename fichier))
+ (Pretty_utils.pp_list dot_state) states
+ (Pretty_utils.pp_list dot_trans) trans
+ (fun fmt ->
+ if DotSeparatedLabels.get () then
+ (Format.fprintf fmt
+ "/* guards of transitions */@\ncomment=\"%a\";@\n"
+ (Pretty_utils.pp_list ~sep:"@\n" print_trans) trans));
+ Format.pp_set_formatter_out_functions fmt output_functions;
+ close_out cout
+end
(*
Local Variables:
diff --git a/src/plugins/aorai/promelaoutput.mli b/src/plugins/aorai/promelaoutput.mli
index 75dcc4bba26..3edf6aabb28 100644
--- a/src/plugins/aorai/promelaoutput.mli
+++ b/src/plugins/aorai/promelaoutput.mli
@@ -23,35 +23,35 @@
(* *)
(**************************************************************************)
-val print_raw_automata :
- Format.formatter -> Promelaast.typed_automaton -> unit
+open Promelaast
+
+type 'a printer = Format.formatter -> 'a -> unit
+
+val print_state : state printer
+val print_statel : state list printer
+
+module Parsed:
+sig
+ val print_expression: expression printer
+ val print_condition: condition printer
+ val print_seq_elt: seq_elt printer
+ val print_sequence: sequence printer
+ val print_guard: guard printer
+ val print_action: action printer
+ val print_actionl: action list printer
+end
+
+module Typed:
+sig
+ val print_condition : typed_condition printer
+ val print_action: typed_action printer
+ val print_actionl: typed_action list printer
+ val print_transition: typed_trans printer
+ val print_transitionl: typed_trans list printer
+ val print_automata : typed_automaton printer
+ val output_dot_automata : typed_automaton -> string -> unit
+end
-val print_parsed_expression: Format.formatter -> Promelaast.expression -> unit
-
-val print_parsed_condition: Format.formatter -> Promelaast.condition -> unit
-
-val print_seq_elt: Format.formatter -> Promelaast.seq_elt -> unit
-
-val print_sequence: Format.formatter -> Promelaast.sequence -> unit
-
-val print_parsed: Format.formatter -> Promelaast.parsed_condition -> unit
-
-val print_condition: Format.formatter -> Promelaast.typed_condition -> unit
-
-val print_action: Format.formatter -> Promelaast.action -> unit
-
-val print_transition:
- Format.formatter ->
- (Promelaast.typed_condition * Promelaast.action) Promelaast.trans -> unit
-
-val print_transitionl:
- Format.formatter ->
- (Promelaast.typed_condition * Promelaast.action) Promelaast.trans list -> unit
-
-val print_state : Format.formatter -> Promelaast.state -> unit
-val print_statel : Format.formatter -> Promelaast.state list -> unit
-
-val output_dot_automata : Promelaast.typed_automaton -> string -> unit
(*
Local Variables:
diff --git a/src/plugins/aorai/promelaparser.mly b/src/plugins/aorai/promelaparser.mly
index 2946304bdbe..4bcac643722 100644
--- a/src/plugins/aorai/promelaparser.mly
+++ b/src/plugins/aorai/promelaparser.mly
@@ -119,9 +119,9 @@ state
trans
else
let tr_list=
- List.fold_left (fun l1 (cr,stop_st) ->
- List.fold_left (fun l2 st ->
- {start=st;stop=stop_st;cross=Seq (to_seq cr);numt=(-1)}::l2
+ List.fold_left (fun l1 (cr,stop) ->
+ List.fold_left (fun l2 start ->
+ {start;stop;cross=Seq (to_seq cr);actions=[];numt=(-1)}::l2
) l1 stl
) [] trl
in
@@ -166,7 +166,7 @@ label
(String.compare (String.sub $1 0 10) "accept_all")=0
then
trans:=
- {start=old;stop=old;cross=Seq (to_seq PTrue);numt=(-1)} ::
+ {start=old;stop=old;cross=Seq (to_seq PTrue);actions=[];numt=(-1)} ::
!trans;
(* If the name includes accept then
this state is an acceptation one. *)
diff --git a/src/plugins/aorai/promelaparser_withexps.mly b/src/plugins/aorai/promelaparser_withexps.mly
index 1fd125c99c7..bf852a65f37 100644
--- a/src/plugins/aorai/promelaparser_withexps.mly
+++ b/src/plugins/aorai/promelaparser_withexps.mly
@@ -128,9 +128,9 @@ state
trans
else
let tr_list=
- List.fold_left (fun l1 (cr,stop_st) ->
- List.fold_left (fun l2 st ->
- {start=st;stop=stop_st;cross=Seq (to_seq cr);numt=(-1)}::l2
+ List.fold_left (fun l1 (cr,stop) ->
+ List.fold_left (fun l2 start ->
+ {start;stop;cross=Seq (to_seq cr);actions=[];numt=(-1)}::l2
) l1 stl
) [] trl
in
@@ -178,7 +178,7 @@ label
(String.compare (String.sub $1 0 10) "accept_all")=0
then
trans:=
- {start=old;stop=old;cross=Seq (to_seq PTrue);numt=(-1)}::!trans;
+ {start=old;stop=old;cross=Seq (to_seq PTrue);actions=[];numt=(-1)}::!trans;
(* If the name includes accept then this state is
an acceptation one. *)
diff --git a/src/plugins/aorai/tests/ya/metavariables-right.ya b/src/plugins/aorai/tests/ya/metavariables-right.ya
index 2e5be920ec1..bacd7713870 100644
--- a/src/plugins/aorai/tests/ya/metavariables-right.ya
+++ b/src/plugins/aorai/tests/ya/metavariables-right.ya
@@ -7,7 +7,7 @@ $x : int;
a : { CALL(main) } -> b;
b :
- { CALL(f) && $x := f().x } -> c
+ { CALL(f) } $x := f().x -> c
| { CALL(g) } -> d
;
@@ -24,6 +24,6 @@ f : { RETURN(h) } -> g;
g : { CALL(i) } -> h;
-h : { RETURN(i) && $x := 1 } -> e;
+h : { RETURN(i) } $x := 1 -> e;
i : -> i;
diff --git a/src/plugins/aorai/tests/ya/metavariables-wrong.ya b/src/plugins/aorai/tests/ya/metavariables-wrong.ya
index 6ab66a2fa64..8a29440dfdd 100644
--- a/src/plugins/aorai/tests/ya/metavariables-wrong.ya
+++ b/src/plugins/aorai/tests/ya/metavariables-wrong.ya
@@ -7,7 +7,7 @@ $x : int;
a : { CALL(main) } -> b;
b :
- { CALL(f) && $x := f().x } -> c
+ { CALL(f) } $x := f().x -> c
| { CALL(g) } -> d
| { RETURN(main) } -> g
;
diff --git a/src/plugins/aorai/tests/ya/stack.ya b/src/plugins/aorai/tests/ya/stack.ya
index 4bbf8c1355f..29c24e7847e 100644
--- a/src/plugins/aorai/tests/ya/stack.ya
+++ b/src/plugins/aorai/tests/ya/stack.ya
@@ -5,7 +5,7 @@
$n : int;
init:
- { CALL(main) && $n := 0 } -> empty_stack
+ { CALL(main) } $n := 0 -> empty_stack
;
empty_stack:
@@ -14,7 +14,7 @@ empty_stack:
;
filling_stack:
- { RETURN(push) && $n := $n + 1 } -> filled_stack
+ { RETURN(push) } $n := $n + 1 -> filled_stack
;
filled_stack:
@@ -23,8 +23,8 @@ filled_stack:
;
emptying_stack:
- { RETURN(pop) && $n > 1 && $n := $n - 1 } -> filled_stack
-| { RETURN(pop) && $n == 1 && $n := $n - 1 } -> empty_stack
+ { RETURN(pop) && $n > 1 } $n := $n - 1 -> filled_stack
+| { RETURN(pop) && $n == 1 } $n := $n - 1 -> empty_stack
;
accept: -> accept;
diff --git a/src/plugins/aorai/yaparser.mly b/src/plugins/aorai/yaparser.mly
index ab9603e45c5..655a5d32db9 100644
--- a/src/plugins/aorai/yaparser.mly
+++ b/src/plugins/aorai/yaparser.mly
@@ -158,7 +158,7 @@ type pre_cond = Behavior of string | Pre of Promelaast.condition
%left DOT
%nonassoc NOT TRUE FALSE
%nonassoc QUESTION
-%right SEMICOLON
+%right SEMI_COLON
%nonassoc lowest
%type <Promelaast.parsed_automaton> main
@@ -214,7 +214,7 @@ state
let start_state = fetch_and_create_state $1 in
let (_, transitions) =
List.fold_left
- (fun (otherwise, transitions) (cross,stop_state) ->
+ (fun (otherwise, transitions) (cross,actions,stop_state) ->
if otherwise then
Aorai_option.abort
"'other' directive in definition of %s \
@@ -222,7 +222,7 @@ state
else begin
let trans =
{ start=start_state; stop=stop_state;
- cross=cross; numt=(-1) }::transitions
+ cross; actions; numt=(-1) }::transitions
in
let otherwise =
match cross with
@@ -242,10 +242,12 @@ transitions /*=> [transition; ...] */
transition: /*=> (guard, state) */
- | LCURLY seq_elt RCURLY RARROW IDENTIFIER
- { (Seq $2, prefetch_and_create_state $5) }
- | OTHERWISE RARROW IDENTIFIER {(Otherwise, prefetch_and_create_state $3) }
- | RARROW IDENTIFIER { (Seq (to_seq PTrue), prefetch_and_create_state $2) }
+ | LCURLY seq_elt RCURLY actions RARROW IDENTIFIER
+ { (Seq $2, $4, prefetch_and_create_state $6) }
+ | OTHERWISE actions RARROW IDENTIFIER
+ { (Otherwise, $2, prefetch_and_create_state $4) }
+ | actions RARROW IDENTIFIER
+ { (Seq (to_seq PTrue), $1, prefetch_and_create_state $3) }
;
non_empty_seq:
@@ -338,7 +340,6 @@ single_cond:
| single_cond OR single_cond { POr ($1,$3) }
| LPAREN single_cond RPAREN { $2 }
| logic_relation { $1 }
- | METAVAR AFF arith_relation { PAssign ($1, $3) }
;
logic_relation
@@ -392,3 +393,17 @@ access_leaf
| LPAREN access RPAREN { $2 }
| METAVAR { PMetavar $1 }
;
+
+actions
+ : /* epsilon */ { [] }
+ | non_empty_actions { $1 }
+ ;
+
+non_empty_actions
+ : non_empty_actions action { $1 @ [$2] }
+ | action { [$1] }
+ ;
+
+action
+ : METAVAR AFF arith_relation { Metavar_assign ($1, $3) }
+ ;
--
GitLab