From c9c0b1176d42804ac9a27c728a03f7bba0957268 Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Wed, 10 Dec 2008 12:40:03 +0000 Subject: [PATCH] Re-tidy csma. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@892 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/csma/.csmaK.pctl.pp | 27 --------------------------- 1 file changed, 27 deletions(-) delete mode 100644 prism-examples/csma/.csmaK.pctl.pp diff --git a/prism-examples/csma/.csmaK.pctl.pp b/prism-examples/csma/.csmaK.pctl.pp deleted file mode 100644 index 910ad94e..00000000 --- a/prism-examples/csma/.csmaK.pctl.pp +++ /dev/null @@ -1,27 +0,0 @@ -#const K# - -// expected time for all messages to be sent -R{"time"}min=?[ F "all_delivered" ] -R{"time"}max=?[ F "all_delivered" ] - -// expected time for one message to be sent -Rmin=?[ F "one_delivered" ] -Rmax=?[ F "one_delivered" ] - -// message of any station eventually delivered before i backoffs -#for i=1:K# -Pmin=?[ F "success_with_backoff_under_#i#" ] -Pmax=?[ F "success_with_backoff_under_#i#" ] -#end# - -// probability all sent successfully before a collision with max backoff -Pmin=?[ !"collision_max_backoff" U "all_delivered" ] -Pmax=?[ !"collision_max_backoff" U "all_delivered" ] - -// probability a station suffers i collisions -#for i=1:K# -Pmin=?[ F "collisions_equal_#i#" ] -Pmax=?[ F "collisions_equal_#i#" ] -#end# - -