From a747b382336717478cd77f50bbd55e0a101d05c6 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 20 Nov 2023 17:20:48 -0500 Subject: [PATCH 1/8] Handling edge cases in precondition -> formula --- src/main/java/org/rairlab/planner/Action.java | 9 ++++++++- src/main/java/org/rairlab/planner/State.java | 3 +++ 2 files changed, 11 insertions(+), 1 deletion(-) diff --git a/src/main/java/org/rairlab/planner/Action.java b/src/main/java/org/rairlab/planner/Action.java index 7d4d0f0..057de89 100644 --- a/src/main/java/org/rairlab/planner/Action.java +++ b/src/main/java/org/rairlab/planner/Action.java @@ -49,7 +49,14 @@ public class Action { this.freeVariables = freeVariables; - this.precondition = new And(preconditions.stream().collect(Collectors.toList())); + if (preconditions.size() > 1) { + this.precondition = new And(preconditions.stream().collect(Collectors.toList())); + } else if (preconditions.size() == 1) { + this.precondition = preconditions.iterator().next(); + } else { + this.precondition = State.TRUE; + } + this.weight = preconditions.stream().mapToInt(Formula::getWeight).sum() + additions.stream().mapToInt(Formula::getWeight).sum() + diff --git a/src/main/java/org/rairlab/planner/State.java b/src/main/java/org/rairlab/planner/State.java index 38de048..cbc9697 100644 --- a/src/main/java/org/rairlab/planner/State.java +++ b/src/main/java/org/rairlab/planner/State.java @@ -12,14 +12,17 @@ import java.util.Set; public class State { final Set formulae; + static Formula TRUE; static Formula FALSE; static{ try { + TRUE = Reader.readFormulaFromString("(or P (not P))"); FALSE = Reader.readFormulaFromString("(and P (not P))"); } catch (Reader.ParsingException e) { e.printStackTrace(); + TRUE = null; FALSE = null; } From 01883787dad4ed044c805f3d5cfabb6688ba9f2c Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 20 Nov 2023 17:23:49 -0500 Subject: [PATCH 2/8] Improving DCEC support - Time based search algorithm - Added new variables ?now and ?next --- .../java/org/rairlab/planner/Operations.java | 164 +++++++++++++++++- .../rairlab/planner/search/AStarPlanner.java | 20 ++- .../org/rairlab/planner/utils/Runner.java | 2 +- .../problems/conformant/block_tiny.clj | 108 ++++++++++++ .../problems/conformant/progression.clj | 81 +++++++++ 5 files changed, 364 insertions(+), 11 deletions(-) create mode 100644 src/main/resources/org/rairlab/planner/problems/conformant/block_tiny.clj create mode 100644 src/main/resources/org/rairlab/planner/problems/conformant/progression.clj 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))) + ] + +} From 8692700b8fb06e04636186759c1be78594632690 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 29 Mar 2024 16:53:29 -0400 Subject: [PATCH 3/8] Epistemic problem --- .../rairlab/planner/problems/epistemic/grapevine.clj | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj b/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj index ecded3f..3cce961 100644 --- a/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj +++ b/src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj @@ -61,16 +61,17 @@ ] :additions [ (Believes! ?a2 (the ?a1)) - (Believes ?a3 (the ?a1)) - (Believes ?a1 (Believes! ?a2 (the ?a1))) - (Believes ?a1 (Believes! ?a3 (the ?a1))) + (Believes! ?a3 (the ?a1)) + (Believes! ?a1 (Believes! ?a2 (the ?a1))) + (Believes! ?a1 (Believes! ?a3 (the ?a1))) ] :deletions [ (not (Believes! ?a2 (the ?a1))) (not (Believes! ?a3 (the ?a1))) - (not (Believes ?a1 (Believes! ?a2 (the ?a1)))) - (not (Believes ?a1 (Believes! ?a3 (the ?a1)))) + (not (Believes! ?a1 (Believes! ?a2 (the ?a1)))) + (not (Believes! ?a1 (Believes! ?a3 (the ?a1)))) ] + :cost 2 }) (define-action share-single [?a1 ?a2 ?a3 ?r] { @@ -96,6 +97,7 @@ (not (Believes! ?a2 (the ?a1))) (not (Believes! ?a1 (Believes! ?a2 (the ?a1)))) ] + :cost 2 }) ] From 59b6845107c08b8857f88c070ff477b3069a87c8 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 29 Mar 2024 17:30:45 -0400 Subject: [PATCH 4/8] Removed dead code --- .../java/org/rairlab/planner/Operations.java | 176 ++++-------------- .../rairlab/planner/search/AStarPlanner.java | 13 +- 2 files changed, 38 insertions(+), 151 deletions(-) diff --git a/src/main/java/org/rairlab/planner/Operations.java b/src/main/java/org/rairlab/planner/Operations.java index 2435404..183a7f3 100644 --- a/src/main/java/org/rairlab/planner/Operations.java +++ b/src/main/java/org/rairlab/planner/Operations.java @@ -33,6 +33,7 @@ public class Operations { private static boolean DEEP_EQUIVALENCE = false; private static boolean THROW_AWAY_EMPTY_BINDINGS = true; + private static boolean MONOTONIC = true; private static Prover prover; @@ -52,40 +53,44 @@ public class Operations { } public static synchronized Optional proveCached(Set assumptions, Formula goal) { - - // (1) If we've asked to prove this exact goal from assumptions before - // then return the previous result Pair, Formula> inputPair = ImmutablePair.of(assumptions, goal); - if (proverCache.containsKey(inputPair)) { - return proverCache.get(inputPair); - } - // Iterate through the cache - for (Map.Entry, Formula>, Optional> entry : proverCache.entrySet()) { - Set cachedAssumptions = entry.getKey().getLeft(); - Formula cachedGoal = entry.getKey().getRight(); - Optional optJust = entry.getValue(); - - // (2) Return the cached justification if: - // - Goals are the same - // - The cached assumptions are a subset of the current ones - // - A justification was found - if (optJust.isPresent() && cachedGoal.equals(goal) && Sets.subset(cachedAssumptions, assumptions)) { - return optJust; + if (MONOTONIC) { + // (1) If we've asked to prove this exact goal from assumptions before + // then return the previous result + if (proverCache.containsKey(inputPair)) { + return proverCache.get(inputPair); } - // (3) Return cached failure if: - // - Goals are the same - // - Assumptions are a subset of cached assumptions - // - No justification was found - if (optJust.isEmpty() && cachedGoal.equals(goal) && Sets.subset(assumptions, cachedAssumptions)) { - return optJust; + // Iterate through the cache + for (Map.Entry, Formula>, Optional> entry : proverCache.entrySet()) { + Set cachedAssumptions = entry.getKey().getLeft(); + Formula cachedGoal = entry.getKey().getRight(); + Optional optJust = entry.getValue(); + + // (2) Return the cached justification if: + // - Goals are the same + // - The cached assumptions are a subset of the current ones + // - A justification was found + if (optJust.isPresent() && cachedGoal.equals(goal) && Sets.subset(cachedAssumptions, assumptions)) { + return optJust; + } + + // (3) Return cached failure if: + // - Goals are the same + // - Assumptions are a subset of cached assumptions + // - No justification was found + if (optJust.isEmpty() && cachedGoal.equals(goal) && Sets.subset(assumptions, cachedAssumptions)) { + return optJust; + } } - } + } // Otherwise create a new call to the theorem prover Optional answer = prover.prove(assumptions, goal); - proverCache.put(inputPair, answer); + if (MONOTONIC) { + proverCache.put(inputPair, answer); + } return answer; } @@ -176,18 +181,7 @@ public class Operations { return -1; } } - - // 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) { + public static Optional>> apply(Set background, Action action, State state) { // // Get resulting states from cache if computed before if(applyCache.containsKey(Triple.of(background, action, state))){ @@ -201,20 +195,12 @@ public class Operations { // Ask theorem prover for witnesses that satisfy the precondition Set givens = Sets.union(background, state.getFormulae()); - // 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 @@ -240,13 +226,6 @@ public class Operations { 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(), deletions), additions @@ -264,97 +243,6 @@ public class Operations { } - 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 4799748..6212d9d 100644 --- a/src/main/java/org/rairlab/planner/search/AStarPlanner.java +++ b/src/main/java/org/rairlab/planner/search/AStarPlanner.java @@ -86,11 +86,11 @@ public class AStarPlanner { State lastState = currentSearch.getLeft(); List previous_actions = currentSearch.getRight(); - 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("--------------------"); + // 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(); @@ -116,8 +116,7 @@ public class AStarPlanner { for (Action action : nonTrivialActions) { // System.out.println("Considering action: " + action.getName()); - Value currentTime = Operations.getTime(previous_actions.size()); - Optional>> optNextStateActionPairs = Operations.apply(background, action, lastState, currentTime); + Optional>> optNextStateActionPairs = Operations.apply(background, action, lastState); // Ignore actions that aren't applicable if (optNextStateActionPairs.isEmpty()) { From 7760125ea4b34e716138dc3b2686eea183d0b27d Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 29 Mar 2024 17:30:57 -0400 Subject: [PATCH 5/8] Create runner jar --- pom.xml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pom.xml b/pom.xml index 12694c2..52044d9 100644 --- a/pom.xml +++ b/pom.xml @@ -16,17 +16,17 @@ 2.4 - sandbox + runner - org.rairlab.planner.Py4JServer + org.rairlab.planner.utils.Runner jar-with-dependencies - sandbox + runner package From 13b387963099c8b347d54cb152b8dd7557dbfd75 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 29 Mar 2024 17:33:43 -0400 Subject: [PATCH 6/8] Removed dead code --- .../java/org/rairlab/planner/Operations.java | 17 ----------------- 1 file changed, 17 deletions(-) diff --git a/src/main/java/org/rairlab/planner/Operations.java b/src/main/java/org/rairlab/planner/Operations.java index 183a7f3..c3999ed 100644 --- a/src/main/java/org/rairlab/planner/Operations.java +++ b/src/main/java/org/rairlab/planner/Operations.java @@ -164,23 +164,6 @@ public class Operations { return Optional.of(ans.get().getRight()); } - public static Value getTime(int time) { - return new Constant("t" + time); - } - - 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; - } - } public static Optional>> apply(Set background, Action action, State state) { // // Get resulting states from cache if computed before From f44c75e3a69950e7bacf4abc1d8ff02ec7868ebc Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 29 Mar 2024 17:33:51 -0400 Subject: [PATCH 7/8] Added timing code --- src/main/java/org/rairlab/planner/utils/Runner.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/main/java/org/rairlab/planner/utils/Runner.java b/src/main/java/org/rairlab/planner/utils/Runner.java index 624eaf2..a95b46a 100644 --- a/src/main/java/org/rairlab/planner/utils/Runner.java +++ b/src/main/java/org/rairlab/planner/utils/Runner.java @@ -50,6 +50,7 @@ public final class Runner { for (PlanningProblem planningProblem : planningProblemList) { + long start = System.currentTimeMillis(); Set plans = astarplanner.plan( planningProblem.getBackground(), planningProblem.getActions(), @@ -57,9 +58,11 @@ public final class Runner { planningProblem.getGoal(), ConstantHeuristic::h ); + long end = System.currentTimeMillis(); if(plans.size() > 0) { System.out.println(plans.toString()); + System.out.println("Time (ms): " + (end - start)); } else { System.out.println("FAILED"); From aec7d98c13dc248947837a2a970269b528e99931 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 29 Mar 2024 17:37:41 -0400 Subject: [PATCH 8/8] Removed unused domain, commented out debug code --- .../rairlab/planner/search/AStarPlanner.java | 6 +- .../problems/conformant/block_tiny.clj | 108 ------------------ .../problems/conformant/progression.clj | 81 ------------- 3 files changed, 3 insertions(+), 192 deletions(-) delete mode 100644 src/main/resources/org/rairlab/planner/problems/conformant/block_tiny.clj delete mode 100644 src/main/resources/org/rairlab/planner/problems/conformant/progression.clj diff --git a/src/main/java/org/rairlab/planner/search/AStarPlanner.java b/src/main/java/org/rairlab/planner/search/AStarPlanner.java index 6212d9d..bbed1ba 100644 --- a/src/main/java/org/rairlab/planner/search/AStarPlanner.java +++ b/src/main/java/org/rairlab/planner/search/AStarPlanner.java @@ -69,8 +69,8 @@ public class AStarPlanner { search.add(searchStart); // For debugging... - Map> seq = new HashMap>(); - seq.put(start, new ArrayList()); + // Map> seq = new HashMap>(); + // seq.put(start, new ArrayList()); // Current set of plans Set plansFound = new HashSet(); @@ -150,7 +150,7 @@ public class AStarPlanner { search.add(futureSearch); // For debugging... - seq.put(nextState, next_actions); + // seq.put(nextState, next_actions); } } 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 deleted file mode 100644 index a11b566..0000000 --- a/src/main/resources/org/rairlab/planner/problems/conformant/block_tiny.clj +++ /dev/null @@ -1,108 +0,0 @@ -; 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 deleted file mode 100644 index b565e91..0000000 --- a/src/main/resources/org/rairlab/planner/problems/conformant/progression.clj +++ /dev/null @@ -1,81 +0,0 @@ -; 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))) - ] - -}