diff --git a/src/main/java/org/rairlab/planner/Operations.java b/src/main/java/org/rairlab/planner/Operations.java index 7f90582..2435404 100644 --- a/src/main/java/org/rairlab/planner/Operations.java +++ b/src/main/java/org/rairlab/planner/Operations.java @@ -4,11 +4,12 @@ import org.rairlab.planner.utils.Visualizer; import org.rairlab.shadow.prover.core.Prover; import org.rairlab.shadow.prover.core.ccprovers.CognitiveCalculusProver; import org.rairlab.shadow.prover.core.proof.Justification; -import org.rairlab.shadow.prover.representations.formula.BiConditional; -import org.rairlab.shadow.prover.representations.formula.Formula; - import org.rairlab.shadow.prover.representations.value.Value; import org.rairlab.shadow.prover.representations.value.Variable; +import org.rairlab.shadow.prover.representations.formula.*; +import org.rairlab.shadow.prover.representations.value.Constant; + + import org.rairlab.shadow.prover.utils.CollectionUtils; import org.rairlab.shadow.prover.utils.Sets; @@ -16,11 +17,14 @@ import org.apache.commons.lang3.tuple.Pair; import org.apache.commons.lang3.tuple.ImmutablePair; import org.apache.commons.lang3.tuple.Triple; +import java.util.ArrayList; +import java.util.HashSet; import java.util.List; import java.util.Map; import java.util.Optional; import java.util.Set; import java.util.concurrent.*; +import java.util.stream.Collectors; /** * Created by naveensundarg on 1/13/17. @@ -155,10 +159,37 @@ public class Operations { return Optional.of(ans.get().getRight()); } + public static Value getTime(int time) { + return new Constant("t" + time); + } - public static Optional>> apply(Set background, Action action, State state) { + public static int getTime(Value time) { + String s = time.getName(); + String[] ss = s.split("t"); + if (ss.length != 2) { + return -1; + } + try { + int t = Integer.parseInt(ss[1]); + return t + 1; + } catch (NumberFormatException e) { + return -1; + } + } - // Get resulting states from cache if computed before + // Take a time value, get the integer number out and + // increment by 1 + public static Value incrementTime(Value time) { + int t = getTime(time); + if (t < 0) { + return new Constant("ERROR"); + } + return new Constant("t" + (t + 1)); + } + + public static Optional>> apply(Set background, Action action, State state, Value t) { + + // // Get resulting states from cache if computed before if(applyCache.containsKey(Triple.of(background, action, state))){ Optional>> ans = applyCache.get(Triple.of(background, action, state)); if(ans.isPresent()){ @@ -169,7 +200,22 @@ public class Operations { // Ask theorem prover for witnesses that satisfy the precondition Set givens = Sets.union(background, state.getFormulae()); - Optional>> bindingsOpt = proveAndGetBindingsCached(givens, action.getPrecondition(), action.openVars()); + + // TODO: Have all this ?now and (next ?now) code within Action.java + + // Replace ?now with current time within preconditions + Formula precondition = action.getPrecondition(); + Value now = new Variable("?now"); + precondition = replaceValue(precondition, now, t); + + // We already replaced the ?now + List openVars = action.openVars() + .stream() + .filter(v -> !v.getName().equals("?now")) + .collect(Collectors.toList()); + + // TODO: Can likely more intelligently cache considering time... + Optional>> bindingsOpt = proveAndGetBindingsCached(givens, precondition, openVars); // If not witnesses found, return nothing if (!bindingsOpt.isPresent()) { @@ -191,9 +237,19 @@ public class Operations { // newState = (oldState - Deletions(a)) U Additions(a) Action groundedAction = action.instantiate(binding); + Set additions = groundedAction.getAdditions(); + Set deletions = groundedAction.getDeletions(); + + // Replace (next ?now) with appropriate time + Value nextTime = incrementTime(t); + Value nextTimeVar = new Variable("?next"); + additions = replaceValue(additions, nextTimeVar, nextTime); + deletions = replaceValue(deletions, nextTimeVar, nextTime); + + State newState = State.initializeWith(Sets.union( - Sets.difference(state.getFormulae(), groundedAction.getDeletions()), - groundedAction.getAdditions() + Sets.difference(state.getFormulae(), deletions), + additions )); // If the state progresses, record it as a possible next state @@ -203,10 +259,102 @@ public class Operations { } applyCache.put(Triple.of(background, action, state), Optional.of(nextStates)); + return Optional.of(nextStates); } + public static State replaceValue(State s, Value r, Value t) { + Set newFormulae = replaceValue(s.getFormulae(), r, t); + return State.initializeWith(newFormulae); + } + + public static Set replaceValue(Set s, Value r, Value t) { + Set newFormulae = new HashSet(); + for (Formula f : s) { + newFormulae.add(replaceValue(f, r, t)); + } + return newFormulae; + } + + public static Value replaceValue(Value v, Value r, Value t) { + if (v.getName().equals(r.getName())) { + return t; + } + return v; + } + + // Everywhere where there's a ?now replace with value t + public static Formula replaceValue(Formula f, Value r, Value t) { + // Base Cases: + + // Bottom of Formula graph wouldn't have any time points under it + if (f instanceof Predicate || f instanceof Atom) { + return f; + } + + // Check if these quantifiers contain our bound varialbe + if (f instanceof UnaryModalFormula) { + UnaryModalFormula uf = (UnaryModalFormula) f; + + Value agent = uf.getAgent(); + Value time = uf.getTime(); + Value newTime = replaceValue(time, r, t); + Formula uf_sub = uf.getFormula(); + Formula new_uf_sub = replaceValue(uf_sub, r, t); + + if (f instanceof Belief) { + return new Belief(agent, newTime, new_uf_sub); + } else if (f instanceof Intends) { + return new Intends(agent, newTime, new_uf_sub); + } else if (f instanceof Knowledge) { + return new Knowledge(agent, newTime, new_uf_sub); + } + // Assumes Perception + if (! (f instanceof Perception)) { + System.out.println("[fixTimepoints:Operations.java] Doesn't account for new modal operator"); + } + return new Perception(agent, newTime, new_uf_sub); + } + + // Recusive Case: Iterate over each subformula and replace + + if (f instanceof Not) { + Formula subFormula = ((Not) f).getArgument(); + return new Not(replaceValue(subFormula, r, t)); + } else if (f instanceof Universal) { + Formula subFormula = ((Universal) f).getArgument(); + return new Universal(((Universal) f).vars(), replaceValue(subFormula, r, t)); + } else if (f instanceof Existential) { + Formula subFormula = ((Existential) f).getArgument(); + return new Universal(((Existential) f).vars(), replaceValue(subFormula, r, t)); + } else if (f instanceof Implication) { + Formula antecedant = ((Implication) f).getAntecedent(); + Formula consequent = ((Implication) f).getConsequent(); + return new Implication(replaceValue(antecedant, r, t), replaceValue(consequent, r, t)); + } else if (f instanceof BiConditional) { + Formula left = ((BiConditional) f).getLeft(); + Formula right = ((BiConditional) f).getRight(); + return new BiConditional(replaceValue(left, r, t), replaceValue(right, r, t)); + } + + List subFormulae = f.getArgs(); + List newArguments = new ArrayList(); + for (Formula sf : subFormulae) { + newArguments.add(replaceValue(sf, r, t)); + } + + if (f instanceof And) { + return new And(newArguments); + } + + // Assume Or + if (! (f instanceof Or)) { + System.out.println("[fixTimepoints:Operations.java] Not accounting for formula type in recursive case"); + } + return new Or(newArguments); + } + public static boolean equivalent(Set background, Formula f1, Formula f2) { if (!DEEP_EQUIVALENCE) { return f1.equals(f2); diff --git a/src/main/java/org/rairlab/planner/search/AStarPlanner.java b/src/main/java/org/rairlab/planner/search/AStarPlanner.java index ec79e63..4799748 100644 --- a/src/main/java/org/rairlab/planner/search/AStarPlanner.java +++ b/src/main/java/org/rairlab/planner/search/AStarPlanner.java @@ -6,6 +6,7 @@ import org.rairlab.planner.State; import org.rairlab.planner.Action; import org.rairlab.planner.Plan; import org.rairlab.planner.Operations; +import org.rairlab.shadow.prover.representations.value.Value; import java.util.*; import java.util.function.Function; @@ -67,6 +68,10 @@ public class AStarPlanner { comparator.setValue(searchStart, 0); search.add(searchStart); + // For debugging... + Map> seq = new HashMap>(); + seq.put(start, new ArrayList()); + // Current set of plans Set plansFound = new HashSet(); @@ -81,7 +86,11 @@ public class AStarPlanner { State lastState = currentSearch.getLeft(); List previous_actions = currentSearch.getRight(); - // System.out.println("Considering state with heuristic: " + comparator.getValue(currentSearch)); + System.out.println("--------------------"); + System.out.println("Considering state with heuristic: " + comparator.getValue(currentSearch)); + System.out.println("Current Plan: " + seq.get(lastState).toString()); + System.out.println("Current State: " + lastState.toString()); + System.out.println("--------------------"); // Exit loop if we've passed the depth limit int currentDepth = previous_actions.size(); @@ -105,7 +114,10 @@ public class AStarPlanner { // Apply the action to the state and add to the search space for (Action action : nonTrivialActions) { - Optional>> optNextStateActionPairs = Operations.apply(background, action, lastState); + // System.out.println("Considering action: " + action.getName()); + + Value currentTime = Operations.getTime(previous_actions.size()); + Optional>> optNextStateActionPairs = Operations.apply(background, action, lastState, currentTime); // Ignore actions that aren't applicable if (optNextStateActionPairs.isEmpty()) { @@ -137,6 +149,10 @@ public class AStarPlanner { int heuristicValue = heuristic.apply(nextState); comparator.setValue(futureSearch, planCost + heuristicValue); search.add(futureSearch); + + // For debugging... + seq.put(nextState, next_actions); + } } } diff --git a/src/main/java/org/rairlab/planner/utils/Runner.java b/src/main/java/org/rairlab/planner/utils/Runner.java index c540233..624eaf2 100644 --- a/src/main/java/org/rairlab/planner/utils/Runner.java +++ b/src/main/java/org/rairlab/planner/utils/Runner.java @@ -46,7 +46,7 @@ public final class Runner { } AStarPlanner astarplanner = new AStarPlanner(); - astarplanner.setK(2); + astarplanner.setK(1); for (PlanningProblem planningProblem : planningProblemList) { diff --git a/src/main/resources/org/rairlab/planner/problems/conformant/block_tiny.clj b/src/main/resources/org/rairlab/planner/problems/conformant/block_tiny.clj new file mode 100644 index 0000000..a11b566 --- /dev/null +++ b/src/main/resources/org/rairlab/planner/problems/conformant/block_tiny.clj @@ -0,0 +1,108 @@ +; Original problem from Joerg Hoffmann and Ronen Brafman +{:name "Block-Conformant-Tiny" + :background [ + ; Setting object types + (block b1) + (block b2) + + ; Unique name axioms + (not (= b1 b2)) + + ; Block World Axioms + + ; Blocks are never on themselves + (forall [x] (not (on x x))) + ; on is not symmetric + (forall [x y] (if (on x y) (not (on y x)))) + ; Any block on a table isn't on top of another block + (forall [x y] (if (on-table x) (not (on x y)))) + ; Any block that is cleared does not have another block on top of it + (forall [x y] (if (clear x) (not (on y x)))) + + ; NOTE: Slow if we use complicated definitions + ;; ; A block is on the table if it isn't on top of any other block + ;; (forall [x] (iff (on-table x) (forall [y] (not (on x y))))) + ;; ; A block is cleared if there is no other block on top of it + ;; (forall [x] (iff (clear x) (forall [y] (not (on y x))))) + ] + + + :actions [ + + (define-action move-bstack-to-t [?b ?b1] { + :preconditions [ + ; Type restriction + (block ?b) + (block ?b1) + ; Arguments unique + (not (= ?b ?b1)) + + ; Preconditions + ;; (not (on-table ?b)) + + ] + ; TODO: Think hard about the effect + ;; :effect (and (when (on ?b ?bl) + ;; (and (not (on ?b ?bl)) (on-table ?b) (clear ?bl))))) + :additions [ + ; The following creates a contradiction because + ; (on-table ?b) -> (not (on ?b ?b1)) and + ; we can't have P -> \neg P + ;; (if (on ?b ?b1) (and (on-table ?b) (clear ?b1))) + + ] + :deletions [ ] + }) + + (define-action move-t-to-b [?bm ?bt ?t] { + :preconditions [ + ; Type restrictions + (block ?bm) + (block ?bt) + ; Arguments unique + (not (= ?bm ?bt)) + ; Primary preconditions + (clear ?bm ?t) + (clear ?bt ?t) + (on-table ?bm ?t) + ] + :additions [ + (on ?bm ?bt (s ?t)) + + (not (clear ?bt (s ?t))) + (not (on-table ?bm (s ?t))) + ] + :deletions [ + ;; (not (on ?bm ?bt)) + + ;; (clear ?bt) + ;; (on-table ?bm) + ] + }) + ] + :start [ + ; Unknown facts don't need to be stated + ; since we don't assume closed world assumption. + + ; Negated predicates in this example is handled by + ; the block world axioms + + (or + (and + (on b2 b1 t0) + (clear b2 t0) + (on-table b1 t0) + ) + + (and + (on b1 b2 t0) + (clear b1 t0) + (on-table b2 t0) + ) + ) + ] + :goal [ + (exists [x] (on b2 b1 x)) + ] + +} diff --git a/src/main/resources/org/rairlab/planner/problems/conformant/progression.clj b/src/main/resources/org/rairlab/planner/problems/conformant/progression.clj new file mode 100644 index 0000000..b565e91 --- /dev/null +++ b/src/main/resources/org/rairlab/planner/problems/conformant/progression.clj @@ -0,0 +1,81 @@ +; Original problem from Joerg Hoffmann and Ronen Brafman +{:name "Block-Conformant-Tiny" + :background [ + ; Setting object types + (Believes! a t0 (block b1)) + (Believes! a t0 (block b2)) + + ; Unique name axioms + (Believes! a t0 (not (= b1 b2))) + + ; Block World Axioms + + ; Blocks are never on themselves + (Believes! a t0 (forall [x] (not (on x x)))) + ; on is not symmetric + (Believes! a t0 (forall [x y] (if (on x y) (not (on y x))))) + ; Any block on a table isn't on top of another block + (Believes! a t0 (forall [x y] (if (on-table x) (not (on x y))))) + ; Any block that is cleared does not have another block on top of it + (Believes! a t0 (forall [x y] (if (clear x) (not (on y x))))) + ] + + + :actions [ + + (define-action move-t-to-b [?bm ?bt] { + :preconditions [ + (Believes! a ?now (and + ; Type Restrictions + (block ?bm) + (block ?bt) + ; Arguments Unique + (not (= ?bm ?bt)) + ; Primary preconditions + (clear ?bm) + (clear ?bt) + (on-table ?bm) + )) + ; NOTE: QA Algorithm is very barebones, + ; currently does not support beliefs under + ; binary operations. Example: + ;; (and + ;; (Believes! a t0 (block ?bm)) + ;; (Believes! a t0 (block ?bt)) + ;; ) + ] + :additions [ + ; ShadowProver uses string comparisons to determine + ; ordering on time points. + ; Spectra currently hacks around this by replacing + ; ?next where the constant + ; that represents ?now + 1. + ; ShadowProver Limitation: Cannot go beyond 10 time points + (Believes! a ?next (on ?bm ?bt)) + + ; These below shouldn't be needed but left for posterity + ;; (Believes! a ?next (not (clear ?bt))) + ;; (Believes! a ?next (not (on-table ?bm))) + ] + :deletions [ ] + }) + ] + :start [ + ; Unknown facts don't need to be stated + ; since we don't assume closed world assumption. + + ; Negated predicates in this example is handled by + ; the block world axioms + + (Believes! a t0 (on-table b2)) + (Believes! a t0 (on-table b1)) + (Believes! a t0 (clear b1)) + (Believes! a t0 (clear b2)) + ] + :goal [ + ;; (Believes! a t0 (clear ?bm)) + ; Try a there exists at some point + (exists [t] (Believes! a t (on b1 b2))) + ] + +}