diff --git a/examples/CENELEC_50128/mini_odo/mini_odo.thy b/examples/CENELEC_50128/mini_odo/mini_odo.thy index 1db0044..532cca6 100644 --- a/examples/CENELEC_50128/mini_odo/mini_odo.thy +++ b/examples/CENELEC_50128/mini_odo/mini_odo.thy @@ -222,7 +222,11 @@ text\ type_synonym distance_function = "real[s] \ real[m]" consts Speed::"distance_function \ real[s] \ real[m\s\<^sup>-\<^sup>1]" consts Accel::"distance_function \ real[s] \ real[m\s\<^sup>-\<^sup>2]" -definition "kilohertz = kilo *\<^sub>Q hertz" +consts Speed\<^sub>M\<^sub>a\<^sub>x::"real[m\s\<^sup>-\<^sup>1]" + +(* Non - SI conform common abrbreviations *) +definition "kmh \ kilo *\<^sub>Q metre \<^bold>/ hour :: real[m\s\<^sup>-\<^sup>1]" +definition "kHz \ kilo *\<^sub>Q hertz :: real[s\<^sup>-\<^sup>1]" (*>*) text\ @@ -290,13 +294,13 @@ and the global model parameters such as wheel diameter, the number of teeth per sampling frequency etc., we can infer the maximal time of service as well the maximum distance the device can measure. As an example configuration, choosing: - \<^item> \<^term>\(1 *\<^sub>Q metre)::real[m]\ for \<^term>\w\<^sub>d\, - \<^item> \<^term>\100 :: real\ for \<^term>\tpw\, - \<^item> \<^term>\80 *\<^sub>Q kilo *\<^sub>Q metre \<^bold>/ hour :: real[m\s\<^sup>-\<^sup>1] \ for \<^term>\Speed\<^sub>M\<^sub>a\<^sub>x\, - \<^item> \<^term>\14.4 *\<^sub>Q kilo *\<^sub>Q hertz\ for the sampling frequency, + \<^item> \<^term>\(1 *\<^sub>Q metre)::real[m]\ for \<^term>\w\<^sub>d\ (wheel-diameter), + \<^item> \<^term>\100 :: real\ for \<^term>\tpw\ (teeth per wheel), + \<^item> \<^term>\80 *\<^sub>Q kmh :: real[m\s\<^sup>-\<^sup>1]\ for \<^term>\Speed\<^sub>M\<^sub>a\<^sub>x\, + \<^item> \<^term>\14.4 *\<^sub>Q kHz :: real[s\<^sup>-\<^sup>1]\ for the sampling frequency, results in an odometer resolution of \<^term>\2.3 *\<^sub>Q milli *\<^sub>Q metre\, a maximum distance of -\<^term>\9878*\<^sub>Q kilo *\<^sub>Q metre\, and a maximal system up-time of \<^term>\123.4 *\<^sub>Q hour\s. +\<^term>\9878 *\<^sub>Q kilo *\<^sub>Q metre\, and a maximal system up-time of \<^term>\123.4 *\<^sub>Q hour\s. The required precision of an odometer can be defined by a constant describing the maximally allowed difference between \df(n*\t)\ and \sampling df init\<^sub>p\<^sub>o\<^sub>s \t n\ for all \init\<^sub>p\<^sub>o\<^sub>s \{0..5}\.