mirror of
				https://github.com/RAIRLab/Spectra.git
				synced 2025-10-26 22:51:19 +00:00 
			
		
		
		
	
				
				The Spectra Automated Planner for DCEC built on ShadowProver
				
			
		| .idea | ||
| snark-20120808r02 | ||
| src | ||
| .gitignore | ||
| _config.yml | ||
| pom.xml | ||
| README.md | ||
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).
- Existing Planners are propositional
- Drawbacks:
- 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.
 
Architecture
Example
Scaling Up
Two approaches:
- 
Procedural Attachments: Special purpose procedural code that can bypass strict formal reasoning. 
- 
μ-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. 

