diff --git a/Dockerfile b/Dockerfile index 63f5fc5a..57424311 100644 --- a/Dockerfile +++ b/Dockerfile @@ -132,7 +132,7 @@ RUN AUTO_UPDATE=1 conda install --no-update-deps -y \ # Tier 2: tools with regular updates (2-4/year) RUN AUTO_UPDATE=1 conda install --no-update-deps -y \ -c daemontus \ - biodivine_aeon=0.0.9a3=py311h9bf148f_0 \ + biodivine_aeon=1.0.1=py311h9bf148f_0 \ cabean=1.0.0=0 \ ginsim=3.0.0b=12 \ maboss=2.5.7=he9e06a5_1 \ diff --git a/tutorials/aeon/AEON.py Tutorial.ipynb b/tutorials/aeon/AEON.py Tutorial.ipynb index 45c14592..d4e2cd9e 100644 --- a/tutorials/aeon/AEON.py Tutorial.ipynb +++ b/tutorials/aeon/AEON.py Tutorial.ipynb @@ -26,7 +26,7 @@ }, { "cell_type": "code", - "execution_count": 1, + "execution_count": 16, "metadata": { "cell_id": "00000-2aa8354c-b904-4b5f-80b2-599e98cf09f3", "deepnote_app_coordinates": { @@ -48,6 +48,18 @@ "tags": [] }, "outputs": [ + { + "data": { + "text/html": [ + "Using local file cellcollective-36604-1.sbml
" + ], + "text/plain": [ + "/notebook/tutorials/aeon/cellcollective-36604-1.sbml" + ] + }, + "metadata": {}, + "output_type": "display_data" + }, { "name": "stdout", "output_type": "stream", @@ -58,6 +70,7 @@ ], "source": [ "from biodivine_aeon import *\n", + "import biodivine_aeon as ba\n", "from pathlib import Path\n", "import cellcollective\n", "\n", @@ -66,7 +79,19 @@ "\n", "# Open the loaded SBML and parse it as a Boolean network.\n", "model = BooleanNetwork.from_file(sbml.localfile)\n", - "print(f\"Loaded model with {model.num_vars()} variables.\")" + "#model = BooleanNetwork.from_file(\"cellcollective-36604-1.sbml\")\n", + "print(f\"Loaded model with {model.variable_count()} variables.\")" + ] + }, + { + "cell_type": "code", + "execution_count": 17, + "metadata": {}, + "outputs": [], + "source": [ + "# Print some basic messages (unfortunately, in jupyter notebooks, these may be delayed until the cell finishes computing\n", + "# but you can see them in the terminal). ba.LOG_NOTHING is the default, but ba.LOG_VERBOSE is also available.\n", + "ba.LOG_LEVEL = ba.LOG_ESSENTIAL" ] }, { @@ -78,7 +103,7 @@ }, { "cell_type": "code", - "execution_count": 2, + "execution_count": 18, "metadata": {}, "outputs": [ { @@ -91,12 +116,8 @@ } ], "source": [ - "print(f\"Number of explicit parameters: {model.num_parameters()}.\")\n", - "implicit_parameters = 0\n", - "for var in model.variables():\n", - " if model.get_update_function(var) == None:\n", - " implicit_parameters += 1\n", - "print(f\"Number of implicit parameters: {implicit_parameters}.\")" + "print(f\"Number of explicit parameters: {model.explicit_parameter_count()}.\")\n", + "print(f\"Number of implicit parameters: {model.implicit_parameter_count()}.\")" ] }, { @@ -119,7 +140,7 @@ }, { "cell_type": "code", - "execution_count": 3, + "execution_count": 19, "metadata": { "cell_id": "00003-df3adfd6-aa81-4bbc-92ac-913749e86c21", "deepnote_app_coordinates": { @@ -151,7 +172,7 @@ ], "source": [ "try:\n", - " stg = SymbolicAsyncGraph(model)\n", + " stg = AsynchronousGraph(model)\n", "except Exception as e:\n", " print(e)" ] @@ -165,24 +186,52 @@ }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 20, "metadata": {}, - "outputs": [], + "outputs": [ + { + "data": { + "text/plain": [ + "{'source': VariableId(51),\n", + " 'target': VariableId(58),\n", + " 'essential': True,\n", + " 'sign': '+'}" + ] + }, + "execution_count": 20, + "metadata": {}, + "output_type": "execute_result" + } + ], "source": [ + "# You can also automatically fix all issues using model.infer_valid_graph()\n", + "\n", "# Export the Boolean network as `.aeon` model string.\n", "model_aeon = model.to_aeon()\n", "\n", "# Relax the problematic regulation constraints:\n", "\n", "# Mark regulation \"spoIIE -> spoIIAB\" as non-monotonous:\n", - "model_aeon = model_aeon.replace(\"spoIIE -> spoIIAB\", \"spoIIE -? spoIIAB\")\n", + "model.ensure_regulation({\n", + " 'source': 'spoIIE',\n", + " 'target': 'spoIIAB',\n", + " 'essential': True,\n", + " 'sign': None,\n", + "})\n", "# Mark regulation \"sporulation -| glucose___PTS\" as non-essential:\n", - "model_aeon = model_aeon.replace(\"sporulation -| glucose___PTS\", \"sporulation -|? glucose___PTS\")\n", + "model.ensure_regulation({\n", + " 'source': 'sporulation',\n", + " 'target': 'glucose___PTS',\n", + " 'essential': False,\n", + " 'sign': '-',\n", + "})\n", "# Mark regulation \"sigA -> spo0A_p\" as non-essential:\n", - "model_aeon = model_aeon.replace(\"sigA -> spo0A_p\", \"sigA ->? spo0A_p\")\n", - "\n", - "# Load back the modified model:\n", - "model = BooleanNetwork.from_aeon(model_aeon)" + "model.ensure_regulation({\n", + " 'source': 'sigA',\n", + " 'target': 'spo0A_p',\n", + " 'essential': False,\n", + " 'sign': '+',\n", + "})" ] }, { @@ -205,7 +254,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 21, "metadata": { "cell_id": "00005-b69efddf-725f-4354-bbad-cc27abb2e4d1", "deepnote_app_coordinates": { @@ -226,21 +275,200 @@ "tags": [] }, "outputs": [ + { + "name": "stdout", + "output_type": "stream", + "text": [ + "Start interleaved transition guided reduction with 604462909807314600000000[nodes:2] candidates.\n", + " > Discarded 302231454903657300000000 instances based on the BnVariable(63) extended component.\n", + " > State space reduced to 302231454903657300000000[nodes:5].\n", + " > Discarded 151115727451828650000000 instances based on the BnVariable(51) extended component.\n", + " > State space reduced to 151115727451828650000000[nodes:8].\n", + " > Discarded 75557863725914320000000 instances based on the BnVariable(55) extended component.\n", + " > State space reduced to 75557863725914320000000[nodes:10].\n", + " > Discarded 37778931862957160000000 instances based on the BnVariable(46) extended component.\n", + " > State space reduced to 37778931862957160000000[nodes:13].\n", + " > Discarded 18889465931478580000000 instances based on the BnVariable(45) extended component.\n", + " > State space reduced to 18889465931478580000000[nodes:16].\n", + " > Discarded 9444732965739290000000 instances based on the BnVariable(44) extended component.\n", + " > State space reduced to 9444732965739290000000[nodes:19].\n", + " > Discarded 4722366482869645000000 instances based on the BnVariable(43) extended component.\n", + " > State space reduced to 4722366482869645000000[nodes:22].\n", + " > Discarded 2361183241434822600000 instances based on the BnVariable(38) extended component.\n", + " > State space reduced to 2361183241434822600000[nodes:25].\n", + " > Discarded 1180591620717411300000 instances based on the BnVariable(37) extended component.\n", + " > State space reduced to 1180591620717411300000[nodes:28].\n", + " > Discarded 590295810358705700000 instances based on the BnVariable(35) extended component.\n", + " > State space reduced to 590295810358705700000[nodes:31].\n", + " > Discarded 295147905179352830000 instances based on the BnVariable(6) extended component.\n", + " > State space reduced to 295147905179352830000[nodes:34].\n", + " > Discarded 147573952589676410000 instances based on the BnVariable(5) extended component.\n", + " > State space reduced to 147573952589676410000[nodes:37].\n", + " > Discarded 73786976294838210000 instances based on the BnVariable(4) extended component.\n", + " > State space reduced to 73786976294838210000[nodes:40].\n", + " > Discarded 36893488147419103000 instances based on the BnVariable(3) extended component.\n", + " > State space reduced to 36893488147419103000[nodes:43].\n", + " > Discarded 18446744073709552000 instances based on the BnVariable(2) extended component.\n", + " > State space reduced to 18446744073709552000[nodes:45].\n", + " > Discarded 9223372036854776000 instances based on the BnVariable(36) extended component.\n", + " > State space reduced to 9223372036854776000[nodes:50].\n", + " > Discarded 4611686018427388000 instances based on the BnVariable(49) extended component.\n", + " > State space reduced to 4611686018427388000[nodes:61].\n", + " > Discarded 2448832297382707000 instances based on the BnVariable(59) extended component.\n", + " > State space reduced to 2162853721044680700[nodes:147].\n", + " > Discarded 937311672446484500 instances based on the BnVariable(60) extended component.\n", + " > State space reduced to 1225542048598196200[nodes:151].\n", + " > Discarded 468655836223242240 instances based on the BnVariable(62) extended component.\n", + " > State space reduced to 756886212374954000[nodes:155].\n", + " > Discarded 234327918111621120 instances based on the BnVariable(61) extended component.\n", + " > State space reduced to 522558294263332860[nodes:159].\n", + " > Discarded 117163959055810560 instances based on the BnVariable(53) extended component.\n", + " > State space reduced to 405394335207522300[nodes:167].\n", + " > Discarded 53409876830846980 instances based on the BnVariable(58) extended component.\n", + " > State space reduced to 351984458376675300[nodes:180].\n", + " > Discarded 18155135997837310 instances based on the BnVariable(64) extended component.\n", + " > State space reduced to 333829322378838000[nodes:204].\n", + " > Discarded 0 instances based on the BnVariable(25) extended component.\n", + " > Discarded 9288674231451648 instances based on the BnVariable(65) extended component.\n", + " > State space reduced to 324540648147386400[nodes:212].\n", + " > Discarded 18084767253659650 instances based on the BnVariable(52) extended component.\n", + " > State space reduced to 306455880893726700[nodes:217].\n", + " > Discarded 9042383626829824 instances based on the BnVariable(54) extended component.\n", + " > State space reduced to 297413497266896900[nodes:223].\n", + " > Discarded 4521191813414912 instances based on the BnVariable(56) extended component.\n", + " > State space reduced to 292892305453482000[nodes:229].\n", + " > Discarded 2260595906707456 instances based on the BnVariable(57) extended component.\n", + " > State space reduced to 290631709546774500[nodes:230].\n", + " > Discarded 356241767399424 instances based on the BnVariable(32) extended component.\n", + " > State space reduced to 290275467779375100[nodes:294].\n", + " > Discarded 178120883699712 instances based on the BnVariable(33) extended component.\n", + " > State space reduced to 290097346895675400[nodes:298].\n", + " > Discarded 72703339149656060 instances based on the BnVariable(39) extended component.\n", + " > State space reduced to 217394007746019330[nodes:841].\n", + " > Discarded 37279242387456 instances based on the BnVariable(29) extended component.\n", + " > State space reduced to 217356728503631870[nodes:1490].\n", + " > Discarded 1535450808320 instances based on the BnVariable(48) extended component.\n", + " > State space reduced to 217355193052823550[nodes:1496].\n", + " > Discarded 104155224670732290 instances based on the BnVariable(50) extended component.\n", + " > State space reduced to 113199968382091260[nodes:1494].\n", + " > Discarded 54338838528524290 instances based on the BnVariable(41) extended component.\n", + " > State space reduced to 58861129853566980[nodes:2031].\n", + " > Discarded 14433982238162944 instances based on the BnVariable(42) extended component.\n", + " > Finished ITGR process. 28 processes remaining.\n", + " > State space reduced to 44427147615404030[nodes:2095].\n", + " > Discarded 59408121856 instances using the BnVariable(13) transition basin.\n", + " > Finished ITGR process. 28 processes remaining.\n", + " > State space reduced to 44427088207282180[nodes:2218].\n", + " > Discarded 20658435540385790 instances based on the BnVariable(13) extended component.\n", + " > Finished ITGR process. 27 processes remaining.\n", + " > State space reduced to 23768652666896384[nodes:2630].\n", + " > Discarded 10329238934650880 instances based on the BnVariable(14) extended component.\n", + " > Finished ITGR process. 26 processes remaining.\n", + " > State space reduced to 13439413732245504[nodes:2670].\n", + " > Finished ITGR process. 26 processes remaining.\n", + " > Discarded 7746903680745472 instances based on the BnVariable(10) extended component.\n", + " > Finished ITGR process. 25 processes remaining.\n", + " > State space reduced to 5692510051500032[nodes:2431].\n", + " > Finished ITGR process. 25 processes remaining.\n", + " > Discarded 10468982784 instances based on the BnVariable(12) extended component.\n", + " > Finished ITGR process. 24 processes remaining.\n", + " > State space reduced to 5692499582517248[nodes:1678].\n", + " > Discarded 125829120 instances using the BnVariable(7) transition basin.\n", + " > State space reduced to 5692499456688128[nodes:1447].\n", + " > Discarded 1301624903434240 instances based on the BnVariable(7) extended component.\n", + " > State space reduced to 4390874553253888[nodes:2071].\n", + " > Finished ITGR process. 23 processes remaining.\n", + " > Finished ITGR process. 23 processes remaining.\n", + " > Discarded 309237645312 instances using the BnVariable(19) transition basin.\n", + " > Finished ITGR process. 23 processes remaining.\n", + " > State space reduced to 4390565315608576[nodes:2396].\n", + " > Discarded 3466340597760 instances based on the BnVariable(19) extended component.\n", + " > Finished ITGR process. 22 processes remaining.\n", + " > State space reduced to 4387098975010816[nodes:2525].\n", + " > Discarded 3270785368064 instances based on the BnVariable(34) extended component.\n", + " > Finished ITGR process. 21 processes remaining.\n", + " > State space reduced to 4383828189642752[nodes:2549].\n", + " > Discarded 1896420554833920 instances based on the BnVariable(27) extended component.\n", + " > Finished ITGR process. 20 processes remaining.\n", + " > State space reduced to 2487407634808832[nodes:4257].\n", + " > Finished ITGR process. 20 processes remaining.\n", + " > Discarded 645569491894272 instances based on the BnVariable(23) extended component.\n", + " > Finished ITGR process. 19 processes remaining.\n", + " > State space reduced to 1841838142914560[nodes:4393].\n", + " > Discarded 322784745947136 instances based on the BnVariable(28) extended component.\n", + " > Finished ITGR process. 18 processes remaining.\n", + " > State space reduced to 1519053396967424[nodes:4529].\n", + " > Discarded 319782912 instances based on the BnVariable(24) extended component.\n", + " > Finished ITGR process. 17 processes remaining.\n", + " > State space reduced to 1519053077184512[nodes:4655].\n", + " > Discarded 2916352 instances using the BnVariable(0) transition basin.\n", + " > Finished ITGR process. 17 processes remaining.\n", + " > State space reduced to 1519053074268160[nodes:4661].\n", + " > Discarded 46768661561344 instances based on the BnVariable(0) extended component.\n", + " > Finished ITGR process. 16 processes remaining.\n", + " > State space reduced to 1472284412706816[nodes:4527].\n", + " > Discarded 42135884922880 instances based on the BnVariable(30) extended component.\n", + " > Finished ITGR process. 15 processes remaining.\n", + " > State space reduced to 1430148527783936[nodes:3055].\n", + " > Discarded 7841709416448 instances using the BnVariable(11) transition basin.\n", + " > State space reduced to 1422306818367488[nodes:3491].\n", + " > Discarded 0 instances based on the BnVariable(11) extended component.\n", + " > Discarded 8126464 instances based on the BnVariable(40) extended component.\n", + " > State space reduced to 1422306810241024[nodes:3495].\n", + " > Discarded 6410457088 instances based on the BnVariable(21) extended component.\n", + " > State space reduced to 1422300399783936[nodes:3667].\n", + " > Discarded 3205228544 instances based on the BnVariable(17) extended component.\n", + " > State space reduced to 1422297194555392[nodes:3733].\n", + " > Discarded 1602614272 instances based on the BnVariable(18) extended component.\n", + " > State space reduced to 1422295591941120[nodes:3775].\n", + " > Discarded 801307136 instances based on the BnVariable(16) extended component.\n", + " > State space reduced to 1422294790633984[nodes:3817].\n", + " > Discarded 400653568 instances based on the BnVariable(1) extended component.\n", + " > State space reduced to 1422294389980416[nodes:3933].\n", + " > Discarded 865024 instances based on the BnVariable(47) extended component.\n", + " > State space reduced to 1422294389115392[nodes:3614].\n", + " > Discarded 370944 instances based on the BnVariable(22) extended component.\n", + " > State space reduced to 1422294388744448[nodes:3648].\n", + " > Discarded 240896 instances based on the BnVariable(31) extended component.\n", + " > State space reduced to 1422294388503552[nodes:3628].\n", + " > Discarded 129536 instances based on the BnVariable(20) extended component.\n", + " > State space reduced to 1422294388374016[nodes:3676].\n", + " > Discarded 64768 instances based on the BnVariable(15) extended component.\n", + " > State space reduced to 1422294388309248[nodes:3748].\n", + " > Discarded 44288 instances based on the BnVariable(9) extended component.\n", + " > State space reduced to 1422294388264960[nodes:3484].\n", + " > Discarded 4096 instances based on the BnVariable(26) extended component.\n", + " > State space reduced to 1422294388260864[nodes:3496].\n", + " > Discarded 2048 ins" + ] + }, { "data": { "text/plain": [ - "[ColoredVertexSet(cardinality = 867718363543552, unique vertices = 867718363543552, unique colors = 6704),\n", - " ColoredVertexSet(cardinality = 15959465984, unique vertices = 15959465984, unique colors = 1488)]" + "[ColoredVertexSet(cardinality=867718363543552, colors=6704, vertices=867718363543552, symbolic_size=5924),\n", + " ColoredVertexSet(cardinality=15959465984, colors=1488, vertices=15959465984, symbolic_size=1393)]" ] }, - "execution_count": 5, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" + }, + { + "name": "stdout", + "output_type": "stream", + "text": [ + "tances based on the BnVariable(8) extended component.\n", + "Interleaved transition guided reduction finished with 1422294388258816[nodes:3502] candidates.\n", + "Start Xie-Beerel attractor detection on 1422294388258816[nodes:3502] candidates.\n", + " > Found a bottom SCC: 867718363543552x6704[nodes:5924].\n", + " > Found a bottom SCC: 15959465984x1488[nodes:1393].\n", + "Attractor detection finished with 2 results.\n" + ] } ], "source": [ - "stg = SymbolicAsyncGraph(model)\n", - "attractors = find_attractors(stg)\n", + "stg = AsynchronousGraph(model)\n", + "attractors = Attractors.attractors(stg)\n", "attractors" ] }, @@ -255,23 +483,23 @@ }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 22, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ - "Number of colors appearing in both sets: 0.0\n" + "Number of colors appearing in both sets: 0\n" ] }, { "data": { "text/plain": [ - "ColoredVertexSet(cardinality = 867734323009536, unique vertices = 867734323009536, unique colors = 8192)" + "ColoredVertexSet(cardinality=867734323009536, colors=8192, vertices=867734323009536, symbolic_size=6154)" ] }, - "execution_count": 6, + "execution_count": 22, "metadata": {}, "output_type": "execute_result" } @@ -306,7 +534,7 @@ }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 23, "metadata": { "cell_id": "00019-f365985f-aad1-4fbe-a885-9f4f0801a2fa", "deepnote_app_coordinates": { @@ -330,17 +558,17 @@ { "data": { "text/plain": [ - "{'stability': ColorSet(cardinality=2048),\n", - " 'disorder': ColorSet(cardinality=6144)}" + "{Class([\"stability\"]): ColorSet(cardinality=2048, symbolic_size=4),\n", + " Class([\"disorder\"]): ColorSet(cardinality=6144, symbolic_size=4)}" ] }, - "execution_count": 7, + "execution_count": 23, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "classes = classify_attractor(stg, attractor)\n", + "classes = Classification.classify_long_term_behavior(stg, attractor)\n", "classes" ] }, @@ -366,7 +594,7 @@ }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 24, "metadata": { "cell_id": "00021-167a83d3-e88f-4a80-a79e-b387167cb8d9", "deepnote_app_coordinates": { @@ -388,14 +616,14 @@ "name": "stdout", "output_type": "stream", "text": [ - "ColoredVertexSet(cardinality = 2048, unique vertices = 2048, unique colors = 2048)\n", - "ColoredVertexSet(cardinality = 867734323007488, unique vertices = 867734323007488, unique colors = 6144)\n" + "ColoredVertexSet(cardinality=2048, symbolic_size=281)\n", + "ColoredVertexSet(cardinality=867734323007488, symbolic_size=5670)\n" ] } ], "source": [ - "stable_attractor = attractor.intersect_colors(classes[\"stability\"])\n", - "disordered_attractor = attractor.intersect_colors(classes[\"disorder\"])\n", + "stable_attractor = attractor.intersect_colors(classes[Class(\"stability\")])\n", + "disordered_attractor = attractor.intersect_colors(classes[Class(\"disorder\")])\n", "\n", "print(stable_attractor)\n", "print(disordered_attractor)" @@ -423,7 +651,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 25, "metadata": { "cell_id": "00023-ada43388-bf43-4427-ac09-9c8a98e20a68", "deepnote_app_coordinates": { @@ -445,17 +673,17 @@ "name": "stdout", "output_type": "stream", "text": [ - "Sporulation is ON in 2048.0 stable states.\n", - "Sporulation is OFF in 0.0 stable states.\n", + "Sporulation is ON in 2048 stable states.\n", + "Sporulation is OFF in 0 stable states.\n", "Sporulation is ON in 100.0 % of stable attractor states.\n", - "Sporulation is ON in 335223420223488.0 disorder states.\n", - "Sporulation is OFF in 532510902784000.0 disorder states.\n", + "Sporulation is ON in 335223420223488 disorder states.\n", + "Sporulation is OFF in 532510902784000 disorder states.\n", "Sporulation is ON in 38.63 % of disordered attractor states.\n" ] } ], "source": [ - "sporulation_on = stg.fix_variable(\"sporulation\", True)\n", + "sporulation_on = stg.mk_subspace({ \"sporulation\": True })\n", "\n", "on_in_stable_attractor = stable_attractor.intersect(sporulation_on).vertices().cardinality()\n", "off_in_stable_attractor = stable_attractor.minus(sporulation_on).vertices().cardinality()\n", @@ -494,7 +722,7 @@ }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 26, "metadata": { "cell_id": "00025-57239e8c-7c42-4f7c-97df-b312b625f165", "deepnote_app_coordinates": { @@ -525,10 +753,12 @@ } ], "source": [ - "witness = stg.pick_witness(classes[\"stability\"])\n", + "# One color from the color set:\n", + "color_model = next(iter(classes[Class(\"stability\")]))\n", + "witness = color_model.instantiate(model)\n", "\n", - "print(f\"Number of explicit parameters: {witness.num_parameters()}.\")\n", - "print(f\"Number of implicit parameters: {witness.num_implicit_parameters()}.\")" + "print(f\"Number of explicit parameters: {witness.explicit_parameter_count()}.\")\n", + "print(f\"Number of implicit parameters: {witness.implicit_parameter_count()}.\")" ] }, { @@ -551,7 +781,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 27, "metadata": { "cell_id": "00027-4ab2af98-e712-4d0a-977d-d31a03e4bb13", "deepnote_app_coordinates": { @@ -578,14 +808,34 @@ "62415" ] }, - "execution_count": 11, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "Path(\"stable_attractor.bdd\").write_text(stable_attractor.to_bdd().to_raw_string())\n", - "Path(\"disordered_attractor.bdd\").write_text(disordered_attractor.to_bdd().to_raw_string())" + "Path(\"stable_attractor.bdd\").write_text(stable_attractor.to_bdd().data_string())\n", + "Path(\"disordered_attractor.bdd\").write_text(disordered_attractor.to_bdd().data_string())" + ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Or we can use `pickle`:" + ] + }, + { + "cell_type": "code", + "execution_count": 28, + "metadata": {}, + "outputs": [], + "source": [ + "import pickle\n", + "with open(\"stable_attractors.bdd.pickle\", \"wb\") as f:\n", + " pickle.dump(stable_attractor.to_bdd(), f)\n", + "with open(\"disordered_attractor.bdd.pickle\", \"wb\") as f:\n", + " pickle.dump(disordered_attractor.to_bdd(), f)" ] }, { @@ -608,7 +858,7 @@ }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 29, "metadata": { "cell_id": "00029-0a4cb41e-fc60-4843-8be9-17c58a337729", "deepnote_app_coordinates": { @@ -630,14 +880,17 @@ "name": "stdout", "output_type": "stream", "text": [ - "ColoredVertexSet(cardinality = 2048, unique vertices = 2048, unique colors = 2048)\n", - "ColoredVertexSet(cardinality = 867734323007488, unique vertices = 867734323007488, unique colors = 6144)\n" + "ColoredVertexSet(cardinality=2048, symbolic_size=281)\n", + "ColoredVertexSet(cardinality=867734323007488, symbolic_size=5670)\n" ] } ], "source": [ - "stable_reloaded = ColoredVertexSet(stg, Bdd.from_raw_string(Path(\"stable_attractor.bdd\").read_text()))\n", - "disordered_reloaded = ColoredVertexSet(stg, Bdd.from_raw_string(Path(\"disordered_attractor.bdd\").read_text()))\n", + "network_context = stg.symbolic_context()\n", + "bdd_context = network_context.bdd_variable_set()\n", + "\n", + "stable_reloaded = ColoredVertexSet(network_context, Bdd(bdd_context, Path(\"stable_attractor.bdd\").read_text()))\n", + "disordered_reloaded = ColoredVertexSet(network_context, Bdd(bdd_context, Path(\"disordered_attractor.bdd\").read_text()))\n", "\n", "print(stable_reloaded)\n", "print(disordered_reloaded)\n", @@ -668,7 +921,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 30, "metadata": { "cell_id": "00031-1f68d1ca-0d56-4e88-969b-aecefbb72573", "deepnote_app_coordinates": { @@ -691,24 +944,28 @@ "output_type": "stream", "text": [ "Vertex [False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False, False]\n", - "Basin ColoredVertexSet(cardinality = 11558771119839542000000, unique vertices = 63365787494591230000, unique colors = 8192)\n", - "SCC ColoredVertexSet(cardinality = 8192, unique vertices = 1, unique colors = 8192)\n" + "Basin ColoredVertexSet(cardinality=11558771119839541985280, symbolic_size=101)\n", + "SCC ColoredVertexSet(cardinality=8192, symbolic_size=68)\n", + "Start basic symbolic reachability with 8192[nodes:68] candidates.\n", + "Basic reachability done: 11558771119839542000000[nodes:101] candidates. Max intermediate size: 441.\n", + "Start basic symbolic reachability with 8192[nodes:68] candidates.\n", + "Basic reachability done: 44364707639821350000[nodes:28057] candidates. Max intermediate size: 43163.\n" ] } ], "source": [ "# Pick a set containing a single arbitrary vertex from the whole state space:\n", - "vertex = stg.unit_colored_vertices().pick_vertex()\n", + "vertex = stg.mk_unit_colored_vertices().pick_vertex()\n", "\n", "# The actual vertex is just a list of Boolean values.\n", - "print(\"Vertex\", next(vertex.vertices().iterator()))\n", + "print(\"Vertex\", next(iter(vertex.vertices())).values())\n", "\n", "# Compute the set of states backward-reachable from the vertex.\n", - "basin = reach_bwd(stg, vertex)\n", + "basin = Reachability.reach_bwd(stg, vertex)\n", "print(\"Basin\", basin)\n", "\n", "# Compute the strongly-connected-component in which the vertex resides.\n", - "scc = reach_fwd(stg, vertex, basin)\n", + "scc = Reachability.reach_fwd(stg, vertex).intersect(basin)\n", "print(\"SCC\", scc)" ] }, @@ -732,8 +989,15 @@ "\n", "So far, this is the end of our demo. In case of any issues, feel free to contact us on [github](https://github.com/sybila/biodivine-aeon-py)! \n", "\n", - "To learn more about what features and functions are available in AEON.py, you can follow the tuturial on [partially specified Boolean networks](./bn_tutorial.ipynb) and [symbolic computation using BDDs](bdd_tutorial.ipynb). Further tutorials, examples and case studies are available in the [AEON.py repository](https://github.com/sybila/biodivine-aeon-py/tree/main/example)." + "To learn more about what features and functions are available in AEON.py, you can follow the tuturial on [partially specified Boolean networks](./bn_tutorial.ipynb) and [symbolic computation using BDDs](bdd_tutorial.ipynb). Further tutorials, examples and case studies are available in the [AEON.py repository](https://github.com/sybila/biodivine-aeon-py/tree/main/example). API documentation is also available [here](https://biodivine.fi.muni.cz/docs/aeon-py/latest/)." ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -758,9 +1022,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.10.6" + "version": "3.11.8" } }, "nbformat": 4, - "nbformat_minor": 2 + "nbformat_minor": 4 } diff --git a/tutorials/aeon/Partially specified networks in AEON.ipynb b/tutorials/aeon/Partially specified networks in AEON.ipynb index 483333b2..cc0dee58 100644 --- a/tutorials/aeon/Partially specified networks in AEON.ipynb +++ b/tutorials/aeon/Partially specified networks in AEON.ipynb @@ -17,11 +17,11 @@ "source": [ "# Parametrised Boolean Networks in AEON.py\n", "\n", - "AEON.py offers basic functionality for working with Boolean networks. In particular, it supports **three major formats** (`.bnet`, `.sbml`, and `.aeon`), can perform basic **integrity checks** (e.g. that an update function only uses variables that are actually declared as regulators, etc.), and can be used to run simple operations on the regulatory graph (like decomposition into **strongly connected components**).\n", + "AEON.py offers basic functionality for working with Boolean networks. In particular, it supports **three major formats** (`.bnet`, `.sbml`, and `.aeon`), can perform basic **integrity checks** (e.g. that an update function only uses variables that are actually declared as regulators, etc.), and can be used to run simple operations on the regulatory graph (like decomposition into **strongly connected components** or detection of **feedback vertex sets**).\n", "\n", "However, there are two features in particular that (as of now) are uniquely implemented in this library:\n", " \n", - " - Support for fully symbolic exploration of the asynchronous dynamics of a Boolean network (using `SymbolicAsyncGraph`). With this functionality, you can typically explore the dynamics of networks with tens or hundreds of variables without suffering from state space explosion.\n", + " - Support for fully symbolic exploration of the asynchronous dynamics of a Boolean network (using `AsynchronousGraph`). With this functionality, you can typically explore the dynamics of networks with tens or hundreds of variables without suffering from state space explosion.\n", " - Support for \"parametrised\" (or \"partially specified\") networks, where the transitions possibly depend on unknown (uninterpreted) functions. For example, this means that if your data isn't sufficient to actually produce a single \"correct\" network, you can automatically work with a collection of networks with different dynamical constraints." ] }, @@ -111,7 +111,7 @@ "# BooleanNetwork.from_bnet(...)\n", "# BooleanNetwork.from_aeon(...)\n", "\n", - "g2a.num_vars()" + "g2a.variable_count()" ] }, { @@ -181,7 +181,7 @@ { "data": { "text/markdown": [ - "This notebook has been executed using the docker image `colomoto/colomoto-docker` built on `2021-11-16`" + "This notebook has been executed using the docker image `colomoto/colomoto-docker:local`" ], "text/plain": [ "" @@ -193,7 +193,7 @@ { "data": { "text/html": [ - "" + "" ], "text/plain": [ "" @@ -231,12 +231,12 @@ "source": [ "### Regulatory Graphs\n", "\n", - "Now, if you want to create your network in code, you have to first create its `RegulatoryGraph`. A regulatory graph consists simply of variables connected using regulation edges. Each regulation edge can have a monotonicity (`activation` or `inhibition`), and can be observable (`true` or `false`). Monotonicity means that once we try to assign actual Boolean function to this regulation, it must be non-decreasing or non-increasing in the input coresponding to the regulator. Meanwhile, an observable regulation must have an impact on the regulated variable, while non-observable may simply ignore the regulation." + "Now, if you want to create your network in code, you usually have to first create its `RegulatoryGraph`. A regulatory graph consists simply of variables connected using regulation edges. Each regulation edge can have a monotonicity (sign; `+` or `-`), and can be essential (`True` or `False`). Monotonicity means that once we try to assign actual Boolean function to this regulation, it must be non-decreasing or non-increasing in the input coresponding to the regulator. Meanwhile, an essential regulation must have an impact on the regulated variable, while non-essential may simply ignore the regulation." ] }, { "cell_type": "code", - "execution_count": 4, + "execution_count": 5, "metadata": { "cell_id": "00005-d3120c45-9d5f-4d0c-a93d-9ee483011167", "deepnote_app_coordinates": { @@ -263,7 +263,7 @@ "[VariableId(0), VariableId(1), VariableId(2)]" ] }, - "execution_count": 4, + "execution_count": 5, "metadata": {}, "output_type": "execute_result" } @@ -296,7 +296,7 @@ }, { "cell_type": "code", - "execution_count": 5, + "execution_count": 6, "metadata": { "cell_id": "00007-4dd890ff-0bbc-4e93-ba03-caf710fe0f51", "deepnote_app_coordinates": { @@ -323,18 +323,19 @@ "'b'" ] }, - "execution_count": 5, + "execution_count": 6, "metadata": {}, "output_type": "execute_result" } ], "source": [ + "# Note that rg.variable_names() also exists.\n", "rg.get_variable_name(rg.variables()[1])" ] }, { "cell_type": "code", - "execution_count": 6, + "execution_count": 7, "metadata": { "cell_id": "00008-0b764f9b-d953-415c-8886-1035a6a66809", "deepnote_app_coordinates": { @@ -361,7 +362,7 @@ "VariableId(2)" ] }, - "execution_count": 6, + "execution_count": 7, "metadata": {}, "output_type": "execute_result" } @@ -385,12 +386,12 @@ "tags": [] }, "source": [ - "Now, we can start adding regulations to our graph. Notice that monotonicity and observability are optional and will use a default value when not provided." + "Now, we can start adding regulations to our graph. Notice that the sign and essentiality always need to be specified. To identify variables, we can use both names and numeric IDs." ] }, { "cell_type": "code", - "execution_count": 7, + "execution_count": 8, "metadata": { "cell_id": "00006-7eda1733-33a7-44ec-8fb8-e7dffe222e1a", "deepnote_app_coordinates": { @@ -416,34 +417,48 @@ "text/plain": [ "[{'source': VariableId(0),\n", " 'target': VariableId(1),\n", - " 'monotonicity': 'activation',\n", - " 'observable': True},\n", - " {'source': VariableId(1), 'target': VariableId(2), 'observable': True},\n", - " {'source': VariableId(1), 'target': VariableId(0), 'observable': True},\n", - " {'source': VariableId(0), 'target': VariableId(0), 'observable': True},\n", - " {'source': VariableId(2), 'target': VariableId(2), 'observable': True}]" + " 'essential': True,\n", + " 'sign': '+'},\n", + " {'source': VariableId(1),\n", + " 'target': VariableId(2),\n", + " 'essential': False,\n", + " 'sign': None},\n", + " {'source': VariableId(1),\n", + " 'target': VariableId(0),\n", + " 'essential': False,\n", + " 'sign': None},\n", + " {'source': VariableId(0),\n", + " 'target': VariableId(0),\n", + " 'essential': False,\n", + " 'sign': None},\n", + " {'source': VariableId(2),\n", + " 'target': VariableId(2),\n", + " 'essential': False,\n", + " 'sign': None}]" ] }, - "execution_count": 7, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "rg.add_regulation({ \"source\": \"a\", \"target\": \"b\", \"monotonicity\": \"activation\", \"observable\": True })\n", + "# You can also use rg.ensure_regulation to update existing regulations.\n", "\n", - "rg.add_regulation({ \"source\": \"b\", \"target\": \"c\" }) # monotonicity = none, observable = false\n", - "rg.add_regulation({ \"source\": \"b\", \"target\": \"a\" })\n", + "rg.add_regulation({ \"source\": \"a\", \"target\": \"b\", \"sign\": \"+\", \"essential\": True })\n", "\n", - "rg.add_regulation({ \"source\": \"a\", \"target\": \"a\" }) # autoregulations\n", - "rg.add_regulation({ \"source\": \"c\", \"target\": \"c\" })\n", + "rg.add_regulation({ \"source\": \"b\", \"target\": \"c\", \"sign\": None, \"essential\": False })\n", + "rg.add_regulation({ \"source\": \"b\", \"target\": \"a\", \"sign\": None, \"essential\": False })\n", + "\n", + "rg.add_regulation({ \"source\": \"a\", \"target\": \"a\", \"sign\": None, \"essential\": False }) # autoregulations\n", + "rg.add_regulation({ \"source\": \"c\", \"target\": \"c\", \"sign\": None, \"essential\": False })\n", "\n", "rg.regulations()" ] }, { "cell_type": "code", - "execution_count": 8, + "execution_count": 9, "metadata": { "cell_id": "00015-65ba85db-3989-4bbf-8a19-c4c90dfd0fd8", "deepnote_app_coordinates": { @@ -469,11 +484,11 @@ "text/plain": [ "{'source': VariableId(0),\n", " 'target': VariableId(1),\n", - " 'monotonicity': 'activation',\n", - " 'observable': True}" + " 'essential': True,\n", + " 'sign': '+'}" ] }, - "execution_count": 8, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } @@ -502,7 +517,7 @@ }, { "cell_type": "code", - "execution_count": 9, + "execution_count": 10, "metadata": { "cell_id": "00016-2ce026c1-89f9-4706-91c2-aa68a9a47fd6", "deepnote_app_coordinates": { @@ -529,18 +544,18 @@ "{VariableId(0)}" ] }, - "execution_count": 9, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "rg.regulators(\"b\")" + "rg.predecessors(\"b\")" ] }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 11, "metadata": { "cell_id": "00018-d6fb7c98-42c8-4210-9a21-f4d86fe3b7e3", "deepnote_app_coordinates": { @@ -567,18 +582,18 @@ "{VariableId(0), VariableId(2)}" ] }, - "execution_count": 10, + "execution_count": 11, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "rg.targets(\"b\")" + "rg.successors(\"b\")" ] }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 12, "metadata": { "cell_id": "00019-3d8d5561-1d82-4415-9657-d7d2598d3628", "deepnote_app_coordinates": { @@ -605,18 +620,18 @@ "{VariableId(0), VariableId(1)}" ] }, - "execution_count": 11, + "execution_count": 12, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "rg.regulators_transitive(\"b\")" + "rg.backward_reachable(\"b\")" ] }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 13, "metadata": { "cell_id": "00020-82994a8e-970d-431c-b51d-229c4cea76f3", "deepnote_app_coordinates": { @@ -643,13 +658,13 @@ "{VariableId(0), VariableId(1), VariableId(2)}" ] }, - "execution_count": 12, + "execution_count": 13, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "rg.targets_transitive(\"b\")" + "rg.forward_reachable(\"b\")" ] }, { @@ -672,7 +687,7 @@ }, { "cell_type": "code", - "execution_count": 13, + "execution_count": 14, "metadata": { "cell_id": "00022-c3a64513-3489-4461-9f21-de2b7c252594", "deepnote_app_coordinates": { @@ -699,7 +714,7 @@ "[{VariableId(2)}, {VariableId(0), VariableId(1)}]" ] }, - "execution_count": 13, + "execution_count": 14, "metadata": {}, "output_type": "execute_result" } @@ -723,12 +738,12 @@ "tags": [] }, "source": [ - "If we already have a Boolean network, we can easily obtain its regulatory graph:" + "Each Boolean network inherits from a regulatory graph, hence we can use the same methods:" ] }, { "cell_type": "code", - "execution_count": 14, + "execution_count": 15, "metadata": { "cell_id": "00024-71af2a7d-2134-495b-a273-6f53d9180387", "deepnote_app_coordinates": { @@ -755,7 +770,7 @@ "[{VariableId(0), VariableId(1), VariableId(2), VariableId(3), VariableId(4)}]" ] }, - "execution_count": 14, + "execution_count": 15, "metadata": {}, "output_type": "execute_result" } @@ -804,7 +819,7 @@ }, { "cell_type": "code", - "execution_count": 15, + "execution_count": 16, "metadata": { "cell_id": "00027-43d487fb-dc69-4a62-8b29-82e8e53df7a6", "deepnote_app_coordinates": { @@ -853,14 +868,14 @@ "tags": [] }, "source": [ - "We can still work with such a network, but in this case, our implementation of `SymbolicAsyncGraph` would consider **every possible** update function for every variable (as long as it satisfies requirements on regulation observability and monotonicity). That is mostly fine for such a small network, but would be impossible to solve for networks with hundreds of variables and thousands of regulations.\n", + "We can still work with such a network, but in this case, our implementation of `AsynchronousGraph` would consider **every possible** update function for every variable (as long as it satisfies requirements on regulation observability and monotonicity). That is mostly fine for such a small network, but would be impossible to solve for networks with hundreds of variables and thousands of regulations.\n", "\n", "To specify exact update functions, we can simply provide a Boolean expression which describes the function:" ] }, { "cell_type": "code", - "execution_count": 16, + "execution_count": 17, "metadata": { "cell_id": "00029-410f8f09-778b-4e8e-96ae-3380a117a219", "deepnote_app_coordinates": { @@ -884,17 +899,17 @@ { "data": { "text/plain": [ - "'(b & !a)'" + "'b & !a'" ] }, - "execution_count": 16, + "execution_count": 17, "metadata": {}, "output_type": "execute_result" } ], "source": [ "bn.set_update_function(\"a\", \"b & !a\")\n", - "bn.get_update_function(\"a\").to_string(bn)" + "str(bn.get_update_function(\"a\"))" ] }, { @@ -920,7 +935,7 @@ }, { "cell_type": "code", - "execution_count": 17, + "execution_count": 18, "metadata": { "cell_id": "00031-63d948e0-e8b2-45c2-988d-581d5a74476a", "deepnote_app_coordinates": { @@ -937,19 +952,30 @@ "source_hash": "7a08106b", "tags": [] }, - "outputs": [], + "outputs": [ + { + "data": { + "text/plain": [ + "'b & (p1 => c)'" + ] + }, + "execution_count": 18, + "metadata": {}, + "output_type": "execute_result" + } + ], "source": [ "# Add a basic parameter. Arity 0 means the parameter is a constant.\n", - "bn.add_parameter({ \"name\": \"p1\", \"arity\": 0 })\n", + "bn.add_explicit_parameter(\"p1\", 0)\n", "\n", "# Update function for `c` will depend on `c` only when `p1` is set.\n", "bn.set_update_function(\"c\", \"b & (p1 => c)\")\n", "\n", "# Parameter of arity one is a Boolean function with one argument.\n", - "bn.add_parameter({ \"name\": \"p2\", \"arity\": 1 })\n", + "bn.add_explicit_parameter(\"p2\", 1)\n", "\n", "# We can use it for example like this:\n", - "bn.set_update_function(\"c\", \"b & p2(c)\")" + "str(bn.set_update_function(\"c\", \"b & p2(c)\"))" ] }, { @@ -998,7 +1024,7 @@ { "data": { "text/plain": [ - "'((false | ((((!CtrA & GcrA) & !CcrM) & !SciP) & true)) | ((CtrA & !CcrM) & !SciP))'" + "'false | (!CtrA & GcrA & !CcrM & !SciP & true) | (CtrA & !CcrM & !SciP)'" ] }, "execution_count": 19, @@ -1007,12 +1033,12 @@ } ], "source": [ - "g2a.get_update_function(\"CtrA\").to_string(g2a)" + "str(g2a.get_update_function(\"CtrA\"))" ] }, { "cell_type": "code", - "execution_count": 18, + "execution_count": 20, "metadata": { "cell_id": "00034-5221ad3a-4968-4963-b7e4-34a25fb199c4", "deepnote_app_coordinates": { @@ -1036,19 +1062,19 @@ { "data": { "text/plain": [ - "'(CtrA & (!SciP & f1(CcrM, GcrA)))'" + "'CtrA & !SciP & f1(CcrM, GcrA)'" ] }, - "execution_count": 18, + "execution_count": 20, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "g2a.add_parameter({ \"name\": \"f1\", \"arity\": 2 })\n", + "g2a.add_explicit_parameter(\"f1\", 2)\n", "g2a.set_update_function(\"CtrA\", \"CtrA & !SciP & f1(CcrM, GcrA)\")\n", "\n", - "g2a.get_update_function(\"CtrA\").to_string(g2a)" + "str(g2a.get_update_function(\"CtrA\"))" ] }, { @@ -1091,7 +1117,7 @@ }, { "cell_type": "code", - "execution_count": 19, + "execution_count": 21, "metadata": { "cell_id": "00037-6af4a961-3ac5-44ae-a1be-02714d5bc9b2", "deepnote_app_coordinates": { @@ -1115,22 +1141,22 @@ { "data": { "text/plain": [ - "64.0" + "ColoredVertexSet(cardinality=64, colors=2, vertices=32, symbolic_size=9)" ] }, - "execution_count": 19, + "execution_count": 21, "metadata": {}, "output_type": "execute_result" } ], "source": [ "try:\n", - " graph = SymbolicAsyncGraph(g2a)\n", + " graph = AsynchronousGraph(g2a)\n", "except Exception as e:\n", " print(e)\n", "\n", "# There are 32 states and 2 colors (two possible instantiations of function `f1`)\n", - "graph.unit_colored_vertices().cardinality()" + "graph.mk_unit_colored_vertices()" ] }, { @@ -1155,7 +1181,7 @@ }, { "cell_type": "code", - "execution_count": 20, + "execution_count": 22, "metadata": { "cell_id": "00039-e420e444-4f88-41b6-a854-eb4d6d1c59c4", "deepnote_app_coordinates": { @@ -1179,16 +1205,16 @@ { "data": { "text/plain": [ - "1.0" + "1" ] }, - "execution_count": 20, + "execution_count": 22, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "a_color = graph.unit_colors().pick_singleton()\n", + "a_color = graph.mk_unit_colors().pick_singleton()\n", "a_color.cardinality()" ] }, @@ -1207,12 +1233,12 @@ "tags": [] }, "source": [ - "A set of vertices can be also \"dumped\" to a list, but keep in mind that the set can be huge and will easily exhaust memory for models with more than 10 variables. Always check the size of your set using `cardinality` first." + "A set of vertices can be also \"dumped\" to a list or iterated, but keep in mind that the set can be huge and will easily exhaust memory for models with more than 10 variables. Always check the size of your set using `cardinality` first." ] }, { "cell_type": "code", - "execution_count": 21, + "execution_count": 23, "metadata": { "cell_id": "00040-d7333dfb-9b7b-471a-9fda-755dc357d5cf", "deepnote_app_coordinates": { @@ -1237,84 +1263,31 @@ "name": "stdout", "output_type": "stream", "text": [ - "[False, False, False, False, False]\n", - "[True, False, False, False, False]\n", - "[False, True, False, False, False]\n", - "[True, True, False, False, False]\n", - "[False, False, True, False, False]\n", - "[True, False, True, False, False]\n", - "[False, True, True, False, False]\n", - "[True, True, True, False, False]\n", - "[False, False, False, True, False]\n", - "[True, False, False, True, False]\n", - "[False, True, False, True, False]\n", - "[True, True, False, True, False]\n", - "[False, False, True, True, False]\n", - "[True, False, True, True, False]\n", - "[False, True, True, True, False]\n", - "[True, True, True, True, False]\n" + "VertexModel({'CcrM': 0, 'CtrA': 0, 'DnaA': 0, 'GcrA': 0, 'SciP': 0})\n", + "VertexModel({'CcrM': 1, 'CtrA': 0, 'DnaA': 0, 'GcrA': 0, 'SciP': 0})\n", + "VertexModel({'CcrM': 0, 'CtrA': 1, 'DnaA': 0, 'GcrA': 0, 'SciP': 0})\n", + "VertexModel({'CcrM': 1, 'CtrA': 1, 'DnaA': 0, 'GcrA': 0, 'SciP': 0})\n", + "VertexModel({'CcrM': 0, 'CtrA': 0, 'DnaA': 1, 'GcrA': 0, 'SciP': 0})\n", + "VertexModel({'CcrM': 1, 'CtrA': 0, 'DnaA': 1, 'GcrA': 0, 'SciP': 0})\n", + "VertexModel({'CcrM': 0, 'CtrA': 1, 'DnaA': 1, 'GcrA': 0, 'SciP': 0})\n", + "VertexModel({'CcrM': 1, 'CtrA': 1, 'DnaA': 1, 'GcrA': 0, 'SciP': 0})\n", + "VertexModel({'CcrM': 0, 'CtrA': 0, 'DnaA': 0, 'GcrA': 1, 'SciP': 0})\n", + "VertexModel({'CcrM': 1, 'CtrA': 0, 'DnaA': 0, 'GcrA': 1, 'SciP': 0})\n", + "VertexModel({'CcrM': 0, 'CtrA': 1, 'DnaA': 0, 'GcrA': 1, 'SciP': 0})\n", + "VertexModel({'CcrM': 1, 'CtrA': 1, 'DnaA': 0, 'GcrA': 1, 'SciP': 0})\n", + "VertexModel({'CcrM': 0, 'CtrA': 0, 'DnaA': 1, 'GcrA': 1, 'SciP': 0})\n", + "VertexModel({'CcrM': 1, 'CtrA': 0, 'DnaA': 1, 'GcrA': 1, 'SciP': 0})\n", + "VertexModel({'CcrM': 0, 'CtrA': 1, 'DnaA': 1, 'GcrA': 1, 'SciP': 0})\n", + "VertexModel({'CcrM': 1, 'CtrA': 1, 'DnaA': 1, 'GcrA': 1, 'SciP': 0})\n" ] } ], "source": [ - "vertices = graph.fix_variable(\"SciP\", False).vertices()\n", - "for v in vertices.iterator():\n", + "vertices = graph.mk_subspace_vertices({ \"SciP\": False })\n", + "for v in vertices:\n", " print(v)" ] }, - { - "cell_type": "markdown", - "metadata": { - "cell_id": "00042-619e52ac-83dc-4a0e-8373-d7c4a07dd852", - "deepnote_app_coordinates": { - "h": 5, - "w": 12, - "x": 0, - "y": 252 - }, - "deepnote_cell_height": 52.390625, - "deepnote_cell_type": "markdown", - "tags": [] - }, - "source": [ - "We can also create a vertex singleton directly (this will still contain every possible color though!):" - ] - }, - { - "cell_type": "code", - "execution_count": 22, - "metadata": { - "cell_id": "00043-bffe30e0-af52-49e7-adb7-679206b2f798", - "deepnote_app_coordinates": { - "h": 5, - "w": 12, - "x": 0, - "y": 258 - }, - "deepnote_cell_height": 167.390625, - "deepnote_cell_type": "code", - "deepnote_to_be_reexecuted": false, - "execution_millis": 3, - "execution_start": 1647976199506, - "source_hash": "1bd5ff55", - "tags": [] - }, - "outputs": [ - { - "name": "stdout", - "output_type": "stream", - "text": [ - "1.0\n", - "2.0\n" - ] - } - ], - "source": [ - "singleton = graph.fix_vertex([True, False, False, True, False])\n", - "print(singleton.vertices().cardinality())\n", - "print(singleton.colors().cardinality())" - ] - }, { "cell_type": "markdown", "metadata": { @@ -1335,7 +1308,7 @@ }, { "cell_type": "code", - "execution_count": 23, + "execution_count": 24, "metadata": { "cell_id": "00045-fc9778f6-63c2-4071-a3bd-4f5556abe234", "deepnote_app_coordinates": { @@ -1357,24 +1330,102 @@ "name": "stdout", "output_type": "stream", "text": [ - "1 Discovered 2.0 using colors 2.0\n", - "2 Discovered 1.0 using colors 2.0\n", - "3 Discovered 0.0 using colors 0.0\n", - "Total discovered vertices: 4.0\n" + "Picked: VertexModel({'CcrM': 0, 'CtrA': 0, 'DnaA': 0, 'GcrA': 0, 'SciP': 0})\n", + "1 Discovered 0 using colors 0\n", + "Total discovered vertices: 1\n", + "Picked: VertexModel({'CcrM': 0, 'CtrA': 0, 'DnaA': 0, 'GcrA': 0, 'SciP': 1})\n", + "1 Discovered 1 using colors 2\n", + "2 Discovered 0 using colors 0\n", + "Total discovered vertices: 2\n", + "Picked: VertexModel({'CcrM': 0, 'CtrA': 0, 'DnaA': 0, 'GcrA': 1, 'SciP': 0})\n", + "1 Discovered 1 using colors 2\n", + "2 Discovered 0 using colors 0\n", + "Total discovered vertices: 2\n", + "Picked: VertexModel({'CcrM': 0, 'CtrA': 0, 'DnaA': 0, 'GcrA': 1, 'SciP': 1})\n", + "1 Discovered 2 using colors 2\n", + "2 Discovered 1 using colors 2\n", + "3 Discovered 0 using colors 0\n", + "Total discovered vertices: 4\n", + "Picked: VertexModel({'CcrM': 0, 'CtrA': 0, 'DnaA': 1, 'GcrA': 0, 'SciP': 0})\n", + "1 Discovered 2 using colors 2\n", + "2 Discovered 1 using colors 2\n", + "3 Discovered 0 using colors 0\n", + "Total discovered vertices: 4\n", + "Picked: VertexModel({'CcrM': 0, 'CtrA': 0, 'DnaA': 1, 'GcrA': 0, 'SciP': 1})\n", + "1 Discovered 3 using colors 2\n", + "2 Discovered 3 using colors 2\n", + "3 Discovered 1 using colors 2\n", + "4 Discovered 0 using colors 0\n", + "Total discovered vertices: 8\n", + "Picked: VertexModel({'CcrM': 0, 'CtrA': 1, 'DnaA': 0, 'GcrA': 0, 'SciP': 0})\n", + "1 Discovered 3 using colors 2\n", + "2 Discovered 4 using colors 2\n", + "3 Discovered 5 using colors 2\n", + "4 Discovered 4 using colors 2\n", + "5 Discovered 4 using colors 2\n", + "6 Discovered 3 using colors 2\n", + "7 Discovered 1 using colors 2\n", + "8 Discovered 0 using colors 0\n", + "Total discovered vertices: 24\n", + "Picked: VertexModel({'CcrM': 0, 'CtrA': 1, 'DnaA': 0, 'GcrA': 1, 'SciP': 0})\n", + "1 Discovered 3 using colors 2\n", + "2 Discovered 6 using colors 2\n", + "3 Discovered 6 using colors 2\n", + "4 Discovered 6 using colors 2\n", + "5 Discovered 4 using colors 2\n", + "6 Discovered 3 using colors 2\n", + "7 Discovered 1 using colors 2\n", + "8 Discovered 0 using colors 0\n", + "Total discovered vertices: 28\n", + "Picked: VertexModel({'CcrM': 0, 'CtrA': 1, 'DnaA': 1, 'GcrA': 1, 'SciP': 0})\n", + "1 Discovered 3 using colors 2\n", + "2 Discovered 6 using colors 2\n", + "3 Discovered 8 using colors 2\n", + "4 Discovered 7 using colors 2\n", + "5 Discovered 5 using colors 2\n", + "6 Discovered 2 using colors 2\n", + "7 Discovered 2 using colors 2\n", + "8 Discovered 1 using colors 2\n", + "9 Discovered 0 using colors 0\n", + "Total discovered vertices: 30\n", + "Picked: VertexModel({'CcrM': 0, 'CtrA': 1, 'DnaA': 1, 'GcrA': 1, 'SciP': 1})\n", + "1 Discovered 4 using colors 2\n", + "2 Discovered 7 using colors 2\n", + "3 Discovered 7 using colors 2\n", + "4 Discovered 5 using colors 2\n", + "5 Discovered 4 using colors 2\n", + "6 Discovered 3 using colors 2\n", + "7 Discovered 1 using colors 2\n", + "8 Discovered 1 using colors 2\n", + "9 Discovered 0 using colors 0\n", + "Total discovered vertices: 31\n", + "Picked: VertexModel({'CcrM': 1, 'CtrA': 1, 'DnaA': 1, 'GcrA': 1, 'SciP': 1})\n", + "1 Discovered 5 using colors 2\n", + "2 Discovered 10 using colors 2\n", + "3 Discovered 10 using colors 2\n", + "4 Discovered 5 using colors 2\n", + "5 Discovered 1 using colors 2\n", + "6 Discovered 0 using colors 0\n", + "Total discovered vertices: 32\n" ] } ], "source": [ - "reachable = singleton\n", - "for i in range(10):\n", - " step = graph.post(reachable)\n", - " new = step.minus(reachable)\n", - " print(i+1, \"Discovered\", new.vertices().cardinality(), \"using colors\", new.colors().cardinality())\n", - " if new.is_empty():\n", - " break\n", - " reachable = reachable.union(new)\n", - "\n", - "print(\"Total discovered vertices:\", reachable.vertices().cardinality())" + "universe = graph.mk_unit_vertices()\n", + "while not universe.is_empty():\n", + " one_state = universe.pick_singleton()\n", + " print(\"Picked:\", next(iter(one_state)))\n", + " reachable = one_state.extend_with_colors(graph.mk_unit_colors())\n", + " for i in range(10):\n", + " step = graph.post(reachable)\n", + " new = step.minus(reachable)\n", + " print(i+1, \"Discovered\", new.vertices().cardinality(), \"using colors\", new.colors().cardinality())\n", + " if new.is_empty():\n", + " break\n", + " reachable = reachable.union(new)\n", + " \n", + " print(\"Total discovered vertices:\", reachable.vertices().cardinality())\n", + " universe = universe.minus(reachable.vertices())" ] }, { @@ -1394,12 +1445,12 @@ "source": [ "It is also possible to use `var_post` and `var_pre` to only update a specific variable in the network during a transition.\n", "\n", - "To save the results of the computation, we can use the fact that these sets are all internally represented as BDDs, which we can dump to a string, or show as a `.dot`:" + "To save the results of the computation, we can use the fact that these sets are all internally represented as BDDs, which we can dump to a string, show as a `.dot`, or save using `pickle`:" ] }, { "cell_type": "code", - "execution_count": 24, + "execution_count": 25, "metadata": { "cell_id": "00047-3c7de998-5228-42dc-b1d3-4a6046680496", "deepnote_app_coordinates": { @@ -1423,22 +1474,22 @@ { "data": { "text/plain": [ - "'|9,0,0|9,1,1|8,1,0|6,2,0|5,0,3|4,0,4|3,5,0|5,3,0|4,0,7|3,8,0|2,9,6|1,10,0|'" + "'|9,0,0|9,1,1|5,0,1|4,0,2|3,3,0|5,1,0|4,0,5|3,6,0|2,7,4|'" ] }, - "execution_count": 24, + "execution_count": 25, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "reachable_string = reachable.to_bdd().to_raw_string()\n", + "reachable_string = reachable.to_bdd().data_string()\n", "reachable_string" ] }, { "cell_type": "code", - "execution_count": 25, + "execution_count": 26, "metadata": { "cell_id": "00048-9eccafd7-768d-4fe0-aa70-96680e0665ea", "deepnote_app_coordinates": { @@ -1465,161 +1516,125 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", - "11\n", - "\n", - "x_1\n", + "8\n", + "\n", + "f1[0,0]\n", "\n", - "\n", + "\n", "\n", - "init__->11\n", - "\n", - "\n", + "init__->8\n", + "\n", + "\n", "\n", - "\n", - "\n", - "10\n", - "\n", - "x_2\n", + "\n", + "\n", + "4\n", + "\n", + "f1[1,0]\n", "\n", - "\n", - "\n", - "11->10\n", - "\n", - "\n", + "\n", + "\n", + "8->4\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "7\n", + "\n", + "f1[1,0]\n", + "\n", + "\n", + "\n", + "8->7\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "x_8\n", + "\n", + "f1[1,1]\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "x_6\n", + "\n", + "f1[0,1]\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4\n", - "\n", - "x_5\n", + "\n", + "\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "x_4\n", + "\n", + "f1[1,1]\n", "\n", - "\n", + "\n", "\n", - "5->4\n", - "\n", - "\n", + "5->1\n", + "\n", + "\n", "\n", "\n", "\n", "6\n", - "\n", - "x_3\n", + "\n", + "f1[0,1]\n", "\n", "\n", "\n", "6->5\n", - "\n", - "\n", + "\n", + "\n", "\n", - "\n", - "\n", - "7\n", - "\n", - "x_5\n", - "\n", - "\n", + "\n", "\n", - "7->3\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "8\n", - "\n", - "x_4\n", - "\n", - "\n", - "\n", - "8->7\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "9\n", - "\n", - "x_3\n", - "\n", - "\n", - "\n", - "9->8\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "10->6\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "10->9\n", - "\n", - "\n", + "7->6\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - "" + "" ] }, - "execution_count": 25, + "execution_count": 26, "metadata": {}, "output_type": "execute_result" } @@ -1632,7 +1647,7 @@ }, { "cell_type": "code", - "execution_count": 26, + "execution_count": 27, "metadata": { "cell_id": "00048-fc4789fc-4288-49ba-b018-8963ce70441c", "deepnote_app_coordinates": { @@ -1659,7 +1674,7 @@ "True" ] }, - "execution_count": 26, + "execution_count": 27, "metadata": {}, "output_type": "execute_result" } @@ -1667,10 +1682,13 @@ "source": [ "# We need to copy an existing set to preserve all metadata about the model,\n", "# since these are not save in the BDD\n", - "reachable_reloaded = graph.empty_colored_vertices().copy_with_raw_string(reachable_string) \n", + "reachable_reloaded = ColoredVertexSet(\n", + " graph.symbolic_context(), \n", + " Bdd(graph.symbolic_context().bdd_variable_set(), reachable_string)\n", + ")\n", "\n", "# r1 <=> r2 must be a tautology if the sets are equivalent:\n", - "reachable_reloaded.to_bdd().sem_eq(reachable.to_bdd())" + "reachable_reloaded.to_bdd() == reachable.to_bdd()" ] }, { @@ -1690,6 +1708,13 @@ "source": [ "However, keep in mind that the raw string does not contain any information about the underlying model, and you cannot mix BDD representations between different models!" ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -1714,9 +1739,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.10.6" + "version": "3.11.8" } }, "nbformat": 4, - "nbformat_minor": 2 + "nbformat_minor": 4 } diff --git a/tutorials/aeon/Symbolic Computation in AEON.ipynb b/tutorials/aeon/Symbolic Computation in AEON.ipynb index 93e7d52f..9f9d374f 100644 --- a/tutorials/aeon/Symbolic Computation in AEON.ipynb +++ b/tutorials/aeon/Symbolic Computation in AEON.ipynb @@ -21,7 +21,7 @@ "\n", "Compared to other BDD libraries, here we do not have a single shared \"BDD storage\" or \"BDD manager\". Instead, **every BDD is a separate object**, which means it can be more easily passed around during asynchronous or parallel computing (i.e. more than one BDD operation can be running at the same time).\n", "\n", - "That being said, we still use a separate `BddVariableSet` to manage the mapping from *names* to the BDD variables, since these are not used as often and there is no need to keep them around in each BDD. This `BddVariableSet` object is also used to initially create atomic BDDs, so it is probably the first thing that you'll need to create before creating the BDDs. However, each BDD actually maintains the *number* of variables that it supports (which is injected based on the `BddVariableSet`), and you **cannot mix BDDs with a different variable count**. So in practice, you should try to only use together BDDs created using the same `BddVariableSet`." + "That being said, we still use a separate `BddVariableSet` to manage the mapping from *names* to the BDD variables, since these are not used as often and there is no need to keep them around in each BDD. This `BddVariableSet` object is also used to initially create atomic BDDs, so it is probably the first thing that you'll need to create before creating the BDDs. However, each BDD actually maintains the *number* of variables that it supports (which is injected based on the `BddVariableSet`), and you **cannot mix BDDs with a different variable count**. So in practice, you should try to only use together BDDs created using the same `BddVariableSet` (You can migrate BDDs between variable sets using `BddVariableSet.transfer_from` as long as the relevant variables appear in both sets). " ] }, { @@ -90,20 +90,18 @@ }, "outputs": [ { - "data": { - "text/plain": [ - "['x_0', 'x_1', 'x_2', 'x_3', 'x_4', 'x_5', 'x_6', 'x_7', 'x_8', 'x_9']" - ] - }, - "execution_count": 2, - "metadata": {}, - "output_type": "execute_result" + "name": "stdout", + "output_type": "stream", + "text": [ + "['x_0', 'x_1', 'x_2', 'x_3', 'x_4', 'x_5', 'x_6', 'x_7', 'x_8', 'x_9']\n", + "['x_0', 'x_1', 'x_2', 'x_3', 'x_4', 'x_5', 'x_6', 'x_7', 'x_8', 'x_9']\n" + ] } ], "source": [ "# Create a BddVariableSet with 5 variables names a, b, c, d, e.\n", "vars = BddVariableSet([\"a\", \"b\", \"c\", \"d\", \"e\"])\n", - "assert vars.var_count() == 5\n", + "assert vars.variable_count() == 5\n", "# To actually use the variables in the future, we have to use a reference. \n", "# Here, v_a now contains a BDD variable reference. \n", "v_a = vars.find_variable(\"a\")\n", @@ -125,11 +123,13 @@ "anonymous_vars = BddVariableSet(10)\n", "\n", "# It is always possible to obtain all variables in the set, just in case:\n", - "actual_anonymous_vars = anonymous_vars.all_variables()\n", + "actual_anonymous_vars = anonymous_vars.variable_ids()\n", "\n", "# This gives you a list of all \"variable references\". \n", "# You can however read back their names easily:\n", - "list(map(lambda v: anonymous_vars.name_of(v), actual_anonymous_vars))" + "print([ anonymous_vars.get_variable_name(v) for v in actual_anonymous_vars ])\n", + "# Since this is a common operation, we also have a utility function for that:\n", + "print(anonymous_vars.variable_names())" ] }, { @@ -189,16 +189,16 @@ "\n", "# You can create variables one by one, and the builder will always \n", "# give you the variable reference for later use.\n", - "v_first = builder.make(\"first\")\n", + "v_first = builder.add(\"first\")\n", "\n", "# You can also create multiple variable at the same time if you want to.\n", - "created = builder.make_all([\"second\", \"third\", \"fourth\"])\n", + "created = builder.add_all([\"second\", \"third\", \"fourth\"])\n", "v_third = created[1]\n", "\n", "# In the end, you can just call build to turn the builder into \n", "# a valid variable set.\n", "four_vars = builder.build()\n", - "four_vars.var_count()" + "four_vars.variable_count()" ] }, { @@ -247,7 +247,7 @@ { "data": { "text/plain": [ - "4.0" + "4" ] }, "execution_count": 4, @@ -317,86 +317,86 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "x_0\n", + "\n", + "a\n", "\n", "\n", "\n", "init__->5\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "x_1\n", + "\n", + "b\n", "\n", "\n", "\n", "5->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "x_3\n", + "\n", + "d\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "x_2\n", + "\n", + "c\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - "" + "" ] }, "execution_count": 5, @@ -425,7 +425,7 @@ "tags": [] }, "source": [ - "For readability, the generated plot omits edges that lead to the `zero` terminal node, as these are easy to infer. However, the plot is also missing **variable names** -- defaulting to anonymous variables instead. If we want to actually use the names we declared when creating the BDD, we have to provide the variable set during conversion." + "For readability, the generated plot omits edges that lead to the `zero` terminal node. We can show these edges with an optional argument:" ] }, { @@ -457,86 +457,110 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "\n", "5\n", - "\n", - "a\n", + "\n", + "a\n", "\n", "\n", "\n", "init__->5\n", - "\n", - "\n", + "\n", + "\n", + "\n", + "\n", + "\n", + "0\n", + "\n", + "0\n", + "\n", + "\n", + "\n", + "5->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "4\n", - "\n", - "b\n", + "\n", + "b\n", "\n", "\n", - "\n", + "\n", "5->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", - "\n", + "\n", "2\n", - "\n", - "d\n", + "\n", + "d\n", "\n", - "\n", + "\n", "\n", + "2->0\n", + "\n", + "\n", + "\n", + "\n", + "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "3\n", - "\n", - "c\n", + "\n", + "c\n", + "\n", + "\n", + "\n", + "3->0\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "4->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", - "\n", + "\n", "4->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - "" + "" ] }, "execution_count": 6, @@ -545,7 +569,7 @@ } ], "source": [ - "graphviz.Source(formula.to_dot(vars))" + "graphviz.Source(formula.to_dot(zero_pruned=False))" ] }, { @@ -589,7 +613,7 @@ { "data": { "text/plain": [ - "(x_0 & ((x_1 & (!x_2 & !x_3)) | (!x_1 & !x_3)))" + "BooleanExpression(\"(a & ((b & (!c & !d)) | (!b & !d)))\")" ] }, "execution_count": 7, @@ -598,60 +622,7 @@ } ], "source": [ - "formula.to_boolean_expression()" - ] - }, - { - "cell_type": "markdown", - "metadata": { - "cell_id": "00014-ee26678c-1724-44d8-9f16-479aa0bafabd", - "deepnote_app_coordinates": { - "h": 5, - "w": 12, - "x": 0, - "y": 84 - }, - "deepnote_cell_height": 52.390625, - "deepnote_cell_type": "markdown", - "tags": [] - }, - "source": [ - "Here, the variable names are again missing, but we can again easily fix it by providing the original variable set:" - ] - }, - { - "cell_type": "code", - "execution_count": 8, - "metadata": { - "cell_id": "00015-8efb1249-2f9c-41d6-8978-349041072d88", - "deepnote_app_coordinates": { - "h": 5, - "w": 12, - "x": 0, - "y": 90 - }, - "deepnote_cell_height": 111.6875, - "deepnote_cell_type": "code", - "deepnote_to_be_reexecuted": false, - "execution_millis": 123, - "execution_start": 1647976187267, - "source_hash": "31c25269", - "tags": [] - }, - "outputs": [ - { - "data": { - "text/plain": [ - "(a & ((b & (!c & !d)) | (!b & !d)))" - ] - }, - "execution_count": 8, - "metadata": {}, - "output_type": "execute_result" - } - ], - "source": [ - "formula.to_boolean_expression(vars)" + "formula.to_expression()" ] }, { @@ -669,12 +640,12 @@ "tags": [] }, "source": [ - "To actually manipulate the BDDs, we can use normal logical operators, as well as projection and selection. But note that Python automatically translates methods `and` and `or` to infix notation. Unfortunately, the rest of the logical operations do not support this notation." + "To actually manipulate the BDDs, we can use normal logical operators, as well as projection and selection. But note that Python automatically translates methods `and` and `or` to reserved operators, even if used as method names. Therefore, we opted to use a prefix `l_*` to denote the logical operations and `r_*` to denote relational operations:" ] }, { "cell_type": "code", - "execution_count": 10, + "execution_count": 8, "metadata": { "cell_id": "00017-25f4af71-30db-432d-ba30-9573d9490f35", "deepnote_app_coordinates": { @@ -701,89 +672,77 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", - "\n", + "\n", "\n", - "5\n", - "\n", - "b\n", + "4\n", + "\n", + "b\n", "\n", - "\n", + "\n", "\n", - "init__->5\n", - "\n", - "\n", + "init__->4\n", + "\n", + "\n", "\n", - "\n", - "\n", - "3\n", - "\n", - "c\n", + "\n", + "\n", + "2\n", + "\n", + "d\n", "\n", - "\n", + "\n", "\n", - "5->3\n", - "\n", - "\n", + "4->2\n", + "\n", + "\n", "\n", - "\n", - "\n", - "4\n", - "\n", - "d\n", + "\n", + "\n", + "3\n", + "\n", + "c\n", "\n", - "\n", - "\n", - "5->4\n", - "\n", - "\n", + "\n", + "\n", + "4->3\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", - "\n", - "\n", - "\n", - "2\n", - "\n", - "d\n", + "\n", + "1\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", - "\n", - "\n", - "\n", - "4->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - "" + "" ] }, - "execution_count": 10, + "execution_count": 8, "metadata": {}, "output_type": "execute_result" } @@ -801,11 +760,11 @@ "# Projection, either using one variable, or a set of variables.\n", "# Here, we have to use variable references instead of names though, \n", "# since the BDD object has no idea what the actual names of the variables are.\n", - "formula.project_exists([v_a, v_c])\n", - "formula.project_for_all([v_a, v_c])\n", + "formula.r_exists([v_a, v_c])\n", + "formula.r_for_all([v_a, v_c])\n", "\n", "# Projection \"removes\" the influence of a particular variable: F = F[a/0] | F[a/1]\n", - "graphviz.Source(formula.project_exists(v_a).to_dot(vars))" + "graphviz.Source(formula.r_exists(v_a).to_dot())" ] }, { @@ -817,7 +776,7 @@ }, { "cell_type": "code", - "execution_count": 11, + "execution_count": 9, "metadata": { "cell_id": "00018-215df1c3-7c75-4ba3-a157-a2186d3c0e1a", "deepnote_app_coordinates": { @@ -844,77 +803,77 @@ "\n", "\n", - "\n", "\n", - "\n", - "\n", + "\n", + "\n", "G\n", - "\n", + "\n", "\n", "\n", "\n", "4\n", - "\n", - "a\n", + "\n", + "a\n", "\n", "\n", "\n", "init__->4\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3\n", - "\n", - "c\n", + "\n", + "c\n", "\n", "\n", "\n", "4->3\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "1\n", - "\n", - "1\n", + "\n", + "1\n", "\n", "\n", "\n", "2\n", - "\n", - "d\n", + "\n", + "d\n", "\n", "\n", "\n", "2->1\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n", "3->2\n", - "\n", - "\n", + "\n", + "\n", "\n", "\n", "\n" ], "text/plain": [ - "" + "" ] }, - "execution_count": 11, + "execution_count": 9, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "graphviz.Source(formula.select({ v_c: False }).to_dot(vars))" + "graphviz.Source(formula.r_select({ v_c: False }).to_dot())" ] }, { @@ -932,12 +891,12 @@ "tags": [] }, "source": [ - "Finally, to transfer and save BDDs, you can use a simple string format that encodes the directed graph:" + "Finally, to transfer and save BDDs, you can use a simple string format that encodes the directed graph. However, a BDD can be also saved using `pickle`." ] }, { "cell_type": "code", - "execution_count": 12, + "execution_count": 10, "metadata": { "cell_id": "00020-1b064503-facd-4a62-a805-bd45847f9e9f", "deepnote_app_coordinates": { @@ -964,15 +923,17 @@ "'|5,0,0|5,1,1|3,1,0|2,2,0|1,2,3|0,0,4|'" ] }, - "execution_count": 12, + "execution_count": 10, "metadata": {}, "output_type": "execute_result" } ], "source": [ - "assert Bdd.from_raw_string(formula.to_raw_string()).to_raw_string() == formula.to_raw_string()\n", + "# Note that you need to provide the variable set together with the data string:\n", + "assert Bdd(vars, formula.data_string()).data_string() == formula.data_string()\n", "\n", - "formula.to_raw_string()" + "# formula.data_bytes() also exists.\n", + "formula.data_string()" ] }, { @@ -990,10 +951,17 @@ "tags": [] }, "source": [ - "Now you've covered most of the BDD functionality available in AEON. For more details, you can explore the [tutorial](https://docs.rs/biodivine-lib-bdd/latest/biodivine_lib_bdd/tutorial/index.html) which describes the original Rust implementation (but has some extra details on certain topics). The rest of the documentation can be also helpful to get deeper insight into how the library works. \n", + "Now you've covered most of the BDD functionality available in AEON. For more details, you can explore the [tutorial](https://docs.rs/biodivine-lib-bdd/latest/biodivine_lib_bdd/tutorial/index.html) which describes the original Rust implementation of BDDs (it has some extra details on certain topics). The rest of the Rust documentation can be also helpful to get deeper insight into how the library works. \n", "\n", - "Alternatively, you can also explore the documentation in the source code of these Python bindings [here](https://biodivine.fi.muni.cz/docs/aeon-py/v0.1.0/), where you'll find some notes on how are these Rust functions translated to Python." + "Alternatively, you can also explore the documentation for the Python bindings [here](https://biodivine.fi.muni.cz/docs/aeon-py/latest/), where you'll find the actual list of methods that is available in Python." ] + }, + { + "cell_type": "code", + "execution_count": null, + "metadata": {}, + "outputs": [], + "source": [] } ], "metadata": { @@ -1018,9 +986,9 @@ "name": "python", "nbconvert_exporter": "python", "pygments_lexer": "ipython3", - "version": "3.10.6" + "version": "3.11.8" } }, "nbformat": 4, - "nbformat_minor": 2 + "nbformat_minor": 4 } diff --git a/tutorials/aeon/disordered_attractor.bdd b/tutorials/aeon/disordered_attractor.bdd deleted file mode 100644 index 1bdce336..00000000 --- a/tutorials/aeon/disordered_attractor.bdd +++ /dev/null @@ -1 +0,0 @@ -|79,0,0|79,1,1|77,1,0|76,2,0|75,3,0|70,4,0|69,5,4|67,0,6|72,4,0|70,8,4|70,8,0|69,10,9|68,11,6|67,0,12|66,7,13|65,7,14|64,15,7|63,0,16|62,0,17|61,0,18|60,0,19|57,0,20|56,0,21|55,0,22|55,22,0|54,24,23|53,0,25|53,25,0|52,27,26|51,0,28|60,19,0|57,0,30|56,0,31|55,0,32|55,32,0|54,34,33|53,0,35|53,35,0|52,37,36|51,38,0|50,39,29|49,40,0|48,41,0|45,0,42|44,0,43|43,0,44|43,44,0|42,46,45|41,0,47|40,0,48|60,18,0|57,0,50|56,0,51|55,52,0|54,53,33|53,0,54|53,54,0|52,56,55|51,57,0|50,58,29|49,59,0|48,60,0|45,0,61|44,0,62|43,63,0|42,64,45|41,0,65|40,66,0|39,67,49|76,0,2|75,3,69|74,70,4|73,71,4|72,72,4|71,4,73|69,5,74|68,6,75|67,0,76|66,7,77|65,7,78|64,7,79|63,0,80|75,0,69|74,82,0|73,83,0|72,84,0|71,0,85|69,0,86|68,0,87|67,88,0|66,0,89|65,0,90|64,0,91|63,92,0|62,93,81|61,0,94|60,0,95|57,0,96|56,0,97|55,0,98|55,98,0|54,100,99|53,0,101|53,101,0|52,103,102|51,0,104|60,95,0|57,0,106|56,0,107|55,0,108|55,108,0|54,110,109|53,0,111|53,111,0|52,113,112|51,114,0|50,115,105|49,116,0|48,117,0|45,0,118|62,93,0|61,0,120|60,0,121|57,0,122|56,0,123|55,0,124|55,124,0|54,126,125|53,0,127|53,127,0|52,129,128|51,0,130|60,121,0|57,0,132|56,0,133|55,0,134|55,134,0|54,136,135|53,0,137|53,137,0|52,139,138|51,140,0|50,141,131|49,142,0|48,143,0|46,144,0|45,145,0|44,146,119|43,0,147|43,147,0|42,149,148|41,0,150|40,0,151|60,94,0|57,0,153|56,0,154|55,155,0|54,156,109|53,0,157|53,157,0|52,159,158|51,160,0|50,161,105|49,162,0|48,163,0|45,0,164|61,120,0|60,166,0|57,0,167|56,0,168|55,169,0|54,170,135|53,0,171|53,171,0|52,173,172|51,174,0|50,175,131|49,176,0|48,177,0|46,178,0|45,179,0|44,180,165|43,181,0|42,182,148|41,0,183|40,184,0|39,185,152|38,186,68|34,0,187|76,1,0|75,189,0|70,190,0|69,191,190|67,0,192|77,0,1|76,194,0|75,195,0|72,190,196|70,197,190|70,197,0|69,199,198|68,200,192|67,0,201|66,193,202|65,193,203|64,204,193|63,0,205|62,0,206|61,0,207|60,0,208|57,0,209|56,0,210|55,0,211|55,211,0|54,213,212|53,0,214|53,214,0|52,216,215|51,0,217|60,208,0|57,0,219|56,0,220|55,0,221|55,221,0|54,223,222|53,0,224|53,224,0|52,226,225|51,227,0|50,228,218|49,229,0|48,230,0|45,0,231|44,0,232|43,0,233|43,233,0|42,235,234|41,0,236|40,0,237|60,207,0|57,0,239|56,0,240|55,241,0|54,242,222|53,0,243|53,243,0|52,245,244|51,246,0|50,247,218|49,248,0|48,249,0|45,0,250|44,0,251|43,252,0|42,253,234|41,0,254|40,255,0|39,256,238|76,0,1|75,189,258|74,259,190|73,260,190|72,261,190|71,190,262|69,191,263|68,192,264|67,0,265|66,193,266|65,193,267|64,193,268|63,0,269|75,0,258|74,271,0|73,272,0|72,273,0|71,0,274|69,0,275|68,0,276|67,277,0|66,0,278|65,0,279|64,0,280|63,281,0|62,282,270|61,0,283|60,0,284|57,0,285|56,0,286|55,0,287|55,287,0|54,289,288|53,0,290|53,290,0|52,292,291|51,0,293|60,284,0|57,0,295|56,0,296|55,0,297|55,297,0|54,299,298|53,0,300|53,300,0|52,302,301|51,303,0|50,304,294|49,305,0|48,306,0|45,0,307|62,282,0|61,0,309|60,0,310|57,0,311|56,0,312|55,0,313|55,313,0|54,315,314|53,0,316|53,316,0|52,318,317|51,0,319|60,310,0|57,0,321|56,0,322|55,0,323|55,323,0|54,325,324|53,0,326|53,326,0|52,328,327|51,329,0|50,330,320|49,331,0|48,332,0|46,333,0|45,334,0|44,335,308|43,0,336|43,336,0|42,338,337|41,0,339|40,0,340|60,283,0|57,0,342|56,0,343|55,344,0|54,345,298|53,0,346|53,346,0|52,348,347|51,349,0|50,350,294|49,351,0|48,352,0|45,0,353|61,309,0|60,355,0|57,0,356|56,0,357|55,358,0|54,359,324|53,0,360|53,360,0|52,362,361|51,363,0|50,364,320|49,365,0|48,366,0|46,367,0|45,368,0|44,369,354|43,370,0|42,371,337|41,0,372|40,373,0|39,374,341|38,375,257|34,0,376|33,377,188|32,0,378|31,0,379|27,0,380|63,0,7|62,0,382|61,0,383|60,0,384|57,0,385|56,0,386|55,0,387|55,387,0|54,389,388|53,0,390|53,390,0|52,392,391|51,0,393|60,384,0|57,0,395|56,0,396|55,0,397|55,397,0|54,399,398|53,0,400|53,400,0|52,402,401|51,403,0|50,404,394|49,405,0|48,406,0|45,0,407|44,0,408|43,0,409|43,409,0|42,411,410|41,0,412|40,0,413|60,383,0|57,0,415|56,0,416|55,417,0|54,418,398|53,0,419|53,419,0|52,421,420|51,422,0|50,423,394|49,424,0|48,425,0|45,0,426|44,0,427|43,428,0|42,429,410|41,0,430|40,431,0|39,432,414|34,0,433|63,0,193|62,0,435|61,0,436|60,0,437|57,0,438|56,0,439|55,0,440|55,440,0|54,442,441|53,0,443|53,443,0|52,445,444|51,0,446|60,437,0|57,0,448|56,0,449|55,0,450|55,450,0|54,452,451|53,0,453|53,453,0|52,455,454|51,456,0|50,457,447|49,458,0|48,459,0|45,0,460|44,0,461|43,0,462|43,462,0|42,464,463|41,0,465|40,0,466|60,436,0|57,0,468|56,0,469|55,470,0|54,471,451|53,0,472|53,472,0|52,474,473|51,475,0|50,476,447|49,477,0|48,478,0|45,0,479|44,0,480|43,481,0|42,482,463|41,0,483|40,484,0|39,485,467|34,0,486|33,487,434|32,0,488|31,0,489|27,0,490|23,491,381|78,1,0|77,493,0|76,0,494|75,0,495|74,496,0|73,497,0|72,498,0|76,494,0|75,500,0|74,501,0|73,502,0|72,503,0|71,504,499|70,505,0|69,0,506|68,0,507|67,0,508|66,0,509|65,0,510|64,0,511|63,0,512|62,0,513|61,0,514|60,0,515|57,516,0|56,517,97|55,0,518|55,518,0|54,520,519|53,0,521|53,521,0|52,523,522|51,0,524|60,515,0|57,526,0|56,527,107|55,0,528|55,528,0|54,530,529|53,0,531|53,531,0|52,533,532|51,534,0|50,535,525|49,536,0|48,537,0|45,0,538|44,146,539|43,0,540|43,540,0|42,542,541|41,0,543|40,0,544|60,514,0|57,546,0|56,547,154|55,548,0|54,549,529|53,0,550|53,550,0|52,552,551|51,553,0|50,554,525|49,555,0|48,556,0|45,0,557|44,180,558|43,559,0|42,560,541|41,0,561|40,562,0|39,563,545|38,564,68|37,565,187|36,566,187|34,0,567|76,0,493|75,0,569|74,570,0|73,571,0|72,572,0|76,493,0|75,574,0|74,575,0|73,576,0|72,577,0|71,578,573|70,579,0|69,0,580|68,0,581|67,0,582|66,0,583|65,0,584|64,0,585|63,0,586|62,0,587|61,0,588|60,0,589|57,590,0|56,591,286|55,0,592|55,592,0|54,594,593|53,0,595|53,595,0|52,597,596|51,0,598|60,589,0|57,600,0|56,601,296|55,0,602|55,602,0|54,604,603|53,0,605|53,605,0|52,607,606|51,608,0|50,609,599|49,610,0|48,611,0|71,0,499|70,613,0|69,0,614|68,0,615|67,616,0|66,0,617|65,0,618|64,0,619|63,620,0|62,621,587|61,0,622|60,0,623|59,590,624|58,590,625|57,626,0|56,627,286|55,0,628|55,628,0|54,630,629|53,0,631|53,631,0|52,633,632|51,0,634|60,623,0|59,600,636|58,600,637|57,638,0|56,639,296|55,0,640|55,640,0|54,642,641|53,0,643|53,643,0|52,645,644|51,646,0|50,647,635|49,648,0|48,649,0|47,612,650|46,651,612|45,0,652|62,621,0|61,0,654|60,0,655|59,0,656|58,0,657|57,658,0|56,659,312|55,0,660|55,660,0|54,662,661|53,0,663|53,663,0|52,665,664|51,0,666|60,655,0|59,0,668|58,0,669|57,670,0|56,671,322|55,0,672|55,672,0|54,674,673|53,0,675|53,675,0|52,677,676|51,678,0|50,679,667|49,680,0|48,681,0|47,333,682|46,683,0|45,684,0|44,685,653|43,0,686|43,686,0|42,688,687|41,0,689|40,0,690|60,588,0|57,692,0|56,693,343|55,694,0|54,695,603|53,0,696|53,696,0|52,698,697|51,699,0|50,700,599|49,701,0|48,702,0|61,622,588|60,704,0|59,692,705|58,692,706|57,707,0|56,708,343|55,709,0|54,710,641|53,0,711|53,711,0|52,713,712|51,714,0|50,715,635|49,716,0|48,717,0|47,703,718|46,719,703|45,0,720|61,654,0|60,722,0|59,0,723|58,0,724|57,725,0|56,726,357|55,727,0|54,728,673|53,0,729|53,729,0|52,731,730|51,732,0|50,733,667|49,734,0|48,735,0|47,367,736|46,737,0|45,738,0|44,739,721|43,740,0|42,741,687|41,0,742|40,743,0|39,744,691|38,745,257|37,746,376|36,747,376|45,0,612|44,335,749|43,0,750|43,750,0|42,752,751|41,0,753|40,0,754|45,0,703|44,369,756|43,757,0|42,758,751|41,0,759|40,760,0|39,761,755|38,762,257|37,763,376|36,764,376|35,765,748|34,0,766|33,767,568|32,0,768|31,0,769|34,0,765|33,771,568|32,0,772|31,0,773|28,774,770|27,0,775|27,0,774|26,777,776|25,778,381|25,777,381|24,780,779|71,504,0|70,782,0|69,783,0|68,784,0|67,785,0|66,786,0|65,787,0|64,788,0|63,789,0|62,790,435|61,0,791|60,0,792|59,438,793|58,438,794|57,0,795|62,790,0|61,0,797|60,0,798|59,0,799|58,0,800|57,801,0|56,802,796|55,0,803|55,803,0|54,805,804|53,0,806|53,806,0|52,808,807|51,0,809|60,792,0|59,448,811|58,448,812|57,0,813|60,798,0|59,0,815|58,0,816|57,817,0|56,818,814|55,0,819|55,819,0|54,821,820|53,0,822|53,822,0|52,824,823|51,825,0|50,826,810|49,827,0|48,828,0|47,460,829|46,830,460|45,0,831|57,0,801|56,802,833|55,0,834|55,834,0|54,836,835|53,0,837|53,837,0|52,839,838|51,0,840|57,0,817|56,818,842|55,0,843|55,843,0|54,845,844|53,0,846|53,846,0|52,848,847|51,849,0|50,850,841|49,851,0|48,852,0|47,0,853|46,854,0|45,855,0|44,856,832|43,0,857|43,857,0|42,859,858|41,0,860|40,0,861|61,791,436|60,863,0|59,468,864|58,468,865|57,0,866|61,797,0|60,868,0|59,0,869|58,0,870|57,871,0|56,872,867|55,873,0|54,874,820|53,0,875|53,875,0|52,877,876|51,878,0|50,879,810|49,880,0|48,881,0|47,479,882|46,883,479|45,0,884|57,0,871|56,872,886|55,887,0|54,888,844|53,0,889|53,889,0|52,891,890|51,892,0|50,893,841|49,894,0|48,895,0|47,0,896|46,897,0|45,898,0|44,899,885|43,900,0|42,901,858|41,0,902|40,903,0|39,904,862|38,486,905|37,906,486|36,907,486|35,486,908|34,0,909|33,910,434|32,0,911|31,0,912|28,490,913|27,0,914|26,491,915|25,916,491|24,491,917|23,918,781|22,919,492|21,920,492|20,921,492|23,491,780|22,923,492|21,924,492|20,925,492|19,926,922|54,53,0|53,928,0|52,929,0|51,930,0|50,931,0|49,932,0|48,933,0|45,0,934|44,0,935|43,936,0|42,937,0|41,0,938|40,939,0|39,940,0|54,156,0|53,942,0|52,943,0|51,944,0|50,945,0|49,946,0|48,947,0|45,0,948|54,170,0|53,950,0|52,951,0|51,952,0|50,953,0|49,954,0|48,955,0|46,956,0|45,957,0|44,958,949|43,959,0|42,960,0|41,0,961|40,962,0|39,963,0|38,964,941|34,0,965|54,242,0|53,967,0|52,968,0|51,969,0|50,970,0|49,971,0|48,972,0|45,0,973|44,0,974|43,975,0|42,976,0|41,0,977|40,978,0|39,979,0|54,345,0|53,981,0|52,982,0|51,983,0|50,984,0|49,985,0|48,986,0|45,0,987|54,359,0|53,989,0|52,990,0|51,991,0|50,992,0|49,993,0|48,994,0|46,995,0|45,996,0|44,997,988|43,998,0|42,999,0|41,0,1000|40,1001,0|39,1002,0|38,1003,980|34,0,1004|33,1005,966|32,0,1006|31,0,1007|27,0,1008|54,418,0|53,1010,0|52,1011,0|51,1012,0|50,1013,0|49,1014,0|48,1015,0|45,0,1016|44,0,1017|43,1018,0|42,1019,0|41,0,1020|40,1021,0|39,1022,0|34,0,1023|54,471,0|53,1025,0|52,1026,0|51,1027,0|50,1028,0|49,1029,0|48,1030,0|45,0,1031|44,0,1032|43,1033,0|42,1034,0|41,0,1035|40,1036,0|39,1037,0|34,0,1038|33,1039,1024|32,0,1040|31,0,1041|27,0,1042|23,1043,1009|54,549,0|53,1045,0|52,1046,0|51,1047,0|50,1048,0|49,1049,0|48,1050,0|45,0,1051|44,958,1052|43,1053,0|42,1054,0|41,0,1055|40,1056,0|39,1057,0|38,1058,941|37,1059,965|36,1060,965|34,0,1061|54,695,0|53,1063,0|52,1064,0|51,1065,0|50,1066,0|49,1067,0|48,1068,0|45,0,1069|44,997,1070|43,1071,0|42,1072,0|41,0,1073|40,1074,0|39,1075,0|38,1076,980|37,1077,1004|36,1078,1004|34,0,1079|33,1080,1062|32,0,1081|31,0,1082|27,0,1083|25,1084,1009|23,1043,1085|22,1086,1044|21,1087,1044|20,1088,1044|18,1089,927|17,1089,1090|38,375,68|34,0,1092|33,377,1093|32,0,1094|31,0,1095|76,0,194|75,189,1097|74,1098,190|73,1099,190|72,1100,190|71,190,1101|69,191,1102|68,192,1103|67,0,1104|66,193,1105|65,193,1106|64,204,1107|63,0,1108|62,282,1109|61,0,1110|60,0,1111|57,0,1112|56,0,1113|55,0,1114|55,1114,0|54,1116,1115|53,0,1117|53,1117,0|52,1119,1118|51,0,1120|60,1111,0|57,0,1122|56,0,1123|55,0,1124|55,1124,0|54,1126,1125|53,0,1127|53,1127,0|52,1129,1128|51,1130,0|50,1131,1121|49,1132,0|48,1133,0|45,0,1134|44,335,1135|43,0,1136|43,1136,0|42,1138,1137|41,0,1139|40,0,1140|60,1110,0|57,0,1142|56,0,1143|55,1144,0|54,1145,1125|53,0,1146|70,1102,263|69,191,1148|68,192,1149|67,0,1150|66,193,1151|65,193,1152|64,204,1153|63,0,1154|62,282,1155|60,1156,0|57,0,1157|56,0,1158|55,1159,0|54,1160,1125|53,1161,0|52,1162,1147|51,1163,0|50,1164,1121|49,1165,0|48,1166,0|45,0,1167|44,369,1168|43,1169,0|42,1170,1137|41,0,1171|40,1172,0|39,1173,1141|38,1174,257|34,0,1175|33,1176,1093|32,0,1177|31,0,1178|28,1179,1096|27,0,1180|38,486,433|34,0,1182|33,487,1183|32,0,1184|31,0,1185|68,192,200|67,0,1187|66,1188,193|70,196,190|70,196,0|69,1191,1190|68,192,1192|67,0,1193|66,1194,193|65,1195,1189|67,0,200|66,1188,1197|65,193,1198|64,1199,1196|63,0,1200|62,0,1201|61,0,1202|60,0,1203|57,0,1204|56,0,1205|55,0,1206|55,1206,0|54,1208,1207|53,0,1209|53,1209,0|52,1211,1210|51,0,1212|60,1203,0|57,0,1214|56,0,1215|55,0,1216|55,1216,0|54,1218,1217|53,0,1219|53,1219,0|52,1221,1220|51,1222,0|50,1223,1213|49,1224,0|48,1225,0|45,0,1226|44,0,1227|43,0,1228|43,1228,0|42,1230,1229|41,0,1231|40,0,1232|60,1202,0|57,0,1234|56,0,1235|55,1236,0|54,1237,1217|53,0,1238|53,1238,0|52,1240,1239|51,1241,0|50,1242,1213|49,1243,0|48,1244,0|45,0,1245|44,0,1246|43,1247,0|42,1248,1229|41,0,1249|40,1250,0|39,1251,1233|38,1252,486|34,0,1253|33,1254,1183|32,0,1255|31,0,1256|28,1257,1186|27,0,1258|23,1259,1181|54,471,1217|53,1261,0|52,1262,1239|51,1263,0|50,1264,1213|49,1265,0|48,1266,0|45,0,1267|44,0,1268|43,1269,0|42,1270,1229|41,0,1271|40,1272,0|39,1273,1233|38,1274,486|34,0,1275|33,1276,1183|32,0,1277|31,0,1278|28,1279,1186|27,0,1280|23,1281,1181|22,1282,1260|21,1283,1260|54,345,1125|53,1285,0|52,1286,1147|51,1287,0|50,1288,1121|49,1289,0|48,1290,0|45,0,1291|44,369,1292|43,1293,0|42,1294,1137|41,0,1295|40,1296,0|39,1297,1141|38,1298,257|34,0,1299|33,1300,1093|32,0,1301|31,0,1302|28,1303,1096|27,0,1304|23,1281,1305|38,762,68|37,1307,1092|36,1308,1092|34,0,1309|33,771,1310|32,0,1311|31,0,1312|77,0,493|76,0,1314|75,0,1315|74,1316,0|73,1317,0|72,1318,0|76,1314,0|75,1320,0|74,1321,0|73,1322,0|72,1323,0|71,1324,1319|70,1325,0|69,0,1326|68,0,1327|67,0,1328|66,0,1329|65,0,1330|64,0,1331|63,0,1332|62,0,1333|61,0,1334|60,0,1335|57,1336,0|56,1337,1113|55,0,1338|55,1338,0|54,1340,1339|53,0,1341|53,1341,0|52,1343,1342|51,0,1344|60,1335,0|57,1346,0|56,1347,1123|55,0,1348|55,1348,0|54,1350,1349|53,0,1351|53,1351,0|52,1353,1352|51,1354,0|50,1355,1345|49,1356,0|48,1357,0|45,0,1358|44,335,1359|43,0,1360|43,1360,0|42,1362,1361|41,0,1363|40,0,1364|60,1334,0|57,1366,0|56,1367,1143|55,1368,0|54,1369,1349|53,0,1370|54,695,1349|53,1372,0|52,1373,1371|51,1374,0|50,1375,1345|49,1376,0|48,1377,0|45,0,1378|44,369,1379|43,1380,0|42,1381,1361|41,0,1382|40,1383,0|39,1384,1365|38,1385,257|37,1386,1299|36,1387,1299|34,0,1388|33,1389,1310|32,0,1390|31,0,1391|28,1392,1313|27,0,1393|25,1394,1305|23,1281,1395|22,1396,1306|21,1397,1306|20,1398,1284|38,1003,941|34,0,1400|33,1005,1401|32,0,1402|31,0,1403|54,1160,0|53,1405,0|52,1406,0|51,1407,0|50,1408,0|49,1409,0|48,1410,0|45,0,1411|44,997,1412|43,1413,0|42,1414,0|41,0,1415|40,1416,0|39,1417,0|38,1418,980|34,0,1419|33,1420,1401|32,0,1421|31,0,1422|28,1423,1404|27,0,1424|38,1038,1023|34,0,1426|33,1039,1427|32,0,1428|31,0,1429|54,1237,0|53,1431,0|52,1432,0|51,1433,0|50,1434,0|49,1435,0|48,1436,0|45,0,1437|44,0,1438|43,1439,0|42,1440,0|41,0,1441|40,1442,0|39,1443,0|38,1444,1038|34,0,1445|33,1446,1427|32,0,1447|31,0,1448|28,1449,1430|27,0,1450|23,1451,1425|27,0,1430|23,1453,1425|22,1454,1452|21,1455,1452|27,0,1404|23,1453,1457|38,1076,941|37,1459,1400|36,1460,1400|34,0,1461|33,1080,1462|32,0,1463|31,0,1464|27,0,1465|25,1466,1457|23,1453,1467|22,1468,1458|21,1469,1458|20,1470,1456|18,1471,1399|77,493,1|76,1473,0|75,1474,0|72,190,1475|70,1476,190|70,1476,0|69,1478,1477|68,192,1479|67,0,1480|66,1481,193|70,1475,190|70,1475,0|69,1484,1483|68,192,1485|67,0,1486|66,1487,193|65,1488,1482|67,0,1479|66,1481,1490|65,193,1491|64,1492,1489|63,0,1493|62,0,1494|60,1495,0|57,0,1496|56,0,1497|55,1498,0|54,1499,0|53,1500,0|52,1501,0|51,1502,0|50,1503,0|49,1504,0|48,1505,0|45,0,1506|44,0,1507|43,1508,0|42,1509,0|41,0,1510|40,1511,0|39,1512,0|38,1513,1038|34,0,1514|33,1515,1427|32,0,1516|31,0,1517|28,1518,1430|27,0,1519|23,1520,1425|22,1521,1452|21,1522,1452|20,1470,1523|17,1524,1472|16,1525,1091|61,1334,588|60,1527,0|57,1528,0|56,1529,343|55,1530,0|54,1531,0|53,1532,0|52,1533,0|51,1534,0|50,1535,0|49,1536,0|48,1537,0|46,1069,1538|45,0,1539|44,997,1540|43,1541,0|42,1542,0|41,0,1543|40,1544,0|39,1545,0|38,1546,980|37,1547,1004|36,1548,1004|34,0,1549|33,1550,1462|32,0,1551|31,0,1552|28,1553,1465|27,0,1554|25,1555,1457|23,1453,1556|22,1557,1458|21,1558,1458|20,1559,1456|17,1524,1560|16,1561,1089|15,1562,1526|61,514,0|60,1564,0|57,1565,0|56,1566,154|55,1567,0|54,1568,0|53,1569,0|52,1570,0|51,1571,0|50,1572,0|49,1573,0|48,1574,0|47,1575,1051|46,1576,1051|45,0,1577|44,958,1578|43,1579,0|42,1580,0|41,0,1581|40,1582,0|39,1583,0|38,1584,941|37,1585,965|36,1586,965|34,0,1587|33,1080,1588|32,0,1589|31,0,1590|27,0,1591|25,1592,1009|23,1043,1593|22,1594,1044|21,1595,1044|20,1596,1044|58,0,1565|57,1598,0|56,1599,154|55,1600,0|54,1601,0|53,1602,0|52,1603,0|51,1604,0|50,1605,0|49,1606,0|48,1607,0|47,1608,1051|46,1609,1051|45,0,1610|44,958,1611|43,1612,0|42,1613,0|41,0,1614|40,1615,0|39,1616,0|38,1617,941|37,1618,965|36,1619,965|34,0,1620|33,1080,1621|32,0,1622|31,0,1623|27,0,1624|25,1625,1009|23,1043,1626|22,1627,1044|21,1628,1044|20,1629,1044|19,1630,1597|17,1631,1089|17,1524,1471|16,1633,1632|16,1633,1089|15,1635,1634|14,1636,1563|18,1089,926|17,1089,1638|16,1525,1639|15,1562,1640|14,1636,1641|13,1642,1637|17,1597,1089|16,1633,1644|15,1635,1645|14,1646,1641|12,1647,1643|38,1023,941|34,0,1649|38,1038,980|34,0,1651|33,1652,1650|32,0,1653|31,0,1654|27,0,1655|23,1043,1656|38,1038,941|34,0,1658|33,1652,1659|32,0,1660|31,0,1661|34,0,980|33,1663,1659|32,0,1664|31,0,1665|28,1666,1662|27,0,1667|23,1451,1668|23,1453,1668|22,1670,1669|21,1671,1669|27,0,1662|23,1453,1673|20,1674,1672|16,1675,1657|11,1676,1648|10,0,1677|48,0,40|45,0,1679|44,0,1680|43,0,1681|43,1681,0|42,1683,1682|41,1684,0|40,0,1685|53,0,928|52,929,1687|51,1688,0|50,1689,0|48,1690,59|45,0,1691|44,0,1692|43,1693,0|42,1694,1682|41,1695,0|40,1696,0|39,1697,1686|48,0,116|45,0,1699|48,0,142|46,1701,0|45,1702,0|44,1703,1700|43,0,1704|43,1704,0|42,1706,1705|41,1707,0|40,0,1708|53,0,942|52,943,1710|51,1711,0|50,1712,0|48,1713,162|45,0,1714|54,0,135|53,0,1716|53,1716,0|52,1718,1717|51,1719,0|50,1720,131|53,0,950|52,951,1722|51,1723,0|50,1724,0|49,1725,0|48,1726,1721|46,1727,0|45,1728,0|44,1729,1715|43,1730,0|42,1731,1705|41,1732,0|40,1733,0|39,1734,1709|38,1735,1698|45,0,932|44,0,1737|43,1738,0|42,1739,0|41,1740,0|40,1741,0|39,1742,0|45,0,946|44,958,1744|43,1745,0|42,1746,0|41,1747,0|40,1748,0|39,1749,0|38,1750,1743|34,1751,1736|48,0,229|45,0,1753|44,0,1754|43,0,1755|43,1755,0|42,1757,1756|41,1758,0|40,0,1759|53,0,967|52,968,1761|51,1762,0|50,1763,0|48,1764,248|45,0,1765|44,0,1766|43,1767,0|42,1768,1756|41,1769,0|40,1770,0|39,1771,1760|48,0,305|45,0,1773|48,0,331|46,1775,0|45,1776,0|44,1777,1774|43,0,1778|43,1778,0|42,1780,1779|41,1781,0|40,0,1782|53,0,981|52,982,1784|51,1785,0|50,1786,0|48,1787,351|45,0,1788|54,0,324|53,0,1790|53,1790,0|52,1792,1791|51,1793,0|50,1794,320|53,0,989|52,990,1796|51,1797,0|50,1798,0|49,1799,0|48,1800,1795|46,1801,0|45,1802,0|44,1803,1789|43,1804,0|42,1805,1779|41,1806,0|40,1807,0|39,1808,1783|38,1809,1772|45,0,971|44,0,1811|43,1812,0|42,1813,0|41,1814,0|40,1815,0|39,1816,0|45,0,985|44,997,1818|43,1819,0|42,1820,0|41,1821,0|40,1822,0|39,1823,0|38,1824,1817|34,1825,1810|33,1826,1752|32,0,1827|31,0,1828|27,0,1829|48,0,405|45,0,1831|44,0,1832|43,0,1833|43,1833,0|42,1835,1834|41,1836,0|40,0,1837|53,0,1010|52,1011,1839|51,1840,0|50,1841,0|48,1842,424|45,0,1843|44,0,1844|43,1845,0|42,1846,1834|41,1847,0|40,1848,0|39,1849,1838|45,0,1014|44,0,1851|43,1852,0|42,1853,0|41,1854,0|40,1855,0|39,1856,0|34,1857,1850|48,0,458|45,0,1859|44,0,1860|43,0,1861|43,1861,0|42,1863,1862|41,1864,0|40,0,1865|53,0,1025|52,1026,1867|51,1868,0|50,1869,0|48,1870,477|45,0,1871|44,0,1872|43,1873,0|42,1874,1862|41,1875,0|40,1876,0|39,1877,1866|45,0,1029|44,0,1879|43,1880,0|42,1881,0|41,1882,0|40,1883,0|39,1884,0|34,1885,1878|33,1886,1858|32,0,1887|31,0,1888|27,0,1889|23,1890,1830|48,0,536|45,0,1892|44,1703,1893|43,0,1894|43,1894,0|42,1896,1895|41,1897,0|40,0,1898|53,0,1045|52,1046,1900|51,1901,0|50,1902,0|48,1903,555|45,0,1904|44,1729,1905|43,1906,0|42,1907,1895|41,1908,0|40,1909,0|39,1910,1899|38,1911,1698|37,1912,1736|36,1913,1736|45,0,1049|44,958,1915|43,1916,0|42,1917,0|41,1918,0|40,1919,0|39,1920,0|38,1921,1743|37,1922,1751|36,1923,1751|34,1924,1914|48,0,610|49,610,648|48,0,1927|47,1926,1928|46,1929,1926|45,0,1930|49,331,680|48,0,1932|47,1775,1933|46,1934,0|45,1935,0|44,1936,1931|43,0,1937|43,1937,0|42,1939,1938|41,1940,0|40,0,1941|53,0,1063|52,1064,1943|51,1944,0|50,1945,0|48,1946,701|54,695,641|53,0,1948|53,1948,0|52,1950,1949|51,1951,0|50,1952,635|49,701,1953|54,710,0|53,0,1955|53,1955,0|52,1957,1956|51,1958,0|50,1959,0|49,1960,1946|48,1961,1954|47,1947,1962|46,1963,1947|45,0,1964|54,0,673|53,0,1966|53,1966,0|52,1968,1967|51,1969,0|50,1970,667|49,1795,1971|54,728,0|53,0,1973|53,1973,0|52,1975,1974|51,1976,0|50,1977,0|49,1978,0|48,1979,1972|47,1801,1980|46,1981,0|45,1982,0|44,1983,1965|43,1984,0|42,1985,1938|41,1986,0|40,1987,0|39,1988,1942|38,1989,1772|37,1990,1810|36,1991,1810|45,0,1926|44,1777,1993|43,0,1994|43,1994,0|42,1996,1995|41,1997,0|40,0,1998|45,0,1947|44,1803,2000|43,2001,0|42,2002,1995|41,2003,0|40,2004,0|39,2005,1999|38,2006,1772|37,2007,1810|36,2008,1810|35,2009,1992|45,0,1067|44,997,2011|43,2012,0|42,2013,0|41,2014,0|40,2015,0|39,2016,0|38,2017,1817|37,2018,1825|36,2019,1825|34,2020,2010|33,2021,1925|32,0,2022|31,0,2023|34,2020,2009|33,2025,1925|32,0,2026|31,0,2027|28,2028,2024|27,0,2029|27,0,2028|26,2031,2030|25,2032,1830|25,2031,1830|24,2034,2033|49,458,827|48,0,2036|47,1859,2037|46,2038,1859|45,0,2039|49,0,851|48,0,2041|47,0,2042|46,2043,0|45,2044,0|44,2045,2040|43,0,2046|43,2046,0|42,2048,2047|41,2049,0|40,0,2050|54,471,820|53,0,2052|53,2052,0|52,2054,2053|51,2055,0|50,2056,810|49,477,2057|54,874,0|53,0,2059|53,2059,0|52,2061,2060|51,2062,0|50,2063,0|49,2064,1870|48,2065,2058|47,1871,2066|46,2067,1871|45,0,2068|54,0,844|53,0,2070|53,2070,0|52,2072,2071|51,2073,0|50,2074,841|49,0,2075|54,888,0|53,0,2077|53,2077,0|52,2079,2078|51,2080,0|50,2081,0|49,2082,0|48,2083,2076|47,0,2084|46,2085,0|45,2086,0|44,2087,2069|43,2088,0|42,2089,2047|41,2090,0|40,2091,0|39,2092,2051|38,1878,2093|37,2094,1878|36,2095,1878|35,1878,2096|34,1885,2097|33,2098,1858|32,0,2099|31,0,2100|28,1889,2101|27,0,2102|26,1890,2103|25,2104,1890|24,1890,2105|23,2106,2035|22,2107,1891|21,2108,1891|20,2109,1891|23,1890,2034|22,2111,1891|21,2112,1891|20,2113,1891|19,2114,2110|33,1825,1751|32,0,2116|31,0,2117|27,0,2118|33,1885,1857|32,0,2120|31,0,2121|27,0,2122|23,2123,2119|33,2020,1924|32,0,2125|31,0,2126|27,0,2127|25,2128,2119|23,2123,2129|22,2130,2124|21,2131,2124|20,2132,2124|18,2133,2115|17,2133,2134|38,1809,1698|38,1824,1743|34,2137,2136|33,1826,2138|32,0,2139|31,0,2140|48,0,1132|45,0,2142|44,1777,2143|43,0,2144|43,2144,0|42,2146,2145|41,2147,0|40,0,2148|54,1145,0|53,0,2150|52,1406,2151|51,2152,0|50,2153,0|48,2154,1165|45,0,2155|44,1803,2156|43,2157,0|42,2158,2145|41,2159,0|40,2160,0|39,2161,2149|38,2162,1772|45,0,1409|44,997,2164|43,2165,0|42,2166,0|41,2167,0|40,2168,0|39,2169,0|38,2170,1817|34,2171,2163|33,2172,2138|32,0,2173|31,0,2174|28,2175,2141|27,0,2176|38,1878,1850|38,1885,1857|34,2179,2178|33,1886,2180|32,0,2181|31,0,2182|48,0,1224|45,0,2184|44,0,2185|43,0,2186|43,2186,0|42,2188,2187|41,2189,0|40,0,2190|53,0,1431|52,1432,2192|51,2193,0|50,2194,0|48,2195,1243|45,0,2196|44,0,2197|43,2198,0|42,2199,2187|41,2200,0|40,2201,0|39,2202,2191|38,2203,1878|45,0,1435|44,0,2205|43,2206,0|42,2207,0|41,2208,0|40,2209,0|39,2210,0|38,2211,1885|34,2212,2204|33,2213,2180|32,0,2214|31,0,2215|28,2216,2183|27,0,2217|23,2218,2177|52,1026,2192|51,2220,0|50,2221,0|48,2222,1265|45,0,2223|44,0,2224|43,2225,0|42,2226,2187|41,2227,0|40,2228,0|39,2229,2191|38,2230,1878|34,1885,2231|33,2232,2180|32,0,2233|31,0,2234|28,2235,2183|27,0,2236|23,2237,2177|22,2238,2219|21,2239,2219|52,982,2151|51,2241,0|50,2242,0|48,2243,1289|45,0,2244|44,1803,2245|43,2246,0|42,2247,2145|41,2248,0|40,2249,0|39,2250,2149|38,2251,1772|34,1825,2252|33,2253,2138|32,0,2254|31,0,2255|28,2256,2141|27,0,2257|23,2237,2258|38,2006,1698|37,2260,2136|36,2261,2136|38,2017,1743|37,2263,2137|36,2264,2137|34,2265,2262|33,2025,2266|32,0,2267|31,0,2268|48,0,1356|45,0,2270|44,1777,2271|43,0,2272|43,2272,0|42,2274,2273|41,2275,0|40,0,2276|54,1369,0|53,0,2278|52,1064,2279|51,2280,0|50,2281,0|48,2282,1376|45,0,2283|44,1803,2284|43,2285,0|42,2286,2273|41,2287,0|40,2288,0|39,2289,2277|38,2290,1772|37,2291,2252|36,2292,2252|34,2020,2293|33,2294,2266|32,0,2295|31,0,2296|28,2297,2269|27,0,2298|25,2299,2258|23,2237,2300|22,2301,2259|21,2302,2259|20,2303,2240|33,1825,2137|32,0,2305|31,0,2306|33,2171,2137|32,0,2308|31,0,2309|28,2310,2307|27,0,2311|33,1885,2179|32,0,2313|31,0,2314|33,2212,2179|32,0,2316|31,0,2317|28,2318,2315|27,0,2319|23,2320,2312|27,0,2315|23,2322,2312|22,2323,2321|21,2324,2321|27,0,2307|23,2322,2326|33,2020,2265|32,0,2328|31,0,2329|27,0,2330|25,2331,2326|23,2322,2332|22,2333,2327|21,2334,2327|20,2335,2325|18,2336,2304|45,0,1504|44,0,2338|43,2339,0|42,2340,0|41,2341,0|40,2342,0|39,2343,0|38,2344,1885|33,2345,2179|32,0,2346|31,0,2347|28,2348,2315|27,0,2349|23,2350,2312|22,2351,2321|21,2352,2321|20,2335,2353|17,2354,2337|16,2355,2135|46,1067,1536|45,0,2357|44,997,2358|43,2359,0|42,2360,0|41,2361,0|40,2362,0|39,2363,0|38,2364,1817|37,2365,1825|36,2366,1825|33,2367,2265|32,0,2368|31,0,2369|28,2370,2330|27,0,2371|25,2372,2326|23,2322,2373|22,2374,2327|21,2375,2327|20,2376,2325|17,2354,2377|16,2378,2133|15,2379,2356|47,1573,1049|46,2381,1049|45,0,2382|44,958,2383|43,2384,0|42,2385,0|41,2386,0|40,2387,0|39,2388,0|38,2389,1743|37,2390,1751|36,2391,1751|33,2020,2392|32,0,2393|31,0,2394|27,0,2395|25,2396,2119|23,2123,2397|22,2398,2124|21,2399,2124|20,2400,2124|47,1606,1049|46,2402,1049|45,0,2403|44,958,2404|43,2405,0|42,2406,0|41,2407,0|40,2408,0|39,2409,0|38,2410,1743|37,2411,1751|36,2412,1751|33,2020,2413|32,0,2414|31,0,2415|27,0,2416|25,2417,2119|23,2123,2418|22,2419,2124|21,2420,2124|20,2421,2124|19,2422,2401|17,2423,2133|17,2354,2336|16,2425,2424|16,2425,2133|15,2427,2426|14,2428,2380|18,2133,2114|17,2133,2430|16,2355,2431|15,2379,2432|14,2428,2433|13,2434,2429|17,2401,2133|16,2425,2436|15,2427,2437|14,2438,2433|12,2439,2435|38,1857,1743|38,1885,1817|33,2442,2441|32,0,2443|31,0,2444|27,0,2445|23,2123,2446|38,1885,1743|33,2442,2448|32,0,2449|31,0,2450|33,1817,2448|32,0,2452|31,0,2453|28,2454,2451|27,0,2455|23,2320,2456|23,2322,2456|22,2458,2457|21,2459,2457|27,0,2451|23,2322,2461|20,2462,2460|16,2463,2447|11,2464,2440|10,2465,0|9,2466,1678|8,0,2467|46,42,0|45,0,2469|44,0,2470|43,0,2471|43,2471,0|42,2473,2472|41,0,2474|40,0,2475|61,18,0|60,2477,0|57,0,2478|56,0,2479|55,2480,0|54,2481,33|53,0,2482|53,2482,0|52,2484,2483|51,2485,0|50,2486,29|49,2487,0|48,2488,0|46,2489,0|45,0,2490|44,0,2491|43,2492,0|42,2493,2472|41,0,2494|40,2495,0|39,2496,2476|46,118,0|45,0,2498|44,146,2499|43,0,2500|43,2500,0|42,2502,2501|41,0,2503|40,0,2504|61,94,0|60,2506,0|57,0,2507|56,0,2508|55,2509,0|54,2510,109|53,0,2511|53,2511,0|52,2513,2512|51,2514,0|50,2515,105|49,2516,0|48,2517,0|46,2518,0|45,0,2519|44,180,2520|43,2521,0|42,2522,2501|41,0,2523|40,2524,0|39,2525,2505|38,2526,2497|34,0,2527|46,231,0|45,0,2529|44,0,2530|43,0,2531|43,2531,0|42,2533,2532|41,0,2534|40,0,2535|61,207,0|60,2537,0|57,0,2538|56,0,2539|55,2540,0|54,2541,222|53,0,2542|53,2542,0|52,2544,2543|51,2545,0|50,2546,218|49,2547,0|48,2548,0|46,2549,0|45,0,2550|44,0,2551|43,2552,0|42,2553,2532|41,0,2554|40,2555,0|39,2556,2536|46,307,0|45,0,2558|44,335,2559|43,0,2560|43,2560,0|42,2562,2561|41,0,2563|40,0,2564|61,283,0|60,2566,0|57,0,2567|56,0,2568|55,2569,0|54,2570,298|53,0,2571|53,2571,0|52,2573,2572|51,2574,0|50,2575,294|49,2576,0|48,2577,0|46,2578,0|45,0,2579|44,369,2580|43,2581,0|42,2582,2561|41,0,2583|40,2584,0|39,2585,2565|38,2586,2557|34,0,2587|33,2588,2528|32,0,2589|31,0,2590|27,0,2591|46,407,0|45,0,2593|44,0,2594|43,0,2595|43,2595,0|42,2597,2596|41,0,2598|40,0,2599|61,383,0|60,2601,0|57,0,2602|56,0,2603|55,2604,0|54,2605,398|53,0,2606|53,2606,0|52,2608,2607|51,2609,0|50,2610,394|49,2611,0|48,2612,0|46,2613,0|45,0,2614|44,0,2615|43,2616,0|42,2617,2596|41,0,2618|40,2619,0|39,2620,2600|34,0,2621|46,460,0|45,0,2623|44,0,2624|43,0,2625|43,2625,0|42,2627,2626|41,0,2628|40,0,2629|61,436,0|60,2631,0|57,0,2632|56,0,2633|55,2634,0|54,2635,451|53,0,2636|53,2636,0|52,2638,2637|51,2639,0|50,2640,447|49,2641,0|48,2642,0|46,2643,0|45,0,2644|44,0,2645|43,2646,0|42,2647,2626|41,0,2648|40,2649,0|39,2650,2630|34,0,2651|33,2652,2622|32,0,2653|31,0,2654|27,0,2655|23,2656,2592|46,538,0|45,0,2658|44,146,2659|43,0,2660|43,2660,0|42,2662,2661|41,0,2663|40,0,2664|56,1566,2508|55,2666,0|54,2667,529|53,0,2668|53,2668,0|52,2670,2669|51,2671,0|50,2672,525|49,2673,0|48,2674,0|46,2675,0|45,0,2676|44,180,2677|43,2678,0|42,2679,2661|41,0,2680|40,2681,0|39,2682,2665|38,2683,2497|37,2684,2527|36,2685,2527|34,0,2686|46,651,0|45,0,2688|44,685,2689|43,0,2690|43,2690,0|42,2692,2691|41,0,2693|40,0,2694|61,622,0|60,2696,0|61,588,0|60,2698,0|59,2699,2697|58,2699,2700|57,2701,0|56,2702,2568|55,2703,0|54,2704,641|53,0,2705|53,2705,0|52,2707,2706|51,2708,0|50,2709,635|49,2710,0|48,2711,0|57,2699,0|56,2713,2568|55,2714,0|54,2715,603|53,0,2716|53,2716,0|52,2718,2717|51,2719,0|50,2720,599|49,2721,0|48,2722,0|47,2723,2712|46,2724,0|45,0,2725|44,739,2726|43,2727,0|42,2728,2691|41,0,2729|40,2730,0|39,2731,2695|38,2732,2557|37,2733,2587|36,2734,2587|46,612,0|45,0,2736|44,335,2737|43,0,2738|43,2738,0|42,2740,2739|41,0,2741|40,0,2742|46,2723,0|45,0,2744|44,369,2745|43,2746,0|42,2747,2739|41,0,2748|40,2749,0|39,2750,2743|38,2751,2557|37,2752,2587|36,2753,2587|35,2754,2735|34,0,2755|33,2756,2687|32,0,2757|31,0,2758|34,0,2754|33,2760,2687|32,0,2761|31,0,2762|28,2763,2759|27,0,2764|27,0,2763|26,2766,2765|25,2767,2592|25,2766,2592|24,2769,2768|46,830,0|45,0,2771|44,856,2772|43,0,2773|43,2773,0|42,2775,2774|41,0,2776|40,0,2777|61,791,0|60,2779,0|59,2632,2780|58,2632,2781|57,0,2782|56,872,2783|55,2784,0|54,2785,820|53,0,2786|53,2786,0|52,2788,2787|51,2789,0|50,2790,810|49,2791,0|48,2792,0|47,2643,2793|46,2794,0|45,0,2795|44,899,2796|43,2797,0|42,2798,2774|41,0,2799|40,2800,0|39,2801,2778|38,2651,2802|37,2803,2651|36,2804,2651|35,2651,2805|34,0,2806|33,2807,2622|32,0,2808|31,0,2809|28,2655,2810|27,0,2811|26,2656,2812|25,2813,2656|24,2656,2814|23,2815,2770|22,2816,2657|21,2817,2657|20,2818,2657|23,2656,2769|22,2820,2657|21,2821,2657|20,2822,2657|19,2823,2819|54,2481,0|53,2825,0|52,2826,0|51,2827,0|50,2828,0|49,2829,0|48,2830,0|46,2831,0|45,0,2832|44,0,2833|43,2834,0|42,2835,0|41,0,2836|40,2837,0|39,2838,0|54,2510,0|53,2840,0|52,2841,0|51,2842,0|50,2843,0|49,2844,0|48,2845,0|46,2846,0|45,0,2847|44,958,2848|43,2849,0|42,2850,0|41,0,2851|40,2852,0|39,2853,0|38,2854,2839|34,0,2855|54,2541,0|53,2857,0|52,2858,0|51,2859,0|50,2860,0|49,2861,0|48,2862,0|46,2863,0|45,0,2864|44,0,2865|43,2866,0|42,2867,0|41,0,2868|40,2869,0|39,2870,0|54,2570,0|53,2872,0|52,2873,0|51,2874,0|50,2875,0|49,2876,0|48,2877,0|46,2878,0|45,0,2879|44,997,2880|43,2881,0|42,2882,0|41,0,2883|40,2884,0|39,2885,0|38,2886,2871|34,0,2887|33,2888,2856|32,0,2889|31,0,2890|27,0,2891|54,2605,0|53,2893,0|52,2894,0|51,2895,0|50,2896,0|49,2897,0|48,2898,0|46,2899,0|45,0,2900|44,0,2901|43,2902,0|42,2903,0|41,0,2904|40,2905,0|39,2906,0|34,0,2907|54,2635,0|53,2909,0|52,2910,0|51,2911,0|50,2912,0|49,2913,0|48,2914,0|46,2915,0|45,0,2916|44,0,2917|43,2918,0|42,2919,0|41,0,2920|40,2921,0|39,2922,0|34,0,2923|33,2924,2908|32,0,2925|31,0,2926|27,0,2927|23,2928,2892|54,2667,0|53,2930,0|52,2931,0|51,2932,0|50,2933,0|49,2934,0|48,2935,0|46,2936,0|45,0,2937|44,958,2938|43,2939,0|42,2940,0|41,0,2941|40,2942,0|39,2943,0|38,2944,2839|37,2945,2855|36,2946,2855|34,0,2947|54,2715,0|53,2949,0|52,2950,0|51,2951,0|50,2952,0|49,2953,0|48,2954,0|46,2955,0|45,0,2956|44,997,2957|43,2958,0|42,2959,0|41,0,2960|40,2961,0|39,2962,0|38,2963,2871|37,2964,2887|36,2965,2887|34,0,2966|33,2967,2948|32,0,2968|31,0,2969|27,0,2970|25,2971,2892|23,2928,2972|22,2973,2929|21,2974,2929|20,2975,2929|18,2976,2824|17,2976,2977|38,2586,2497|34,0,2979|33,2588,2980|32,0,2981|31,0,2982|46,1134,0|45,0,2984|44,335,2985|43,0,2986|43,2986,0|42,2988,2987|41,0,2989|40,0,2990|61,1110,0|60,2992,0|57,0,2993|56,0,2994|55,2995,0|54,2996,1125|53,0,2997|61,1156,0|60,2999,0|57,0,3000|56,0,3001|55,3002,0|54,3003,1125|53,3004,0|52,3005,2998|51,3006,0|50,3007,1121|49,3008,0|48,3009,0|46,3010,0|45,0,3011|44,369,3012|43,3013,0|42,3014,2987|41,0,3015|40,3016,0|39,3017,2991|38,3018,2557|34,0,3019|33,3020,2980|32,0,3021|31,0,3022|28,3023,2983|27,0,3024|61,0,1156|60,0,3026|59,3027,285|57,0,3028|56,0,3029|55,0,3030|55,3030,0|54,3032,3031|53,0,3033|53,3033,0|52,3035,3034|51,0,3036|60,3026,0|59,3038,295|57,0,3039|56,0,3040|55,0,3041|55,3041,0|54,3043,3042|53,0,3044|53,3044,0|52,3046,3045|51,3047,0|50,3048,3037|49,3049,0|48,3050,0|46,3051,0|45,0,3052|44,335,3053|43,0,3054|43,3054,0|42,3056,3055|41,0,3057|40,0,3058|59,3000,2567|57,0,3060|56,0,3061|55,3062,0|54,3063,3042|53,0,3064|53,3064,0|52,3066,3065|51,3067,0|50,3068,3037|49,3069,0|48,3070,0|46,3071,0|45,0,3072|44,369,3073|43,3074,0|42,3075,3055|41,0,3076|40,3077,0|39,3078,3059|38,3079,2557|34,0,3080|33,3081,2980|32,0,3082|31,0,3083|29,2983,3084|28,3023,3085|27,0,3086|26,3087,3025|38,2651,2621|34,0,3089|33,2652,3090|32,0,3091|31,0,3092|46,1226,0|45,0,3094|44,0,3095|43,0,3096|43,3096,0|42,3098,3097|41,0,3099|40,0,3100|61,1202,0|60,3102,0|57,0,3103|56,0,3104|55,3105,0|54,3106,1217|53,0,3107|53,3107,0|52,3109,3108|51,3110,0|50,3111,1213|49,3112,0|48,3113,0|46,3114,0|45,0,3115|44,0,3116|43,3117,0|42,3118,3097|41,0,3119|40,3120,0|39,3121,3101|38,3122,2651|34,0,3123|33,3124,3090|32,0,3125|31,0,3126|28,3127,3093|27,0,3128|59,1204,438|57,0,3130|56,0,3131|55,0,3132|55,3132,0|54,3134,3133|53,0,3135|53,3135,0|52,3137,3136|51,0,3138|59,1214,448|57,0,3140|56,0,3141|55,0,3142|55,3142,0|54,3144,3143|53,0,3145|53,3145,0|52,3147,3146|51,3148,0|50,3149,3139|49,3150,0|48,3151,0|46,3152,0|45,0,3153|44,0,3154|43,0,3155|43,3155,0|42,3157,3156|41,0,3158|40,0,3159|59,3103,2632|57,0,3161|56,0,3162|55,3163,0|54,3164,3143|53,0,3165|53,3165,0|52,3167,3166|51,3168,0|50,3169,3139|49,3170,0|48,3171,0|46,3172,0|45,0,3173|44,0,3174|43,3175,0|42,3176,3156|41,0,3177|40,3178,0|39,3179,3160|38,3180,2651|34,0,3181|33,3182,3090|32,0,3183|31,0,3184|29,3093,3185|28,3127,3186|27,0,3187|26,3188,3129|23,3189,3088|54,2635,1217|53,3191,0|52,3192,3108|51,3193,0|50,3194,1213|49,3195,0|48,3196,0|46,3197,0|45,0,3198|44,0,3199|43,3200,0|42,3201,3097|41,0,3202|40,3203,0|39,3204,3101|38,3205,2651|34,0,3206|33,3207,3090|32,0,3208|31,0,3209|28,3210,3093|27,0,3211|54,2635,3143|53,3213,0|52,3214,3166|51,3215,0|50,3216,3139|49,3217,0|48,3218,0|46,3219,0|45,0,3220|44,0,3221|43,3222,0|42,3223,3156|41,0,3224|40,3225,0|39,3226,3160|38,3227,2651|34,0,3228|33,3229,3090|32,0,3230|31,0,3231|29,3093,3232|28,3210,3233|27,0,3234|26,3235,3212|23,3236,3088|22,3237,3190|21,3238,3190|54,2570,1125|53,3240,0|52,3241,2998|51,3242,0|50,3243,1121|49,3244,0|48,3245,0|46,3246,0|45,0,3247|44,369,3248|43,3249,0|42,3250,2987|41,0,3251|40,3252,0|39,3253,2991|38,3254,2557|34,0,3255|33,3256,2980|32,0,3257|31,0,3258|28,3259,2983|27,0,3260|54,2570,3042|53,3262,0|52,3263,3065|51,3264,0|50,3265,3037|49,3266,0|48,3267,0|46,3268,0|45,0,3269|44,369,3270|43,3271,0|42,3272,3055|41,0,3273|40,3274,0|39,3275,3059|38,3276,2557|34,0,3277|33,3278,2980|32,0,3279|31,0,3280|29,2983,3281|28,3259,3282|27,0,3283|26,3284,3261|23,3236,3285|38,2751,2497|37,3287,2979|36,3288,2979|34,0,3289|33,2760,3290|32,0,3291|31,0,3292|46,1358,0|45,0,3294|44,335,3295|43,0,3296|43,3296,0|42,3298,3297|41,0,3299|40,0,3300|61,1334,0|60,3302,0|57,3303,0|56,3304,2994|55,3305,0|54,3306,1349|53,0,3307|54,2715,1349|53,3309,0|52,3310,3308|51,3311,0|50,3312,1345|49,3313,0|48,3314,0|56,3304,2568|55,3316,0|54,3317,1349|53,3318,0|52,3319,3308|51,3320,0|50,3321,1345|49,3322,0|48,3323,0|47,3324,3315|46,3325,0|45,0,3326|44,369,3327|43,3328,0|42,3329,3297|41,0,3330|40,3331,0|39,3332,3301|38,3333,2557|37,3334,3255|36,3335,3255|34,0,3336|33,3337,3290|32,0,3338|31,0,3339|28,3340,3293|27,0,3341|59,1336,590|57,3343,0|56,3344,3029|55,0,3345|55,3345,0|54,3347,3346|53,0,3348|53,3348,0|52,3350,3349|51,0,3351|59,1346,600|57,3353,0|56,3354,3040|55,0,3355|55,3355,0|54,3357,3356|53,0,3358|53,3358,0|52,3360,3359|51,3361,0|50,3362,3352|49,3363,0|48,3364,0|46,3365,0|45,0,3366|44,335,3367|43,0,3368|43,3368,0|42,3370,3369|41,0,3371|40,0,3372|59,3303,2699|57,3374,0|56,3375,3061|55,3376,0|54,3377,3356|53,0,3378|54,2715,3356|53,3380,0|52,3381,3379|51,3382,0|50,3383,3352|49,3384,0|48,3385,0|56,3375,2568|55,3387,0|54,3388,3356|53,3389,0|52,3390,3379|51,3391,0|50,3392,3352|49,3393,0|48,3394,0|47,3395,3386|46,3396,0|45,0,3397|44,369,3398|43,3399,0|42,3400,3369|41,0,3401|40,3402,0|39,3403,3373|38,3404,2557|37,3405,3277|36,3406,3277|34,0,3407|33,3408,3290|32,0,3409|31,0,3410|29,3293,3411|28,3340,3412|27,0,3413|26,3414,3342|25,3415,3285|23,3236,3416|22,3417,3286|21,3418,3286|20,3419,3239|38,2886,2839|34,0,3421|33,2888,3422|32,0,3423|31,0,3424|54,3003,0|53,3426,0|52,3427,0|51,3428,0|50,3429,0|49,3430,0|48,3431,0|46,3432,0|45,0,3433|44,997,3434|43,3435,0|42,3436,0|41,0,3437|40,3438,0|39,3439,0|38,3440,2871|34,0,3441|33,3442,3422|32,0,3443|31,0,3444|28,3445,3425|27,0,3446|54,3063,0|53,3448,0|52,3449,0|51,3450,0|50,3451,0|49,3452,0|48,3453,0|46,3454,0|45,0,3455|44,997,3456|43,3457,0|42,3458,0|41,0,3459|40,3460,0|39,3461,0|38,3462,2871|34,0,3463|33,3464,3422|32,0,3465|31,0,3466|29,3425,3467|28,3445,3468|27,0,3469|26,3470,3447|38,2923,2907|34,0,3472|33,2924,3473|32,0,3474|31,0,3475|54,3106,0|53,3477,0|52,3478,0|51,3479,0|50,3480,0|49,3481,0|48,3482,0|46,3483,0|45,0,3484|44,0,3485|43,3486,0|42,3487,0|41,0,3488|40,3489,0|39,3490,0|38,3491,2923|34,0,3492|33,3493,3473|32,0,3494|31,0,3495|28,3496,3476|27,0,3497|54,3164,0|53,3499,0|52,3500,0|51,3501,0|50,3502,0|49,3503,0|48,3504,0|46,3505,0|45,0,3506|44,0,3507|43,3508,0|42,3509,0|41,0,3510|40,3511,0|39,3512,0|38,3513,2923|34,0,3514|33,3515,3473|32,0,3516|31,0,3517|29,3476,3518|28,3496,3519|27,0,3520|26,3521,3498|23,3522,3471|27,0,3476|23,3524,3471|22,3525,3523|21,3526,3523|27,0,3425|23,3524,3528|38,2963,2839|37,3530,3421|36,3531,3421|34,0,3532|33,2967,3533|32,0,3534|31,0,3535|54,3317,0|53,3537,0|52,3538,0|51,3539,0|50,3540,0|49,3541,0|48,3542,0|47,3543,2955|46,3544,0|45,0,3545|44,997,3546|43,3547,0|42,3548,0|41,0,3549|40,3550,0|39,3551,0|38,3552,2871|37,3553,2887|36,3554,2887|34,0,3555|33,3556,3533|32,0,3557|31,0,3558|28,3559,3536|27,0,3560|54,3388,0|53,3562,0|52,3563,0|51,3564,0|50,3565,0|49,3566,0|48,3567,0|47,3568,2955|46,3569,0|45,0,3570|44,997,3571|43,3572,0|42,3573,0|41,0,3574|40,3575,0|39,3576,0|38,3577,2871|37,3578,2887|36,3579,2887|34,0,3580|33,3581,3533|32,0,3582|31,0,3583|29,3536,3584|28,3559,3585|27,0,3586|26,3587,3561|25,3588,3528|23,3524,3589|22,3590,3529|21,3591,3529|20,3592,3527|18,3593,3420|61,1495,0|60,3595,0|57,0,3596|56,0,3597|55,3598,0|54,3599,0|53,3600,0|52,3601,0|51,3602,0|50,3603,0|49,3604,0|48,3605,0|46,3606,0|45,0,3607|44,0,3608|43,3609,0|42,3610,0|41,0,3611|40,3612,0|39,3613,0|38,3614,2923|34,0,3615|33,3616,3473|32,0,3617|31,0,3618|28,3619,3476|27,0,3620|59,3596,2632|57,0,3622|56,0,3623|55,3624,0|54,3625,0|53,3626,0|52,3627,0|51,3628,0|50,3629,0|49,3630,0|48,3631,0|46,3632,0|45,0,3633|44,0,3634|43,3635,0|42,3636,0|41,0,3637|40,3638,0|39,3639,0|38,3640,2923|34,0,3641|33,3642,3473|32,0,3643|31,0,3644|29,3476,3645|28,3619,3646|27,0,3647|26,3648,3621|23,3649,3471|22,3650,3523|21,3651,3523|20,3592,3652|17,3653,3594|16,3654,2978|17,2976,2929|20,3529,3527|46,3543,0|45,0,3658|44,997,3659|43,3660,0|42,3661,0|41,0,3662|40,3663,0|39,3664,0|38,3665,2871|37,3666,2887|36,3667,2887|34,0,3668|33,3669,3533|32,0,3670|31,0,3671|28,3672,3536|27,0,3673|46,3568,0|45,0,3675|44,997,3676|43,3677,0|42,3678,0|41,0,3679|40,3680,0|39,3681,0|38,3682,2871|37,3683,2887|36,3684,2887|34,0,3685|33,3686,3533|32,0,3687|31,0,3688|29,3536,3689|28,3672,3690|27,0,3691|26,3692,3674|25,3693,3528|23,3524,3694|22,3695,3529|21,3696,3529|20,3697,3652|17,3698,3657|16,3699,3656|15,3700,3655|47,2846,2936|46,3702,0|45,0,3703|44,958,3704|43,3705,0|42,3706,0|41,0,3707|40,3708,0|39,3709,0|38,3710,2839|37,3711,2855|36,3712,2855|34,0,3713|33,3556,3714|32,0,3715|31,0,3716|27,0,3717|25,3718,2892|23,2928,3719|22,3720,2929|21,3721,2929|20,3722,2929|17,3653,3593|16,3724,3723|27,0,3536|25,3726,3528|23,3524,3727|22,3728,3529|21,3729,3529|20,3730,3652|17,3731,3657|16,3732,3656|15,3733,3725|14,3734,3701|18,2976,2823|17,2976,3736|16,3654,3737|15,3700,3738|14,3734,3739|13,3740,3735|12,3740,3741|38,2907,2839|34,0,3743|38,2923,2871|34,0,3745|33,3746,3744|32,0,3747|31,0,3748|27,0,3749|23,2928,3750|38,2923,2839|34,0,3752|33,3746,3753|32,0,3754|31,0,3755|34,0,2871|33,3757,3753|32,0,3758|31,0,3759|28,3760,3756|27,0,3761|59,2538,2632|57,0,3763|56,0,3764|55,3765,0|54,3766,0|53,3767,0|52,3768,0|51,3769,0|50,3770,0|49,3771,0|48,3772,0|46,3773,0|45,0,3774|44,0,3775|43,3776,0|42,3777,0|41,0,3778|40,3779,0|39,3780,0|38,3781,2871|34,0,3782|33,3783,3753|32,0,3784|31,0,3785|29,3756,3786|28,3760,3787|27,0,3788|26,3789,3762|23,3522,3790|23,3524,3790|22,3792,3791|21,3793,3791|27,0,3756|23,3524,3795|20,3796,3794|16,3797,3751|11,3798,3742|10,0,3799|46,1679,0|45,0,3801|44,0,3802|43,0,3803|43,3803,0|42,3805,3804|41,3806,0|40,0,3807|54,0,33|53,0,3809|53,3809,0|52,3811,3810|51,3812,0|50,3813,29|53,0,2825|52,2826,3815|51,3816,0|50,3817,0|49,3818,0|48,3819,3814|46,3820,0|45,0,3821|44,0,3822|43,3823,0|42,3824,3804|41,3825,0|40,3826,0|39,3827,3808|46,1699,0|45,0,3829|44,1703,3830|43,0,3831|43,3831,0|42,3833,3832|41,3834,0|40,0,3835|54,0,109|53,0,3837|53,3837,0|52,3839,3838|51,3840,0|50,3841,105|53,0,2840|52,2841,3843|51,3844,0|50,3845,0|49,3846,0|48,3847,3842|46,3848,0|45,0,3849|44,1729,3850|43,3851,0|42,3852,3832|41,3853,0|40,3854,0|39,3855,3836|38,3856,3828|41,2836,0|40,3858,0|39,3859,0|41,2851,0|40,3861,0|39,3862,0|38,3863,3860|34,3864,3857|46,1753,0|45,0,3866|44,0,3867|43,0,3868|43,3868,0|42,3870,3869|41,3871,0|40,0,3872|54,0,222|53,0,3874|53,3874,0|52,3876,3875|51,3877,0|50,3878,218|53,0,2857|52,2858,3880|51,3881,0|50,3882,0|49,3883,0|48,3884,3879|46,3885,0|45,0,3886|44,0,3887|43,3888,0|42,3889,3869|41,3890,0|40,3891,0|39,3892,3873|46,1773,0|45,0,3894|44,1777,3895|43,0,3896|43,3896,0|42,3898,3897|41,3899,0|40,0,3900|54,0,298|53,0,3902|53,3902,0|52,3904,3903|51,3905,0|50,3906,294|53,0,2872|52,2873,3908|51,3909,0|50,3910,0|49,3911,0|48,3912,3907|46,3913,0|45,0,3914|44,1803,3915|43,3916,0|42,3917,3897|41,3918,0|40,3919,0|39,3920,3901|38,3921,3893|41,2868,0|40,3923,0|39,3924,0|41,2883,0|40,3926,0|39,3927,0|38,3928,3925|34,3929,3922|33,3930,3865|32,0,3931|31,0,3932|27,0,3933|46,1831,0|45,0,3935|44,0,3936|43,0,3937|43,3937,0|42,3939,3938|41,3940,0|40,0,3941|54,0,398|53,0,3943|53,3943,0|52,3945,3944|51,3946,0|50,3947,394|53,0,2893|52,2894,3949|51,3950,0|50,3951,0|49,3952,0|48,3953,3948|46,3954,0|45,0,3955|44,0,3956|43,3957,0|42,3958,3938|41,3959,0|40,3960,0|39,3961,3942|41,2904,0|40,3963,0|39,3964,0|34,3965,3962|46,1859,0|45,0,3967|44,0,3968|43,0,3969|43,3969,0|42,3971,3970|41,3972,0|40,0,3973|54,0,451|53,0,3975|53,3975,0|52,3977,3976|51,3978,0|50,3979,447|53,0,2909|52,2910,3981|51,3982,0|50,3983,0|49,3984,0|48,3985,3980|46,3986,0|45,0,3987|44,0,3988|43,3989,0|42,3990,3970|41,3991,0|40,3992,0|39,3993,3974|41,2920,0|40,3995,0|39,3996,0|34,3997,3994|33,3998,3966|32,0,3999|31,0,4000|27,0,4001|23,4002,3934|46,1892,0|45,0,4004|44,1703,4005|43,0,4006|43,4006,0|42,4008,4007|41,4009,0|40,0,4010|54,0,529|53,0,4012|53,4012,0|52,4014,4013|51,4015,0|50,4016,525|53,0,2930|52,2931,4018|51,4019,0|50,4020,0|49,4021,0|48,4022,4017|46,4023,0|45,0,4024|44,1729,4025|43,4026,0|42,4027,4007|41,4028,0|40,4029,0|39,4030,4011|38,4031,3828|37,4032,3857|36,4033,3857|41,2941,0|40,4035,0|39,4036,0|38,4037,3860|37,4038,3864|36,4039,3864|34,4040,4034|46,1929,0|45,0,4042|44,1936,4043|43,0,4044|43,4044,0|42,4046,4045|41,4047,0|40,0,4048|54,0,641|53,0,4050|53,4050,0|52,4052,4051|51,4053,0|50,4054,635|54,0,603|53,0,4056|53,4056,0|52,4058,4057|51,4059,0|50,4060,599|49,4061,4055|54,2704,0|53,0,4063|53,4063,0|52,4065,4064|51,4066,0|50,4067,0|49,4068,0|48,4069,4062|53,0,2949|52,2950,4071|51,4072,0|50,4073,0|49,4074,0|48,4075,4061|47,4076,4070|46,4077,0|45,0,4078|44,1983,4079|43,4080,0|42,4081,4045|41,4082,0|40,4083,0|39,4084,4049|38,4085,3893|37,4086,3922|36,4087,3922|46,1926,0|45,0,4089|44,1777,4090|43,0,4091|43,4091,0|42,4093,4092|41,4094,0|40,0,4095|46,4076,0|45,0,4097|44,1803,4098|43,4099,0|42,4100,4092|41,4101,0|40,4102,0|39,4103,4096|38,4104,3893|37,4105,3922|36,4106,3922|35,4107,4088|41,2960,0|40,4109,0|39,4110,0|38,4111,3925|37,4112,3929|36,4113,3929|34,4114,4108|33,4115,4041|32,0,4116|31,0,4117|34,4114,4107|33,4119,4041|32,0,4120|31,0,4121|28,4122,4118|27,0,4123|27,0,4122|26,4125,4124|25,4126,3934|25,4125,3934|24,4128,4127|46,2038,0|45,0,4130|44,2045,4131|43,0,4132|43,4132,0|42,4134,4133|41,4135,0|40,0,4136|54,0,820|53,0,4138|53,4138,0|52,4140,4139|51,4141,0|50,4142,810|49,3980,4143|54,2785,0|53,0,4145|53,4145,0|52,4147,4146|51,4148,0|50,4149,0|49,4150,0|48,4151,4144|47,3986,4152|46,4153,0|45,0,4154|44,2087,4155|43,4156,0|42,4157,4133|41,4158,0|40,4159,0|39,4160,4137|38,3994,4161|37,4162,3994|36,4163,3994|35,3994,4164|34,3997,4165|33,4166,3966|32,0,4167|31,0,4168|28,4001,4169|27,0,4170|26,4002,4171|25,4172,4002|24,4002,4173|23,4174,4129|22,4175,4003|21,4176,4003|20,4177,4003|23,4002,4128|22,4179,4003|21,4180,4003|20,4181,4003|19,4182,4178|33,3929,3864|32,0,4184|31,0,4185|27,0,4186|33,3997,3965|32,0,4188|31,0,4189|27,0,4190|23,4191,4187|33,4114,4040|32,0,4193|31,0,4194|27,0,4195|25,4196,4187|23,4191,4197|22,4198,4192|21,4199,4192|20,4200,4192|18,4201,4183|17,4201,4202|38,3921,3828|38,3928,3860|34,4205,4204|33,3930,4206|32,0,4207|31,0,4208|46,2142,0|45,0,4210|44,1777,4211|43,0,4212|43,4212,0|42,4214,4213|41,4215,0|40,0,4216|54,0,1125|53,0,4218|53,4218,0|52,4220,4219|51,4221,0|50,4222,1121|54,2996,0|53,0,4224|52,3427,4225|51,4226,0|50,4227,0|49,4228,0|48,4229,4223|46,4230,0|45,0,4231|44,1803,4232|43,4233,0|42,4234,4213|41,4235,0|40,4236,0|39,4237,4217|38,4238,3893|41,3437,0|40,4240,0|39,4241,0|38,4242,3925|34,4243,4239|33,4244,4206|32,0,4245|31,0,4246|28,4247,4209|27,0,4248|48,0,3049|46,4250,0|45,0,4251|44,1777,4252|43,0,4253|43,4253,0|42,4255,4254|41,4256,0|40,0,4257|54,0,3042|53,0,4259|53,4259,0|52,4261,4260|51,4262,0|50,4263,3037|53,0,3448|52,3449,4265|51,4266,0|50,4267,0|49,4268,0|48,4269,4264|46,4270,0|45,0,4271|44,1803,4272|43,4273,0|42,4274,4254|41,4275,0|40,4276,0|39,4277,4258|38,4278,3893|41,3459,0|40,4280,0|39,4281,0|38,4282,3925|34,4283,4279|33,4284,4206|32,0,4285|31,0,4286|29,4209,4287|28,4247,4288|27,0,4289|26,4290,4249|38,3994,3962|38,3997,3965|34,4293,4292|33,3998,4294|32,0,4295|31,0,4296|46,2184,0|45,0,4298|44,0,4299|43,0,4300|43,4300,0|42,4302,4301|41,4303,0|40,0,4304|54,0,1217|53,0,4306|53,4306,0|52,4308,4307|51,4309,0|50,4310,1213|53,0,3477|52,3478,4312|51,4313,0|50,4314,0|49,4315,0|48,4316,4311|46,4317,0|45,0,4318|44,0,4319|43,4320,0|42,4321,4301|41,4322,0|40,4323,0|39,4324,4305|38,4325,3994|41,3488,0|40,4327,0|39,4328,0|38,4329,3997|34,4330,4326|33,4331,4294|32,0,4332|31,0,4333|28,4334,4297|27,0,4335|48,0,3150|46,4337,0|45,0,4338|44,0,4339|43,0,4340|43,4340,0|42,4342,4341|41,4343,0|40,0,4344|54,0,3143|53,0,4346|53,4346,0|52,4348,4347|51,4349,0|50,4350,3139|53,0,3499|52,3500,4352|51,4353,0|50,4354,0|49,4355,0|48,4356,4351|46,4357,0|45,0,4358|44,0,4359|43,4360,0|42,4361,4341|41,4362,0|40,4363,0|39,4364,4345|38,4365,3994|41,3510,0|40,4367,0|39,4368,0|38,4369,3997|34,4370,4366|33,4371,4294|32,0,4372|31,0,4373|29,4297,4374|28,4334,4375|27,0,4376|26,4377,4336|23,4378,4291|52,2910,4312|51,4380,0|50,4381,0|49,4382,0|48,4383,4311|46,4384,0|45,0,4385|44,0,4386|43,4387,0|42,4388,4301|41,4389,0|40,4390,0|39,4391,4305|38,4392,3994|34,3997,4393|33,4394,4294|32,0,4395|31,0,4396|28,4397,4297|27,0,4398|52,2910,4352|51,4400,0|50,4401,0|49,4402,0|48,4403,4351|46,4404,0|45,0,4405|44,0,4406|43,4407,0|42,4408,4341|41,4409,0|40,4410,0|39,4411,4345|38,4412,3994|34,3997,4413|33,4414,4294|32,0,4415|31,0,4416|29,4297,4417|28,4397,4418|27,0,4419|26,4420,4399|23,4421,4291|22,4422,4379|21,4423,4379|52,2873,4225|51,4425,0|50,4426,0|49,4427,0|48,4428,4223|46,4429,0|45,0,4430|44,1803,4431|43,4432,0|42,4433,4213|41,4434,0|40,4435,0|39,4436,4217|38,4437,3893|34,3929,4438|33,4439,4206|32,0,4440|31,0,4441|28,4442,4209|27,0,4443|52,2873,4265|51,4445,0|50,4446,0|49,4447,0|48,4448,4264|46,4449,0|45,0,4450|44,1803,4451|43,4452,0|42,4453,4254|41,4454,0|40,4455,0|39,4456,4258|38,4457,3893|34,3929,4458|33,4459,4206|32,0,4460|31,0,4461|29,4209,4462|28,4442,4463|27,0,4464|26,4465,4444|23,4421,4466|38,4104,3828|37,4468,4204|36,4469,4204|38,4111,3860|37,4471,4205|36,4472,4205|34,4473,4470|33,4119,4474|32,0,4475|31,0,4476|46,2270,0|45,0,4478|44,1777,4479|43,0,4480|43,4480,0|42,4482,4481|41,4483,0|40,0,4484|54,0,1349|53,0,4486|53,4486,0|52,4488,4487|51,4489,0|50,4490,1345|54,3306,0|53,0,4492|52,2950,4493|51,4494,0|50,4495,0|49,4496,0|48,4497,4491|52,3538,4493|51,4499,0|50,4500,0|49,4501,0|48,4502,4491|47,4503,4498|46,4504,0|45,0,4505|44,1803,4506|43,4507,0|42,4508,4481|41,4509,0|40,4510,0|39,4511,4485|38,4512,3893|37,4513,4438|36,4514,4438|41,3549,0|40,4516,0|39,4517,0|38,4518,3925|37,4519,3929|36,4520,3929|34,4521,4515|33,4522,4474|32,0,4523|31,0,4524|28,4525,4477|27,0,4526|48,0,3363|46,4528,0|45,0,4529|44,1777,4530|43,0,4531|43,4531,0|42,4533,4532|41,4534,0|40,0,4535|54,0,3356|53,0,4537|53,4537,0|52,4539,4538|51,4540,0|50,4541,3352|54,3377,0|53,0,4543|52,2950,4544|51,4545,0|50,4546,0|49,4547,0|48,4548,4542|52,3563,4544|51,4550,0|50,4551,0|49,4552,0|48,4553,4542|47,4554,4549|46,4555,0|45,0,4556|44,1803,4557|43,4558,0|42,4559,4532|41,4560,0|40,4561,0|39,4562,4536|38,4563,3893|37,4564,4458|36,4565,4458|41,3574,0|40,4567,0|39,4568,0|38,4569,3925|37,4570,3929|36,4571,3929|34,4572,4566|33,4573,4474|32,0,4574|31,0,4575|29,4477,4576|28,4525,4577|27,0,4578|26,4579,4527|25,4580,4466|23,4421,4581|22,4582,4467|21,4583,4467|20,4584,4424|33,3929,4205|32,0,4586|31,0,4587|33,4243,4205|32,0,4589|31,0,4590|28,4591,4588|27,0,4592|33,4283,4205|32,0,4594|31,0,4595|29,4588,4596|28,4591,4597|27,0,4598|26,4599,4593|33,3997,4293|32,0,4601|31,0,4602|33,4330,4293|32,0,4604|31,0,4605|28,4606,4603|27,0,4607|33,4370,4293|32,0,4609|31,0,4610|29,4603,4611|28,4606,4612|27,0,4613|26,4614,4608|23,4615,4600|27,0,4603|23,4617,4600|22,4618,4616|21,4619,4616|27,0,4588|23,4617,4621|33,4114,4473|32,0,4623|31,0,4624|33,4521,4473|32,0,4626|31,0,4627|28,4628,4625|27,0,4629|33,4572,4473|32,0,4631|31,0,4632|29,4625,4633|28,4628,4634|27,0,4635|26,4636,4630|25,4637,4621|23,4617,4638|22,4639,4622|21,4640,4622|20,4641,4620|18,4642,4585|41,3611,0|40,4644,0|39,4645,0|38,4646,3997|33,4647,4293|32,0,4648|31,0,4649|28,4650,4603|27,0,4651|41,3637,0|40,4653,0|39,4654,0|38,4655,3997|33,4656,4293|32,0,4657|31,0,4658|29,4603,4659|28,4650,4660|27,0,4661|26,4662,4652|23,4663,4600|22,4664,4616|21,4665,4616|20,4641,4666|17,4667,4643|16,4668,4203|17,4201,4192|20,4622,4620|41,3662,0|40,4672,0|39,4673,0|38,4674,3925|37,4675,3929|36,4676,3929|33,4677,4473|32,0,4678|31,0,4679|28,4680,4625|27,0,4681|41,3679,0|40,4683,0|39,4684,0|38,4685,3925|37,4686,3929|36,4687,3929|33,4688,4473|32,0,4689|31,0,4690|29,4625,4691|28,4680,4692|27,0,4693|26,4694,4682|25,4695,4621|23,4617,4696|22,4697,4622|21,4698,4622|20,4699,4666|17,4700,4671|16,4701,4670|15,4702,4669|41,3707,0|40,4704,0|39,4705,0|38,4706,3860|37,4707,3864|36,4708,3864|33,4521,4709|32,0,4710|31,0,4711|27,0,4712|25,4713,4187|23,4191,4714|22,4715,4192|21,4716,4192|20,4717,4192|17,4667,4642|16,4719,4718|27,0,4625|25,4721,4621|23,4617,4722|22,4723,4622|21,4724,4622|20,4725,4666|17,4726,4671|16,4727,4670|15,4728,4720|14,4729,4703|18,4201,4182|17,4201,4731|16,4668,4732|15,4702,4733|14,4729,4734|13,4735,4730|12,4735,4736|38,3965,3860|38,3997,3925|33,4739,4738|32,0,4740|31,0,4741|27,0,4742|23,4191,4743|38,3997,3860|33,4739,4745|32,0,4746|31,0,4747|33,3925,4745|32,0,4749|31,0,4750|28,4751,4748|27,0,4752|41,3778,0|40,4754,0|39,4755,0|38,4756,3925|33,4757,4745|32,0,4758|31,0,4759|29,4748,4760|28,4751,4761|27,0,4762|26,4763,4753|23,4615,4764|23,4617,4764|22,4766,4765|21,4767,4765|27,0,4748|23,4617,4769|20,4770,4768|16,4771,4744|11,4772,4737|10,4773,0|9,4774,3800|8,4775,0|7,4776,2468|6,0,4777|6,4777,0|5,4779,4778|4,0,4780|3,0,4781|32,2443,1827|31,2443,4783|27,2443,4784|32,2120,1887|31,2120,4786|27,2120,4787|23,4788,4785|32,2443,2022|31,2443,4790|32,2443,2026|31,2443,4792|28,4793,4791|27,2443,4794|27,2443,4793|26,4796,4795|25,4797,4785|25,4796,4785|24,4799,4798|32,2120,2099|31,2120,4801|28,4787,4802|27,2120,4803|26,4788,4804|25,4805,4788|24,4788,4806|23,4807,4800|22,4808,4789|21,4809,4789|20,4810,4789|23,4788,4799|22,4812,4789|21,4813,4789|20,4814,4789|19,4815,4811|32,2443,2116|31,2443,4817|27,2443,4818|23,2120,4819|32,2443,2125|31,2443,4821|27,2443,4822|25,4823,4819|23,2120,4824|22,4825,4820|21,4826,4820|20,4827,4820|18,4828,4816|17,4828,4829|32,2449,2139|31,2449,4831|32,2452,2173|31,2452,4833|28,4834,4832|28,2452,2449|27,4836,4835|32,2313,2181|31,2313,4838|32,2316,2214|31,2316,4840|28,4841,4839|28,2316,2313|27,4843,4842|23,4844,4837|32,2313,2233|31,2313,4846|28,4847,4839|27,2313,4848|23,4849,4837|22,4850,4845|21,4851,4845|32,2449,2254|31,2449,4853|28,4854,4832|27,2449,4855|23,4849,4856|32,2449,2267|31,2449,4858|32,2449,2295|31,2449,4860|28,4861,4859|27,2449,4862|25,4863,4856|23,4849,4864|22,4865,4857|21,4866,4857|20,4867,4852|32,2449,2305|31,2449,4869|32,2452,2308|31,2452,4871|28,4872,4870|27,4836,4873|23,4843,4874|23,2313,4874|22,4876,4875|21,4877,4875|27,2449,4870|23,2313,4879|32,2449,2328|31,2449,4881|27,2449,4882|25,4883,4879|23,2313,4884|22,4885,4880|21,4886,4880|20,4887,4878|18,4888,4868|28,2346,2313|23,4890,4874|22,4891,4875|21,4892,4875|20,4887,4893|17,4894,4889|16,4895,4830|32,2449,2368|31,2449,4897|28,4898,4882|27,2449,4899|25,4900,4879|23,2313,4901|22,4902,4880|21,4903,4880|20,4904,4878|17,4894,4905|16,4906,4828|15,4907,4896|32,2443,2393|31,2443,4909|27,2443,4910|25,4911,4819|23,2120,4912|22,4913,4820|21,4914,4820|20,4915,4820|32,2443,2414|31,2443,4917|27,2443,4918|25,4919,4819|23,2120,4920|22,4921,4820|21,4922,4820|20,4923,4820|19,4924,4916|17,4925,4828|17,4894,4888|16,4927,4926|16,4927,4828|15,4929,4928|14,4930,4908|18,4828,4815|17,4828,4932|16,4895,4933|15,4907,4934|14,4930,4935|13,4936,4931|17,4916,4828|16,4927,4938|15,4929,4939|14,4940,4935|12,4941,4937|23,2120,2443|23,4843,4836|23,2313,4836|22,4945,4944|21,4946,4944|23,2313,2449|20,4948,4947|16,4949,4943|11,4950,4942|10,4951,0|9,4952,1678|8,0,4953|32,4740,3931|31,4740,4955|27,4740,4956|32,4188,3999|31,4188,4958|27,4188,4959|23,4960,4957|32,4740,4116|31,4740,4962|32,4740,4120|31,4740,4964|28,4965,4963|27,4740,4966|27,4740,4965|26,4968,4967|25,4969,4957|25,4968,4957|24,4971,4970|32,4188,4167|31,4188,4973|28,4959,4974|27,4188,4975|26,4960,4976|25,4977,4960|24,4960,4978|23,4979,4972|22,4980,4961|21,4981,4961|20,4982,4961|23,4960,4971|22,4984,4961|21,4985,4961|20,4986,4961|19,4987,4983|32,4740,4184|31,4740,4989|27,4740,4990|23,4188,4991|32,4740,4193|31,4740,4993|27,4740,4994|25,4995,4991|23,4188,4996|22,4997,4992|21,4998,4992|20,4999,4992|18,5000,4988|17,5000,5001|32,4746,4207|31,4746,5003|32,4749,4245|31,4749,5005|28,5006,5004|28,4749,4746|27,5008,5007|32,4758,4285|31,4758,5010|29,5004,5011|28,5006,5012|29,4746,4758|28,4749,5014|27,5015,5013|26,5016,5009|32,4601,4295|31,4601,5018|32,4604,4332|31,4604,5020|28,5021,5019|28,4604,4601|27,5023,5022|32,4609,4372|31,4609,5025|29,5019,5026|28,5021,5027|29,4601,4609|28,4604,5029|27,5030,5028|26,5031,5024|23,5032,5017|32,4601,4395|31,4601,5034|28,5035,5019|27,4601,5036|32,4601,4415|31,4601,5038|29,5019,5039|28,5035,5040|27,4601,5041|26,5042,5037|23,5043,5017|22,5044,5033|21,5045,5033|32,4746,4440|31,4746,5047|28,5048,5004|27,4746,5049|32,4746,4460|31,4746,5051|29,5004,5052|28,5048,5053|27,4746,5054|26,5055,5050|23,5043,5056|32,4746,4475|31,4746,5058|32,4746,4523|31,4746,5060|28,5061,5059|27,4746,5062|32,4746,4574|31,4746,5064|29,5059,5065|28,5061,5066|27,4746,5067|26,5068,5063|25,5069,5056|23,5043,5070|22,5071,5057|21,5072,5057|20,5073,5046|32,4746,4586|31,4746,5075|32,4749,4589|31,4749,5077|28,5078,5076|27,5008,5079|32,4758,4594|31,4758,5081|29,5076,5082|28,5078,5083|27,5015,5084|26,5085,5080|26,5030,5023|23,5087,5086|23,4601,5086|22,5089,5088|21,5090,5088|27,4746,5076|23,4601,5092|32,4746,4623|31,4746,5094|32,4746,4626|31,4746,5096|28,5097,5095|27,4746,5098|32,4746,4631|31,4746,5100|29,5095,5101|28,5097,5102|27,4746,5103|26,5104,5099|25,5105,5092|23,4601,5106|22,5107,5093|21,5108,5093|20,5109,5091|18,5110,5074|28,4648,4601|29,4601,4657|28,4648,5113|26,5114,5112|23,5115,5086|22,5116,5088|21,5117,5088|20,5109,5118|17,5119,5111|16,5120,5002|17,5000,4992|20,5093,5091|32,4746,4678|31,4746,5124|28,5125,5095|27,4746,5126|32,4746,4689|31,4746,5128|29,5095,5129|28,5125,5130|27,4746,5131|26,5132,5127|25,5133,5092|23,4601,5134|22,5135,5093|21,5136,5093|20,5137,5118|17,5138,5123|16,5139,5122|15,5140,5121|32,4740,4710|31,4740,5142|27,4740,5143|25,5144,4991|23,4188,5145|22,5146,4992|21,5147,4992|20,5148,4992|17,5119,5110|16,5150,5149|27,4746,5095|25,5152,5092|23,4601,5153|22,5154,5093|21,5155,5093|20,5156,5118|17,5157,5123|16,5158,5122|15,5159,5151|14,5160,5141|18,5000,4987|17,5000,5162|16,5120,5163|15,5140,5164|14,5160,5165|13,5166,5161|12,5166,5167|23,4188,4740|26,5015,5008|23,5087,5170|23,4601,5170|22,5172,5171|21,5173,5171|23,4601,4746|20,5175,5174|16,5176,5169|11,5177,5168|10,5178,0|9,5179,3800|8,5180,0|7,5181,4954|6,0,5182|64,193,1153|63,0,5184|62,282,5185|60,5186,0|57,0,5187|56,0,5188|55,5189,0|54,5190,1125|53,5191,0|52,5192,1147|51,5193,0|50,5194,1121|54,5190,0|53,5196,0|52,5197,2151|51,5198,0|50,5199,0|48,5200,5195|45,0,5201|44,1803,5202|43,5203,0|42,5204,2145|41,5205,0|40,5206,0|39,5207,2149|38,5208,1772|52,5197,0|51,5210,0|50,5211,0|45,0,5212|44,997,5213|43,5214,0|42,5215,0|41,5216,0|40,5217,0|39,5218,0|38,5219,1817|34,5220,5209|33,5221,2138|32,2449,5222|31,2449,5223|28,5224,4832|27,2449,5225|25,5226,4837|23,4849,5227|22,5228,4845|21,5229,4845|20,4867,5230|33,5220,2137|32,2449,5232|31,2449,5233|28,5234,4870|27,2449,5235|25,5236,4874|23,2313,5237|22,5238,4875|21,5239,4875|20,4887,5240|18,5241,5231|25,2313,4890|23,5243,5237|22,5244,4875|21,5245,4875|20,4887,5246|17,5247,5242|16,5248,4830|20,4904,5240|17,5247,5250|16,5251,4828|15,5252,5249|17,5247,5241|16,5254,4926|16,5254,4828|15,5256,5255|14,5257,5253|16,5248,4933|15,5252,5259|14,5257,5260|13,5261,5258|16,5254,4938|15,5256,5263|14,5264,5260|12,5265,5262|25,2449,4836|23,2313,5267|22,5268,4944|21,5269,4944|20,4948,5270|16,5271,4943|11,5272,5266|10,5273,0|9,5274,1678|8,0,5275|61,5186,0|60,5277,0|57,0,5278|56,0,5279|55,5280,0|54,5281,0|53,5282,0|52,5283,4225|51,5284,0|50,5285,0|49,5286,0|48,5287,4223|46,5288,0|45,0,5289|44,1803,5290|43,5291,0|42,5292,4213|41,5293,0|40,5294,0|39,5295,4217|38,5296,3893|52,5283,0|51,5298,0|50,5299,0|49,5300,0|48,5301,0|46,5302,0|45,0,5303|44,997,5304|43,5305,0|42,5306,0|41,5307,0|40,5308,0|39,5309,0|38,5310,3925|34,5311,5297|33,5312,4206|32,4746,5313|31,4746,5314|28,5315,5004|27,4746,5316|59,3000,5278|57,0,5318|56,0,5319|55,5320,0|54,5321,0|53,5322,0|52,5323,4225|51,5324,0|50,5325,0|49,5326,0|48,5327,4223|46,5328,0|45,0,5329|44,1803,5330|43,5331,0|42,5332,4213|41,5333,0|40,5334,0|39,5335,4217|38,5336,3893|52,5323,0|51,5338,0|50,5339,0|49,5340,0|48,5341,0|46,5342,0|45,0,5343|44,997,5344|43,5345,0|42,5346,0|41,5347,0|40,5348,0|39,5349,0|38,5350,3925|34,5351,5337|33,5352,4206|32,4758,5353|31,4758,5354|29,5315,5355|28,5356,5012|27,5014,5357|26,5358,5317|25,5359,5017|23,5043,5360|22,5361,5033|21,5362,5033|20,5073,5363|33,5311,4205|32,4746,5365|31,4746,5366|28,5367,5076|27,4746,5368|33,5351,4205|32,4758,5370|31,4758,5371|29,5367,5372|28,5373,5083|27,5014,5374|26,5375,5369|25,5376,5086|23,4601,5377|22,5378,5088|21,5379,5088|20,5109,5380|18,5381,5364|26,5113,4601|25,5383,5115|23,5384,5377|22,5385,5088|21,5386,5088|20,5109,5387|17,5388,5382|16,5389,5002|20,5093,5380|20,5137,5387|17,5392,5391|16,5393,5122|15,5394,5390|17,5388,5381|16,5396,5149|20,5156,5387|17,5398,5391|16,5399,5122|15,5400,5397|14,5401,5395|16,5389,5163|15,5394,5403|14,5401,5404|13,5405,5402|12,5405,5406|26,5014,4746|25,5408,5170|23,4601,5409|22,5410,5171|21,5411,5171|20,5175,5412|16,5413,5169|11,5414,5407|10,5415,0|9,5416,3800|8,5417,0|7,5418,5276|6,5419,0|5,5420,5183|4,5421,0|3,5422,0|2,5423,4782|18,1044,492|17,1044,5425|20,1306,1284|20,1458,1456|18,5428,5427|20,1458,1523|17,5430,5429|16,5431,5426|17,5430,5428|16,5433,1044|15,5434,5432|14,5434,5435|11,1676,5436|10,0,5437|18,2124,1891|17,2124,5439|20,2259,2240|20,2327,2325|18,5442,5441|20,2327,2353|17,5444,5443|16,5445,5440|17,5444,5442|16,5447,2124|15,5448,5446|14,5448,5449|11,2464,5450|10,5451,0|9,5452,5438|8,0,5453|18,2929,2657|17,2929,5455|20,3286,3239|18,3657,5457|20,3529,3652|17,5459,5458|16,5460,5456|17,5459,3657|16,5462,2929|15,5463,5461|14,5463,5464|11,3798,5465|10,0,5466|18,4192,4003|17,4192,5468|20,4467,4424|18,4671,5470|20,4622,4666|17,5472,5471|16,5473,5469|17,5472,4671|16,5475,4192|15,5476,5474|14,5476,5477|11,4772,5478|10,5479,0|9,5480,5467|8,5481,0|7,5482,5454|6,0,5483|6,5483,0|5,5485,5484|4,0,5486|3,0,5487|18,4820,4789|17,4820,5489|20,4857,4852|20,4880,4878|18,5492,5491|20,4880,4893|17,5494,5493|16,5495,5490|17,5494,5492|16,5497,4820|15,5498,5496|14,5498,5499|11,4950,5500|10,5501,0|9,5502,5438|8,0,5503|18,4992,4961|17,4992,5505|20,5057,5046|18,5123,5507|20,5093,5118|17,5509,5508|16,5510,5506|17,5509,5123|16,5512,4992|15,5513,5511|14,5513,5514|11,5177,5515|10,5516,0|9,5517,5467|8,5518,0|7,5519,5504|6,0,5520|20,4857,5230|20,4880,5240|18,5523,5522|20,4880,5246|17,5525,5524|16,5526,5490|17,5525,5523|16,5528,4820|15,5529,5527|14,5529,5530|11,5272,5531|10,5532,0|9,5533,5438|8,0,5534|20,5057,5363|18,5391,5536|20,5093,5387|17,5538,5537|16,5539,5506|17,5538,5391|16,5541,4992|15,5542,5540|14,5542,5543|11,5414,5544|10,5545,0|9,5546,5467|8,5547,0|7,5548,5535|6,5549,0|5,5550,5521|4,5551,0|3,5552,0|2,5553,5488|1,5554,5424|15,1562,1635|14,1636,5556|14,1646,5556|12,5558,5557|11,1676,5559|10,0,5560|15,2379,2427|14,2428,5562|14,2438,5562|12,5564,5563|11,2464,5565|10,5566,0|9,5567,5561|8,0,5568|16,3724,2976|15,3700,5570|14,3734,5571|11,3798,5572|10,0,5573|16,4719,4201|15,4702,5575|14,4729,5576|11,4772,5577|10,5578,0|9,5579,5574|8,5580,0|7,5581,5569|6,0,5582|6,5582,0|5,5584,5583|4,0,5585|3,0,5586|15,4907,4929|14,4930,5588|14,4940,5588|12,5590,5589|11,4950,5591|10,5592,0|9,5593,5561|8,0,5594|16,5150,5000|15,5140,5596|14,5160,5597|11,5177,5598|10,5599,0|9,5600,5574|8,5601,0|7,5602,5595|6,0,5603|15,5252,5256|14,5257,5605|14,5264,5605|12,5607,5606|11,5272,5608|10,5609,0|9,5610,5561|8,0,5611|16,5396,5000|15,5394,5613|14,5401,5614|11,5414,5615|10,5616,0|9,5617,5574|8,5618,0|7,5619,5612|6,5620,0|5,5621,5604|4,5622,0|3,5623,0|2,5624,5587|11,1676,5434|10,0,5626|11,2464,5448|10,5628,0|9,5629,5627|8,0,5630|11,3798,5463|10,0,5632|11,4772,5476|10,5634,0|9,5635,5633|8,5636,0|7,5637,5631|6,0,5638|6,5638,0|5,5640,5639|4,0,5641|3,0,5642|11,4950,5498|10,5644,0|9,5645,5627|8,0,5646|11,5177,5513|10,5648,0|9,5649,5633|8,5650,0|7,5651,5647|6,0,5652|11,5272,5529|10,5654,0|9,5655,5627|8,0,5656|11,5414,5542|10,5658,0|9,5659,5633|8,5660,0|7,5661,5657|6,5662,0|5,5663,5653|4,5664,0|3,5665,0|2,5666,5643|1,5667,5625|0,5668,5555| \ No newline at end of file diff --git a/tutorials/aeon/stable_attractor.bdd b/tutorials/aeon/stable_attractor.bdd deleted file mode 100644 index 5014e75c..00000000 --- a/tutorials/aeon/stable_attractor.bdd +++ /dev/null @@ -1 +0,0 @@ -|79,0,0|79,1,1|78,1,0|77,0,2|76,0,3|75,0,4|74,5,0|73,6,0|72,7,0|76,3,0|75,9,0|74,10,0|73,11,0|72,12,0|71,13,8|70,14,0|69,0,15|68,0,16|67,0,17|66,0,18|65,0,19|64,0,20|63,0,21|62,0,22|61,0,23|60,0,24|59,25,0|58,26,0|57,0,27|57,27,0|56,29,28|55,0,30|55,30,0|54,32,31|53,0,33|53,33,0|52,35,34|51,0,36|60,24,0|59,38,0|58,39,0|57,0,40|57,40,0|56,42,41|55,0,43|55,43,0|54,45,44|53,0,46|53,46,0|52,48,47|51,49,0|50,50,37|49,51,0|48,52,0|47,53,0|46,54,0|45,55,0|44,56,0|43,0,57|43,57,0|42,59,58|41,0,60|40,0,61|61,23,0|60,63,0|59,64,0|58,65,0|57,0,66|57,66,0|56,68,67|55,69,0|54,70,44|53,0,71|54,0,44|53,73,0|52,74,72|51,75,0|50,76,37|49,77,0|48,78,0|47,79,0|46,80,0|45,81,0|44,82,0|43,83,0|42,84,58|41,0,85|40,86,0|39,87,62|38,88,0|37,89,0|36,90,0|35,91,0|34,0,92|33,93,0|32,0,94|31,0,95|30,96,0|29,97,0|28,98,0|27,0,99|26,100,0|25,101,0|24,102,0|23,0,103|22,104,0|21,105,0|20,106,0|19,107,0|18,0,108|17,0,109|16,110,0|15,0,111|14,0,112|13,113,0|12,114,0|11,0,115|10,0,116|48,0,52|47,118,0|46,119,0|45,120,0|44,121,0|43,0,122|43,122,0|42,124,123|41,125,0|40,0,126|53,0,73|52,74,128|51,129,0|50,130,37|49,131,0|54,70,0|53,0,133|52,0,134|51,135,0|50,136,0|49,137,0|48,138,132|47,139,0|46,140,0|45,141,0|44,142,0|43,143,0|42,144,123|41,145,0|40,146,0|39,147,127|38,148,0|37,149,0|36,150,0|35,151,0|34,0,152|33,153,0|32,0,154|31,0,155|30,156,0|29,157,0|28,158,0|27,0,159|26,160,0|25,161,0|24,162,0|23,0,163|22,164,0|21,165,0|20,166,0|19,167,0|18,0,168|17,0,169|16,170,0|15,0,171|14,0,172|13,173,0|12,174,0|11,0,175|10,176,0|9,177,117|8,0,178|8,178,0|7,180,179|6,0,181|6,181,0|5,183,182|4,0,184|3,0,185|4,184,0|3,187,0|2,188,186|1,0,189|53,133,0|52,191,0|51,192,0|50,193,0|49,194,0|48,195,0|47,196,0|46,197,0|45,198,0|44,199,0|43,200,0|42,201,0|41,0,202|40,203,0|39,204,0|38,205,0|37,206,0|36,207,0|35,208,0|34,0,209|33,210,0|32,0,211|31,0,212|30,213,0|29,214,0|28,215,0|27,0,216|26,217,0|25,218,0|24,219,0|23,0,220|22,221,0|21,222,0|20,223,0|19,224,0|18,225,0|17,226,0|16,227,0|15,228,0|14,229,0|13,230,0|12,231,0|11,0,232|10,0,233|41,202,0|40,235,0|39,236,0|38,237,0|37,238,0|36,239,0|35,240,0|34,241,0|33,242,0|32,0,243|31,0,244|30,245,0|29,246,0|28,247,0|27,0,248|26,249,0|25,250,0|24,251,0|23,0,252|22,253,0|21,254,0|20,255,0|19,256,0|18,257,0|17,258,0|16,259,0|15,260,0|14,261,0|13,262,0|12,263,0|11,0,264|10,265,0|9,266,234|8,0,267|8,267,0|7,269,268|6,0,270|6,270,0|5,272,271|4,0,273|3,0,274|4,273,0|3,276,0|2,277,275|1,0,278|0,279,190| \ No newline at end of file