diff --git a/prism-examples/firewire/README.txt b/prism-examples/firewire/README.txt
index 31e1104f..3e7a68d6 100644
--- a/prism-examples/firewire/README.txt
+++ b/prism-examples/firewire/README.txt
@@ -1,29 +1,30 @@
-This case study concerns the Tree Identify Protocol of the IEEE 1394 High Performance Serial Bus (called ``FireWire'').
-
-We consider the following probabilistic timed automata models of the root contention part of the 
-tree identify protocol, which are based on probabilistic I/O automata models presented in [SV99].
-
-impl: which consists of the parallel composition of two nodes (Node1 and Node2),
-      and two communication channels (Wire12 for messages from Node1 to Node2,
-      and Wire21 for messages from Node2 to Node1) and corresponds to the 
-      system Impl of [SV99]. 
-
-abst: which is represented by a single probabilistic timed automaton and is an abstraction of Impl 
-      based on the the probabilistic I/O automaton I1 of [SV99].
-
-For both models we have used the integer semantics given in [KNPS06].
-
-For more information, see: http://www.prismmodelchecker.org/casestudies/firewire.php
-
-=====================================================================================
-
-[SV99]
-M. Stoelinga and F. Vaandrager
-Root Contention in IEEE 1394
-In Proc.  5th AMAST Workshop on Real-Time and Probabilistic Systems (ARTS'99), pp. 53-74, 1999
-(Available as Volume 1601 of LNCS, (c) Springer Verlag)
-
-[KNPS06]
-M. Kwiatkowska, G. Norman, D. Parker and J. Sproston
-Performance Analysis of Probabilistic Timed Automata using Digital Clocks
+This case study concerns the Tree Identify Protocol of the IEEE 1394 High Performance Serial Bus (called ``FireWire'').
+
+These are MDP models, manually constructed from probabilistic timed automaton (PTA) models,
+using the "digital clocks" semantics [KNPS06]. You can also find the PTA models, in the directory ../pta/firewire.
+
+We consider the following probabilistic timed automata models of the root contention part of the 
+tree identify protocol, which are based on probabilistic I/O automata models presented in [SV99].
+
+impl: which consists of the parallel composition of two nodes (Node1 and Node2),
+      and two communication channels (Wire12 for messages from Node1 to Node2,
+      and Wire21 for messages from Node2 to Node1) and corresponds to the 
+      system Impl of [SV99]. 
+
+abst: which is represented by a single probabilistic timed automaton and is an abstraction of Impl 
+      based on the the probabilistic I/O automaton I1 of [SV99].
+
+For more information, see: http://www.prismmodelchecker.org/casestudies/firewire.php
+
+=====================================================================================
+
+[SV99]
+M. Stoelinga and F. Vaandrager
+Root Contention in IEEE 1394
+In Proc.  5th AMAST Workshop on Real-Time and Probabilistic Systems (ARTS'99), pp. 53-74, 1999
+(Available as Volume 1601 of LNCS, (c) Springer Verlag)
+
+[KNPS06]
+M. Kwiatkowska, G. Norman, D. Parker and J. Sproston
+Performance Analysis of Probabilistic Timed Automata using Digital Clocks
 Formal Methods in System Design, 29:33-78, 2006
\ No newline at end of file
diff --git a/prism-examples/pta/firewire/README.txt b/prism-examples/pta/firewire/README.txt
new file mode 100644
index 00000000..c9e9bb51
--- /dev/null
+++ b/prism-examples/pta/firewire/README.txt
@@ -0,0 +1,30 @@
+This case study concerns the Tree Identify Protocol of the IEEE 1394 High Performance Serial Bus (called ``FireWire'').
+
+These are probabilistic timed automaton (PTA) models. You can also find, in the directory ../../firewire,
+manually-created MDP models for this case study, built using the "digital clocks" semantics [KNPS06].
+
+We consider the following probabilistic timed automata models of the root contention part of the 
+tree identify protocol, which are based on probabilistic I/O automata models presented in [SV99].
+
+impl: which consists of the parallel composition of two nodes (Node1 and Node2),
+      and two communication channels (Wire12 for messages from Node1 to Node2,
+      and Wire21 for messages from Node2 to Node1) and corresponds to the 
+      system Impl of [SV99]. 
+
+abst: which is represented by a single probabilistic timed automaton and is an abstraction of Impl 
+      based on the the probabilistic I/O automaton I1 of [SV99].
+
+For more information, see: http://www.prismmodelchecker.org/casestudies/firewire.php
+
+=====================================================================================
+
+[SV99]
+M. Stoelinga and F. Vaandrager
+Root Contention in IEEE 1394
+In Proc.  5th AMAST Workshop on Real-Time and Probabilistic Systems (ARTS'99), pp. 53-74, 1999
+(Available as Volume 1601 of LNCS, (c) Springer Verlag)
+
+[KNPS06]
+M. Kwiatkowska, G. Norman, D. Parker and J. Sproston
+Performance Analysis of Probabilistic Timed Automata using Digital Clocks
+Formal Methods in System Design, 29:33-78, 2006
\ No newline at end of file