rairlab/Spectra
1
0
Fork 0
mirror of https://github.com/RAIRLab/Spectra.git synced 2024-11-22 00:46:29 -05:00
Code Issues Projects Releases Packages Wiki Activity

Support for plan methods

Browse source
This commit is contained in:
Naveen Sundar Govindarajulu 2017-12-22 17:44:24 -08:00
parent 381bbc60af
commit 9bdf4fe029
39 changed files with 1539 additions and 229 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
pom.xml
View file

@ -14,7 +14,7 @@
<dependency> <dependency>
<groupId>logic</groupId> <groupId>logic</groupId>
<artifactId>prover</artifactId> <artifactId>prover</artifactId>
<version>0.09</version> <version>0.84</version>
</dependency> </dependency>
<dependency> <dependency>

2
snark-20120808r02/snark-interface.lisp
View file

@ -91,7 +91,7 @@
(snark:initialize :verbose verbose) (snark:initialize :verbose verbose)
(if (not verbose) (snark-deverbose) ) (if (not verbose) (snark-deverbose) )
(temp-sorts) (temp-sorts)
(snark:run-time-limit 0.05) (snark:run-time-limit 1)
(snark:assert-supported t) (snark:assert-supported t)
(snark:assume-supported t) (snark:assume-supported t)
(snark:prove-supported t) (snark:prove-supported t)

9
src/main/java/edu/rpi/rair/Action.java
View file

@ -1,13 +1,13 @@
package edu.rpi.rair; 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.And;
import com.naveensundarg.shadow.prover.representations.formula.Formula; import com.naveensundarg.shadow.prover.representations.formula.Formula;
import com.naveensundarg.shadow.prover.representations.value.Compound; import com.naveensundarg.shadow.prover.representations.value.Compound;
import com.naveensundarg.shadow.prover.representations.value.Value; import com.naveensundarg.shadow.prover.representations.value.Value;
import com.naveensundarg.shadow.prover.representations.value.Variable; import com.naveensundarg.shadow.prover.representations.value.Variable;
import com.naveensundarg.shadow.prover.utils.CollectionUtils; 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.List;
import java.util.Map; import java.util.Map;
@ -159,6 +159,11 @@ public class Action {
return trivial; return trivial;
} }
public Compound getShorthand() {
return shorthand;
}
@Override @Override
public String toString() { public String toString() {
return shorthand.getArguments().length == 0? name: shorthand.toString(); return shorthand.getArguments().length == 0? name: shorthand.toString();

67
src/main/java/edu/rpi/rair/DepthFirstPlanner.java
View file

@ -3,6 +3,8 @@ package edu.rpi.rair;
import com.naveensundarg.shadow.prover.representations.formula.Formula; import com.naveensundarg.shadow.prover.representations.formula.Formula;
import com.naveensundarg.shadow.prover.utils.Pair; import com.naveensundarg.shadow.prover.utils.Pair;
import com.naveensundarg.shadow.prover.utils.Sets; 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.*;
import java.util.stream.Collectors; import java.util.stream.Collectors;
@ -13,8 +15,8 @@ import java.util.stream.Collectors;
public class DepthFirstPlanner implements Planner { public class DepthFirstPlanner implements Planner {
private static int MAX_DEPTH = 4; private static int MAX_DEPTH = 5;
private static boolean EXHAUSTIVE_TILL_MAX_DEPTH = false; private static boolean EXHAUSTIVE_TILL_MAX_DEPTH = true;
public static int getMaxDepth() { public static int getMaxDepth() {
return MAX_DEPTH; return MAX_DEPTH;
@ -59,6 +61,61 @@ public class DepthFirstPlanner implements Planner {
} }
@Override
public Optional<Set<Plan>> plan(PlanningProblem problem, Set<Formula> background, Set<Action> actions, State start, State goal) {
if (!EXHAUSTIVE_TILL_MAX_DEPTH) {
return planInternal(Sets.newSet(), 0, MAX_DEPTH, background, actions, start, goal);
} else {
Set<Plan> possiblePlans = Sets.newSet();
for (int i = 1; i <= MAX_DEPTH; i++) {
Optional<Set<Plan>> plansOpt = planInternal(Sets.newSet(), 0, i, background, actions, start, goal);
if (plansOpt.isPresent()) {
Set<Plan> 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<Set<Plan>> planInternal(Set<Pair<State, Action>> history, int currentDepth, int maxDepth, Set<Formula> background, Set<Action> actions, State start, State goal) { private Optional<Set<Plan>> planInternal(Set<Pair<State, Action>> history, int currentDepth, int maxDepth, Set<Formula> background, Set<Action> actions, State start, State goal) {
@ -83,9 +140,11 @@ public class DepthFirstPlanner implements Planner {
for (Pair<State, Action> stateActionPair : nextStateActionPairs.get()) { for (Pair<State, Action> stateActionPair : nextStateActionPairs.get()) {
Visualizer.push();
Optional<Set<Plan>> planOpt = planInternal(history, currentDepth + 1, maxDepth, background, actions, stateActionPair.first(), goal); Optional<Set<Plan>> planOpt = planInternal(history, currentDepth + 1, maxDepth, background, actions, stateActionPair.first(), goal);
Visualizer.pop();
if (planOpt.isPresent()) { if (planOpt.isPresent()) {
atleastOnePlanFound = true; atleastOnePlanFound = true;
@ -100,6 +159,8 @@ public class DepthFirstPlanner implements Planner {
allPlans.addAll(augmentedPlans); allPlans.addAll(augmentedPlans);
// return Optional.of(allPlans);
//TODO: store different plans and return the best plan. //TODO: store different plans and return the best plan.
} }
} }

25
src/main/java/edu/rpi/rair/Goal.java
View file

@ -10,6 +10,8 @@ public class Goal {
private final State goalState; private final State goalState;
private final double priority; private final double priority;
private final String name; private final String name;
private final String description;
private static final AtomicInteger nameCounter; private static final AtomicInteger nameCounter;
static { static {
@ -19,12 +21,22 @@ public class Goal {
this.goalState = goalState; this.goalState = goalState;
this.priority = priority; this.priority = priority;
this.name = "G" + nameCounter.incrementAndGet(); this.name = "G" + nameCounter.incrementAndGet();
this.description = goalState.toString();
} }
private Goal(State goalState, double priority, String name) { private Goal(State goalState, double priority, String name) {
this.goalState = goalState; this.goalState = goalState;
this.priority = priority; this.priority = priority;
this.name = name; 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){ 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; return name;
} }
public String getDescription() {
return description;
}
@Override @Override
public String toString() { public String toString() {
return "Goal{" + return "(" + name + ": " + description + ": " + priority+ ")";
"goalState=" + goalState +
", priority=" + priority +
", name='" + name + '\'' +
'}';
} }
@Override @Override

21
src/main/java/edu/rpi/rair/GoalTracker.java
View file

@ -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.CollectionUtils;
import com.naveensundarg.shadow.prover.utils.Pair; import com.naveensundarg.shadow.prover.utils.Pair;
import com.naveensundarg.shadow.prover.utils.Sets; import com.naveensundarg.shadow.prover.utils.Sets;
import edu.rpi.rair.utils.PlanningProblem;
import java.util.Comparator; import java.util.Comparator;
import java.util.List; import java.util.List;
@ -24,14 +25,16 @@ public class GoalTracker {
private final Set<Goal> currentGoals; private final Set<Goal> currentGoals;
private final Planner planner; private final Planner planner;
private final Set<Action> actions; private final Set<Action> actions;
private final PlanningProblem problem;
public GoalTracker(Set<Formula> background, State startState, Set<Action> actions) { public GoalTracker(PlanningProblem problem, Set<Formula> background, State startState, Set<Action> actions) {
this.background = background; this.background = background;
this.currentState = startState; this.currentState = startState;
this.currentGoals = CollectionUtils.newEmptySet(); this.currentGoals = CollectionUtils.newEmptySet();
this.planner = new DepthFirstPlanner(); this.planner = new DepthFirstPlanner();
this.actions = actions; this.actions = actions;
this.problem = problem;
Operations.reset(); Operations.reset();
} }
@ -68,7 +71,7 @@ public class GoalTracker {
Optional<Set<Plan>> possiblePlans = planner.plan(background, actions, currentState, goal.getGoalState()); Optional<Set<Plan>> possiblePlans = planner.plan(problem, background, actions, currentState, goal.getGoalState());
if (!possiblePlans.isPresent()) { if (!possiblePlans.isPresent()) {
@ -151,6 +154,18 @@ public class GoalTracker {
} }
public Set<Formula> getBackground() {
return background;
}
public State getCurrentState() {
return currentState;
}
public PlanningProblem getProblem() {
return problem;
}
public Set<Goal> getCurrentGoals() { public Set<Goal> getCurrentGoals() {
return currentGoals; return currentGoals;
} }

13
src/main/java/edu/rpi/rair/Inducer.java Normal file
View file

@ -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);
}

36
src/main/java/edu/rpi/rair/Operations.java
View file

@ -3,7 +3,6 @@ package edu.rpi.rair;
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.core.SnarkWrapper;
import com.naveensundarg.shadow.prover.core.proof.Justification; 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.BiConditional;
import com.naveensundarg.shadow.prover.representations.formula.Formula; import com.naveensundarg.shadow.prover.representations.formula.Formula;
import com.naveensundarg.shadow.prover.representations.formula.Predicate; 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.CollectionUtils;
import com.naveensundarg.shadow.prover.utils.ImmutablePair; import com.naveensundarg.shadow.prover.utils.ImmutablePair;
import com.naveensundarg.shadow.prover.utils.Pair; import com.naveensundarg.shadow.prover.utils.Pair;
import com.naveensundarg.shadow.prover.utils.Sets; import com.naveensundarg.shadow.prover.utils.Sets;
import edu.rpi.rair.utils.Visualizer;
import org.apache.commons.lang3.tuple.Triple; import org.apache.commons.lang3.tuple.Triple;
import java.util.List; import java.util.List;
@ -30,7 +31,7 @@ import static edu.rpi.rair.State.FALSE;
public class Operations { public class Operations {
private static boolean DEEP_EQUIVALENCE = false; 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; private static Prover prover;
@ -46,7 +47,8 @@ public class Operations {
applyCache.clear(); applyCache.clear();
} }
static { static {
prover = new SnarkWrapper(); prover = SnarkWrapper.getInstance();
} }
@ -110,7 +112,7 @@ public class Operations {
if(room1.equals(room2)){ 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<Set<Map<Variable, Value>>> proveAndGetMultipleBindings(Set<Formula> givens, Formula goal, List<Variable> variables) { public static synchronized Optional<Set<Map<Variable, Value>>> proveAndGetMultipleBindings(Set<Formula> givens, Formula goal, List<Variable> variables) {
return prover.proveAndGetMultipleBindings(givens, goal, variables); Optional<org.apache.commons.lang3.tuple.Pair<Justification, Set<Map<Variable, Value>>>> ans = prover.proveAndGetMultipleBindings(givens, goal, variables);
if(ans.isPresent()){
return Optional.of(ans.get().getRight());
}else {
return Optional.empty();
}
/* Future<Optional<Set<Map<Variable, Value>>>> future = new FutureTask<>(()-> prover.proveAndGetMultipleBindings(givens, goal, variables)); /* Future<Optional<Set<Map<Variable, Value>>>> future = new FutureTask<>(()-> prover.proveAndGetMultipleBindings(givens, goal, variables));
Optional<Set<Map<Variable, Value>>> answer; Optional<Set<Map<Variable, Value>>> answer;
@ -192,9 +201,14 @@ public class Operations {
public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background, Action action, State state) { public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background, Action action, State state) {
if(applyCache.containsKey(Triple.of(background, action, state))){ if(applyCache.containsKey(Triple.of(background, action, state))){
return applyCache.get(Triple.of(background, action, state)); Optional<Set<Pair<State, Action>>> ans = applyCache.get(Triple.of(background, action, state));
if(ans.isPresent()){
return applyCache.get(Triple.of(background, action, state));
}
} }
Set<Formula> givens = Sets.union(background, state.getFormulae()); Set<Formula> givens = Sets.union(background, state.getFormulae());
@ -206,11 +220,14 @@ public class Operations {
if (!bindingsOpt.isPresent()) { if (!bindingsOpt.isPresent()) {
applyCache.put(Triple.of(background, action ,state), Optional.empty()); applyCache.put(Triple.of(background, action ,state), Optional.empty());
return Optional.empty(); return Optional.empty();
} }
Visualizer.nested(action.getName());
Set<Pair<State, Action>> nexts = Sets.newSet(); Set<Pair<State, Action>> nexts = Sets.newSet();
for (Map<Variable, Value> binding : bindingsOpt.get()) { for (Map<Variable, Value> binding : bindingsOpt.get()) {
@ -222,7 +239,7 @@ public class Operations {
Set<Formula> instantiatedDeletions = action.instantiateDeletions(binding); Set<Formula> instantiatedDeletions = action.instantiateDeletions(binding);
Set<Formula> formulaeToRemove = state.getFormulae().stream(). Set<Formula> 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<Formula> newFormulae = Sets.union(background, state.getFormulae()); Set<Formula> newFormulae = Sets.union(background, state.getFormulae());
@ -239,6 +256,7 @@ public class Operations {
} }
if (nexts.isEmpty()) { if (nexts.isEmpty()) {
Map<Variable, Value> emptyBinding = CollectionUtils.newMap(); Map<Variable, Value> 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)); applyCache.put(Triple.of(background, action ,state), Optional.of(nexts));
return Optional.of(nexts); return Optional.of(nexts);

26
src/main/java/edu/rpi/rair/Plan.java
View file

@ -2,6 +2,7 @@ package edu.rpi.rair;
import com.naveensundarg.shadow.prover.representations.formula.Formula; import com.naveensundarg.shadow.prover.representations.formula.Formula;
import com.naveensundarg.shadow.prover.utils.CollectionUtils; import com.naveensundarg.shadow.prover.utils.CollectionUtils;
import edu.rpi.rair.utils.Visualizer;
import java.util.List; import java.util.List;
import java.util.Set; import java.util.Set;
@ -63,15 +64,32 @@ public class Plan {
public boolean noConflicts(Set<Goal> goals){ public boolean noConflicts(Set<Goal> goals){
return getConflictingGoals(goals).isEmpty(); Set<Goal> 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<Action> actions = plan.getActions();
List<State> states = plan.getExpectedStates();
return null;
} }
@Override @Override
public String toString() { public String toString() {
return "Plan{" + return actions.stream().map(x-> x.toString() + " ").reduce((x,y) -> x + y).get();
"actions=" + actions +
'}';
} }
@Override @Override

123
src/main/java/edu/rpi/rair/PlanMethod.java Normal file
View file

@ -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<Formula> backGroundStatePreconditions;
private final Set<Formula> goalPreconditions;
private final List<Variable> freeVariables;
private final List<Compound> actionCompounds;
public PlanMethod(Set<Formula> goalPreconditions, Set<Formula> backGroundStatePreconditions, List<Variable> freeVariables, List<Compound> actionCompounds) {
this.goalPreconditions = goalPreconditions;
this.backGroundStatePreconditions = backGroundStatePreconditions;
this.freeVariables = freeVariables;
this.actionCompounds = actionCompounds;
}
public PlanMethod(Set<Formula> goalPreconditions, List<Variable> freeVariables, List<Compound> actionCompounds) {
this.goalPreconditions = goalPreconditions;
this.backGroundStatePreconditions = Sets.newSet();
this.freeVariables = freeVariables;
this.actionCompounds = actionCompounds;
}
public Optional<List<PlanSketch>> apply(Set<Formula> background, Set<Formula> start, Set<Formula> goal, Set<Action> actionSpecs) {
Optional<Set<Map<Variable, Value>>> mappingsOpt = Operations.proveAndGetMultipleBindings(goal, new And(new ArrayList<>(goalPreconditions)), freeVariables);
if (mappingsOpt.isPresent()) {
Set<Map<Variable, Value>> mappings = mappingsOpt.get();
List<PlanSketch> 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<Compound> instantiatedActionCompounds = actionCompounds.stream().map(compound -> (Compound) compound.apply(mapping)).collect(Collectors.toList());
List<Action> 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 +
'}';
}
}

14
src/main/java/edu/rpi/rair/PlanSketch.java Normal file
View file

@ -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<Action> actions, Set<Formula> background) {
super(actions, CollectionUtils.newEmptyList(), background);
}
}

2
src/main/java/edu/rpi/rair/Planner.java
View file

@ -1,6 +1,7 @@
package edu.rpi.rair; package edu.rpi.rair;
import com.naveensundarg.shadow.prover.representations.formula.Formula; import com.naveensundarg.shadow.prover.representations.formula.Formula;
import edu.rpi.rair.utils.PlanningProblem;
import java.util.List; import java.util.List;
import java.util.Optional; import java.util.Optional;
@ -12,5 +13,6 @@ import java.util.Set;
public interface Planner { public interface Planner {
Optional<Set<Plan>> plan(Set<Formula> background, Set<Action> actions, State start, State goal); Optional<Set<Plan>> plan(Set<Formula> background, Set<Action> actions, State start, State goal);
Optional<Set<Plan>> plan(PlanningProblem problem, Set<Formula> background, Set<Action> actions, State start, State goal);
} }

2
src/main/java/edu/rpi/rair/State.java
View file

@ -17,7 +17,7 @@ import java.util.stream.Collectors;
public class State { public class State {
final Set<Formula> formulae; final Set<Formula> formulae;
private static final Prover prover = new SnarkWrapper(); private static final Prover prover = SnarkWrapper.getInstance();
static Formula FALSE; static Formula FALSE;
static{ static{

63
src/main/java/edu/rpi/rair/inducers/SimpleInducer.java Normal file
View file

@ -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<Action> actionList = plan.getActions();
List<Compound> actionCompounds = actionList.stream().map(Action::getShorthand).collect(Collectors.toList());
Set<Formula> backgroundFormula = planningProblem.getBackground().stream().collect(Collectors.toSet());
Set<Formula> initFormula = start.getFormulae().stream().collect(Collectors.toSet());
Set<Formula> goalFormula = goal.getGoalState().getFormulae().stream().collect(Collectors.toSet());
Set<Value> 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<Value, Variable> valueVariableMap = Commons.makeVariables(values);
Function<Set<Formula>,Set<Formula>> getRelevantFormula = formulae -> formulae.stream().
filter(formula -> !Sets.intersection(values, formula.valuesPresent()).isEmpty()).
collect(Collectors.toSet());
Set<Formula> relevantBackgroundFormula = getRelevantFormula.apply(backgroundFormula);
Set<Formula> relevantInitFormula = getRelevantFormula.apply(initFormula);
Set<Formula> 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;
}
}

96
src/main/java/edu/rpi/rair/utils/Commons.java
View file

@ -1,12 +1,108 @@
package edu.rpi.rair.utils; 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 edu.rpi.rair.State;
import us.bpsm.edn.parser.Parseable; 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. * Created by naveensundarg on 1/15/17.
*/ */
public class Commons { public class Commons {
public static Map<Value, Variable> makeVariables(Set<Value> values){
return makeVariables(values, 1);
}
public static Map<Value, Variable> makeVariables(Set<Value> values, int startValue){
int n = startValue;
Map<Value, Variable> 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<Value, Variable> universalValueVariableMap, Set<Formula> formulae){
Set<Value> allValues = formulae.stream().map(Formula::valuesPresent).reduce(Sets.newSet(), Sets::union).stream().filter(x->x.isConstant()).collect(Collectors.toSet());
Map<Value, Variable> existentialValueVariableMap = makeVariables(Sets.difference(allValues, universalValueVariableMap.keySet()), universalValueVariableMap.size() + 1);
Map<Value, Variable> 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 <U, V> Map<V, U> reverse(Map<U, V> map){
Map<V, U> reverseMap = CollectionUtils.newMap();
map.forEach((u, v) -> reverseMap.put(v, u));
return reverseMap;
}
public static <U, V> Map<U, V> combine(Map<U, V> map1, Map<U, V> map2){
Map<U, V> combinedMap = CollectionUtils.newMap();
map1.forEach(combinedMap::put);
map2.forEach(combinedMap::put);
return combinedMap;
}
public static<U, V, W> Object runAndTime(BiFunction<U, V, W> 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;
}
} }

18
src/main/java/edu/rpi/rair/utils/FrozenPrinter.java Normal file
View file

@ -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);
}
}

4
src/main/java/edu/rpi/rair/utils/GoalTrackingProblem.java
View file

@ -27,6 +27,7 @@ public class GoalTrackingProblem {
private static final Keyword DEFINITIONS = Keyword.newKeyword("definitions"); private static final Keyword DEFINITIONS = Keyword.newKeyword("definitions");
private static final Keyword GOALS = Keyword.newKeyword("goals"); 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 PRIORITY = Keyword.newKeyword("priority");
private static final Keyword STATE = Keyword.newKeyword("state"); private static final Keyword STATE = Keyword.newKeyword("state");
@ -69,7 +70,8 @@ public class GoalTrackingProblem {
double priority = ((Double) goalSpec.get(PRIORITY)); double priority = ((Double) goalSpec.get(PRIORITY));
Set<Formula> stateFormulae = PlanningProblem.readFrom((List<?>) goalSpec.get(STATE)); Set<Formula> 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));
} }

77
src/main/java/edu/rpi/rair/utils/LearningSystem.java Normal file
View file

@ -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<Triple<BiConsumer<String, String>, String, String>> printQueue = new ArrayList<>();
public static void main(String[] args) throws Reader.ParsingException, InterruptedException {
System.out.println();
RunDemo.planningProblemWarmUp();
Visualizer.setShouldVisualize(false);
List<GoalTrackingProblem> goalTrackingProblemList1 = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("seriated_challenge_1.clj")));
List<GoalTrackingProblem> 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<Formula> background, State startState, Set<Action> 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<GoalTracker, GoalTrackingProblem, Plan> 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"));
}
}

71
src/main/java/edu/rpi/rair/utils/PlanningProblem.java
View file

@ -2,10 +2,12 @@ package edu.rpi.rair.utils;
import clojure.lang.Obj; import clojure.lang.Obj;
import com.naveensundarg.shadow.prover.representations.formula.Formula; 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.Value;
import com.naveensundarg.shadow.prover.representations.value.Variable; import com.naveensundarg.shadow.prover.representations.value.Variable;
import com.naveensundarg.shadow.prover.utils.CollectionUtils; import com.naveensundarg.shadow.prover.utils.CollectionUtils;
import com.naveensundarg.shadow.prover.utils.Reader; import com.naveensundarg.shadow.prover.utils.Reader;
import com.naveensundarg.shadow.prover.utils.Sets;
import edu.rpi.rair.Action; import edu.rpi.rair.Action;
import edu.rpi.rair.State; import edu.rpi.rair.State;
import us.bpsm.edn.Keyword; import us.bpsm.edn.Keyword;
@ -17,6 +19,7 @@ import us.bpsm.edn.parser.Token;
import java.io.InputStream; import java.io.InputStream;
import java.io.InputStreamReader; import java.io.InputStreamReader;
import java.io.StringReader;
import java.security.Key; import java.security.Key;
import java.util.*; import java.util.*;
import java.util.stream.Collectors; import java.util.stream.Collectors;
@ -34,11 +37,14 @@ public class PlanningProblem {
private Optional<Set<List<Action>>> expectedActionSequencesOpt; private Optional<Set<List<Action>>> expectedActionSequencesOpt;
private Map<String, Action> actionMap; private Map<String, Action> actionMap;
private Set<Value> avoidIfPossible;
private static final Keyword BACKGROUND = Keyword.newKeyword("background"); private static final Keyword BACKGROUND = Keyword.newKeyword("background");
private static final Keyword START = Keyword.newKeyword("start"); private static final Keyword START = Keyword.newKeyword("start");
private static final Keyword GOAL = Keyword.newKeyword("goal"); private static final Keyword GOAL = Keyword.newKeyword("goal");
private static final Keyword NAME = Keyword.newKeyword("name"); private static final Keyword NAME = Keyword.newKeyword("name");
private static final Keyword ACTION = Keyword.newKeyword("actions"); 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 PRECONDITIONS = Keyword.newKeyword("preconditions");
private static final Keyword ADDITIONS = Keyword.newKeyword("additions"); 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"); private static final Keyword EXPECTED_PLANS = Keyword.newKeyword("expected-plans");
public PlanningProblem(String name, Set<Formula> background, State start, State goal, Set<Action> actions) { private PlanningProblem(String name, Set<Formula> background, State start, State goal, Set<Action> actions, Set<Value> avoidIfPossible) {
this.background = background; this.background = background;
this.start = start; this.start = start;
@ -56,10 +62,13 @@ public class PlanningProblem {
this.goal = goal; this.goal = goal;
this.name = name; this.name = name;
this.actionMap = CollectionUtils.newMap(); this.actionMap = CollectionUtils.newMap();
this.avoidIfPossible = avoidIfPossible;
this.expectedActionSequencesOpt = Optional.empty(); this.expectedActionSequencesOpt = Optional.empty();
} }
public PlanningProblem(String name, Set<Formula> background, State start, State goal, Set<Action> actions, Set<List<Action>> expectedActionSequences) { private PlanningProblem(String name, Set<Formula> background, State start, State goal, Set<Action> actions, Set<Value> avoidIfPossible, Set<List<Action>>expectedActionSequences) {
this.background = background; this.background = background;
this.start = start; this.start = start;
@ -67,6 +76,8 @@ public class PlanningProblem {
this.goal = goal; this.goal = goal;
this.name = name; this.name = name;
this.actionMap = CollectionUtils.newMap(); this.actionMap = CollectionUtils.newMap();
this.avoidIfPossible = avoidIfPossible;
this.expectedActionSequencesOpt = Optional.of(expectedActionSequences); this.expectedActionSequencesOpt = Optional.of(expectedActionSequences);
} }
@ -100,6 +111,7 @@ public class PlanningProblem {
Set<Formula> goal = readFrom((List<?>) planningProblemSpec.get(GOAL)); Set<Formula> goal = readFrom((List<?>) planningProblemSpec.get(GOAL));
Set<Value> avoidIfPossible = readValuesFrom((List<?>) planningProblemSpec.get(AVOID_IF_POSSIBLE));
List<?> actionDefinitions = (List<?>) planningProblemSpec.get(ACTION); List<?> actionDefinitions = (List<?>) planningProblemSpec.get(ACTION);
@ -110,6 +122,7 @@ public class PlanningProblem {
actions.stream().forEach(action->{ actions.stream().forEach(action->{
actionMap.put(action.getName(), action); actionMap.put(action.getName(), action);
}); });
if(planningProblemSpec.containsKey(EXPECTED_PLANS)){ if(planningProblemSpec.containsKey(EXPECTED_PLANS)){
List<?> plans = (List<?>) planningProblemSpec.get(EXPECTED_PLANS); List<?> plans = (List<?>) planningProblemSpec.get(EXPECTED_PLANS);
@ -135,15 +148,32 @@ public class PlanningProblem {
return new PlanningProblem(name, background, State.initializeWith(start), return new PlanningProblem(name, background, State.initializeWith(start),
State.initializeWith(goal), actions, expectedActions); State.initializeWith(goal), actions, avoidIfPossible, expectedActions);
} else { } else {
return new PlanningProblem(name, background, State.initializeWith(start), return new PlanningProblem(name, background, State.initializeWith(start),
State.initializeWith(goal), actions); State.initializeWith(goal),actions, avoidIfPossible);
} }
} }
public static Action readInstantiatedAction(Set<Action> 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<String, Action> actionMap = CollectionUtils.newMap();
actions.stream().forEach(action->{
actionMap.put(action.getName(), action);
});
return readInstantiatedAction(actionMap, instantiatedActionSpec);
}
private static Action readInstantiatedAction(Map<String, Action> actionMap, Object instantiatedActionSpec) throws Reader.ParsingException { private static Action readInstantiatedAction(Map<String, Action> actionMap, Object instantiatedActionSpec) throws Reader.ParsingException {
if(instantiatedActionSpec instanceof List<?>){ if(instantiatedActionSpec instanceof List<?>){
@ -229,6 +259,10 @@ public class PlanningProblem {
public static Set<Formula> readFrom(List<?> objects) throws Reader.ParsingException { public static Set<Formula> readFrom(List<?> objects) throws Reader.ParsingException {
if(objects==null){
return Sets.newSet();
}
Set<Formula> formulae = objects.stream().map(x -> { Set<Formula> formulae = objects.stream().map(x -> {
try { try {
return Reader.readFormula(x); return Reader.readFormula(x);
@ -249,6 +283,31 @@ public class PlanningProblem {
} }
public static Set<Value> readValuesFrom(List<?> objects) throws Reader.ParsingException {
if(objects==null){
return Sets.newSet();
}
Set<Value> 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<Formula> getBackground() { public Set<Formula> getBackground() {
return background; return background;
} }
@ -277,6 +336,10 @@ public class PlanningProblem {
return actionMap; return actionMap;
} }
public Set<Value> getAvoidIfPossible() {
return avoidIfPossible;
}
@Override @Override
public String toString() { public String toString() {
return "PlanningProblem{" + return "PlanningProblem{" +

112
src/main/java/edu/rpi/rair/utils/Reader.java Normal file
View file

@ -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<PlanMethod> 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<PlanMethod> 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<Symbol> variableObjs = (List<Symbol>) planMethodSpec.get(2);
List<Variable> 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<Formula> goalPreconds = CollectionUtils.newEmptySet();
Set<Formula> whilePreconds = CollectionUtils.newEmptySet();
List<Compound> 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);
}
}

202
src/main/java/edu/rpi/rair/utils/RunDemo.java
View file

@ -1,22 +1,26 @@
package edu.rpi.rair.utils; package edu.rpi.rair.utils;
import com.diogonunes.jcdp.color.ColoredPrinter; import com.diogonunes.jcdp.color.ColoredPrinter;
import com.diogonunes.jcdp.color.api.Ansi; import com.diogonunes.jcdp.color.api.Ansi;
import com.google.common.collect.Sets; import com.google.common.collect.Sets;
import com.naveensundarg.shadow.prover.Sandbox; import com.naveensundarg.shadow.prover.core.Prover;
import com.naveensundarg.shadow.prover.core.Problem;
import com.naveensundarg.shadow.prover.core.Prover;
import com.naveensundarg.shadow.prover.core.SnarkWrapper; 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.ProblemReader;
import com.naveensundarg.shadow.prover.utils.Reader; import com.naveensundarg.shadow.prover.utils.Reader;
import edu.rpi.rair.Goal; import edu.rpi.rair.*;
import edu.rpi.rair.GoalTracker; import edu.rpi.rair.inducers.SimpleInducer;
import edu.rpi.rair.Plan;
import edu.rpi.rair.Planner;
import edu.rpi.rair.utils.GoalTrackingProblem; 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.List;
import java.util.Optional; import java.util.function.BiConsumer;
import java.util.Set; import java.util.function.BiFunction;
import java.util.stream.Collectors; import java.util.stream.Collectors;
/** /**
@ -27,84 +31,100 @@ public class RunDemo {
static ColoredPrinter cp = new ColoredPrinter.Builder(1, false).build(); static ColoredPrinter cp = new ColoredPrinter.Builder(1, false).build();
static List<Triple<BiConsumer<String, String>, String, String>> printQueue = new ArrayList<>();
static { static {
Prover prover = new SnarkWrapper(); Prover prover = SnarkWrapper.getInstance();
try { /* try {
List<Problem> problems = ProblemReader.readFrom(Sandbox.class.getResourceAsStream("firstorder-completness-tests.clj")); List<Problem> problems = ProblemReader.readFrom(Sandbox.class.getResourceAsStream("../firstorder-completness-tests.clj"));
problems.forEach(problem -> { problems.forEach(problem -> {
for (int i = 0; i < 30; i++) { for (int i = 0; i < 100; i++) {
prover.prove(problem.getAssumptions(), problem.getGoal()); prover.prove(problem.getAssumptions(), problem.getGoal());
} }
}); });
planningProblemWarmUp(); planningProblemWarmUp();
System.out.println("\nWARM UP DONE"); System.out.println("\nWARM UP DONE");
} catch (Reader.ParsingException e) { } catch (Reader.ParsingException e) {
e.printStackTrace(); 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<GoalTrackingProblem> 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<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("seriated_challenge_1.clj"))); long start = System.currentTimeMillis();
Goal g1 = goalTrackingProblem.getGoalNamed("G1");
GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0); tryAndAddGoal(g1, goalTracker);
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");
Goal g3 = goalTrackingProblem.getGoalNamed("G3"); long end = System.currentTimeMillis();
Goal g4 = goalTrackingProblem.getGoalNamed("G4");
Goal g5 = goalTrackingProblem.getGoalNamed("G5");
*/
tryAndAddGoal(g1, goalTracker);
/* tryAndAddGoal(g2, goalTracker);
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("--------------------------"); Triple<BiConsumer<String, String>, String, String> task = printQueue.get(i);
cp.setForegroundColor(Ansi.FColor.CYAN);
cp.print("Time Taken:"); task.getLeft().accept(task.getMiddle(), task.getRight());
cp.clear();
cp.print(" ");
cp.setAttribute(Ansi.Attribute.BOLD);
cp.print((end - start) / 1000.0 + "s");
}
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 { public static void planningProblemWarmUp() throws Reader.ParsingException {
@ -118,7 +138,7 @@ public class RunDemo {
GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0); 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().getStart(),
goalTrackingProblem.getPlanningProblem().getActions()); goalTrackingProblem.getPlanningProblem().getActions());
@ -154,34 +174,47 @@ public class RunDemo {
static void tryAndAddGoal(Goal g, GoalTracker goalTracker) { static void tryAndAddGoal(Goal g, GoalTracker goalTracker) {
System.out.println("========================"); Inducer simpleInducer = new SimpleInducer();
printInfo("Trying to Add Goal:", g.getName());
Set<String> oldGoals = goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()); System.out.println("========================");
printInfoLater("Trying to Add Goal or Constraint:", "");
printInfoLater(" ", g.toString());
Set<Goal> oldGoals = goalTracker.getCurrentGoals().stream().collect(Collectors.toSet());
Optional<Plan> possibleGoalPlan = goalTracker.adoptGoal(g); Optional<Plan> possibleGoalPlan = goalTracker.adoptGoal(g);
if (possibleGoalPlan.isPresent()) { if (possibleGoalPlan.isPresent()) {
printSuccess("Successfully added:", g.getName()); simpleInducer.induce(goalTracker.getProblem(), goalTracker.getProblem().getStart(), g, possibleGoalPlan.get());
printDebug1("Current Goals:", goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()).toString());
Set<String> 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()){ Set<Goal> newGoals = goalTracker.getCurrentGoals().stream().collect(Collectors.toSet());
printDropped("Dropped Goals:" + Sets.difference(oldGoals, newGoals));
if (!Sets.difference(oldGoals, newGoals).isEmpty()) {
printDroppedLater("", "Dropped Goals and Contraints:" + Sets.difference(oldGoals, newGoals));
} }
Plan plan = possibleGoalPlan.get(); 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 { } else {
printFailure("Could not add " + g.getName()); printFailureLater("", "Could not add " + g);
printDebug1("Current Goals: ", goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()).toString());
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) { static void printInfo(String header, String message) {
cp.setForegroundColor(Ansi.FColor.WHITE); cp.setForegroundColor(Ansi.FColor.WHITE);
@ -195,6 +228,14 @@ public class RunDemo {
cp.clear(); 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) { static void printSuccess(String header, String message) {
cp.setForegroundColor(Ansi.FColor.BLACK); 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) { static void printDebug1(String header, String message) {
cp.setForegroundColor(Ansi.FColor.BLACK); cp.setForegroundColor(Ansi.FColor.BLACK);
@ -222,6 +271,13 @@ public class RunDemo {
cp.clear(); 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) { static void printDebug2(String header, String message) {
cp.setForegroundColor(Ansi.FColor.BLACK); cp.setForegroundColor(Ansi.FColor.BLACK);
@ -235,7 +291,14 @@ public class RunDemo {
cp.clear(); 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.setForegroundColor(Ansi.FColor.WHITE);
cp.setBackgroundColor(Ansi.BColor.RED); //setting format cp.setBackgroundColor(Ansi.BColor.RED); //setting format
@ -245,7 +308,16 @@ public class RunDemo {
cp.clear(); 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.setForegroundColor(Ansi.FColor.WHITE);
cp.setBackgroundColor(Ansi.BColor.RED); //setting format cp.setBackgroundColor(Ansi.BColor.RED); //setting format

31
src/main/java/edu/rpi/rair/utils/Sandbox.java Normal file
View file

@ -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<GoalTrackingProblem> 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()
));
}
}

177
src/main/java/edu/rpi/rair/utils/Visualizer.java Normal file
View file

@ -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<String> 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<depth+1; i++){
stringBuffer.append(" ▶ ");
}
stringBuffer.append(name);
}
spool.add(stringBuffer.toString());
}
public static void unspool(long delay){
spool.forEach(x->{
// 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();
}
}

268
src/main/resources/edu/rpi/rair/completeness_problems.clj
View file

@ -2,15 +2,12 @@
:background [p] :background [p]
:start [q] :start [q]
:goal [r] :goal [r]
:actions :actions [(define-action a1 ()
[(define-action a1 () {:preconditions [(or q r)]
{:preconditions [(or q r)] :additions [r]
:additions [r] :deletions [q]})]
:deletions [q]})]
:expected-plans ([a1])
}
:expected-plans ([a1])}
{:name "simple killing" {:name "simple killing"
@ -18,14 +15,12 @@
:start [(forall ?x (alive ?x))] :start [(forall ?x (alive ?x))]
:goal [(forall ?x (dead ?x))] :goal [(forall ?x (dead ?x))]
:actions :actions
[(define-action kill () [(define-action kill ()
{:preconditions [(alive ?x)] {:preconditions [(alive ?x)]
:additions [(dead ?x)] :additions [(dead ?x)]
:deletions [(alive ?x)]})] :deletions [(alive ?x)]})]
:expected-plans ([kill]) :expected-plans ([kill])}
}
{:name "thirsty" {:name "thirsty"
@ -33,18 +28,16 @@
:start [thirsty] :start [thirsty]
:goal [(not thirsty)] :goal [(not thirsty)]
:actions :actions
[(define-action drink () [(define-action drink ()
{:preconditions [thirsty] {:preconditions [thirsty]
:additions [(not thirsty)] :additions [(not thirsty)]
:deletions [thirsty]}) :deletions [thirsty]})
(define-action eat () (define-action eat ()
{:preconditions [hungry] {:preconditions [hungry]
:additions [(not hungry)] :additions [(not hungry)]
:deletions [hungry]})] :deletions [hungry]})]
:expected-plans ([drink]) :expected-plans ([drink])}
}
{:name "hungry" {:name "hungry"
@ -53,18 +46,17 @@
:goal [(not hungry)] :goal [(not hungry)]
:actions :actions
[(define-action drink () [(define-action drink ()
{:preconditions [thirsty] {:preconditions [thirsty]
:additions [(not thirsty)] :additions [(not thirsty)]
:deletions [thirsty]}) :deletions [thirsty]})
(define-action eat () (define-action eat ()
{:preconditions [hungry] {:preconditions [hungry]
:additions [(not hungry)] :additions [(not hungry)]
:deletions [hungry]})] :deletions [hungry]})]
:expected-plans ([eat]) :expected-plans ([eat])}
}
{:name "hungry and thirsty" {:name "hungry and thirsty"
@ -72,19 +64,18 @@
:start [hungry thirsty] :start [hungry thirsty]
:goal [(not (or hungry thirsty))] :goal [(not (or hungry thirsty))]
:actions :actions
[(define-action drink () [(define-action drink ()
{:preconditions [thirsty] {:preconditions [thirsty]
:additions [(not thirsty)] :additions [(not thirsty)]
:deletions [thirsty]}) :deletions [thirsty]})
(define-action eat () (define-action eat ()
{:preconditions [hungry] {:preconditions [hungry]
:additions [(not hungry)] :additions [(not hungry)]
:deletions [hungry]})] :deletions [hungry]})]
:expected-plans ([eat drink] :expected-plans ([eat drink]
[drink eat]) [drink eat])}
}
{:name "hungry and thirsty" {:name "hungry and thirsty"
:background [] :background []
@ -92,94 +83,141 @@
:goal [work-finished] :goal [work-finished]
:actions :actions
[(define-action drink () [(define-action drink ()
{:preconditions [thirsty] {:preconditions [thirsty]
:additions [(not thirsty)] :additions [(not thirsty)]
:deletions [thirsty]}) :deletions [thirsty]})
(define-action eat () (define-action eat ()
{:preconditions [hungry] {:preconditions [hungry]
:additions [(not hungry)] :additions [(not hungry)]
:deletions [hungry]}) :deletions [hungry]})
(define-action work () (define-action work ()
{:preconditions [(and (not hungry) (not thirsty))] {:preconditions [(and (not hungry) (not thirsty))]
:additions [work-finished] :additions [work-finished]
:deletions [work-unfinished]})] :deletions [work-unfinished]})]
:expected-plans ([eat drink work] :expected-plans ([eat drink work]
[drink eat work])} [drink eat work])}
{:name "Heinz Dilemma"
:background [(cures radium-drug-x cancerx)]
:start [(sick (wife heinz) cancerx)
{:name "demo 1" (= 5000 (cost radium-drug-x))
:background [ (not (can-spend 5000))
(not (= room1 room2)) (not (possess radium-drug-x))]
(not (= prisoner commander)) :goal [(healthy (wife heinz))]
(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)]
:actions :actions
[(define-action open-door [?room]
{:preconditions [(not (open (door ?room)))] [(define-action administer-medicine [?medicine ?condition ?person]
:additions [(open (door ?room))] {:preconditions [(sick ?person ?condition)
:deletions [(not (open (door ?room)))]}) (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) (define-action finance [?amount]
(in self ?room2)] {:preconditions [(not (can-spend ?amount))]
:additions [(can-spend ?amount)]
:deletions [(not (can-spend ?amount))]})]
:deletions [(in ?person ?room1) :expected-plans ([buy-medicine administer-medicine])}
(in self ?room1)]})
(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] (define-action believe-without-support [?p]
{:preconditions [(in commander ?room) {:preconditions [(Proposition ?p)]
(in prisoner ?room)] :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) :actions [(define-action and-intro [?p ?q]
(move commander room2 room1) {:preconditions [(! ?p) (! ?q)]
(get-interrogated room1)] :additions [(! (and ?p ?q))]
:deletions []})
[(open-door room1) (define-action cond-elim [?p ?q]
(move prisoner room1 room2) {:preconditions [(! (if ?p ?q)) (! ?p)]
(get-interrogated room2)] :additions [(! ?q)]
:deletions []})
[(open-door room1)
(accompany prisoner room1 room2)
(get-interrogated room2)])}
(define-action cond-intro [?p ?q]
{:preconditions [ (Prop ?p) (! ?q)]
:additions [(! (if ?p ?q))]
:deletions []})]
:expected-plans ([and-intro])}

36
src/main/resources/edu/rpi/rair/file.clj Normal file
View file

@ -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)]}}
}

60
src/main/resources/edu/rpi/rair/problems/heinz/heinz_challenge.clj Normal file
View file

@ -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))]}}}

0
src/main/resources/edu/rpi/rair/goal_management_1.clj → src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_1.clj
View file

0
src/main/resources/edu/rpi/rair/goal_management_2.clj → src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_2.clj
View file

0
src/main/resources/edu/rpi/rair/goal_management_3.clj → src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_3.clj
View file

0
src/main/resources/edu/rpi/rair/goal_management_4.clj → src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_4.clj
View file

0
src/main/resources/edu/rpi/rair/goal_management_5.clj → src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_5.clj
View file

0
src/main/resources/edu/rpi/rair/goal_management_6.clj → src/main/resources/edu/rpi/rair/problems/prisoner/goal_management_6.clj
View file

9
src/main/resources/edu/rpi/rair/problems/seriated/methods.clj Normal file
View file

@ -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)]})

21
src/main/resources/edu/rpi/rair/seriated_challenge_1.clj → src/main/resources/edu/rpi/rair/problems/seriated/seriated_challenge_1.clj
View file

@ -21,16 +21,18 @@
(< (size a) (size b)) (< (size a) (size b))
(< (size b) (size c)) (< (size b) (size c))
(< (size c) (size d)) (< (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) :start [(In a b)
(In b d) (In b d)
(In d e) (Empty c)]
(Empty c)]
:goal [] :goal [ ]
:actions [(define-action placeInside [?x ?y] :actions [(define-action placeInside [?x ?y]
{:preconditions [(< (size ?x) (size ?y)) {:preconditions [(< (size ?x) (size ?y))
@ -41,20 +43,15 @@
(define-action removeFrom [?x ?y] (define-action removeFrom [?x ?y]
{:preconditions [(In ?x ?y)] {:preconditions [(In ?x ?y)]
:additions [(Empty ?y)] :additions [(Empty ?y)]
:deletions [(In ?x ?y)]} )] :deletions [(In ?x ?y)]})]}
}
:goals {G1 {:priority 1.0 :goals {G1 {:priority 1.0
:state [(In a b) :state [(In a b)
(In b c) (In b c)
(In c d) (In c d)]}}
(In d e)]}}
;;(removeFrom b d) (placeInside b c) (placeInside c d)
} }

70
src/main/resources/edu/rpi/rair/problems/seriated/seriated_challenge_2.clj Normal file
View file

@ -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)
}

62
src/main/resources/edu/rpi/rair/self_deception.clj Normal file
View file

@ -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)]}}}

4
src/test/java/edu/rpi/rair/DepthFirstPlannerTest.java
View file

@ -33,7 +33,9 @@ public class DepthFirstPlannerTest {
Planner depthFirstPlanner = new DepthFirstPlanner(); 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); depthFirstPlanner.plan(planningProblem.getBackground(), planningProblem.getActions(), planningProblem.getStart(), planningProblem.getGoal()).get().forEach(System.out::println);
} }

4
src/test/java/edu/rpi/rair/GoalTrackerTest.java
View file

@ -17,12 +17,12 @@ public class GoalTrackerTest {
public static void main(String[] args) throws Reader.ParsingException { public static void main(String[] args) throws Reader.ParsingException {
List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_1.clj"))); List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_6.clj")));
GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0); 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().getStart(),
goalTrackingProblem.getPlanningProblem().getActions()); goalTrackingProblem.getPlanningProblem().getActions());

41
src/test/java/edu/rpi/rair/HeinzGoalTrackerTest.java Normal file
View file

@ -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<GoalTrackingProblem> 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"));
}
}