Next >>

A1

Automaton A1 is the prototypical automaton, drawn as a part of the project proposal. Implementation details were not considered; rather, the implementation evolved to recognize the features present in this image.

Annotated Image

Program Specification

;;;
;;; Preamble
;;;
(set-logic ALL)

;;;
;;; State Definitions
;;;
(define-fun is-state ((q Int)) Bool
    (and (< (- 1) q) (< q 4)))

(define-fun is-accepting ((q Int)) Bool
    (or (= q 3)))

(declare-fun IS () Int)
(assert (is-state IS))
(assert (not (= 0 IS)))

;;;
;;; Transition Definitions
;;;
(declare-fun T (Int String) Int)

;; All transitions must go to a valid state
(assert (forall ((q Int) (symb String))
    (=> (is-state q) (is-state (T q symb)))))

;; It must not be possible to leave the zero state
(assert (forall ((symb String)) (= 0 (T 0 symb))))

;; Defined transitions
(assert (= 2 (T 1 "A")))
(assert (= 2 (T 2 "B")))
(assert (= 3 (T 2 "A")))

;; Negative transitions
(assert (forall ((symb String))
    (=> (not (or (= symb "A")))
        (= 0 (T 1 symb)))))
(assert (forall ((symb String))
    (=> (not (or (= symb "B") (= symb "A")))
        (= 0 (T 2 symb)))))
(assert (forall ((symb String))
    (=> (not (or false))
        (= 0 (T 3 symb)))))
;;;
;;; Examples
;;;
(define-fun-rec exec-dfa ((q Int) (input String)) Bool
    (ite (= 0 (str.len input))
         (is-accepting q)
         (exec-dfa (T q (str.at input 0)) (str.substr input 1 (- (str.len input) 1)))))

;; Positive
(assert (exec-dfa IS "ABBBA"))

;; Negative
(assert (not (exec-dfa IS "ABBB")))
;;;
;;; Postamble
;;;
(check-sat)
(get-model)

Synthesized Program

sat
(
  (define-fun IS () Int
    1)
  (define-fun T ((x!0 Int) (x!1 String)) Int
    (let ((a!1 (or (and (<= 1 x!0) (not (<= 2 x!0)) (= x!1 "B"))
                   (and (not (<= 1 x!0)) (not (= x!1 "A")) (not (= x!1 "B")))
                   (and (not (<= 1 x!0)) (= x!1 "B"))
                   (and (<= 1 x!0)
                        (<= 2 x!0)
                        (<= 3 x!0)
                        (not (= x!1 "A"))
                        (not (= x!1 "B")))
                   (and (<= 1 x!0)
                        (not (<= 2 x!0))
                        (not (= x!1 "A"))
                        (not (= x!1 "B")))
                   (and (<= 1 x!0)
                        (<= 2 x!0)
                        (<= 3 x!0)
                        (= x!1 "A")
                        (not (= x!1 "B")))
                   (and (<= 1 x!0)
                        (<= 2 x!0)
                        (not (<= 3 x!0))
                        (not (= x!1 "A"))
                        (not (= x!1 "B")))
                   (and (not (<= 1 x!0)) (= x!1 "A") (not (= x!1 "B")))
                   (and (<= 1 x!0) (<= 2 x!0) (<= 3 x!0) (= x!1 "B"))))
          (a!2 (or (and (<= 1 x!0) (<= 2 x!0) (not (<= 3 x!0)) (= x!1 "B"))
                   (and (<= 1 x!0)
                        (not (<= 2 x!0))
                        (= x!1 "A")
                        (not (= x!1 "B"))))))
    (let ((a!3 (ite (and (<= 1 x!0)
                         (<= 2 x!0)
                         (not (<= 3 x!0))
                         (= x!1 "A")
                         (not (= x!1 "B")))
                    3
                    (ite a!2 2 7))))
      (ite a!1 0 a!3))))
)

Next >>