<< Previous

Next >>

A2

Automaton A2 is the simplest automaton, with a single accepting state. Or, it should be, except that it is unrealizable as drawn. The intent of the automaton, as shown in the input examples, is that it accepts all single-character strings `1` and `0`. This requires a second state that transitions to the drawn state on all inputs. This error was not realized until this automaton was synthesized for the first time, illustrating the importance of providing input examples for a sanity check. However, our use of program synthesis lets us simply add an additional "extra" state to the program specification, which generates the intended automaton program.

Annotated Image

Program Specification

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

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

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

(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

;; Negative transitions
(assert (forall ((symb String))
    (=> (not (or false))
        (= 0 (T 1 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 "1"))
(assert (exec-dfa IS "0"))

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

Synthesized Program

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

<< Previous

Next >>