Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
M
menhir
Project
Project
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
10
Issues
10
List
Boards
Labels
Milestones
Merge Requests
2
Merge Requests
2
CI / CD
CI / CD
Pipelines
Jobs
Schedules
Charts
Packages
Packages
Container Registry
Wiki
Wiki
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Jobs
Commits
Issue Boards
Open sidebar
POTTIER Francois
menhir
Commits
5eb576e7
Commit
5eb576e7
authored
Jul 06, 2015
by
POTTIER Francois
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Some work to bring [Dijstra] and A* closer to one another.
parent
822ce6f6
Changes
4
Hide whitespace changes
Inline
Sidebyside
Showing
4 changed files
with
102 additions
and
105 deletions
+102
105
Coverage.ml
src/Coverage.ml
+18
2
astar.ml
src/astar.ml
+76
93
astar.mli
src/astar.mli
+5
7
dijkstra.ml
src/dijkstra.ml
+3
3
No files found.
src/Coverage.ml
View file @
5eb576e7
...
...
@@ 52,7 +52,7 @@ module ForwardAutomaton = struct
(* The sources are the entry states. *)
ProductionMap
.
iter
(
fun
_
s
>
f
s
)
Lr1
.
entry
let
successors
edge
s
=
let
successors
s
edge
=
SymbolMap
.
iter
(
fun
sym
s'
>
(* The weight of the edge from [s] to [s'] is given by the function
[Grammar.Analysis.minimal_symbol]. *)
...
...
@@ 65,6 +65,22 @@ let approximate : Lr1.node > int =
let
module
D
=
Dijkstra
.
Make
(
ForwardAutomaton
)
in
D
.
search
(
fun
(
_
,
_
,
_
)
>
()
)
let
approx
:
Lr1
.
node
>
int
=
let
module
A
=
Astar
.
Make
(
struct
include
ForwardAutomaton
let
estimate
_
=
0
type
node
=
vertex
end
)
in
let
distance
,
_
=
A
.
search
(
fun
(
_
,
_
)
>
()
)
in
distance
(* Debugging. TEMPORARY *)
let
approximate
s
=
let
d1
=
approximate
s
and
d2
=
approx
s
in
assert
(
d1
=
d2
);
d1
(* Test. TEMPORARY *)
let
()
=
...
...
@@ 390,7 +406,7 @@ let backward (s', z) : P.property =
(* Backward search from the single source [s', z]. *)
let
sources
f
=
f
(
s'
,
z
)
let
successors
edge
(
s'
,
z
)
=
let
successors
(
s'
,
z
)
edge
=
match
Lr1
.
incoming_symbol
s'
with

None
>
(* An entry state has no predecessor states. *)
...
...
src/astar.ml
View file @
5eb576e7
...
...
@@ 41,9 +41,6 @@ module Make (G : sig
val
sources
:
(
node
>
unit
)
>
unit
(* Whether a node is a goal node. *)
val
is_goal
:
node
>
bool
(* [successors n f] presents each of [n]'s successors, in
an arbitrary order, to [f], together with the cost of
the edge that was followed. *)
...
...
@@ 59,24 +56,24 @@ end) = struct
type
cost
=
int
type
priority
=
cost
(* Nodes with low priorities are dealt with first. *)
(* Nodes with low priorities are dealt with first. *)
type
priority
=
cost
type
inode
=
{
this
:
G
.
node
;
(* Graph node associated with this internal record. *)
mutable
cost
:
cost
;
(* Cost of the best known path from a source node to this node. (ghat) *)
estimate
:
cost
;
(* Estimated cost of the best path from this node to a goal node. (hhat) *)
mutable
father
:
inode
;
(* Last node on the best known path from a source node to this node. *)
mutable
prev
:
inode
;
(* Previous node on doubly linked priority list *)
mutable
next
:
inode
;
(* Next node on doubly linked priority list *)
mutable
priority
:
priority
;
(* The node's priority, if the node is in the queue; 1 otherwise *)
(* Graph node associated with this internal record. *)
this
:
G
.
node
;
(* Cost of the best known path from a source node to this node. (ghat) *)
mutable
cost
:
cost
;
(* Estimated cost of the best path from this node to a goal node. (hhat) *)
estimate
:
cost
;
(* Best known path from a source node to this node. *)
mutable
path
:
G
.
label
list
;
(* Previous node on doubly linked priority list *)
mutable
prev
:
inode
;
(* Next node on doubly linked priority list *)
mutable
next
:
inode
;
(* The node's priority, if the node is in the queue; 1 otherwise *)
mutable
priority
:
priority
;
}
(* This auxiliary module maintains a mapping of graph nodes
...
...
@@ 120,9 +117,8 @@ end) = struct
can only decrease. *)
val
add_or_decrease
:
inode
>
priority
>
unit
(* Retrieve a node with lowest priority of the queue.
Raises [Not_found] if the queue is empty. *)
val
get
:
unit
>
inode
(* Retrieve a node with lowest priority of the queue. *)
val
get
:
unit
>
inode
option
end
=
struct
...
...
@@ 167,18 +163,18 @@ end) = struct
let
get
()
=
if
!
best
=
max
then
raise
Not_found
(* queue is empty *)
None
else
match
a
.
(
!
best
)
with

None
>
assert
false

Some
inode
>

Some
inode
as
result
>
remove
inode
;
(* look for next nonempty bucket *)
while
(
!
best
<
max
)
&&
(
a
.
(
!
best
)
=
None
)
do
incr
best
done
;
inode
result
let
add_or_decrease
inode
priority
=
if
inode
.
priority
>=
0
then
...
...
@@ 195,7 +191,7 @@ end) = struct
this
=
node
;
cost
=
0
;
estimate
=
G
.
estimate
node
;
father
=
inode
;
path
=
[]
;
prev
=
inode
;
next
=
inode
;
priority
=

1
...
...
@@ 207,91 +203,78 @@ end) = struct
let
expanded
=
ref
0
(* Search. *)
let
rec
search
()
=
(* Pick the open node that currently has lowest fhat, (* TEMPORARY resolve ties in favor of goal nodes *)
that is, lowest estimated distance to a goal node. *)
(* Access to the search results (after the search is over). *)
let
inode
=
P
.
get
()
in
(* may raise Not_found; then, no goal node is reachable *)
let
node
=
inode
.
this
in
let
distance
node
=
try
(
M
.
get
node
)
.
cost
with
Not_found
>
max_int
(* If it is a goal node, we are done. *)
if
G
.
is_goal
node
then
inode
else
begin
let
path
node
=
(
M
.
get
node
)
.
path
(* let [Not_found] escape if no path was found *)
(* Monitoring. *)
incr
expanded
;
(* Otherwise, examine its successors. *)
G
.
successors
node
(
fun
_
edge_cost
son
>
(* Determine the cost of the best known path from the
start node, through this node, to this son. *)
let
new_cost
=
inode
.
cost
+
edge_cost
in
(* Search. *)
try
let
ison
=
M
.
get
son
in
if
new_cost
<
ison
.
cost
then
begin
let
rec
search
f
=
(* This son has been visited before, but this new
path to it is shorter. If it was already open
and waiting in the priority queue, increase its
priority; otherwise, mark it as open and insert
it into the queue. *)
(* Pick the open node that currently has lowest fhat,
that is, lowest estimated distance to a goal node. *)
let
new_fhat
=
new_cost
+
ison
.
estimate
in
P
.
add_or_decrease
ison
new_fhat
;
ison
.
cost
<
new_cost
;
ison
.
father
<
inode
match
P
.
get
()
with

None
>
(* Finished. *)
distance
,
path
end
with
Not_found
>

Some
inode
>
let
node
=
inode
.
this
in
(* This son was never visited before. Allocate a new
status record for it and mark it as open. *)
(* Let the user know about this newly discovered node. *)
f
(
node
,
inode
.
path
);
let
e
=
G
.
estimate
son
in
let
rec
ison
=
{
this
=
son
;
cost
=
new_cost
;
estimate
=
e
;
father
=
inode
;
prev
=
ison
;
next
=
ison
;
priority
=

1
}
in
M
.
add
son
ison
;
P
.
add
ison
(
new_cost
+
e
)
(* Monitoring. *)
incr
expanded
;
);
(* Otherwise, examine its successors. *)
G
.
successors
node
(
fun
label
edge_cost
son
>
search
()
(* Determine the cost of the best known path from the
start node, through this node, to this son. *)
let
new_cost
=
inode
.
cost
+
edge_cost
in
end
try
let
ison
=
M
.
get
son
in
if
new_cost
<
ison
.
cost
then
begin
(* Main function. *)
(* This son has been visited before, but this new
path to it is shorter. If it was already open
and waiting in the priority queue, increase its
priority; otherwise, mark it as open and insert
it into the queue. *)
let
path
()
=
let
new_fhat
=
new_cost
+
ison
.
estimate
in
P
.
add_or_decrease
ison
new_fhat
;
ison
.
cost
<
new_cost
;
ison
.
path
<
label
::
inode
.
path
(* Find the nearest goal node. *)
end
with
Not_found
>
let
goal
=
search
()
in
(* This son was never visited before. Allocate a new
status record for it and mark it as open. *)
(* Build the shortest path back to the start node. *)
let
e
=
G
.
estimate
son
in
let
rec
ison
=
{
this
=
son
;
cost
=
new_cost
;
estimate
=
e
;
path
=
label
::
inode
.
path
;
prev
=
ison
;
next
=
ison
;
priority
=

1
}
in
M
.
add
son
ison
;
P
.
add
ison
(
new_cost
+
e
)
let
rec
build
path
inode
=
let
path
=
inode
.
this
::
path
in
let
father
=
inode
.
father
in
if
father
==
inode
then
path
else
build
path
father
);
in
let
path
=
build
[]
goal
in
path
search
f
end
src/astar.mli
View file @
5eb576e7
...
...
@@ 23,9 +23,6 @@ module Make (G : sig
the edge that was followed. *)
val
successors
:
node
>
(
label
>
int
>
node
>
unit
)
>
unit
(* Whether a node is a goal node. *)
val
is_goal
:
node
>
bool
(* An estimate of the cost of the shortest path from the
supplied node to some goal node. This estimate must
be a correct underapproximation of the actual cost. *)
...
...
@@ 33,9 +30,10 @@ module Make (G : sig
end
)
:
sig
(* This function produces a shortest path from the start
node to some goal node. It raises [Not_found] if no
such path exists. *)
val
path
:
unit
>
G
.
node
list
(* Search. Newly discovered nodes are presented to the user, in order of
increasing distance from the source nodes, by invoking the usersupplied
function [f]. At the end, a mapping of nodes to distances to the source
nodes and a mapping of nodes to shortest paths are returned. *)
val
search
:
(
G
.
node
*
G
.
label
list
>
unit
)
>
(
G
.
node
>
int
)
*
(
G
.
node
>
G
.
label
list
)
end
src/dijkstra.ml
View file @
5eb576e7
...
...
@@ 18,7 +18,7 @@ module Make (G : sig
(* The weighted outgoing edges of a vertex. *)
val
successors
:
(
label
>
int
>
vertex
>
unit
)
>
vertex
>
unit
val
successors
:
vertex
>
(
label
>
int
>
vertex
>
unit
)
>
unit
end
)
=
struct
open
G
...
...
@@ 67,14 +67,14 @@ end) = struct
(* Let the client know about it. *)
f
(
w
,
v
,
p
);
(* Examine its outgoing edges. *)
successors
(
fun
label
weight
v'
>
successors
v
(
fun
label
weight
v'
>
let
w'
=
weight
+
w
in
if
w'
<
distance
v'
then
begin
assert
(
not
(
H
.
mem
fixed
v'
));
H
.
replace
dist
v'
w'
;
PQ
.
add
queue
(
w'
,
v'
,
label
::
p
)
end
)
v
)
end
done
;
distance
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment