<jupyter_start><jupyter_text>Reachability & Büchi example* It distinghuishes:1. **Positive reachability** from **Sufficent levels**:  - state 0: safe=2, pos_reach=52. **Almost-sure reachability** from **Positive reachability**  - state 3: pos_reach=2, alsure_reach=3(via-reaload)/63. **Büchi** from **Almost-sure reachability**  - state 6: alsure_reach=4, Büchi=10* Some of the good paths go via a reload state.  - almost-sure reachability+ of 3 goes via 4  - everything from 5 goes via 4* Includes little_alsure gadget.  - states 6, 7, 9, 10<jupyter_code>m, T = reachability_examples.ultimate()
solver = BasicES(m, 30, T)
solver.get_min_levels(BUCHI)
solver.get_min_levels(POS_REACH)
solver.get_min_levels(AS_REACH)
solver<jupyter_output><empty_output><jupyter_text>The numbers indicate minimal values of energy needed in a state for: * minimal initial consumption (until we reach some reload) * sufficient levels for survival (as above but does not consider reoads with ∞ * positive reachability (have positive probability to hit the blue states from `s` and always survive (before and after reaching the blue states)) * almost sure reachability (always survive and have probability 1 to reach blue states + survive) * just helper values for almost sure reachability * Büchi (always survive and have probability 1 of visiting blue states infinitely often) * just helper values for Büchi We can't use the numbers to compute the minimal capacity easily as you can see in the following, where we decrease the capacity to 14. It is not enough for the Büchi objective (as the cycle  4 - 5 - 3 - 6 - 8 - 5 - 4 needs at least 15 energy).<jupyter_code>m, T = reachability_examples.ultimate()
solver = BasicES(m, 14, T)
solver.get_min_levels(BUCHI)
solver.get_min_levels(POS_REACH)
solver.get_min_levels(AS_REACH)
solver
solver = BasicES(m, 16, T)
solver.get_min_levels(BUCHI)
solver.get_min_levels(POS_REACH)
solver.get_min_levels(AS_REACH)
solver
solver.get_selector(BUCHI)<jupyter_output><empty_output>
{'fraction_non_alphanumeric': 0.08608608608608609, 'fraction_numerical': 0.021021021021021023, 'mean_word_length': 5.641196013289036, 'pattern_counts': {'":': 0, '<': 9, '<?xml version=': 0, '>': 9, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 1, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'chain_length': '2', 'dir': 'jupyter-structured-clean-dedup', 'id': '191695', 'license': 'MIT', 'n_tokens_mistral': 684, 'n_tokens_neox': 629, 'n_words': 232, 'path': 'examples/reach_buchi.ipynb', 'repo_name': 'MaxDauber/FiMDP', 'size': '1998'}