The Spectra Automated Planner for DCEC built on ShadowProver
Find a file
2024-03-29 16:53:29 -04:00
.github/workflows Checkout submodule 2023-03-30 16:01:12 -04:00
.idea Fixes 2018-03-15 00:25:49 -07:00
snark@1b657eadf4 Moved snark to submodule 2023-03-30 15:33:03 -04:00
src Epistemic problem 2024-03-29 16:53:29 -04:00
.gitignore TORA example 2018-06-18 18:29:40 -07:00
.gitmodules Moved snark to submodule 2023-03-30 15:33:03 -04:00
docker-compose.yml Added a docker image containg a Py4J server. 2021-01-04 17:46:04 -08:00
Dockerfile Moved snark to submodule 2023-03-30 15:33:03 -04:00
Example.ipynb Added a docker image containg a Py4J server. 2021-01-04 17:46:04 -08:00
interface.py Added a docker image containg a Py4J server. 2021-01-04 17:46:04 -08:00
pom.xml Renaming imports to support ShadowProver changes 2023-10-27 10:57:15 -04:00
README.md Added installation instructions 2023-10-27 11:03:45 -04:00
run_spectra.sh Renaming imports to support ShadowProver changes 2023-10-27 10:57:15 -04:00

Spectra

Spectra is a general purpose planning system. It extends STRIPS-style planning by allowing arbitray first-order formulae for state descriptions and background knowledge rather than just predicates. This allows, for instance, handling domains with infinite or unbounded objects elegantly (among other things).

Overview Presentation (pdf)

  • Drawbacks of propositional planning (current planning systems):
  • Expressivity: Cannot express arbitrary constraints. “At every step make sure that no two blocks on the table have same color”
    • Domain Size: Scaling to large domains of arbitrary sizes poses difficulty.

Installation

First, we need to make sure ShadowProver is installed.

git clone --recursive https://github.com/RAIRLab/ShadowProver.git
cd ShadowProver
mvn package
mvn install

Now, we can clone the Spectra repository.

git clone --recursive https://github.com/RAIRLab/Spectra.git

Similarly build and install the java project

cd Spectra
mvn package
mvn install

Now you should be able to run Spectra:

./run_spectra.sh [problem_file_path]

Spectra's Architecture

spectra-arch.png

Example Input File

examples.png

Scaling Up

Two approaches:

  1. Procedural Attachments: Special purpose procedural code that can bypass strict formal reasoning.

  2. μ-methods: Written in denotational proof language. Preserves soundness by letting us write down commonly used patterns of reasoning (a bit unwieldy integration now than the first approach)

;; (removeFrom  ?x ?y) => "Remove ?x from ?y"
;; (placeInside  ?x ?y) ==> "Place ?x inside ?y"
(define-method planMethod [?b ?c ?d]
  {:goal [(In ?b ?c) (In ?c ?d)]
   :while [(In ?b ?d) (Empty ?c)
           (< (size ?c) (size ?d))
           (< (size ?b) (size ?c))]
   :actions [(removeFrom  ?b ?d) (placeInside  ?b ?c) (placeInside  ?c ?d)]})

Roughly, a method has conditions that the goal and background + start state should satisfy. If the conditions are satisfied, a plan template is generated (note the variables). The planner then verifies if the plan template works, if so it outputs the plan.

Spectra on a Seriated Cup Challenge

download-3.gif