mirror of
https://github.com/RAIRLab/Spectra.git
synced 2024-09-19 07:15:12 -04:00
First commit
This commit is contained in:
Naveen Sundar Govindarajulu
commit
ecd7c00454
12 changed files with 1020 additions and 0 deletions
134
src/main/java/edu/rpi/rair/Action.java
Normal file
134
src/main/java/edu/rpi/rair/Action.java
Normal file
|
|
@ -0,0 +1,134 @@
|
||||||
|
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.Value;
|
||||||
|
import com.naveensundarg.shadow.prover.representations.value.Variable;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.CollectionUtils;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.Sets;
|
||||||
|
|
||||||
|
import java.util.List;
|
||||||
|
import java.util.Map;
|
||||||
|
import java.util.Set;
|
||||||
|
import java.util.stream.Collectors;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Created by naveensundarg on 1/13/17.
|
||||||
|
*/
|
||||||
|
public class Action {
|
||||||
|
|
||||||
|
private final Set<Formula> preconditions;
|
||||||
|
private final Set<Formula> additions;
|
||||||
|
private final Set<Formula> deletions;
|
||||||
|
private final List<Variable> freeVariables;
|
||||||
|
|
||||||
|
private final String name;
|
||||||
|
private final Formula precondition;
|
||||||
|
|
||||||
|
private int weight;
|
||||||
|
|
||||||
|
private Action(String name, Set<Formula> preconditions, Set<Formula> additions, Set<Formula> deletions, List<Variable> freeVariables) {
|
||||||
|
this.name = name;
|
||||||
|
this.preconditions = preconditions;
|
||||||
|
|
||||||
|
this.additions = additions;
|
||||||
|
this.deletions = deletions;
|
||||||
|
List<Variable> computedFreeVariables = preconditions.
|
||||||
|
stream().
|
||||||
|
map(x -> Sets.difference(x.variablesPresent(), x.boundVariablesPresent())).
|
||||||
|
reduce(Sets.newSet(), Sets::union).
|
||||||
|
stream().sorted().collect(Collectors.toList());
|
||||||
|
|
||||||
|
this.freeVariables = freeVariables;
|
||||||
|
|
||||||
|
this.precondition = new And(preconditions.stream().collect(Collectors.toList()));
|
||||||
|
|
||||||
|
this.weight = preconditions.stream().mapToInt(Formula::getWeight).sum() +
|
||||||
|
additions.stream().mapToInt(Formula::getWeight).sum() +
|
||||||
|
deletions.stream().mapToInt(Formula::getWeight).sum();
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
public static Action buildActionFrom(String name,
|
||||||
|
Set<Formula> preconditions,
|
||||||
|
Set<Formula> additions,
|
||||||
|
Set<Formula> deletions,
|
||||||
|
List<Variable> freeVariables) {
|
||||||
|
|
||||||
|
return new Action(name, preconditions, additions, deletions, freeVariables);
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
public int getWeight() {
|
||||||
|
return weight;
|
||||||
|
}
|
||||||
|
|
||||||
|
public Formula getPrecondition() {
|
||||||
|
return precondition;
|
||||||
|
}
|
||||||
|
|
||||||
|
public List<Variable> openVars() {
|
||||||
|
|
||||||
|
return freeVariables;
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
public Set<Formula> instantiateAdditions(Map<Variable, Value> mapping) {
|
||||||
|
|
||||||
|
return additions.stream().map(x -> x.apply(mapping)).collect(Collectors.toSet());
|
||||||
|
}
|
||||||
|
|
||||||
|
public Set<Formula> instantiateDeletions(Map<Variable, Value> mapping) {
|
||||||
|
|
||||||
|
return deletions.stream().map(x -> x.apply(mapping)).collect(Collectors.toSet());
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
public Action instantiate(Map<Variable, Value> binding){
|
||||||
|
|
||||||
|
Set<Formula> newPreconditions = preconditions.stream().map(x->x.apply(binding)).collect(Collectors.toSet());
|
||||||
|
Set<Formula> newAdditions = additions.stream().map(x->x.apply(binding)).collect(Collectors.toSet());
|
||||||
|
Set<Formula> newDeletions = deletions.stream().map(x->x.apply(binding)).collect(Collectors.toSet());
|
||||||
|
|
||||||
|
List<Variable> newFreeVraibles = CollectionUtils.newEmptyList();
|
||||||
|
for(Variable var: freeVariables){
|
||||||
|
|
||||||
|
if(!binding.keySet().contains(var)){
|
||||||
|
newFreeVraibles.add(var);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
return new Action(name, newPreconditions, newAdditions, newDeletions, newFreeVraibles);
|
||||||
|
}
|
||||||
|
@Override
|
||||||
|
public String toString() {
|
||||||
|
return "Action{" +
|
||||||
|
"preconditions=" + preconditions +
|
||||||
|
", additions=" + additions +
|
||||||
|
", deletions=" + deletions +
|
||||||
|
", name='" + name + '\'' +
|
||||||
|
'}';
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public boolean equals(Object o) {
|
||||||
|
if (this == o) return true;
|
||||||
|
if (o == null || getClass() != o.getClass()) return false;
|
||||||
|
|
||||||
|
Action action = (Action) o;
|
||||||
|
|
||||||
|
if (!preconditions.equals(action.preconditions)) return false;
|
||||||
|
if (!additions.equals(action.additions)) return false;
|
||||||
|
if (!deletions.equals(action.deletions)) return false;
|
||||||
|
return name.equals(action.name);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public int hashCode() {
|
||||||
|
int result = preconditions.hashCode();
|
||||||
|
result = 31 * result + additions.hashCode();
|
||||||
|
result = 31 * result + deletions.hashCode();
|
||||||
|
result = 31 * result + name.hashCode();
|
||||||
|
return result;
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
70
src/main/java/edu/rpi/rair/DepthFirstPlanner.java
Normal file
70
src/main/java/edu/rpi/rair/DepthFirstPlanner.java
Normal file
|
|
@ -0,0 +1,70 @@
|
||||||
|
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.Pair;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.Sets;
|
||||||
|
|
||||||
|
import java.util.*;
|
||||||
|
import java.util.stream.Collectors;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Created by naveensundarg on 1/13/17.
|
||||||
|
*/
|
||||||
|
public class DepthFirstPlanner implements Planner {
|
||||||
|
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public Optional<Set<Plan>> plan(Set<Formula> background, Set<Action> actions, State start, State goal) {
|
||||||
|
|
||||||
|
|
||||||
|
if (Operations.satisfies(background, start, goal)) {
|
||||||
|
//Already satisfied. Do nothing. Return a set with an empty plan.
|
||||||
|
return Optional.of(Sets.with(Plan.newEmptyPlan(goal, background)));
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
Set<Plan> allPlans = Sets.newSet();
|
||||||
|
boolean atleastOnePlanFound = false;
|
||||||
|
|
||||||
|
for (Action action : actions) {
|
||||||
|
|
||||||
|
Optional<Pair<State, Action>> nextStateActionPair = Operations.apply(background, action, start);
|
||||||
|
|
||||||
|
if (nextStateActionPair.isPresent()) {
|
||||||
|
|
||||||
|
Optional<Set<Plan>> planOpt = plan(background, actions, nextStateActionPair.get().first(), goal);
|
||||||
|
|
||||||
|
if (planOpt.isPresent()) {
|
||||||
|
|
||||||
|
atleastOnePlanFound = true;
|
||||||
|
Set<Plan> nextPlans = planOpt.get();
|
||||||
|
|
||||||
|
State nextSate = nextStateActionPair.get().first();
|
||||||
|
Action instantiatedAction = nextStateActionPair.get().second();
|
||||||
|
|
||||||
|
Set<Plan> augmentedPlans = nextPlans.stream().
|
||||||
|
map(plan -> plan.getPlanByStartingWith(instantiatedAction, nextSate)).
|
||||||
|
collect(Collectors.toSet());
|
||||||
|
|
||||||
|
allPlans.addAll(augmentedPlans);
|
||||||
|
//TODO: store different plans and return the best plan.
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
if (atleastOnePlanFound) {
|
||||||
|
|
||||||
|
return Optional.of(allPlans);
|
||||||
|
|
||||||
|
} else {
|
||||||
|
|
||||||
|
//No plan found.
|
||||||
|
return Optional.empty();
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
|
}
|
||||||
55
src/main/java/edu/rpi/rair/Goal.java
Normal file
55
src/main/java/edu/rpi/rair/Goal.java
Normal file
|
|
@ -0,0 +1,55 @@
|
||||||
|
package edu.rpi.rair;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Created by naveensundarg on 1/14/17.
|
||||||
|
*/
|
||||||
|
public class Goal {
|
||||||
|
|
||||||
|
private final State goalState;
|
||||||
|
private final int priority;
|
||||||
|
|
||||||
|
private Goal(State goalState, int priority) {
|
||||||
|
this.goalState = goalState;
|
||||||
|
this.priority = priority;
|
||||||
|
}
|
||||||
|
|
||||||
|
public static Goal makeGoal(State goalState, int priority){
|
||||||
|
|
||||||
|
return new Goal(goalState, priority);
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
public State getGoalState() {
|
||||||
|
return goalState;
|
||||||
|
}
|
||||||
|
|
||||||
|
public int getPriority() {
|
||||||
|
return priority;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public String toString() {
|
||||||
|
return "Goal{" +
|
||||||
|
"goalState=" + goalState +
|
||||||
|
", priority=" + priority +
|
||||||
|
'}';
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public boolean equals(Object o) {
|
||||||
|
if (this == o) return true;
|
||||||
|
if (o == null || getClass() != o.getClass()) return false;
|
||||||
|
|
||||||
|
Goal goal = (Goal) o;
|
||||||
|
|
||||||
|
if (priority != goal.priority) return false;
|
||||||
|
return goalState.equals(goal.goalState);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public int hashCode() {
|
||||||
|
int result = goalState.hashCode();
|
||||||
|
result = 31 * result + priority;
|
||||||
|
return result;
|
||||||
|
}
|
||||||
|
}
|
||||||
107
src/main/java/edu/rpi/rair/GoalTracker.java
Normal file
107
src/main/java/edu/rpi/rair/GoalTracker.java
Normal file
|
|
@ -0,0 +1,107 @@
|
||||||
|
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.Pair;
|
||||||
|
|
||||||
|
import java.util.List;
|
||||||
|
import java.util.Optional;
|
||||||
|
import java.util.Set;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Created by naveensundarg on 1/14/17.
|
||||||
|
*/
|
||||||
|
public class GoalTracker {
|
||||||
|
|
||||||
|
|
||||||
|
private final Set<Formula> background;
|
||||||
|
private State currentState;
|
||||||
|
private final Set<Goal> currentGoals;
|
||||||
|
private final Planner planner;
|
||||||
|
private final Set<Action> actions;
|
||||||
|
|
||||||
|
public GoalTracker(Set<Formula> background, State startState, Set<Action> actions) {
|
||||||
|
this.background = background;
|
||||||
|
this.currentState = startState;
|
||||||
|
this.currentGoals = CollectionUtils.newEmptySet();
|
||||||
|
this.planner = new DepthFirstPlanner();
|
||||||
|
this.actions = actions;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
public boolean adoptGoal(Goal goal) {
|
||||||
|
|
||||||
|
|
||||||
|
Optional<Set<Plan>> possiblePlans = planner.plan(background, actions, currentState, goal.getGoalState());
|
||||||
|
|
||||||
|
if (!possiblePlans.isPresent()) {
|
||||||
|
|
||||||
|
return false;
|
||||||
|
|
||||||
|
} else if (possiblePlans.get().isEmpty()) {
|
||||||
|
|
||||||
|
throw new AssertionError("Unexpected condition: possible plans is empty");
|
||||||
|
|
||||||
|
} else {
|
||||||
|
|
||||||
|
Set<Plan> plans = possiblePlans.get();
|
||||||
|
|
||||||
|
|
||||||
|
if (plans.stream().anyMatch(plan -> plan.noConflicts(currentGoals))) {
|
||||||
|
|
||||||
|
/*
|
||||||
|
* If there is any plan without any goal conflicts, then adopt the goal.
|
||||||
|
*/
|
||||||
|
currentGoals.add(goal);
|
||||||
|
return true;
|
||||||
|
|
||||||
|
} else {
|
||||||
|
|
||||||
|
/*
|
||||||
|
* Find goals to drop.
|
||||||
|
* For each plan, find the sum of the priorities of the goals that conflict.
|
||||||
|
* If any plan exists, where sum of priorities of existing goals is less than the new goal,
|
||||||
|
* add the new goal and remove the conflict goals.
|
||||||
|
* Otherwise return false and don't adopt the new goal.
|
||||||
|
*/
|
||||||
|
|
||||||
|
boolean feasiblePlanExists = false;
|
||||||
|
int bestPriorityGap = 0;
|
||||||
|
Set<Goal> bestRemovalCandidates = null;
|
||||||
|
for (Plan plan : plans) {
|
||||||
|
|
||||||
|
Set<Goal> conflictingGoals = plan.getConflictingGoals(currentGoals);
|
||||||
|
int conflictSum = conflictingGoals.stream().mapToInt(Goal::getPriority).sum();
|
||||||
|
int gap = goal.getPriority() - conflictSum;
|
||||||
|
|
||||||
|
if(gap > 0 && gap > bestPriorityGap ){
|
||||||
|
|
||||||
|
feasiblePlanExists = true;
|
||||||
|
bestPriorityGap = gap;
|
||||||
|
bestRemovalCandidates= conflictingGoals;
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
if(feasiblePlanExists){
|
||||||
|
|
||||||
|
currentGoals.removeAll(bestRemovalCandidates);
|
||||||
|
currentGoals.add(goal);
|
||||||
|
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
else {
|
||||||
|
|
||||||
|
return false;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
80
src/main/java/edu/rpi/rair/Operations.java
Normal file
80
src/main/java/edu/rpi/rair/Operations.java
Normal file
|
|
@ -0,0 +1,80 @@
|
||||||
|
package edu.rpi.rair;
|
||||||
|
|
||||||
|
import com.naveensundarg.shadow.prover.core.Prover;
|
||||||
|
import com.naveensundarg.shadow.prover.core.SnarkWrapper;
|
||||||
|
import com.naveensundarg.shadow.prover.representations.formula.And;
|
||||||
|
import com.naveensundarg.shadow.prover.representations.formula.Formula;
|
||||||
|
import com.naveensundarg.shadow.prover.representations.value.Value;
|
||||||
|
import com.naveensundarg.shadow.prover.representations.value.Variable;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.ImmutablePair;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.Pair;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.Sets;
|
||||||
|
|
||||||
|
import java.util.List;
|
||||||
|
import java.util.Map;
|
||||||
|
import java.util.Optional;
|
||||||
|
import java.util.Set;
|
||||||
|
import java.util.stream.Collectors;
|
||||||
|
|
||||||
|
import static edu.rpi.rair.State.FALSE;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Created by naveensundarg on 1/13/17.
|
||||||
|
*/
|
||||||
|
public class Operations {
|
||||||
|
|
||||||
|
private static Prover prover;
|
||||||
|
|
||||||
|
static{
|
||||||
|
prover = new SnarkWrapper();
|
||||||
|
}
|
||||||
|
|
||||||
|
public static synchronized Optional<Map<Variable, Value>> proveAndGetBindings(Set<Formula> givens, Formula goal, List<Variable> variables){
|
||||||
|
|
||||||
|
return prover.proveAndGetBindings(givens, goal, variables);
|
||||||
|
}
|
||||||
|
|
||||||
|
public static Optional<Pair<State,Action>> apply(Set<Formula> background, Action action, State state){
|
||||||
|
|
||||||
|
Prover prover = new SnarkWrapper();
|
||||||
|
|
||||||
|
|
||||||
|
Set<Formula> givens = Sets.union(background, state.getFormulae());
|
||||||
|
|
||||||
|
Optional<Map<Variable, Value>> bingdingsOpt = proveAndGetBindings(givens, action.getPrecondition(), action.openVars());
|
||||||
|
|
||||||
|
State newState;
|
||||||
|
|
||||||
|
if(!bingdingsOpt.isPresent()){
|
||||||
|
|
||||||
|
|
||||||
|
return Optional.empty();
|
||||||
|
|
||||||
|
}
|
||||||
|
Set<Formula> newFormulae = state.getFormulae();
|
||||||
|
|
||||||
|
newFormulae = Sets.union(newFormulae, action.instantiateAdditions(bingdingsOpt.get()));
|
||||||
|
|
||||||
|
newFormulae = Sets.difference(newFormulae, action.instantiateDeletions(bingdingsOpt.get()));
|
||||||
|
|
||||||
|
newState = State.initializeWith(newFormulae);
|
||||||
|
|
||||||
|
return Optional.of(ImmutablePair.from(newState, action.instantiate(bingdingsOpt.get())));
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
public static boolean satisfies(Set<Formula> background, State state, State goal){
|
||||||
|
|
||||||
|
return goal.getFormulae().stream().
|
||||||
|
allMatch(x->prover.prove(Sets.union(background, state.getFormulae()), x).isPresent());
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
public static boolean conflicts(Set<Formula> background, State state1, State state2){
|
||||||
|
|
||||||
|
return prover.prove(Sets.union(background, Sets.union(state1.getFormulae(), state2.getFormulae())), FALSE ).isPresent();
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
87
src/main/java/edu/rpi/rair/Plan.java
Normal file
87
src/main/java/edu/rpi/rair/Plan.java
Normal file
|
|
@ -0,0 +1,87 @@
|
||||||
|
package edu.rpi.rair;
|
||||||
|
|
||||||
|
import com.naveensundarg.shadow.prover.representations.formula.Formula;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.CollectionUtils;
|
||||||
|
|
||||||
|
import java.util.List;
|
||||||
|
import java.util.Set;
|
||||||
|
import java.util.stream.Collectors;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Created by naveensundarg on 1/14/17.
|
||||||
|
*/
|
||||||
|
public class Plan {
|
||||||
|
|
||||||
|
private final List<Action> actions;
|
||||||
|
private final List<State> expectedStates;
|
||||||
|
private final Set<Formula> background;
|
||||||
|
public static Plan newEmptyPlan(State currentState, Set<Formula> background){
|
||||||
|
List<Action> newActions = CollectionUtils.newEmptyList();
|
||||||
|
List<State> newExpectedStates = CollectionUtils.listOf(currentState);
|
||||||
|
return new Plan(newActions, newExpectedStates, background);
|
||||||
|
}
|
||||||
|
|
||||||
|
public Plan(List<Action> actions, List<State> expectedStates, Set<Formula> background) {
|
||||||
|
this.actions = actions;
|
||||||
|
this.expectedStates = expectedStates;
|
||||||
|
this.background = background;
|
||||||
|
}
|
||||||
|
|
||||||
|
public List<Action> getActions() {
|
||||||
|
return actions;
|
||||||
|
}
|
||||||
|
|
||||||
|
public Plan getPlanByStartingWith(Action action, State state){
|
||||||
|
List<Action> newActions = CollectionUtils.newEmptyList();
|
||||||
|
newActions.addAll(actions);
|
||||||
|
newActions.add(0, action);
|
||||||
|
|
||||||
|
List<State> newExpectedStates = CollectionUtils.newEmptyList();
|
||||||
|
newExpectedStates.addAll(expectedStates);
|
||||||
|
newExpectedStates.add(0, state);
|
||||||
|
|
||||||
|
return new Plan(newActions, newExpectedStates, background);
|
||||||
|
}
|
||||||
|
|
||||||
|
public boolean conflictsWith(Goal goal){
|
||||||
|
|
||||||
|
return expectedStates.stream().anyMatch(state-> Operations.conflicts(background, state,goal.getGoalState()));
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
public Set<Goal> getConflictingGoals(Set<Goal> goals){
|
||||||
|
|
||||||
|
return goals.stream().filter(this::conflictsWith).collect(Collectors.toSet());
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
public boolean noConflicts(Set<Goal> goals){
|
||||||
|
|
||||||
|
return getConflictingGoals(goals).isEmpty();
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public String toString() {
|
||||||
|
return "Plan{" +
|
||||||
|
"actions=" + actions +
|
||||||
|
'}';
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public boolean equals(Object o) {
|
||||||
|
if (this == o) return true;
|
||||||
|
if (o == null || getClass() != o.getClass()) return false;
|
||||||
|
|
||||||
|
Plan plan = (Plan) o;
|
||||||
|
|
||||||
|
return actions != null ? actions.equals(plan.actions) : plan.actions == null;
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public int hashCode() {
|
||||||
|
return actions != null ? actions.hashCode() : 0;
|
||||||
|
}
|
||||||
|
}
|
||||||
16
src/main/java/edu/rpi/rair/Planner.java
Normal file
16
src/main/java/edu/rpi/rair/Planner.java
Normal file
|
|
@ -0,0 +1,16 @@
|
||||||
|
package edu.rpi.rair;
|
||||||
|
|
||||||
|
import com.naveensundarg.shadow.prover.representations.formula.Formula;
|
||||||
|
|
||||||
|
import java.util.List;
|
||||||
|
import java.util.Optional;
|
||||||
|
import java.util.Set;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Created by naveensundarg on 1/13/17.
|
||||||
|
*/
|
||||||
|
public interface Planner {
|
||||||
|
|
||||||
|
Optional<Set<Plan>> plan(Set<Formula> background, Set<Action> actions, State start, State goal);
|
||||||
|
|
||||||
|
}
|
||||||
83
src/main/java/edu/rpi/rair/State.java
Normal file
83
src/main/java/edu/rpi/rair/State.java
Normal file
|
|
@ -0,0 +1,83 @@
|
||||||
|
package edu.rpi.rair;
|
||||||
|
|
||||||
|
import com.naveensundarg.shadow.prover.core.Prover;
|
||||||
|
import com.naveensundarg.shadow.prover.core.SnarkWrapper;
|
||||||
|
import com.naveensundarg.shadow.prover.representations.formula.And;
|
||||||
|
import com.naveensundarg.shadow.prover.representations.formula.Formula;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.CollectionUtils;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.Reader;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.Sets;
|
||||||
|
|
||||||
|
import java.util.Set;
|
||||||
|
import java.util.stream.Collectors;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Created by naveensundarg on 1/13/17.
|
||||||
|
*/
|
||||||
|
public class State {
|
||||||
|
|
||||||
|
final Set<Formula> formulae;
|
||||||
|
private static final Prover prover = new SnarkWrapper();
|
||||||
|
static Formula FALSE;
|
||||||
|
|
||||||
|
static{
|
||||||
|
|
||||||
|
try {
|
||||||
|
FALSE = Reader.readFormulaFromString("(and P (not P))");
|
||||||
|
} catch (Reader.ParsingException e) {
|
||||||
|
e.printStackTrace();
|
||||||
|
FALSE = null;
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
private State(Set<Formula> formulae){
|
||||||
|
|
||||||
|
this.formulae = formulae;
|
||||||
|
}
|
||||||
|
|
||||||
|
public static State initializeWith(Set<Formula> formulae){
|
||||||
|
|
||||||
|
State newState = new State(formulae);
|
||||||
|
return newState;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
public void add(Set<Formula> formulae){
|
||||||
|
|
||||||
|
this.formulae.addAll(formulae);
|
||||||
|
}
|
||||||
|
|
||||||
|
public void remove(Set<Formula> formulae){
|
||||||
|
|
||||||
|
this.formulae.removeAll(formulae);
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
public Set<Formula> getFormulae() {
|
||||||
|
return CollectionUtils.setFrom(formulae);
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public String toString() {
|
||||||
|
return "State{" +
|
||||||
|
"formulae=" + formulae +
|
||||||
|
'}';
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public boolean equals(Object o) {
|
||||||
|
if (this == o) return true;
|
||||||
|
if (o == null || getClass() != o.getClass()) return false;
|
||||||
|
|
||||||
|
State state = (State) o;
|
||||||
|
|
||||||
|
return formulae.equals(state.formulae);
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public int hashCode() {
|
||||||
|
return formulae.hashCode();
|
||||||
|
}
|
||||||
|
}
|
||||||
169
src/main/java/edu/rpi/rair/utils/PlanningProblem.java
Normal file
169
src/main/java/edu/rpi/rair/utils/PlanningProblem.java
Normal file
|
|
@ -0,0 +1,169 @@
|
||||||
|
package edu.rpi.rair.utils;
|
||||||
|
|
||||||
|
import clojure.lang.Obj;
|
||||||
|
import com.naveensundarg.shadow.prover.representations.formula.Formula;
|
||||||
|
import com.naveensundarg.shadow.prover.representations.value.Variable;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.CollectionUtils;
|
||||||
|
import com.naveensundarg.shadow.prover.utils.Reader;
|
||||||
|
import edu.rpi.rair.Action;
|
||||||
|
import edu.rpi.rair.State;
|
||||||
|
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 us.bpsm.edn.parser.Token;
|
||||||
|
|
||||||
|
import java.io.InputStream;
|
||||||
|
import java.io.InputStreamReader;
|
||||||
|
import java.util.List;
|
||||||
|
import java.util.Map;
|
||||||
|
import java.util.Objects;
|
||||||
|
import java.util.Set;
|
||||||
|
import java.util.stream.Collectors;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Created by naveensundarg on 1/13/17.
|
||||||
|
*/
|
||||||
|
public class PlanningProblem {
|
||||||
|
|
||||||
|
public Set<Formula> background;
|
||||||
|
public Set<Action> actions;
|
||||||
|
public State start;
|
||||||
|
public State goal;
|
||||||
|
public String name;
|
||||||
|
|
||||||
|
private static final Keyword BACKGROUND = Keyword.newKeyword("background");
|
||||||
|
private static final Keyword START = Keyword.newKeyword("start");
|
||||||
|
private static final Keyword GOAL = Keyword.newKeyword("goal");
|
||||||
|
private static final Keyword NAME = Keyword.newKeyword("name");
|
||||||
|
private static final Keyword ACTION = Keyword.newKeyword("actions");
|
||||||
|
|
||||||
|
private static final Keyword PRECONDITIONS = Keyword.newKeyword("preconditions");
|
||||||
|
private static final Keyword ADDITIONS = Keyword.newKeyword("additions");
|
||||||
|
private static final Keyword DELETIONS = Keyword.newKeyword("deletions");
|
||||||
|
|
||||||
|
private static final Symbol ACTION_DEFINER = Symbol.newSymbol("define-action");
|
||||||
|
|
||||||
|
|
||||||
|
public PlanningProblem(String name, Set<Formula> background, State start, State goal, Set<Action> actions) {
|
||||||
|
|
||||||
|
this.background = background;
|
||||||
|
this.start = start;
|
||||||
|
this.actions = actions;
|
||||||
|
this.goal = goal;
|
||||||
|
this.name = name;
|
||||||
|
}
|
||||||
|
|
||||||
|
public static List<PlanningProblem> readFromFile(InputStream inputStream) throws Reader.ParsingException {
|
||||||
|
|
||||||
|
Parseable parseable = Parsers.newParseable(new InputStreamReader(inputStream));
|
||||||
|
Parser parser = Parsers.newParser(Parsers.defaultConfiguration());
|
||||||
|
|
||||||
|
List<PlanningProblem> planningProblems = CollectionUtils.newEmptyList();
|
||||||
|
|
||||||
|
Object nextValue = parser.nextValue(parseable);
|
||||||
|
|
||||||
|
while (!nextValue.equals(Token.END_OF_INPUT)) {
|
||||||
|
|
||||||
|
Map<?, ?> planningProblemSpec = (Map<?, ?>) nextValue;
|
||||||
|
|
||||||
|
Set<Formula> background = readFrom((List<?>) planningProblemSpec.get(BACKGROUND));
|
||||||
|
Set<Formula> start = readFrom((List<?>) planningProblemSpec.get(START));
|
||||||
|
Set<Formula> goal = readFrom((List<?>) planningProblemSpec.get(GOAL));
|
||||||
|
|
||||||
|
List<?> actionDefinitions = (List<?>) planningProblemSpec.get(ACTION);
|
||||||
|
|
||||||
|
String name = planningProblemSpec.get(NAME).toString();
|
||||||
|
Set<Action> actions = readActionsFrom(actionDefinitions);
|
||||||
|
|
||||||
|
planningProblems.add(new PlanningProblem(name, background, State.initializeWith(start),
|
||||||
|
State.initializeWith(goal), actions));
|
||||||
|
|
||||||
|
nextValue = parser.nextValue(parseable);
|
||||||
|
}
|
||||||
|
|
||||||
|
return planningProblems;
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
private static Set<Action> readActionsFrom(List<?> actionSpecs) throws Reader.ParsingException {
|
||||||
|
|
||||||
|
Set<Action> actions = actionSpecs.stream().map(spec -> {
|
||||||
|
List<?> specBody = (List<?>) spec;
|
||||||
|
if(!specBody.get(0).equals(ACTION_DEFINER)){
|
||||||
|
|
||||||
|
return null;
|
||||||
|
}
|
||||||
|
String name = specBody.get(1).toString();
|
||||||
|
List<Variable> vars = ((List<?>)specBody.get(2)).stream().map(x -> {
|
||||||
|
try {
|
||||||
|
return Reader.readLogicValue(x);
|
||||||
|
} catch (Reader.ParsingException e) {
|
||||||
|
e.printStackTrace();
|
||||||
|
return null;
|
||||||
|
}
|
||||||
|
}).map(x->(Variable)x).collect(Collectors.toList());
|
||||||
|
|
||||||
|
if(vars.stream().anyMatch(Objects::isNull)){
|
||||||
|
return null;
|
||||||
|
}
|
||||||
|
Map<?, ?> actionSpec = (Map<?, ?>) specBody.get(3);
|
||||||
|
try {
|
||||||
|
|
||||||
|
|
||||||
|
Set<Formula> preconditions = readFrom((List<?>) actionSpec.get(PRECONDITIONS));
|
||||||
|
Set<Formula> additions = readFrom((List<?>) actionSpec.get(ADDITIONS));
|
||||||
|
Set<Formula> deletions = readFrom((List<?>) actionSpec.get(DELETIONS));
|
||||||
|
|
||||||
|
return Action.buildActionFrom(name, preconditions, additions, deletions, vars);
|
||||||
|
|
||||||
|
|
||||||
|
} catch (Reader.ParsingException e) {
|
||||||
|
e.printStackTrace();
|
||||||
|
return null;
|
||||||
|
}
|
||||||
|
}).collect(Collectors.toSet());
|
||||||
|
|
||||||
|
if (actions.stream().anyMatch(Objects::isNull)) {
|
||||||
|
|
||||||
|
throw new Reader.ParsingException("Couldn't read actions: " + actionSpecs);
|
||||||
|
}
|
||||||
|
|
||||||
|
return actions;
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
private static Set<Formula> readFrom(List<?> objects) throws Reader.ParsingException {
|
||||||
|
|
||||||
|
Set<Formula> formulae = objects.stream().map(x -> {
|
||||||
|
try {
|
||||||
|
return Reader.readFormula(x);
|
||||||
|
} catch (Reader.ParsingException e) {
|
||||||
|
e.printStackTrace();
|
||||||
|
return null;
|
||||||
|
}
|
||||||
|
}).collect(Collectors.toSet());
|
||||||
|
|
||||||
|
|
||||||
|
if (formulae.stream().anyMatch(Objects::isNull)) {
|
||||||
|
|
||||||
|
throw new Reader.ParsingException("Couldn't read formulae: " + objects);
|
||||||
|
}
|
||||||
|
|
||||||
|
return formulae;
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
@Override
|
||||||
|
public String toString() {
|
||||||
|
return "PlanningProblem{" +
|
||||||
|
"name='" + name + '\'' +
|
||||||
|
", background=" + background +
|
||||||
|
", actions=" + actions +
|
||||||
|
", start=" + start +
|
||||||
|
", goal=" + goal +
|
||||||
|
'}';
|
||||||
|
}
|
||||||
|
}
|
||||||
122
src/main/resources/edu/rpi/rair/completeness_problems.clj
Normal file
122
src/main/resources/edu/rpi/rair/completeness_problems.clj
Normal file
|
|
@ -0,0 +1,122 @@
|
||||||
|
{:name "test 1"
|
||||||
|
:background [P]
|
||||||
|
:start [Q]
|
||||||
|
:goal [R]
|
||||||
|
:actions
|
||||||
|
[(define-action a1 ()
|
||||||
|
{:preconditions [(or Q R)]
|
||||||
|
:additions [R]
|
||||||
|
:deletions [Q]})]
|
||||||
|
|
||||||
|
:expected-plan [a1]
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
{:name "simple killing"
|
||||||
|
:background []
|
||||||
|
:start [(forall ?x (Alive ?x))]
|
||||||
|
:goal [(forall ?x (Dead ?x))]
|
||||||
|
:actions
|
||||||
|
[(define-action kill ()
|
||||||
|
{:preconditions [(Alive ?x)]
|
||||||
|
:additions [(Dead ?x)]
|
||||||
|
:deletions [(Alive ?x)]})]
|
||||||
|
|
||||||
|
:expected-plans ([kill])
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
{:name "thirsty"
|
||||||
|
:background []
|
||||||
|
:start [thirsty]
|
||||||
|
:goal [(not thirsty)]
|
||||||
|
:actions
|
||||||
|
[(define-action drink ()
|
||||||
|
{:preconditions [thirsty]
|
||||||
|
:additions [(not thirsty)]
|
||||||
|
:deletions [thirsty]})
|
||||||
|
(define-action eat ()
|
||||||
|
{:preconditions [hungry]
|
||||||
|
:additions [(not hungry)]
|
||||||
|
:deletions [hungry]})]
|
||||||
|
|
||||||
|
:expected-plans ([drink])
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
{:name "hungry"
|
||||||
|
:background []
|
||||||
|
:start [hungry]
|
||||||
|
:goal [(not hungry)]
|
||||||
|
:actions
|
||||||
|
|
||||||
|
[(define-action drink ()
|
||||||
|
{:preconditions [thirsty]
|
||||||
|
:additions [(not thirsty)]
|
||||||
|
:deletions [thirsty]})
|
||||||
|
|
||||||
|
(define-action eat ()
|
||||||
|
{:preconditions [hungry]
|
||||||
|
:additions [(not hungry)]
|
||||||
|
:deletions [hungry]})]
|
||||||
|
|
||||||
|
:expected-plans ([eat])
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
{:name "hungry and thirsty"
|
||||||
|
:background []
|
||||||
|
:start [hungry thirsty]
|
||||||
|
:goal [(not (or hungry thirsty))]
|
||||||
|
:actions
|
||||||
|
[(define-action drink ()
|
||||||
|
{:preconditions [thirsty]
|
||||||
|
:additions [(not thirsty)]
|
||||||
|
:deletions [thirsty]})
|
||||||
|
|
||||||
|
(define-action eat ()
|
||||||
|
{:preconditions [hungry]
|
||||||
|
:additions [(not hungry)]
|
||||||
|
:deletions [hungry]})]
|
||||||
|
|
||||||
|
:expected-plans ([eat drink]
|
||||||
|
[drink eat])
|
||||||
|
}
|
||||||
|
|
||||||
|
{:name "hungry and thirsty"
|
||||||
|
:background []
|
||||||
|
:start [hungry thirsty work-unfinished]
|
||||||
|
:goal [work-finished]
|
||||||
|
:actions
|
||||||
|
|
||||||
|
[(define-action drink ()
|
||||||
|
{:preconditions [thirsty]
|
||||||
|
:additions [(not thirsty)]
|
||||||
|
:deletions [thirsty]})
|
||||||
|
|
||||||
|
(define-action eat ()
|
||||||
|
{:preconditions [hungry]
|
||||||
|
:additions [(not hungry)]
|
||||||
|
:deletions [hungry]})
|
||||||
|
|
||||||
|
(define-action work ()
|
||||||
|
{:preconditions [(and (not hungry) (not thirsty))]
|
||||||
|
:additions [work-finished]
|
||||||
|
:deletions [work-unfinished]})]
|
||||||
|
|
||||||
|
:expected-plans ([eat drink work]
|
||||||
|
[drink eat work])}
|
||||||
|
|
||||||
|
|
||||||
|
{:name "bidding problem"
|
||||||
|
:background []
|
||||||
|
:start [(bid 0)]
|
||||||
|
:goal [(bid 5)]
|
||||||
|
:actions
|
||||||
|
[(define-action post-new-bid (?number)
|
||||||
|
{:preconditions [(bid ?number)]
|
||||||
|
:additions [(bid ($$sum 1 ?number))]
|
||||||
|
:deletions [(bid ?number)]})]}
|
||||||
27
src/main/resources/edu/rpi/rair/goal_tracking_tests.clj
Normal file
27
src/main/resources/edu/rpi/rair/goal_tracking_tests.clj
Normal file
|
|
@ -0,0 +1,27 @@
|
||||||
|
{
|
||||||
|
:name "test 1"
|
||||||
|
:background [ (forall (?x ?y ?room1 ?room2)
|
||||||
|
(if (and (Interrogates ?x ?y)
|
||||||
|
(In ?x ?room1)
|
||||||
|
(In ?y ?room2))
|
||||||
|
(= ?room1 ?room2)))
|
||||||
|
|
||||||
|
(In commander room2)
|
||||||
|
()
|
||||||
|
]
|
||||||
|
:start [Be_In_Room
|
||||||
|
(Closed (door room1))
|
||||||
|
(Accompany self prisoner)]
|
||||||
|
|
||||||
|
:goalSequence [
|
||||||
|
[G1 1 [(In prisoner1 room1)]]
|
||||||
|
[G2 1 [(Closed (door room1))]]
|
||||||
|
[G3 1 [(Accompany self prisoner)]]
|
||||||
|
|
||||||
|
[G4 2 [(Interrogates command robot)]]
|
||||||
|
[G5 2 []]
|
||||||
|
|
||||||
|
]
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
70
src/test/java/edu/rpi/rair/DepthFirstPlannerTest.java
Normal file
70
src/test/java/edu/rpi/rair/DepthFirstPlannerTest.java
Normal file
|
|
@ -0,0 +1,70 @@
|
||||||
|
package edu.rpi.rair;
|
||||||
|
|
||||||
|
import com.naveensundarg.shadow.prover.utils.Reader;
|
||||||
|
import edu.rpi.rair.utils.PlanningProblem;
|
||||||
|
import org.testng.Assert;
|
||||||
|
import org.testng.annotations.BeforeMethod;
|
||||||
|
import org.testng.annotations.DataProvider;
|
||||||
|
import org.testng.annotations.Test;
|
||||||
|
|
||||||
|
import java.util.List;
|
||||||
|
import java.util.Optional;
|
||||||
|
import java.util.Set;
|
||||||
|
|
||||||
|
import static org.testng.Assert.*;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* Created by naveensundarg on 1/13/17.
|
||||||
|
*/
|
||||||
|
public class DepthFirstPlannerTest {
|
||||||
|
|
||||||
|
DepthFirstPlanner depthFirstPlanner;
|
||||||
|
|
||||||
|
@BeforeMethod
|
||||||
|
public void setUp() throws Exception {
|
||||||
|
|
||||||
|
depthFirstPlanner = new DepthFirstPlanner();
|
||||||
|
}
|
||||||
|
|
||||||
|
public static void main(String[] args) throws Reader.ParsingException {
|
||||||
|
|
||||||
|
List<PlanningProblem> planningProblemList = (PlanningProblem.readFromFile(Planner.class.getResourceAsStream("completeness_problems.clj")));
|
||||||
|
|
||||||
|
Planner depthFirstPlanner = new DepthFirstPlanner();
|
||||||
|
|
||||||
|
PlanningProblem planningProblem = planningProblemList.get(2);
|
||||||
|
System.out.println(depthFirstPlanner.plan(planningProblem.background, planningProblem.actions, planningProblem.start, planningProblem.goal));
|
||||||
|
}
|
||||||
|
|
||||||
|
@DataProvider
|
||||||
|
public static Object[][] testCompletenessDataProvider() throws Reader.ParsingException {
|
||||||
|
|
||||||
|
List<PlanningProblem> planningProblemList = (PlanningProblem.readFromFile(Planner.class.getResourceAsStream("completeness_problems.clj")));
|
||||||
|
|
||||||
|
Object[][] cases = new Object[planningProblemList.size()][1];
|
||||||
|
|
||||||
|
for (int i = 0; i < planningProblemList.size(); i++) {
|
||||||
|
|
||||||
|
cases[i][0] = planningProblemList.get(i);
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
return cases;
|
||||||
|
|
||||||
|
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
@Test(dataProvider = "testCompletenessDataProvider")
|
||||||
|
public void testCompletness(PlanningProblem planningProblem) throws Exception {
|
||||||
|
|
||||||
|
Optional<Set<Plan>> possiblePlans = depthFirstPlanner.plan(
|
||||||
|
planningProblem.background,
|
||||||
|
planningProblem.actions,
|
||||||
|
planningProblem.start,
|
||||||
|
planningProblem.goal);
|
||||||
|
|
||||||
|
Assert.assertTrue(possiblePlans.isPresent());
|
||||||
|
|
||||||
|
}
|
||||||
|
}
|
||||||
Loading…
Reference in a new issue