diff --git a/assets/diagram-anon.png b/assets/diagram-anon.png
new file mode 100644
index 0000000..59fb989
Binary files /dev/null and b/assets/diagram-anon.png differ
diff --git a/korg-examples/pan b/korg-examples/pan
new file mode 100755
index 0000000..3604504
Binary files /dev/null and b/korg-examples/pan differ
diff --git a/korg-examples/test.pml b/korg-examples/test.pml
new file mode 100644
index 0000000..3d97829
--- /dev/null
+++ b/korg-examples/test.pml
@@ -0,0 +1,12 @@
+chan msgs = [4] of { bit };
+int count = 0;
+
+active [1] proctype Producer() { // one producer
+  do :: atomic { count++; msgs ! 1; } od
+}
+
+active [4] proctype Consumer() { // four consumers
+  do :: atomic { msgs ? 1 -> count--; } od
+}
+
+ltl always_positive { always (count >= 0) }
diff --git a/korg-examples/test.pml.trail b/korg-examples/test.pml.trail
new file mode 100644
index 0000000..6e4f7e2
--- /dev/null
+++ b/korg-examples/test.pml.trail
@@ -0,0 +1,29 @@
+-2:2:-2
+-4:-4:-4
+1:0:18
+2:2:0
+3:0:18
+4:1:0
+5:0:18
+6:2:1
+7:0:18
+8:4:8
+9:0:18
+10:4:9
+11:0:18
+12:2:2
+13:0:18
+14:1:1
+15:0:18
+16:2:0
+17:0:18
+18:4:8
+19:0:18
+20:4:9
+21:0:18
+22:2:1
+23:0:18
+24:4:8
+25:0:18
+26:4:9
+27:0:15