From f084aca19213222bef7fa6b29b9103c78d9226b5 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 20 Apr 2007 10:18:41 +0000
Subject: [PATCH] Tidied up embedded example.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@281 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 .../{embedded_prob.csl => embedded.csl}       | 45 ++++++-------------
 prism-examples/embedded/embedded_exptime.csl  | 14 ------
 2 files changed, 13 insertions(+), 46 deletions(-)
 rename prism-examples/embedded/{embedded_prob.csl => embedded.csl} (59%)
 delete mode 100644 prism-examples/embedded/embedded_exptime.csl

diff --git a/prism-examples/embedded/embedded_prob.csl b/prism-examples/embedded/embedded.csl
similarity index 59%
rename from prism-examples/embedded/embedded_prob.csl
rename to prism-examples/embedded/embedded.csl
index 9f69c4fc..ca927fea 100644
--- a/prism-examples/embedded/embedded_prob.csl
+++ b/prism-examples/embedded/embedded.csl
@@ -1,56 +1,37 @@
-// File: /home/staff/dxp/prism/embedded/embedded.csl
-// Generated by PRISM on Tue Oct 12 10:52:02 BST 2004
+const double T;
 
-// Labels:
 label "fail_sensors" = i=2&s<MIN_SENSORS;
 label "fail_actuators" = o=2&a<MIN_ACTUATORS;
 label "fail_io" = count=MAX_COUNT+1;
 label "fail_main" = m=0;
 label "down" = (i=2&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0);
 
-// Constants:
-const double T;
-
-// Properties:
+// Probability of any failure occurring within T hours
+P=? [ true U<=T*3600 "down" ]
 
-// Probability of each failure type occuring first (T hours)
+// Probability of each failure type occurring first (within T hours)
 P=? [ !"down" U<=T*3600 "fail_sensors" ]
-
-// 
 P=? [ !"down" U<=T*3600 "fail_actuators" ]
-
-// 
 P=? [ !"down" U<=T*3600 "fail_io" ]
-
-// 
 P=? [ !"down" U<=T*3600 "fail_main" ]
 
-// Probability of each failure type occuring first (T days)
+// Probability of each failure type occurring first (within T days)
 P=? [ !"down" U<=T*3600*24 "fail_sensors" ]
-
-// 
 P=? [ !"down" U<=T*3600*24 "fail_actuators" ]
-
-// 
 P=? [ !"down" U<=T*3600*24 "fail_io" ]
-
-// 
 P=? [ !"down" U<=T*3600*24 "fail_main" ]
 
-// Probability of each failure type occuring in the long run
-P=? [ !"down" U "fail_sensors" ]
+// Probability of any failure occurring within T days
+P=? [ true U<=T*3600*24 "down" ]
 
-// 
+// Long-run probability of each failure type occurring
+P=? [ !"down" U "fail_sensors" ]
 P=? [ !"down" U "fail_actuators" ]
-
-// 
 P=? [ !"down" U "fail_io" ]
-
-// 
 P=? [ !"down" U "fail_main" ]
 
-// Probability of any failure occuring (T hours)
-P=? [ true U<=T*3600 "down" ]
+// Expected time spent in "up"/"danger"/"shutdown" by time T
+R=? [ C<=T*3600 ]
 
-// Probability of any failure occuring (T days)
-P=? [ true U<=T*3600*24 "down" ]
+// Expected time spent in "up"/"danger" before "shutdown"
+R=? [ F "down" ]
diff --git a/prism-examples/embedded/embedded_exptime.csl b/prism-examples/embedded/embedded_exptime.csl
deleted file mode 100644
index 1d03daec..00000000
--- a/prism-examples/embedded/embedded_exptime.csl
+++ /dev/null
@@ -1,14 +0,0 @@
-// File: /home/staff/dxp/prism/embedded/embedded.csl
-// Generated by PRISM on Tue Oct 12 10:52:02 BST 2004
-
-// Labels:
-label "down" = (i=2&s<MIN_SENSORS)|(count=MAX_COUNT+1)|(o=2&a<MIN_ACTUATORS)|(m=0);
-
-// Constants:
-const double T;
-
-// Expected time spent in "up"/"danger"/"shutdown" by time T
-R=? [ C<=T*3600 ]
-
-// Expected time spent in "up"/"danger" before "shutdown"
-R=? [ F "down" ]