From 3b9f20026d04b28876614e046ad9b572887c441b Mon Sep 17 00:00:00 2001 From: Gethin Norman Date: Mon, 12 Oct 2009 16:09:55 +0000 Subject: [PATCH] firewire git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1531 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/firewire/README | 13 ++++++------- prism-examples/firewire/impl/expected.pctl | 2 +- 2 files changed, 7 insertions(+), 8 deletions(-) diff --git a/prism-examples/firewire/README b/prism-examples/firewire/README index 2c890fda..174578db 100644 --- a/prism-examples/firewire/README +++ b/prism-examples/firewire/README @@ -11,7 +11,7 @@ impl: which consists of the parallel composition of two nodes (Node1 and Node2), 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 [KNS02b]. +For both models we have used the integer semantics given in [KNPS06]. For more information, see: http://www.prismmodelchecker.org/casestudies/firewire.php @@ -22,9 +22,8 @@ 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) - -[KNS02b] -M. Kwiatkowska, G. Norman and J. Sproston -Probabilistic Model Checking of Deadline Properties in the IEEE1394 FireWire Root Contention Protocol -Special Issue of Formal Aspects of Computing, To appear - + +[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 diff --git a/prism-examples/firewire/impl/expected.pctl b/prism-examples/firewire/impl/expected.pctl index cc8914c8..4af88819 100644 --- a/prism-examples/firewire/impl/expected.pctl +++ b/prism-examples/firewire/impl/expected.pctl @@ -1,4 +1,4 @@ // maximum expected time -R{"time"}max=?[F ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)) ] +R{"time"}min=?[F ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)) ] // maximum expected rounds R{"time_sending"}max=?[F ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)) ]