Create the sexpr-alist to use as the initial state for fully general simulations of a module.
(stv-fully-general-st-alist mod) → state-alist
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.
(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")))))