diff --git a/thys/Buchi_Complementation/Complementation_Build.thy b/thys/Buchi_Complementation/Complementation_Build.thy --- a/thys/Buchi_Complementation/Complementation_Build.thy +++ b/thys/Buchi_Complementation/Complementation_Build.thy @@ -1,34 +1,32 @@ section \Build and test exported program with MLton\ theory Complementation_Build - imports Complementation_Final +imports Complementation_Final begin -external_file \code/Complementation.mlb\ +external_file \code/Autool.mlb\ external_file \code/Prelude.sml\ external_file \code/Automaton.sml\ -external_file \code/Complementation.sml\ +external_file \code/Autool.sml\ compile_generated_files \<^marker>\contributor Makarius\ - \code/Complementation_Export.ML\ (in Complementation_Final) + \code/Complementation.ML\ (in Complementation_Final) external_files - \code/Complementation.mlb\ + \code/Autool.mlb\ \code/Prelude.sml\ \code/Automaton.sml\ + \code/Autool.sml\ + export_files + \code/Autool\ (exe) + and \code/Complementation.sml\ - export_files \code/Complementation\ (exe) and - \code/Complementation_Export.sml\ - \code/Complementation.out\ - \code/mlmon.out\ where \fn dir => let val exec = Generated_Files.execute (Path.append dir (Path.basic "code")); - val _ = - exec \Compilation\ - ("mv Complementation_Export.ML Complementation_Export.sml && " ^ - File.bash_path \<^path>\$ISABELLE_MLTON\ ^ - " -profile time -default-type intinf Complementation.mlb"); - val _ = exec \Test\ "./Complementation Complementation.out"; + val _ = exec \Prepare\ "mv Complementation.ML Complementation.sml"; + val _ = exec \Compilation\ (File.bash_path \<^path>\$ISABELLE_MLTON\ ^ + " -profile time -default-type intinf Autool.mlb"); + val _ = exec \Test\ "./Autool help"; in () end\ -end +end \ No newline at end of file diff --git a/thys/Buchi_Complementation/Complementation_Final.thy b/thys/Buchi_Complementation/Complementation_Final.thy --- a/thys/Buchi_Complementation/Complementation_Final.thy +++ b/thys/Buchi_Complementation/Complementation_Final.thy @@ -1,105 +1,180 @@ -section \Complementation to Explicit Büchi Automaton\ +section \Final Instantiation of Algorithms Related to Complementation\ theory Complementation_Final imports "Complementation_Implement" "Transition_Systems_and_Automata.NBA_Translate" + "Transition_Systems_and_Automata.NGBA_Algorithms" "HOL-Library.Permutation" begin + subsection \Syntax\ + + (* TODO: this syntax has unnecessarily high inner binding strength, requiring extra parentheses + the regular let syntax correctly uses inner binding strength 0: ("(2_ =/ _)" 10) *) + no_syntax "_do_let" :: "[pttrn, 'a] \ do_bind" ("(2let _ =/ _)" [1000, 13] 13) + syntax "_do_let" :: "[pttrn, 'a] \ do_bind" ("(2let _ =/ _)" 13) + + subsection \Hashcodes on Complement States\ + definition "hci k \ uint32_of_nat k * 1103515245 + 12345" definition "hc \ \ (p, q, b). hci p + hci q * 31 + (if b then 1 else 0)" definition "list_hash xs \ fold (bitXOR \ hc) xs 0" lemma list_hash_eq: assumes "distinct xs" "distinct ys" "set xs = set ys" shows "list_hash xs = list_hash ys" proof - have "remdups xs <~~> remdups ys" using eq_set_perm_remdups assms(3) by this then have "xs <~~> ys" using assms(1, 2) by (simp add: distinct_remdups_id) then have "fold (bitXOR \ hc) xs a = fold (bitXOR \ hc) ys a" for a proof (induct arbitrary: a) case (swap y x l) have "x XOR y XOR a = y XOR x XOR a" for x y by (transfer) (simp add: word_bw_lcs(3)) then show ?case by simp qed simp+ then show ?thesis unfolding list_hash_def by this qed definition state_hash :: "nat \ Complementation_Implement.state \ nat" where "state_hash n p \ nat_of_hashcode (list_hash p) mod n" - (* there should be a simpler way to prove this (and others) from some "state_hash is a - valid hash function lemma *) lemma state_hash_bounded_hashcode[autoref_ga_rules]: "is_bounded_hashcode state_rel (gen_equals (Gen_Map.gen_ball (foldli \ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (\))) state_hash" proof show [param]: "(gen_equals (Gen_Map.gen_ball (foldli \ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (\)), (=)) \ state_rel \ state_rel \ bool_rel" by autoref show "state_hash n xs = state_hash n ys" if "xs \ Domain state_rel" "ys \ Domain state_rel" "gen_equals (Gen_Map.gen_ball (foldli \ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (=)) xs ys" for xs ys n proof - have 1: "distinct (map fst xs)" "distinct (map fst ys)" using that(1, 2) unfolding list_map_rel_def list_map_invar_def by (auto simp: in_br_conv) have 2: "distinct xs" "distinct ys" using 1 by (auto intro: distinct_mapI) have 3: "(xs, map_of xs) \ state_rel" "(ys, map_of ys) \ state_rel" using 1 unfolding list_map_rel_def list_map_invar_def by (auto simp: in_br_conv) have 4: "(gen_equals (Gen_Map.gen_ball (foldli \ list_map_to_list)) (list_map_lookup (=)) (prod_eq (=) (\)) xs ys, map_of xs = map_of ys) \ bool_rel" using 3 by parametricity have 5: "map_to_set (map_of xs) = map_to_set (map_of ys)" using that(3) 4 by simp have 6: "set xs = set ys" using map_to_set_map_of 1 5 by blast show "state_hash n xs = state_hash n ys" unfolding state_hash_def using list_hash_eq 2 6 by metis qed show "state_hash n x < n" if "1 < n" for n x using that unfolding state_hash_def by simp qed + subsection \Complementation\ + schematic_goal complement_impl: - assumes [simp]: "finite (nodes A)" + assumes [simp]: "finite (NBA.nodes A)" assumes [autoref_rules]: "(Ai, A) \ \Id, nat_rel\ nbai_nba_rel" shows "(?f :: ?'c, op_translate (complement_4 A)) \ ?R" by (autoref_monadic (plain)) concrete_definition complement_impl uses complement_impl theorem complement_impl_correct: - assumes "finite (nodes A)" + assumes "finite (NBA.nodes A)" assumes "(Ai, A) \ \Id, nat_rel\ nbai_nba_rel" - shows "language (nbae_nba (nbaei_nbae (complement_impl Ai))) = streams (alphabet A) - language A" + shows "NBA.language (nbae_nba (nbaei_nbae (complement_impl Ai))) = + streams (nba.alphabet A) - NBA.language A" + using op_translate_language[OF complement_impl.refine[OF assms]] + using complement_4_correct[OF assms(1)] + by simp + + subsection \Language Subset\ + + definition [simp]: "op_language_subset A B \ NBA.language A \ NBA.language B" + + lemmas [autoref_op_pat] = op_language_subset_def[symmetric] + + (* TODO: maybe we can implement emptiness check on NGBAs and skip degeneralization step *) + schematic_goal language_subset_impl: + assumes [simp]: "finite (NBA.nodes B)" + assumes [autoref_rules]: "(Ai, A) \ \Id, nat_rel\ nbai_nba_rel" + assumes [autoref_rules]: "(Bi, B) \ \Id, nat_rel\ nbai_nba_rel" + shows "(?f :: ?'c, do { + let AB' = intersect A (complement_4 B); + ASSERT (finite (NBA.nodes AB')); + RETURN (NBA.language AB' = {}) + }) \ ?R" + by (autoref_monadic (plain)) + concrete_definition language_subset_impl uses language_subset_impl + lemma language_subset_impl_refine[autoref_rules]: + assumes "SIDE_PRECOND (finite (NBA.nodes A))" + assumes "SIDE_PRECOND (finite (NBA.nodes B))" + assumes "SIDE_PRECOND (nba.alphabet A \ nba.alphabet B)" + assumes "(Ai, A) \ \Id, nat_rel\ nbai_nba_rel" + assumes "(Bi, B) \ \Id, nat_rel\ nbai_nba_rel" + shows "(language_subset_impl Ai Bi, (OP op_language_subset ::: + \Id, nat_rel\ nbai_nba_rel \ \Id, nat_rel\ nbai_nba_rel \ bool_rel) $ A $ B) \ bool_rel" proof - - (* TODO: can we leave all this inside the nres without explicit obtain? *) - (* TODO: or at least avoid unfolding op_translate and reasoning about injectivity? *) - obtain f where 1: - "(complement_impl Ai, nba_nbae (nba_image f (complement_4 A))) \ \Id, nat_rel\ nbaei_nbae_rel" - "inj_on f (nodes (complement_4 A))" - using complement_impl.refine[OF assms, unfolded in_nres_rel_iff op_translate_def, THEN RETURN_ref_SPECD] - by metis - let ?C = "nba_image f (complement_4 A)" - have "(nbae_nba (nbaei_nbae (complement_impl Ai)), nbae_nba (id (nba_nbae ?C))) \ \Id, nat_rel\ nba_rel" - using 1(1) by parametricity auto - also have "nbae_nba (id (nba_nbae ?C)) = (nbae_nba \ nba_nbae) ?C" by simp - also have "(\, id ?C) \ \Id_on (alphabet ?C), Id_on (nodes ?C)\ nba_rel" by parametricity - finally have 2: "(nbae_nba (nbaei_nbae (complement_impl Ai)), ?C) \ - \Id_on (alphabet ?C), Id_on (nodes ?C)\ nba_rel" by simp - have "(language (nbae_nba (nbaei_nbae (complement_impl Ai))), language ?C) \ - \\Id_on (alphabet ?C)\ stream_rel\ set_rel" - using 2 by parametricity - also have "language ?C = language (complement_4 A)" using 1(2) by simp - also have "language (complement_4 A) = streams (alphabet A) - language A" - using complement_4_correct assms(1) by this - finally show ?thesis by simp + have "(RETURN (language_subset_impl Ai Bi), do { + let AB' = intersect A (complement_4 B); + ASSERT (finite (NBA.nodes AB')); + RETURN (NBA.language AB' = {}) + }) \ \bool_rel\ nres_rel" + using language_subset_impl.refine assms(2, 4, 5) unfolding autoref_tag_defs by this + also have "(do { + let AB' = intersect A (complement_4 B); + ASSERT (finite (NBA.nodes AB')); + RETURN (NBA.language AB' = {}) + }, RETURN (NBA.language A \ NBA.language B)) \ \bool_rel\ nres_rel" + proof refine_vcg + show "finite (NBA.nodes (intersect A (complement_4 B)))" using assms(1, 2) by auto + have 1: "NBA.language A \ streams (nba.alphabet B)" + using nba.language_alphabet streams_mono2 assms(3) unfolding autoref_tag_defs by blast + have 2: "NBA.language (complement_4 B) = streams (nba.alphabet B) - NBA.language B" + using complement_4_correct assms(2) by auto + show "(NBA.language (intersect A (complement_4 B)) = {}, + NBA.language A \ NBA.language B) \ bool_rel" using 1 2 by auto + qed + finally show ?thesis using RETURN_nres_relD unfolding nres_rel_comp by force qed - definition nbaei_nbai :: "(String.literal, nat) nbaei \ (String.literal, nat) nbai" where - "nbaei_nbai \ nbae_nba_impl (=) (=)" + subsection \Language Equality\ + + definition [simp]: "op_language_equal A B \ NBA.language A = NBA.language B" + + lemmas [autoref_op_pat] = op_language_equal_def[symmetric] + + schematic_goal language_equal_impl: + assumes [simp]: "finite (NBA.nodes A)" + assumes [simp]: "finite (NBA.nodes B)" + assumes [simp]: "nba.alphabet A = nba.alphabet B" + assumes [autoref_rules]: "(Ai, A) \ \Id, nat_rel\ nbai_nba_rel" + assumes [autoref_rules]: "(Bi, B) \ \Id, nat_rel\ nbai_nba_rel" + shows "(?f :: ?'c, NBA.language A \ NBA.language B \ NBA.language B \ NBA.language A) \ ?R" + by autoref + concrete_definition language_equal_impl uses language_equal_impl + lemma language_equal_impl_refine[autoref_rules]: + assumes "SIDE_PRECOND (finite (NBA.nodes A))" + assumes "SIDE_PRECOND (finite (NBA.nodes B))" + assumes "SIDE_PRECOND (nba.alphabet A = nba.alphabet B)" + assumes "(Ai, A) \ \Id, nat_rel\ nbai_nba_rel" + assumes "(Bi, B) \ \Id, nat_rel\ nbai_nba_rel" + shows "(language_equal_impl Ai Bi, (OP op_language_equal ::: + \Id, nat_rel\ nbai_nba_rel \ \Id, nat_rel\ nbai_nba_rel \ bool_rel) $ A $ B) \ bool_rel" + using language_equal_impl.refine[OF assms[unfolded autoref_tag_defs]] by auto + + schematic_goal product_impl: + assumes [simp]: "finite (NBA.nodes B)" + assumes [autoref_rules]: "(Ai, A) \ \Id, nat_rel\ nbai_nba_rel" + assumes [autoref_rules]: "(Bi, B) \ \Id, nat_rel\ nbai_nba_rel" + shows "(?f :: ?'c, do { + let AB' = intersect A (complement_4 B); + ASSERT (finite (NBA.nodes AB')); + op_translate AB' + }) \ ?R" + by (autoref_monadic (plain)) + concrete_definition product_impl uses product_impl (* TODO: possible optimizations: - introduce op_map_map operation for maps instead of manually iterating via FOREACH - consolidate various binds and maps in expand_map_get_7 *) export_code nat_of_integer integer_of_nat nbaei alphabetei initialei transitionei acceptingei - nbaei_nbai complement_impl - in SML module_name Complementation file_prefix Complementation_Export + nbae_nba_impl complement_impl language_equal_impl + in SML module_name Complementation file_prefix Complementation end \ No newline at end of file diff --git a/thys/Buchi_Complementation/code/Automaton.sml b/thys/Buchi_Complementation/code/Automaton.sml --- a/thys/Buchi_Complementation/code/Automaton.sml +++ b/thys/Buchi_Complementation/code/Automaton.sml @@ -1,4 +1,5 @@ open Complementation structure Automaton = struct -val automaton : (string, nat) nbaei = Nbaei (["a", "b", "c", "d"], [nat_of_integer (0 : IntInf.int)], [(nat_of_integer (0 : IntInf.int), ("a", nat_of_integer (1 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("b", nat_of_integer (2 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("c", nat_of_integer (1 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int))), (nat_of_integer (2 : IntInf.int), ("a", nat_of_integer (2 : IntInf.int))), (nat_of_integer (2 : IntInf.int), ("b", nat_of_integer (2 : IntInf.int))), (nat_of_integer (2 : IntInf.int), ("c", nat_of_integer (2 : IntInf.int))), (nat_of_integer (2 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("a", nat_of_integer (3 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("b", nat_of_integer (3 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("c", nat_of_integer (3 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("d", nat_of_integer (3 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("c", nat_of_integer (4 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("d", nat_of_integer (4 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("a", nat_of_integer (3 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("b", nat_of_integer (3 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("c", nat_of_integer (4 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("d", nat_of_integer (4 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("a", nat_of_integer (3 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("b", nat_of_integer (3 : IntInf.int)))], [nat_of_integer (1 : IntInf.int), nat_of_integer (2 : IntInf.int), nat_of_integer (3 : IntInf.int)]) +val automaton1 : (string, nat) nbaei = Nbaei (["a", "b", "c", "d"], [nat_of_integer (0 : IntInf.int)], [(nat_of_integer (0 : IntInf.int), ("a", nat_of_integer (1 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("b", nat_of_integer (2 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("c", nat_of_integer (3 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("c", nat_of_integer (4 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("a", nat_of_integer (4 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("b", nat_of_integer (2 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("c", nat_of_integer (4 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("a", nat_of_integer (1 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("b", nat_of_integer (2 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("c", nat_of_integer (3 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("c", nat_of_integer (4 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int))), (nat_of_integer (2 : IntInf.int), ("c", nat_of_integer (1 : IntInf.int))), (nat_of_integer (2 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("a", nat_of_integer (1 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("b", nat_of_integer (2 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("c", nat_of_integer (1 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int)))], [nat_of_integer (1 : IntInf.int), nat_of_integer (2 : IntInf.int), nat_of_integer (3 : IntInf.int), nat_of_integer (4 : IntInf.int)]) +val automaton2 : (string, nat) nbaei = Nbaei (["a", "b", "c", "d"], [nat_of_integer (0 : IntInf.int)], [(nat_of_integer (0 : IntInf.int), ("a", nat_of_integer (1 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("b", nat_of_integer (2 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("c", nat_of_integer (3 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("c", nat_of_integer (4 : IntInf.int))), (nat_of_integer (0 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("a", nat_of_integer (4 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("b", nat_of_integer (2 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("c", nat_of_integer (4 : IntInf.int))), (nat_of_integer (4 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("a", nat_of_integer (1 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("b", nat_of_integer (2 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("c", nat_of_integer (3 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("c", nat_of_integer (4 : IntInf.int))), (nat_of_integer (3 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int))), (nat_of_integer (2 : IntInf.int), ("c", nat_of_integer (1 : IntInf.int))), (nat_of_integer (2 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("a", nat_of_integer (1 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("b", nat_of_integer (2 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("c", nat_of_integer (1 : IntInf.int))), (nat_of_integer (1 : IntInf.int), ("d", nat_of_integer (2 : IntInf.int)))], [nat_of_integer (1 : IntInf.int), nat_of_integer (2 : IntInf.int), nat_of_integer (3 : IntInf.int), nat_of_integer (4 : IntInf.int)]) end diff --git a/thys/Buchi_Complementation/code/Complementation.mlb b/thys/Buchi_Complementation/code/Autool.mlb rename from thys/Buchi_Complementation/code/Complementation.mlb rename to thys/Buchi_Complementation/code/Autool.mlb --- a/thys/Buchi_Complementation/code/Complementation.mlb +++ b/thys/Buchi_Complementation/code/Autool.mlb @@ -1,5 +1,5 @@ $(SML_LIB)/basis/basis.mlb Prelude.sml -Complementation_Export.sml +Complementation.sml Automaton.sml -Complementation.sml +Autool.sml diff --git a/thys/Buchi_Complementation/code/Complementation.sml b/thys/Buchi_Complementation/code/Autool.sml rename from thys/Buchi_Complementation/code/Complementation.sml rename to thys/Buchi_Complementation/code/Autool.sml --- a/thys/Buchi_Complementation/code/Complementation.sml +++ b/thys/Buchi_Complementation/code/Autool.sml @@ -1,17 +1,24 @@ open Complementation open Automaton +open List + +fun eq x y = (x = y) fun write_automaton path automaton = let fun t (p, (a, q)) = Int.toString (integer_of_nat p) ^ " " ^ a ^ " " ^ Int.toString (integer_of_nat q) ^ "\n" val out = TextIO.openOut path fun write [] = () | write (x :: xs) = (TextIO.output (out, t x); write xs) val _ = write (transitionei automaton) val _ = TextIO.closeOut out in () end -val path = hd (CommandLine.arguments ()) -(* TODO: maybe we want to optimize the representation, nbae_nba_impl includes list lookups *) -val _ = write_automaton path (complement_impl (nbaei_nbai automaton)) +(* TODO: output number of explored states in emptiness check *) + +val parameters = CommandLine.arguments () +val _ = case hd parameters of + "help" => print "Available Commands: help | complement | equivalence \n" | + "complement" => write_automaton (nth (parameters, 1)) (complement_impl (nbae_nba_impl eq eq automaton1)) | + "equivalence" => print (Bool.toString (language_equal_impl {equal = eq} (nbae_nba_impl eq eq automaton1) (nbae_nba_impl eq eq automaton2)) ^ "\n")