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

Cleanup and updates

Browse source 
- Runner jar
- Optimizations for when calling out to ShadowProver
- Fixed bug in precondition code
- Fixed grapevine domain
This commit is contained in:
Brandon Rozek 2024-03-29 17:40:48 -04:00 committed by GitHub
commit f36a886631
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 93 additions and 44 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
pom.xml
View file

@ -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>

9
src/main/java/org/rairlab/planner/Action.java
View file

@ -49,7 +49,14 @@ public class Action {
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() +

87
src/main/java/org/rairlab/planner/Operations.java
View file

@ -4,11 +4,12 @@ import org.rairlab.planner.utils.Visualizer;
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;
@ -16,11 +17,14 @@ 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.
@ -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;
@ -48,40 +53,44 @@ public class Operations {
}
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;
}
@ -155,10 +164,9 @@ public class Operations {
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()){
@ -169,7 +177,14 @@ public class Operations {
// 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()) {
@ -191,9 +206,12 @@ public class Operations {
// 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
@ -203,6 +221,7 @@ public class Operations {
}
applyCache.put(Triple.of(background, action, state), Optional.of(nextStates));
return Optional.of(nextStates);
}

3
src/main/java/org/rairlab/planner/State.java
View file

@ -12,14 +12,17 @@ import java.util.Set;
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;
}

15
src/main/java/org/rairlab/planner/search/AStarPlanner.java
View file

@ -6,6 +6,7 @@ import org.rairlab.planner.State;
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;
@ -67,6 +68,10 @@ public class AStarPlanner {
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>();
@ -81,7 +86,11 @@ public class AStarPlanner {
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();
@ -105,6 +114,8 @@ public class AStarPlanner {
// 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
@ -137,6 +148,10 @@ public class AStarPlanner {
int heuristicValue = heuristic.apply(nextState);
comparator.setValue(futureSearch, planCost + heuristicValue);
search.add(futureSearch);
// For debugging...
// seq.put(nextState, next_actions);
}
}
}

5
src/main/java/org/rairlab/planner/utils/Runner.java
View file

@ -46,10 +46,11 @@ public final class Runner {
}
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(),
@ -57,9 +58,11 @@ public final class Runner {
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");

12
src/main/resources/org/rairlab/planner/problems/epistemic/grapevine.clj
View file

@ -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] {
@ -96,6 +97,7 @@
(not (Believes! ?a2 (the ?a1)))
(not (Believes! ?a1 (Believes! ?a2 (the ?a1))))
]
:cost 2
})
]