Untitled

#const k = 2.
node(1..5).
edge(1,2). edge(1,3). edge(2,4).
edge(2,5). edge(3, 4). edge(4,5). 
edge(X, Y) :- edge(Y, X).

k {choose(N) : node(N)} k.
reachable(N, N):- node(N), choose(N).
reachable(N, M2) :- reachable(N, M1), edge(M1, M2), choose(N), choose(M1), choose(M2).
:- choose(N), choose(M), not reachable(N, M).
dominated(N) :- choose(N).
dominated(N) :- choose(M), edge(N, M).
:- node(N), not dominated(N).
    
#show choose/1.

#const t=2.
node(1..5).
edge(1,2). edge(1,3).
edge(2,4). edge(2,5).
edge(3,4). edge(4,5).
edge(X,Y) :- edge(Y,X).

pawn(1..2).
initial_location(1,1).
initial_location(2,5).
time(1..t+1).
action(move(N,M)) :- node(N), node(M), edge(N,M).
1{ do(P,A,T) : action(A)}1 :- pawn(P), time(T), T<t+1.

%initial location at time 1
pawn_at(P,1,X) :- initial_location(P,X).

pawn_at(P,T2,X) :- time(T1), time(T2), T2=T1+1, pawn_at(P,T1,Y), edge(X,Y), do(P, move(Y,X),T1).
% cannot move if there is no edge
:- do(P, move(X,Y),T), time(T), pawn(P), not edge(X,Y).
% cannot move to same location
:- do(P, move(X,Y),T), time(T), pawn(P), X=Y.

% Pawns cannot be moved if they are not on a node
:- not pawn_at(P,T,X), do(P, move(X,Y),T), time(T).
% never at same location
:- pawn_at(P1,T,X), pawn_at(P2,T,X), P1!=P2.
% never in adjacent location
:- pawn_at(P1,T,X), pawn_at(P2,T,Y), P1!=P2, edge(X,Y).


visited(X) :- pawn_at(P,T,X), time(T), pawn(P), node(X).
:- not visited(N), time(T), node(N).

#show do/3.