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