Skip to content

Commit

Permalink
Cleanup and updates
Browse files Browse the repository at this point in the history 
- Runner jar
- Optimizations for when calling out to ShadowProver
- Fixed bug in precondition code
- Fixed grapevine domain
  • Loading branch information
@Brandon-Rozek
Brandon-Rozek authored Mar 29, 2024
2 parents 492e7ba + aec7d98 commit f36a886
Show file tree
Hide file tree
Showing 7 changed files with 93 additions and 44 deletions.
6 changes: 3 additions & 3 deletions pom.xml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,17 +16,17 @@
<version>2.4</version>
<executions>
<execution>
<id>sandbox</id>
<id>runner</id>
<configuration>
<archive>
<manifest>
<mainClass>org.rairlab.planner.Py4JServer</mainClass>
<mainClass>org.rairlab.planner.utils.Runner</mainClass>
</manifest>
</archive>
<descriptorRefs>
<descriptorRef>jar-with-dependencies</descriptorRef>
</descriptorRefs>
<finalName>sandbox</finalName>
<finalName>runner</finalName>
</configuration>
<phase>package</phase>
<goals>
Expand Down
9 changes: 8 additions & 1 deletion src/main/java/org/rairlab/planner/Action.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,7 +49,14 @@ public Action(String name, Set<Formula> preconditions, Set<Formula> additions, S

this.freeVariables = freeVariables;

this.precondition = new And(preconditions.stream().collect(Collectors.toList()));
if (preconditions.size() > 1) {
this.precondition = new And(preconditions.stream().collect(Collectors.toList()));
} else if (preconditions.size() == 1) {
this.precondition = preconditions.iterator().next();
} else {
this.precondition = State.TRUE;
}


this.weight = preconditions.stream().mapToInt(Formula::getWeight).sum() +
additions.stream().mapToInt(Formula::getWeight).sum() +
Expand Down
87 changes: 53 additions & 34 deletions src/main/java/org/rairlab/planner/Operations.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,23 +4,27 @@
import org.rairlab.shadow.prover.core.Prover;
import org.rairlab.shadow.prover.core.ccprovers.CognitiveCalculusProver;
import org.rairlab.shadow.prover.core.proof.Justification;
import org.rairlab.shadow.prover.representations.formula.BiConditional;
import org.rairlab.shadow.prover.representations.formula.Formula;

import org.rairlab.shadow.prover.representations.value.Value;
import org.rairlab.shadow.prover.representations.value.Variable;
import org.rairlab.shadow.prover.representations.formula.*;
import org.rairlab.shadow.prover.representations.value.Constant;


import org.rairlab.shadow.prover.utils.CollectionUtils;

import org.rairlab.shadow.prover.utils.Sets;
import org.apache.commons.lang3.tuple.Pair;
import org.apache.commons.lang3.tuple.ImmutablePair;
import org.apache.commons.lang3.tuple.Triple;

import java.util.ArrayList;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
import java.util.Optional;
import java.util.Set;
import java.util.concurrent.*;
import java.util.stream.Collectors;

/**
* Created by naveensundarg on 1/13/17.
Expand All @@ -29,6 +33,7 @@ public class Operations {

private static boolean DEEP_EQUIVALENCE = false;
private static boolean THROW_AWAY_EMPTY_BINDINGS = true;
private static boolean MONOTONIC = true;
private static Prover prover;


Expand All @@ -48,40 +53,44 @@ public static void reset(){
}

public static synchronized Optional<Justification> proveCached(Set<Formula> assumptions, Formula goal) {

// (1) If we've asked to prove this exact goal from assumptions before
// then return the previous result
Pair<Set<Formula>, Formula> inputPair = ImmutablePair.of(assumptions, goal);
if (proverCache.containsKey(inputPair)) {
return proverCache.get(inputPair);
}

// Iterate through the cache
for (Map.Entry<Pair<Set<Formula>, Formula>, Optional<Justification>> entry : proverCache.entrySet()) {
Set<Formula> cachedAssumptions = entry.getKey().getLeft();
Formula cachedGoal = entry.getKey().getRight();
Optional<Justification> optJust = entry.getValue();

// (2) Return the cached justification if:
// - Goals are the same
// - The cached assumptions are a subset of the current ones
// - A justification was found
if (optJust.isPresent() && cachedGoal.equals(goal) && Sets.subset(cachedAssumptions, assumptions)) {
return optJust;
if (MONOTONIC) {
// (1) If we've asked to prove this exact goal from assumptions before
// then return the previous result
if (proverCache.containsKey(inputPair)) {
return proverCache.get(inputPair);
}

// (3) Return cached failure if:
// - Goals are the same
// - Assumptions are a subset of cached assumptions
// - No justification was found
if (optJust.isEmpty() && cachedGoal.equals(goal) && Sets.subset(assumptions, cachedAssumptions)) {
return optJust;
// Iterate through the cache
for (Map.Entry<Pair<Set<Formula>, Formula>, Optional<Justification>> entry : proverCache.entrySet()) {
Set<Formula> cachedAssumptions = entry.getKey().getLeft();
Formula cachedGoal = entry.getKey().getRight();
Optional<Justification> optJust = entry.getValue();

// (2) Return the cached justification if:
// - Goals are the same
// - The cached assumptions are a subset of the current ones
// - A justification was found
if (optJust.isPresent() && cachedGoal.equals(goal) && Sets.subset(cachedAssumptions, assumptions)) {
return optJust;
}

// (3) Return cached failure if:
// - Goals are the same
// - Assumptions are a subset of cached assumptions
// - No justification was found
if (optJust.isEmpty() && cachedGoal.equals(goal) && Sets.subset(assumptions, cachedAssumptions)) {
return optJust;
}
}
}
}

// Otherwise create a new call to the theorem prover
Optional<Justification> answer = prover.prove(assumptions, goal);
proverCache.put(inputPair, answer);
if (MONOTONIC) {
proverCache.put(inputPair, answer);
}
return answer;

}
Expand Down Expand Up @@ -155,10 +164,9 @@ public static synchronized Optional<Set<Map<Variable, Value>>> proveAndGetMultip
return Optional.of(ans.get().getRight());
}


public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background, Action action, State state) {

// Get resulting states from cache if computed before
// // Get resulting states from cache if computed before
if(applyCache.containsKey(Triple.of(background, action, state))){
Optional<Set<Pair<State, Action>>> ans = applyCache.get(Triple.of(background, action, state));
if(ans.isPresent()){
Expand All @@ -169,7 +177,14 @@ public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background,

// Ask theorem prover for witnesses that satisfy the precondition
Set<Formula> givens = Sets.union(background, state.getFormulae());
Optional<Set<Map<Variable, Value>>> bindingsOpt = proveAndGetBindingsCached(givens, action.getPrecondition(), action.openVars());

Formula precondition = action.getPrecondition();

List<Variable> openVars = action.openVars()
.stream()
.collect(Collectors.toList());

Optional<Set<Map<Variable, Value>>> bindingsOpt = proveAndGetBindingsCached(givens, precondition, openVars);

// If not witnesses found, return nothing
if (!bindingsOpt.isPresent()) {
Expand All @@ -191,9 +206,12 @@ public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background,
// newState = (oldState - Deletions(a)) U Additions(a)
Action groundedAction = action.instantiate(binding);

Set<Formula> additions = groundedAction.getAdditions();
Set<Formula> deletions = groundedAction.getDeletions();

State newState = State.initializeWith(Sets.union(
Sets.difference(state.getFormulae(), groundedAction.getDeletions()),
groundedAction.getAdditions()
Sets.difference(state.getFormulae(), deletions),
additions
));

// If the state progresses, record it as a possible next state
Expand All @@ -203,6 +221,7 @@ public static Optional<Set<Pair<State, Action>>> apply(Set<Formula> background,
}

applyCache.put(Triple.of(background, action, state), Optional.of(nextStates));

return Optional.of(nextStates);

}
Expand Down
3 changes: 3 additions & 0 deletions src/main/java/org/rairlab/planner/State.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,14 +12,17 @@
public class State {

final Set<Formula> formulae;
static Formula TRUE;
static Formula FALSE;

static{

try {
TRUE = Reader.readFormulaFromString("(or P (not P))");
FALSE = Reader.readFormulaFromString("(and P (not P))");
} catch (Reader.ParsingException e) {
e.printStackTrace();
TRUE = null;
FALSE = null;
}

Expand Down
15 changes: 15 additions & 0 deletions src/main/java/org/rairlab/planner/search/AStarPlanner.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,6 +6,7 @@
import org.rairlab.planner.Action;
import org.rairlab.planner.Plan;
import org.rairlab.planner.Operations;
import org.rairlab.shadow.prover.representations.value.Value;

import java.util.*;
import java.util.function.Function;
Expand Down Expand Up @@ -67,6 +68,10 @@ public Set<Plan> plan(Set<Formula> background, Set<Action> actions, State start,
comparator.setValue(searchStart, 0);
search.add(searchStart);

// For debugging...
// Map<State, List<Action>> seq = new HashMap<State, List<Action>>();
// seq.put(start, new ArrayList<Action>());

// Current set of plans
Set<Plan> plansFound = new HashSet<Plan>();

Expand All @@ -81,7 +86,11 @@ public Set<Plan> plan(Set<Formula> background, Set<Action> actions, State start,
State lastState = currentSearch.getLeft();
List<Action> previous_actions = currentSearch.getRight();

// System.out.println("--------------------");
// System.out.println("Considering state with heuristic: " + comparator.getValue(currentSearch));
// System.out.println("Current Plan: " + seq.get(lastState).toString());
// System.out.println("Current State: " + lastState.toString());
// System.out.println("--------------------");

// Exit loop if we've passed the depth limit
int currentDepth = previous_actions.size();
Expand All @@ -105,6 +114,8 @@ public Set<Plan> plan(Set<Formula> background, Set<Action> actions, State start,

// Apply the action to the state and add to the search space
for (Action action : nonTrivialActions) {
// System.out.println("Considering action: " + action.getName());

Optional<Set<Pair<State, Action>>> optNextStateActionPairs = Operations.apply(background, action, lastState);

// Ignore actions that aren't applicable
Expand Down Expand Up @@ -137,6 +148,10 @@ public Set<Plan> plan(Set<Formula> background, Set<Action> actions, State start,
int heuristicValue = heuristic.apply(nextState);
comparator.setValue(futureSearch, planCost + heuristicValue);
search.add(futureSearch);

// For debugging...
// seq.put(nextState, next_actions);

}
}
}
Expand Down
5 changes: 4 additions & 1 deletion src/main/java/org/rairlab/planner/utils/Runner.java
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,20 +46,23 @@ public static void main(String[] args) {
}

AStarPlanner astarplanner = new AStarPlanner();
astarplanner.setK(2);
astarplanner.setK(1);

for (PlanningProblem planningProblem : planningProblemList) {

long start = System.currentTimeMillis();
Set<Plan> plans = astarplanner.plan(
planningProblem.getBackground(),
planningProblem.getActions(),
planningProblem.getStart(),
planningProblem.getGoal(),
ConstantHeuristic::h
);
long end = System.currentTimeMillis();

if(plans.size() > 0) {
System.out.println(plans.toString());
System.out.println("Time (ms): " + (end - start));
}
else {
System.out.println("FAILED");
Expand Down
12 changes: 7 additions & 5 deletions src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj
View file
Original file line number Diff line number Diff line change
Expand Up @@ -61,16 +61,17 @@
]
:additions [
(Believes! ?a2 (the ?a1))
(Believes ?a3 (the ?a1))
(Believes ?a1 (Believes! ?a2 (the ?a1)))
(Believes ?a1 (Believes! ?a3 (the ?a1)))
(Believes! ?a3 (the ?a1))
(Believes! ?a1 (Believes! ?a2 (the ?a1)))
(Believes! ?a1 (Believes! ?a3 (the ?a1)))
]
:deletions [
(not (Believes! ?a2 (the ?a1)))
(not (Believes! ?a3 (the ?a1)))
(not (Believes ?a1 (Believes! ?a2 (the ?a1))))
(not (Believes ?a1 (Believes! ?a3 (the ?a1))))
(not (Believes! ?a1 (Believes! ?a2 (the ?a1))))
(not (Believes! ?a1 (Believes! ?a3 (the ?a1))))
]
:cost 2
})

(define-action share-single [?a1 ?a2 ?a3 ?r] {
Expand All @@ -96,6 +97,7 @@
(not (Believes! ?a2 (the ?a1)))
(not (Believes! ?a1 (Believes! ?a2 (the ?a1))))
]
:cost 2
})

]
Expand Down

0 comments on commit f36a886

Please sign in to comment.