From 3412be80a7df947db2fde7c3cd19937a0855da56 Mon Sep 17 00:00:00 2001 From: Chun Tian Date: Mon, 2 Sep 2024 13:47:11 +1000 Subject: [PATCH] FTBFS examples/dependability --- examples/dependability/AvailabilityScript.sml | 109 ++++++++++-------- .../dependability/case_studies/WSNScript.sml | 20 ++-- .../case_studies/smart_gridScript.sml | 22 ++-- 3 files changed, 79 insertions(+), 72 deletions(-) diff --git a/examples/dependability/AvailabilityScript.sml b/examples/dependability/AvailabilityScript.sml index 3e4db2a205..821b206bc8 100644 --- a/examples/dependability/AvailabilityScript.sml +++ b/examples/dependability/AvailabilityScript.sml @@ -372,10 +372,10 @@ RW_TAC std_ss[] >> DEP_REWRITE_TAC[SEQ_ADD] >> RW_TAC std_ss[] >- (RW_TAC std_ss[SEQ_CONST]) - >- ((`(seq$--> (\t. (FST (m:real#real) / (SND m + FST m)) * exp (-(SND m + FST m) * &t)) 0) = - (seq$--> (\t. + >- ((`((\t. (FST (m:real#real) / (SND m + FST m)) * exp (-(SND m + FST m) * &t)) --> 0) = + ((\t. (\t. FST m / (SND m + FST m)) t * - (\t. exp (-(SND m + FST m) * &t)) t) + (\t. exp (-(SND m + FST m) * &t)) t) --> ((FST m / (SND m + FST m)) *0))` by (RW_TAC real_ss[])) >> POP_ORW >> MATCH_MP_TAC SEQ_MUL @@ -393,8 +393,9 @@ RW_TAC std_ss[] >> POP_ORW >> MATCH_MP_TAC SEQ_ADD >> RW_TAC std_ss[SEQ_CONST] - >> (`(seq$--> (\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) 0) = - (seq$--> (\t. (\t. FST m / (SND m + FST m))t * (\t. exp (-(SND m + FST m) * &t))t) ((FST m / (SND m + FST m)) *0))` + >> (`((\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) --> 0) = + ((\t. (\t. FST m / (SND m + FST m))t * (\t. exp (-(SND m + FST m) * &t))t) --> + ((FST m / (SND m + FST m)) *0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_MUL @@ -406,18 +407,20 @@ RW_TAC std_ss[] >> RW_TAC std_ss[steady_avail_temp]) >> RW_TAC std_ss [expec_avail_def] >> FULL_SIMP_TAC std_ss[inst_avail_exp_def,expec_def] ->> (`(seq$--> (\t. +>> (`((\t. SND m / (SND m + FST m) + - FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) (SND m / (SND m + FST m))) = - (seq$--> (\t. + FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) --> (SND m / (SND m + FST m))) = + ((\t. (\t. SND m / (SND m + FST m)) t + - (\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t))t) ((SND m / (SND m + FST m)) + 0))` by RW_TAC real_ss[]) + (\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t))t) --> + ((SND m / (SND m + FST m)) + 0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_ADD >> RW_TAC std_ss[] >- (RW_TAC std_ss[SEQ_CONST]) ->> (`(seq$--> (\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) 0) = - (seq$--> (\t. (\t. FST m / (SND m + FST m))t * (\t. exp (-(SND m + FST m) * &t))t) ((FST m / (SND m + FST m)) *0))` +>> (`((\t. FST m / (SND m + FST m) * exp (-(SND m + FST m) * &t)) --> 0) = + ((\t. (\t. FST m / (SND m + FST m))t * (\t. exp (-(SND m + FST m) * &t))t) + --> ((FST m / (SND m + FST m)) *0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_MUL @@ -529,21 +532,21 @@ GEN_TAC >> RW_TAC std_ss[] >- (FULL_SIMP_TAC list_ss[inst_avail_exp_list1_def,inst_avail_exp2_def] >> REWRITE_TAC[steady_state_avail_def] - >> (`(seq$--> (\t. + >> (`((\t. SND (h':real#real) / (SND h' + FST h') + - FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) + FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (SND h' / (SND h' + FST h'))) = - (seq$--> (\t. + ((\t. (\t. SND h' / (SND h'+ FST h')) t + - (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) + (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) t) --> (SND h' / (SND h' + FST h') + 0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_ADD >> RW_TAC std_ss[] >- (RW_TAC std_ss[SEQ_CONST]) - >- ((`(seq$--> (\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) 0) = - (seq$--> (\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t) - ((FST h' / (SND h' + FST h')) *0))` by RW_TAC real_ss[]) + >- ((`((\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> 0) = + ((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t) + --> ((FST h' / (SND h' + FST h')) *0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_MUL >> RW_TAC real_ss[SEQ_CONST] @@ -632,19 +635,21 @@ GEN_TAC >> RW_TAC std_ss[SEQ_CONST] >> FULL_SIMP_TAC list_ss[inst_avail_exp_list1_def,inst_avail_exp2_def] >> REWRITE_TAC[steady_state_avail_def] - >> (`(seq$--> (\t. + >> (`((\t. SND (h':real#real) / (SND h' + FST h') + - FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (SND h' / (SND h' + FST h'))) = - (seq$--> (\t. + FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (SND h' / (SND h' + FST h'))) = + ((\t. (\t. SND h' / (SND h'+ FST h')) t + - (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (SND h' / (SND h' + FST h') + 0))` + (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) + --> (SND h' / (SND h' + FST h') + 0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_ADD >> RW_TAC std_ss[] >- (RW_TAC std_ss[SEQ_CONST]) - >- ((`(seq$--> (\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) 0) = - (seq$--> (\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t) ((FST h' / (SND h' + FST h')) *0))` + >- ((`((\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> 0) = + ((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t) + --> ((FST h' / (SND h' + FST h')) *0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_MUL @@ -1119,19 +1124,21 @@ GEN_TAC >> RW_TAC std_ss[] >- (FULL_SIMP_TAC list_ss[inst_unavail_exp_list_def,inst_unavail_exp_def] >> REWRITE_TAC[steady_state_unavail_def] - >> (`(seq$--> (\t. + >> (`((\t. FST (h':real#real) / (SND h' + FST h') - - FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (FST h' / (SND h' + FST h'))) = - (seq$--> (\t. + FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (FST h' / (SND h' + FST h'))) = + ((\t. (\t. FST (h':real#real) / (SND h'+ FST h')) t - - (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (FST h' / (SND h' + FST h') - 0))` + (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) t) + --> (FST h' / (SND h' + FST h') - 0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_SUB >> RW_TAC std_ss[] >- (RW_TAC std_ss[SEQ_CONST]) - >- ((`(seq$--> (\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) 0) = - (seq$--> (\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t) ((FST h' / (SND h' + FST h')) *0))` + >- ((`((\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> 0) = + ((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t) + --> ((FST h' / (SND h' + FST h')) * 0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_MUL @@ -1221,19 +1228,21 @@ GEN_TAC >> RW_TAC std_ss[SEQ_CONST] >> FULL_SIMP_TAC list_ss[inst_unavail_exp_list_def,inst_unavail_exp_def] >> REWRITE_TAC[steady_state_unavail_def] - >> (`(seq$--> (\t. + >> (`((\t. FST (h':real#real) / (SND h' + FST h') - - FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (FST h' / (SND h' + FST h'))) = - (seq$--> (\t. + FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (FST h' / (SND h' + FST h'))) = + ((\t. (\t. FST h' / (SND h'+ FST h')) t - - (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (FST h' / (SND h' + FST h') - 0))` + (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) t) + --> (FST h' / (SND h' + FST h') - 0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_SUB >> RW_TAC std_ss[] >- (RW_TAC std_ss[SEQ_CONST]) - >- ((`(seq$--> (\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) 0) = - (seq$--> (\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t) ((FST h' / (SND h' + FST h')) *0))` + >- ((`((\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> 0) = + ((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t)) t) + --> ((FST h' / (SND h' + FST h')) *0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_MUL @@ -1408,19 +1417,21 @@ GEN_TAC >> POP_ORW >> FULL_SIMP_TAC list_ss[inst_avail_exp_list2_def,inst_avail_exp3_def] >> RW_TAC std_ss[steady_state_avail_def] - >> (`(seq$--> (\t. + >> (`((\t. SND (h':real#real) / (SND h' + FST h') + - FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) (SND h' / (SND h' + FST h'))) = - (seq$--> (\t. + FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> (SND h' / (SND h' + FST h'))) = + ((\t. (\t. SND h' / (SND h'+ FST h')) t + - (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) (SND h' / (SND h' + FST h') + 0))` + (\t. FST h' / (SND h' + FST h') * exp (-(SND h' + FST h') * &t))t) + --> (SND h' / (SND h' + FST h') + 0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_ADD >> RW_TAC std_ss[] >- (RW_TAC std_ss[SEQ_CONST]) - >- ((`(seq$--> (\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) 0) = - (seq$--> (\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t) ((FST h' / (SND h' + FST h')) *0))` + >- ((`((\t. FST h'/ (SND h' + FST h') * exp (-(SND h' + FST h') * &t)) --> 0) = + ((\t. (\t. FST h' / (SND h' + FST h'))t * (\t. exp (-(SND h' + FST h') * &t))t) + --> ((FST h' / (SND h' + FST h')) *0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_MUL @@ -1524,19 +1535,21 @@ Proof RW_TAC std_ss[] >> FULL_SIMP_TAC std_ss[inst_unavail_exp_def] >> RW_TAC std_ss[steady_state_unavail_def] - >> (`(seq$--> (\t. + >> (`((\t. FST (m1:real#real) / (SND m1 + FST m1) - - FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) (FST m1 / (SND m1 + FST m1))) = - (seq$--> (\t. + FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) --> (FST m1 / (SND m1 + FST m1))) = + ((\t. (\t. FST m1 / (SND m1+ FST m1)) t - - (\t. FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t))t) (FST m1 / (SND m1 + FST m1) - 0))` + (\t. FST m1 / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) t) + --> (FST m1 / (SND m1 + FST m1) - 0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_SUB >> RW_TAC std_ss[] >- (RW_TAC std_ss[SEQ_CONST]) - >> (`(seq$--> (\t. FST (m1:real#real) / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) 0) = - (seq$--> (\t. (\t. FST m1 / (SND m1 + FST m1))t * (\t. exp (-(SND m1 + FST m1) * &t))t) ((FST m1 / (SND m1 + FST m1)) *0))` + >> (`((\t. FST (m1:real#real) / (SND m1 + FST m1) * exp (-(SND m1 + FST m1) * &t)) --> 0) = + ((\t. (\t. FST m1 / (SND m1 + FST m1))t * (\t. exp (-(SND m1 + FST m1) * &t)) t) + --> ((FST m1 / (SND m1 + FST m1)) *0))` by RW_TAC real_ss[]) >> POP_ORW >> MATCH_MP_TAC SEQ_MUL diff --git a/examples/dependability/case_studies/WSNScript.sml b/examples/dependability/case_studies/WSNScript.sml index 474995a665..e1a65b6ccd 100644 --- a/examples/dependability/case_studies/WSNScript.sml +++ b/examples/dependability/case_studies/WSNScript.sml @@ -14,23 +14,17 @@ (* *) (* ========================================================================= *) -(*loadPath := "/home/waqar/Downloads/RBD" :: !loadPath;*) - -(*app load ["arithmeticTheory", "realTheory", "prim_recTheory", "seqTheory", - "pred_setTheory","res_quanTheory", "res_quanTools", "listTheory", "real_probabilityTheory", "numTheory", - "transcTheory", "rich_listTheory", "pairTheory", "extra_pred_setTools", - "combinTheory","limTheory","sortingTheory", "realLib", "optionTheory","satTheory", - "util_probTheory", "extrealTheory", "real_measureTheory", "real_lebesgueTheory","real_sigmaTheory", - "dep_rewrite","RBDTheory","FT_deepTheory","VDCTheory","smart_gridTheory","ASN_gatewayTheory"];*) -open HolKernel Parse boolLib bossLib limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory +open HolKernel boolLib bossLib Parse; + +open limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory seqTheory pred_setTheory res_quanTheory sortingTheory res_quanTools listTheory transcTheory rich_listTheory pairTheory combinTheory realLib optionTheory util_probTheory extrealTheory real_measureTheory - real_lebesgueTheory real_sigmaTheory satTheory numTheory dep_rewrite extra_pred_setTools - RBDTheory FT_deepTheory VDCTheory smart_gridTheory ASN_gatewayTheory ; + real_lebesgueTheory real_sigmaTheory satTheory numTheory dep_rewrite extra_pred_setTools; + +open RBDTheory FT_deepTheory VDCTheory smart_gridTheory ASN_gatewayTheory; fun K_TAC _ = ALL_TAC; -open HolKernel boolLib bossLib Parse; val _ = new_theory "WSN"; (*--------------------*) @@ -62,8 +56,10 @@ RW_TAC std_ss[] >> RW_TAC list_ss[] >> RW_TAC list_ss[exp_func_list_def,list_sum_def,list_prod_def] >> RW_TAC real_ss[GSYM transcTheory.EXP_ADD] +>> AP_TERM_TAC >> REAL_ARITH_TAC QED + (*------------------------------------*) Theorem one_minus_exp_equi : !t c. (one_minus_list (exp_func_list c t)) = diff --git a/examples/dependability/case_studies/smart_gridScript.sml b/examples/dependability/case_studies/smart_gridScript.sml index 77f833bef4..6394bca79f 100644 --- a/examples/dependability/case_studies/smart_gridScript.sml +++ b/examples/dependability/case_studies/smart_gridScript.sml @@ -14,20 +14,18 @@ (* *) (* ========================================================================= *) -(*app load ["arithmeticTheory", "realTheory", "prim_recTheory", "seqTheory", - "pred_setTheory","res_quanTheory", "res_quanTools", "listTheory", "real_probabilityTheory", "numTheory", "dep_rewrite", - "transcTheory", "rich_listTheory", "pairTheory", "extra_pred_setTools", - "combinTheory","limTheory","sortingTheory", "realLib", "optionTheory","satTheory", - "util_probTheory", "extrealTheory", "real_measureTheory", "real_lebesgueTheory","real_sigmaTheory", - "RBDTheory","FT_deepTheory","VDCTheory","ASN_gatewayTheory"];*) - -open HolKernel Parse boolLib bossLib limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory +open HolKernel boolLib bossLib Parse; + +open limTheory arithmeticTheory realTheory prim_recTheory real_probabilityTheory seqTheory pred_setTheory res_quanTheory sortingTheory res_quanTools listTheory transcTheory rich_listTheory pairTheory combinTheory realLib optionTheory dep_rewrite extra_pred_setTools - util_probTheory extrealTheory real_measureTheory real_lebesgueTheory real_sigmaTheory satTheory numTheory - RBDTheory FT_deepTheory VDCTheory ASN_gatewayTheory; -open HolKernel boolLib bossLib Parse; + util_probTheory extrealTheory real_measureTheory real_lebesgueTheory real_sigmaTheory + satTheory numTheory; + +open RBDTheory FT_deepTheory VDCTheory ASN_gatewayTheory; + val _ = new_theory "smart_grid"; + (*--------------------*) val op by = BasicProvers.byA; val POP_ORW = POP_ASSUM (fn thm => ONCE_REWRITE_TAC [thm]); @@ -933,7 +931,7 @@ RW_TAC std_ss[] >> `Reliability p ESWs t = exp (-C_ESWs * t)` by RW_TAC std_ss[Reliability_def] >- (FULL_SIMP_TAC real_ss[exp_distribution_def]) >> POP_ORW ->> REAL_ARITH_TAC +>> rw [REAL_NEG_LMUL] QED (*----------------------------------------------*)