This example shows how models of memory mapped I/O devices can be
connected to the current version of Anthony's ARM model. The idea is
to take the ARM next-state function and build a wrapper around it. The
wrapper essentially models the effect of the environment, i.e. the I/O
devices, as a relational operational semantics.

This example is based on polling, but interrupt-driven I/O devices
should also fit into the same wrapper-based approach.

Peter Homeier pointed out that files were missing.
Here are the missing files.