		Search-engine friendly clone of the ACL2 documentation.

Transitions-timeout

Timeout-possiblep

Check if a timeout event is possible.

Signature
(timeout-possiblep val systate) → yes/no
Arguments: val — Guard (addressp val).; systate — Guard (system-statep systate).
Returns: yes/no — Type (booleanp yes/no).

The val input of this function is the address in the timeout event; see event.

The validator must be a correct one.

The timer of the validator must be running.

Definitions and Theorems

Function: timeout-possiblep

(defun timeout-possiblep (val systate)
  (declare (xargs :guard (and (addressp val)
                              (system-statep systate))))
  (let ((__function__ 'timeout-possiblep))
    (declare (ignorable __function__))
    (b* (((unless (in (address-fix val)
                      (correct-addresses systate)))
          nil)
         ((validator-state vstate)
          (get-validator-state val systate)))
      (timer-case vstate.timer :running))))

Theorem: booleanp-of-timeout-possiblep

(defthm booleanp-of-timeout-possiblep
  (b* ((yes/no (timeout-possiblep val systate)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: timeout-possiblep-of-address-fix-val

(defthm timeout-possiblep-of-address-fix-val
  (equal (timeout-possiblep (address-fix val)
                            systate)
         (timeout-possiblep val systate)))

Theorem: timeout-possiblep-address-equiv-congruence-on-val

(defthm timeout-possiblep-address-equiv-congruence-on-val
  (implies (address-equiv val val-equiv)
           (equal (timeout-possiblep val systate)
                  (timeout-possiblep val-equiv systate)))
  :rule-classes :congruence)

Theorem: timeout-possiblep-of-system-state-fix-systate

(defthm timeout-possiblep-of-system-state-fix-systate
  (equal (timeout-possiblep val (system-state-fix systate))
         (timeout-possiblep val systate)))

Theorem: timeout-possiblep-system-state-equiv-congruence-on-systate

(defthm timeout-possiblep-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (timeout-possiblep val systate)
                  (timeout-possiblep val systate-equiv)))
  :rule-classes :congruence)