(******************************************************************)
(*               Dynamic Dependability Analysis                   *)
(*                using HOL Theorem Proving with                  *)
(*         Application in Multiprocessor Systems                  *)  
(*                                                                *)
(*              Copyright 2019, Yassmeen Elderhalli               *)
(*                                                                *)
(*              Contact: y_elderh@encs.concordia.ca               *)
(*                                                                *)
(******************************************************************)

INSTALLATION:

Requirement: HOL4 "Kananaskis" 12 release, polyml 5.7 

1) Download "Required-Theories.zip"
   This archive contains some required theories including
   - The extreal, measure and probability theories developed by Tarek Mhamdi for extended real datatypes 
   - The lebesgue measure theory and some other theories1 ported (from HOL light and Isablle/HOL) by Mohamed Qasim
   - The PIE_EXTREAL theory developed by Waqar Ahmad

2) Download "DFT-Thoeries.zip"

   This archive contains:
   - integration_before_afterScript.sml which has the Pr (X < Y /\ Y <=t) and Pr (X < Y /\ X <=t)
   - DFT_Gates_def_PROBScript.sml which has the definitions of the gates, their probabilities and the simplification theorems
   - WCSPScript.sml which has the probabilistic behavior for the Warm and Cold spare gates.
   - Holmakefile which is required to include the path for the "Required-Theories"  directory, 
     the path in the file should be changed to point to the path of the "Required-Theories" directory

3) Download "DRBD-Thoeries.zip"

   This archive contains:
   - The "DRBDScript.sml" which has DRBD operators and constructs definitions and verified reliability expressions
 
3) Download "DFT_DRBD-Theory.zip"
   
   This archive contains:
   - The "DFT_DRBDScript.sml" which has the equivalence of DFT and DRBD 
 
4) Download "SEN.zip" 
   This archive contains:
   -The "SENScript.sml"  which has the verified dependability analysis of the shuffle-exchange network
   - Holmakefile which is required to include the path for the "Required-Theories", "DFT-Theories"  and "DRBD-Theories" directories, 
     the path in the file should be changed to point to the path of these directories.

5) run Holmake to build the theories in the Required-Theories, DFT-Theories directories, DRBD, DFT_DRBD and SEN theories