1open HolKernel Parse boolLib bossLib; 2 3open modelCheckLib testutils; 4 5(* To run this test, the environment variable HOL4_SMV_EXECUTABLE must be set to 6 the full path of "NuSMV" [1] executation. 7 8 [1] http://nusmv.fbk.eu 9 *) 10 11val ltl1 = ``LTL_SUNTIL (LTL_PROP (P_PROP a), LTL_PROP (P_PROP b))``; 12 13val ltl2 = ``LTL_EVENTUAL (LTL_AND (LTL_PROP (P_PROP b), 14 LTL_PNEXT (LTL_PALWAYS (LTL_PROP (P_PROP a)))))``; 15 16val result1 = ���LTL_EQUIVALENT_INITIAL 17 (LTL_SUNTIL (LTL_PROP (P_PROP a),LTL_PROP (P_PROP b))) 18 (LTL_EVENTUAL 19 (LTL_AND 20 (LTL_PROP (P_PROP b), 21 LTL_PNEXT (LTL_PALWAYS (LTL_PROP (P_PROP a))))))���; 22 23fun modelCheck_test1 () = let 24 val test1 = model_check___ltl_equivalent_initial ltl1 ltl2; 25in 26 if aconv (concl (valOf test1)) result1 then OK () 27 else die ("Got " ^ term_to_string (concl (valOf test1))); 28 Process.system ("rm " ^ (!model_check_temp_file))) 29end; 30 31fun modelCheck_test2 () = let 32 val test2 = model_check___ltl_equivalent ltl1 ltl2; 33in 34 if (isSome test2) then 35 die ("Got " ^ term_to_string (concl (valOf test2))) 36 else OK (); 37 Process.system ("rm " ^ (!model_check_temp_file))) 38end; 39 40val _ = modelCheck_test1 (); 41val _ = modelCheck_test2 (); 42 43val _ = Process.exit Process.success; 44