		Search-engine friendly clone of the ACL2 documentation.

Transitions-timer-expires

Timer-expires-possiblep

Check if a timer-expires event is possible.

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

This event is possible when the timer is running. The address must be that of a correct validator; we do not model the internal state of faulty validators, and whether they have any timers at all.

Definitions and Theorems

Function: timer-expires-possiblep

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

Theorem: booleanp-of-timer-expires-possiblep

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

Theorem: timer-expires-possiblep-of-system-state-fix-systate

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

Theorem: timer-expires-possiblep-system-state-equiv-congruence-on-systate

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