let print ppf ?(sep="\n") l =
iter (fun t ->
let q, lab, f = Transition.node t in
- fprintf ppf "%a, %a -> %a%s" State.print q QNameSet.print lab Formula.print f sep) l
+ fprintf ppf "%a, %a → %a%s"
+ State.print q
+ QNameSet.print lab
+ Formula.print f sep) l
end
[]
in
let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) ->
- let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c))
+ let c = State.compare q2 q1 in if c == 0 then QNameSet.compare s2 s1 else c)
trs
in
let _ = _flush_str_fmt () in
- let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) ->
- let s1 = State.print _str_fmt q; _flush_str_fmt () in
- let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in
- let s3 = Formula.print _str_fmt f; _flush_str_fmt () in
- let pre = Pretty.length s1 + Pretty.length s2 in
- let all = Pretty.length s3 in
- ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
- ) ([], 0, 0) sorted_trs
+ let strs_strings, max_pre, max_all =
+ List.fold_left (fun (accl, accp, acca) (q, s, f) ->
+ let s1 = State.print _str_fmt q; _flush_str_fmt () in
+ let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in
+ let s3 = Formula.print _str_fmt f; _flush_str_fmt () in
+ let pre = Pretty.length s1 + Pretty.length s2 in
+ let all = Pretty.length s3 in
+ ( (q, s1, s2, s3) :: accl, max accp pre, max acca all)
+ ) ([], 0, 0) sorted_trs
in
let line = Pretty.line (max_all + max_pre + 6) in
let prev_q = ref State.dummy in
if !prev_q != q && !prev_q != State.dummy then fprintf fmt "%s@\n" line;
prev_q := q;
fprintf fmt "%s, %s" s1 s2;
- fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
+ fprintf fmt "%s"
+ (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2));
fprintf fmt " %s %s@\n" Pretty.right_arrow s3;
) strs_strings;
fprintf fmt "%s@\n" line
let rec flip b f =
match Formula.expr f with
Boolean.True | Boolean.False -> if b then f else Formula.not_ f
- | Boolean.Or(f1, f2) -> (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2)
- | Boolean.And(f1, f2) -> (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2)
+ | Boolean.Or(f1, f2) ->
+ (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2)
+ | Boolean.And(f1, f2) ->
+ (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2)
| Boolean.Atom(a, b') -> begin
match a.Atom.node with
| Move (m, q) ->
done;
let by_rank = Hashtbl.create 17 in
List.iter (fun (r,s) ->
- let r = r/2 in
let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in
Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list;
auto.ranked_states <-