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