-
Notifications
You must be signed in to change notification settings - Fork 0
/
astar.req
81 lines (66 loc) · 3.51 KB
/
astar.req
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
# problem ::= Problem(initialstate, statespace)
# assume operators:
# goaltest(?space, ?state) -> True or False
# actions(?space, ?state) -> List of Actions
# result(?space, ?state, ?action) -> State
# path ::= EmptyPath(startstate) | PathNode(finalstate, finalaction, parent)
# define an accessor:
last(EmptyPath(?startstate)) == ?startstate
last(PathNode(?finalstate, ?finalaction, ?parent)) == ?finalstate
# assume a smart constructor, add:
# add(priority queue, path)
# assume dumb destructors
# priorityqueue ::= EmptyPQueue | PQueue(shortest path, rest of frontier)
treesearchStart(Problem(?init, ?s)) == treesearchMaybeFail(add(EmptyPQueue, EmptyPath(?init)), ?s)
treesearchMaybeFail(EmptyPQueue, ?s) == Fail
treesearchMaybeFail(PQueue(?p, ?f), ?s) == treesearchMaybeFound(goaltest(?s, last(?p)), ?p, ?f, ?s)
treesearchMaybeFound(True, ?p, ?f, ?s) == Found(?p)
treesearchMaybeFound(False, ?p, ?f, ?s) == treesearchExpand(actions(?s, last(?p)), ?p, ?f, ?s)
treesearchExpand(Nil, ?p, ?f, ?s) == treesearchMaybeFail(?f, ?s)
treesearchExpand(Cons(?a, ?as), ?p, ?f, ?s) ==
treesearchExpand(?as, ?p, add(?f, PathNode(result(?s, last(?p), ?a), ?a, ?p)), ?s)
# for graphsearch, we need a set data structure for the explored set
# we assume there's an "in" accessor, for both the frontier and the explored
graphsearchStart(Problem(?init, ?s)) ==
graphsearchMaybeFail(add(EmptyPQueue, EmptyPath(?init)), EmptySet, ?s)
graphsearchMaybeFail(EmptyPQueue, ?e, ?s) ==
Fail
graphsearchMaybeFail(PQueue(?p, ?f), ?e, ?s) ==
graphsearchMaybeFound(goaltest(?s, last(?p)), ?p, ?f, ?e, ?s)
graphsearchMaybeFound(True, ?p, ?f, ?e, ?s) ==
Found(?p)
graphsearchMaybeFound(False, ?p, ?f, ?e, ?s) ==
graphsearchMaybeExpand(or(in(?f, last(?p)), in(?e, last(?p))), ?p, ?f, ?e, ?s)
graphsearchMaybeExpand(True, ?p, ?f, ?e, ?s) ==
graphsearchMaybeFail(?f, ?e, ?s) # already either scheduled or explored
graphsearchMaybeExpand(False, ?p, ?f, ?e, ?s) ==
graphsearchExpand(actions(?s, last(?p)), ?p, ?f, ?e, ?s)
graphsearchExpand(Nil, ?p, ?f, ?e, ?s) ==
graphsearchMaybeFail(?f, add(?e, ?p), ?s)
graphsearchExpand(Cons(?a, ?as), ?p, ?f, ?e, ?s) ==
graphsearchExpand(?as, ?p, add(?f, PathNode(result(?s, last(?p), ?a), ?a, ?p)), ?e, ?s)
# this is all very well, but we need some actual data structures,
# and actual spaces to search.
SussmanAnomaly := Problem(Cons(On(C, A), Cons(On(A, Table), Cons(On(B, Table), Cons(Clear(C), Cons(Clear(B), Cons(Clear(Table), Nil)))))), UcBlocksWorld)
# goaltest(?space, ?state) -> True or False
goaltest(UcBlocksWorld, ?state) == and(member(?state, On(B, C)), member(?state, On(A, B)))
# actions(?space, ?state) -> List of Actions
actions(UcBlocksWorld, ?state)
# Puton(?x, ?y, ?z) is an action if they are all different, ?x is on ?z, and both ?x and ?y are clear
clears(Nil) == Nil
clears(Cons(On(?o1, ?o2), ?rest)) == clears(?rest)
clears(Cons(Clear(?o), ?rest)) == Cons(?o, clears(?rest))
crossproduct(?xs, ?ys) == crossproductHelper(?xs, mapToSingleton(?ys))
crossproductHelper(Nil, ?ys) == mapToSingleton(?ys)
crossproductHelper(Cons(?x, Nil), ?ys) == mapCons(?ys, ?x)
crossproductHelper(Cons(?x, Cons(?xs1, ?xss)), ?ys) ==
mapToSingleton(Nil) == Nil
mapToSingleton(Cons(?x, ?xs)) == Cons(Cons(?x, Nil), mapToSingleton(?xs))
mapCons(Nil, ?x) == Nil
mapCons(Cons(?y, ?ys), ?x) == Cons(Cons(?y, ?x), mapCons(?ys, ?x))
allpossibles := crossproduct(abc, crossproduct(abc,
Triple(
# result(?space, ?state, ?action) -> State
result(UcBlocksWorld, ?state)
# problem ::= Problem(initialstate, statespace)
# assume operators: