From b8357629a2cf5dcbdee430fe7ea00eb833e96283 Mon Sep 17 00:00:00 2001
From: mgebser <gebser@cs.uni-potsdam.de>
Date: Mon, 14 Nov 2016 12:00:14 +0100
Subject: [PATCH] started to develop STRIPS encoding variants

---
 encodings/strips/preprocess.lp         | 48 +++++++++++++++
 encodings/strips/strips-incremental.lp | 84 ++++++++++++++++++++++++++
 2 files changed, 132 insertions(+)
 create mode 100644 encodings/strips/preprocess.lp
 create mode 100644 encodings/strips/strips-incremental.lp

diff --git a/encodings/strips/preprocess.lp b/encodings/strips/preprocess.lp
new file mode 100644
index 0000000..bd60246
--- /dev/null
+++ b/encodings/strips/preprocess.lp
@@ -0,0 +1,48 @@
+% Constant '_closure' to (de)activate analysis of potentially relevant actions
+% - value '1': forward chaining of effects w.r.t. initial variable values
+% - value '2': backward regression of effects w.r.t. goal variable values
+% - value '3': both forward chaining and backward regression of effects
+% - otherwise: off
+
+#const _closure = 3.
+
+% Check feature requirements
+
+:- requires(feature(actionCosts)).
+:- requires(feature(axiomRules)).
+:- requires(feature(conditionalEffects)).
+
+% Basic redundancy check for actions
+
+postcondition(A,X,V) :- postcondition(A,E,X,V).
+
+has_condition(A,X,0) :- action(A), precondition(A,X,V).
+has_condition(A,X,1) :- action(A), postcondition(A,X,V).
+
+inconsistent(A) :- has_condition(A,X,P),
+                   #count{V : precondition(A,X,V), P = 0;
+                          V : postcondition(A,X,V), P = 1} > 1.
+consistent(A)   :- action(A), not inconsistent(A).
+irredundant(A)  :- consistent(A), postcondition(A,X,V), not precondition(A,X,V).
+
+% Forward chaining of effects w.r.t. initial variable values
+
+feasible(X,V) :- initialState(X,V).
+feasible(X,V) :- possible(A), postcondition(A,X,V).
+
+possible(A) :- irredundant(A), feasible(X,V) : precondition(A,X,V).
+possible(A) :- irredundant(A), _closure != 1, _closure != 3.
+
+:- goal(X,V), not feasible(X,V).
+
+% Backward regression of effects w.r.t. goal variable values
+
+produce(X,V) :- goal(X,V), not initialState(X,V).
+produce(X,V) :- active(A), precondition(A,X,V), not initialState(X,V).
+produce(X,V) :- persist(X,V), active(A), has_condition(A,X,1), not postcondition(A,X,V).
+
+persist(X,V) :- goal(X,V), initialState(X,V).
+persist(X,V) :- active(A), precondition(A,X,V), initialState(X,V).
+
+active(A) :- possible(A), postcondition(A,X,V), produce(X,V).
+active(A) :- possible(A), _closure != 2, _closure != 3.
diff --git a/encodings/strips/strips-incremental.lp b/encodings/strips/strips-incremental.lp
new file mode 100644
index 0000000..a128717
--- /dev/null
+++ b/encodings/strips/strips-incremental.lp
@@ -0,0 +1,84 @@
+#include <incmode>.
+
+#const _parallel = 0.
+
+% BASE PROGRAM
+
+% Define relevant fluents w.r.t. parallel mode
+
+diverge(A1,A2,X) :- active(A1), active(A2), A1 < A2, postcondition(A1,X,V),
+                    has_condition(A2,X,1), not postcondition(A2,X,V),
+                    _parallel = 1 : _parallel != 2.
+diverge(A1,A2)   :- diverge(A1,A2,X), _parallel = 1.
+
+exclude(A1,A2) :- diverge(A1,A2), precondition(A1,X,V),
+                  has_condition(A2,X,0), not precondition(A2,X,V).
+
+fluent(X,V) :- produce(X,V).
+fluent(X,V) :- persist(X,V).
+fluent(X,V) :- initialState(X,V), fluent(X).
+fluent(X,V) :- active(A), postcondition(A,X,V), fluent(X).
+fluent(X)   :- fluent(X,V).
+fluent(X)   :- diverge(A1,A2,X), not exclude(A1,A2).
+
+% Define unsubsumed mutexes
+
+mutex(G,V) :- mutexGroup(G), contains(G,X,V), fluent(X,V).
+mutex(G)   :- mutexGroup(G), #count{V : mutex(G,V)} > 1.
+
+% Define initial state
+
+holds(X,V,0) :- initialState(X,V), fluent(X).
+
+:- fluent(X), #count{V : holds(X,V,0) } > 1.
+:- mutex(G), #count{X,V : holds(X,V,0), contains(G,X,V) } > 1.
+
+% STEP PROGRAM
+
+#program step(t).
+
+% Generate successor state
+
+1 {holds(X,V,t) : fluent(X,V)} 1 :- fluent(X).
+
+:- mutex(G), #count{X,V : holds(X,V,t), contains(G,X,V) } > 1.
+
+change(X,t) :- holds(X,V,t), not holds(X,V,t-1).
+
+% Generate actions
+
+1 {occurs(A,t) : active(A)}.
+
+:- occurs(A,t), postcondition(A,X,V), fluent(X), not holds(X,V,t).
+
+effect(X,t) :- occurs(A,t), postcondition(A,X,V), fluent(X), not precondition(A,X,V).
+
+:- change(X,t), not effect(X,t).
+
+% Check w.r.t. parallel mode
+
+:- _parallel != 1, _parallel != 2, #count{A : occurs(A,t)} > 1.
+
+:- _parallel != 2, occurs(A,t), precondition(A,X,V), not holds(X,V,t-1).
+
+invariant(X,t) :- occurs(A,t), precondition(A,X,V), _parallel = 1,
+                  not has_condition(A,X,1).
+
+:- invariant(X,t), effect(X,t).
+
+singleton(X,t) :- occurs(A,t), precondition(A,X,V), _parallel = 1,
+                  has_condition(A,X,1), not postcondition(A,X,V).
+
+:- singleton(X,t), #count{A : occurs(A,t), postcondition(A,X,V), not precondition(A,X,V) } > 1.
+
+% CHECK PROGRAM
+
+#program check(t).
+
+% Check goal conditions
+
+:- query(t), goal(X,V), not holds(X,V,t).
+
+% DISPLAY PART
+
+#show occurs/2.