From 36544d14f427abeaa236251a00194b2b36ca58db Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 18 Feb 2010 13:47:44 +0000 Subject: [PATCH] File tidy. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1740 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism/examples/pta/brp/README | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/prism/examples/pta/brp/README b/prism/examples/pta/brp/README index 8bc53aa9..ef87bfc7 100644 --- a/prism/examples/pta/brp/README +++ b/prism/examples/pta/brp/README @@ -4,14 +4,14 @@ Its parameters are: N = number of chunks in a file MAX = maximum number of retransmissions - TD = the transition delay - TIME_OUT = the time the sender waits before timing out - -TIME_OUT should be greater than the time to send and receive an ack (i.e. greater than 2*TD) + TD = the transition delay + TIME_OUT = the time the sender waits before timing out + +TIME_OUT should be greater than the time to send and receive an ack (i.e. greater than 2*TD) For more information, see the untimed version: http://www.prismmodelchecker.org/casestudies/brp.php - -The PTA extension is based on that used in [HH09] + +The PTA extension is based on that used in [HH09] ===================================================================================== @@ -19,8 +19,9 @@ The PTA extension is based on that used in [HH09] L. Helmink, M. Sellink and F Vaandrager Proof checking a data link protocol In Proc. Types for Proofs and Programs (TYPES'93), LNCS 806, pp 127-165, Springer-Verlag, 1994 -[HH09] -A. Hartmanns and H. Hermanns -A Modest Approach to Checking Probabilistic Timed Automata -Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09), IEEE, 2009 - + +[HH09] +A. Hartmanns and H. Hermanns +A Modest Approach to Checking Probabilistic Timed Automata +Proc. 6th International Conference on Quantitative Evaluation of Systems (QEST'09), IEEE, 2009 +