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

Hooked in changes from ShadowProver and introduced grapevine domain

Browse source
This commit is contained in:
Brandon Rozek 2023-11-03 16:13:05 -04:00
parent f6e1dc19eb
commit 48971ad770
No known key found for this signature in database
GPG key ID: 26E457DA82C9F480
3 changed files with 129 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -2,7 +2,7 @@ package org.rairlab.planner;
import org.rairlab.planner.utils.Visualizer;
import org.rairlab.shadow.prover.core.Prover;
import org.rairlab.shadow.prover.core.SnarkWrapper;
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;
@ -44,9 +44,7 @@ public class Operations {
applyCache.clear();
}
static {
prover = SnarkWrapper.getInstance();
prover = new CognitiveCalculusProver();
}
public static synchronized Optional<Justification> proveCached(Set<Formula> assumptions, Formula goal) {
@ -192,6 +190,7 @@ public class Operations {
// Apply binding to get grounded action and calculate the next state
// newState = (oldState - Deletions(a)) U Additions(a)
Action groundedAction = action.instantiate(binding);
State newState = State.initializeWith(Sets.union(
Sets.difference(state.getFormulae(), groundedAction.getDeletions()),
groundedAction.getAdditions()

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

@ -1,7 +1,5 @@
package org.rairlab.planner;
import org.rairlab.shadow.prover.core.Prover;
import org.rairlab.shadow.prover.core.SnarkWrapper;
import org.rairlab.shadow.prover.representations.formula.Formula;
import org.rairlab.shadow.prover.utils.CollectionUtils;
import org.rairlab.shadow.prover.utils.Reader;
@ -14,7 +12,6 @@ import java.util.Set;
public class State {
final Set<Formula> formulae;
private static final Prover prover = SnarkWrapper.getInstance();
static Formula FALSE;
static{

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

@ -0,0 +1,126 @@
{:name "GrapeVine"
:background [
(agent a)
(agent b)
(agent c)
(room p1)
(room p2)
(not (= a b))
(not (= a c))
(not (= b c))
]
:actions [
(define-action left [?a] {
:preconditions [
(agent ?a) ; Type restriction
(at ?a p2)
]
:additions [
(at ?a p1)
(not (at ?a p2))
]
:deletions [
(at ?a p2)
(not (at ?a p1))
]
})
(define-action right [?a] {
:preconditions [
(agent ?a) ; Type restriction
(at ?a p1)
]
:additions [
(at ?a p2)
(not (at ?a p1))
]
:deletions [
(at ?a p1)
(not (at ?a p2))
]
})
(define-action share-both [?a1 ?a2 ?a3 ?r] {
:preconditions [
; Type restrictions
(agent ?a1)
(agent ?a2)
(agent ?a3)
(room ?r)
; Precondition
(at ?a1 ?r)
(at ?a2 ?r)
(at ?a3 ?r)
(not (= ?a1 ?a2))
(not (= ?a1 ?a3))
(not (= ?a2 ?a3))
]
:additions [
(Believes! ?a2 (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)))
]
})
(define-action share-single [?a1 ?a2 ?a3 ?r] {
:preconditions [
; Type restrictions
(agent ?a1)
(agent ?a2)
(agent ?a3)
(room ?r)
; Precondition
(at ?a1 ?r)
(at ?a2 ?r)
(not (at ?a3 ?r))
(not (= ?a1 ?a2))
(not (= ?a1 ?a3))
(not (= ?a2 ?a3))
]
:additions [
(Believes! ?a2 (the ?a1))
(Believes! ?a1 (Believes! ?a2 (the ?a1)))
]
:deletions [
(not (Believes! ?a2 (the ?a1)))
]
})
]
:start [
; Locations
(at a p1)
(not (at a p2))
(at b p1)
(not (at b p2))
(at c p1)
(not (at c p2))
; Each agent has a secret
(Believes! a (the a))
(Believes! b (the b))
(Believes! c (the c))
; No one believes a's secret
(not (Believes! b (the a)))
(not (Believes! c (the a)))
]
:goal [
(Believes! b (the a))
(Believes! a (Believes! b (the a)))
(not (Believes! c (the a)))
]
}