anchor.diff:                                   (fa-start fa))))
             ;;(format t "states: ~A~&~&start: ~A~&accept: ~A~&" states-i start-i accept-i)
           (make-pda edges start-i accept-i)))))
  +
  +
  +
  +
  +
  +;; A. Finkel, B. Willems, and P. Wolper. A direct symbolic approach to model
  +;; checking pushdown systems. Electronic Notes in Theoretical Computer Science, 9,
  +;; 1997.
  +
  +
  +(defun pda-reachability-automaton (pda)
  +  (let ((epsilon-hash (make-hash-table :test #'equal))
  +        (edges)) ;; TODO: could do better than a dumb list
  +    ;; init epsilon hash
  +    (let ((empty-set (make-finite-set :compare #'gsymbol-compare)))
  +      (do-finite-set (q (pda-states pda))
  +        (setf (gethash q epsilon-hash) (finite-set-add empty-set q))))
  +    (labels ((epsilon-closure (q)
  +               (gethash q epsilon-hash))
  +             (new-edge (q0 g q1)
  +               ;; update epsilon closure
  +               (when (eq :epsilon g)
  +                 (setf (gethash q0 epsilon-hash)
  +                       (finite-set-union (epsilon-closure q0)
  +                                         (epsilon-closure q1))))
  +               ;; add edge
  +               ;(print (list q0 g q1))
  +               (let ((e (list q0 g q1)))
  +                 ;(print (not (finite-set-inp e edges)))
  +                 (prog1 (not (finite-set-inp e edges))
  +                   (setq edges (finite-set-add edges e)))))
  +             )
  +      ;; add initial transitions
  +      (pda-destructure-transitions ((q0 z g0) (q1 g1)) pda
  +        (declare (ignore z))
  +        (destructuring-bind (g1) g1
  +          (when (epsilon-p g0) ;; pop nothing
  +          ;  (print (list :push q0 g1 q1))
  +            (new-edge q0 g1 q1))))
  +      ;; saturate
  +      (do ((modified t))
  +          ((not modified))
  +        ;(print 'loop)
  +        (setq modified nil)
  +        (pda-destructure-transitions ((q z g0) (qp g1)) pda
  +          (declare (ignore z))
  +          (unless (epsilon-p g0)  ;; pop g0
  +            (assert (epsilon-p g1))
  +            (loop for (eqpp eg eq) in edges
  +               when (and (equal g0 eg) ;; push g0
  +                         (finite-set-inp q (epsilon-closure eq))) ;; eq -> q on :epsilon (get from pushed to popped)
  +               do
  +                 ;(print (list :pop eg g0 q0 eq1))
  +                 (setq modified (or modified (new-edge eqpp :epsilon qp))))))
  +        ;(print `(modified ,modified))
  +        ))
  +    ;; make FA
  +    (%make-fa :states (pda-states pda)
  +              :edges edges
  +              :terminals (pda-stack-alphabet pda)
  +              :start (pda-start pda)
  +              :accept (pda-accept pda))))
  +
  +
  +
  +
  +
  +;;
  +
  +;; (defun pda-accepting-p (pda)
  +;;   "Test if PDA is empty."
  +;;   (let ((hash (make-hash-table :test #'equal))
  +;;         (empty-fa (make-epsilon-fa (pda-stack-alphabet pda)))
  +;;         (accept (pda-accept pda))
  +;;         (succ (pda-index-successor-state-stack pda))) ;; state => stack langauge FA
  +;;     (labels ((state-fa (q) (gethash q hash empty-fa))
  +;;              (visit (q)
  +;;                (print q)
  +;;                (print (state-fa q))
  +;;                (if (finite-set-inp q accept)
  +;;                    (return-from pda-accepting-p q)
  +;;                    (let* ((old-fa (state-fa q))
  +;;                           (stack-top (fa-initial-terminals old-fa)))
  +;;                      (do-finite-set (g (finite-set-add stack-top :epsilon))
  +;;                        (let ((pop-fa (if (eq :epsilon g) old-fa
  +;;                                          (fa-canonicalize (fa-pop-initial old-fa g)))))
  +;;                          (print (list 'pop pop-fa))
  +;;                          (do-finite-set (y (funcall succ q g))
  +;;                            (destructuring-bind  (q1 &rest g1) y
  +;;                              (let* ((succ-fa (state-fa q1))
  +;;                                     (new-fa (fa-canonicalize (fa-concatenate (regex->dfa `(:concatenation ,@g1))
  +;;                                                                              pop-fa))))
  +;;                                (print (list 'new-fa y pop-fa))
  +;;                                (unless (dfa-eq new-fa succ-fa)
  +;;                                  (setf (gethash q1 hash)
  +;;                                        (fa-canonicalize (fa-union new-fa succ-fa)))
  +;;                                  (visit q1)))))))))
  +;;                nil))
  +;;       (visit (pda-start pda)))))
  
positive.code:                :transition tree-map
                 :start start
                 :accept accept)))
  
  (defun pda-dot (pda &key output (font-size 12))
    (let ((state-numbers (finite-set-enumerate (pda-states pda))))
  
negative.code:                 (lambda (x yy)
                    (finite-set-map nil (lambda (y) (funcall function x y)) yy))
                  (pda-transition pda)))
  
  (defmacro pda-destructure-transitions (((q0 z g0) (q1 g1)) pda &body body)
    (alexandria:with-gensyms (x y yy)
      `(map-tree-map :inorder nil
                     (lambda (,x ,yy)
                       (do-finite-set (,y ,yy)
                         (destructuring-bind ((,q0 ,z ,g0) (,q1 &rest ,g1)) (list ,x ,y)
                           ,@body)))
                     (pda-transition ,pda))))
  
  (defun pda-index-successor-state-stack (pda)
    (let ((hash (make-hash-table :test #'equal)))
      (pda-map-transtions nil (lambda (x y)
                                (destructuring-bind (q0 z g0) x
                                  (declare (ignore z))
                                  (let ((key (list q0 g0)))
                                    (setf (gethash key hash)
                                          (finite-set-union (gethash key hash nil)
                                                            (finite-set y))))))
                          pda)
      (lambda (q g) (let ((key (list q g)))
                 (declare (dynamic-extent key))
                 (gethash key hash)))))
  
  (defun make-pda (edges start accept)
    (let ((tree-map (make-tree-map #'gsymbol-compare))
  