diff --git a/micro-examples/microkit/aadl_port_types/data/aadl/.system b/micro-examples/microkit/aadl_port_types/data/aadl/.system
index a68546c..c44b15d 100644
--- a/micro-examples/microkit/aadl_port_types/data/aadl/.system
+++ b/micro-examples/microkit/aadl_port_types/data/aadl/.system
@@ -1,3 +1,3 @@
 system_impl=top.impl
-system_impl_file=event_data_1_prod_2_cons.aadl
+system_impl_file=data_1_prod_2_cons.aadl
 projects=.
\ No newline at end of file
diff --git a/micro-examples/microkit/aadl_port_types/data/aadl/bin/run-hamr.cmd b/micro-examples/microkit/aadl_port_types/data/aadl/bin/run-hamr.cmd
new file mode 100755
index 0000000..688869c
--- /dev/null
+++ b/micro-examples/microkit/aadl_port_types/data/aadl/bin/run-hamr.cmd
@@ -0,0 +1,103 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val aadlDir = Os.slashDir.up
+
+
+val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" 
+val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum")
+
+val osate: Os.Path = Os.env("OSATE_HOME") match {
+  case Some(s) => Os.path(s) / (if (Os.isWin) "osate.exe" else if (Os.isLinux) "osate" else "Contents/MacOs/osate")
+  case _ if (Os.isWin) => sireumBin / "win" / "fmide" / "fmide.exe"
+  case _ if (Os.isMac) => sireumBin / "mac" / "fmide.app" / "Contents" / "MacOs" / "osate"
+  case _ if (Os.isLinux) => sireumBin / "linux" / "fmide" / "fmide"
+  case _ =>
+    println("Unsupported operating system")
+    Os.exit(1)
+    halt("")
+}
+
+if (!osate.exists) {
+  eprintln("Please install FMIDE (e.g. '$SIREUM_HOME/bin/install/fmide.cmd') or OSATE (e.g. 'sireum hamr phantom -u')")
+  Os.exit(1)
+  halt("")
+}
+
+val osireum = ISZ(osate.string, "-nosplash", "--launcher.suppressErrors", "-data", "@user.home/.sireum", "-application", "org.sireum.aadl.osate.cli")
+
+if(Os.cliArgs.size > 1) {
+  eprintln("Only expecting a single argument")
+  Os.exit(1)
+}
+
+val platform: String =
+  if(Os.cliArgs.nonEmpty) Os.cliArgs(0)
+  else "Microkit"
+
+val packageName = "microkit" // not used for 'microkit' platform 
+
+val excludeComponentImpl = F
+
+// commenting out options that are not used by 'microkit' platform
+var codegenArgs = ISZ("hamr", "codegen",
+  "--platform", platform,
+  //"--package-name", packageName,
+  //"--output-dir", (aadlDir.up / "hamr" / "slang").string,
+  //"--output-c-dir", (aadlDir.up / "hamr" / "c").string,
+  "--camkes-output-dir", (aadlDir.up / "hamr" / "microkit").string,  
+  //"--run-transpiler",
+  //"--bit-width", "32",
+  //"--max-string-size", "256",
+  //"--max-array-size", "1",
+  "--verbose",
+  //"--workspace-root-dir", aadlDir.string
+  )
+
+if (platform == "JVM") {
+  codegenArgs = codegenArgs :+ "--runtime-monitoring"
+} else {
+  println("***********************************************************************")
+  println(s"Note: runtime-monitoring support is not yet avialable for ${platform}")
+  println("***********************************************************************")
+}
+
+if (excludeComponentImpl) {
+  //codegenArgs = codegenArgs :+ "--exclude-component-impl"
+}
+
+if ((aadlDir.up / "hamr" / "slang" / ".idea").exists) {
+  codegenArgs = codegenArgs :+ "--no-proyek-ive"
+}
+
+codegenArgs = codegenArgs :+ (aadlDir / ".system").string
+
+val results = Os.proc(osireum ++ codegenArgs).echo.console.run()
+ 
+// Running under windows results in 23 which is an indication 
+// a platform restart was requested. Codegen completes 
+// successfully and the cli app returns 0 so 
+// not sure why this is being issued.
+if(results.exitCode == 0 || results.exitCode == 23) {
+  Os.exit(0)
+} else {
+  println(results.err)
+  Os.exit(results.exitCode)
+}
diff --git a/micro-examples/microkit/aadl_port_types/data/readme.md b/micro-examples/microkit/aadl_port_types/data/readme.md
index 8cae700..2c12ec3 100644
--- a/micro-examples/microkit/aadl_port_types/data/readme.md
+++ b/micro-examples/microkit/aadl_port_types/data/readme.md
@@ -16,4 +16,132 @@
 |--|--|
 |Threads|3|
 |Ports|3|
-|Connections|2|
\ No newline at end of file
+|Connections|2|
+
+
+
+## Codegen
+
+1. Install [Docker Desktop](https://www.docker.com/products/docker-desktop/)
+
+1. Clone this repo and cd into it ``INSPECTA-models``
+
+   ```
+   git clone https://github.com/loonwerks/INSPECTA-models.git
+   cd INSPECTA-models
+   ```
+
+1. *OPTIONAL*
+
+    If you want to rerun codegen then you will need to install Sireum
+    and OSATE.  You can do this inside or outside of the container that you'll install in the next step (the latter is probably preferable as you could then use Sireum outside of the container).
+
+    Copy/paste the following to install Sireum
+    ```
+    git clone https://github.com/sireum/kekinian.git
+    kekinian/bin/build.cmd
+    ```
+
+    This installs/build Sireum from source rather than via a binary distribution (which is probably the prefered method for PROVERS).  
+
+    Now set ``SIREUM_HOME`` to point to where you cloned kekinian and add ``$SIREUM_HOME/bin`` to your path.  E.g. for bash
+
+    ```
+    echo "export SIREUM_HOME=$(pwd)/kekinian" >> $HOME/.bashrc
+    echo "export PATH=\$SIREUM_HOME/bin:\$PATH" >> $HOME/.bashrc
+    source $HOME/.bashrc
+    ```
+
+    To update Sireum in the future do the following
+    ```
+    cd $SIREUM_HOME
+    git pull --rec
+    bin/build.cmd
+    ```
+
+
+    Now install OSATE and the Sireum OSATE plugins into your current directory (or wherever as indicated via the ``-o`` option).  For Windows/Linux 
+
+    ```
+    sireum hamr phantom -u -v -o $(pwd)/osate
+    ```
+
+    or for Mac copy/paste
+    ```
+    sireum hamr phantom -u -v -o $(pwd)/osate.app
+    ```
+
+    Now set ``OSATE_HOME`` to point to where you installed Osate
+
+    ```
+    echo "export OSATE_HOME=$(pwd)/osate" >> $HOME/.bashrc
+    source $HOME/.bashrc
+    ```
+
+1. Download and run the CAmkES docker container, mounting the ``INSPECTA-models`` directory into it
+
+   ```
+   docker run -it -w /root -v $(pwd):/root/INSPECTA-models jasonbelt/microkit_domain_scheduling
+   ```
+
+   This container includes customized versions of Microkit and seL4 that support domain scheduling.  They were built off the following pull requests
+
+   - [microkit #175](https://github.com/seL4/microkit/pull/175)
+   - [seL4 #1308](https://github.com/seL4/seL4/pull/1308)
+
+1. *OPTIONAL* Rerun codegen
+   
+    Launch the Slash script [micro-examples/microkit/aadl_port_types/data/aadl/bin/run-hamr.cmd](aadl/bin/run-hamr.cmd) from the command line.  
+
+   ```
+   micro-examples/microkit/aadl_port_types/data/aadl/bin/run-hamr.cmd
+   ```
+
+1. Build and simulate the image
+
+    Inside the container do the following
+
+    ```
+    export MICROKIT_BOARD=qemu_virt_aarch64
+    export MICROKIT_SDK=/root/microkit/release/microkit-sdk-1.4.1-dev.14+cf88629
+    cd $HOME/INSPECTA-models/micro-examples/microkit/aadl_port_types/data/hamr/microkit
+    make qemu
+    ```
+
+    Type ``CTRL-a x`` to exit the QEMU simulation
+    
+    You should get output similar to
+    ```
+    Booting all finished, dropped to user space
+    MON|INFO: Microkit Bootstrap
+    MON|INFO: bootinfo untyped list matches expected list
+    MON|INFO: Number of bootstrap invocations: 0x00000009
+    MON|INFO: Number of system invocations:    0x000000c5
+    MON|INFO: completed bootstrap invocations
+    MON|INFO: completed system invocations
+    consumer_p_p_con: I'm periodic
+    consumer_p_s_con: I'm sporadic so you'll never hear from me again :(
+    producer_p_p_pro: I'm periodic, initialized outgoing data port
+    consumer_p_p_con: retrieved 0 which is fresh
+    ------
+    producer_p_p_pro: nothing sent
+    consumer_p_p_con: retrieved 0 which is stale
+    ------
+    producer_p_p_pro: sent 2
+    consumer_p_p_con: retrieved 2 which is fresh
+    ------
+    producer_p_p_pro: nothing sent
+    consumer_p_p_con: retrieved 2 which is stale
+    ------
+    producer_p_p_pro: sent 4
+    consumer_p_p_con: retrieved 4 which is fresh
+    ------
+    producer_p_p_pro: nothing sent
+    consumer_p_p_con: retrieved 4 which is stale
+    ------
+    producer_p_p_pro: sent 6
+    consumer_p_p_con: retrieved 6 which is fresh
+    ------
+    producer_p_p_pro: nothing sent
+    consumer_p_p_con: retrieved 6 which is stale
+    ```
\ No newline at end of file
diff --git a/micro-examples/microkit/aadl_port_types/event/aadl/.system b/micro-examples/microkit/aadl_port_types/event/aadl/.system
index a68546c..bfe3002 100644
--- a/micro-examples/microkit/aadl_port_types/event/aadl/.system
+++ b/micro-examples/microkit/aadl_port_types/event/aadl/.system
@@ -1,3 +1,3 @@
 system_impl=top.impl
-system_impl_file=event_data_1_prod_2_cons.aadl
+system_impl_file=event_2_prod_2_cons.aadl
 projects=.
\ No newline at end of file
diff --git a/micro-examples/microkit/aadl_port_types/event/aadl/bin/run-hamr.cmd b/micro-examples/microkit/aadl_port_types/event/aadl/bin/run-hamr.cmd
new file mode 100755
index 0000000..688869c
--- /dev/null
+++ b/micro-examples/microkit/aadl_port_types/event/aadl/bin/run-hamr.cmd
@@ -0,0 +1,103 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val aadlDir = Os.slashDir.up
+
+
+val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" 
+val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum")
+
+val osate: Os.Path = Os.env("OSATE_HOME") match {
+  case Some(s) => Os.path(s) / (if (Os.isWin) "osate.exe" else if (Os.isLinux) "osate" else "Contents/MacOs/osate")
+  case _ if (Os.isWin) => sireumBin / "win" / "fmide" / "fmide.exe"
+  case _ if (Os.isMac) => sireumBin / "mac" / "fmide.app" / "Contents" / "MacOs" / "osate"
+  case _ if (Os.isLinux) => sireumBin / "linux" / "fmide" / "fmide"
+  case _ =>
+    println("Unsupported operating system")
+    Os.exit(1)
+    halt("")
+}
+
+if (!osate.exists) {
+  eprintln("Please install FMIDE (e.g. '$SIREUM_HOME/bin/install/fmide.cmd') or OSATE (e.g. 'sireum hamr phantom -u')")
+  Os.exit(1)
+  halt("")
+}
+
+val osireum = ISZ(osate.string, "-nosplash", "--launcher.suppressErrors", "-data", "@user.home/.sireum", "-application", "org.sireum.aadl.osate.cli")
+
+if(Os.cliArgs.size > 1) {
+  eprintln("Only expecting a single argument")
+  Os.exit(1)
+}
+
+val platform: String =
+  if(Os.cliArgs.nonEmpty) Os.cliArgs(0)
+  else "Microkit"
+
+val packageName = "microkit" // not used for 'microkit' platform 
+
+val excludeComponentImpl = F
+
+// commenting out options that are not used by 'microkit' platform
+var codegenArgs = ISZ("hamr", "codegen",
+  "--platform", platform,
+  //"--package-name", packageName,
+  //"--output-dir", (aadlDir.up / "hamr" / "slang").string,
+  //"--output-c-dir", (aadlDir.up / "hamr" / "c").string,
+  "--camkes-output-dir", (aadlDir.up / "hamr" / "microkit").string,  
+  //"--run-transpiler",
+  //"--bit-width", "32",
+  //"--max-string-size", "256",
+  //"--max-array-size", "1",
+  "--verbose",
+  //"--workspace-root-dir", aadlDir.string
+  )
+
+if (platform == "JVM") {
+  codegenArgs = codegenArgs :+ "--runtime-monitoring"
+} else {
+  println("***********************************************************************")
+  println(s"Note: runtime-monitoring support is not yet avialable for ${platform}")
+  println("***********************************************************************")
+}
+
+if (excludeComponentImpl) {
+  //codegenArgs = codegenArgs :+ "--exclude-component-impl"
+}
+
+if ((aadlDir.up / "hamr" / "slang" / ".idea").exists) {
+  codegenArgs = codegenArgs :+ "--no-proyek-ive"
+}
+
+codegenArgs = codegenArgs :+ (aadlDir / ".system").string
+
+val results = Os.proc(osireum ++ codegenArgs).echo.console.run()
+ 
+// Running under windows results in 23 which is an indication 
+// a platform restart was requested. Codegen completes 
+// successfully and the cli app returns 0 so 
+// not sure why this is being issued.
+if(results.exitCode == 0 || results.exitCode == 23) {
+  Os.exit(0)
+} else {
+  println(results.err)
+  Os.exit(results.exitCode)
+}
diff --git a/micro-examples/microkit/aadl_port_types/event/readme.md b/micro-examples/microkit/aadl_port_types/event/readme.md
index 778fce9..30d6228 100644
--- a/micro-examples/microkit/aadl_port_types/event/readme.md
+++ b/micro-examples/microkit/aadl_port_types/event/readme.md
@@ -16,4 +16,143 @@
 |--|--|
 |Threads|4|
 |Ports|6|
-|Connections|4|
\ No newline at end of file
+|Connections|4|
+
+
+## Codegen
+
+1. Install [Docker Desktop](https://www.docker.com/products/docker-desktop/)
+
+1. Clone this repo and cd into it ``INSPECTA-models``
+
+   ```
+   git clone https://github.com/loonwerks/INSPECTA-models.git
+   cd INSPECTA-models
+   ```
+
+1. *OPTIONAL*
+
+    If you want to rerun codegen then you will need to install Sireum
+    and OSATE.  You can do this inside or outside of the container that you'll install in the next step (the latter is probably preferable as you could then use Sireum outside of the container).
+
+    Copy/paste the following to install Sireum
+    ```
+    git clone https://github.com/sireum/kekinian.git
+    kekinian/bin/build.cmd
+    ```
+
+    This installs/build Sireum from source rather than via a binary distribution (which is probably the prefered method for PROVERS).  
+
+    Now set ``SIREUM_HOME`` to point to where you cloned kekinian and add ``$SIREUM_HOME/bin`` to your path.  E.g. for bash
+
+    ```
+    echo "export SIREUM_HOME=$(pwd)/kekinian" >> $HOME/.bashrc
+    echo "export PATH=\$SIREUM_HOME/bin:\$PATH" >> $HOME/.bashrc
+    source $HOME/.bashrc
+    ```
+
+    To update Sireum in the future do the following
+    ```
+    cd $SIREUM_HOME
+    git pull --rec
+    bin/build.cmd
+    ```
+
+
+    Now install OSATE and the Sireum OSATE plugins into your current directory (or wherever as indicated via the ``-o`` option).  For Windows/Linux 
+
+    ```
+    sireum hamr phantom -u -v -o $(pwd)/osate
+    ```
+
+    or for Mac copy/paste
+    ```
+    sireum hamr phantom -u -v -o $(pwd)/osate.app
+    ```
+
+    Now set ``OSATE_HOME`` to point to where you installed Osate
+
+    ```
+    echo "export OSATE_HOME=$(pwd)/osate" >> $HOME/.bashrc
+    source $HOME/.bashrc
+    ```
+
+1. Download and run the CAmkES docker container, mounting the ``INSPECTA-models`` directory into it
+
+   ```
+   docker run -it -w /root -v $(pwd):/root/INSPECTA-models jasonbelt/microkit_domain_scheduling
+   ```
+
+   This container includes customized versions of Microkit and seL4 that support domain scheduling.  They were built off the following pull requests
+
+   - [microkit #175](https://github.com/seL4/microkit/pull/175)
+   - [seL4 #1308](https://github.com/seL4/seL4/pull/1308)
+
+1. *OPTIONAL* Rerun codegen
+   
+    Launch the Slash script [micro-examples/microkit/aadl_port_types/event/aadl/bin/run-hamr.cmd](aadl/bin/run-hamr.cmd) from the command line.  
+
+   ```
+   micro-examples/microkit/aadl_port_types/event/aadl/bin/run-hamr.cmd
+   ```
+
+1. Build and simulate the image
+
+    Inside the container do the following
+
+    ```
+    export MICROKIT_BOARD=qemu_virt_aarch64
+    export MICROKIT_SDK=/root/microkit/release/microkit-sdk-1.4.1-dev.14+cf88629
+    cd $HOME/INSPECTA-models/micro-examples/microkit/aadl_port_types/event/hamr/microkit
+    make qemu
+    ```
+
+    Type ``CTRL-a x`` to exit the QEMU simulation
+    
+    You should get output similar to
+    ```
+    Booting all finished, dropped to user space
+    MON|INFO: Microkit Bootstrap
+    MON|INFO: bootinfo untyped list matches expected list
+    MON|INFO: Number of bootstrap invocations: 0x00000009
+    MON|INFO: Number of system invocations:    0x000000fe
+    MON|INFO: completed bootstrap invocations
+    MON|INFO: completed system invocations
+    producer_p_p2_pr: I'm periodic
+    consumer_p_p_con: I'm periodic
+    consumer_p_s_con: I'm sporadic
+    producer_p_p1_pr: I'm periodic
+    producer_p_p2_pr: sent an event
+    consumer_p_p_con: nothing received on read port 1
+    consumer_p_p_con: received a read port 2 event
+    consumer_p_s_con: received a read port 2 event
+    -------
+    producer_p_p1_pr: sent an event
+    producer_p_p2_pr: no send
+    consumer_p_p_con: received a read port 1 event
+    consumer_p_p_con: nothing received on read port 2
+    consumer_p_s_con: received a read port 1 event
+    -------
+    producer_p_p1_pr: no send
+    producer_p_p2_pr: no send
+    consumer_p_p_con: nothing received on read port 1
+    consumer_p_p_con: nothing received on read port 2
+    -------
+    producer_p_p1_pr: sent an event
+    producer_p_p2_pr: sent an event
+    consumer_p_p_con: received a read port 1 event
+    consumer_p_p_con: received a read port 2 event
+    consumer_p_s_con: received a read port 1 event
+    consumer_p_s_con: received a read port 2 event
+    -------
+    producer_p_p1_pr: no send
+    producer_p_p2_pr: no send
+    consumer_p_p_con: nothing received on read port 1
+    consumer_p_p_con: nothing received on read port 2
+    -------
+    producer_p_p1_pr: sent an event
+    producer_p_p2_pr: no send
+    consumer_p_p_con: received a read port 1 event
+    consumer_p_p_con: nothing received on read port 2
+    consumer_p_s_con: received a read port 1 event
+    ```
\ No newline at end of file
diff --git a/micro-examples/microkit/aadl_port_types/event_data/aadl/.system b/micro-examples/microkit/aadl_port_types/event_data/aadl/.system
index a68546c..bd62d91 100644
--- a/micro-examples/microkit/aadl_port_types/event_data/aadl/.system
+++ b/micro-examples/microkit/aadl_port_types/event_data/aadl/.system
@@ -1,3 +1,3 @@
 system_impl=top.impl
-system_impl_file=event_data_1_prod_2_cons.aadl
+system_impl_file=event_data_2_prod_2_cons.aadl
 projects=.
\ No newline at end of file
diff --git a/micro-examples/microkit/aadl_port_types/event_data/aadl/bin/run-hamr.cmd b/micro-examples/microkit/aadl_port_types/event_data/aadl/bin/run-hamr.cmd
new file mode 100755
index 0000000..688869c
--- /dev/null
+++ b/micro-examples/microkit/aadl_port_types/event_data/aadl/bin/run-hamr.cmd
@@ -0,0 +1,103 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val aadlDir = Os.slashDir.up
+
+
+val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" 
+val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum")
+
+val osate: Os.Path = Os.env("OSATE_HOME") match {
+  case Some(s) => Os.path(s) / (if (Os.isWin) "osate.exe" else if (Os.isLinux) "osate" else "Contents/MacOs/osate")
+  case _ if (Os.isWin) => sireumBin / "win" / "fmide" / "fmide.exe"
+  case _ if (Os.isMac) => sireumBin / "mac" / "fmide.app" / "Contents" / "MacOs" / "osate"
+  case _ if (Os.isLinux) => sireumBin / "linux" / "fmide" / "fmide"
+  case _ =>
+    println("Unsupported operating system")
+    Os.exit(1)
+    halt("")
+}
+
+if (!osate.exists) {
+  eprintln("Please install FMIDE (e.g. '$SIREUM_HOME/bin/install/fmide.cmd') or OSATE (e.g. 'sireum hamr phantom -u')")
+  Os.exit(1)
+  halt("")
+}
+
+val osireum = ISZ(osate.string, "-nosplash", "--launcher.suppressErrors", "-data", "@user.home/.sireum", "-application", "org.sireum.aadl.osate.cli")
+
+if(Os.cliArgs.size > 1) {
+  eprintln("Only expecting a single argument")
+  Os.exit(1)
+}
+
+val platform: String =
+  if(Os.cliArgs.nonEmpty) Os.cliArgs(0)
+  else "Microkit"
+
+val packageName = "microkit" // not used for 'microkit' platform 
+
+val excludeComponentImpl = F
+
+// commenting out options that are not used by 'microkit' platform
+var codegenArgs = ISZ("hamr", "codegen",
+  "--platform", platform,
+  //"--package-name", packageName,
+  //"--output-dir", (aadlDir.up / "hamr" / "slang").string,
+  //"--output-c-dir", (aadlDir.up / "hamr" / "c").string,
+  "--camkes-output-dir", (aadlDir.up / "hamr" / "microkit").string,  
+  //"--run-transpiler",
+  //"--bit-width", "32",
+  //"--max-string-size", "256",
+  //"--max-array-size", "1",
+  "--verbose",
+  //"--workspace-root-dir", aadlDir.string
+  )
+
+if (platform == "JVM") {
+  codegenArgs = codegenArgs :+ "--runtime-monitoring"
+} else {
+  println("***********************************************************************")
+  println(s"Note: runtime-monitoring support is not yet avialable for ${platform}")
+  println("***********************************************************************")
+}
+
+if (excludeComponentImpl) {
+  //codegenArgs = codegenArgs :+ "--exclude-component-impl"
+}
+
+if ((aadlDir.up / "hamr" / "slang" / ".idea").exists) {
+  codegenArgs = codegenArgs :+ "--no-proyek-ive"
+}
+
+codegenArgs = codegenArgs :+ (aadlDir / ".system").string
+
+val results = Os.proc(osireum ++ codegenArgs).echo.console.run()
+ 
+// Running under windows results in 23 which is an indication 
+// a platform restart was requested. Codegen completes 
+// successfully and the cli app returns 0 so 
+// not sure why this is being issued.
+if(results.exitCode == 0 || results.exitCode == 23) {
+  Os.exit(0)
+} else {
+  println(results.err)
+  Os.exit(results.exitCode)
+}
diff --git a/micro-examples/microkit/aadl_port_types/event_data/readme.md b/micro-examples/microkit/aadl_port_types/event_data/readme.md
index 28e4e58..da4a25c 100644
--- a/micro-examples/microkit/aadl_port_types/event_data/readme.md
+++ b/micro-examples/microkit/aadl_port_types/event_data/readme.md
@@ -1,4 +1,4 @@
-# AADL Event DataPorts
+# AADL Event Data Ports
 
  Table of Contents
   * [Diagrams](#diagrams)
@@ -16,4 +16,159 @@
 |--|--|
 |Threads|4|
 |Ports|6|
-|Connections|4|
\ No newline at end of file
+|Connections|4|
+
+
+## Codegen
+
+1. Install [Docker Desktop](https://www.docker.com/products/docker-desktop/)
+
+1. Clone this repo and cd into it ``INSPECTA-models``
+
+   ```
+   git clone https://github.com/loonwerks/INSPECTA-models.git
+   cd INSPECTA-models
+   ```
+
+1. *OPTIONAL*
+
+    If you want to rerun codegen then you will need to install Sireum
+    and OSATE.  You can do this inside or outside of the container that you'll install in the next step (the latter is probably preferable as you could then use Sireum outside of the container).
+
+    Copy/paste the following to install Sireum
+    ```
+    git clone https://github.com/sireum/kekinian.git
+    kekinian/bin/build.cmd
+    ```
+
+    This installs/build Sireum from source rather than via a binary distribution (which is probably the prefered method for PROVERS).  
+
+    Now set ``SIREUM_HOME`` to point to where you cloned kekinian and add ``$SIREUM_HOME/bin`` to your path.  E.g. for bash
+
+    ```
+    echo "export SIREUM_HOME=$(pwd)/kekinian" >> $HOME/.bashrc
+    echo "export PATH=\$SIREUM_HOME/bin:\$PATH" >> $HOME/.bashrc
+    source $HOME/.bashrc
+    ```
+
+    To update Sireum in the future do the following
+    ```
+    cd $SIREUM_HOME
+    git pull --rec
+    bin/build.cmd
+    ```
+
+
+    Now install OSATE and the Sireum OSATE plugins into your current directory (or wherever as indicated via the ``-o`` option).  For Windows/Linux 
+
+    ```
+    sireum hamr phantom -u -v -o $(pwd)/osate
+    ```
+
+    or for Mac copy/paste
+    ```
+    sireum hamr phantom -u -v -o $(pwd)/osate.app
+    ```
+
+    Now set ``OSATE_HOME`` to point to where you installed Osate
+
+    ```
+    echo "export OSATE_HOME=$(pwd)/osate" >> $HOME/.bashrc
+    source $HOME/.bashrc
+    ```
+
+1. Download and run the CAmkES docker container, mounting the ``INSPECTA-models`` directory into it
+
+   ```
+   docker run -it -w /root -v $(pwd):/root/INSPECTA-models jasonbelt/microkit_domain_scheduling
+   ```
+
+   This container includes customized versions of Microkit and seL4 that support domain scheduling.  They were built off the following pull requests
+
+   - [microkit #175](https://github.com/seL4/microkit/pull/175)
+   - [seL4 #1308](https://github.com/seL4/seL4/pull/1308)
+
+1. *OPTIONAL* Rerun codegen
+   
+    Launch the Slash script [micro-examples/microkit/aadl_port_types/event_data/aadl/bin/run-hamr.cmd](aadl/bin/run-hamr.cmd) from the command line.  
+
+   ```
+   micro-examples/microkit/aadl_port_types/event_data/aadl/bin/run-hamr.cmd
+   ```
+
+1. Build and simulate the image
+
+    Inside the container do the following
+
+    ```
+    export MICROKIT_BOARD=qemu_virt_aarch64
+    export MICROKIT_SDK=/root/microkit/release/microkit-sdk-1.4.1-dev.14+cf88629
+    cd $HOME/INSPECTA-models/micro-examples/microkit/aadl_port_types/event_data/hamr/microkit
+    make qemu
+    ```
+
+    Type ``CTRL-a x`` to exit the QEMU simulation
+
+    You should get output similar to
+    ```
+    Booting all finished, dropped to user space
+    MON|INFO: Microkit Bootstrap
+    MON|INFO: bootinfo untyped list matches expected list
+    MON|INFO: Number of bootstrap invocations: 0x00000009
+    MON|INFO: Number of system invocations:    0x000000fe
+    MON|INFO: completed bootstrap invocations
+    MON|INFO: completed system invocations
+    consumer_p_p_con: I'm periodic
+    consumer_p_s_con: I'm sporadic
+    producer_p_p1_pr: I'm periodic
+    producer_p_p2_pr: I'm periodic
+    consumer_p_p_con: nothing received on read port 1
+    consumer_p_p_con: nothing received on read port 2
+    -------
+    producer_p_p1_pr: sent event 0
+    producer_p_p2_pr: sent event 0
+    consumer_p_p_con: received 0 on read port 1 event
+    consumer_p_p_con: received 0 on read port 2 event
+    consumer_p_s_con: Received 0 on read port 1
+    consumer_p_s_con: Received 0 on read port 2
+    -------
+    producer_p_p1_pr: no send
+    producer_p_p2_pr: no send
+    consumer_p_p_con: nothing received on read port 1
+    consumer_p_p_con: nothing received on read port 2
+    -------
+    producer_p_p1_pr: sent event 2
+    producer_p_p2_pr: no send
+    consumer_p_p_con: received 2 on read port 1 event
+    consumer_p_p_con: nothing received on read port 2
+    consumer_p_s_con: Received 2 on read port 1
+    -------
+    producer_p_p1_pr: no send
+    producer_p_p2_pr: sent event 3
+    consumer_p_p_con: nothing received on read port 1
+    consumer_p_p_con: received 3 on read port 2 event
+    consumer_p_s_con: Received 3 on read port 2
+    -------
+    producer_p_p1_pr: sent event 4
+    producer_p_p2_pr: no send
+    consumer_p_p_con: received 4 on read port 1 event
+    consumer_p_p_con: nothing received on read port 2
+    consumer_p_s_con: Received 4 on read port 1
+    -------
+    producer_p_p1_pr: no send
+    producer_p_p2_pr: no send
+    consumer_p_p_con: nothing received on read port 1
+    consumer_p_p_con: nothing received on read port 2
+    -------
+    producer_p_p1_pr: sent event 6
+    producer_p_p2_pr: sent event 6
+    consumer_p_p_con: received 6 on read port 1 event
+    consumer_p_p_con: received 6 on read port 2 event
+    consumer_p_s_con: Received 6 on read port 1
+    consumer_p_s_con: Received 6 on read port 2
+    -------
+    producer_p_p1_pr: no send
+    producer_p_p2_pr: no send
+    consumer_p_p_con: nothing received on read port 1
+    consumer_p_p_con: nothing received on read port 2
+    ```
\ No newline at end of file
diff --git a/micro-examples/microkit/port_queues/event_data/aadl/.system b/micro-examples/microkit/port_queues/event_data/aadl/.system
index a68546c..0ae6588 100644
--- a/micro-examples/microkit/port_queues/event_data/aadl/.system
+++ b/micro-examples/microkit/port_queues/event_data/aadl/.system
@@ -1,3 +1,3 @@
 system_impl=top.impl
-system_impl_file=event_data_1_prod_2_cons.aadl
+system_impl_file=event_data_port_queues.aadl
 projects=.
\ No newline at end of file
diff --git a/micro-examples/microkit/port_queues/event_data/aadl/bin/run-hamr.cmd b/micro-examples/microkit/port_queues/event_data/aadl/bin/run-hamr.cmd
new file mode 100755
index 0000000..688869c
--- /dev/null
+++ b/micro-examples/microkit/port_queues/event_data/aadl/bin/run-hamr.cmd
@@ -0,0 +1,103 @@
+::/*#! 2> /dev/null                                 #
+@ 2>/dev/null # 2>nul & echo off & goto BOF         #
+if [ -z ${SIREUM_HOME} ]; then                      #
+  echo "Please set SIREUM_HOME env var"             #
+  exit -1                                           #
+fi                                                  #
+exec ${SIREUM_HOME}/bin/sireum slang run "$0" "$@"  #
+:BOF
+setlocal
+if not defined SIREUM_HOME (
+  echo Please set SIREUM_HOME env var
+  exit /B -1
+)
+%SIREUM_HOME%\\bin\\sireum.bat slang run "%0" %*
+exit /B %errorlevel%
+::!#*/
+// #Sireum
+
+import org.sireum._
+
+val aadlDir = Os.slashDir.up
+
+
+val sireumBin = Os.path(Os.env("SIREUM_HOME").get) / "bin" 
+val sireum = sireumBin / (if(Os.isWin) "sireum.bat" else "sireum")
+
+val osate: Os.Path = Os.env("OSATE_HOME") match {
+  case Some(s) => Os.path(s) / (if (Os.isWin) "osate.exe" else if (Os.isLinux) "osate" else "Contents/MacOs/osate")
+  case _ if (Os.isWin) => sireumBin / "win" / "fmide" / "fmide.exe"
+  case _ if (Os.isMac) => sireumBin / "mac" / "fmide.app" / "Contents" / "MacOs" / "osate"
+  case _ if (Os.isLinux) => sireumBin / "linux" / "fmide" / "fmide"
+  case _ =>
+    println("Unsupported operating system")
+    Os.exit(1)
+    halt("")
+}
+
+if (!osate.exists) {
+  eprintln("Please install FMIDE (e.g. '$SIREUM_HOME/bin/install/fmide.cmd') or OSATE (e.g. 'sireum hamr phantom -u')")
+  Os.exit(1)
+  halt("")
+}
+
+val osireum = ISZ(osate.string, "-nosplash", "--launcher.suppressErrors", "-data", "@user.home/.sireum", "-application", "org.sireum.aadl.osate.cli")
+
+if(Os.cliArgs.size > 1) {
+  eprintln("Only expecting a single argument")
+  Os.exit(1)
+}
+
+val platform: String =
+  if(Os.cliArgs.nonEmpty) Os.cliArgs(0)
+  else "Microkit"
+
+val packageName = "microkit" // not used for 'microkit' platform 
+
+val excludeComponentImpl = F
+
+// commenting out options that are not used by 'microkit' platform
+var codegenArgs = ISZ("hamr", "codegen",
+  "--platform", platform,
+  //"--package-name", packageName,
+  //"--output-dir", (aadlDir.up / "hamr" / "slang").string,
+  //"--output-c-dir", (aadlDir.up / "hamr" / "c").string,
+  "--camkes-output-dir", (aadlDir.up / "hamr" / "microkit").string,  
+  //"--run-transpiler",
+  //"--bit-width", "32",
+  //"--max-string-size", "256",
+  //"--max-array-size", "1",
+  "--verbose",
+  //"--workspace-root-dir", aadlDir.string
+  )
+
+if (platform == "JVM") {
+  codegenArgs = codegenArgs :+ "--runtime-monitoring"
+} else {
+  println("***********************************************************************")
+  println(s"Note: runtime-monitoring support is not yet avialable for ${platform}")
+  println("***********************************************************************")
+}
+
+if (excludeComponentImpl) {
+  //codegenArgs = codegenArgs :+ "--exclude-component-impl"
+}
+
+if ((aadlDir.up / "hamr" / "slang" / ".idea").exists) {
+  codegenArgs = codegenArgs :+ "--no-proyek-ive"
+}
+
+codegenArgs = codegenArgs :+ (aadlDir / ".system").string
+
+val results = Os.proc(osireum ++ codegenArgs).echo.console.run()
+ 
+// Running under windows results in 23 which is an indication 
+// a platform restart was requested. Codegen completes 
+// successfully and the cli app returns 0 so 
+// not sure why this is being issued.
+if(results.exitCode == 0 || results.exitCode == 23) {
+  Os.exit(0)
+} else {
+  println(results.err)
+  Os.exit(results.exitCode)
+}
diff --git a/micro-examples/microkit/port_queues/event_data/readme.md b/micro-examples/microkit/port_queues/event_data/readme.md
index a4c7065..a92a494 100644
--- a/micro-examples/microkit/port_queues/event_data/readme.md
+++ b/micro-examples/microkit/port_queues/event_data/readme.md
@@ -16,4 +16,183 @@
 |--|--|
 |Threads|4|
 |Ports|4|
-|Connections|3|
\ No newline at end of file
+|Connections|3|
+
+
+
+## Codegen
+
+1. Install [Docker Desktop](https://www.docker.com/products/docker-desktop/)
+
+1. Clone this repo and cd into it ``INSPECTA-models``
+
+   ```
+   git clone https://github.com/loonwerks/INSPECTA-models.git
+   cd INSPECTA-models
+   ```
+
+1. *OPTIONAL*
+
+    If you want to rerun codegen then you will need to install Sireum
+    and OSATE.  You can do this inside or outside of the container that you'll install in the next step (the latter is probably preferable as you could then use Sireum outside of the container).
+
+    Copy/paste the following to install Sireum
+    ```
+    git clone https://github.com/sireum/kekinian.git
+    kekinian/bin/build.cmd
+    ```
+
+    This installs/build Sireum from source rather than via a binary distribution (which is probably the prefered method for PROVERS).  
+
+    Now set ``SIREUM_HOME`` to point to where you cloned kekinian and add ``$SIREUM_HOME/bin`` to your path.  E.g. for bash
+
+    ```
+    echo "export SIREUM_HOME=$(pwd)/kekinian" >> $HOME/.bashrc
+    echo "export PATH=\$SIREUM_HOME/bin:\$PATH" >> $HOME/.bashrc
+    source $HOME/.bashrc
+    ```
+
+    To update Sireum in the future do the following
+    ```
+    cd $SIREUM_HOME
+    git pull --rec
+    bin/build.cmd
+    ```
+
+
+    Now install OSATE and the Sireum OSATE plugins into your current directory (or wherever as indicated via the ``-o`` option).  For Windows/Linux 
+
+    ```
+    sireum hamr phantom -u -v -o $(pwd)/osate
+    ```
+
+    or for Mac copy/paste
+    ```
+    sireum hamr phantom -u -v -o $(pwd)/osate.app
+    ```
+
+    Now set ``OSATE_HOME`` to point to where you installed Osate
+
+    ```
+    echo "export OSATE_HOME=$(pwd)/osate" >> $HOME/.bashrc
+    source $HOME/.bashrc
+    ```
+
+1. Download and run the CAmkES docker container, mounting the ``INSPECTA-models`` directory into it
+
+   ```
+   docker run -it -w /root -v $(pwd):/root/INSPECTA-models jasonbelt/microkit_domain_scheduling
+   ```
+
+   This container includes customized versions of Microkit and seL4 that support domain scheduling.  They were built off the following pull requests
+
+   - [microkit #175](https://github.com/seL4/microkit/pull/175)
+   - [seL4 #1308](https://github.com/seL4/seL4/pull/1308)
+
+1. *OPTIONAL* Rerun codegen
+   
+    Launch the Slash script [micro-examples/microkit/port_queues/event_data/aadl/bin/run-hamr.cmd](aadl/bin/run-hamr.cmd) from the command line.  
+
+   ```
+   micro-examples/microkit/port_queues/event_data/aadl/bin/run-hamr.cmd
+   ```
+
+1. Build and simulate the image
+
+    Inside the container do the following
+
+    ```
+    export MICROKIT_BOARD=qemu_virt_aarch64
+    export MICROKIT_SDK=/root/microkit/release/microkit-sdk-1.4.1-dev.14+cf88629
+    cd $HOME/INSPECTA-models/micro-examples/microkit/port_queues/event_data/hamr/microkit
+    make qemu
+    ```
+
+    Type ``CTRL-a x`` to exit the QEMU simulation
+
+    You should get output similar to
+    ```
+    Booting all finished, dropped to user space
+    MON|INFO: Microkit Bootstrap
+    MON|INFO: bootinfo untyped list matches expected list
+    MON|INFO: Number of bootstrap invocations: 0x00000009
+    MON|INFO: Number of system invocations:    0x00000103
+    MON|INFO: completed bootstrap invocations
+    MON|INFO: completed system invocations
+    consumer_p_s2_co: I'm sporadic
+    consumer_p_s5_co: I'm sporadic
+    producer_p_p_pro: I'm periodic
+    consumer_p_s1_co: I'm sporadic
+    ---------------------------------------
+    producer_p_p_pro: Sent 0 events.
+    ---------------------------------------
+    producer_p_p_pro: Sent 1 events.
+    consumer_p_s1_co: received value {1}
+    consumer_p_s1_co: 1 events received
+    consumer_p_s2_co: received value {1}
+    consumer_p_s2_co: 1 events received
+    consumer_p_s5_co: received value {1}
+    consumer_p_s5_co: 1 events received
+    ---------------------------------------
+    producer_p_p_pro: Sent 2 events.
+    consumer_p_s1_co: received value {2}
+    consumer_p_s1_co: 1 events received
+    consumer_p_s2_co: received value {1}
+    consumer_p_s2_co: received value {2}
+    consumer_p_s2_co: 2 events received
+    consumer_p_s5_co: received value {1}
+    consumer_p_s5_co: received value {2}
+    consumer_p_s5_co: 2 events received
+    ---------------------------------------
+    producer_p_p_pro: Sent 3 events.
+    consumer_p_s1_co: received value {3}
+    consumer_p_s1_co: 1 events received
+    consumer_p_s2_co: received value {2}
+    consumer_p_s2_co: received value {3}
+    consumer_p_s2_co: 2 events received
+    consumer_p_s5_co: received value {1}
+    consumer_p_s5_co: received value {2}
+    consumer_p_s5_co: received value {3}
+    consumer_p_s5_co: 3 events received
+    ---------------------------------------
+    producer_p_p_pro: Sent 4 events.
+    consumer_p_s1_co: received value {4}
+    consumer_p_s1_co: 1 events received
+    consumer_p_s2_co: received value {3}
+    consumer_p_s2_co: received value {4}
+    consumer_p_s2_co: 2 events received
+    consumer_p_s5_co: received value {1}
+    consumer_p_s5_co: received value {2}
+    consumer_p_s5_co: received value {3}
+    consumer_p_s5_co: received value {4}
+    consumer_p_s5_co: 4 events received
+    ---------------------------------------
+    producer_p_p_pro: Sent 5 events.
+    consumer_p_s1_co: received value {5}
+    consumer_p_s1_co: 1 events received
+    consumer_p_s2_co: received value {4}
+    consumer_p_s2_co: received value {5}
+    consumer_p_s2_co: 2 events received
+    consumer_p_s5_co: received value {1}
+    consumer_p_s5_co: received value {2}
+    consumer_p_s5_co: received value {3}
+    consumer_p_s5_co: received value {4}
+    consumer_p_s5_co: received value {5}
+    consumer_p_s5_co: 5 events received
+    ---------------------------------------
+    producer_p_p_pro: Sent 6 events.
+    consumer_p_s1_co: received value {6}
+    consumer_p_s1_co: 1 events received
+    consumer_p_s2_co: received value {5}
+    consumer_p_s2_co: received value {6}
+    consumer_p_s2_co: 2 events received
+    consumer_p_s5_co: received value {2}
+    consumer_p_s5_co: received value {3}
+    consumer_p_s5_co: received value {4}
+    consumer_p_s5_co: received value {5}
+    consumer_p_s5_co: received value {6}
+    consumer_p_s5_co: 5 events received
+    ---------------------------------------
+    producer_p_p_pro: Sent 0 events.
+    ---------------------------------------
+    ```
\ No newline at end of file