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

A lot of commits.

Browse source
This commit is contained in:
Naveen Sundar Govindarajulu 2018-01-02 14:32:09 -08:00
parent 9bdf4fe029
commit e6cfb3e654
17 changed files with 239 additions and 61 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

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

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

@ -105,6 +105,18 @@ public class Action {
return precondition;
}
public Set<Formula> getPreconditions() {
return preconditions;
}
public Set<Formula> getAdditions() {
return additions;
}
public Set<Formula> getDeletions() {
return deletions;
}
public List<Variable> openVars() {
return freeVariables;

26
src/main/java/edu/rpi/rair/ContextNormPlanner.java Normal file
View file

@ -0,0 +1,26 @@
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;
import java.util.Set;
public class ContextNormPlanner implements Planner {
private static DepthFirstPlanner depthFirstPlanner = new DepthFirstPlanner();
@Override
public Optional<Set<Plan>> plan(Set<Formula> background, Set<Action> actions, State start, State goal) {
return depthFirstPlanner.plan(background, actions, start, goal);
}
@Override
public Optional<Set<Plan>> plan(PlanningProblem problem, Set<Formula> background, Set<Action> actions, State start, State goal) {
List<Plan> methods = problem.getPlanMethods();
}
}

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

@ -1,12 +1,16 @@
package edu.rpi.rair;
import com.naveensundarg.shadow.prover.core.proof.Justification;
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.Commons;
import edu.rpi.rair.utils.PlanningProblem;
import edu.rpi.rair.utils.Visualizer;
import java.util.*;
import java.util.function.Function;
import java.util.stream.Collectors;
/**
@ -18,6 +22,8 @@ public class DepthFirstPlanner implements Planner {
private static int MAX_DEPTH = 5;
private static boolean EXHAUSTIVE_TILL_MAX_DEPTH = true;
private static boolean USE_METHODS = true;
public static int getMaxDepth() {
return MAX_DEPTH;
}
@ -64,6 +70,15 @@ public class DepthFirstPlanner implements Planner {
@Override
public Optional<Set<Plan>> plan(PlanningProblem problem, Set<Formula> background, Set<Action> actions, State start, State goal) {
if(USE_METHODS){
Optional<Set<Plan>> optionalPlansFromMethods = plan(problem, background, actions, start, goal, problem.getPlanMethods());
if(optionalPlansFromMethods.isPresent()){
return optionalPlansFromMethods;
}
}
if (!EXHAUSTIVE_TILL_MAX_DEPTH) {
@ -117,6 +132,79 @@ public class DepthFirstPlanner implements Planner {
}
public Optional<Set<Plan>> plan(PlanningProblem problem, Set<Formula> background, Set<Action> actions, State start, State goal, List<PlanMethod> planMethods){
Set<Plan> plans = Sets.newSet();
Function<PlanSketch, Optional<Plan>> verifier = (planSketch) -> verify(background, start, goal, planSketch);
for (PlanMethod planMethod: planMethods){
Optional<List<PlanSketch>> optionalPlanSketches = planMethod.apply(background, start.getFormulae(), goal.getFormulae(), problem.getActions());
optionalPlanSketches.ifPresent(planSketches -> planSketches.forEach(planSketch -> verifier.apply(planSketch).ifPresent(plans::add)));
}
if(!plans.isEmpty()){
return Optional.of(plans);
} else {
return Optional.empty();
}
}
public Optional<Plan> verify(Set<Formula> background, State start, State goal, PlanSketch planSketch){
List<Action> sketchActions = planSketch.getActions();
List<State> expectedStates = CollectionUtils.newEmptyList();
Set<Formula> current = Sets.union(background, start.getFormulae());
expectedStates.add(State.initializeWith(current));
for(Action action: sketchActions){
Set<Formula> preconditions = action.getPreconditions();
Set<Formula> additions = action.getAdditions();
Set<Formula> deletions = action.getDeletions();
Optional<Justification> optPrecond = Operations.proveCached(current, Commons.makeAnd(preconditions));
if(optPrecond.isPresent()){
current.addAll(additions);
current.removeAll(deletions);
expectedStates.add(State.initializeWith(current));
} else {
return Optional.empty();
}
}
if(!Operations.proveCached(current, Commons.makeAnd(goal.getFormulae())).isPresent()){
return Optional.empty();
}
return Optional.of(new Plan(sketchActions, expectedStates, background));
}
private Optional<Set<Plan>> planInternal(Set<Pair<State, Action>> history, int currentDepth, int maxDepth, Set<Formula> background, Set<Action> actions, State start, State goal) {
if (currentDepth >= maxDepth) {

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

@ -8,6 +8,6 @@ import edu.rpi.rair.utils.PlanningProblem;
*/
public interface Inducer {
Plan induce(PlanningProblem planningProblem, State start, Goal goal, Plan plan);
PlanMethod induce(PlanningProblem planningProblem, State start, Goal goal, Plan plan);
}

17
src/main/java/edu/rpi/rair/PlanMethod.java
View file

@ -111,13 +111,18 @@ public class PlanMethod {
}
/* (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)]})
*/
@Override
public String toString() {
return "PlanMethod{" +
"backGroundStatePreconditions=" + backGroundStatePreconditions +
", goalPreconditions=" + goalPreconditions +
", freeVariables=" + freeVariables +
", actionCompounds=" + actionCompounds +
'}';
return "(define-method planMethod " + freeVariables.toString().replace(",", " ") + "\n" +
"\t{:goal " + goalPreconditions.toString().replace(",", " ") + "\n" +
"\t:while " + backGroundStatePreconditions.toString().replace(",", " ") + "\n" +
"\t:actions " + actionCompounds.toString().replace(",", " ") + "})";
}
}

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

@ -15,4 +15,7 @@ public interface Planner {
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);
}

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

@ -10,19 +10,18 @@ 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.*;
import java.util.function.Function;
import java.util.stream.Collectors;
/**
* Created by naveensundarg on 12/19/17.
*/
public class SimpleInducer implements Inducer{
public class SimpleInducer implements Inducer {
@Override
public Plan induce(PlanningProblem planningProblem, State start, Goal goal, Plan plan) {
public PlanMethod induce(PlanningProblem planningProblem, State start, Goal goal, Plan plan) {
List<Action> actionList = plan.getActions();
@ -41,9 +40,14 @@ public class SimpleInducer implements Inducer{
Map<Value, Variable> valueVariableMap = Commons.makeVariables(values);
Function<Set<Formula>,Set<Formula>> getRelevantFormula = formulae -> formulae.stream().
filter(formula -> !Sets.intersection(values, formula.valuesPresent()).isEmpty()).
Function<Set<Formula>,Set<Formula>> getRelevantFormula = formulae -> {
return formulae.stream().
filter(formula -> Sets.difference(formula.valuesPresent().stream().filter(Value::isConstant).collect(Collectors.toSet()),
values).isEmpty() &&
!Sets.intersection(values, formula.valuesPresent()).isEmpty()).
collect(Collectors.toSet());
};
Set<Formula> relevantBackgroundFormula = getRelevantFormula.apply(backgroundFormula);
Set<Formula> relevantInitFormula = getRelevantFormula.apply(initFormula);
@ -58,6 +62,14 @@ public class SimpleInducer implements Inducer{
System.out.println(relevantInitFormula);
System.out.println(relevantGoalFormula);
return null;
//PlanMethod(Set<Formula> goalPreconditions, Set<Formula> backGroundStatePreconditions, List<Variable> freeVariables, List<Compound> actionCompounds
return new PlanMethod(Commons.generalize(valueVariableMap, relevantGoalFormula),
Sets.union(Commons.generalize(valueVariableMap, relevantBackgroundFormula),
Commons.generalize(valueVariableMap, relevantInitFormula)),
new ArrayList<>(valueVariableMap.values()), actionCompounds.stream().map(x-> (Compound) x.generalize(valueVariableMap)).
collect(Collectors.toList()));
}
}

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

@ -12,6 +12,7 @@ import com.naveensundarg.shadow.prover.utils.Sets;
import edu.rpi.rair.State;
import us.bpsm.edn.parser.Parseable;
import java.util.ArrayList;
import java.util.Map;
import java.util.Set;
import java.util.function.BiFunction;
@ -49,25 +50,10 @@ public class Commons {
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);
public static Set<Formula> generalize(Map<Value, Variable> universalValueVariableMap, Set<Formula> formulae){
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));
return formulae.stream().map(x->x.generalize(universalValueVariableMap)).collect(Collectors.toSet());
}
public static <U, V> Map<V, U> reverse(Map<U, V> map){
@ -104,5 +90,10 @@ public class Commons {
return w;
}
public static And makeAnd(Set<Formula> formulae){
return new And(new ArrayList<>(formulae));
}
}

16
src/main/java/edu/rpi/rair/utils/GoalTrackingProblem.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.Reader;
import edu.rpi.rair.Goal;
import edu.rpi.rair.PlanMethod;
import edu.rpi.rair.State;
import us.bpsm.edn.Keyword;
import us.bpsm.edn.parser.Parseable;
@ -16,6 +17,8 @@ import java.io.InputStream;
import java.io.InputStreamReader;
import java.util.*;
import static edu.rpi.rair.utils.Reader.readPlanMethodsFrom;
/**
* Created by naveensundarg on 1/13/17.
*/
@ -32,6 +35,7 @@ public class GoalTrackingProblem {
private static final Keyword PRIORITY = Keyword.newKeyword("priority");
private static final Keyword STATE = Keyword.newKeyword("state");
public GoalTrackingProblem(PlanningProblem planningProblem, Set<Goal> goals) {
this.planningProblem = planningProblem;
this.goals = goals;
@ -44,6 +48,18 @@ public class GoalTrackingProblem {
}
public static List<GoalTrackingProblem> readFromFiles(InputStream definitionInputStream, InputStream methodsInputStream) throws Reader.ParsingException {
List<GoalTrackingProblem> goalTrackingProblems = readFromFile(definitionInputStream);
List<PlanMethod> planMethods = readPlanMethodsFrom(methodsInputStream);
goalTrackingProblems.stream().map(GoalTrackingProblem::getPlanningProblem).forEach(x->x.addToPlanMethods(planMethods));
return goalTrackingProblems;
}
public static List<GoalTrackingProblem> readFromFile(InputStream inputStream) throws Reader.ParsingException {
Parseable parseable = Parsers.newParseable(new InputStreamReader(inputStream));

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

@ -39,8 +39,10 @@ public class LearningSystem {
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")));
List<GoalTrackingProblem> goalTrackingProblemList1 = (GoalTrackingProblem.readFromFiles(Sandbox.class.getResourceAsStream("../problems/seriated/seriated_challenge_1.clj"),
Sandbox.class.getResourceAsStream("../problems/seriated/methods.clj")));
List<GoalTrackingProblem> goalTrackingProblemList2 = (GoalTrackingProblem.readFromFiles(Sandbox.class.getResourceAsStream("../problems/seriated/seriated_challenge_2.clj"),
Sandbox.class.getResourceAsStream("../problems/seriated/methods.clj")));
GoalTrackingProblem goalTrackingProblem1 = goalTrackingProblemList1.get(0);

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

@ -9,6 +9,7 @@ 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.PlanMethod;
import edu.rpi.rair.State;
import us.bpsm.edn.Keyword;
import us.bpsm.edn.Symbol;
@ -38,6 +39,7 @@ public class PlanningProblem {
private Map<String, Action> actionMap;
private Set<Value> avoidIfPossible;
private final List<PlanMethod> planMethods;
private static final Keyword BACKGROUND = Keyword.newKeyword("background");
private static final Keyword START = Keyword.newKeyword("start");
@ -63,7 +65,7 @@ public class PlanningProblem {
this.name = name;
this.actionMap = CollectionUtils.newMap();
this.avoidIfPossible = avoidIfPossible;
this.planMethods = CollectionUtils.newEmptyList();
this.expectedActionSequencesOpt = Optional.empty();
}
@ -77,6 +79,7 @@ public class PlanningProblem {
this.name = name;
this.actionMap = CollectionUtils.newMap();
this.avoidIfPossible = avoidIfPossible;
this.planMethods = CollectionUtils.newEmptyList();
this.expectedActionSequencesOpt = Optional.of(expectedActionSequences);
}
@ -340,6 +343,15 @@ public class PlanningProblem {
return avoidIfPossible;
}
public List<PlanMethod> getPlanMethods() {
return planMethods;
}
public void addToPlanMethods(List<PlanMethod> methods){
planMethods.addAll(methods);
}
@Override
public String toString() {
return "PlanningProblem{" +

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

@ -5,8 +5,7 @@ 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.sandboxes.Sandbox;
import com.naveensundarg.shadow.prover.utils.Problem;
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.*;
@ -62,14 +61,14 @@ public class RunDemo {
Visualizer.setShouldVisualize(false);
runProblem("seriated_challenge_1.clj");
runProblem("../problems/seriated/seriated_challenge_1.clj");
// runProblem("seriated_challenge_2.clj");
}
private static void runProblem(String name) throws Reader.ParsingException {
List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream(name)));
List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Sandbox.class.getResourceAsStream(name)));
GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0);
@ -130,10 +129,10 @@ public class RunDemo {
public static void planningProblemWarmUp() throws Reader.ParsingException {
for (int i = 0; i < 0; i++) {
for (int i = 0; i < 1; i++) {
List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_1.clj")));
List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Sandbox.class.getResourceAsStream("../problems/prisoner/goal_management_1.clj")));
GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0);
@ -184,7 +183,7 @@ public class RunDemo {
Optional<Plan> possibleGoalPlan = goalTracker.adoptGoal(g);
if (possibleGoalPlan.isPresent()) {
simpleInducer.induce(goalTracker.getProblem(), goalTracker.getProblem().getStart(), g, possibleGoalPlan.get());
System.out.println(simpleInducer.induce(goalTracker.getProblem(), goalTracker.getProblem().getStart(), g, possibleGoalPlan.get()));
printSuccessLater("Successfully added:", g.getName());
printDebug1Later("Current Goals and Constraint:", "\n" + goalTracker.getCurrentGoals().stream().collect(Collectors.toSet()).toString());

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

@ -17,6 +17,7 @@ public class Sandbox {
List<GoalTrackingProblem> goalTrackingProblemList1 = (GoalTrackingProblem.readFromFile(Sandbox.class.getResourceAsStream("../problems/seriated/seriated_challenge_1.clj")));
List<GoalTrackingProblem> goalTrackingProblemList2 = (GoalTrackingProblem.readFromFile(Sandbox.class.getResourceAsStream("../problems/seriated/seriated_challenge_2.clj")));
System.out.println(seriatedPlanMethod.apply(goalTrackingProblemList1.get(0).getPlanningProblem().getBackground(),
goalTrackingProblemList1.get(0).getPlanningProblem().getStart().getFormulae(),
@ -26,6 +27,15 @@ public class Sandbox {
));
System.out.println(seriatedPlanMethod.apply(goalTrackingProblemList2.get(0).getPlanningProblem().getBackground(),
goalTrackingProblemList2.get(0).getPlanningProblem().getStart().getFormulae(),
goalTrackingProblemList2.get(0).getGoalNamed("G1").getGoalState().getFormulae(),
goalTrackingProblemList2.get(0).getPlanningProblem().getActions()
));
}
}

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

@ -1,9 +1,7 @@
;; (removeFrom ?x ?y) => "Remove ?x from ?y"
;; (placeInside ?x ?y) ==> "Place ?x inside ?y"
(define-method planMethod [?b ?c ?d]
(define-method planMethod [?b ?d ?c]
{:goal [(In ?b ?c) (In ?c ?d)]
:while [(In ?b ?d) (Empty ?c)
(< (size ?c) (size ?d))
(< (size ?b) (size ?c))]
:while [(< (size ?c) (size ?d)) (< (size ?b) (size ?c)) (In ?b ?d) (Empty ?c)]
:actions [(removeFrom ?b ?d) (placeInside ?b ?c) (placeInside ?c ?d)]})

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

@ -20,11 +20,7 @@
;;; 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))]
(< (size c) (size d))]
:start [(In a b)
@ -46,12 +42,17 @@
:deletions [(In ?x ?y)]})]}
:goals {G1 {:priority 1.0
:context { :work-from-scratch false
:plan-methods
(define-method planMethod [?b ?d ?c]
{:goal [(In ?b ?c) (In ?c ?d)]
:while [(< (size ?c) (size ?d)) (< (size ?b) (size ?c)) (In ?b ?d) (Empty ?c)]
:actions [(removeFrom ?b ?d) (placeInside ?b ?c) (placeInside ?c ?d)]})}
:state [(In a b)
(In b c)
(In c d)]}}
;;(removeFrom b d) (placeInside b c) (placeInside c d)
}

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

@ -54,14 +54,17 @@
}
: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)
]}}
(In g h)]
}}
;;(removeFrom b d) (placeInside b c) (placeInside c d)