plasp/encodings/sequential-horizon.lp

#const horizon=1.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Horizon, must be defined externally
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

time(0..horizon).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Establish initial state
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

holds(Variable, Value, 0) :- initialState(Variable, Value).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Compute derived predicates
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% conjunctive preconditions
satisfied(DerivedPredicate, type(and), T) :- derivedPredicate(DerivedPredicate, type(and)), holds(Variable, Value, T) : precondition(DerivedPredicate, type(and), Variable, Value); time(T).

% disjunctive preconditions
satisfied(DerivedPredicate, type(or), T) :- precondition(DerivedPredicate, type(or), Variable, Value), holds(Variable, Value, T), time(T).

holds(DerivedVariable, Value, T) :- satisfied(DerivedPredicate, Type, T), postcondition(DerivedPredicate, Type, effect(unconditional), DerivedVariable, Value).

holds(derivedVariable(DerivedVariable), value(DerivedVariable, false), T) :- derivedVariable(DerivedVariable), not holds(derivedVariable(DerivedVariable), value(DerivedVariable, true), T), time(T).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Perform actions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

1 {occurs(Action, T) : action(Action)} 1 :- time(T), T > 0.

% Check preconditions
:- occurs(Action, T), precondition(Action, Variable, Value), not holds(Variable, Value, T - 1).

% Apply effects
caused(Variable, Value, T) :-
	occurs(Action, T),
	postcondition(Action, Effect, Variable, Value),
	holds(VariablePre, ValuePre, T - 1) : precondition(Effect, VariablePre, ValuePre).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Inertia rules
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

modified(Variable, T) :- caused(Variable, Value, T).

holds(Variable, Value, T) :- caused(Variable, Value, T).
holds(variable(V), Value, T) :- holds(variable(V), Value, T - 1), not modified(variable(V), T), time(T).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Variables and mutex groups
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% Check that variables have unique values
:- variable(Variable), not 1 {holds(Variable, Value, T) : contains(Variable, Value)} 1, time(T).

% Check mutexes
:- mutexGroup(MutexGroup), not {holds(Variable, Value, T) : contains(MutexGroup, Variable, Value)} 1, time(T).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Verify that goal is met
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

:- goal(Variable, Value), not holds(Variable, Value, horizon).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

#show occurs/2.
Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00			`#const horizon=1.`

Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`
Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00			`% Horizon, must be defined externally`
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`

Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00			`time(0..horizon).`

Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`
Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00			`% Establish initial state`
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`

Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00			`holds(Variable, Value, 0) :- initialState(Variable, Value).`

Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`
			`% Compute derived predicates`
			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`

			`% conjunctive preconditions`
Fixed handling of goal in example encoding. The example encoding assumed that derived predicates weren’t necessary in the final time step. This is, however, incorrect, as the goal may have a precondition that requires derived predicates. In this case, the derived variables must be evaluated for the final time step. 2017-11-17 17:32:05 +01:00			`satisfied(DerivedPredicate, type(and), T) :- derivedPredicate(DerivedPredicate, type(and)), holds(Variable, Value, T) : precondition(DerivedPredicate, type(and), Variable, Value); time(T).`
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00
			`% disjunctive preconditions`
Fixed handling of goal in example encoding. The example encoding assumed that derived predicates weren’t necessary in the final time step. This is, however, incorrect, as the goal may have a precondition that requires derived predicates. In this case, the derived variables must be evaluated for the final time step. 2017-11-17 17:32:05 +01:00			`satisfied(DerivedPredicate, type(or), T) :- precondition(DerivedPredicate, type(or), Variable, Value), holds(Variable, Value, T), time(T).`
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00
			`holds(DerivedVariable, Value, T) :- satisfied(DerivedPredicate, Type, T), postcondition(DerivedPredicate, Type, effect(unconditional), DerivedVariable, Value).`

Fixed handling of goal in example encoding. The example encoding assumed that derived predicates weren’t necessary in the final time step. This is, however, incorrect, as the goal may have a precondition that requires derived predicates. In this case, the derived variables must be evaluated for the final time step. 2017-11-17 17:32:05 +01:00			`holds(derivedVariable(DerivedVariable), value(DerivedVariable, false), T) :- derivedVariable(DerivedVariable), not holds(derivedVariable(DerivedVariable), value(DerivedVariable, true), T), time(T).`
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00
			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`
Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00			`% Perform actions`
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`

Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00			`1 {occurs(Action, T) : action(Action)} 1 :- time(T), T > 0.`

			`% Check preconditions`
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`:- occurs(Action, T), precondition(Action, Variable, Value), not holds(Variable, Value, T - 1).`
Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00
			`% Apply effects`
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`caused(Variable, Value, T) :-`
			`occurs(Action, T),`
			`postcondition(Action, Effect, Variable, Value),`
			`holds(VariablePre, ValuePre, T - 1) : precondition(Effect, VariablePre, ValuePre).`

			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`
			`% Inertia rules`
			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`

Minor formatting. This change doesn’t affect derived variables, because these aren’t affected by the “caused” predicate (the “caused” predicate requires a variable to be in the postcondition of an action, and these may never be derived variables). 2017-11-17 17:34:16 +01:00			`modified(Variable, T) :- caused(Variable, Value, T).`
Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`holds(Variable, Value, T) :- caused(Variable, Value, T).`
Excluding derived variables from inertia. In the example encoding, derived variables were accidentally included in the inertia rule, as this only checked the position of the parameter. This commit fixes this by only allowing common variables (and not derived ones) within the inertia rule. 2017-11-17 17:43:44 +01:00			`holds(variable(V), Value, T) :- holds(variable(V), Value, T - 1), not modified(variable(V), T), time(T).`
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00
			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`
			`% Variables and mutex groups`
			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`
Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00
			`% Check that variables have unique values`
			`:- variable(Variable), not 1 {holds(Variable, Value, T) : contains(Variable, Value)} 1, time(T).`

			`% Check mutexes`
			`:- mutexGroup(MutexGroup), not {holds(Variable, Value, T) : contains(MutexGroup, Variable, Value)} 1, time(T).`

Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`
Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00			`% Verify that goal is met`
Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`

Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00			`:- goal(Variable, Value), not holds(Variable, Value, horizon).`

Updated sequential horizon-bound meta encoding to match new output format. 2017-06-28 16:41:31 +02:00			`%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%`

Added a sequential, fixed-horizon meta encoding. 2016-11-20 23:52:55 +01:00			`#show occurs/2.`