Post by Lars Ericson on Aug 1, 2015 16:56:41 GMT -8
Re: s translation of B&L to ASP Clingo LP version 4.5.1 as described here: tcpdiag.dl.sourceforge.net/project/potassco/guide/2.0/guide-2.0.pdf.
I wrote a Python program, following the guide in mrg's book Chapter 15, to translate GDL to LP for BL. The rules of BL are:
;;; Components
(role robot)
(base p)
(base q)
(base r)
(base 1)
(base 2)
(base 3)
(base 4)
(base 5)
(base 6)
(base 7)
(input robot a)
(input robot b)
(input robot c)
;;; init
(init 1)
;;; legal
(legal robot a)
(legal robot b)
(legal robot c)
;;; next
(<= (next p) (does robot a) (not (true p)))
(<= (next p) (does robot b) (true q))
(<= (next p) (does robot c) (true p))
(<= (next q) (does robot a) (true q))
(<= (next q) (does robot b) (true p))
(<= (next q) (does robot c) (true r))
(<= (next r) (does robot a) (true r))
(<= (next r) (does robot b) (true r))
(<= (next r) (does robot c) (true q))
(<= (next ?y) (true ?x) (successor ?x ?y))
;;; goal
(<= (goal robot 100) (true p) (true q) (true r))
(<= (goal robot 0) (not (true p)))
(<= (goal robot 0) (not (true q)))
(<= (goal robot 0) (not (true r)))
;;; terminal
(<= terminal (true p) (true q) (true r))
(<= terminal (true 7))
;;; Data
(successor 1 2)
(successor 2 3)
(successor 3 4)
(successor 4 5)
(successor 5 6)
(successor 6 7)
From the suggestions in Chapter 15, this translates to LP as follows (this is stored in file bl_robot.lp):
role(robot).
base(p).
base(q).
base(r).
base(1).
base(2).
base(3).
base(4).
base(5).
base(6).
base(7).
input(robot,a).
input(robot,b).
input(robot,c).
true(1,1).
legal(robot,a,T) :- time(T), not terminal(T).
input(robot,a).
legal(robot,b,T) :- time(T), not terminal(T).
input(robot,b).
legal(robot,c,T) :- time(T), not terminal(T).
input(robot,c).
true(p,T+1) :- time(T), does(robot,a,T), not true(p,T).
true(p,T+1) :- time(T), does(robot,b,T), true(q,T).
true(p,T+1) :- time(T), does(robot,c,T), true(p,T).
true(q,T+1) :- time(T), does(robot,a,T), true(q,T).
true(q,T+1) :- time(T), does(robot,b,T), true(p,T).
true(q,T+1) :- time(T), does(robot,c,T), true(r,T).
true(r,T+1) :- time(T), does(robot,a,T), true(r,T).
true(r,T+1) :- time(T), does(robot,b,T), true(r,T).
true(r,T+1) :- time(T), does(robot,c,T), true(q,T).
true(Y,T+1) :- time(T), true(X,T), successor(X,Y).
goal(robot,100,T) :- time(T), true(p,T), true(q,T), true(r,T).
goal(robot,0,T) :- time(T), not true(p,T).
goal(robot,0,T) :- time(T), not true(q,T).
goal(robot,0,T) :- time(T), not true(r,T).
terminal(T) :- time(T), true(p,T), true(q,T), true(r,T).
terminal(T) :- time(T), true(7,T).
successor(1,2).
successor(2,3).
successor(3,4).
successor(4,5).
successor(5,6).
successor(6,7).
:- does(R,M,T), not legal(R,M,T).
:- 0{ terminal(T) : time(T) }0.
:- terminal(T), role(robot), not goal(robot,100,T).
time(1..7).
1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T).
As-is, Clingo 4.5.1 thinks this is unsatisfiable:
clingo version 4.5.1
Reading from bl_robot.lp
Solving...
UNSATISFIABLE
Models : 0
Calls : 1
Time : 0.016s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.016s
However, there is a solution, namely the one in which robot does a,b,c,a,b,a on steps 1 through 6 leading to a terminal state with goal value 100 on step 7:
does(robot,a,1).
does(robot,b,2).
does(robot,c,3).
does(robot,a,4).
does(robot,b,5).
does(robot,a,6).
The purpose of constraint 1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T) is to make sure that only one move is played at a time by robot. The development of this constraint in Chapter 15 is as follows:
1. Start with (where by "," I assume I am getting AND in this case; this may be a basic problem):
does(robot,a,T) :- time(T), not does(robot,b,T), not does(robot,c,T).
does(robot,b,T) :- time(T), not does(robot,a,T), not does(robot,c,T).
does(robot,c,T) :- time(T), not does(robot,a,T), not does(robot,b,T).
2. This reduces to
1{ does(robot,a,T); does(robot,b,T); does(robot,c,T) }1 :- time(T).
3. This reduces to
1{ does(robot,M,T) : input(robot,M) }1 :- time(T).
4. This reduces to
1{ does(R,M,T) : input(R,M) }1 :- role(R) , time(T).
It turns out this is unsatisfiable, but it can be fixed. If we replace form (4) with form (3), doesn't work. Replace (3) by (2), doesn't work. Replace (2) by (1), doesn't work. Next step is to replace 1 by this (call it 0):
does(robot,a,1) :- time(1), not does(robot,b,1), not does(robot,c,1).
does(robot,b,1) :- time(1), not does(robot,a,1), not does(robot,c,1).
does(robot,c,1) :- time(1), not does(robot,a,1), not does(robot,b,1).
does(robot,a,2) :- time(2), not does(robot,b,2), not does(robot,c,2).
does(robot,b,2) :- time(2), not does(robot,a,2), not does(robot,c,2).
does(robot,c,2) :- time(2), not does(robot,a,2), not does(robot,b,2).
does(robot,a,3) :- time(3), not does(robot,b,3), not does(robot,c,3).
does(robot,b,3) :- time(3), not does(robot,a,3), not does(robot,c,3).
does(robot,c,3) :- time(3), not does(robot,a,3), not does(robot,b,3).
does(robot,a,4) :- time(4), not does(robot,b,4), not does(robot,c,4).
does(robot,b,4) :- time(4), not does(robot,a,4), not does(robot,c,4).
does(robot,c,4) :- time(4), not does(robot,a,4), not does(robot,b,4).
does(robot,a,5) :- time(5), not does(robot,b,5), not does(robot,c,5).
does(robot,b,5) :- time(5), not does(robot,a,5), not does(robot,c,5).
does(robot,c,5) :- time(5), not does(robot,a,5), not does(robot,b,5).
does(robot,a,6) :- time(6), not does(robot,b,6), not does(robot,c,6).
does(robot,b,6) :- time(6), not does(robot,a,6), not does(robot,c,6).
does(robot,c,6) :- time(6), not does(robot,a,6), not does(robot,b,6).
At this point, a solution pops out, and it is the expected one, and it has one move per step:
c:\Users\Lars\Desktop\randori\thirdparty\clingo-4.5.1-win64>clingo bl_robot.lp
clingo version 4.5.1
Reading from bl_robot.lp
Solving...
Answer: 1
role(robot) base(p) base(q) base(r) base(1) base(2) base(3) base(4) base(5) base(6) base(7) input(robot,a) input(robot,b) input(robot,c) true(1,1) successor(1,2) successor(2,3) successor(3,4) successor(4,5) successor(5,6) successor(6,7) time(1) time(2) time(3) time(4) time(5) time(6) time(7) does(robot,a,1) does(robot,b,2) does(robot,c,3) does(robot,a,4) does(robot,b,5) does(robot,a,6) true(p,2) true(p,5) true(p,7) true(2,2) true(q,3) true(q,6) true(q,7) true(3,3) true(r,4) true(r,5) true(r,6) true(r,7) true(4,4) true(5,5) true(6,6) true(7,7) terminal(7) legal(robot,a,1) legal(robot,a,2) legal(robot,a,3) legal(robot,a,4) legal(robot,a,5) legal(robot,a,6) legal(robot,b,1) legal(robot,b,2) legal(robot,b,3) legal(robot,b,4) legal(robot,b,5) legal(robot,b,6) legal(robot,c,1) legal(robot,c,2) legal(robot,c,3) legal(robot,c,4) legal(robot,c,5) legal(robot,c,6) goal(robot,100,7) goal(robot,0,1) goal(robot,0,2) goal(robot,0,3) goal(robot,0,4) goal(robot,0,5) goal(robot,0,6)
SATISFIABLE
Models : 1+
Calls : 1
Time : 0.006s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.000s
Note that we are not adding
does(robot,c,7) :- time(7), not does(robot,a,7), not does(robot,b,7).
does(robot,a,7) :- time(7), not does(robot,c,7), not does(robot,b,7).
does(robot,b,7) :- time(7), not does(robot,c,7), not does(robot,a,7).
It turns out that if you add this, then the above becomes unsatisfiable again.
So this is a clue, that 1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T). needs to be restricted to 1<=T<=6.
So let's try that:
1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T), 1 <= T, T <= 6.
And it works! It gaves the same solution above. The original form is unsatisfiable if it's scope includes the final time step, because in the final time step, there is no move. To recap, the final, working version of bl_robot.lp is:
role(robot).
base(p).
base(q).
base(r).
base(1).
base(2).
base(3).
base(4).
base(5).
base(6).
base(7).
input(robot,a).
input(robot,b).
input(robot,c).
true(1,1).
legal(robot,a,T) :- time(T), not terminal(T).
input(robot,a).
legal(robot,b,T) :- time(T), not terminal(T).
input(robot,b).
legal(robot,c,T) :- time(T), not terminal(T).
input(robot,c).
true(p,T+1) :- time(T), does(robot,a,T), not true(p,T).
true(p,T+1) :- time(T), does(robot,b,T), true(q,T).
true(p,T+1) :- time(T), does(robot,c,T), true(p,T).
true(q,T+1) :- time(T), does(robot,a,T), true(q,T).
true(q,T+1) :- time(T), does(robot,b,T), true(p,T).
true(q,T+1) :- time(T), does(robot,c,T), true(r,T).
true(r,T+1) :- time(T), does(robot,a,T), true(r,T).
true(r,T+1) :- time(T), does(robot,b,T), true(r,T).
true(r,T+1) :- time(T), does(robot,c,T), true(q,T).
true(Y,T+1) :- time(T), true(X,T), successor(X,Y).
goal(robot,100,T) :- time(T), true(p,T), true(q,T), true(r,T).
goal(robot,0,T) :- time(T), not true(p,T).
goal(robot,0,T) :- time(T), not true(q,T).
goal(robot,0,T) :- time(T), not true(r,T).
terminal(T) :- time(T), true(p,T), true(q,T), true(r,T).
terminal(T) :- time(T), true(7,T).
successor(1,2).
successor(2,3).
successor(3,4).
successor(4,5).
successor(5,6).
successor(6,7).
:- does(R,M,T), not legal(R,M,T).
:- 0{ terminal(T) : time(T) }0.
:- terminal(T), role(robot), not goal(robot,100,T).
time(1..7).
1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T), 1 <= T, T <= 6.
We generate this from the original bl.kif file with the following Python code:
from __future__ import division
import sys
### First a LISP parser copied off the Internet from Peter Norvig: ###
Symbol = str # A Lisp Symbol is implemented as a Python str
List = list # A Lisp List is implemented as a Python list
Number = (int, float) # A Lisp Number is implemented as a Python int or float
def parse(program):
"Read a Scheme expression from a string."
return read_from_tokens(tokenize(program))
def tokenize(s):
"Convert a string into a list of tokens."
return s.replace('(',' ( ').replace(')',' ) ').split()
def atom(token):
"Numbers become numbers; every other token is a symbol."
try:
return int(token)
except ValueError:
try:
return float(token)
except ValueError:
return Symbol(token)
def read_from_tokens(tokens):
"Read an expression from a sequence of tokens."
if len(tokens) == 0:
raise SyntaxError('unexpected EOF while reading')
token = tokens.pop(0)
if '(' == token:
L = []
while tokens[0] != ')':
L.append(read_from_tokens(tokens))
tokens.pop(0) # pop off ')'
return L
elif ')' == token:
raise SyntaxError('unexpected )')
else:
return atom(token)
### End LISP parser ###
def parse_file(kf):
with open (kf, "r") as myfile:
lisp = myfile.readlines()
program = '('+''.join([x for x in lisp if x[0] != ';']).replace('\n', '')+')'
gdl = parse(program)
return gdl
def rewrite_init(s):
[init,F]=s
return ['true',F,1]
def rewrite_next(s):
[nxt,F]=s
return ['true',F,['plus','T',1]]
def rewrite_does(s):
return ['does']+s[1:]+['T']
def rewrite_not(s):
return ['not', rewriter(s[1])]
def is_input_base(s):
try:
return s[0] in ['base', 'input']
except:
return False
def rewrite_rule(s):
time = [] if is_input_base(s[1]) else [['time', 'T']]
return ['<=']+[rewriter(s[1])]+time+[rewriter(t) for t in s[2:]]
roles = []
goals = {}
actions = {}
has_input = False
def rewrite_timed_atom(s):
global goals, has_input
if s[0] == 'input':
has_input = True
role = s[1]
action = s[2]
actions[role].add(action)
elif s[0] == 'goal':
[g,role,level]=s
if role in goals:
goals[role] = max(goals[role], level)
else:
goals[role]=level
return s+['T']
def rewriter(s):
global roles, actions
if type(s)==type('a'):
return [s, 'T']
head = s[0]
if head in ['index', 'successor']:
return s
elif head == 'init':
return rewrite_init(s)
elif head == 'next':
return rewrite_next(s)
elif head == 'not':
return rewrite_not(s)
elif head == 'does':
return rewrite_does(s)
elif head in ['role', 'base', 'input']:
if head == 'role':
role = s[1]
roles.append(role)
if role not in actions:
actions[role] = set()
elif head == 'input':
role = s[1]
action = s[2]
actions[role].add(action)
return s
elif head == '<=':
return rewrite_rule(s)
else:
return rewrite_timed_atom(s)
def rewriter_top(s):
if type(s)==type('a'):
return [s, 'T']
head = s[0]
if head == 'input':
role = s[1]
action = s[2]
actions[role].add(action)
return s
elif head in ['legal', 'input']:
return ['<=', s+['T'], ['time', 'T'], ['not', ['terminal', 'T']]]
else:
return rewriter(s)
def expand_legal(gdl):
global has_input
R = []
for x in gdl:
if x[0] == 'legal':
R.extend([x, ['input']+x[1:]])
has_input = True
else:
R.append(x)
return R
def rewrite(gdl):
gdl = expand_legal(gdl)
return [rewriter_top(rule) for rule in gdl]
def aspy(s):
if type(s) == type([]):
try:
if s[0] == '<=':
return aspy(s[1])+' :- '+', '.join([aspy(x) for x in s[2:]])
elif s[0] == 'plus':
return aspy(s[1])+'+'+aspy(s[2])
elif s[0] == 'not':
return 'not '+aspy(s[1])
else:
return s[0]+'('+','.join([aspy(x) for x in s[1:]])+')'
except:
return s[0]
elif type(s)==type('a') and s[0] == '?':
return s[1:].upper()
else:
return str(s)
if __name__ == '__main__':
root = sys.argv[1]
steps = int(sys.argv[2])
role = sys.argv[3]
kf = root + '.kif'
lf = root + '_' + role + '.lp'
gdl = parse_file(kf)
gdlplus = rewrite(gdl)
with open(lf, 'w') as f:
for x in gdlplus:
f.write(aspy(x)+'.\n')
f.write(':- does(R,M,T), not legal(R,M,T).\n')
f.write(':- 0{ terminal(T) : time(T) }0.\n')
f.write(':- terminal(T), role(%s), not goal(%s,%d,T).\n' % (role, role, goals[role]))
f.write('time(1..%d).\n' % steps)
f.write('1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T), 1 <= T, T <= %d.\n' % (steps-1))
I wrote a Python program, following the guide in mrg's book Chapter 15, to translate GDL to LP for BL. The rules of BL are:
;;; Components
(role robot)
(base p)
(base q)
(base r)
(base 1)
(base 2)
(base 3)
(base 4)
(base 5)
(base 6)
(base 7)
(input robot a)
(input robot b)
(input robot c)
;;; init
(init 1)
;;; legal
(legal robot a)
(legal robot b)
(legal robot c)
;;; next
(<= (next p) (does robot a) (not (true p)))
(<= (next p) (does robot b) (true q))
(<= (next p) (does robot c) (true p))
(<= (next q) (does robot a) (true q))
(<= (next q) (does robot b) (true p))
(<= (next q) (does robot c) (true r))
(<= (next r) (does robot a) (true r))
(<= (next r) (does robot b) (true r))
(<= (next r) (does robot c) (true q))
(<= (next ?y) (true ?x) (successor ?x ?y))
;;; goal
(<= (goal robot 100) (true p) (true q) (true r))
(<= (goal robot 0) (not (true p)))
(<= (goal robot 0) (not (true q)))
(<= (goal robot 0) (not (true r)))
;;; terminal
(<= terminal (true p) (true q) (true r))
(<= terminal (true 7))
;;; Data
(successor 1 2)
(successor 2 3)
(successor 3 4)
(successor 4 5)
(successor 5 6)
(successor 6 7)
From the suggestions in Chapter 15, this translates to LP as follows (this is stored in file bl_robot.lp):
role(robot).
base(p).
base(q).
base(r).
base(1).
base(2).
base(3).
base(4).
base(5).
base(6).
base(7).
input(robot,a).
input(robot,b).
input(robot,c).
true(1,1).
legal(robot,a,T) :- time(T), not terminal(T).
input(robot,a).
legal(robot,b,T) :- time(T), not terminal(T).
input(robot,b).
legal(robot,c,T) :- time(T), not terminal(T).
input(robot,c).
true(p,T+1) :- time(T), does(robot,a,T), not true(p,T).
true(p,T+1) :- time(T), does(robot,b,T), true(q,T).
true(p,T+1) :- time(T), does(robot,c,T), true(p,T).
true(q,T+1) :- time(T), does(robot,a,T), true(q,T).
true(q,T+1) :- time(T), does(robot,b,T), true(p,T).
true(q,T+1) :- time(T), does(robot,c,T), true(r,T).
true(r,T+1) :- time(T), does(robot,a,T), true(r,T).
true(r,T+1) :- time(T), does(robot,b,T), true(r,T).
true(r,T+1) :- time(T), does(robot,c,T), true(q,T).
true(Y,T+1) :- time(T), true(X,T), successor(X,Y).
goal(robot,100,T) :- time(T), true(p,T), true(q,T), true(r,T).
goal(robot,0,T) :- time(T), not true(p,T).
goal(robot,0,T) :- time(T), not true(q,T).
goal(robot,0,T) :- time(T), not true(r,T).
terminal(T) :- time(T), true(p,T), true(q,T), true(r,T).
terminal(T) :- time(T), true(7,T).
successor(1,2).
successor(2,3).
successor(3,4).
successor(4,5).
successor(5,6).
successor(6,7).
:- does(R,M,T), not legal(R,M,T).
:- 0{ terminal(T) : time(T) }0.
:- terminal(T), role(robot), not goal(robot,100,T).
time(1..7).
1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T).
As-is, Clingo 4.5.1 thinks this is unsatisfiable:
clingo version 4.5.1
Reading from bl_robot.lp
Solving...
UNSATISFIABLE
Models : 0
Calls : 1
Time : 0.016s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.016s
However, there is a solution, namely the one in which robot does a,b,c,a,b,a on steps 1 through 6 leading to a terminal state with goal value 100 on step 7:
does(robot,a,1).
does(robot,b,2).
does(robot,c,3).
does(robot,a,4).
does(robot,b,5).
does(robot,a,6).
The purpose of constraint 1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T) is to make sure that only one move is played at a time by robot. The development of this constraint in Chapter 15 is as follows:
1. Start with (where by "," I assume I am getting AND in this case; this may be a basic problem):
does(robot,a,T) :- time(T), not does(robot,b,T), not does(robot,c,T).
does(robot,b,T) :- time(T), not does(robot,a,T), not does(robot,c,T).
does(robot,c,T) :- time(T), not does(robot,a,T), not does(robot,b,T).
2. This reduces to
1{ does(robot,a,T); does(robot,b,T); does(robot,c,T) }1 :- time(T).
3. This reduces to
1{ does(robot,M,T) : input(robot,M) }1 :- time(T).
4. This reduces to
1{ does(R,M,T) : input(R,M) }1 :- role(R) , time(T).
It turns out this is unsatisfiable, but it can be fixed. If we replace form (4) with form (3), doesn't work. Replace (3) by (2), doesn't work. Replace (2) by (1), doesn't work. Next step is to replace 1 by this (call it 0):
does(robot,a,1) :- time(1), not does(robot,b,1), not does(robot,c,1).
does(robot,b,1) :- time(1), not does(robot,a,1), not does(robot,c,1).
does(robot,c,1) :- time(1), not does(robot,a,1), not does(robot,b,1).
does(robot,a,2) :- time(2), not does(robot,b,2), not does(robot,c,2).
does(robot,b,2) :- time(2), not does(robot,a,2), not does(robot,c,2).
does(robot,c,2) :- time(2), not does(robot,a,2), not does(robot,b,2).
does(robot,a,3) :- time(3), not does(robot,b,3), not does(robot,c,3).
does(robot,b,3) :- time(3), not does(robot,a,3), not does(robot,c,3).
does(robot,c,3) :- time(3), not does(robot,a,3), not does(robot,b,3).
does(robot,a,4) :- time(4), not does(robot,b,4), not does(robot,c,4).
does(robot,b,4) :- time(4), not does(robot,a,4), not does(robot,c,4).
does(robot,c,4) :- time(4), not does(robot,a,4), not does(robot,b,4).
does(robot,a,5) :- time(5), not does(robot,b,5), not does(robot,c,5).
does(robot,b,5) :- time(5), not does(robot,a,5), not does(robot,c,5).
does(robot,c,5) :- time(5), not does(robot,a,5), not does(robot,b,5).
does(robot,a,6) :- time(6), not does(robot,b,6), not does(robot,c,6).
does(robot,b,6) :- time(6), not does(robot,a,6), not does(robot,c,6).
does(robot,c,6) :- time(6), not does(robot,a,6), not does(robot,b,6).
At this point, a solution pops out, and it is the expected one, and it has one move per step:
c:\Users\Lars\Desktop\randori\thirdparty\clingo-4.5.1-win64>clingo bl_robot.lp
clingo version 4.5.1
Reading from bl_robot.lp
Solving...
Answer: 1
role(robot) base(p) base(q) base(r) base(1) base(2) base(3) base(4) base(5) base(6) base(7) input(robot,a) input(robot,b) input(robot,c) true(1,1) successor(1,2) successor(2,3) successor(3,4) successor(4,5) successor(5,6) successor(6,7) time(1) time(2) time(3) time(4) time(5) time(6) time(7) does(robot,a,1) does(robot,b,2) does(robot,c,3) does(robot,a,4) does(robot,b,5) does(robot,a,6) true(p,2) true(p,5) true(p,7) true(2,2) true(q,3) true(q,6) true(q,7) true(3,3) true(r,4) true(r,5) true(r,6) true(r,7) true(4,4) true(5,5) true(6,6) true(7,7) terminal(7) legal(robot,a,1) legal(robot,a,2) legal(robot,a,3) legal(robot,a,4) legal(robot,a,5) legal(robot,a,6) legal(robot,b,1) legal(robot,b,2) legal(robot,b,3) legal(robot,b,4) legal(robot,b,5) legal(robot,b,6) legal(robot,c,1) legal(robot,c,2) legal(robot,c,3) legal(robot,c,4) legal(robot,c,5) legal(robot,c,6) goal(robot,100,7) goal(robot,0,1) goal(robot,0,2) goal(robot,0,3) goal(robot,0,4) goal(robot,0,5) goal(robot,0,6)
SATISFIABLE
Models : 1+
Calls : 1
Time : 0.006s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time : 0.000s
Note that we are not adding
does(robot,c,7) :- time(7), not does(robot,a,7), not does(robot,b,7).
does(robot,a,7) :- time(7), not does(robot,c,7), not does(robot,b,7).
does(robot,b,7) :- time(7), not does(robot,c,7), not does(robot,a,7).
It turns out that if you add this, then the above becomes unsatisfiable again.
So this is a clue, that 1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T). needs to be restricted to 1<=T<=6.
So let's try that:
1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T), 1 <= T, T <= 6.
And it works! It gaves the same solution above. The original form is unsatisfiable if it's scope includes the final time step, because in the final time step, there is no move. To recap, the final, working version of bl_robot.lp is:
role(robot).
base(p).
base(q).
base(r).
base(1).
base(2).
base(3).
base(4).
base(5).
base(6).
base(7).
input(robot,a).
input(robot,b).
input(robot,c).
true(1,1).
legal(robot,a,T) :- time(T), not terminal(T).
input(robot,a).
legal(robot,b,T) :- time(T), not terminal(T).
input(robot,b).
legal(robot,c,T) :- time(T), not terminal(T).
input(robot,c).
true(p,T+1) :- time(T), does(robot,a,T), not true(p,T).
true(p,T+1) :- time(T), does(robot,b,T), true(q,T).
true(p,T+1) :- time(T), does(robot,c,T), true(p,T).
true(q,T+1) :- time(T), does(robot,a,T), true(q,T).
true(q,T+1) :- time(T), does(robot,b,T), true(p,T).
true(q,T+1) :- time(T), does(robot,c,T), true(r,T).
true(r,T+1) :- time(T), does(robot,a,T), true(r,T).
true(r,T+1) :- time(T), does(robot,b,T), true(r,T).
true(r,T+1) :- time(T), does(robot,c,T), true(q,T).
true(Y,T+1) :- time(T), true(X,T), successor(X,Y).
goal(robot,100,T) :- time(T), true(p,T), true(q,T), true(r,T).
goal(robot,0,T) :- time(T), not true(p,T).
goal(robot,0,T) :- time(T), not true(q,T).
goal(robot,0,T) :- time(T), not true(r,T).
terminal(T) :- time(T), true(p,T), true(q,T), true(r,T).
terminal(T) :- time(T), true(7,T).
successor(1,2).
successor(2,3).
successor(3,4).
successor(4,5).
successor(5,6).
successor(6,7).
:- does(R,M,T), not legal(R,M,T).
:- 0{ terminal(T) : time(T) }0.
:- terminal(T), role(robot), not goal(robot,100,T).
time(1..7).
1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T), 1 <= T, T <= 6.
We generate this from the original bl.kif file with the following Python code:
from __future__ import division
import sys
### First a LISP parser copied off the Internet from Peter Norvig: ###
Symbol = str # A Lisp Symbol is implemented as a Python str
List = list # A Lisp List is implemented as a Python list
Number = (int, float) # A Lisp Number is implemented as a Python int or float
def parse(program):
"Read a Scheme expression from a string."
return read_from_tokens(tokenize(program))
def tokenize(s):
"Convert a string into a list of tokens."
return s.replace('(',' ( ').replace(')',' ) ').split()
def atom(token):
"Numbers become numbers; every other token is a symbol."
try:
return int(token)
except ValueError:
try:
return float(token)
except ValueError:
return Symbol(token)
def read_from_tokens(tokens):
"Read an expression from a sequence of tokens."
if len(tokens) == 0:
raise SyntaxError('unexpected EOF while reading')
token = tokens.pop(0)
if '(' == token:
L = []
while tokens[0] != ')':
L.append(read_from_tokens(tokens))
tokens.pop(0) # pop off ')'
return L
elif ')' == token:
raise SyntaxError('unexpected )')
else:
return atom(token)
### End LISP parser ###
def parse_file(kf):
with open (kf, "r") as myfile:
lisp = myfile.readlines()
program = '('+''.join([x for x in lisp if x[0] != ';']).replace('\n', '')+')'
gdl = parse(program)
return gdl
def rewrite_init(s):
[init,F]=s
return ['true',F,1]
def rewrite_next(s):
[nxt,F]=s
return ['true',F,['plus','T',1]]
def rewrite_does(s):
return ['does']+s[1:]+['T']
def rewrite_not(s):
return ['not', rewriter(s[1])]
def is_input_base(s):
try:
return s[0] in ['base', 'input']
except:
return False
def rewrite_rule(s):
time = [] if is_input_base(s[1]) else [['time', 'T']]
return ['<=']+[rewriter(s[1])]+time+[rewriter(t) for t in s[2:]]
roles = []
goals = {}
actions = {}
has_input = False
def rewrite_timed_atom(s):
global goals, has_input
if s[0] == 'input':
has_input = True
role = s[1]
action = s[2]
actions[role].add(action)
elif s[0] == 'goal':
[g,role,level]=s
if role in goals:
goals[role] = max(goals[role], level)
else:
goals[role]=level
return s+['T']
def rewriter(s):
global roles, actions
if type(s)==type('a'):
return [s, 'T']
head = s[0]
if head in ['index', 'successor']:
return s
elif head == 'init':
return rewrite_init(s)
elif head == 'next':
return rewrite_next(s)
elif head == 'not':
return rewrite_not(s)
elif head == 'does':
return rewrite_does(s)
elif head in ['role', 'base', 'input']:
if head == 'role':
role = s[1]
roles.append(role)
if role not in actions:
actions[role] = set()
elif head == 'input':
role = s[1]
action = s[2]
actions[role].add(action)
return s
elif head == '<=':
return rewrite_rule(s)
else:
return rewrite_timed_atom(s)
def rewriter_top(s):
if type(s)==type('a'):
return [s, 'T']
head = s[0]
if head == 'input':
role = s[1]
action = s[2]
actions[role].add(action)
return s
elif head in ['legal', 'input']:
return ['<=', s+['T'], ['time', 'T'], ['not', ['terminal', 'T']]]
else:
return rewriter(s)
def expand_legal(gdl):
global has_input
R = []
for x in gdl:
if x[0] == 'legal':
R.extend([x, ['input']+x[1:]])
has_input = True
else:
R.append(x)
return R
def rewrite(gdl):
gdl = expand_legal(gdl)
return [rewriter_top(rule) for rule in gdl]
def aspy(s):
if type(s) == type([]):
try:
if s[0] == '<=':
return aspy(s[1])+' :- '+', '.join([aspy(x) for x in s[2:]])
elif s[0] == 'plus':
return aspy(s[1])+'+'+aspy(s[2])
elif s[0] == 'not':
return 'not '+aspy(s[1])
else:
return s[0]+'('+','.join([aspy(x) for x in s[1:]])+')'
except:
return s[0]
elif type(s)==type('a') and s[0] == '?':
return s[1:].upper()
else:
return str(s)
if __name__ == '__main__':
root = sys.argv[1]
steps = int(sys.argv[2])
role = sys.argv[3]
kf = root + '.kif'
lf = root + '_' + role + '.lp'
gdl = parse_file(kf)
gdlplus = rewrite(gdl)
with open(lf, 'w') as f:
for x in gdlplus:
f.write(aspy(x)+'.\n')
f.write(':- does(R,M,T), not legal(R,M,T).\n')
f.write(':- 0{ terminal(T) : time(T) }0.\n')
f.write(':- terminal(T), role(%s), not goal(%s,%d,T).\n' % (role, role, goals[role]))
f.write('time(1..%d).\n' % steps)
f.write('1{ does(R,M,T) : input(R,M) }1 :- role(R), time(T), 1 <= T, T <= %d.\n' % (steps-1))