1 (* ========================================================================= *)
5 (* (c) Copyright, Muhammad Umair Siddique, Vincent Aravantinos, 2012 *)
6 (* Hardware Verification Group, *)
7 (* Concordia University *)
9 (* Contact: <muh_sidd@ece.concordia.ca> *)
11 (* Last update: July 2014 *)
13 (* ========================================================================= *)
15 (*--------------------------------------------------------------------------*)
16 (*--------------It will load all the files in the development---------------*)
17 (*--------------------------------------------------------------------------*)
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";;
28 (*-----------------------------------------------------------------------*)
29 (*-----------------------TEST--------------------------------------------*)
30 (*-----------------------------------------------------------------------*)
31 (*-----------------------------------------------------------------------
36 you should get the following output--
39 system_composition (unfold_resonator res n) =
40 system_composition (unfold_resonator res 1) pow n
43 Moreover, If the last theorem is following:
45 val ( STABLE_FP ) : thm =
47 ~(R = &0) /\ &0 < d / R /\ d / R < &2 /\ &0 < n /\ &0 < d
48 ==> is_stable_resonator (fp_cavity R d n)
51 It means everything is loaded correctly :)
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.
59 --------------------------------------------------------------------------*)