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,32 +1,27 @@ section \Build and test exported program with MLton\ theory Complementation_Build imports Complementation_Final begin external_file \code/Autool.mlb\ external_file \code/Prelude.sml\ -external_file \code/Automaton.sml\ external_file \code/Autool.sml\ compile_generated_files \<^marker>\contributor Makarius\ \code/Complementation.ML\ (in Complementation_Final) external_files \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.sml\ and \code/Autool\ (exe) where \fn dir => let val exec = Generated_Files.execute (Path.append dir (Path.basic "code")); 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 \ 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,180 +1,184 @@ section \Final Instantiation of Algorithms Related to Complementation\ theory Complementation_Final imports "Complementation_Implement" + "Formula" "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" 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 (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 (NBA.nodes A)" assumes "(Ai, A) \ \Id, nat_rel\ nbai_nba_rel" 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 - 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 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 + Set.empty Set.insert Set.member + "Inf :: 'a set set \ 'a set" "Sup :: 'a set set \ 'a set" image Pow set nat_of_integer integer_of_nat + Variable Negation Conjunction Disjunction satisfies nbaei alphabetei initialei transitionei acceptingei - nbae_nba_impl complement_impl language_equal_impl + nbae_nba_impl complement_impl language_equal_impl product_impl in SML module_name Complementation file_prefix Complementation end \ No newline at end of file diff --git a/thys/Buchi_Complementation/Formula.thy b/thys/Buchi_Complementation/Formula.thy new file mode 100644 --- /dev/null +++ b/thys/Buchi_Complementation/Formula.thy @@ -0,0 +1,23 @@ +section \Boolean Formulae\ + +theory Formula +imports Main +begin + + datatype 'a formula = + False | + True | + Variable 'a | + Negation "'a formula" | + Conjunction "'a formula" "'a formula" | + Disjunction "'a formula" "'a formula" + + primrec satisfies :: "'a set \ 'a formula \ bool" where + "satisfies A False \ HOL.False" | + "satisfies A True \ HOL.True" | + "satisfies A (Variable a) \ a \ A" | + "satisfies A (Negation x) \ \ satisfies A x" | + "satisfies A (Conjunction x y) \ satisfies A x \ satisfies A y" | + "satisfies A (Disjunction x y) \ satisfies A x \ satisfies A y" + +end \ No newline at end of file diff --git a/thys/Buchi_Complementation/code/Automaton.sml b/thys/Buchi_Complementation/code/Automaton.sml deleted file mode 100644 --- a/thys/Buchi_Complementation/code/Automaton.sml +++ /dev/null @@ -1,5 +0,0 @@ -open Complementation -structure Automaton = struct -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/Autool.mlb b/thys/Buchi_Complementation/code/Autool.mlb --- a/thys/Buchi_Complementation/code/Autool.mlb +++ b/thys/Buchi_Complementation/code/Autool.mlb @@ -1,5 +1,11 @@ $(SML_LIB)/basis/basis.mlb Prelude.sml -Complementation.sml -Automaton.sml +ann + "nonexhaustiveBind ignore" + "nonexhaustiveMatch ignore" + "redundantBind ignore" + "redundantMatch ignore" +in + Complementation.sml +end Autool.sml diff --git a/thys/Buchi_Complementation/code/Autool.sml b/thys/Buchi_Complementation/code/Autool.sml --- a/thys/Buchi_Complementation/code/Autool.sml +++ b/thys/Buchi_Complementation/code/Autool.sml @@ -1,24 +1,234 @@ open Complementation -open Automaton +open String 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) +fun println w = print (w ^ "\n") + +fun return x = [x] +fun bind xs f = concat (map f xs) +fun foldl' y f [] = y + | foldl' y f (x :: xs) = foldl f x xs +fun takeWhile P [] = [] + | takeWhile P (x :: xs) = if P x then x :: takeWhile P xs else [] +fun lookup x [] = NONE | + lookup x ((k, v) :: xs) = if x = k then SOME v else lookup x xs +fun upto k = if k = 0 then [] else (k - 1) :: upto (k - 1) + +fun splitFirst u w = + if w = "" + then if u = "" then SOME ("", "") else NONE + else + if isPrefix u w + then SOME ("", extract (w, size u, NONE)) + else case splitFirst u (extract (w, 1, NONE)) of + NONE => NONE | + SOME (v, w') => SOME (str (sub (w, 0)) ^ v, w') +fun split u w = case splitFirst u w of NONE => [w] | SOME (v, w') => v :: split u w' + +fun showInt k = Int.toString k +fun parseInt w = case Int.fromString w of SOME n => n + +fun showNat k = showInt (integer_of_nat k) +fun parseNat w = nat_of_integer (parseInt w) + +fun showString w = "\"" ^ w ^ "\"" +fun parseString w = substring (w, 1, size w - 2) + +fun showTuple f g (x, y) = "(" ^ f x ^ ", " ^ g y ^ ")" +fun showSequence f xs = concatWith ", " (map f xs) +fun showList f xs = "[" ^ showSequence f xs ^ "]" +fun showSet f (Set xs) = "{" ^ showSequence f xs ^ "}" + | showSet f (Coset xs) = "- {" ^ showSequence f xs ^ "}" + +fun showFormula f False = "f" + | showFormula f True = "t" + | showFormula f (Variable v) = f v + | showFormula f (Negation x) = "!" ^ showFormula f x + | showFormula f (Conjunction (x, y)) = "(" ^ showFormula f x ^ " & " ^ showFormula f y ^ ")" + | showFormula f (Disjunction (x, y)) = "(" ^ showFormula f x ^ " | " ^ showFormula f y ^ ")" +fun parseFormula parseVariable input = let + fun parseConstant w cs = if isPrefix w (implode cs) then [(w, drop (cs, size w))] else [] + fun parseAtom input1 = + bind (parseConstant "f" input1) (fn (_, input2) => + return (False, input2)) + @ + bind (parseConstant "t" input1) (fn (_, input2) => + return (True, input2)) + @ + bind (parseVariable input1) (fn (variable, input2) => + return (Variable variable, input2)) + @ + bind (parseConstant "(" input1) (fn (_, input2) => + bind (parseDisjunction input2) (fn (disjunction, input3) => + bind (parseConstant ")" input3) (fn (_, input4) => + return (disjunction, input4)))) + and parseLiteral input1 = + bind (parseAtom input1) (fn (atom, input2) => + return (atom, input2)) + @ + bind (parseConstant "!" input1) (fn (_, input2) => + bind (parseAtom input2) (fn (atom, input3) => + return (Negation atom, input3))) + and parseConjunction input1 = + bind (parseLiteral input1) (fn (literal, input2) => + return (literal, input2)) + @ + bind (parseLiteral input1) (fn (literal, input2) => + bind (parseConstant "&" input2) (fn (_, input3) => + bind (parseConjunction input3) (fn (conjunction, input4) => + return (Conjunction (literal, conjunction), input4)))) + and parseDisjunction input1 = + bind (parseConjunction input1) (fn (conjunction, input2) => + return (conjunction, input2)) + @ + bind (parseConjunction input1) (fn (conjunction, input2) => + bind (parseConstant "|" input2) (fn (_, input3) => + bind (parseDisjunction input3) (fn (disjunction, input4) => + return (Disjunction (conjunction, disjunction), input4)))) + val input' = filter (not o Char.isSpace) (explode input) + val result = map (fn (exp, _) => exp) (filter (fn (exp, rest) => null rest) (parseDisjunction input')) + in hd result end + +datatype hoaProperty = + HoaVersion of string | + HoaName of string | + HoaProperties of string list | + HoaAtomicPropositions of nat * string list | + HoaAcceptanceConditionName of string | + HoaAcceptanceCondition of string | + HoaStartState of nat | + HoaStateCount of nat +datatype hoaTransition = HoaTransition of nat formula * nat +datatype hoaState = HoaState of nat * nat list * hoaTransition list +datatype hoaAutomaton = HoaAutomaton of hoaProperty list * hoaState list + +fun showHoaAutomaton (HoaAutomaton (ps, ss)) = let + fun showProperty (HoaVersion w) = "HOA: " ^ w ^ "\n" + | showProperty (HoaName w) = "name: " ^ showString w ^ "\n" + | showProperty (HoaProperties ws) = "properties: " ^ concatWith " " ws ^ "\n" + | showProperty (HoaAtomicPropositions (n, ps)) = "AP: " ^ showNat n ^ " " ^ concatWith " " (map showString ps) ^ "\n" + | showProperty (HoaAcceptanceConditionName w) = "acc-name: " ^ w ^ "\n" + | showProperty (HoaAcceptanceCondition w) = "Acceptance: " ^ w ^ "\n" + | showProperty (HoaStartState p) = "Start: " ^ showNat p ^ "\n" + | showProperty (HoaStateCount n) = "States: " ^ showNat n ^ "\n" + fun showTransition (HoaTransition (a, q)) = "[" ^ showFormula showNat a ^ "]" ^ " " ^ showNat q ^ "\n" + fun showState (HoaState (p, cs, ts)) = "State: " ^ showNat p ^ " " ^ showSet showNat (Set cs) ^ "\n" ^ String.concat (map showTransition ts) + in String.concat (map showProperty ps) ^ "--BODY--" ^ "\n" ^ String.concat (map showState ss) ^ "--END--" ^ "\n" end +fun parseHoaAutomaton path = let + fun parseVariable cs = case takeWhile Char.isDigit cs of + [] => [] | xs => [(parseNat (implode xs), drop (cs, length xs))] + fun inputLine input = case TextIO.inputLine input of SOME w => substring (w, 0, size w - 1) + fun parseProperty w = case split ": " w of + ["HOA", u] => HoaVersion u | + ["name", u] => HoaName (substring (u, 1, size u - 2)) | + ["properties", u] => HoaProperties (split " " u) | + ["AP", u] => (case split " " u of v :: vs => HoaAtomicPropositions (parseNat v, map parseString vs)) | + ["acc-name", u] => HoaAcceptanceConditionName u | + ["Acceptance", u] => HoaAcceptanceCondition u | + ["Start", u] => HoaStartState (parseNat u) | + ["States", u] => HoaStateCount (parseNat u) + fun parseProperties input = case inputLine input of w => + if w = "--BODY--" then [] + else parseProperty w :: parseProperties input + fun parseTransition w = case split "] " (substring (w, 1, size w - 1)) of + [u, v] => HoaTransition (parseFormula parseVariable u, parseNat v) + fun parseTransitions input = case inputLine input of w => + if isPrefix "State" w orelse w = "--END--" then ([], w) + else case parseTransitions input of (ts, w') => (parseTransition w :: ts, w') + fun parseStateHeader w = case split " {" w of + [u] => (parseNat u, []) | + [u, "}"] => (parseNat u, []) | + [u, v] => (parseNat u, map parseNat (split ", " (substring (v, 0, size v - 1)))) + fun parseState input w = + case split ": " w of ["State", u] => + case parseStateHeader u of (p, cs) => + case parseTransitions input of (ts, w') => + (HoaState (p, cs, ts), w') + fun parseStates input w = + if w = "--END--" then [] + else case parseState input w of (p, w') => p :: parseStates input w' + val input = TextIO.openIn path + val properties = parseProperties input + val states = parseStates input (inputLine input) + in HoaAutomaton (properties, states) before TextIO.closeIn input end + +fun toNbaei (HoaAutomaton (properties, states)) = let + fun atomicPropositions (HoaAtomicPropositions (_, ps) :: properties) = ps + | atomicPropositions (_ :: properties) = atomicPropositions properties + val aps = atomicPropositions properties + val alphabet = case pow {equal = eq} (image nat_of_integer (Set (upto (length aps)))) of Set pps => pps + fun startStates [] = [] + | startStates (HoaStartState p :: properties) = p :: startStates properties + | startStates (property :: properties) = startStates properties + val initial = startStates properties + fun expandTransition p f q = map (fn P => (p, (P, q))) (filter (fn x => satisfies {equal = eq} x f) alphabet) + fun stateTransitions (HoaState (p, cs, ts)) = concat (map (fn HoaTransition (f, q) => expandTransition p f q) ts) + val transitions = concat (map stateTransitions states) + val accepting = map (fn HoaState (p, cs, ts) => p) (filter (fn HoaState (p, cs, ts) => not (null cs)) states) + in (aps, Nbaei (alphabet, initial, transitions, accepting)) end +fun toHoaAutomaton aps (Nbaei (a, i, t, c)) = let + val Set nodes = sup_seta {equal = eq} + (image (fn (p, (_, q)) => insert {equal = eq} p (insert {equal = eq} q bot_set)) (Set t)); + val properties = + [HoaVersion "v1"] @ + [HoaProperties ["trans-labels", "explicit-labels", "state-acc"]] @ + [HoaAtomicPropositions (nat_of_integer (length aps), aps)] @ + [HoaAcceptanceConditionName "Buchi"] @ + [HoaAcceptanceCondition "1 Inf(0)"] @ + map HoaStartState i @ + [HoaStateCount (nat_of_integer (length nodes))] + fun literal ps ap = if member {equal = eq} ap ps then Variable ap else Negation (Variable ap) + fun formula ps = foldl' True Conjunction (map (literal ps) (map nat_of_integer (upto (length aps)))) + fun transitions p = map (fn (p, (a, q)) => HoaTransition (formula a, q)) (filter (fn (p', (a, q)) => p' = p) t) + fun state p = HoaState (p, if member {equal = eq} p (Set c) then [nat_of_integer 0] else [], transitions p) + val states = map state nodes + in HoaAutomaton (properties, states) end + +fun showNbaei f g (Nbaei (a, i, t, c)) = + showList f a ^ "\n" ^ + showList g i ^ "\n" ^ + showList (showTuple g (showTuple f g)) t ^ "\n" ^ + showList g c ^ "\n" +fun write_automaton f path automaton = let + fun t (p, (a, q)) = Int.toString (integer_of_nat p) ^ " " ^ f a ^ " " ^ Int.toString (integer_of_nat q) ^ "\n" + val output = TextIO.openOut path + fun write [] = () | write (x :: xs) = (TextIO.output (output, t x); write xs) val _ = write (transitionei automaton) - val _ = TextIO.closeOut out -in - () -end + val _ = TextIO.closeOut output + in () end (* 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") + "help" => println "Available Commands: help | complement | equivalence " | + "complement" => let + val (aps, nbaei) = toNbaei (parseHoaAutomaton (nth (parameters, 1))) + val nbai = nbae_nba_impl eq eq nbaei + val complement = toHoaAutomaton aps (complement_impl nbai) + in print (showHoaAutomaton complement) end | + "complement_quick" => let + val (aps, nbaei) = toNbaei (parseHoaAutomaton (nth (parameters, 1))) + val nbai = nbae_nba_impl eq eq nbaei + val complement = complement_impl nbai + in write_automaton (showSet showNat) (nth (parameters, 2)) complement end | + "equivalence" => let + val (aps1, nbaei1) = toNbaei (parseHoaAutomaton (nth (parameters, 1))) + val (aps2, nbaei2) = toNbaei (parseHoaAutomaton (nth (parameters, 2))) + val nbai1 = nbae_nba_impl eq eq nbaei1 + val nbai2 = nbae_nba_impl eq eq nbaei2 + in println (Bool.toString (language_equal_impl {equal = eq} nbai1 nbai2)) end | + "product" => let + val (aps1, nbaei1) = toNbaei (parseHoaAutomaton (nth (parameters, 1))) + val (aps2, nbaei2) = toNbaei (parseHoaAutomaton (nth (parameters, 2))) + val nbai1 = nbae_nba_impl eq eq nbaei1 + val nbai2 = nbae_nba_impl eq eq nbaei2 + val product = product_impl {equal = eq} nbai1 nbai2 + in write_automaton (showSet showNat) (nth (parameters, 3)) product end | + "parse" => let + val ha = parseHoaAutomaton (nth (parameters, 1)) + val (aps, nbaei) = toNbaei ha + val _ = println (showNbaei (showSet showNat) showNat nbaei) + in print (showHoaAutomaton (toHoaAutomaton aps nbaei)) end \ No newline at end of file diff --git a/thys/Buchi_Complementation/code/benchmark.py b/thys/Buchi_Complementation/code/benchmark.py new file mode 100755 --- /dev/null +++ b/thys/Buchi_Complementation/code/benchmark.py @@ -0,0 +1,34 @@ +#!/usr/bin/python + +import sys, random, subprocess + +def write(path, text): + f = open(path, "w") + f.write(text) + f.close() + +def generate_automaton(): + seed = random.randrange(0x10000) + result = subprocess.run(["randaut", "--seed={}".format(seed), "--ba", "--states=20", "a", "b", "c", "d"], stdout = subprocess.PIPE, text = True) + return result.stdout +def generate_formula(): + seed = random.randrange(0x10000) + result = subprocess.run(["randltl", "--seed={}".format(seed), "4"], stdout = subprocess.PIPE, text = True) + return result.stdout +def translate_formula(formula): + result = subprocess.run(["ltl2tgba", "--ba", formula], stdout = subprocess.PIPE, text = True) + return result.stdout + +if sys.argv[1] == "complement_automaton": + write("a.hoa", generate_automaton()) + subprocess.run(["./Autool", "complement_quick", "a.hoa", "c.txt"]) +if sys.argv[1] == "complement_formula": + write("formula.hoa", translate_formula(generate_formula())) + subprocess.run(["./Autool", "complement_quick", "formula.hoa", "formula_complement.txt"]) +# TODO: doesn't work if alphabets aren't equal +if sys.argv[1] == "equivalence": + while True: + write("a.hoa", translate_formula(generate_formula())) + write("b.hoa", translate_formula(generate_formula())) + result = subprocess.run(["./Autool", "equivalence", "a.hoa", "b.hoa"], stdout = subprocess.PIPE, text = True) + if result.stdout == "true": break