		Search-engine friendly clone of the ACL2 documentation.

Make-fsm

Basic constructor macro for fsm structures.

Syntax

(make-fsm [:values <values>] 
          [:nextstate <nextstate>])

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-fsm

(defmacro make-fsm (&rest args)
  (std::make-aggregate 'fsm
                       args '((:values) (:nextstate))
                       'make-fsm
                       nil))

Function: fsm

(defun fsm (values nextstate)
  (declare (xargs :guard (and (svex-alist-p values)
                              (svex-alist-p nextstate))))
  (declare (xargs :guard t))
  (let ((__function__ 'fsm))
    (declare (ignorable __function__))
    (b* ((values (mbe :logic (svex-alist-fix values)
                      :exec values))
         (nextstate (mbe :logic (svex-alist-fix nextstate)
                         :exec nextstate)))
      (list (cons 'values values)
            (cons 'nextstate nextstate)))))