		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-certificate
      (create-certificate-next event.certificate systate)
      :receive-certificate
      (receive-certificate-next event.message systate)
      :store-certificate
      (store-certificate-next event.certificate
                              event.validator systate)
      :advance-round (advance-round-next event.validator systate)
      :commit-anchors (commit-anchors-next event.validator systate)
      :timer-expires (timer-expires-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)