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
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
#script(lua)
-- VARIABLES --
parts = {}
-- indicate solving approaches or grounding instructions, respectively
debugs = true -- false
debugg = false -- true
-- maximum time stamp for solving approaches
limit = math.huge
-- smallest and current time stamp
iinit = 0
time = 0
-- sequence number for blocks
block = 0
-- FUNCTIONS --
-- integrate a block appearing at time stamp "init"
function addblock(init)
if limit < init then time = init end
if limit < time then return end
if init < iinit then
for t = init+1, iinit do
if debugg then print("Ground: table("..t..")") end
parts[#parts+1] = {"table", {t}}
for k = 1, block do
if debugg then print("Ground: move("..k..","..t..")") end
parts[#parts+1] = {"move", {k, t}}
end
end
iinit = init
end
rollout(init)
block = block+1
if debugg then print("Ground: base_"..block) end
parts[#parts+1] = {"base_"..block, {}}
if debugg then print("Ground: init("..block..","..init..")") end
parts[#parts+1] = {"init", {block, init}}
if debugg then print("Ground: state("..block..","..init..")") end
parts[#parts+1] = {"state", {block, init}}
for t = iinit+1, time do
if debugg then print("Ground: move("..block..","..t..")") end
parts[#parts+1] = {"move", {block, t}}
if init < t then
if debugg then print("Ground: state("..block..","..t..")") end
parts[#parts+1] = {"state", {block, t}}
end
end
end
-- ground encoding parts beyond current time stamp up to "next"
function rollout(next)
if limit < next then
time = next
return
end
if time < next then
time = time+1
if debugg then print("Ground: table("..time..")") end
parts[#parts+1] = {"table", {time}}
for k = 1, block do
if debugg then print("Ground: state("..k..","..time..")") end
parts[#parts+1] = {"state", {k, time}}
if debugg then print("Ground: move("..k..","..time..")") end
parts[#parts+1] = {"move", {k, time}}
end
rollout(next)
end
end
-- incrementally solve and ground for increasing time stamps until a plan exists
function incsolve()
if limit < time then return end
if debugs then
print("=============")
print("TIME "..time)
end
prg:ground(parts)
parts = {}
ret = prg:solve()
if debugs then
if ret == gringo.SolveResult.SAT then print "SATISFIABLE"
elseif ret == gringo.SolveResult.UNSAT then print "UNSATISFIABLE"
elseif ret == gringo.SolveResult.UNKNOWN then print "UNKNOWN"
end
print("=============")
end
if ret == gringo.SolveResult.UNSAT then
rollout(time+1)
incsolve()
end
end
-- AUXILIARY FUNCTIONS --
function setdebugg(debug)
debugg = debug
end
function setdebugs(debug)
debugs = debug
end
function setdebug(debug)
debugg = debug
debugs = debug
end
function setlimit(custom)
limit = custom
end
function setiinit(custom)
iinit = custom
time = iinit
end
#end.
|
