anchor.diff:    (nth w (get-valuation m)))
   
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  -; FORMULAS
  +; SYNTAX
   ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
   
   ; following are somewhat based on Manolios's formulation of formulas for the
  
positive.code: ; SEMANTICS
  ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
  
  ;we assume m, w, f are wellformed.
  (defun pdl-satisfies-symbol (m w f)
    (cond ((equal f 'true) t)
  
negative.code:                t
               nil))))
  
  ; Pointwise modal valuation. (pdl-satisfies M w phi) iff $M, w \models phi$.
  ; That is, if pdl formula f is satisfied at world w of model m, then this will
  ; return t, otherwise it will return nil.
  ;
  ; For now, we return nil if m, w, or f aren't valid. We may have to reassess
  ; this.
  (mutual-recursion
   (defun pdl-satisfies (m w f)
     (if (and (modelp m)
              (world-valid-in-model m w)
              (pdl-formulap f
                            (get-prop-atoms m)
                            (get-prog-atoms m)))
         (cond ((symbolp f)
                (pdl-satisfies-symbol m w f))
               ((equal (len f) 2)
                (not (pdl-satisfies m w (second f))))
               ((equal (len f) 3)
                (cond ((equal (first f) 'v)
                       (or (pdl-satisfies m w (second f))
                           (pdl-satisfies m w (third f))))
                      ((equal (first f) 'diamond)
                       (pdl-satisfies-diamond
                        m w (prog-accessible-worlds m w (second f)) (third f)))))
               (t nil))
       nil))
   (defun pdl-satisfies-diamond (m w p-accessible-worlds f)
     (if (consp p-accessible-worlds)
         (if (pdl-satisfies m (car p-accessible-worlds) f)
             t
           (pdl-satisfies-diamond m w (cdr p-accessible-worlds) f))
       nil)))
  
  
  
  