		Search-engine friendly clone of the ACL2 documentation.

Stv-process

Stv-fully-general-st-alist

Create the sexpr-alist to use as the initial state for fully general simulations of a module.

Signature
(stv-fully-general-st-alist mod) → state-alist
Arguments: mod — The esim module.
Returns: state-alist — Alist binding every state bit |foo| to |foo.INIT|.

These names (obviously) can't clash with each other, or with those produced by stv-fully-general-in-alists.

We memoize this to ensure we'll get the same initial state alist across different STVs that target the same module.

Definitions and Theorems

Function: stv-fully-general-st-alist

(defun stv-fully-general-st-alist (mod)
 (declare (xargs :guard t))
 (let ((__function__ 'stv-fully-general-st-alist))
   (declare (ignorable __function__))
   (b*
    ((sts (mod-state mod))
     (flat-sts (pat-flatten sts nil))
     ((unless (symbol-listp flat-sts))
      (raise
           "Expected mod-state to produce a symbol pattern for ~x0."
           (gpl :n mod))))
    (pairlis$ flat-sts
              (stv-suffix-signals flat-sts ".INIT")))))