Commit 7fcc03cc authored by Valentin Perrelle's avatar Valentin Perrelle Committed by Virgile Prevosto
Browse files

[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
parent 10121047
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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';
......
......@@ -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;
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
This diff is collapsed.
......@@ -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
......
......@@ -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 :
......
......@@ -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 :
......
......@@ -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 =
......
......@@ -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*)