		Search-engine friendly clone of the ACL2 documentation.

System-states

Get-network-state

Retrieve the state of the network in the system.

Signature
(get-network-state systate) → network
Arguments: systate — Guard (system-statep systate).
Returns: network — Type (message-setp network).

This is a thin layer, but it provides slightly more abstraction.

Definitions and Theorems

Function: get-network-state

(defun get-network-state (systate)
  (declare (xargs :guard (system-statep systate)))
  (let ((__function__ 'get-network-state))
    (declare (ignorable __function__))
    (system-state->network systate)))

Theorem: message-setp-of-get-network-state

(defthm message-setp-of-get-network-state
  (b* ((network (get-network-state systate)))
    (message-setp network))
  :rule-classes :rewrite)

Theorem: get-network-state-of-update-validator-state

(defthm get-network-state-of-update-validator-state
 (equal
     (get-network-state (update-validator-state val vstate systate))
     (get-network-state systate)))

Theorem: get-network-state-of-system-state-fix-systate

(defthm get-network-state-of-system-state-fix-systate
  (equal (get-network-state (system-state-fix systate))
         (get-network-state systate)))

Theorem: get-network-state-system-state-equiv-congruence-on-systate

(defthm get-network-state-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (get-network-state systate)
                  (get-network-state systate-equiv)))
  :rule-classes :congruence)