		Search-engine friendly clone of the ACL2 documentation.

Transitions

Event-next

New state resulting from an event.

Signature
(event-next event systate) → new-systate
Arguments: event — Guard (eventp event).; systate — Guard (system-statep systate).
Returns: new-systate — Type (system-statep new-systate).

Based on the event, we use the appropriate function.

Definitions and Theorems

Function: event-next

(defun event-next (event systate)
  (declare (xargs :guard (and (eventp event)
                              (system-statep systate))))
  (declare (xargs :guard (event-possiblep event systate)))
  (let ((__function__ 'event-next))
    (declare (ignorable __function__))
    (event-case event
                :create (create-next event.certificate systate)
                :receive (receive-next event.message systate)
                :store (store-next event.validator
                                   event.certificate systate)
                :advance (advance-next event.validator systate)
                :commit (commit-next event.validator systate)
                :timeout (timeout-next event.validator systate))))

Theorem: system-statep-of-event-next

(defthm system-statep-of-event-next
  (b* ((new-systate (event-next event systate)))
    (system-statep new-systate))
  :rule-classes :rewrite)

Theorem: correct-addresses-of-event-next

(defthm correct-addresses-of-event-next
  (implies (event-possiblep event systate)
           (b* ((?new-systate (event-next event systate)))
             (equal (correct-addresses new-systate)
                    (correct-addresses systate)))))

Theorem: event-next-of-event-fix-event

(defthm event-next-of-event-fix-event
  (equal (event-next (event-fix event) systate)
         (event-next event systate)))

Theorem: event-next-event-equiv-congruence-on-event

(defthm event-next-event-equiv-congruence-on-event
  (implies (event-equiv event event-equiv)
           (equal (event-next event systate)
                  (event-next event-equiv systate)))
  :rule-classes :congruence)

Theorem: event-next-of-system-state-fix-systate

(defthm event-next-of-system-state-fix-systate
  (equal (event-next event (system-state-fix systate))
         (event-next event systate)))

Theorem: event-next-system-state-equiv-congruence-on-systate

(defthm event-next-system-state-equiv-congruence-on-systate
  (implies (system-state-equiv systate systate-equiv)
           (equal (event-next event systate)
                  (event-next event systate-equiv)))
  :rule-classes :congruence)