mirror of
https://github.com/RAIRLab/Spectra.git
synced 2024-09-19 07:15:12 -04:00
Speeding up things
This commit is contained in:
Naveen Sundar Govindarajulu
parent
b2da460d5c
commit
bfaaf6d882
5 changed files with 319 additions and 105 deletions
|
|
@ -5,6 +5,7 @@ import com.naveensundarg.shadow.prover.utils.CollectionUtils;
|
|||
import com.naveensundarg.shadow.prover.utils.Pair;
|
||||
import com.naveensundarg.shadow.prover.utils.Sets;
|
||||
|
||||
import javax.swing.text.html.Option;
|
||||
import java.util.*;
|
||||
import java.util.stream.Collectors;
|
||||
|
||||
|
|
@ -15,22 +16,40 @@ public class DepthFirstPlanner implements Planner {
|
|||
|
||||
|
||||
private static final int MAX_DEPTH = 4;
|
||||
private static final boolean EXHAUSTIVE_TILL_MAX_DEPTH = true;
|
||||
|
||||
|
||||
@Override
|
||||
public Optional<Set<Plan>> plan(Set<Formula> background, Set<Action> actions, State start, State goal) {
|
||||
|
||||
|
||||
return planInternal(Sets.newSet(), 0, background, actions, start, goal);
|
||||
if (!EXHAUSTIVE_TILL_MAX_DEPTH) {
|
||||
|
||||
return planInternal(Sets.newSet(), 0, MAX_DEPTH, background, actions, start, goal);
|
||||
|
||||
} else {
|
||||
|
||||
for (int i = 1; i <= MAX_DEPTH; i++) {
|
||||
|
||||
Optional<Set<Plan>> plans = planInternal(Sets.newSet(), 0, i, background, actions, start, goal);
|
||||
|
||||
if (plans.isPresent()) {
|
||||
return plans;
|
||||
}
|
||||
|
||||
}
|
||||
//
|
||||
return Optional.empty();
|
||||
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
||||
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, Set<Formula> background, Set<Action> actions, State start, State goal) {
|
||||
|
||||
if(currentDepth>=MAX_DEPTH){
|
||||
if (currentDepth >= maxDepth) {
|
||||
return Optional.empty();
|
||||
}
|
||||
|
||||
|
|
@ -52,8 +71,7 @@ public class DepthFirstPlanner implements Planner {
|
|||
for (Pair<State, Action> stateActionPair : nextStateActionPairs.get()) {
|
||||
|
||||
|
||||
|
||||
Optional<Set<Plan>> planOpt = planInternal(history, currentDepth+1, background, actions, stateActionPair.first(), goal);
|
||||
Optional<Set<Plan>> planOpt = planInternal(history, currentDepth + 1, maxDepth, background, actions, stateActionPair.first(), goal);
|
||||
|
||||
if (planOpt.isPresent()) {
|
||||
|
||||
|
|
|
|||
|
|
@ -2,6 +2,11 @@ package edu.rpi.rair.utils;
|
|||
|
||||
import com.diogonunes.jcdp.color.ColoredPrinter;
|
||||
import com.diogonunes.jcdp.color.api.Ansi;
|
||||
import com.naveensundarg.shadow.prover.Sandbox;
|
||||
import com.naveensundarg.shadow.prover.core.Problem;
|
||||
import com.naveensundarg.shadow.prover.core.Prover;
|
||||
import com.naveensundarg.shadow.prover.core.SnarkWrapper;
|
||||
import com.naveensundarg.shadow.prover.utils.ProblemReader;
|
||||
import com.naveensundarg.shadow.prover.utils.Reader;
|
||||
import edu.rpi.rair.Goal;
|
||||
import edu.rpi.rair.GoalTracker;
|
||||
|
|
@ -19,37 +24,124 @@ public class RunDemo {
|
|||
|
||||
static ColoredPrinter cp = new ColoredPrinter.Builder(1, false).build();
|
||||
|
||||
|
||||
static {
|
||||
|
||||
Prover prover = new SnarkWrapper();
|
||||
try {
|
||||
List<Problem> problems = ProblemReader.readFrom(Sandbox.class.getResourceAsStream("firstorder-completness-tests.clj"));
|
||||
|
||||
problems.forEach(problem -> {
|
||||
for (int i = 0; i < 5; i++) {
|
||||
prover.prove(problem.getAssumptions(), problem.getGoal());
|
||||
|
||||
}
|
||||
});
|
||||
|
||||
planningProblemWarmUp();
|
||||
System.out.println("WARM UP DONE");
|
||||
} catch (Reader.ParsingException e) {
|
||||
e.printStackTrace();
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
||||
public static void main(String[] args) throws Reader.ParsingException {
|
||||
|
||||
|
||||
List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_2.clj")));
|
||||
|
||||
System.out.println();
|
||||
|
||||
List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_3.clj")));
|
||||
|
||||
|
||||
GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0);
|
||||
GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0);
|
||||
|
||||
GoalTracker goalTracker = new GoalTracker(goalTrackingProblem.getPlanningProblem().getBackground(),
|
||||
goalTrackingProblem.getPlanningProblem().getStart(),
|
||||
goalTrackingProblem.getPlanningProblem().getActions());
|
||||
GoalTracker goalTracker = new GoalTracker(goalTrackingProblem.getPlanningProblem().getBackground(),
|
||||
goalTrackingProblem.getPlanningProblem().getStart(),
|
||||
goalTrackingProblem.getPlanningProblem().getActions());
|
||||
|
||||
long start = System.currentTimeMillis();
|
||||
long start = System.currentTimeMillis();
|
||||
|
||||
Goal g1 = goalTrackingProblem.getGoalNamed("G1");
|
||||
Goal g2 = goalTrackingProblem.getGoalNamed("G2");
|
||||
Goal g1 = goalTrackingProblem.getGoalNamed("G1");
|
||||
Goal g2 = goalTrackingProblem.getGoalNamed("G2");
|
||||
Goal g3 = goalTrackingProblem.getGoalNamed("G3");
|
||||
Goal g4 = goalTrackingProblem.getGoalNamed("G4");
|
||||
|
||||
tryAndAddGoal(g1, goalTracker);
|
||||
tryAndAddGoal(g2, goalTracker);
|
||||
|
||||
long end = System.currentTimeMillis();
|
||||
tryAndAddGoal(g1, goalTracker);
|
||||
|
||||
cp.println("--------------------------");
|
||||
cp.setForegroundColor(Ansi.FColor.CYAN);
|
||||
tryAndAddGoal(g2, goalTracker);
|
||||
|
||||
cp.print("Time Taken:");
|
||||
cp.clear();
|
||||
cp.print(" ");
|
||||
cp.setAttribute(Ansi.Attribute.BOLD);
|
||||
cp.print((end-start)/1000 + "s");
|
||||
tryAndAddGoal(g3, goalTracker);
|
||||
|
||||
tryAndAddGoal(g4, goalTracker);
|
||||
|
||||
|
||||
long end = System.currentTimeMillis();
|
||||
|
||||
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 + "s");
|
||||
|
||||
|
||||
|
||||
}
|
||||
|
||||
public static void planningProblemWarmUp() throws Reader.ParsingException {
|
||||
|
||||
|
||||
for (int i = 0; i < 5; i++) {
|
||||
|
||||
System.out.println();
|
||||
|
||||
List<GoalTrackingProblem> goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_1.clj")));
|
||||
|
||||
|
||||
GoalTrackingProblem goalTrackingProblem = goalTrackingProblemList.get(0);
|
||||
|
||||
GoalTracker goalTracker = new GoalTracker(goalTrackingProblem.getPlanningProblem().getBackground(),
|
||||
goalTrackingProblem.getPlanningProblem().getStart(),
|
||||
goalTrackingProblem.getPlanningProblem().getActions());
|
||||
|
||||
long start = System.currentTimeMillis();
|
||||
|
||||
Goal g1 = goalTrackingProblem.getGoalNamed("G1");
|
||||
Goal g2 = goalTrackingProblem.getGoalNamed("G2");
|
||||
Goal g3 = goalTrackingProblem.getGoalNamed("G3");
|
||||
Goal g4 = goalTrackingProblem.getGoalNamed("G4");
|
||||
Goal g5 = goalTrackingProblem.getGoalNamed("G5");
|
||||
|
||||
|
||||
goalTracker.adoptGoal(g1);
|
||||
|
||||
System.out.print(".");
|
||||
|
||||
goalTracker.adoptGoal(g2);
|
||||
|
||||
|
||||
System.out.print(".");
|
||||
|
||||
goalTracker.adoptGoal(g3);
|
||||
|
||||
System.out.print(".");
|
||||
|
||||
goalTracker.adoptGoal(g4);
|
||||
|
||||
System.out.print(".");
|
||||
|
||||
goalTracker.adoptGoal(g5);
|
||||
|
||||
System.out.print(".");
|
||||
|
||||
|
||||
}
|
||||
|
||||
|
||||
}
|
||||
|
|
@ -57,20 +149,20 @@ public class RunDemo {
|
|||
static void tryAndAddGoal(Goal g, GoalTracker goalTracker) {
|
||||
|
||||
System.out.println("========================");
|
||||
printInfo("Trying to Add Goal:", g.getName());
|
||||
printInfo("Trying to Add Goal:", g.getName());
|
||||
|
||||
Optional<Plan> possibleGoalPlan = goalTracker.adoptGoal(g);
|
||||
if (possibleGoalPlan.isPresent()) {
|
||||
|
||||
printSuccess("Successfully added:" , g.getName());
|
||||
printDebug1("Current Goals:" , goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()).toString());
|
||||
printSuccess("Successfully added:", g.getName());
|
||||
printDebug1("Current Goals:", goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()).toString());
|
||||
Plan plan = possibleGoalPlan.get();
|
||||
printDebug2("Plan:" , plan.getActions().isEmpty()? "No plan needed. Already satisfied." : plan.getActions().toString() );
|
||||
printDebug2("Plan:", plan.getActions().isEmpty() ? "No plan needed. Already satisfied." : plan.getActions().toString());
|
||||
|
||||
} else {
|
||||
|
||||
printFailure("Could not add " + g.getName());
|
||||
printDebug1("Current Goals: " , goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()).toString());
|
||||
printDebug1("Current Goals: ", goalTracker.getCurrentGoals().stream().map(Goal::getName).collect(Collectors.toSet()).toString());
|
||||
|
||||
}
|
||||
|
||||
|
|
@ -103,8 +195,6 @@ public class RunDemo {
|
|||
}
|
||||
|
||||
|
||||
|
||||
|
||||
static void printDebug1(String header, String message) {
|
||||
|
||||
cp.setForegroundColor(Ansi.FColor.BLACK);
|
||||
|
|
@ -118,7 +208,7 @@ public class RunDemo {
|
|||
cp.clear();
|
||||
}
|
||||
|
||||
static void printDebug2(String header, String message) {
|
||||
static void printDebug2(String header, String message) {
|
||||
|
||||
cp.setForegroundColor(Ansi.FColor.BLACK);
|
||||
cp.setBackgroundColor(Ansi.BColor.MAGENTA); //setting format
|
||||
|
|
@ -130,6 +220,7 @@ public class RunDemo {
|
|||
cp.println("");
|
||||
cp.clear();
|
||||
}
|
||||
|
||||
static void printFailure(String message) {
|
||||
|
||||
cp.setForegroundColor(Ansi.FColor.WHITE);
|
||||
|
|
|
|||
|
|
@ -1,7 +1,6 @@
|
|||
{:definitions
|
||||
{:name "demo 1"
|
||||
:background [
|
||||
(forall [?x ?room1 ?room2]
|
||||
:background [(forall [?x ?room1 ?room2]
|
||||
(if (not (= ?room1 ?room2))
|
||||
(if (in ?x ?room1) (not (in ?x ?room2))) ))
|
||||
(not (= room1 room2))
|
||||
|
|
@ -9,8 +8,8 @@
|
|||
(not (= self prisoner))
|
||||
(not (= self commander))
|
||||
(person prisoner)
|
||||
(person commander)
|
||||
]
|
||||
(person commander)]
|
||||
|
||||
:start [(in self room1)
|
||||
(in commander room2)
|
||||
(in prisoner room1)
|
||||
|
|
@ -67,20 +66,20 @@
|
|||
]
|
||||
}
|
||||
|
||||
:goals {G1 {:priority 6.0
|
||||
:goals {G1 {:priority 1.0
|
||||
:state [(not (open (door room1)))]}
|
||||
|
||||
G2 {:priority 6.0
|
||||
G2 {:priority 1.0
|
||||
:state [(in prisoner room1)]}
|
||||
|
||||
G3 {:priority 6.0
|
||||
G3 {:priority 1.0
|
||||
:state [(forall [?room]
|
||||
(if (in prisoner ?room)
|
||||
(in self ?room)))]}
|
||||
G4 {:priority 3.0
|
||||
:state [(in prisoner room2)
|
||||
G4 {:priority 1.0
|
||||
:state [(in prisoner room2)
|
||||
(in self room2)]}
|
||||
G5 {:priority 2.0
|
||||
G5 {:priority 1.0
|
||||
|
||||
:state [(interrogates commander prisoner)]}}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,71 +1,72 @@
|
|||
{:definitions
|
||||
{:name "test"
|
||||
:background []
|
||||
:start [
|
||||
(forall [?x ?room1 ?room2] (implies (and (not (= ?room1 ?room2)) (in ?x ?room1)) (not (in ?x ?room2))))
|
||||
(not (= room1 room2))
|
||||
(not (= prisoner commander))
|
||||
(not (= self prisoner))
|
||||
(not (= self commander))
|
||||
(person prisoner)
|
||||
(person commander)
|
||||
(in self room1)
|
||||
(in commander room2)
|
||||
(in prisoner room1)
|
||||
(open (door room2))
|
||||
(not (open (door room1)))
|
||||
{:name "test"
|
||||
:background []
|
||||
:start [(forall [?x ?room1 ?room2] (implies (and (not (= ?room1 ?room2)) (in ?x ?room1)) (not (in ?x ?room2))))
|
||||
(not (= room1 room2))
|
||||
(not (= prisoner commander))
|
||||
(not (= self prisoner))
|
||||
(not (= self commander))
|
||||
(person prisoner)
|
||||
(person commander)
|
||||
(in self room1)
|
||||
(in commander room2)
|
||||
(in prisoner room1)
|
||||
(open (door room2))
|
||||
(not (open (door room1)))
|
||||
|
||||
(forall [?x ?y ?room] (implies (and (and (in ?x ?room) (in ?y ?room)) (not (= ?x ?y))) (sameroom ?x ?y)))
|
||||
(forall [?x ?y] (implies (sameroom ?x ?y) (exists ?room (and (in ?x ?room) (in ?y ?room)))))
|
||||
]
|
||||
(forall [?x ?y ?room] (implies (and (and (in ?x ?room) (in ?y ?room)) (not (= ?x ?y))) (sameroom ?x ?y)))
|
||||
(forall [?x ?y] (implies (sameroom ?x ?y) (exists ?room (and (in ?x ?room) (in ?y ?room)))))
|
||||
]
|
||||
|
||||
:goal []
|
||||
:goal []
|
||||
|
||||
:actions
|
||||
[(define-action open-door [?room]
|
||||
:actions
|
||||
[(define-action open-door [?room]
|
||||
{:preconditions [(not (open (door ?room)))]
|
||||
:additions [(open (door ?room))]
|
||||
:deletions [(not (open (door ?room)))]})
|
||||
|
||||
|
||||
|
||||
(define-action accompany [?person ?room1 ?room2]
|
||||
{:preconditions [(in ?person ?room1)
|
||||
(in self ?room1)
|
||||
(open (door ?room1))
|
||||
(open (door ?room2))]
|
||||
|
||||
:additions [(in ?person ?room2)
|
||||
(in self ?room2)]
|
||||
|
||||
:deletions [(in ?person ?room1)
|
||||
(in self ?room1)]})
|
||||
|
||||
(define-action move [?person ?room2 ?room1]
|
||||
{:preconditions [(in ?person ?room2)
|
||||
(open (door ?room1))
|
||||
(open (door ?room2))]
|
||||
|
||||
:additions [(in ?person ?room1)]
|
||||
|
||||
:deletions [(in ?person ?room2)]})
|
||||
|
||||
(define-action get-interrogated [?room]
|
||||
{:preconditions [(in commander ?room)
|
||||
(in prisoner ?room)]
|
||||
|
||||
:additions [(interrogates commander prisoner)]
|
||||
|
||||
:deletions []})
|
||||
|
||||
(define-action open-door [?room ?actor]
|
||||
{:preconditions [(not (open (door ?room)))]
|
||||
:additions [(open (door ?room))]
|
||||
:deletions [(not (open (door ?room)))]})
|
||||
:additions [(open (door ?room))
|
||||
(did (open-door ?actor ?room))]
|
||||
:deletions [(not (open (door ?room)))]})]
|
||||
}
|
||||
|
||||
|
||||
|
||||
(define-action accompany [?person ?room1 ?room2]
|
||||
{:preconditions [(in ?person ?room1)
|
||||
(in self ?room1)
|
||||
(open (door ?room1))
|
||||
(open (door ?room2))]
|
||||
|
||||
:additions [(in ?person ?room2)
|
||||
(in self ?room2)]
|
||||
|
||||
:deletions [(in ?person ?room1)
|
||||
(in self ?room1)]})
|
||||
|
||||
(define-action move [?person ?room2 ?room1]
|
||||
{:preconditions [(in ?person ?room2)
|
||||
(open (door ?room1))
|
||||
(open (door ?room2))]
|
||||
|
||||
:additions [(in ?person ?room1)]
|
||||
|
||||
:deletions [(in ?person ?room2)]})
|
||||
|
||||
(define-action get-interrogated [?room]
|
||||
{:preconditions [(in commander ?room)
|
||||
(in prisoner ?room)]
|
||||
|
||||
:additions [(interrogates commander prisoner)]
|
||||
|
||||
:deletions []})
|
||||
|
||||
|
||||
]
|
||||
}
|
||||
|
||||
:goals {G1 {:priority 1.0
|
||||
:state [(sameroom self prisoner)]}
|
||||
|
||||
G2 {:priority 2.0
|
||||
:state [(in prisoner room2)]}
|
||||
}
|
||||
:goals {
|
||||
G2 {:priority 2.0
|
||||
:state [(sameroom prisoner room2)]}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
105
src/main/resources/edu/rpi/rair/goal_management_3.clj
Normal file
105
src/main/resources/edu/rpi/rair/goal_management_3.clj
Normal file
|
|
@ -0,0 +1,105 @@
|
|||
{:definitions
|
||||
{:name "demo 1"
|
||||
:background []
|
||||
:start [
|
||||
|
||||
(forall (?room ?x ?y) (implies (and (in ?x ?room) (and (in ?y ?room) (not (= ?x ?y)))) (sameroom ?x ?y)))
|
||||
(not (= prisoner commander))
|
||||
(not (= self prisoner))
|
||||
(in prisoner room1)
|
||||
(person prisoner)
|
||||
(not (= room1 room2))
|
||||
(in self room1)
|
||||
(in commander room2)
|
||||
(commander commander)
|
||||
(forall (?room2 ?x ?room1) (implies (and (not (= ?room1 ?room2)) (in ?x ?room1)) (not (in ?x ?room2))))
|
||||
(person commander)
|
||||
(robot self)
|
||||
(not (= self commander))
|
||||
(not (open (door room1)))
|
||||
(open (door room2))
|
||||
(forall (?room ?x ?y) (implies (and (sameroom ?x ?y) (in ?x ?room)) (in ?y ?room)))
|
||||
|
||||
]
|
||||
|
||||
:goal []
|
||||
|
||||
:actions
|
||||
[
|
||||
|
||||
(define-action move [?actor ?person ?room2 ?room1]
|
||||
{:preconditions [(robot ?actor)
|
||||
(person ?person)
|
||||
(not (= ?room1 ?room2))
|
||||
(open (door ?room1))
|
||||
(in ?person ?room2)
|
||||
(open (door ?room2))]
|
||||
:additions [(in ?person ?room1)]
|
||||
:deletions [(in ?person ?room1)]
|
||||
})
|
||||
(define-action keepDoorClosed [?actor ?room]
|
||||
{:preconditions [(robot ?actor)
|
||||
(not (open (door ?room)))]
|
||||
:additions []
|
||||
:deletions [(open (door ?room))]
|
||||
})
|
||||
(define-action accompany [?actor ?person ?room1 ?room2]
|
||||
{:preconditions [(robot ?actor)
|
||||
(person ?person)
|
||||
(not (= ?room1 ?room2))
|
||||
(open (door ?room1))
|
||||
(in ?person ?room1)
|
||||
(open (door ?room2))
|
||||
(not (= ?person ?actor))
|
||||
(in ?actor ?room1)]
|
||||
:additions [(in ?actor ?room2)
|
||||
(in ?person ?room2)]
|
||||
:deletions [(in ?person ?room1)
|
||||
(in ?actor ?room1)]
|
||||
})
|
||||
(define-action openDoor [?actor ?room]
|
||||
{:preconditions [(robot ?actor)
|
||||
(not (open (door ?room)))]
|
||||
:additions [(open (door ?room))]
|
||||
:deletions [(not (open (door ?room)))]
|
||||
})
|
||||
(define-action stayInRoom [?actor ?room]
|
||||
{:preconditions [(in ?actor ?room)]
|
||||
:additions [(in ?actor ?room)]
|
||||
:deletions []
|
||||
})
|
||||
(define-action interrogate [?actor ?person]
|
||||
{:preconditions [(person ?person)
|
||||
(commander ?actor)
|
||||
(in ?actor ?room)
|
||||
(in ?person ?room)]
|
||||
:additions [(interrogates ?actor ?person)]
|
||||
:deletions []
|
||||
})
|
||||
(define-action staySameRoom [?actor ?person]
|
||||
{:preconditions [(robot ?actor)
|
||||
(sameroom ?actor ?person)
|
||||
(person ?person)
|
||||
(in ?actor ?room)
|
||||
(in ?person ?room)]
|
||||
:additions [(sameroom ?actor ?person)]
|
||||
:deletions []
|
||||
})
|
||||
|
||||
]
|
||||
}
|
||||
|
||||
:goals {G1 {:priority 1.0
|
||||
:state [(not (open (door room1)))]}
|
||||
|
||||
G2 {:priority 1.0
|
||||
:state [(in prisoner room1)]}
|
||||
|
||||
G3 {:priority 1.0
|
||||
:state [(sameroom self prisoner)]}
|
||||
|
||||
G4 {:priority 3.0
|
||||
:state [(in prisoner room2)]}
|
||||
}
|
||||
|
||||
}
|
||||
Loading…
Reference in a new issue