diff --git a/src/main/java/edu/rpi/rair/DepthFirstPlanner.java b/src/main/java/edu/rpi/rair/DepthFirstPlanner.java index f30b4f6..590a642 100644 --- a/src/main/java/edu/rpi/rair/DepthFirstPlanner.java +++ b/src/main/java/edu/rpi/rair/DepthFirstPlanner.java @@ -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> plan(Set background, Set 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> plans = planInternal(Sets.newSet(), 0, i, background, actions, start, goal); + + if (plans.isPresent()) { + return plans; + } + + } +// + return Optional.empty(); + + } } + private Optional> planInternal(Set> history, int currentDepth, int maxDepth, Set background, Set actions, State start, State goal) { - private Optional> planInternal(Set> history, int currentDepth, Set background, Set 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 stateActionPair : nextStateActionPairs.get()) { - - Optional> planOpt = planInternal(history, currentDepth+1, background, actions, stateActionPair.first(), goal); + Optional> planOpt = planInternal(history, currentDepth + 1, maxDepth, background, actions, stateActionPair.first(), goal); if (planOpt.isPresent()) { diff --git a/src/main/java/edu/rpi/rair/utils/RunDemo.java b/src/main/java/edu/rpi/rair/utils/RunDemo.java index eb4cced..488cdb8 100644 --- a/src/main/java/edu/rpi/rair/utils/RunDemo.java +++ b/src/main/java/edu/rpi/rair/utils/RunDemo.java @@ -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 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 goalTrackingProblemList = (GoalTrackingProblem.readFromFile(Planner.class.getResourceAsStream("goal_management_2.clj"))); + + System.out.println(); + + List 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 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 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); diff --git a/src/main/resources/edu/rpi/rair/goal_management_1.clj b/src/main/resources/edu/rpi/rair/goal_management_1.clj index d6a8f03..c0b7469 100644 --- a/src/main/resources/edu/rpi/rair/goal_management_1.clj +++ b/src/main/resources/edu/rpi/rair/goal_management_1.clj @@ -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)]}} diff --git a/src/main/resources/edu/rpi/rair/goal_management_2.clj b/src/main/resources/edu/rpi/rair/goal_management_2.clj index 5b68155..61e77fb 100644 --- a/src/main/resources/edu/rpi/rair/goal_management_2.clj +++ b/src/main/resources/edu/rpi/rair/goal_management_2.clj @@ -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)]} + } } diff --git a/src/main/resources/edu/rpi/rair/goal_management_3.clj b/src/main/resources/edu/rpi/rair/goal_management_3.clj new file mode 100644 index 0000000..9ce5db8 --- /dev/null +++ b/src/main/resources/edu/rpi/rair/goal_management_3.clj @@ -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)]} + } + + } \ No newline at end of file