Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Minimal repro triggering the issue in ccfraft.tla AdvanceCommitIndex #5798

Conversation

achamayou
Copy link
Member

@achamayou achamayou commented Oct 30, 2023

AdvanceCommitIndex always picks the smallest possible index to move commit to, which breaks on traces as soon as there is more than one signature pending.

See trace produced under https://dev.azure.com/MSRC-CCF/CCF/_build/results?buildId=78092&view=logs&j=0c81e209-1101-513f-1f15-37e9c3575eb2&t=a05664f3-ab91-5eb2-6acd-14e2179ad708

@ghost
Copy link

ghost commented Oct 30, 2023

repro_scenario_for_advance_commit_index_bug@79900 aka 20240105.5 vs main ewma over 20 builds from 79642 to 79901

Click to see table

main

build_id build_number Commit latency factor pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem tpcc_sgx_cft^ tpcc_sgx_cft_mem ls_sgx_cft^ ls_sgx_cft_mem pi_ls_sgx_cft^ pi_ls_sgx_cft_mem tpcc_virtual_cft^ pi_basic_sgx_cft^ pi_basic_sgx_cft_mem ls_virtual_cft^ pi_ls_virtual_cft^ pi_basic_virtual_cft^ pi_basic_js_virtual_cft^ pi_basic_mt_virtual_cft^ pi_basic_js_sgx_cft^ pi_basic_js_sgx_cft_mem ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ ls_jwt_sgx_cft^ ls_jwt_sgx_cft_mem ls_js_virtual_cft^ pi_ls_jwt_sgx_cft^ pi_ls_jwt_sgx_cft_mem ls_full_js_virtual_cft^ ls_js_jwt_virtual_cft^ ls_js_sgx_cft^ ls_js_sgx_cft_mem ls_full_js_sgx_cft^ ls_full_js_sgx_cft_mem ls_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem tlc_3node_fixed_duration_s tlc_3node_fixed_states tlc_atomic_reconfig_duration_s tlc_atomic_reconfig_states tlc_reconfig_duration_s tlc_reconfig_states hist_sgx_cft^ RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^ tlc_sim_traces tlc_sim_levelmean
79642 20231220.4 0.797657 28505.5 2.30851e+07 5574.1 8.59996e+07 14035.2 1.88908e+07 14152.9 1.05021e+07 17262.1 15669.3 1.25993e+07 52978.3 56536.1 62672 4577 83188.6 1429.7 1.25993e+07 20696.7 22254.4 7246.97 1.67936e+07 17598.7 6980.1 6.30784e+06 17574.9 11711.9 5800.86 1.67936e+07 5459.1 1.67936e+07 3976.44 1.67936e+07 7 86496 433 1.2541e+07 237 6.31473e+06 45331.4 831359 1.18546e+06 8.17402e+06 3.07023e+07 2205 403
79649 20231220.6 0.790672 27856.5 2.30851e+07 5633.93 8.59996e+07 14086.3 1.67936e+07 14136.7 1.05021e+07 17057.1 15662.2 1.25993e+07 52924.1 55935 60678.1 4551.7 98341.7 1425.4 1.25993e+07 21063.8 21328.3 7271.74 1.67936e+07 17352 7090.8 6.30784e+06 17391.2 11532 5802.52 1.67936e+07 5719.34 1.67936e+07 3999.03 1.67936e+07 7 86496 431 1.2541e+07 241 6.31473e+06 43239.8 831415 1.17087e+06 8.14998e+06 3.04395e+07 2422 403
79678 20231220.18 0.791999 28217.3 2.51822e+07 5558.58 8.59996e+07 14061.7 1.88908e+07 14133.4 1.05021e+07 17425.3 15598 1.25993e+07 52743.3 56074.6 61667.5 4603.9 70893.4 1437.1 1.25993e+07 21027.1 22116.6 6906.58 1.88908e+07 17741.1 6985.7 6.30784e+06 17275.2 11597.5 5794.4 1.67936e+07 5731.37 1.67936e+07 3993.12 1.67936e+07 6 86496 431 1.2541e+07 236 6.31473e+06 47191.7 837557 1.18345e+06 8.11176e+06 3.06298e+07 2274 403
79693 20231221.3 0.825277 27963.8 2.51822e+07 5633.86 8.59996e+07 14089 1.88908e+07 14143.4 1.05021e+07 17281.9 15608.7 1.46964e+07 53233.4 57492.4 62214.5 4570.5 73753.8 1418.7 1.25993e+07 20675.4 21741.5 7243.3 1.67936e+07 17380 6931.6 6.30784e+06 17681.7 11860.3 5760.75 1.67936e+07 5475.1 1.67936e+07 3977.28 1.67936e+07 6 86496 443 1.2541e+07 240 6.31473e+06 43951.7 810554 1.17945e+06 8.1552e+06 3.0712e+07 2247 403
79707 20231222.3 0.812946 28028.2 2.30851e+07 5620.72 8.59996e+07 14007.1 1.67936e+07 14111.8 1.05021e+07 17192.9 15564.3 1.46964e+07 52990.6 58113.2 62042.6 4644.1 86154.2 1429.5 1.25993e+07 20983.2 22005.6 6869.23 1.88908e+07 20798.9 7085 6.30784e+06 17660.2 11716.6 5786 1.67936e+07 5731.94 1.67936e+07 3996.47 1.67936e+07 7 86496 433 1.2541e+07 243 6.31473e+06 44675.9 840758 1.17882e+06 8.1646e+06 3.06982e+07 2385 403
79724 20231225.2 0.835919 28166.4 2.30851e+07 5619.85 8.59996e+07 14035.1 1.67936e+07 14190.5 1.05021e+07 17292.1 15651.5 1.25993e+07 52861.9 56705.4 61889.5 4601.8 74118.7 1440.9 1.25993e+07 20650.7 21723.1 7241.84 1.67936e+07 17483.2 6978.6 6.30784e+06 17588.3 11783.8 5808 1.67936e+07 5474.82 1.88908e+07 3994.32 1.67936e+07 7 86496 436 1.2541e+07 237 6.31473e+06 46135.5 834644 1.1791e+06 8.14888e+06 3.27303e+07 2316 403
79739 20231226.3 0.830636 28205.8 2.51822e+07 5613.09 8.59996e+07 14076 1.88908e+07 14178.4 1.05021e+07 17368.3 15658.8 1.25993e+07 52752.6 56752.4 62271.2 4587.3 70865.4 1443.1 1.25993e+07 21018.1 22055.1 7268.57 1.67936e+07 17838.1 6983.8 6.30784e+06 17531.8 11814.9 5759.16 1.67936e+07 5489.93 1.88908e+07 3983.36 1.67936e+07 6 86496 428 1.2541e+07 244 6.31473e+06 47038.4 824513 1.17359e+06 8.14881e+06 3.08443e+07 2478 403
79750 20231227.1 0.818602 27885.2 2.51822e+07 5599.89 8.59996e+07 14026.9 1.67936e+07 14100 1.05021e+07 17400.9 15563.2 1.25993e+07 53080.8 56737.9 61924.4 4624.8 87959.6 1425.9 1.25993e+07 20931.4 18203 6848.41 1.67936e+07 20610 6932.3 6.30784e+06 17300.9 11921.8 5796.65 1.67936e+07 5448.92 1.67936e+07 3976.43 1.67936e+07 6 86496 430 1.2541e+07 242 6.31473e+06 45579.1 838072 1.18283e+06 8.15446e+06 3.07475e+07 2258 403
79764 20231228.1 0.785802 28069.2 2.30851e+07 5579.3 8.59996e+07 14013.7 1.88908e+07 14133.7 1.05021e+07 17482.4 15558.2 1.25993e+07 52691.7 56538.7 62169.5 4606.1 100210 1426 1.25993e+07 21182.6 22162.1 6801.15 1.67936e+07 17804.6 7035 6.30784e+06 17513 11666.7 5760.56 1.67936e+07 5478.71 1.67936e+07 3992.59 1.67936e+07 6 86496 434 1.2541e+07 235 6.31473e+06 47564.7 832827 1.17369e+06 8.16737e+06 3.1373e+07 2144 403
79781 20231229.2 0.801636 27896.7 2.51822e+07 5589.66 8.59996e+07 14027.6 1.88908e+07 14166.7 1.05021e+07 17379.6 15567.2 1.46964e+07 53058 56634.4 62290.7 4544.7 70323.6 1425.2 1.25993e+07 21324.7 22159.2 6793.52 1.67936e+07 17388.8 7078.9 6.30784e+06 17492.5 11838.8 5797.56 1.67936e+07 5483.48 1.67936e+07 3993.74 1.67936e+07 6 86496 436 1.2541e+07 240 6.31473e+06 40847.4 834593 1.18035e+06 8.15979e+06 3.07217e+07 2181 403
79795 20240101.3 0.78501 28203.3 2.51822e+07 5573.08 8.59996e+07 14058.6 1.88908e+07 14075.3 1.05021e+07 17464.7 15400.4 1.25993e+07 53125.1 57116.7 61313 4568.7 88523 1433.5 1.25993e+07 20746.1 22281.6 6907.22 1.88908e+07 17744.9 6981.9 6.30784e+06 17841.4 11654.5 5797.99 1.67936e+07 5721.54 1.67936e+07 3992.77 1.67936e+07 7 86496 437 1.2541e+07 244 6.31473e+06 45491.3 828138 1.18098e+06 8.16847e+06 3.08021e+07 2254 403
79809 20240102.3 0.818907 27998 2.51822e+07 5582.58 8.59996e+07 14069 1.88908e+07 14207.7 1.05021e+07 17426.2 15632.9 1.46964e+07 52688.3 56487.3 62076.8 4588.5 89517.2 1438 1.25993e+07 20938.1 21383.1 7254.86 1.67936e+07 17806.2 6979.5 6.30784e+06 17373.5 11613.7 5809.21 1.67936e+07 5725.47 1.88908e+07 4000.63 1.67936e+07 6 86496 427 1.2541e+07 241 6.31473e+06 39813.8 838128 1.18558e+06 8.15241e+06 3.07577e+07 2304 403
79821 20240102.7 0.812237 28223.4 2.30851e+07 5591.2 8.59996e+07 14003.1 1.88908e+07 14188.3 1.05021e+07 17312.2 15498.1 1.46964e+07 53352.6 57235.7 62129.2 4590.4 100850 1429.2 1.25993e+07 21078.7 22285.6 7246.07 1.67936e+07 20842.2 6934.2 6.30784e+06 17429 11612.2 5809.09 1.67936e+07 5478.56 1.67936e+07 4007.06 1.67936e+07 7 86496 446 1.2541e+07 237 6.31473e+06 40366 832255 1.17903e+06 8.15355e+06 3.03592e+07 2331 403
79832 20240102.10 0.780568 27705.2 2.51822e+07 5592.62 8.59996e+07 14075.6 1.88908e+07 14247 1.05021e+07 17247.1 15580.2 1.46964e+07 52935.7 56910 62683.8 4647.1 90345.4 1429.8 1.25993e+07 20739.3 20193.9 6842.56 1.67936e+07 20729.9 7079.5 6.30784e+06 17575.8 11690.8 5781.21 1.67936e+07 5767.74 1.67936e+07 3982.1 1.67936e+07 6 86496 424 1.2541e+07 245 6.31473e+06 42743.5 823735 1.18304e+06 8.15511e+06 3.0778e+07 2301 403
79836 20240103.1 0.8277 28173 2.51822e+07 5617.23 8.59996e+07 14088.9 1.88908e+07 14246.2 1.05021e+07 17163.7 15684.4 1.46964e+07 52985.4 57238.7 62511.8 4622.6 68113.2 1430.6 1.25993e+07 20776.5 21693.9 7262.76 1.67936e+07 20385 6980.2 6.30784e+06 17974.8 11889.2 5814.99 1.67936e+07 5465.89 1.88908e+07 3973.9 1.67936e+07 6 86496 417 1.2541e+07 238 6.31473e+06 43365.4 827987 1.18005e+06 8.16857e+06 3.13533e+07 2109 403
79850 20240104.1 0.774183 28107.5 2.51822e+07 5647.78 8.59996e+07 14069.1 1.88908e+07 14203.3 1.05021e+07 17222.5 15616.9 1.25993e+07 53076.9 56886.7 62583 4618.3 88847.3 1430.7 1.25993e+07 20820.4 21956.8 7263.29 1.67936e+07 17246.1 7142 6.30784e+06 17545.1 11727 5808.21 1.67936e+07 5739.03 1.88908e+07 4019.28 1.67936e+07 6 86496 447 1.2541e+07 239 6.31473e+06 45361.8 833007 1.17531e+06 8.1401e+06 3.07056e+07 2277 403
79858 20240104.5 0.762951 28151.4 2.30851e+07 5612.73 8.59996e+07 14105.1 1.88908e+07 14237.6 1.05021e+07 17237.2 15657.2 1.46964e+07 53156.1 56700.3 62251.6 4624.7 72092.6 1437 1.05021e+07 20802.9 22305.5 7259.07 1.88908e+07 17912 6983.6 6.30784e+06 17600.9 12005.6 5791.47 1.67936e+07 5734.66 1.67936e+07 4001.19 1.67936e+07 6 86496 420 1.2541e+07 238 6.31473e+06 46312.7 832473 1.18246e+06 8.14589e+06 3.0464e+07 2357 403
79876 20240104.10 0.770841 27983.2 2.51822e+07 5617.52 8.59996e+07 14034.5 1.67936e+07 14165.8 1.05021e+07 17196.9 15592.9 1.25993e+07 53164.5 56410.8 62397 4645.9 82253.2 1427.3 1.25993e+07 20949.8 22178.9 7241.98 1.67936e+07 17324.7 6915.4 6.30784e+06 17551.5 11659.7 5771.22 1.67936e+07 5737.28 1.67936e+07 3985.63 1.67936e+07 6 86496 429 1.2541e+07 234 6.31473e+06 40222.9 829045 1.18083e+06 8.15014e+06 3.10298e+07 2315 403
79893 20240105.3 0.770387 28242.6 2.30851e+07 5619.63 8.59996e+07 14091.5 1.88908e+07 14247.6 1.05021e+07 17195.7 15674.3 1.25993e+07 53109.3 56423.9 61913.6 4637.7 79459.2 1436.8 1.25993e+07 21053.6 21897.2 7241.21 1.67936e+07 17479.2 7028.1 6.30784e+06 17489.6 11786.3 5776.46 1.67936e+07 5739.53 1.67936e+07 4001.54 1.67936e+07 6 86496 438 1.2541e+07 234 6.31473e+06 41192.1 834184 1.18333e+06 8.13454e+06 3.07928e+07 2312 403
79901 20240105.6 0.804442 28134.7 2.51822e+07 5625.32 8.59996e+07 14099 1.88908e+07 14266.8 1.05021e+07 17253.5 15657.8 1.46964e+07 52754.9 54886.9 61431.1 4615.1 96416.1 1428.6 1.25993e+07 20971.5 21889.5 6896.08 1.67936e+07 17410.2 7033.2 6.30784e+06 17219.9 11532.7 5807.41 1.67936e+07 5744.67 1.88908e+07 4003.65 1.67936e+07 6 86496 445 1.2541e+07 240 6.31473e+06 42166 837682 1.17356e+06 8.14881e+06 3.18111e+07 2258 403

repro_scenario_for_advance_commit_index_bug

build_id build_number pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem pi_basic_mt_virtual_cft^ Commit latency factor tpcc_virtual_cft^ ls_virtual_cft^ pi_ls_virtual_cft^ pi_basic_virtual_cft^ tpcc_sgx_cft^ tpcc_sgx_cft_mem pi_basic_js_virtual_cft^ ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ ls_js_virtual_cft^ ls_sgx_cft^ ls_sgx_cft_mem ls_full_js_virtual_cft^ pi_ls_sgx_cft^ pi_ls_sgx_cft_mem ls_js_jwt_virtual_cft^ pi_basic_sgx_cft^ pi_basic_sgx_cft_mem pi_basic_js_sgx_cft^ pi_basic_js_sgx_cft_mem hist_sgx_cft^ ls_jwt_sgx_cft^ ls_jwt_sgx_cft_mem pi_ls_jwt_sgx_cft^ pi_ls_jwt_sgx_cft_mem ls_js_sgx_cft^ ls_js_sgx_cft_mem ls_full_js_sgx_cft^ ls_full_js_sgx_cft_mem ls_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^ tlc_3node_fixed_duration_s tlc_3node_fixed_states tlc_atomic_reconfig_duration_s tlc_atomic_reconfig_states tlc_reconfig_duration_s tlc_reconfig_states tlc_sim_traces tlc_sim_levelmean
78092 20231030.15 28029.7 2.30851e+07 84250.1 0.803602 17100.4 43775.7 47331.7 54334.7 5621.69 8.59996e+07 4401.5 17112.2 19622.1 17162.9 14075.3 1.88908e+07 14865.1 14211 1.05021e+07 9806.38 15591.3 1.46964e+07 1431.4 1.25993e+07 38969.8 6834.41 1.67936e+07 6971 6.30784e+06 5809.83 1.67936e+07 5743.51 1.67936e+07 3998.75 1.67936e+07 831081 1.18175e+06 8.14434e+06 3.14603e+07 nan nan nan nan nan nan nan nan
78214 20231101.9 28012.4 2.72794e+07 73853.3 0.783592 17243 43731.9 46998.9 55018.3 5559.38 8.59996e+07 4411.2 17344.6 18926.5 17541.3 13989.2 1.88908e+07 14923.1 14064.2 1.05021e+07 9760.69 15519.1 1.25993e+07 1416.2 1.25993e+07 45976 6853.36 1.88908e+07 7026.3 6.30784e+06 5773.61 1.67936e+07 5488.97 1.88908e+07 3984.66 1.67936e+07 832588 1.17855e+06 8.14379e+06 3.00174e+07 nan nan nan nan nan nan nan nan
78237 20231101.16 27821.1 2.51822e+07 74311.7 0.804315 17454.3 43865.8 46159.7 54710.4 5552.96 8.59996e+07 4386.2 16994.6 19351.7 17541 13963.8 1.67936e+07 14900.3 14066.9 1.05021e+07 10275.8 15530.5 1.25993e+07 1421.3 1.25993e+07 43531.5 6857.54 1.88908e+07 6887.6 6.30784e+06 5788.03 1.67936e+07 5477.46 1.67936e+07 3988.25 1.67936e+07 838588 1.18113e+06 8.15313e+06 3.06881e+07 nan nan nan nan nan nan nan nan
79674 20231220.16 27660.9 2.30851e+07 88259.7 0.81324 17302.6 52833.3 56977.1 62719 5664.93 8.59996e+07 4614.6 20972.1 21671.3 20588.8 14098.8 1.88908e+07 17579.7 14157.2 1.05021e+07 11688.7 15620.1 1.46964e+07 1441.6 1.25993e+07 45736.7 7250.65 1.67936e+07 6985.9 6.30784e+06 5803.6 1.67936e+07 5487.89 1.67936e+07 3997.67 1.67936e+07 833076 1.17249e+06 8.14823e+06 3.13274e+07 6 86496 435 1.2541e+07 239 6.31473e+06 2353 403
79900 20240105.5 28150.1 2.30851e+07 78383.3 0.787697 17221.8 53155.1 55438.8 62205.8 5650.92 8.59996e+07 4576.8 20768 21875.6 17367.8 14110 1.88908e+07 17444.5 14177.5 1.05021e+07 11726.7 15650.9 1.46964e+07 1436.4 1.25993e+07 47934.3 7272.27 1.67936e+07 6963.6 6.30784e+06 5764.91 1.67936e+07 5497.44 1.67936e+07 4006.83 1.67936e+07 819657 1.17979e+06 8.14356e+06 3.1398e+07 6 86496 421 1.2541e+07 236 6.31473e+06 2312 403

images

@achamayou achamayou added bug tla TLA+ specifications labels Nov 1, 2023
@achamayou achamayou mentioned this pull request Nov 9, 2023
5 tasks
@lemmy
Copy link
Contributor

lemmy commented Dec 20, 2023

Build is green because *_deprecated scenarios do not run.

lemmy added a commit that referenced this pull request Dec 20, 2023
…reas raft.h advances to the largest possible one.

Originally found in #5798.
lemmy added a commit that referenced this pull request Jan 2, 2024
…reas raft.h advances to the largest possible one.

Originally found in #5798.
@heidihoward
Copy link
Member

The link to the trace is no longer working. Would it be possible to increase the retention time for ADO build logs?

@lemmy
Copy link
Contributor

lemmy commented Jan 4, 2024

The link to the trace is no longer working. Would it be possible to increase the retention time for ADO build logs?

If you need to recreate the trace/log, checking out the commit on a Codespace is relatively straight forward.

lemmy added a commit that referenced this pull request Jan 4, 2024
…reas raft.h advances to the largest possible one.

Originally found in #5798.
@heidihoward
Copy link
Member

I had a go at reproducing this against the latest version but it wasn't successful, I assume that is due to the changes in the trace validation since.

Output
JSON=../build/replicate_deprecated.ndjson ./tlc.sh consensus/Traceccfraft.tla 
TLC2 Version 2.18 of Day Month 20?? (rev: 79c86b5)
Running breadth-first search Model-Checking with fp 94 and seed 4637506532843996040 with 1 worker on 32 cores with 27305MB heap and 64MB offheap memory [pid: 2998] (Linux 6.2.0-1018-azure amd64, Ubuntu 11.0.21 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspaces/CCF/tla/consensus/Traceccfraft.tla
Parsing file /workspaces/CCF/tla/consensus/ccfraft.tla
Parsing file /tmp/tlc-3039395389646040712/Json.tla (jar:file:/workspaces/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/Json.tla)
Parsing file /tmp/tlc-3039395389646040712/IOUtils.tla (jar:file:/workspaces/CCF/tla/CommunityModules-deps.jar!/IOUtils.tla)
Parsing file /tmp/tlc-3039395389646040712/Sequences.tla (jar:file:/workspaces/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-3039395389646040712/_TLCTrace.tla (jar:file:/workspaces/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/_TLCTrace.tla)
Parsing file /tmp/tlc-3039395389646040712/Naturals.tla (jar:file:/workspaces/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-3039395389646040712/FiniteSets.tla (jar:file:/workspaces/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-3039395389646040712/TLC.tla (jar:file:/workspaces/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-3039395389646040712/FiniteSetsExt.tla (jar:file:/workspaces/CCF/tla/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Parsing file /tmp/tlc-3039395389646040712/SequencesExt.tla (jar:file:/workspaces/CCF/tla/CommunityModules-deps.jar!/SequencesExt.tla)
Parsing file /tmp/tlc-3039395389646040712/Functions.tla (jar:file:/workspaces/CCF/tla/CommunityModules-deps.jar!/Functions.tla)
Parsing file /workspaces/CCF/tla/consensus/Network.tla
Parsing file /tmp/tlc-3039395389646040712/Bags.tla (jar:file:/workspaces/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/Bags.tla)
Parsing file /tmp/tlc-3039395389646040712/Folds.tla (jar:file:/workspaces/CCF/tla/CommunityModules-deps.jar!/Folds.tla)
Parsing file /tmp/tlc-3039395389646040712/Integers.tla (jar:file:/workspaces/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-3039395389646040712/TLCExt.tla (jar:file:/workspaces/CCF/tla/tla2tools.jar!/tla2sany/StandardModules/TLCExt.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module SequencesExt
Semantic processing of module Bags
Semantic processing of module Network
Semantic processing of module ccfraft
Semantic processing of module Json
Semantic processing of module Integers
Semantic processing of module IOUtils
Semantic processing of module TLCExt
Semantic processing of module _TLCTrace
Semantic processing of module Traceccfraft
Starting... (2024-01-05 10:27:03)
<<"Trace:", "../build/replicate_deprecated.ndjson", "Length:", 65>>  3
<<"Trace:", "../build/replicate_deprecated.ndjson", "Length:", 65>>  3
Implied-temporal checking--satisfiability problem has 1 branches.
Computing initial states...
Finished computing initial states: 0 distinct states generated at 2024-01-05 10:27:04.
Progress(1) at 2024-01-05 10:27:04: 0 states generated, 0 distinct states found, 0 states left on queue.
Checking temporal properties for the complete state space with 0 total distinct states at (2024-01-05 10:27:04)
Finished checking temporal properties in 00s at 2024-01-05 10:27:04
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 0.0
0 states generated, 0 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 0.
Finished in 00s at (2024-01-05 10:27:04)

@achamayou
Copy link
Member Author

@heidihoward it looks like that did not check anything:

0 states generated, 0 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 0.

I believe this is fixed by #5879, we can hopefully make progress on the realistic scenarios again with that out of the way.

@achamayou achamayou closed this Jan 5, 2024
lemmy added a commit that referenced this pull request Jan 5, 2024
…reas raft.h advances to the largest possible one.

Originally found in #5798.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug tla TLA+ specifications
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants