projects
/
tatoo.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Refactor pretty printing of transitions and fix some depracated function uses.
[tatoo.git]
/
src
/
ata.ml
diff --git
a/src/ata.ml
b/src/ata.ml
index
190c4c7
..
c045aaf
100644
(file)
--- a/
src/ata.ml
+++ b/
src/ata.ml
@@
-184,32
+184,28
@@
module Transition =
type t = State.t * QNameSet.t * Formula.t
let equal (a, b, c) (d, e, f) =
a == d && b == e && c == f
type t = State.t * QNameSet.t * Formula.t
let equal (a, b, c) (d, e, f) =
a == d && b == e && c == f
- let hash (
a, b, c
) =
- HASHINT4 (PRIME1,
a
, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int))
+ let hash (
(a, b, c) : t
) =
+ HASHINT4 (PRIME1,
((a) :> int)
, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int))
end)
let print ppf t =
let q, l, f = t.node in
fprintf ppf "%a, %a %s %a"
State.print q
QNameSet.print l
end)
let print ppf t =
let q, l, f = t.node in
fprintf ppf "%a, %a %s %a"
State.print q
QNameSet.print l
- Pretty.
double_righ
t_arrow
+ Pretty.
lef
t_arrow
Formula.print f
end
module TransList : sig
include Hlist.S with type elt = Transition.t
Formula.print f
end
module TransList : sig
include Hlist.S with type elt = Transition.t
- val print :
Format.formatter -> ?sep:string
-> t -> unit
+ val print :
?sep:string -> Format.formatter
-> t -> unit
end =
struct
include Hlist.Make(Transition)
end =
struct
include Hlist.Make(Transition)
- let print
ppf ?(sep="\n")
l =
+ let print
?(sep="\n") ppf
l =
iter (fun t ->
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%s" Transition.print t sep) l
end
end
@@
-276,15
+272,15
@@
let print fmt a =
) ([], 0, 0) sorted_trs
in
let line = Pretty.line (max_all + max_pre + 6) in
) ([], 0, 0) sorted_trs
in
let line = Pretty.line (max_all + max_pre + 6) in
- let prev_q = ref State.dummy in
+ let prev_q = ref State.dummy
_state
in
fprintf fmt "%s@\n" line;
List.iter (fun (q, s1, s2, s3) ->
fprintf fmt "%s@\n" line;
List.iter (fun (q, s1, s2, s3) ->
- if !prev_q != q && !prev_q != State.dummy then fprintf fmt "%s@\n" line;
+ if !prev_q != q && !prev_q != State.dummy
_state
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));
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 %s@\n" Pretty.
righ
t_arrow s3;
+ fprintf fmt " %s %s@\n" Pretty.
lef
t_arrow s3;
) strs_strings;
fprintf fmt "%s@\n" line
) strs_strings;
fprintf fmt "%s@\n" line
@@
-387,7
+383,7
@@
let normalize_negations auto =
with
Not_found ->
(* create a new state and add it to the todo queue *)
with
Not_found ->
(* create a new state and add it to the todo queue *)
- let nq = State.
make
() in
+ let nq = State.
next
() in
auto.states <- StateSet.add nq auto.states;
Hashtbl.add memo_state (q, false) nq;
Queue.add (q, false) todo; nq
auto.states <- StateSet.add nq auto.states;
Hashtbl.add memo_state (q, false) nq;
Queue.add (q, false) todo; nq
@@
-409,7
+405,7
@@
let normalize_negations auto =
with
Not_found ->
let nq = if b then q else
with
Not_found ->
let nq = if b then q else
- let nq = State.
make
() in
+ let nq = State.
next
() in
auto.states <- StateSet.add nq auto.states;
nq
in
auto.states <- StateSet.add nq auto.states;
nq
in
@@
-597,7
+593,7
@@
let rename_states mapper a =
let copy a =
let mapper = Hashtbl.create MED_H_SIZE in
let () =
let copy a =
let mapper = Hashtbl.create MED_H_SIZE in
let () =
- StateSet.iter (fun q -> Hashtbl.add mapper q (State.
make
())) a.states
+ StateSet.iter (fun q -> Hashtbl.add mapper q (State.
next
())) a.states
in
rename_states mapper a
in
rename_states mapper a
@@
-657,7
+653,7
@@
let link a1 a2 q link_phi =
let union a1 a2 =
let a1 = copy a1 in
let a2 = copy a2 in
let union a1 a2 =
let a1 = copy a1 in
let a2 = copy a2 in
- let q = State.
make
() in
+ let q = State.
next
() in
let link_phi =
StateSet.fold
(fun q phi -> Formula.(or_ (stay q) phi))
let link_phi =
StateSet.fold
(fun q phi -> Formula.(or_ (stay q) phi))
@@
-669,7
+665,7
@@
let union a1 a2 =
let inter a1 a2 =
let a1 = copy a1 in
let a2 = copy a2 in
let inter a1 a2 =
let a1 = copy a1 in
let a2 = copy a2 in
- let q = State.
make
() in
+ let q = State.
next
() in
let link_phi =
StateSet.fold
(fun q phi -> Formula.(and_ (stay q) phi))
let link_phi =
StateSet.fold
(fun q phi -> Formula.(and_ (stay q) phi))
@@
-680,7
+676,7
@@
let inter a1 a2 =
let neg a =
let a = copy a in
let neg a =
let a = copy a in
- let q = State.
make
() in
+ let q = State.
next
() in
let link_phi =
StateSet.fold
(fun q phi -> Formula.(and_ (not_(stay q)) phi))
let link_phi =
StateSet.fold
(fun q phi -> Formula.(and_ (not_(stay q)) phi))