1open HolKernel Parse boolLib bossLib;
2
3open pred_setTheory relationTheory pairTheory sumTheory listTheory;
4open prim_recTheory arithmeticTheory combinTheory stringTheory;
5
6open CCSLib CCSTheory CCSSyntax CCSConv;
7open StrongEQTheory StrongEQLib StrongLawsTheory;
8open WeakEQTheory WeakEQLib WeakLawsTheory;
9open ObsCongrTheory ObsCongrLib ObsCongrLawsTheory;
10open CongruenceTheory CoarsestCongrTheory;
11open TraceTheory ExpansionTheory ContractionTheory;
12open BisimulationUptoTheory UniqueSolutionsTheory;
13
14open testutils;
15
16val _ = srw_ss()
17val term_to_string = Portable.with_flag (Globals.linewidth, 3000) term_to_string
18
19fun CCS_TRANS_test (problem, result) = let
20  val padr = StringCvt.padRight #" ";
21  val padl = StringCvt.padLeft #" ";
22  val p_s = padr 30 (term_to_string problem);
23  val r_s = padl 10 (term_to_string result);
24  val _ = tprint (p_s ^ " = " ^ r_s);
25in
26  require_msg (check_result (aconv result o concl o #1))
27              (term_to_string o concl o #1)
28              CCS_TRANS
29              problem
30end;
31
32val CCS_TRANS_tests =
33    [(* test #1 *)
34     (``(restr {name "a"}) (label (name "a")..nil || label (coname "a")..nil)``,
35������u E.
36   �� "a" (In "a"..nil || Out "a"..nil) --u-> E ���
37   (u = ��) ��� (E = �� "a" (nil || nil))���),
38
39     (* test #2 *)
40     (``par (prefix (label (name "a")) nil)
41            (prefix (label (coname "a")) nil)``,
42������u E.
43   In "a"..nil || Out "a"..nil --u-> E ���
44   ((u = In "a") ��� (E = nil || Out "a"..nil) ���
45    (u = Out "a") ��� (E = In "a"..nil || nil)) ���
46   (u = ��) ��� (E = nil || nil)���),
47
48     (* test #3 *)
49     (``par nil nil``,
50������u (E :('a, 'b) CCS). ��(nil || nil --u-> E)���),
51
52     (* test #4 *)
53     (``restr { name "a" } (par nil nil)``,
54������u E. ��(�� "a" (nil || nil) --u-> E)���),
55
56     (* test #5 *)
57     (``label (name "a")..label (name "b")..nil +
58             label (name "b")..label (name "a")..nil``,
59������u E.
60   In "a"..In "b"..nil + In "b"..In "a"..nil --u-> E ���
61   (u = In "a") ��� (E = In "b"..nil) ��� (u = In "b") ��� (E = In "a"..nil)���),
62
63     (* test #6 *)
64     (``(restr {name "a"} (label (name "a")..nil || label (coname "a")..nil)) ||
65                (label (name "a")..nil)``,
66������u E.
67   �� "a" (In "a"..nil || Out "a"..nil) || In "a"..nil --u-> E ���
68   (u = ��) ��� (E = �� "a" (nil || nil) || In "a"..nil) ���
69   (u = In "a") ��� (E = �� "a" (In "a"..nil || Out "a"..nil) || nil)���),
70
71     (* test #7 *)
72     (``rec "VM" (In "coin"..(In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") +
73                              In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))``,
74������u E.
75   rec "VM"
76     (In "coin"
77      ..
78      (In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") +
79       In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))
80   --u->
81   E ���
82   (u = In "coin") ���
83   (E =
84    In "ask-esp"
85    ..
86    rec "VM1"
87      (Out "esp-coffee"
88       ..
89       rec "VM"
90         (In "coin"
91          ..
92          (In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") +
93           In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))) +
94    In "ask-am"
95    ..
96    rec "VM2"
97      (Out "am-coffee"
98       ..
99       rec "VM"
100         (In "coin"
101          ..
102          (In "ask-esp"..rec "VM1" (Out "esp-coffee"..var "VM") +
103           In "ask-am"..rec "VM2" (Out "am-coffee"..var "VM")))))���)];
104
105val _ = List.app CCS_TRANS_test CCS_TRANS_tests;
106
107val _ = Process.exit Process.success;
108