		Search-engine friendly clone of the ACL2 documentation.

Svtv-fsm

Make-svtv-fsm

Basic constructor macro for svtv-fsm structures.

Syntax

(make-svtv-fsm [:fsm <fsm>] 
               [:namemap <namemap>])

This is the usual way to construct svtv-fsm structures. It simply conses together a structure with the specified fields.

This macro generates a new svtv-fsm structure from scratch. See also change-svtv-fsm, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-svtv-fsm

(defmacro make-svtv-fsm (&rest args)
  (std::make-aggregate 'svtv-fsm
                       args '((:fsm) (:namemap))
                       'make-svtv-fsm
                       nil))

Function: svtv-fsm

(defun svtv-fsm (fsm namemap)
  (declare (xargs :guard (and (fsm-p fsm)
                              (svtv-name-lhs-map-p namemap))))
  (declare (xargs :guard t))
  (let ((__function__ 'svtv-fsm))
    (declare (ignorable __function__))
    (b* ((fsm (mbe :logic (fsm-fix fsm) :exec fsm))
         (namemap (mbe :logic (svtv-name-lhs-map-fix namemap)
                       :exec namemap)))
      (list (cons 'fsm fsm)
            (cons 'namemap namemap)))))