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,184 +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 + Variable Negation Conjunction Disjunction satisfies map_formula nbaei alphabetei initialei transitionei acceptingei 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/Ranking.thy b/thys/Buchi_Complementation/Ranking.thy --- a/thys/Buchi_Complementation/Ranking.thy +++ b/thys/Buchi_Complementation/Ranking.thy @@ -1,480 +1,480 @@ section \Rankings\ theory Ranking imports "Alternate" "Graph" begin subsection \Rankings\ type_synonym 'state ranking = "'state node \ nat" definition ranking :: "('label, 'state) nba \ 'label stream \ 'state ranking \ bool" where "ranking A w f \ (\ v \ gunodes A w. f v \ 2 * card (nodes A)) \ (\ v \ gunodes A w. \ u \ gusuccessors A w v. f u \ f v) \ (\ v \ gunodes A w. gaccepting A v \ even (f v)) \ (\ v \ gunodes A w. \ r k. gurun A w r v \ smap f (gtrace r v) = sconst k \ odd k)" subsection \Ranking Implies Word not in Language\ lemma ranking_stuck: assumes "ranking A w f" assumes "v \ gunodes A w" "gurun A w r v" obtains n k where "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k" proof - have 0: "f u \ f v" if "v \ gunodes A w" "u \ gusuccessors A w v" for v u using assms(1) that unfolding ranking_def by auto have 1: "shd (v ## gtrace r v) \ gunodes A w" using assms(2) by auto have 2: "sdescending (smap f (v ## gtrace r v))" using 1 assms(3) proof (coinduction arbitrary: r v rule: sdescending.coinduct) case sdescending obtain u s where 1: "r = u ## s" using stream.exhaust by blast have 2: "v \ gunodes A w" using sdescending(1) by simp have 3: "gurun A w (u ## s) v" using sdescending(2) 1 by auto have 4: "u \ gusuccessors A w v" using 3 by auto have 5: "u \ gureachable A w v" using graph.reachable_successors 4 by blast show ?case unfolding 1 proof (intro exI conjI disjI1) show "f u \ f v" using 0 2 4 by this show "shd (u ## gtrace s u) \ gunodes A w" using 2 5 by auto show "gurun A w s u" using 3 by auto qed auto qed obtain n k where 3: "sdrop n (smap f (v ## gtrace r v)) = sconst k" using sdescending_stuck[OF 2] by metis have "gtrace (sdrop (Suc n) r) (gtarget (stake (Suc n) r) v) = sdrop (Suc n) (gtrace r v)" using sscan_sdrop by rule also have "smap f \ = sdrop n (smap f (v ## gtrace r v))" by (auto, metis 3 id_apply sdrop_smap sdrop_stl siterate.simps(2) sscan_const stream.map stream.map_sel(2) stream.sel(2)) also have "\ = sconst k" using 3 by this finally show ?thesis using that by blast qed lemma ranking_stuck_odd: assumes "ranking A w f" assumes "v \ gunodes A w" "gurun A w r v" obtains n where "sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v))) \ Collect odd" proof - obtain n k where 1: "smap f (gtrace (sdrop n r) (gtarget (stake n r) v)) = sconst k" using ranking_stuck assms by this have 2: "gtarget (stake n r) v \ gunodes A w" using assms(2, 3) by (simp add: graph.nodes_target graph.run_stake) have 3: "gurun A w (sdrop n r) (gtarget (stake n r) v)" using assms(2, 3) by (simp add: graph.run_sdrop) have 4: "odd k" using 1 2 3 assms(1) unfolding ranking_def by meson have "sset (smap f (gtrace (sdrop n r) (gtarget (stake n r) v))) = sset (sconst k)" unfolding 1 by rule also have "\ \ Collect odd" using 4 by simp finally show ?thesis using that by simp qed lemma ranking_language: assumes "ranking A w f" shows "w \ language A" proof assume 1: "w \ language A" obtain r p where 2: "run A (w ||| r) p" "p \ initial A" "infs (accepting A) (p ## r)" using 1 by rule let ?r = "fromN 1 ||| r" let ?v = "(0, p)" have 3: "?v \ gunodes A w" "gurun A w ?r ?v" using 2(1, 2) by (auto intro: run_grun) obtain n where 4: "sset (smap f (gtrace (sdrop n ?r) (gtarget (stake n ?r) ?v))) \ {a. odd a}" using ranking_stuck_odd assms 3 by this let ?s = "stake n ?r" let ?t = "sdrop n ?r" let ?u = "gtarget ?s ?v" have "sset (gtrace ?t ?u) \ gureachable A w ?v" proof (intro graph.reachable_trace graph.reachable_target graph.reachable.reflexive) show "gupath A w ?s ?v" using graph.run_stake 3(2) by this show "gurun A w ?t ?u" using graph.run_sdrop 3(2) by this qed also have "\ \ gunodes A w" using 3(1) by blast finally have 7: "sset (gtrace ?t ?u) \ gunodes A w" by this have 8: "\ p. p \ gunodes A w \ gaccepting A p \ even (f p)" using assms unfolding ranking_def by auto have 9: "\ p. p \ sset (gtrace ?t ?u) \ gaccepting A p \ even (f p)" using 7 8 by auto have 19: "infs (accepting A) (smap snd ?r)" using 2(3) by simp have 18: "infs (gaccepting A) ?r" using 19 by simp have 17: "infs (gaccepting A) (gtrace ?r ?v)" using 18 unfolding gtrace_alt_def by this have 16: "infs (gaccepting A) (gtrace (?s @- ?t) ?v)" using 17 unfolding stake_sdrop by this have 15: "infs (gaccepting A) (gtrace ?t ?u)" using 16 by simp have 13: "infs (even \ f) (gtrace ?t ?u)" using infs_mono[OF _ 15] 9 by simp have 12: "infs even (smap f (gtrace ?t ?u))" using 13 by (simp add: comp_def) have 11: "Bex (sset (smap f (gtrace ?t ?u))) even" using 12 infs_any by metis show False using 4 11 by auto qed subsection \Word not in Language implies Ranking\ subsubsection \Removal of Endangered Nodes\ definition clean :: "('label, 'state) nba \ 'label stream \ 'state node set \ 'state node set" where "clean A w V \ {v \ V. infinite (greachable A w V v)}" lemma clean_decreasing: "clean A w V \ V" unfolding clean_def by auto lemma clean_successors: assumes "v \ V" "u \ gusuccessors A w v" shows "u \ clean A w V \ v \ clean A w V" proof - assume 1: "u \ clean A w V" have 2: "u \ V" "infinite (greachable A w V u)" using 1 unfolding clean_def by auto have 3: "u \ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast have 4: "greachable A w V u \ greachable A w V v" using 3 by blast have 5: "infinite (greachable A w V v)" using 2(2) 4 by (simp add: infinite_super) show "v \ clean A w V" unfolding clean_def using assms(1) 5 by simp qed subsubsection \Removal of Safe Nodes\ definition prune :: "('label, 'state) nba \ 'label stream \ 'state node set \ 'state node set" where "prune A w V \ {v \ V. \ u \ greachable A w V v. gaccepting A u}" lemma prune_decreasing: "prune A w V \ V" unfolding prune_def by auto lemma prune_successors: assumes "v \ V" "u \ gusuccessors A w v" shows "u \ prune A w V \ v \ prune A w V" proof - assume 1: "u \ prune A w V" have 2: "u \ V" "\ x \ greachable A w V u. gaccepting A x" using 1 unfolding prune_def by auto have 3: "u \ greachable A w V v" using graph.reachable.execute assms(2) 2(1) by blast have 4: "greachable A w V u \ greachable A w V v" using 3 by blast show "v \ prune A w V" unfolding prune_def using assms(1) 2(2) 4 by auto qed subsubsection \Run Graph Interation\ definition graph :: "('label, 'state) nba \ 'label stream \ nat \ 'state node set" where "graph A w k \ alternate (clean A w) (prune A w) k (gunodes A w)" abbreviation "level A w k l \ {v \ graph A w k. fst v = l}" lemma graph_0[simp]: "graph A w 0 = gunodes A w" unfolding graph_def by simp lemma graph_Suc[simp]: "graph A w (Suc k) = (if even k then clean A w else prune A w) (graph A w k)" unfolding graph_def by simp lemma graph_antimono: "antimono (graph A w)" using alternate_antimono clean_decreasing prune_decreasing unfolding antimono_def le_fun_def graph_def by metis lemma graph_nodes: "graph A w k \ gunodes A w" using graph_0 graph_antimono le0 antimonoD by metis lemma graph_successors: assumes "v \ gunodes A w" "u \ gusuccessors A w v" shows "u \ graph A w k \ v \ graph A w k" using assms proof (induct k arbitrary: u v) case 0 show ?case using 0(2) by simp next case (Suc k) have 1: "v \ graph A w k" using Suc using antimono_iff_le_Suc graph_antimono rev_subsetD by blast show ?case using Suc(2) clean_successors[OF 1 Suc(4)] prune_successors[OF 1 Suc(4)] by auto qed lemma graph_level_finite: assumes "finite (nodes A)" shows "finite (level A w k l)" proof - have "level A w k l \ {v \ gunodes A w. fst v = l}" by (simp add: graph_nodes subset_CollectI) also have "{v \ gunodes A w. fst v = l} \ {l} \ nodes A" using gnodes_nodes by force also have "finite ({l} \ nodes A)" using assms(1) by simp finally show ?thesis by this qed lemma find_safe: assumes "w \ language A" assumes "V \ {}" "V \ gunodes A w" assumes "\ v. v \ V \ gsuccessors A w V v \ {}" obtains v where "v \ V" "\ u \ greachable A w V v. \ gaccepting A u" proof (rule ccontr) assume 1: "\ thesis" have 2: "\ v. v \ V \ \ u \ greachable A w V v. gaccepting A u" using that 1 by auto have 3: "\ r v. v \ initial A \ run A (w ||| r) v \ fins (accepting A) r" using assms(1) by auto obtain v where 4: "v \ V" using assms(2) by force obtain x where 5: "x \ greachable A w V v" "gaccepting A x" using 2 4 by blast obtain y where 50: "gpath A w V y v" "x = gtarget y v" using 5(1) by rule obtain r where 6: "grun A w V r x" "infs (\ x. x \ V \ gaccepting A x) r" proof (rule graph.recurring_condition) show "x \ V \ gaccepting A x" using greachable_subset 4 5 by blast next fix v assume 1: "v \ V \ gaccepting A v" obtain v' where 20: "v' \ gsuccessors A w V v" using assms(4) 1 by (meson IntE equals0I) have 21: "v' \ V" using 20 by auto have 22: "\ u \ greachable A w V v'. u \ V \ gaccepting A u" using greachable_subset 2 21 by blast obtain r where 30: "gpath A w V r v'" "gtarget r v' \ V \ gaccepting A (gtarget r v')" using 22 by blast show "\ r. r \ [] \ gpath A w V r v \ gtarget r v \ V \ gaccepting A (gtarget r v)" proof (intro exI conjI) show "v' # r \ []" by simp show "gpath A w V (v' # r) v" using 20 30 by auto show "gtarget (v' # r) v \ V" using 30 by simp show "gaccepting A (gtarget (v' # r) v)" using 30 by simp qed qed auto obtain u where 100: "u \ ginitial A" "v \ gureachable A w u" using 4 assms(3) by blast have 101: "gupath A w y v" using gpath_subset 50(1) subset_UNIV by this have 102: "gurun A w r x" using grun_subset 6(1) subset_UNIV by this obtain t where 103: "gupath A w t u" "v = gtarget t u" using 100(2) by rule have 104: "gurun A w (t @- y @- r) u" using 101 102 103 50(2) by auto obtain s q where 7: "t @- y @- r = fromN (Suc 0) ||| s" "u = (0, q)" using grun_elim[OF 104] 100(1) by blast have 8: "run A (w ||| s) q" using grun_run[OF 104[unfolded 7]] by simp have 9: "q \ initial A" using 100(1) 7(2) by auto have 91: "sset (trace (w ||| s) q) \ reachable A q" using nba.reachable_trace nba.reachable.reflexive 8 by this have 10: "fins (accepting A) s" using 3 9 8 by this have 12: "infs (gaccepting A) r" using infs_mono[OF _ 6(2)] by simp have "s = smap snd (t @- y @- r)" unfolding 7(1) by simp also have "infs (accepting A) \" using 12 by (simp add: comp_def) finally have 13: "infs (accepting A) s" by this show False using 10 13 by simp qed lemma remove_run: assumes "finite (nodes A)" "w \ language A" assumes "V \ gunodes A w" "clean A w V \ {}" obtains v r where "grun A w V r v" "sset (gtrace r v) \ clean A w V" "sset (gtrace r v) \ - prune A w (clean A w V)" proof - obtain u where 1: "u \ clean A w V" "\ x \ greachable A w (clean A w V) u. \ gaccepting A x" proof (rule find_safe) show "w \ language A" using assms(2) by this show "clean A w V \ {}" using assms(4) by this show "clean A w V \ gunodes A w" using assms(3) by (meson clean_decreasing subset_iff) next fix v assume 1: "v \ clean A w V" have 2: "v \ V" using 1 clean_decreasing by blast have 3: "infinite (greachable A w V v)" using 1 clean_def by auto have "gsuccessors A w V v \ gusuccessors A w v" by auto also have "finite \" using 2 assms(1, 3) finite_nodes_gsuccessors by blast finally have 4: "finite (gsuccessors A w V v)" by this have 5: "infinite (insert v (\((greachable A w V) ` (gsuccessors A w V v))))" using graph.reachable_step 3 by metis obtain u where 6: "u \ gsuccessors A w V v" "infinite (greachable A w V u)" using 4 5 by auto have 7: "u \ clean A w V" using 6 unfolding clean_def by auto show "gsuccessors A w (clean A w V) v \ {}" using 6(1) 7 by auto qed auto have 2: "u \ V" using 1(1) unfolding clean_def by auto have 3: "infinite (greachable A w V u)" using 1(1) unfolding clean_def by simp have 4: "finite (gsuccessors A w V v)" if "v \ greachable A w V u" for v proof - have 1: "v \ V" using that greachable_subset 2 by blast have "gsuccessors A w V v \ gusuccessors A w v" by auto also have "finite \" using 1 assms(1, 3) finite_nodes_gsuccessors by blast finally show ?thesis by this qed obtain r where 5: "grun A w V r u" using graph.koenig[OF 3 4] by this have 6: "greachable A w V u \ V" using 2 greachable_subset by blast have 7: "sset (gtrace r u) \ V" using graph.reachable_trace[OF graph.reachable.reflexive 5(1)] 6 by blast have 8: "sset (gtrace r u) \ clean A w V" unfolding clean_def using 7 infinite_greachable_gtrace[OF 5(1)] by auto have 9: "sset (gtrace r u) \ greachable A w (clean A w V) u" using 5 8 by (metis graph.reachable.reflexive graph.reachable_trace grun_subset) show ?thesis proof show "grun A w V r u" using 5(1) by this show "sset (gtrace r u) \ clean A w V" using 8 by this show "sset (gtrace r u) \ - prune A w (clean A w V)" proof (intro subsetI ComplI) fix p assume 10: "p \ sset (gtrace r u)" "p \ prune A w (clean A w V)" have 20: "\ x \ greachable A w (clean A w V) p. gaccepting A x" using 10(2) unfolding prune_def by auto have 30: "greachable A w (clean A w V) p \ greachable A w (clean A w V) u" using 10(1) 9 by blast show "False" using 1(2) 20 30 by force qed qed qed lemma level_bounded: assumes "finite (nodes A)" "w \ language A" obtains n where "\ l. l \ n \ card (level A w (2 * k) l) \ card (nodes A) - k" proof (induct k arbitrary: thesis) case (0) show ?case proof (rule 0) fix l :: nat have "finite ({l} \ nodes A)" using assms(1) by simp also have "level A w 0 l \ {l} \ nodes A" using gnodes_nodes by force also (card_mono) have "card \ = card (nodes A)" using assms(1) by simp finally show "card (level A w (2 * 0) l) \ card (nodes A) - 0" by simp qed next case (Suc k) show ?case proof (cases "graph A w (Suc (2 * k)) = {}") case True have 3: "graph A w (2 * Suc k) = {}" using True prune_decreasing by simp blast show ?thesis using Suc(2) 3 by simp next case False obtain v r where 1: "grun A w (graph A w (2 * k)) r v" "sset (gtrace r v) \ graph A w (Suc (2 * k))" "sset (gtrace r v) \ - graph A w (Suc (Suc (2 * k)))" proof (rule remove_run) show "finite (nodes A)" "w \ language A" using assms by this show "clean A w (graph A w (2 * k)) \ {}" using False by simp show "graph A w (2 * k) \ gunodes A w" using graph_nodes by this qed auto obtain l q where 2: "v = (l, q)" by force obtain n where 90: "\ l. n \ l \ card (level A w (2 * k) l) \ card (nodes A) - k" using Suc(1) by blast show ?thesis proof (rule Suc(2)) fix j assume 100: "n + Suc l \ j" have 6: "graph A w (Suc (Suc (2 * k))) \ graph A w (Suc (2 * k))" using graph_antimono antimono_iff_le_Suc by blast have 101: "gtrace r v !! (j - Suc l) \ graph A w (Suc (2 * k))" using 1(2) snth_sset by auto have 102: "gtrace r v !! (j - Suc l) \ graph A w (Suc (Suc (2 * k)))" using 1(3) snth_sset by blast have 103: "gtrace r v !! (j - Suc l) \ level A w (Suc (2 * k)) j" using 1(1) 100 101 2 by (auto elim: grun_elim) have 104: "gtrace r v !! (j - Suc l) \ level A w (Suc (Suc (2 * k))) j" using 100 102 by simp have "level A w (2 * Suc k) j = level A w (Suc (Suc (2 * k))) j" by simp also have "\ \ level A w (Suc (2 * k)) j" using 103 104 6 by blast also have "\ \ level A w (2 * k) j" by (simp add: Collect_mono clean_def) finally have 105: "level A w (2 * Suc k) j \ level A w (2 * k) j" by this have "card (level A w (2 * Suc k) j) < card (level A w (2 * k) j)" using assms(1) 105 by (simp add: graph_level_finite psubset_card_mono) also have "\ \ card (nodes A) - k" using 90 100 by simp finally show "card (level A w (2 * Suc k) j) \ card (nodes A) - Suc k" by simp qed qed qed lemma graph_empty: assumes "finite (nodes A)" "w \ language A" shows "graph A w (Suc (2 * card (nodes A))) = {}" proof - obtain n where 1: "\ l. l \ n \ card (level A w (2 * card (nodes A)) l) = 0" using level_bounded[OF assms(1, 2), of "card (nodes A)"] by auto have "graph A w (2 * card (nodes A)) = (\ l \ {..< n}. level A w (2 * card (nodes A)) l) \ (\ l \ {n ..}. level A w (2 * card (nodes A)) l)" by auto also have "(\ l \ {n ..}. level A w (2 * card (nodes A)) l) = {}" using graph_level_finite assms(1) 1 by fastforce also have "finite ((\ l \ {..< n}. level A w (2 * card (nodes A)) l) \ {})" using graph_level_finite assms(1) by auto finally have 100: "finite (graph A w (2 * card (nodes A)))" by this have 101: "finite (greachable A w (graph A w (2 * card (nodes A))) v)" for v using 100 greachable_subset[of A w "graph A w (2 * card (nodes A))" v] using finite_insert infinite_super by auto show ?thesis using 101 by (simp add: clean_def) qed lemma graph_le: assumes "finite (nodes A)" "w \ language A" assumes "v \ graph A w k" shows "k \ 2 * card (nodes A)" using graph_empty graph_antimono assms by (metis (no_types, lifting) Suc_leI antimono_def basic_trans_rules(30) empty_iff not_le_imp_less) subsection \Node Ranks\ definition rank :: "('label, 'state) nba \ 'label stream \ 'state node \ nat" where "rank A w v \ GREATEST k. v \ graph A w k" lemma rank_member: assumes "finite (nodes A)" "w \ language A" "v \ gunodes A w" shows "v \ graph A w (rank A w v)" unfolding rank_def proof (rule GreatestI_nat) show "v \ graph A w 0" using assms(3) by simp - show "\k. v \ graph A w k \ k \ 2 * card (nodes A)" - using graph_le assms(1, 2) by blast + show "k \ 2 * card (nodes A)" if "v \ graph A w k" for k + using graph_le assms(1, 2) that by blast qed lemma rank_removed: assumes "finite (nodes A)" "w \ language A" shows "v \ graph A w (Suc (rank A w v))" proof assume "v \ graph A w (Suc (rank A w v))" then have 2: "Suc (rank A w v) \ rank A w v" unfolding rank_def using Greatest_le_nat graph_le assms by metis then show "False" by auto qed lemma rank_le: assumes "finite (nodes A)" "w \ language A" assumes "v \ gunodes A w" "u \ gusuccessors A w v" shows "rank A w u \ rank A w v" unfolding rank_def proof (rule Greatest_le_nat) have 1: "u \ gureachable A w v" using graph.reachable_successors assms(4) by blast have 2: "u \ gunodes A w" using assms(3) 1 by auto show "v \ graph A w (GREATEST k. u \ graph A w k)" unfolding rank_def[symmetric] proof (rule graph_successors) show "v \ gunodes A w" using assms(3) by this show "u \ gusuccessors A w v" using assms(4) by this show "u \ graph A w (rank A w u)" using rank_member assms(1, 2) 2 by this qed - show "\k. v \ graph A w k \ k \ 2 * card (nodes A)" - using graph_le assms(1, 2) by blast + show "k \ 2 * card (nodes A)" if "v \ graph A w k" for k + using graph_le assms(1, 2) that by blast qed lemma language_ranking: assumes "finite (nodes A)" "w \ language A" shows "ranking A w (rank A w)" unfolding ranking_def proof (intro conjI ballI allI impI) fix v assume 1: "v \ gunodes A w" have 2: "v \ graph A w (rank A w v)" using rank_member assms 1 by this show "rank A w v \ 2 * card (nodes A)" using graph_le assms 2 by this next fix v u assume 1: "v \ gunodes A w" "u \ gusuccessors A w v" show "rank A w u \ rank A w v" using rank_le assms 1 by this next fix v assume 1: "v \ gunodes A w" "gaccepting A v" have 2: "v \ graph A w (rank A w v)" using rank_member assms 1(1) by this have 3: "v \ graph A w (Suc (rank A w v))" using rank_removed assms by this have 4: "v \ prune A w (graph A w (rank A w v))" using 2 1(2) unfolding prune_def by auto have 5: "graph A w (Suc (rank A w v)) \ prune A w (graph A w (rank A w v))" using 3 4 by blast show "even (rank A w v)" using 5 by auto next fix v r k assume 1: "v \ gunodes A w" "gurun A w r v" "smap (rank A w) (gtrace r v) = sconst k" have "sset (gtrace r v) \ gureachable A w v" using 1(2) by (metis graph.reachable.reflexive graph.reachable_trace) then have 6: "sset (gtrace r v) \ gunodes A w" using 1(1) by blast have 60: "rank A w ` sset (gtrace r v) \ {k}" using 1(3) by (metis equalityD1 sset_sconst stream.set_map) have 50: "sset (gtrace r v) \ graph A w k" using rank_member[OF assms] subsetD[OF 6] 60 unfolding image_subset_iff by auto have 70: "grun A w (graph A w k) r v" using grun_subset 1(2) 50 by this have 7: "sset (gtrace r v) \ clean A w (graph A w k)" unfolding clean_def using 50 infinite_greachable_gtrace[OF 70] by auto have 8: "sset (gtrace r v) \ graph A w (Suc k) = {}" using rank_removed[OF assms] 60 by blast have 9: "sset (gtrace r v) \ {}" using stream.set_sel(1) by auto have 10: "graph A w (Suc k) \ clean A w (graph A w k)" using 7 8 9 by blast show "odd k" using 10 unfolding graph_Suc by auto qed subsection \Correctness Theorem\ theorem language_ranking_iff: assumes "finite (nodes A)" shows "w \ language A \ (\ f. ranking A w f)" using ranking_language language_ranking assms by blast end 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,234 +1,237 @@ open Complementation open String open List fun eq x y = (x = y) 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 + HoaStateCount of nat | + HoaProperty of string * string 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" + | showProperty (HoaProperty (name, value)) = name ^ ": " ^ value ^ "\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) + ["States", u] => HoaStateCount (parseNat u) | + [name, value] => HoaProperty (name, value) 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 + val alphabet = case pow {equal = eq} (Set aps) of Set pps => pps fun startStates [] = [] | startStates (HoaStartState p :: properties) = p :: startStates properties | startStates (property :: properties) = startStates properties val initial = startStates properties + fun mapFormula f = map_formula (fn k => nth (aps, integer_of_nat k)) f 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) + fun stateTransitions (HoaState (p, cs, ts)) = concat (map (fn HoaTransition (f, q) => expandTransition p (mapFormula 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 literal ps k = if member {equal = eq} (nth (aps, k)) ps + then Variable (nat_of_integer k) else Negation (Variable (nat_of_integer k)) + fun formula ps = foldl' True Conjunction (map (literal ps) (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 output in () end -(* TODO: output number of explored states in emptiness check *) - val parameters = CommandLine.arguments () val _ = case hd parameters of "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 | + in write_automaton (showSet showString) (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 | + in write_automaton (showSet showString) (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 + val _ = println (showNbaei (showSet showString) showNat nbaei) + in print (showHoaAutomaton (toHoaAutomaton aps nbaei)) end diff --git a/thys/Buchi_Complementation/code/benchmark.py b/thys/Buchi_Complementation/code/benchmark.py --- a/thys/Buchi_Complementation/code/benchmark.py +++ b/thys/Buchi_Complementation/code/benchmark.py @@ -1,34 +1,92 @@ #!/usr/bin/python -import sys, random, subprocess +import sys, random, subprocess, time +owl = "/home/Projects/owl/build/distributions/owl-minimized-20.XX-development/bin/owl" + +def read(path): + f = open(path, "r") + text = f.read() + f.close + return text def write(path, text): f = open(path, "w") f.write(text) f.close() -def generate_automaton(): +def get_state_count(path): + result = subprocess.run(["autfilt", path, "--stats=%s"], stdout = subprocess.PIPE, text = True) + return int(result.stdout.strip()) + +def spot_generate_automaton(state_count, proposition_count): seed = random.randrange(0x10000) - result = subprocess.run(["randaut", "--seed={}".format(seed), "--ba", "--states=20", "a", "b", "c", "d"], stdout = subprocess.PIPE, text = True) + result = subprocess.run(["randaut", "--seed={}".format(seed), "--ba", "--states={}".format(state_count), str(proposition_count)], stdout = subprocess.PIPE, text = True) return result.stdout -def generate_formula(): +def spot_generate_formula(proposition_count): seed = random.randrange(0x10000) - result = subprocess.run(["randltl", "--seed={}".format(seed), "4"], stdout = subprocess.PIPE, text = True) + result = subprocess.run(["randltl", "--seed={}".format(seed), str(proposition_count)], stdout = subprocess.PIPE, text = True) + return result.stdout.strip() + +def spot_simplify_automaton(path): + result = subprocess.run(["autfilt", "--ba", "--small", path], stdout = subprocess.PIPE, text = True) return result.stdout -def translate_formula(formula): - result = subprocess.run(["ltl2tgba", "--ba", formula], stdout = subprocess.PIPE, text = True) +def owl_simplify_automaton(path): + result = subprocess.run(["owl", "-I", path, "---", "hoa", "---", "optimize-aut", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True) return result.stdout +def spot_formula_to_nba(formula): + result = subprocess.run(["ltl2tgba", "--ba", formula], stdout = subprocess.PIPE, text = True) + return result.stdout +def owl_formula_to_nba(formula): + result = subprocess.run(["owl", "-i", formula, "---", "ltl", "---", "simplify-ltl", "---", "ltl2nba", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True) + return result.stdout +def owl_formula_to_dra(formula): + result = subprocess.run(["owl", "-i", formula, "---", "ltl", "---", "simplify-ltl", "---", "ltl2dra", "---", "hoa", "-s"], stdout = subprocess.PIPE, text = True) + return result.stdout + +def bc_complement(path1, path2): + subprocess.run(["./Autool", "complement_quick", path1, path2], timeout = 10) +def bc_equivalence(path1, path2): + result = subprocess.run(["./Autool", "equivalence", path1, path2], timeout = 10, stdout = subprocess.PIPE, text = True) + return result.stdout.strip() == "true" + +def complement(path_input, path_output): + start = time.time() + try: bc_complement(path_input, path_output) + except subprocess.TimeoutExpired: duration = "T" + else: duration = str(time.time() - start) + print("{} {}".format(get_state_count(path_input), duration)) +def equivalence(path_1, path_2): + start = time.time() + try: eq = bc_equivalence(path_1, path_2) + except subprocess.TimeoutExpired: eq = None; duration = "T" + else: duration = str(time.time() - start) + print("{} {} {} {}".format(get_state_count(path_1), get_state_count(path_2), eq, duration)) + if sys.argv[1] == "complement_automaton": - write("a.hoa", generate_automaton()) - subprocess.run(["./Autool", "complement_quick", "a.hoa", "c.txt"]) + while True: + write("a.hoa", spot_generate_automaton(20, 4)) + complement("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 + write("a.hoa", spot_formula_to_nba(spot_generate_formula(4))) + complement("a.hoa", "c.txt") +if sys.argv[1] == "equivalence_random": + while True: + write("a.hoa", spot_generate_automaton(100, 4)) + write("b.hoa", spot_generate_automaton(100, 4)) + equivalence("a.hoa", "b.hoa") +if sys.argv[1] == "equivalence_simplify": + while True: + write("a.hoa", spot_generate_automaton(20, 4)) + write("b.hoa", spot_simplify_automaton("a.hoa")) + equivalence("a.hoa", "b.hoa") +if sys.argv[1] == "equivalence_translate": + while True: + formula = spot_generate_formula(4) + print(formula) + write("a.hoa", owl_formula_to_nba(formula)) + write("b.hoa", owl_formula_to_dra(formula)) + write("c.hoa", spot_simplify_automaton("b.hoa")) + if not read("c.hoa"): continue + equivalence("a.hoa", "c.hoa")