main.ml

   1 (* ========================================================================= *)
   2 (*                                                                           *)
   3 (*                        Top Level File                                     *)
   4 (*                                                                           *)
   5 (*        (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012  *)
   6 (*                       Hardware Verification Group,                        *)
   7 (*                       Concordia University                                *)
   8 (*                                                                           *)
   9 (*     Contact: <muh_sidd@ece.concordia.ca>                                  *)
  10 (*                                                                           *)
  11 (* Last update: July 2014                                                    *)
  12 (*                                                                           *)
  13 (* ========================================================================= *)
  14
  15 (*--------------------------------------------------------------------------*)
  16 (*--------------It will load all the files in the development---------------*)
  17 (*--------------------------------------------------------------------------*)
  18
  19 (*needs "utils.ml";;*)
  20 needs "geometrical_optics.ml";;
  21 needs "component_library.ml";;
  22 needs "resonator.ml";;
  23 needs "z_resonator.ml";;
  24 needs "fp_resonator.ml";;
  25
  26
  27
  28 (*-----------------------------------------------------------------------*)
  29 (*-----------------------TEST--------------------------------------------*)
  30 (*-----------------------------------------------------------------------*)
  31 (*-----------------------------------------------------------------------
  32     Type in
  33
  34  >  RESONATOR_MATRIX
  35
  36     you should get the following output--
  37
  38     |- !n res.
  39          system_composition (unfold_resonator res n) =
  40          system_composition (unfold_resonator res 1) pow n
  41
  42
  43 Moreover, If the last theorem is following:
  44
  45 val ( STABLE_FP ) : thm =
  46   |- !R d n.
  47          ~(R = &0) /\ &0 < d / R /\ d / R < &2 /\ &0 < n /\ &0 < d
  48          ==> is_stable_resonator (fp_cavity R d n)
  49 - : unit = ()
  50
  51 It means everything is loaded correctly :)
  52
  53
  54 NOTE: This development needs "Multivariate" analysis libraries
  55 of HOL Light. It takes 3 hrs :( on my laptop. On my lab server
  56 it takes one hour or so. In any case it take a while to load
  57 depending upon the machine.
  58
  59 --------------------------------------------------------------------------*)
  60
  61