(******************************************************************)
(*                  Probabilistic Analysis of DFTs in IN HOL4     *)
(*                                                                *)
(*                      Copyright 2019, Yassmeen Elderhalli       *)
(*                                                                *)
(*                      Contact: y_elderh@encs.concordia.ca       *)
(*                                                                *)
(******************************************************************)

INSTALLATION:

Requirement: HOL4 "Kananaskis" 12, 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 theories 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.
   - WCSP_sharedScript which is required for the shared spare gate
   -  Q1_shared_spareScript which is required for the shared spare gate
   - CPDFTScript which has the script for the first example
   - AND_FDEPScript which has the script of the second example
   - WSP_ORScript which has the script for the third example 

   - 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) run Holmake to build the theories in the Required-Theories and DFT-Theories directories