		Search-engine friendly clone of the ACL2 documentation.

Process.lisp

Defsvtv-fn

Signature
(defsvtv-fn name ins overrides outs internals design design-const labels simplify pre-simplify state-machine initial-state-vars keep-final-state keep-all-states define-macros define-mod parents short long form) → *
Arguments: name — Guard (symbolp name).; ins — Guard (true-list-listp ins).; overrides — Guard (true-list-listp overrides).; outs — Guard (true-list-listp outs).; internals — Guard (true-list-listp internals).; design — Guard (design-p design).; design-const — Guard (symbolp design-const).; labels — Guard (symbol-listp labels).

Definitions and Theorems

Function: defsvtv-fn

(defun defsvtv-fn (name ins overrides outs
                        internals design design-const labels
                        simplify pre-simplify state-machine
                        initial-state-vars keep-final-state
                        keep-all-states define-macros
                        define-mod parents short long form)
  (declare (xargs :guard (and (symbolp name)
                              (true-list-listp ins)
                              (true-list-listp overrides)
                              (true-list-listp outs)
                              (true-list-listp internals)
                              (design-p design)
                              (symbolp design-const)
                              (symbol-listp labels))))
  (declare
       (xargs :guard (modalist-addr-p (design->modalist design))))
  (let ((__function__ 'defsvtv-fn))
    (declare (ignorable __function__))
    (b* ((svtv (defsvtv-main name ins overrides outs internals
                             design labels simplify pre-simplify
                             (or state-machine initial-state-vars)
                             (or state-machine keep-final-state)
                             keep-all-states form))
         ((unless svtv)
          (raise "failed to generate svtv")))
      (defsvtv-events svtv design-const define-macros
                      define-mod parents short long))))