diff --git a/pom.xml b/pom.xml index c8473ea..20bf53b 100644 --- a/pom.xml +++ b/pom.xml @@ -14,7 +14,7 @@ logic prover - 0.09 + 0.84 diff --git a/snark-20120808r02/snark-interface.lisp b/snark-20120808r02/snark-interface.lisp index 6ce2e97..15ff55f 100644 --- a/snark-20120808r02/snark-interface.lisp +++ b/snark-20120808r02/snark-interface.lisp @@ -91,7 +91,7 @@ (snark:initialize :verbose verbose) (if (not verbose) (snark-deverbose) ) (temp-sorts) - (snark:run-time-limit 0.05) + (snark:run-time-limit 1) (snark:assert-supported t) (snark:assume-supported t) (snark:prove-supported t) diff --git a/src/main/java/edu/rpi/rair/Action.java b/src/main/java/edu/rpi/rair/Action.java index 2807158..c1ac9dc 100644 --- a/src/main/java/edu/rpi/rair/Action.java +++ b/src/main/java/edu/rpi/rair/Action.java @@ -1,13 +1,13 @@ package edu.rpi.rair; +import com.naveensundarg.shadow.prover.core.Logic; import com.naveensundarg.shadow.prover.representations.formula.And; import com.naveensundarg.shadow.prover.representations.formula.Formula; import com.naveensundarg.shadow.prover.representations.value.Compound; import com.naveensundarg.shadow.prover.representations.value.Value; import com.naveensundarg.shadow.prover.representations.value.Variable; import com.naveensundarg.shadow.prover.utils.CollectionUtils; -import com.naveensundarg.shadow.prover.utils.Logic; -import com.naveensundarg.shadow.prover.utils.Sets; + import com.naveensundarg.shadow.prover.utils.Sets; import java.util.List; import java.util.Map; @@ -159,6 +159,11 @@ public class Action { return trivial; } + + public Compound getShorthand() { + return shorthand; + } + @Override public String toString() { return shorthand.getArguments().length == 0? name: shorthand.toString(); diff --git a/src/main/java/edu/rpi/rair/DepthFirstPlanner.java b/src/main/java/edu/rpi/rair/DepthFirstPlanner.java index 5054f24..c7d707e 100644 --- a/src/main/java/edu/rpi/rair/DepthFirstPlanner.java +++ b/src/main/java/edu/rpi/rair/DepthFirstPlanner.java @@ -3,6 +3,8 @@ package edu.rpi.rair; import com.naveensundarg.shadow.prover.representations.formula.Formula; import com.naveensundarg.shadow.prover.utils.Pair; import com.naveensundarg.shadow.prover.utils.Sets; +import edu.rpi.rair.utils.PlanningProblem; +import edu.rpi.rair.utils.Visualizer; import java.util.*; import java.util.stream.Collectors; @@ -13,8 +15,8 @@ import java.util.stream.Collectors; public class DepthFirstPlanner implements Planner { - private static int MAX_DEPTH = 4; - private static boolean EXHAUSTIVE_TILL_MAX_DEPTH = false; + private static int MAX_DEPTH = 5; + private static boolean EXHAUSTIVE_TILL_MAX_DEPTH = true; public static int getMaxDepth() { return MAX_DEPTH; @@ -59,6 +61,61 @@ public class DepthFirstPlanner implements Planner { } + @Override + public Optional> plan(PlanningProblem problem, Set background, Set actions, State start, State goal) { + + + if (!EXHAUSTIVE_TILL_MAX_DEPTH) { + + return planInternal(Sets.newSet(), 0, MAX_DEPTH, background, actions, start, goal); + + } else { + + Set possiblePlans = Sets.newSet(); + for (int i = 1; i <= MAX_DEPTH; i++) { + + Optional> plansOpt = planInternal(Sets.newSet(), 0, i, background, actions, start, goal); + + if (plansOpt.isPresent()) { + + Set complyingPlans = plansOpt.get().stream(). + filter(plan-> plan.getActions().stream(). + map(Action::getShorthand). + noneMatch(shortHand-> { + + return problem.getAvoidIfPossible(). + stream().map(Object::toString). + collect(Collectors.toSet()). + contains(shortHand.getName()); + + })). + collect(Collectors.toSet()); + + + if(!complyingPlans.isEmpty()){ + return Optional.of(complyingPlans); + } + else{ + + possiblePlans.addAll(plansOpt.get()); + } + + } + + } +// + if(possiblePlans.isEmpty()){ + return Optional.empty(); + + } else{ + + return Optional.of(possiblePlans); + } + + } + + + } private Optional> planInternal(Set> history, int currentDepth, int maxDepth, Set background, Set actions, State start, State goal) { @@ -83,9 +140,11 @@ public class DepthFirstPlanner implements Planner { for (Pair stateActionPair : nextStateActionPairs.get()) { - + Visualizer.push(); Optional> planOpt = planInternal(history, currentDepth + 1, maxDepth, background, actions, stateActionPair.first(), goal); + Visualizer.pop(); + if (planOpt.isPresent()) { atleastOnePlanFound = true; @@ -100,6 +159,8 @@ public class DepthFirstPlanner implements Planner { allPlans.addAll(augmentedPlans); + // return Optional.of(allPlans); + //TODO: store different plans and return the best plan. } } diff --git a/src/main/java/edu/rpi/rair/Goal.java b/src/main/java/edu/rpi/rair/Goal.java index 31e6a3e..12bff0f 100644 --- a/src/main/java/edu/rpi/rair/Goal.java +++ b/src/main/java/edu/rpi/rair/Goal.java @@ -10,6 +10,8 @@ public class Goal { private final State goalState; private final double priority; private final String name; + private final String description; + private static final AtomicInteger nameCounter; static { @@ -19,12 +21,22 @@ public class Goal { this.goalState = goalState; this.priority = priority; this.name = "G" + nameCounter.incrementAndGet(); + this.description = goalState.toString(); + } private Goal(State goalState, double priority, String name) { this.goalState = goalState; this.priority = priority; this.name = name; + this.description = goalState.toString(); + } + + private Goal(State goalState, double priority, String name, String description) { + this.goalState = goalState; + this.priority = priority; + this.name = name; + this.description = description; } public static Goal makeGoal(State goalState, double priority){ @@ -32,9 +44,9 @@ public class Goal { } - public static Goal makeGoal(State goalState, double priority, String name){ + public static Goal makeGoal(State goalState, double priority, String name, String description){ - return new Goal(goalState, priority, name); + return new Goal(goalState, priority, name, description); } @@ -51,13 +63,12 @@ public class Goal { return name; } + public String getDescription() { + return description; + } @Override public String toString() { - return "Goal{" + - "goalState=" + goalState + - ", priority=" + priority + - ", name='" + name + '\'' + - '}'; + return "(" + name + ": " + description + ": " + priority+ ")"; } @Override diff --git a/src/main/java/edu/rpi/rair/GoalTracker.java b/src/main/java/edu/rpi/rair/GoalTracker.java index 3972294..df4164a 100644 --- a/src/main/java/edu/rpi/rair/GoalTracker.java +++ b/src/main/java/edu/rpi/rair/GoalTracker.java @@ -4,6 +4,7 @@ import com.naveensundarg.shadow.prover.representations.formula.Formula; import com.naveensundarg.shadow.prover.utils.CollectionUtils; import com.naveensundarg.shadow.prover.utils.Pair; import com.naveensundarg.shadow.prover.utils.Sets; +import edu.rpi.rair.utils.PlanningProblem; import java.util.Comparator; import java.util.List; @@ -24,14 +25,16 @@ public class GoalTracker { private final Set currentGoals; private final Planner planner; private final Set actions; - - public GoalTracker(Set background, State startState, Set actions) { + private final PlanningProblem problem; + public GoalTracker(PlanningProblem problem, Set background, State startState, Set actions) { this.background = background; this.currentState = startState; this.currentGoals = CollectionUtils.newEmptySet(); this.planner = new DepthFirstPlanner(); this.actions = actions; + this.problem = problem; + Operations.reset(); } @@ -68,7 +71,7 @@ public class GoalTracker { - Optional> possiblePlans = planner.plan(background, actions, currentState, goal.getGoalState()); + Optional> possiblePlans = planner.plan(problem, background, actions, currentState, goal.getGoalState()); if (!possiblePlans.isPresent()) { @@ -151,6 +154,18 @@ public class GoalTracker { } + public Set getBackground() { + return background; + } + + public State getCurrentState() { + return currentState; + } + + public PlanningProblem getProblem() { + return problem; + } + public Set getCurrentGoals() { return currentGoals; } diff --git a/src/main/java/edu/rpi/rair/Inducer.java b/src/main/java/edu/rpi/rair/Inducer.java new file mode 100644 index 0000000..e4c3f8a --- /dev/null +++ b/src/main/java/edu/rpi/rair/Inducer.java @@ -0,0 +1,13 @@ +package edu.rpi.rair; + +import edu.rpi.rair.Plan; +import edu.rpi.rair.utils.PlanningProblem; + +/** + * Created by naveensundarg on 12/19/17. + */ +public interface Inducer { + + Plan induce(PlanningProblem planningProblem, State start, Goal goal, Plan plan); + +} diff --git a/src/main/java/edu/rpi/rair/Operations.java b/src/main/java/edu/rpi/rair/Operations.java index e6bc989..612218b 100644 --- a/src/main/java/edu/rpi/rair/Operations.java +++ b/src/main/java/edu/rpi/rair/Operations.java @@ -3,7 +3,6 @@ package edu.rpi.rair; import com.naveensundarg.shadow.prover.core.Prover; import com.naveensundarg.shadow.prover.core.SnarkWrapper; import com.naveensundarg.shadow.prover.core.proof.Justification; -import com.naveensundarg.shadow.prover.core.proof.TrivialJustification; import com.naveensundarg.shadow.prover.representations.formula.BiConditional; import com.naveensundarg.shadow.prover.representations.formula.Formula; import com.naveensundarg.shadow.prover.representations.formula.Predicate; @@ -12,7 +11,9 @@ import com.naveensundarg.shadow.prover.representations.value.Variable; import com.naveensundarg.shadow.prover.utils.CollectionUtils; import com.naveensundarg.shadow.prover.utils.ImmutablePair; import com.naveensundarg.shadow.prover.utils.Pair; + import com.naveensundarg.shadow.prover.utils.Sets; +import edu.rpi.rair.utils.Visualizer; import org.apache.commons.lang3.tuple.Triple; import java.util.List; @@ -30,7 +31,7 @@ import static edu.rpi.rair.State.FALSE; public class Operations { private static boolean DEEP_EQUIVALENCE = false; - private static boolean THROW_AWAY_EMPTY_BINDINGS = false; + private static boolean THROW_AWAY_EMPTY_BINDINGS = true; private static Prover prover; @@ -46,7 +47,8 @@ public class Operations { applyCache.clear(); } static { - prover = new SnarkWrapper(); + prover = SnarkWrapper.getInstance(); + } @@ -110,7 +112,7 @@ public class Operations { if(room1.equals(room2)){ - return Optional.of(Justification.trivial(goal)); + return Optional.of(Justification.trivial(assumptions, goal)); } } @@ -172,8 +174,15 @@ public class Operations { public static synchronized Optional>> proveAndGetMultipleBindings(Set givens, Formula goal, List variables) { - return prover.proveAndGetMultipleBindings(givens, goal, variables); + Optional>>> ans = prover.proveAndGetMultipleBindings(givens, goal, variables); + if(ans.isPresent()){ + + return Optional.of(ans.get().getRight()); + + }else { + return Optional.empty(); + } /* Future>>> future = new FutureTask<>(()-> prover.proveAndGetMultipleBindings(givens, goal, variables)); Optional>> answer; @@ -192,9 +201,14 @@ public class Operations { public static Optional>> apply(Set background, Action action, State state) { + if(applyCache.containsKey(Triple.of(background, action, state))){ - return applyCache.get(Triple.of(background, action, state)); + Optional>> ans = applyCache.get(Triple.of(background, action, state)); + if(ans.isPresent()){ + return applyCache.get(Triple.of(background, action, state)); + + } } Set givens = Sets.union(background, state.getFormulae()); @@ -206,11 +220,14 @@ public class Operations { if (!bindingsOpt.isPresent()) { + applyCache.put(Triple.of(background, action ,state), Optional.empty()); return Optional.empty(); } + Visualizer.nested(action.getName()); + Set> nexts = Sets.newSet(); for (Map binding : bindingsOpt.get()) { @@ -222,7 +239,7 @@ public class Operations { Set instantiatedDeletions = action.instantiateDeletions(binding); Set formulaeToRemove = state.getFormulae().stream(). - filter(f -> instantiatedDeletions.stream().anyMatch(d -> equivalent(background, f, d))).collect(Collectors.toSet()); + filter(f -> instantiatedDeletions.stream().anyMatch(d -> equivalent(Sets.union(background, state.getFormulae()), f, d))).collect(Collectors.toSet()); Set newFormulae = Sets.union(background, state.getFormulae()); @@ -239,6 +256,7 @@ public class Operations { } + if (nexts.isEmpty()) { Map emptyBinding = CollectionUtils.newMap(); @@ -262,6 +280,10 @@ public class Operations { } + nexts = nexts.stream().filter(n-> !n.first().getFormulae().equals(state.getFormulae())).collect(Collectors.toSet());; + + + applyCache.put(Triple.of(background, action ,state), Optional.of(nexts)); return Optional.of(nexts); diff --git a/src/main/java/edu/rpi/rair/Plan.java b/src/main/java/edu/rpi/rair/Plan.java index dca0e9d..dd684ff 100644 --- a/src/main/java/edu/rpi/rair/Plan.java +++ b/src/main/java/edu/rpi/rair/Plan.java @@ -2,6 +2,7 @@ package edu.rpi.rair; import com.naveensundarg.shadow.prover.representations.formula.Formula; import com.naveensundarg.shadow.prover.utils.CollectionUtils; +import edu.rpi.rair.utils.Visualizer; import java.util.List; import java.util.Set; @@ -63,15 +64,32 @@ public class Plan { public boolean noConflicts(Set goals){ - return getConflictingGoals(goals).isEmpty(); + Set conflicts = getConflictingGoals(goals); + if(!conflicts.isEmpty()){ + + Visualizer.print(this.toString()) ; + Visualizer.printRed(" CONFLICTS WITH "); + Visualizer.print(conflicts.stream().map(x-> x.getDescription()).collect(Collectors.toSet()).toString()); + System.out.println(); + + } + + return conflicts.isEmpty(); + + } + + public static Plan cleanUp(Plan plan){ + + List actions = plan.getActions(); + List states = plan.getExpectedStates(); + + return null; } @Override public String toString() { - return "Plan{" + - "actions=" + actions + - '}'; + return actions.stream().map(x-> x.toString() + " ").reduce((x,y) -> x + y).get(); } @Override diff --git a/src/main/java/edu/rpi/rair/PlanMethod.java b/src/main/java/edu/rpi/rair/PlanMethod.java new file mode 100644 index 0000000..a045040 --- /dev/null +++ b/src/main/java/edu/rpi/rair/PlanMethod.java @@ -0,0 +1,123 @@ +package edu.rpi.rair; + +import com.naveensundarg.shadow.prover.representations.formula.And; +import com.naveensundarg.shadow.prover.representations.formula.Formula; +import com.naveensundarg.shadow.prover.representations.value.Compound; +import com.naveensundarg.shadow.prover.representations.value.Value; +import com.naveensundarg.shadow.prover.representations.value.Variable; +import com.naveensundarg.shadow.prover.utils.CollectionUtils; +import com.naveensundarg.shadow.prover.utils.Reader; +import com.naveensundarg.shadow.prover.utils.Sets; +import edu.rpi.rair.utils.PlanningProblem; + import us.bpsm.edn.Keyword; +import us.bpsm.edn.Symbol; +import us.bpsm.edn.parser.Parseable; +import us.bpsm.edn.parser.Parser; +import us.bpsm.edn.parser.Parsers; + +import java.io.StringReader; +import java.util.*; +import java.util.stream.Collector; +import java.util.stream.Collectors; + +/** + * Created by naveensundarg on 12/22/17. + */ +public class PlanMethod { + + private final Set backGroundStatePreconditions; + private final Set goalPreconditions; + private final List freeVariables; + private final List actionCompounds; + + + + public PlanMethod(Set goalPreconditions, Set backGroundStatePreconditions, List freeVariables, List actionCompounds) { + this.goalPreconditions = goalPreconditions; + this.backGroundStatePreconditions = backGroundStatePreconditions; + this.freeVariables = freeVariables; + this.actionCompounds = actionCompounds; + + } + + + public PlanMethod(Set goalPreconditions, List freeVariables, List actionCompounds) { + this.goalPreconditions = goalPreconditions; + this.backGroundStatePreconditions = Sets.newSet(); + this.freeVariables = freeVariables; + this.actionCompounds = actionCompounds; + + } + + + public Optional> apply(Set background, Set start, Set goal, Set actionSpecs) { + + + Optional>> mappingsOpt = Operations.proveAndGetMultipleBindings(goal, new And(new ArrayList<>(goalPreconditions)), freeVariables); + + if (mappingsOpt.isPresent()) { + + Set> mappings = mappingsOpt.get(); + + List planSketches = CollectionUtils.newEmptyList(); + + + mappings.forEach(mapping ->{ + + Formula whileCondition = (new And(new ArrayList<>(backGroundStatePreconditions))).apply(mapping); + + boolean whileHolds = Operations.proveCached(Sets.union(background, start), whileCondition).isPresent(); + + + if(whileHolds){ + + List instantiatedActionCompounds = actionCompounds.stream().map(compound -> (Compound) compound.apply(mapping)).collect(Collectors.toList()); + + + List actions = CollectionUtils.newEmptyList(); + + for (Compound compound : instantiatedActionCompounds) { + + + try { + + actions.add(PlanningProblem.readInstantiatedAction(actionSpecs, compound.toString())); + + } catch (Reader.ParsingException e) { + + e.printStackTrace(); + + } + } + + planSketches.add(new PlanSketch(actions, background)); + + + + } + + + }); + + + + return Optional.of(planSketches); + + } else { + + return Optional.empty(); + } + + + } + + @Override + public String toString() { + return "PlanMethod{" + + "backGroundStatePreconditions=" + backGroundStatePreconditions + + ", goalPreconditions=" + goalPreconditions + + ", freeVariables=" + freeVariables + + ", actionCompounds=" + actionCompounds + + '}'; + } +} diff --git a/src/main/java/edu/rpi/rair/PlanSketch.java b/src/main/java/edu/rpi/rair/PlanSketch.java new file mode 100644 index 0000000..b91b01c --- /dev/null +++ b/src/main/java/edu/rpi/rair/PlanSketch.java @@ -0,0 +1,14 @@ +package edu.rpi.rair; + +import com.naveensundarg.shadow.prover.representations.formula.Formula; +import com.naveensundarg.shadow.prover.utils.CollectionUtils; +import com.naveensundarg.shadow.prover.utils.Sets; + +import java.util.List; +import java.util.Set; + +public class PlanSketch extends Plan{ + public PlanSketch(List actions, Set background) { + super(actions, CollectionUtils.newEmptyList(), background); + } +} diff --git a/src/main/java/edu/rpi/rair/Planner.java b/src/main/java/edu/rpi/rair/Planner.java index 423555a..b6abf0d 100644 --- a/src/main/java/edu/rpi/rair/Planner.java +++ b/src/main/java/edu/rpi/rair/Planner.java @@ -1,6 +1,7 @@ package edu.rpi.rair; import com.naveensundarg.shadow.prover.representations.formula.Formula; +import edu.rpi.rair.utils.PlanningProblem; import java.util.List; import java.util.Optional; @@ -12,5 +13,6 @@ import java.util.Set; public interface Planner { Optional> plan(Set background, Set actions, State start, State goal); + Optional> plan(PlanningProblem problem, Set background, Set actions, State start, State goal); } diff --git a/src/main/java/edu/rpi/rair/State.java b/src/main/java/edu/rpi/rair/State.java index 06e1ac4..7940680 100644 --- a/src/main/java/edu/rpi/rair/State.java +++ b/src/main/java/edu/rpi/rair/State.java @@ -17,7 +17,7 @@ import java.util.stream.Collectors; public class State { final Set formulae; - private static final Prover prover = new SnarkWrapper(); + private static final Prover prover = SnarkWrapper.getInstance(); static Formula FALSE; static{ diff --git a/src/main/java/edu/rpi/rair/inducers/SimpleInducer.java b/src/main/java/edu/rpi/rair/inducers/SimpleInducer.java new file mode 100644 index 0000000..7567e2d --- /dev/null +++ b/src/main/java/edu/rpi/rair/inducers/SimpleInducer.java @@ -0,0 +1,63 @@ +package edu.rpi.rair.inducers; + +import com.naveensundarg.shadow.prover.representations.formula.Formula; +import com.naveensundarg.shadow.prover.representations.value.Compound; +import com.naveensundarg.shadow.prover.representations.value.Value; +import com.naveensundarg.shadow.prover.representations.value.Variable; +import com.naveensundarg.shadow.prover.utils.Pair; +import com.naveensundarg.shadow.prover.utils.Sets; +import edu.rpi.rair.*; +import edu.rpi.rair.utils.Commons; +import edu.rpi.rair.utils.PlanningProblem; + +import java.util.Arrays; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.function.Function; +import java.util.stream.Collectors; + +/** + * Created by naveensundarg on 12/19/17. + */ +public class SimpleInducer implements Inducer{ + @Override + public Plan induce(PlanningProblem planningProblem, State start, Goal goal, Plan plan) { + + + List actionList = plan.getActions(); + List actionCompounds = actionList.stream().map(Action::getShorthand).collect(Collectors.toList()); + + + Set backgroundFormula = planningProblem.getBackground().stream().collect(Collectors.toSet()); + Set initFormula = start.getFormulae().stream().collect(Collectors.toSet()); + Set goalFormula = goal.getGoalState().getFormulae().stream().collect(Collectors.toSet()); + + Set values = actionCompounds.stream(). + map(Compound::getArguments).map(Arrays::stream).map(x->x.collect(Collectors.toSet())) + .reduce(Sets.newSet(), Sets::union) + .stream().filter(Value::isConstant).collect(Collectors.toSet()); + + + Map valueVariableMap = Commons.makeVariables(values); + + Function,Set> getRelevantFormula = formulae -> formulae.stream(). + filter(formula -> !Sets.intersection(values, formula.valuesPresent()).isEmpty()). + collect(Collectors.toSet()); + + Set relevantBackgroundFormula = getRelevantFormula.apply(backgroundFormula); + Set relevantInitFormula = getRelevantFormula.apply(initFormula); + Set relevantGoalFormula = getRelevantFormula.apply(goalFormula); + + + Commons.generalize(valueVariableMap, relevantBackgroundFormula); + Commons.generalize(valueVariableMap, relevantInitFormula); + Commons.generalize(valueVariableMap, relevantGoalFormula); + + System.out.println(relevantBackgroundFormula); + System.out.println(relevantInitFormula); + System.out.println(relevantGoalFormula); + + return null; + } +} diff --git a/src/main/java/edu/rpi/rair/utils/Commons.java b/src/main/java/edu/rpi/rair/utils/Commons.java index 787f9ed..2b97770 100644 --- a/src/main/java/edu/rpi/rair/utils/Commons.java +++ b/src/main/java/edu/rpi/rair/utils/Commons.java @@ -1,12 +1,108 @@ package edu.rpi.rair.utils; +import clojure.lang.Obj; +import com.naveensundarg.shadow.prover.representations.formula.And; +import com.naveensundarg.shadow.prover.representations.formula.Existential; +import com.naveensundarg.shadow.prover.representations.formula.Formula; +import com.naveensundarg.shadow.prover.representations.formula.Universal; +import com.naveensundarg.shadow.prover.representations.value.Value; +import com.naveensundarg.shadow.prover.representations.value.Variable; +import com.naveensundarg.shadow.prover.utils.CollectionUtils; +import com.naveensundarg.shadow.prover.utils.Sets; import edu.rpi.rair.State; import us.bpsm.edn.parser.Parseable; +import java.util.Map; +import java.util.Set; +import java.util.function.BiFunction; +import java.util.function.Consumer; +import java.util.function.Function; +import java.util.stream.Collectors; + /** * Created by naveensundarg on 1/15/17. */ public class Commons { + public static Map makeVariables(Set values){ + + + return makeVariables(values, 1); + + } + + public static Map makeVariables(Set values, int startValue){ + int n = startValue; + + Map valueVariableMap = CollectionUtils.newMap(); + + for(Value value: values){ + + Variable variable = new Variable("?" +value); + valueVariableMap.put(value, variable); + n = n +1; + + + } + + return valueVariableMap; + } + + public static Formula generalize(Map universalValueVariableMap, Set formulae){ + + Set allValues = formulae.stream().map(Formula::valuesPresent).reduce(Sets.newSet(), Sets::union).stream().filter(x->x.isConstant()).collect(Collectors.toSet()); + + Map existentialValueVariableMap = makeVariables(Sets.difference(allValues, universalValueVariableMap.keySet()), universalValueVariableMap.size() + 1); + + + Map combinedMap = combine((universalValueVariableMap), (existentialValueVariableMap)); + Formula f = (new And(formulae.stream().collect(Collectors.toList()))).generalize(combinedMap); + + Variable[] universalVars = new Variable[universalValueVariableMap.values().size()]; + universalVars = universalValueVariableMap.values().toArray(universalVars); + + Variable[] existentialVars = new Variable[existentialValueVariableMap.values().size()]; + existentialVars = existentialValueVariableMap.values().toArray(existentialVars); + + + System.out.println(new Universal(universalVars, new Existential(existentialVars, f))); + return new Universal(universalVars, new Existential(existentialVars, f)); + } + + public static Map reverse(Map map){ + + Map reverseMap = CollectionUtils.newMap(); + + map.forEach((u, v) -> reverseMap.put(v, u)); + + return reverseMap; + } + + public static Map combine(Map map1, Map map2){ + + Map combinedMap = CollectionUtils.newMap(); + + map1.forEach(combinedMap::put); + map2.forEach(combinedMap::put); + + return combinedMap; + } + + public static Object runAndTime(BiFunction function, U u, V v, String message){ + + long start, end; + + start = System.currentTimeMillis(); + + Object w = function.apply(u, v); + + end = System.currentTimeMillis(); + + + System.out.println("Timing for: " + message + (end - start)/1000 + " s"); + + return w; + } } + diff --git a/src/main/java/edu/rpi/rair/utils/FrozenPrinter.java b/src/main/java/edu/rpi/rair/utils/FrozenPrinter.java new file mode 100644 index 0000000..f3e352b --- /dev/null +++ b/src/main/java/edu/rpi/rair/utils/FrozenPrinter.java @@ -0,0 +1,18 @@ +package edu.rpi.rair.utils; + +import com.diogonunes.jcdp.color.ColoredPrinter; +import com.diogonunes.jcdp.color.api.AbstractColoredPrinter; + +/** + * Created by naveensundarg on 9/29/17. + */ +public class FrozenPrinter extends ColoredPrinter { + + + public FrozenPrinter(Builder b) { + super(b); + } + + + +} diff --git a/src/main/java/edu/rpi/rair/utils/GoalTrackingProblem.java b/src/main/java/edu/rpi/rair/utils/GoalTrackingProblem.java index 6417aa1..0542ce0 100644 --- a/src/main/java/edu/rpi/rair/utils/GoalTrackingProblem.java +++ b/src/main/java/edu/rpi/rair/utils/GoalTrackingProblem.java @@ -27,6 +27,7 @@ public class GoalTrackingProblem { private static final Keyword DEFINITIONS = Keyword.newKeyword("definitions"); private static final Keyword GOALS = Keyword.newKeyword("goals"); + private static final Keyword DESCRIPTION = Keyword.newKeyword("description"); private static final Keyword PRIORITY = Keyword.newKeyword("priority"); private static final Keyword STATE = Keyword.newKeyword("state"); @@ -69,7 +70,8 @@ public class GoalTrackingProblem { double priority = ((Double) goalSpec.get(PRIORITY)); Set stateFormulae = PlanningProblem.readFrom((List) goalSpec.get(STATE)); - goals.add(Goal.makeGoal(State.initializeWith(stateFormulae), priority, name)); + String description = goalSpec.get(DESCRIPTION)!=null? goalSpec.get(DESCRIPTION).toString(): stateFormulae.toString(); + goals.add(Goal.makeGoal(State.initializeWith(stateFormulae), priority, name, description)); } diff --git a/src/main/java/edu/rpi/rair/utils/LearningSystem.java b/src/main/java/edu/rpi/rair/utils/LearningSystem.java new file mode 100644 index 0000000..c1b48af --- /dev/null +++ b/src/main/java/edu/rpi/rair/utils/LearningSystem.java @@ -0,0 +1,77 @@ +package edu.rpi.rair.utils; + +import com.diogonunes.jcdp.color.ColoredPrinter; +import com.diogonunes.jcdp.color.api.Ansi; +import com.google.common.collect.Sets; +import com.naveensundarg.shadow.prover.core.Prover; +import com.naveensundarg.shadow.prover.core.SnarkWrapper; +import com.naveensundarg.shadow.prover.utils.Reader; +import edu.rpi.rair.*; +import edu.rpi.rair.inducers.SimpleInducer; +import org.apache.commons.lang3.tuple.Triple; + +import java.util.ArrayList; +import java.util.List; +import java.util.Optional; +import java.util.Set; +import java.util.function.BiConsumer; +import java.util.function.BiFunction; +import java.util.function.Function; +import java.util.stream.Collectors; + +/** + * Created by naveensundarg on 1/15/17. + */ +public class LearningSystem { + + static ColoredPrinter cp = new ColoredPrinter.Builder(1, false).build(); + + + static List, String, String>> printQueue = new ArrayList<>(); + + + public static void main(String[] args) throws Reader.ParsingException, InterruptedException { + + + System.out.println(); + + RunDemo.planningProblemWarmUp(); + + Visualizer.setShouldVisualize(false); + + List goalTrackingProblemList1 = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("seriated_challenge_1.clj"))); + List goalTrackingProblemList2 = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("seriated_challenge_2.clj"))); + + + GoalTrackingProblem goalTrackingProblem1 = goalTrackingProblemList1.get(0); + GoalTrackingProblem goalTrackingProblem2 = goalTrackingProblemList2.get(0); + + + PlanningProblem planningProblem1 = goalTrackingProblem1.getPlanningProblem(); + PlanningProblem planningProblem2 = goalTrackingProblem2.getPlanningProblem(); + + Planner planner = new DepthFirstPlanner(); + + // GoalTracker(PlanningProblem problem, Set background, State startState, Set actions) + + GoalTracker goalTracker1 = new GoalTracker(planningProblem1, planningProblem1.getBackground(), planningProblem1.getStart(), planningProblem1.getActions()); + GoalTracker goalTracker2 = new GoalTracker(planningProblem2, planningProblem2.getBackground(), planningProblem2.getStart(), planningProblem2.getActions()); + + + long start, end; + + + + + + // Plan plan1 = goalTracker1.adoptGoal(goalTrackingProblem1.getGoalNamed("G1")).get(); + //Plan plan2 = goalTracker2.adoptGoal(goalTrackingProblem2.getGoalNamed("G1")).get(); + + BiFunction run = (goalTracker, goalTrackingProblem) -> goalTracker.adoptGoal(goalTrackingProblem.getGoalNamed("G1")).get(); + + System.out.println(Commons.runAndTime(run, goalTracker1, goalTrackingProblem1, "Problem 1")); + System.out.println(Commons.runAndTime(run, goalTracker2, goalTrackingProblem2, "Problem 2")); + + } + +} diff --git a/src/main/java/edu/rpi/rair/utils/PlanningProblem.java b/src/main/java/edu/rpi/rair/utils/PlanningProblem.java index d806dbd..a6fdea7 100644 --- a/src/main/java/edu/rpi/rair/utils/PlanningProblem.java +++ b/src/main/java/edu/rpi/rair/utils/PlanningProblem.java @@ -2,10 +2,12 @@ package edu.rpi.rair.utils; import clojure.lang.Obj; import com.naveensundarg.shadow.prover.representations.formula.Formula; +import com.naveensundarg.shadow.prover.representations.value.Compound; import com.naveensundarg.shadow.prover.representations.value.Value; import com.naveensundarg.shadow.prover.representations.value.Variable; import com.naveensundarg.shadow.prover.utils.CollectionUtils; import com.naveensundarg.shadow.prover.utils.Reader; +import com.naveensundarg.shadow.prover.utils.Sets; import edu.rpi.rair.Action; import edu.rpi.rair.State; import us.bpsm.edn.Keyword; @@ -17,6 +19,7 @@ import us.bpsm.edn.parser.Token; import java.io.InputStream; import java.io.InputStreamReader; +import java.io.StringReader; import java.security.Key; import java.util.*; import java.util.stream.Collectors; @@ -34,11 +37,14 @@ public class PlanningProblem { private Optional>> expectedActionSequencesOpt; private Map actionMap; + private Set avoidIfPossible; + private static final Keyword BACKGROUND = Keyword.newKeyword("background"); private static final Keyword START = Keyword.newKeyword("start"); private static final Keyword GOAL = Keyword.newKeyword("goal"); private static final Keyword NAME = Keyword.newKeyword("name"); private static final Keyword ACTION = Keyword.newKeyword("actions"); + private static final Keyword AVOID_IF_POSSIBLE = Keyword.newKeyword("avoid-if-possible"); private static final Keyword PRECONDITIONS = Keyword.newKeyword("preconditions"); private static final Keyword ADDITIONS = Keyword.newKeyword("additions"); @@ -48,7 +54,7 @@ public class PlanningProblem { private static final Keyword EXPECTED_PLANS = Keyword.newKeyword("expected-plans"); - public PlanningProblem(String name, Set background, State start, State goal, Set actions) { + private PlanningProblem(String name, Set background, State start, State goal, Set actions, Set avoidIfPossible) { this.background = background; this.start = start; @@ -56,10 +62,13 @@ public class PlanningProblem { this.goal = goal; this.name = name; this.actionMap = CollectionUtils.newMap(); + this.avoidIfPossible = avoidIfPossible; + this.expectedActionSequencesOpt = Optional.empty(); + } - public PlanningProblem(String name, Set background, State start, State goal, Set actions, Set> expectedActionSequences) { + private PlanningProblem(String name, Set background, State start, State goal, Set actions, Set avoidIfPossible, Set>expectedActionSequences) { this.background = background; this.start = start; @@ -67,6 +76,8 @@ public class PlanningProblem { this.goal = goal; this.name = name; this.actionMap = CollectionUtils.newMap(); + this.avoidIfPossible = avoidIfPossible; + this.expectedActionSequencesOpt = Optional.of(expectedActionSequences); } @@ -100,6 +111,7 @@ public class PlanningProblem { Set goal = readFrom((List) planningProblemSpec.get(GOAL)); + Set avoidIfPossible = readValuesFrom((List) planningProblemSpec.get(AVOID_IF_POSSIBLE)); List actionDefinitions = (List) planningProblemSpec.get(ACTION); @@ -110,6 +122,7 @@ public class PlanningProblem { actions.stream().forEach(action->{ actionMap.put(action.getName(), action); }); + if(planningProblemSpec.containsKey(EXPECTED_PLANS)){ List plans = (List) planningProblemSpec.get(EXPECTED_PLANS); @@ -135,15 +148,32 @@ public class PlanningProblem { return new PlanningProblem(name, background, State.initializeWith(start), - State.initializeWith(goal), actions, expectedActions); + State.initializeWith(goal), actions, avoidIfPossible, expectedActions); } else { return new PlanningProblem(name, background, State.initializeWith(start), - State.initializeWith(goal), actions); + State.initializeWith(goal),actions, avoidIfPossible); } } + public static Action readInstantiatedAction(Set actions, String instantiatedActionSpecString) throws Reader.ParsingException { + + + Parseable parseable = Parsers.newParseable(new StringReader(instantiatedActionSpecString)); + Parser parser = Parsers.newParser(Parsers.defaultConfiguration()); + + Object instantiatedActionSpec = parser.nextValue(parseable); + + Map actionMap = CollectionUtils.newMap(); + + actions.stream().forEach(action->{ + actionMap.put(action.getName(), action); + }); + + return readInstantiatedAction(actionMap, instantiatedActionSpec); + + } private static Action readInstantiatedAction(Map actionMap, Object instantiatedActionSpec) throws Reader.ParsingException { if(instantiatedActionSpec instanceof List){ @@ -229,6 +259,10 @@ public class PlanningProblem { public static Set readFrom(List objects) throws Reader.ParsingException { + if(objects==null){ + + return Sets.newSet(); + } Set formulae = objects.stream().map(x -> { try { return Reader.readFormula(x); @@ -249,6 +283,31 @@ public class PlanningProblem { } + public static Set readValuesFrom(List objects) throws Reader.ParsingException { + + if(objects==null){ + + return Sets.newSet(); + } + Set values = objects.stream().map(x -> { + try { + return Reader.readLogicValue(x); + } catch (Reader.ParsingException e) { + e.printStackTrace(); + return null; + } + }).collect(Collectors.toSet()); + + + if (values.stream().anyMatch(Objects::isNull)) { + + throw new Reader.ParsingException("Couldn't read formulae: " + objects); + } + + return values; + + + } public Set getBackground() { return background; } @@ -277,6 +336,10 @@ public class PlanningProblem { return actionMap; } + public Set getAvoidIfPossible() { + return avoidIfPossible; + } + @Override public String toString() { return "PlanningProblem{" + diff --git a/src/main/java/edu/rpi/rair/utils/Reader.java b/src/main/java/edu/rpi/rair/utils/Reader.java new file mode 100644 index 0000000..fa6d052 --- /dev/null +++ b/src/main/java/edu/rpi/rair/utils/Reader.java @@ -0,0 +1,112 @@ +package edu.rpi.rair.utils; + +import com.naveensundarg.shadow.prover.representations.formula.Formula; +import com.naveensundarg.shadow.prover.representations.value.Compound; +import com.naveensundarg.shadow.prover.representations.value.Variable; +import com.naveensundarg.shadow.prover.utils.CollectionUtils; +import edu.rpi.rair.PlanMethod; +import us.bpsm.edn.Keyword; +import us.bpsm.edn.Symbol; +import us.bpsm.edn.parser.Parseable; +import us.bpsm.edn.parser.Parser; +import us.bpsm.edn.parser.Parsers; + +import java.io.InputStream; +import java.io.InputStreamReader; +import java.io.StringReader; +import java.util.List; +import java.util.Map; +import java.util.Set; +import java.util.stream.Collectors; + +public class Reader { + + + private static final Keyword GOAL = Keyword.newKeyword("goal"); + private static final Keyword ACTIONS = Keyword.newKeyword("actions"); + private static final Keyword WHILE = Keyword.newKeyword("while"); + + public static List readPlanMethodsFrom(InputStream inputStream) throws com.naveensundarg.shadow.prover.utils.Reader.ParsingException { + + Parseable parseable = Parsers.newParseable(new InputStreamReader(inputStream)); + Parser parser = Parsers.newParser(Parsers.defaultConfiguration()); + + + + List planMethods = CollectionUtils.newEmptyList(); + + + Object current = parser.nextValue(parseable); + while(current!=Parser.END_OF_INPUT){ + + planMethods.add(readPlanMethodFrom((List) current)); + current = parser.nextValue(parseable); + } + + return planMethods; + } + + + // (def planMethod [?x ?y ?z] {:goal [...] :action [....]) + public static PlanMethod readPlanMethodFromString(String stringSpec) throws com.naveensundarg.shadow.prover.utils.Reader.ParsingException { + + Parseable parseable = Parsers.newParseable(new StringReader(stringSpec)); + Parser parser = Parsers.newParser(Parsers.defaultConfiguration()); + + Object specObj = parser.nextValue(parseable); + return readPlanMethodFrom((List) specObj); + } + + // (def planMethod [?x ?y ?z] {:goal [...] :action [....]) + public static PlanMethod readPlanMethodFrom(List planMethodSpec) throws com.naveensundarg.shadow.prover.utils.Reader.ParsingException { + + Object command = planMethodSpec.get(0); + + if(!command.toString().equals("define-method")){ + throw new AssertionError("Malformed method definition. Was expecting a 'define-method' but got "+ command); + } + Object name = planMethodSpec.get(1); + List variableObjs = (List) planMethodSpec.get(2); + + List variables = CollectionUtils.newEmptyList(); + for(Symbol varSym : variableObjs){ + + variables.add((Variable) com.naveensundarg.shadow.prover.utils.Reader.readLogicValueFromString(varSym.toString())); + + } + + Map body = (Map) planMethodSpec.get(3); + + Set goalPreconds = CollectionUtils.newEmptySet(); + Set whilePreconds = CollectionUtils.newEmptySet(); + + List actionCompounds = CollectionUtils.newEmptyList(); + + List goalPrecondSpecs = (List) body.get(GOAL); + + for(Object goalPrecondSpec : goalPrecondSpecs){ + + goalPreconds.add(com.naveensundarg.shadow.prover.utils.Reader.readFormula(goalPrecondSpec)); + } + + + List whilePrecondSpecs = (List) body.get(WHILE); + + for(Object whilePrecondSpec : whilePrecondSpecs){ + + whilePreconds.add(com.naveensundarg.shadow.prover.utils.Reader.readFormula(whilePrecondSpec)); + } + + + + List actionPrecondSpecs = (List) body.get(ACTIONS); + + for(Object actionPrecondSpec : actionPrecondSpecs){ + + actionCompounds.add((Compound) com.naveensundarg.shadow.prover.utils.Reader.readLogicValue(actionPrecondSpec)); + } + + return new PlanMethod(goalPreconds, whilePreconds, variables, actionCompounds); + } + +} diff --git a/src/main/java/edu/rpi/rair/utils/RunDemo.java b/src/main/java/edu/rpi/rair/utils/RunDemo.java index 35ddbb7..2dce90e 100644 --- a/src/main/java/edu/rpi/rair/utils/RunDemo.java +++ b/src/main/java/edu/rpi/rair/utils/RunDemo.java @@ -1,22 +1,26 @@ package edu.rpi.rair.utils; + import com.diogonunes.jcdp.color.ColoredPrinter; import com.diogonunes.jcdp.color.api.Ansi; import com.google.common.collect.Sets; -import com.naveensundarg.shadow.prover.Sandbox; -import com.naveensundarg.shadow.prover.core.Problem; -import com.naveensundarg.shadow.prover.core.Prover; + import com.naveensundarg.shadow.prover.core.Prover; import com.naveensundarg.shadow.prover.core.SnarkWrapper; +import com.naveensundarg.shadow.prover.sandboxes.Sandbox; +import com.naveensundarg.shadow.prover.utils.Problem; import com.naveensundarg.shadow.prover.utils.ProblemReader; import com.naveensundarg.shadow.prover.utils.Reader; -import edu.rpi.rair.Goal; -import edu.rpi.rair.GoalTracker; -import edu.rpi.rair.Plan; -import edu.rpi.rair.Planner; +import edu.rpi.rair.*; +import edu.rpi.rair.inducers.SimpleInducer; import edu.rpi.rair.utils.GoalTrackingProblem; +import org.apache.commons.lang3.tuple.Triple; +import javax.swing.*; +import java.awt.*; +import java.lang.reflect.Method; +import java.util.*; import java.util.List; -import java.util.Optional; -import java.util.Set; +import java.util.function.BiConsumer; +import java.util.function.BiFunction; import java.util.stream.Collectors; /** @@ -27,84 +31,100 @@ public class RunDemo { static ColoredPrinter cp = new ColoredPrinter.Builder(1, false).build(); + static List, String, String>> printQueue = new ArrayList<>(); + static { - Prover prover = new SnarkWrapper(); - try { - List problems = ProblemReader.readFrom(Sandbox.class.getResourceAsStream("firstorder-completness-tests.clj")); + Prover prover = SnarkWrapper.getInstance(); + /* try { + List problems = ProblemReader.readFrom(Sandbox.class.getResourceAsStream("../firstorder-completness-tests.clj")); problems.forEach(problem -> { - for (int i = 0; i < 30; i++) { + for (int i = 0; i < 100; i++) { prover.prove(problem.getAssumptions(), problem.getGoal()); } }); - planningProblemWarmUp(); + planningProblemWarmUp(); System.out.println("\nWARM UP DONE"); } catch (Reader.ParsingException e) { e.printStackTrace(); } +*/ + } + + public static void main(String[] args) throws Reader.ParsingException, InterruptedException { + planningProblemWarmUp(); + + System.out.println(); + + Visualizer.setShouldVisualize(false); + + runProblem("seriated_challenge_1.clj"); + // runProblem("seriated_challenge_2.clj"); + } - public static void main(String[] args) throws Reader.ParsingException { + private static void runProblem(String name) throws Reader.ParsingException { + List goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream(name))); + GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0); - System.out.println(); + GoalTracker goalTracker = new GoalTracker(goalTrackingProblem.getPlanningProblem(), goalTrackingProblem.getPlanningProblem().getBackground(), + goalTrackingProblem.getPlanningProblem().getStart(), + goalTrackingProblem.getPlanningProblem().getActions()); - List goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("seriated_challenge_1.clj"))); + long start = System.currentTimeMillis(); + + Goal g1 = goalTrackingProblem.getGoalNamed("G1"); - GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0); - - GoalTracker goalTracker = new GoalTracker(goalTrackingProblem.getPlanningProblem().getBackground(), - goalTrackingProblem.getPlanningProblem().getStart(), - goalTrackingProblem.getPlanningProblem().getActions()); - - long start = System.currentTimeMillis(); - - Goal g1 = goalTrackingProblem.getGoalNamed("G1"); - - /* - Goal g2 = goalTrackingProblem.getGoalNamed("G2"); + tryAndAddGoal(g1, goalTracker); - Goal g3 = goalTrackingProblem.getGoalNamed("G3"); - Goal g4 = goalTrackingProblem.getGoalNamed("G4"); - Goal g5 = goalTrackingProblem.getGoalNamed("G5"); - -*/ - - tryAndAddGoal(g1, goalTracker); - - /* tryAndAddGoal(g2, goalTracker); + long end = System.currentTimeMillis(); - tryAndAddGoal(g2, goalTracker); + System.out.println("***************************"); + cp.setAttribute(Ansi.Attribute.BOLD); + cp.println("AVAILABLE GOALS AND CONSTRAINTS"); + cp.clear(); + System.out.println("------------------------------"); - tryAndAddGoal(g3, goalTracker); + goalTrackingProblem.getGoals().forEach(goal->{ + System.out.println(goal); - tryAndAddGoal(g4, goalTracker); + }); - tryAndAddGoal(g5, goalTracker); -*/ + System.out.println("***************************"); - long end = System.currentTimeMillis(); + Visualizer.unspool(200); + for (int i = 0; i < printQueue.size(); i++) { - cp.println("--------------------------"); - cp.setForegroundColor(Ansi.FColor.CYAN); + Triple, String, String> task = printQueue.get(i); - cp.print("Time Taken:"); - cp.clear(); - cp.print(" "); - cp.setAttribute(Ansi.Attribute.BOLD); - cp.print((end - start) / 1000.0 + "s"); + task.getLeft().accept(task.getMiddle(), task.getRight()); + } + cp.println("--------------------------"); + cp.setForegroundColor(Ansi.FColor.CYAN); + cp.print("Time Taken:"); + cp.clear(); + cp.print(" "); + cp.setAttribute(Ansi.Attribute.BOLD); + cp.print((end - start) / 1000.0 + "s"); + cp.println(" "); + + cp.println("--------------------------"); + cp.println(" "); + cp.println(" "); + cp.println(" "); } public static void planningProblemWarmUp() throws Reader.ParsingException { @@ -118,7 +138,7 @@ public class RunDemo { GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0); - GoalTracker goalTracker = new GoalTracker(goalTrackingProblem.getPlanningProblem().getBackground(), + GoalTracker goalTracker = new GoalTracker(goalTrackingProblem.getPlanningProblem(), goalTrackingProblem.getPlanningProblem().getBackground(), goalTrackingProblem.getPlanningProblem().getStart(), goalTrackingProblem.getPlanningProblem().getActions()); @@ -154,34 +174,47 @@ public class RunDemo { static void tryAndAddGoal(Goal g, GoalTracker goalTracker) { - System.out.println("========================"); - printInfo("Trying to Add Goal:", g.getName()); + Inducer simpleInducer = new SimpleInducer(); - Set oldGoals = goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()); + System.out.println("========================"); + printInfoLater("Trying to Add Goal or Constraint:", ""); + printInfoLater(" ", g.toString()); + + Set oldGoals = goalTracker.getCurrentGoals().stream().collect(Collectors.toSet()); Optional possibleGoalPlan = goalTracker.adoptGoal(g); if (possibleGoalPlan.isPresent()) { - printSuccess("Successfully added:", g.getName()); - printDebug1("Current Goals:", goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()).toString()); + simpleInducer.induce(goalTracker.getProblem(), goalTracker.getProblem().getStart(), g, possibleGoalPlan.get()); - Set newGoals = goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()); + printSuccessLater("Successfully added:", g.getName()); + printDebug1Later("Current Goals and Constraint:", "\n" + goalTracker.getCurrentGoals().stream().collect(Collectors.toSet()).toString()); - if(!Sets.difference(oldGoals, newGoals).isEmpty()){ - printDropped("Dropped Goals:" + Sets.difference(oldGoals, newGoals)); + Set newGoals = goalTracker.getCurrentGoals().stream().collect(Collectors.toSet()); + + if (!Sets.difference(oldGoals, newGoals).isEmpty()) { + printDroppedLater("", "Dropped Goals and Contraints:" + Sets.difference(oldGoals, newGoals)); } Plan plan = possibleGoalPlan.get(); - printDebug2("Plan:", plan.getActions().isEmpty() ? "No plan needed. Already satisfied." : plan.getActions().toString()); + printDebug2Later("Plan:", plan.getActions().isEmpty() ? "No plan needed. Already satisfied." : "\n" + plan.toString()); } else { - printFailure("Could not add " + g.getName()); - printDebug1("Current Goals: ", goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()).toString()); + printFailureLater("", "Could not add " + g); + + printDebug1Later("Current Goals and Contraints: ", goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()).toString()); } } + static void printInfoLater(String header, String message) { + + + printQueue.add(Triple.of((x, y) -> RunDemo.printInfo(x, y), header, message)); + + } + static void printInfo(String header, String message) { cp.setForegroundColor(Ansi.FColor.WHITE); @@ -195,6 +228,14 @@ public class RunDemo { cp.clear(); } + static void printSuccessLater(String header, String message) { + + + printQueue.add(Triple.of((x, y) -> RunDemo.printSuccess(x, y), header, message)); + + } + + static void printSuccess(String header, String message) { cp.setForegroundColor(Ansi.FColor.BLACK); @@ -209,6 +250,14 @@ public class RunDemo { } + static void printDebug1Later(String header, String message) { + + + printQueue.add(Triple.of((x, y) -> RunDemo.printDebug1(x, y), header, message)); + + } + + static void printDebug1(String header, String message) { cp.setForegroundColor(Ansi.FColor.BLACK); @@ -222,6 +271,13 @@ public class RunDemo { cp.clear(); } + static void printDebug2Later(String header, String message) { + + + printQueue.add(Triple.of((x, y) -> RunDemo.printDebug2(x, y), header, message)); + + } + static void printDebug2(String header, String message) { cp.setForegroundColor(Ansi.FColor.BLACK); @@ -235,7 +291,14 @@ public class RunDemo { cp.clear(); } - static void printFailure(String message) { + static void printFailureLater(String header, String message) { + + + printQueue.add(Triple.of((x, y) -> RunDemo.printFailure(x, y), header, message)); + + } + + static void printFailure(String header, String message) { cp.setForegroundColor(Ansi.FColor.WHITE); cp.setBackgroundColor(Ansi.BColor.RED); //setting format @@ -245,7 +308,16 @@ public class RunDemo { cp.clear(); } - static void printDropped(String message) { + + static void printDroppedLater(String header, String message) { + + + printQueue.add(Triple.of((x, y) -> RunDemo.printDropped(x, y), header, message)); + + } + + + static void printDropped(String header, String message) { cp.setForegroundColor(Ansi.FColor.WHITE); cp.setBackgroundColor(Ansi.BColor.RED); //setting format diff --git a/src/main/java/edu/rpi/rair/utils/Sandbox.java b/src/main/java/edu/rpi/rair/utils/Sandbox.java new file mode 100644 index 0000000..5902fed --- /dev/null +++ b/src/main/java/edu/rpi/rair/utils/Sandbox.java @@ -0,0 +1,31 @@ +package edu.rpi.rair.utils; + +import edu.rpi.rair.PlanMethod; +import edu.rpi.rair.Planner; + +import java.util.List; + +/** + * Created by naveensundarg on 12/22/17. + */ +public class Sandbox { + + public static void main(String[] args) throws com.naveensundarg.shadow.prover.utils.Reader.ParsingException { + + PlanMethod seriatedPlanMethod = (Reader.readPlanMethodsFrom(Sandbox.class.getResourceAsStream("../problems/seriated/methods.clj"))).get(0); + + + List goalTrackingProblemList1 = (GoalTrackingProblem.readFromFile(Sandbox.class.getResourceAsStream("../problems/seriated/seriated_challenge_1.clj"))); + + + System.out.println(seriatedPlanMethod.apply(goalTrackingProblemList1.get(0).getPlanningProblem().getBackground(), + goalTrackingProblemList1.get(0).getPlanningProblem().getStart().getFormulae(), + goalTrackingProblemList1.get(0).getGoalNamed("G1").getGoalState().getFormulae(), + goalTrackingProblemList1.get(0).getPlanningProblem().getActions() + + )); + + + + } +} diff --git a/src/main/java/edu/rpi/rair/utils/Visualizer.java b/src/main/java/edu/rpi/rair/utils/Visualizer.java new file mode 100644 index 0000000..9d986a5 --- /dev/null +++ b/src/main/java/edu/rpi/rair/utils/Visualizer.java @@ -0,0 +1,177 @@ +package edu.rpi.rair.utils; + +import com.diogonunes.jcdp.color.ColoredPrinter; +import com.diogonunes.jcdp.color.api.Ansi; + +import java.util.ArrayDeque; +import java.util.Queue; +import java.util.concurrent.atomic.AtomicBoolean; + +/** + * Created by naveensundarg on 9/29/17. + */ +public class Visualizer { + + + private Visualizer(){ + throw new AssertionError("Cannot instantiate the Visualizer"); + + + } + static ColoredPrinter cp = new ColoredPrinter.Builder(1, false).build(); + + + static Queue spool = new ArrayDeque<>(); + private static final AtomicBoolean shouldVisualize; + private static int depth = 0; + static { + shouldVisualize = new AtomicBoolean(true); + } + + public static boolean getShouldVisualize() { + return shouldVisualize.get(); + } + + public static void setShouldVisualize(boolean visualize) { + shouldVisualize.set(visualize); + + } + + + public static void nested(String name){ + + StringBuffer stringBuffer = new StringBuffer(""); + if(shouldVisualize.get()){ + for(int i = 0; i{ + // try { + // Thread.sleep(delay); + cp.println(x); + /* } catch (InterruptedException e) { + e.printStackTrace(); + }*/ + + }); + } + + public static void push(){ + + depth = depth + 1; + } + + public static void pop(){ + + depth = depth - 1; + } + + public static void reset(){ + + depth = 0; + } + + + public static void print(String message) { + cp.print(message); + cp.clear(); + } + + + public static void printRed(String message) { + + cp.setForegroundColor(Ansi.FColor.RED); + cp.setAttribute(Ansi.Attribute.BOLD); + cp.print(message); + cp.clear(); + } + + public static void printInfo(String header, String message) { + + cp.setForegroundColor(Ansi.FColor.WHITE); + cp.setBackgroundColor(Ansi.BColor.BLUE); //setting format + cp.print(header); + cp.clear(); + cp.print(" "); + cp.setAttribute(Ansi.Attribute.BOLD); + cp.print(message); + cp.println(""); + cp.clear(); + } + + public static void printSuccess(String header, String message) { + + cp.setForegroundColor(Ansi.FColor.BLACK); + cp.setBackgroundColor(Ansi.BColor.GREEN); //setting format + cp.print(header); + cp.clear(); + cp.print(" "); + cp.setAttribute(Ansi.Attribute.BOLD); + cp.print(message); + cp.println(""); + cp.clear(); + } + + + public static void printDebug1(String header, String message) { + + cp.setForegroundColor(Ansi.FColor.BLACK); + cp.setBackgroundColor(Ansi.BColor.YELLOW); //setting format + cp.print(header); + cp.clear(); + cp.print(" "); + cp.setAttribute(Ansi.Attribute.BOLD); + cp.print(message); + cp.println(""); + cp.clear(); + } + + public static void printDebug2(String header, String message) { + + cp.setForegroundColor(Ansi.FColor.BLACK); + cp.setBackgroundColor(Ansi.BColor.MAGENTA); //setting format + cp.print(header); + cp.clear(); + cp.print(" "); + cp.setAttribute(Ansi.Attribute.BOLD); + cp.print(message); + cp.println(""); + cp.clear(); + } + + public static void printFailure(String message) { + + cp.setForegroundColor(Ansi.FColor.WHITE); + cp.setBackgroundColor(Ansi.BColor.RED); //setting format + cp.print(message); + cp.clear(); + cp.println(""); + cp.clear(); + } + + public static void printDropped(String message) { + + cp.setForegroundColor(Ansi.FColor.WHITE); + cp.setBackgroundColor(Ansi.BColor.RED); //setting format + cp.print("Dropped Goals:"); + cp.clear(); + cp.print(" "); + cp.setAttribute(Ansi.Attribute.BOLD); + cp.print(message); + cp.println(""); + cp.clear(); + } + +} diff --git a/src/main/resources/edu/rpi/rair/completeness_problems.clj b/src/main/resources/edu/rpi/rair/completeness_problems.clj index 0a016df..36724b3 100644 --- a/src/main/resources/edu/rpi/rair/completeness_problems.clj +++ b/src/main/resources/edu/rpi/rair/completeness_problems.clj @@ -2,15 +2,12 @@ :background [p] :start [q] :goal [r] - :actions - [(define-action a1 () - {:preconditions [(or q r)] - :additions [r] - :deletions [q]})] - - :expected-plans ([a1]) - } + :actions [(define-action a1 () + {:preconditions [(or q r)] + :additions [r] + :deletions [q]})] + :expected-plans ([a1])} {:name "simple killing" @@ -18,14 +15,12 @@ :start [(forall ?x (alive ?x))] :goal [(forall ?x (dead ?x))] :actions - [(define-action kill () - {:preconditions [(alive ?x)] - :additions [(dead ?x)] - :deletions [(alive ?x)]})] + [(define-action kill () + {:preconditions [(alive ?x)] + :additions [(dead ?x)] + :deletions [(alive ?x)]})] - :expected-plans ([kill]) - - } + :expected-plans ([kill])} {:name "thirsty" @@ -33,18 +28,16 @@ :start [thirsty] :goal [(not thirsty)] :actions - [(define-action drink () - {:preconditions [thirsty] - :additions [(not thirsty)] - :deletions [thirsty]}) - (define-action eat () - {:preconditions [hungry] - :additions [(not hungry)] - :deletions [hungry]})] + [(define-action drink () + {:preconditions [thirsty] + :additions [(not thirsty)] + :deletions [thirsty]}) + (define-action eat () + {:preconditions [hungry] + :additions [(not hungry)] + :deletions [hungry]})] - :expected-plans ([drink]) - - } + :expected-plans ([drink])} {:name "hungry" @@ -53,18 +46,17 @@ :goal [(not hungry)] :actions - [(define-action drink () - {:preconditions [thirsty] - :additions [(not thirsty)] - :deletions [thirsty]}) + [(define-action drink () + {:preconditions [thirsty] + :additions [(not thirsty)] + :deletions [thirsty]}) - (define-action eat () - {:preconditions [hungry] - :additions [(not hungry)] - :deletions [hungry]})] + (define-action eat () + {:preconditions [hungry] + :additions [(not hungry)] + :deletions [hungry]})] - :expected-plans ([eat]) - } + :expected-plans ([eat])} {:name "hungry and thirsty" @@ -72,19 +64,18 @@ :start [hungry thirsty] :goal [(not (or hungry thirsty))] :actions - [(define-action drink () - {:preconditions [thirsty] - :additions [(not thirsty)] - :deletions [thirsty]}) + [(define-action drink () + {:preconditions [thirsty] + :additions [(not thirsty)] + :deletions [thirsty]}) - (define-action eat () - {:preconditions [hungry] - :additions [(not hungry)] - :deletions [hungry]})] + (define-action eat () + {:preconditions [hungry] + :additions [(not hungry)] + :deletions [hungry]})] :expected-plans ([eat drink] - [drink eat]) - } + [drink eat])} {:name "hungry and thirsty" :background [] @@ -92,94 +83,141 @@ :goal [work-finished] :actions - [(define-action drink () - {:preconditions [thirsty] - :additions [(not thirsty)] - :deletions [thirsty]}) + [(define-action drink () + {:preconditions [thirsty] + :additions [(not thirsty)] + :deletions [thirsty]}) - (define-action eat () - {:preconditions [hungry] - :additions [(not hungry)] - :deletions [hungry]}) + (define-action eat () + {:preconditions [hungry] + :additions [(not hungry)] + :deletions [hungry]}) - (define-action work () - {:preconditions [(and (not hungry) (not thirsty))] - :additions [work-finished] - :deletions [work-unfinished]})] + (define-action work () + {:preconditions [(and (not hungry) (not thirsty))] + :additions [work-finished] + :deletions [work-unfinished]})] :expected-plans ([eat drink work] [drink eat work])} - - - -{:name "demo 1" - :background [ - (not (= room1 room2)) - (not (= prisoner commander)) - (not (= self prisoner)) - (not (= self commander)) - (person prisoner) - (person commander) - ] - :start [(in self room1) - (in commander room2) - (in prisoner room1) - (open (door room2)) - (not (open (door room1)))] - - :goal [(interrogates commander prisoner)] - +{:name "Heinz Dilemma" + :background [(cures radium-drug-x cancerx)] + :start [(sick (wife heinz) cancerx) + (= 5000 (cost radium-drug-x)) + (not (can-spend 5000)) + (not (possess radium-drug-x))] + :goal [(healthy (wife heinz))] :actions - [(define-action open-door [?room] - {:preconditions [(not (open (door ?room)))] - :additions [(open (door ?room))] - :deletions [(not (open (door ?room)))]}) + + [(define-action administer-medicine [?medicine ?condition ?person] + {:preconditions [(sick ?person ?condition) + (cures ?medicine ?condition) + (possess ?medicine)] + :additions [(healthy ?person)] + :deletions [(sick ?person ?condition)]}) + + (define-action buy-medicine [?medicine] + {:preconditions [(can-spend (cost ?medicine))] + :additions [(possess ?medicine)] + :deletions [(not (possess ?medicine))]}) + (define-action steal-medicine [?medicine] + {:preconditions [(not (possess ?medicine))] + :additions [(possess ?medicine)] + :deletions [(not (possess ?medicine))]}) - (define-action accompany [?person ?room1 ?room2] - {:preconditions [(not (= ?room1 ?room2)) - (in ?person ?room1) - (in self ?room1) - (open (door ?room1)) - (open (door ?room2))] - :additions [(in ?person ?room2) - (in self ?room2)] + (define-action finance [?amount] + {:preconditions [(not (can-spend ?amount))] + :additions [(can-spend ?amount)] + :deletions [(not (can-spend ?amount))]})] - :deletions [(in ?person ?room1) - (in self ?room1)]}) + :expected-plans ([buy-medicine administer-medicine])} - (define-action move [?person ?room2 ?room1] - {:preconditions [(not (= ?room1 ?room2)) - (in ?person ?room2) - (open (door ?room1)) - (open (door ?room2))] - :additions [(in ?person ?room1)] +{:name "belief intro" + :background [(Proposition god-exists) + (forall [?p] (if (Proposition ?p) (or (True ?p) (False ?p)))) + (forall [?p] (iff (True ?p) (not (False ?p)))) + (forall [?p] (iff (True ?p) (HasSupport ?p))) + (False god-exists)] + :start [] + :goal [(Declaration god-exists)] + :actions + [(define-action declare-P [?p] + {:preconditions [(Belief ?p)] + :additions [(Declaration ?p)] + :deletions [(Private ?p)]}) - :deletions [(in ?person ?room2)]}) + (define-action believe-with-support [?p] + {:preconditions [(Proposition ?p) + (HasSupport ?p)] + :additions [(Belief ?p)] + :deletions []}) - (define-action get-interrogated [?room] - {:preconditions [(in commander ?room) - (in prisoner ?room)] + (define-action believe-without-support [?p] + {:preconditions [(Proposition ?p)] + :additions [(Belief ?p)] + :deletions []})] - :additions [(interrogates commander prisoner)] + :expected-plans ([believe-P declare-P])} - :deletions []}) +{:name "reasoning 1" + :background [] + :start [(! p) (! q)] + :goal [(! (and p q))] + + :actions [(define-action and-intro [?p ?q] + {:preconditions [(! ?p) (! ?q)] + :additions [(! (and ?p ?q))] + :deletions []}) + (define-action cond-elim [?p ?q] + {:preconditions [(! (if ?p ?q)) (! ?p)] + :additions [(! ?q)] + :deletions []})] + + :expected-plans ([and-intro])} + + +{:name "reasoning 2" + :background [] + :start [(! p) (! q) + (! (if (and p q) r))] + :goal [(! r)] + + :actions [(define-action and-intro [?p ?q] + {:preconditions [(! ?p) (! ?q)] + :additions [(! (and ?p ?q))] + :deletions []}) + (define-action cond-elim [?p ?q] + {:preconditions [(! (if ?p ?q)) (! ?p)] + :additions [(! ?q)] + :deletions []})] + + :expected-plans ([and-intro])} + +{:name "reasoning 3" + :background [] + :start [(! A) (! B) + (Prop S) + (! (if (and A B) C)) ] + :goal [(! (if S C) )] - :expected-plans ([(open-door room1) - (move commander room2 room1) - (get-interrogated room1)] - - [(open-door room1) - (move prisoner room1 room2) - (get-interrogated room2)] - - [(open-door room1) - (accompany prisoner room1 room2) - (get-interrogated room2)])} + :actions [(define-action and-intro [?p ?q] + {:preconditions [(! ?p) (! ?q)] + :additions [(! (and ?p ?q))] + :deletions []}) + (define-action cond-elim [?p ?q] + {:preconditions [(! (if ?p ?q)) (! ?p)] + :additions [(! ?q)] + :deletions []}) + (define-action cond-intro [?p ?q] + {:preconditions [ (Prop ?p) (! ?q)] + :additions [(! (if ?p ?q))] + :deletions []})] + :expected-plans ([and-intro])} diff --git a/src/main/resources/edu/rpi/rair/file.clj b/src/main/resources/edu/rpi/rair/file.clj new file mode 100644 index 0000000..34225af --- /dev/null +++ b/src/main/resources/edu/rpi/rair/file.clj @@ -0,0 +1,36 @@ +{:definitions + {:name "Blockworld" + + :background [] + + :start [(Clear A) + (Clear B) + (Clear C) + (On A Table) + (On B Table) + (On C Table)] + + :goal [] + + :actions [(define-action stack [?x ?y] + {:preconditions [(On ?x Table) + (On ?y Table) + (Clear ?x) + (Clear ?y)] + :additions [(On ?x ?y)] + :deletions [(Clear ?y) + (On ?x Table)]}) + + (define-action unstack [?x ?y] + {:preconditions [(On ?x ?y) + (Clear ?x)] + :additions [(On ?x Table) + (Clear ?y)] + :deletions [(On ?x ?y)]})] + } + + :goals {G1 {:priority 1.0 + :state [(On A B)]} + G2 {:priority 1.0 + :state [(On C A)]}} +} diff --git a/src/main/resources/edu/rpi/rair/problems/heinz/heinz_challenge.clj b/src/main/resources/edu/rpi/rair/problems/heinz/heinz_challenge.clj new file mode 100644 index 0000000..3c05bc6 --- /dev/null +++ b/src/main/resources/edu/rpi/rair/problems/heinz/heinz_challenge.clj @@ -0,0 +1,60 @@ +{:definitions + {:name "Heinz Dilemma" + :background [(cures radium-drug-x cancerx)] + :start [(not steal) + + + (collateral income) + + + + (sick (wife heinz) cancerx) + + + (= 5000 (cost radium-drug-x)) + (not (can-spend 5000)) + (not (possess radium-drug-x))] + + :actions + + [(define-action administer-medicine [?medicine ?condition ?person] + {:preconditions [(sick ?person ?condition) + (cures ?medicine ?condition) + (possess ?medicine)] + :additions [(healthy ?person)] + :deletions [(sick ?person ?condition)]}) + + (define-action buy-medicine [?medicine] + {:preconditions [(not (possess ?medicine)) + (can-spend (cost ?medicine))] + :additions [(possess ?medicine)] + :deletions [(not (possess ?medicine))]}) + + (define-action steal-medicine [?medicine] + {:preconditions [(not (can-spend (cost ?medicine))) + (not (possess ?medicine))] + :additions [(possess ?medicine) + steal] + :deletions [(not steal) + (not (possess ?medicine))]}) + + (define-action apply-loan [?amount] + {:preconditions [ (not (can-spend ?amount))] + :additions [(approved (loan ?amount))] + :deletions []}) + + (define-action finance [?amount ?with-collateral] + {:preconditions [(collateral ?with-collateral) + (approved (loan ?amount)) (not (can-spend ?amount))] + :additions [(can-spend ?amount) + have-loan] + :deletions [(not (can-spend ?amount))]})]} + + :goals {G1 {:priority 1.0 + :description "Don't steal." + :state [(not steal)]} + + + G2 {:priority 2.0 + :description "My wife should be healthy" + :state [(healthy (wife heinz))]}}} diff --git a/src/main/resources/edu/rpi/rair/goal_management_1.clj b/src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_1.clj similarity index 100% rename from src/main/resources/edu/rpi/rair/goal_management_1.clj rename to src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_1.clj diff --git a/src/main/resources/edu/rpi/rair/goal_management_2.clj b/src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_2.clj similarity index 100% rename from src/main/resources/edu/rpi/rair/goal_management_2.clj rename to src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_2.clj diff --git a/src/main/resources/edu/rpi/rair/goal_management_3.clj b/src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_3.clj similarity index 100% rename from src/main/resources/edu/rpi/rair/goal_management_3.clj rename to src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_3.clj diff --git a/src/main/resources/edu/rpi/rair/goal_management_4.clj b/src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_4.clj similarity index 100% rename from src/main/resources/edu/rpi/rair/goal_management_4.clj rename to src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_4.clj diff --git a/src/main/resources/edu/rpi/rair/goal_management_5.clj b/src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_5.clj similarity index 100% rename from src/main/resources/edu/rpi/rair/goal_management_5.clj rename to src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_5.clj diff --git a/src/main/resources/edu/rpi/rair/goal_management_6.clj b/src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_6.clj similarity index 100% rename from src/main/resources/edu/rpi/rair/goal_management_6.clj rename to src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_6.clj diff --git a/src/main/resources/edu/rpi/rair/problems/seriated/methods.clj b/src/main/resources/edu/rpi/rair/problems/seriated/methods.clj new file mode 100644 index 0000000..951aadd --- /dev/null +++ b/src/main/resources/edu/rpi/rair/problems/seriated/methods.clj @@ -0,0 +1,9 @@ +;; (removeFrom ?x ?y) => "Remove ?x from ?y" +;; (placeInside ?x ?y) ==> "Place ?x inside ?y" + +(define-method planMethod [?b ?c ?d] + {:goal [(In ?b ?c) (In ?c ?d)] + :while [(In ?b ?d) (Empty ?c) + (< (size ?c) (size ?d)) + (< (size ?b) (size ?c))] + :actions [(removeFrom ?b ?d) (placeInside ?b ?c) (placeInside ?c ?d)]}) \ No newline at end of file diff --git a/src/main/resources/edu/rpi/rair/seriated_challenge_1.clj b/src/main/resources/edu/rpi/rair/problems/seriated/seriated_challenge_1.clj similarity index 83% rename from src/main/resources/edu/rpi/rair/seriated_challenge_1.clj rename to src/main/resources/edu/rpi/rair/problems/seriated/seriated_challenge_1.clj index 10c9c5b..7696e49 100644 --- a/src/main/resources/edu/rpi/rair/seriated_challenge_1.clj +++ b/src/main/resources/edu/rpi/rair/problems/seriated/seriated_challenge_1.clj @@ -21,16 +21,18 @@ (< (size a) (size b)) (< (size b) (size c)) (< (size c) (size d)) - (< (size d) (size e))] + (< (size d) (size e)) + (< (size e) (size f)) + (< (size f) (size g)) + (< (size g) (size h))] :start [(In a b) (In b d) - (In d e) - (Empty c)] + (Empty c)] - :goal [] + :goal [ ] :actions [(define-action placeInside [?x ?y] {:preconditions [(< (size ?x) (size ?y)) @@ -41,20 +43,15 @@ (define-action removeFrom [?x ?y] {:preconditions [(In ?x ?y)] :additions [(Empty ?y)] - :deletions [(In ?x ?y)]} )] - - - - } + :deletions [(In ?x ?y)]})]} :goals {G1 {:priority 1.0 :state [(In a b) (In b c) - (In c d) - (In d e)]}} - + (In c d)]}} +;;(removeFrom b d) (placeInside b c) (placeInside c d) } diff --git a/src/main/resources/edu/rpi/rair/problems/seriated/seriated_challenge_2.clj b/src/main/resources/edu/rpi/rair/problems/seriated/seriated_challenge_2.clj new file mode 100644 index 0000000..ac3aea9 --- /dev/null +++ b/src/main/resources/edu/rpi/rair/problems/seriated/seriated_challenge_2.clj @@ -0,0 +1,70 @@ + + {:definitions + {:name "Seriated Cup Challenge 1" + + :background [ ;; Transitivity of < + (forall [?x ?y ?z] + (if (and (< (size ?x) (size ?y)) + (< (size ?y) (size ?z))) + (< (size ?x) (size ?z)))) + ;; Asymmetry of < + (forall [?x ?y] + (iff (< (size ?x) (size ?y)) + (not (< (size ?y) (size ?x))))) + + ;; If there is something inside a cup, it is not empty. + (forall [?y] + (if (exists [?x] (In ?x ?y)) + (not (Empty ?y)))) + + ;;; Sizes of cups + (< (size a) (size b)) + (< (size b) (size c)) + (< (size c) (size d)) + (< (size d) (size e)) + (< (size e) (size f)) + (< (size f) (size g)) + (< (size g) (size h))] + + + :start [(In a b) + (In b d) + (In d e) + (In e f) + (In f g) + (In g h) + (Empty c)] + + + :goal [ ] + + :actions [(define-action placeInside [?x ?y] + {:preconditions [(< (size ?x) (size ?y)) + (Empty ?y)] + :additions [(In ?x ?y)] + :deletions [(Empty ?y)]}) + + (define-action removeFrom [?x ?y] + {:preconditions [(In ?x ?y)] + :additions [(Empty ?y)] + :deletions [(In ?x ?y)]} )] + + + + } + + :goals {G1 {:priority 1.0 + :state [(In a b) + (In b c) + (In c d) + (In d e) + (In e f) + (In f g) + (In g h) +]}} + + +;;(removeFrom b d) (placeInside b c) (placeInside c d) + + + } diff --git a/src/main/resources/edu/rpi/rair/self_deception.clj b/src/main/resources/edu/rpi/rair/self_deception.clj new file mode 100644 index 0000000..e7bc362 --- /dev/null +++ b/src/main/resources/edu/rpi/rair/self_deception.clj @@ -0,0 +1,62 @@ +{:definitions + {:name "belief intro" + :background [(forall [?p] (if (Proposition ?p) (or (True ?p) (False ?p)))) + (forall [?p] (iff (True ?p) (not (False ?p)))) + (forall [?p] (if (True ?p) (HasSupport ?p))) + + (Proposition (healthy salad)) + (Proposition (healthy ice-cream)) + + (True (healthy salad)) + (False (healthy ice-cream)) + (Be Healthy) + (iff (Be Healthy) (not (Eat ice-cream))) + + (Source dubious-science-journal) + (Read (healthy ice-cream) dubious-science-journal)] + :start [] + + :avoid-if-possible [believe-without-support] + + :actions [(define-action declare-P [?p] + {:preconditions [(Belief ?p)] + :additions [(Declaration ?p)] + :deletions [(Private ?p)]}) + + (define-action believe-with-support [?p] + {:preconditions [(Proposition ?p) + (HasSupport ?p)] + :additions [(Belief ?p)] + :deletions []}) + + (define-action add-support [?p] + {:preconditions [(Proposition ?p) + (Read ?p ?source) + (Trusted ?source)] + :additions [(HasSupport ?p)] + :deletions []}) + + (define-action assume-trust [?source] + {:preconditions [(Source ?source)] + :additions [(Trusted ?source)] + :deletions []}) + + (define-action believe-without-support [?p] + {:preconditions [(Proposition ?p)] + :additions [(Belief ?p)] + :deletions []}) + + (define-action eat [?p] + {:preconditions [(Belief (healthy ?p))] + :additions [(Eat ?p)] + :deletions []})]} + + :avoid-if-possible [believe-without-support] + :goals {G1 {:priority 1.0 + :description "Be Healthy" + :state [(Be Healthy)]} + + + G2 {:priority 2.0 + :description "Eat Ice Cream" + :state [(Eat ice-cream)]}}} diff --git a/src/test/java/edu/rpi/rair/DepthFirstPlannerTest.java b/src/test/java/edu/rpi/rair/DepthFirstPlannerTest.java index 1586553..6289a67 100644 --- a/src/test/java/edu/rpi/rair/DepthFirstPlannerTest.java +++ b/src/test/java/edu/rpi/rair/DepthFirstPlannerTest.java @@ -33,7 +33,9 @@ public class DepthFirstPlannerTest { Planner depthFirstPlanner = new DepthFirstPlanner(); - PlanningProblem planningProblem = planningProblemList.get(5); + PlanningProblem planningProblem = planningProblemList.stream().filter(problem -> problem.getName().equals("reasoning 3")).findFirst().get(); + + depthFirstPlanner.plan(planningProblem.getBackground(), planningProblem.getActions(), planningProblem.getStart(), planningProblem.getGoal()).get().forEach(System.out::println); } diff --git a/src/test/java/edu/rpi/rair/GoalTrackerTest.java b/src/test/java/edu/rpi/rair/GoalTrackerTest.java index a6bc7bf..bc0084b 100644 --- a/src/test/java/edu/rpi/rair/GoalTrackerTest.java +++ b/src/test/java/edu/rpi/rair/GoalTrackerTest.java @@ -17,12 +17,12 @@ public class GoalTrackerTest { public static void main(String[] args) throws Reader.ParsingException { - List goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_1.clj"))); + List goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_6.clj"))); GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0); - GoalTracker goalTracker = new GoalTracker(goalTrackingProblem.getPlanningProblem().getBackground(), + GoalTracker goalTracker = new GoalTracker(goalTrackingProblem.getPlanningProblem(), goalTrackingProblem.getPlanningProblem().getBackground(), goalTrackingProblem.getPlanningProblem().getStart(), goalTrackingProblem.getPlanningProblem().getActions()); diff --git a/src/test/java/edu/rpi/rair/HeinzGoalTrackerTest.java b/src/test/java/edu/rpi/rair/HeinzGoalTrackerTest.java new file mode 100644 index 0000000..1db9d1f --- /dev/null +++ b/src/test/java/edu/rpi/rair/HeinzGoalTrackerTest.java @@ -0,0 +1,41 @@ +package edu.rpi.rair; + +import com.diogonunes.jcdp.color.ColoredPrinter; +import com.diogonunes.jcdp.color.api.Ansi; +import com.naveensundarg.shadow.prover.utils.Reader; +import edu.rpi.rair.utils.GoalTrackingProblem; + +import java.util.List; + +/** + * Created by naveensundarg on 1/15/17. + */ +public class HeinzGoalTrackerTest { + + + public static void main(String[] args) throws Reader.ParsingException { + + List goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("heinz_challenge.clj"))); + + + GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0); + + GoalTracker goalTracker = new GoalTracker(goalTrackingProblem.getPlanningProblem(), goalTrackingProblem.getPlanningProblem().getBackground(), + goalTrackingProblem.getPlanningProblem().getStart(), + goalTrackingProblem.getPlanningProblem().getActions()); + + + ColoredPrinter cp = new ColoredPrinter.Builder(1, false).build(); + + + cp.setForegroundColor(Ansi.FColor.WHITE); + cp.setBackgroundColor(Ansi.BColor.BLUE); //setting format + cp.println("Adding goal G1"); + cp.clear(); + + goalTracker.adoptGoal(goalTrackingProblem.getGoalNamed("G1")); + + + + } +} \ No newline at end of file