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.

Sign up for GitHub

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

Jump to bottom

Align the _logline in a TLA+ counterexample with its corresponding entry in the JSON log, from which the TLA+ state has been constructed. #5812

Merged
merged 1 commit into from
Nov 3, 2023
Merged

Align the _logline in a TLA+ counterexample with its corresponding entry in the JSON log, from which the TLA+ state has been constructed. #5812

merged 1 commit into from
Nov 3, 2023

Conversation

lemmy
Copy link
Contributor

@lemmy lemmy commented Nov 3, 2023

There's an issue in VScode's "TLA+ model checking" view. Expanding the _logline record fails when the current step is "add_configuration", as VScode struggles with "new_configurations: ...".

@lemmy
Align the _logline in a TLA+ counterexample with its corresponding en…
0e9217e 
…try in the JSON log, from which the TLA+ state has been constructed.

There's an issue in VScode's "TLA+ model checking" view. Expanding the _logline record fails when the current step is "add_configuration", as VScode struggles with "new_configurations: ...".
@lemmy lemmy added the tla TLA+ specifications label Nov 3, 2023
@lemmy lemmy added this to the TLA+ Trace Validation milestone Nov 3, 2023
@lemmy lemmy requested a review from a team November 3, 2023 01:47
@lemmy lemmy enabled auto-merge (rebase) November 3, 2023 01:48
@ghost
Copy link

ghost commented Nov 3, 2023

mku-TraceAlias@78354 aka 20231103.1 vs main ewma over 20 builds from 77994 to 78319

Click to see table

main

build_id build_number pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem Commit latency factor tpcc_sgx_cft^ tpcc_sgx_cft_mem ls_sgx_cft^ ls_sgx_cft_mem pi_ls_sgx_cft^ pi_ls_sgx_cft_mem pi_basic_sgx_cft^ pi_basic_sgx_cft_mem pi_basic_js_sgx_cft^ pi_basic_js_sgx_cft_mem pi_basic_mt_virtual_cft^ tpcc_virtual_cft^ ls_jwt_sgx_cft^ ls_jwt_sgx_cft_mem pi_ls_jwt_sgx_cft^ pi_ls_jwt_sgx_cft_mem ls_virtual_cft^ pi_ls_virtual_cft^ ls_js_sgx_cft^ ls_js_sgx_cft_mem pi_basic_virtual_cft^ ls_full_js_sgx_cft^ ls_full_js_sgx_cft_mem pi_basic_js_virtual_cft^ ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ ls_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem ls_js_virtual_cft^ ls_full_js_virtual_cft^ ls_js_jwt_virtual_cft^ hist_sgx_cft^ RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^
77994 20231026.29 27941.4 2.51822e+07 0.80113 5582.56 8.59996e+07 14017.2 1.88908e+07 14167 1.05021e+07 15610.3 1.25993e+07 1446 1.25993e+07 82095.1 17290 6841.03 1.88908e+07 6962.5 6.30784e+06 43873.2 47649.7 5764.66 1.67936e+07 54065 5729.26 1.67936e+07 4441.8 17136.7 19419.7 4003.36 1.67936e+07 17733.8 16838 9840.75 44959.6 840437 1.18274e+06 8.15494e+06 3.07517e+07
78007 20231026.34 27449.9 2.51822e+07 0.765143 5628.96 8.59996e+07 14025.1 1.88908e+07 14089.7 1.05021e+07 15601.5 1.46964e+07 1432.4 1.25993e+07 81427 17307 6850.52 1.88908e+07 7096.8 6.30784e+06 45407.5 47735 5773.88 1.67936e+07 54044.5 5486.07 1.67936e+07 4441.4 17288.5 18904.7 3985.52 1.67936e+07 17015.3 16872.1 9816.73 43179.9 826445 1.17834e+06 8.14738e+06 3.19605e+07
78033 20231027.4 28127.4 2.51822e+07 0.798824 5577.93 8.59996e+07 13972.7 1.88908e+07 14096.8 1.05021e+07 15447.2 1.25993e+07 1432.2 1.25993e+07 65638.2 17273 7250.65 1.67936e+07 6938.4 6.30784e+06 45862.4 48024.5 5786.4 1.67936e+07 53817.4 5743.72 1.67936e+07 4439.6 17160.1 19602.8 4002.74 1.67936e+07 17044.2 16883.5 9854.32 42046.2 829984 1.18448e+06 8.13813e+06 3.06775e+07
78035 20231027.5 27938.3 2.51822e+07 0.785967 5573.65 8.59996e+07 14007.5 1.88908e+07 14114.5 1.05021e+07 15503.3 1.46964e+07 1434.7 1.25993e+07 83501.4 17213.8 6832.63 1.67936e+07 6983.9 6.30784e+06 45970.2 48037.9 5786.59 1.67936e+07 54501.8 5775.4 1.67936e+07 4447.9 17062.2 19333.8 3982.36 1.67936e+07 16911.6 17015.7 9990.67 47144 831267 1.18066e+06 8.09742e+06 3.06715e+07
78049 20231027.10 28049.5 2.51822e+07 0.781085 5504.64 8.59996e+07 14023.9 1.88908e+07 14102.3 1.05021e+07 15421.6 1.46964e+07 1424.4 1.25993e+07 85552.5 17300.2 6846.42 1.67936e+07 6826.6 6.30784e+06 43575 46933.4 5791.73 1.67936e+07 55026 5707.49 1.67936e+07 4431 17056.6 19111.7 3980.86 1.67936e+07 17359 14869.3 9805.16 41017.4 840517 1.18098e+06 8.16672e+06 3.06803e+07
78065 20231030.3 27850.6 2.30851e+07 0.803529 5645.18 8.59996e+07 14038.5 1.88908e+07 14125 1.05021e+07 15560.2 1.46964e+07 1434 1.25993e+07 80986.2 17287.6 7241.2 1.67936e+07 7023.9 6.30784e+06 43811.1 46782.1 5804.59 1.67936e+07 54407.3 5779.74 1.67936e+07 4392.3 17198.2 19724.6 3998.35 1.67936e+07 17634.6 14791.7 10345.8 38753.2 831589 1.1757e+06 8.07743e+06 3.07175e+07
78110 20231031.2 28002.1 2.30851e+07 0.801968 5577.82 8.59996e+07 14078.8 1.88908e+07 14211.9 1.05021e+07 15500.2 1.46964e+07 1434.1 1.25993e+07 90290.4 17706.2 7246.56 1.67936e+07 7122.3 6.30784e+06 43757.1 47025.6 5824.15 1.67936e+07 54021.7 5724.41 1.67936e+07 4412.2 17043.4 19501.2 3999.43 1.67936e+07 17190 14923.3 10161.5 44321.1 833541 1.17964e+06 8.15397e+06 3.09702e+07
78115 20231031.5 28096.6 2.51822e+07 0.788781 5597.14 8.59996e+07 14046.4 1.88908e+07 14149.3 1.05021e+07 15573.1 1.46964e+07 1438.8 1.25993e+07 90398.6 17153.5 6857.73 1.67936e+07 6984.1 6.30784e+06 45717.6 47743.9 5786.81 1.67936e+07 55284.5 5770.07 1.67936e+07 4374.5 17204.3 19257.8 3994.27 1.67936e+07 17318.7 14893.2 9790.65 44365.6 818357 1.17717e+06 8.15176e+06 3.07813e+07
78128 20231031.10 27738.1 2.51822e+07 0.75716 5630.66 8.59996e+07 14058.5 1.88908e+07 14160.9 1.05021e+07 15631.8 1.46964e+07 1441.7 1.25993e+07 71982.3 17076.3 7284.99 1.67936e+07 7044.7 6.30784e+06 43862 47267.7 5805.39 1.67936e+07 55100.9 5776.39 1.67936e+07 4371.6 17200.1 19235.2 3998.07 1.67936e+07 17122 14762.1 10396.2 42934.8 837504 1.18196e+06 8.15251e+06 3.15981e+07
78146 20231031.17 27901 2.51822e+07 0.780638 5598.38 8.59996e+07 14060.8 1.88908e+07 14179 1.05021e+07 15535.7 1.46964e+07 1433.1 1.25993e+07 76464.7 17229.5 6790.28 1.67936e+07 6889.6 6.30784e+06 43813 47595.9 5772.45 1.67936e+07 55096.1 5488.66 1.67936e+07 4355.7 17361 19744.5 3966.05 1.67936e+07 17356.3 14955.7 9799.34 43021.9 820080 1.18077e+06 8.15047e+06 3.07762e+07
78161 20231031.23 28091.4 2.51822e+07 0.782488 5605.13 8.59996e+07 14058.7 1.88908e+07 14092.9 1.05021e+07 15472.1 1.46964e+07 1434.3 1.25993e+07 62893.4 17341.2 6855.37 1.67936e+07 7006.3 6.30784e+06 43725.6 47396.3 5771.02 1.67936e+07 54809.3 5735.27 1.67936e+07 4373.5 17176.1 19492.8 3972.38 1.67936e+07 17576.4 14802.5 9795.27 46424.3 831500 1.17237e+06 8.17199e+06 3.13663e+07
78188 20231031.34 27969.8 2.30851e+07 0.777414 5602.33 8.59996e+07 14059.1 1.88908e+07 14173.3 1.05021e+07 15545.1 1.46964e+07 1434.6 1.05021e+07 69302.6 17118.8 7223.17 1.67936e+07 6938.2 6.30784e+06 43790 47386.9 5775.87 1.67936e+07 54591.4 5491.97 1.67936e+07 4355.1 17093.8 17419.8 3979.22 1.67936e+07 17431.3 14898.7 9859.67 39990.1 830634 1.18149e+06 8.13241e+06 3.07346e+07
78196 20231101.2 28088.2 2.30851e+07 0.832989 5623.15 8.59996e+07 14070.4 1.88908e+07 14239.9 1.05021e+07 15638 1.46964e+07 1437.9 1.25993e+07 88490.7 17212.9 6871.58 1.88908e+07 7054.3 6.30784e+06 43839.1 47046.4 5818.22 1.67936e+07 50979.6 5735.09 1.67936e+07 4393 17147.3 19277.1 3977.77 1.67936e+07 17624.4 14959.6 10005.4 44220.3 834004 1.18027e+06 8.15222e+06 3.09693e+07
78218 20231101.11 27482.4 2.30851e+07 0.794466 5594.46 8.59996e+07 14033 1.88908e+07 14051.8 1.05021e+07 15531.3 1.46964e+07 1428.2 1.25993e+07 83063.2 17267 6867.98 1.67936e+07 6933.2 6.30784e+06 43523.4 39919.2 5807.77 1.67936e+07 54609.1 5469.02 1.67936e+07 4338.1 17157.6 18949.1 3994.19 1.67936e+07 17376.4 14871.1 10180.4 45431.3 833473 1.18618e+06 8.15072e+06 3.08689e+07
78226 20231101.13 27521.2 2.51822e+07 0.798772 5625.43 8.59996e+07 14043.1 1.88908e+07 14097.8 1.05021e+07 15604.3 1.46964e+07 1414.9 1.25993e+07 73492.7 17229.8 7241.73 1.67936e+07 6889 6.30784e+06 43650.8 46528.9 5756.54 1.67936e+07 47448.2 5445.43 1.67936e+07 4341.1 17155.8 18953.8 3965.05 1.67936e+07 14940.7 14721.7 10072.6 46340.6 835263 1.18362e+06 8.1689e+06 3.06211e+07
78246 20231101.20 27565 2.30851e+07 0.784451 5643.71 8.59996e+07 14099.1 1.88908e+07 14165.3 1.05021e+07 15684.7 1.46964e+07 1423.7 1.25993e+07 70500.2 17123.7 7247.5 1.67936e+07 6996.2 6.30784e+06 45792.5 46974.8 5794.78 1.67936e+07 53423.6 5485.63 1.67936e+07 4408.4 17022.2 19427.7 3992.72 1.67936e+07 15054.6 14945.9 10275.3 45075.5 837584 1.17997e+06 8.17199e+06 3.10982e+07
78261 20231101.25 28224.5 2.51822e+07 0.81842 5612.19 8.59996e+07 14117.8 1.88908e+07 14186 1.05021e+07 15647.1 1.25993e+07 1436.8 1.25993e+07 69365.6 17440.2 7264.49 1.67936e+07 7000.4 6.30784e+06 45894.6 47638.6 5797.39 1.67936e+07 53299.1 5486.18 1.67936e+07 4380.3 17042 19569.5 3994.48 1.67936e+07 17247.3 14729.7 10279.9 43354.3 835866 1.1715e+06 8.14353e+06 3.07998e+07
78284 20231102.4 27902.1 2.30851e+07 0.775601 5607 8.59996e+07 14039.4 1.88908e+07 14144.7 1.05021e+07 15534.3 1.46964e+07 1433.6 1.25993e+07 74128.5 17090 6870.67 1.88908e+07 7007.8 6.30784e+06 43810.2 47171.4 5753.55 1.67936e+07 53039.6 5431.34 1.67936e+07 4380.6 16902.4 19632.5 3982.9 1.67936e+07 14945.6 14982 10242.7 40950.5 830357 1.18333e+06 8.13473e+06 3.08373e+07
78305 20231102.12 27661.5 2.30851e+07 0.78799 5520.15 8.59996e+07 14034 1.88908e+07 14105 1.05021e+07 15532.4 1.25993e+07 1421.1 1.25993e+07 88216.8 17322.6 6844.95 1.88908e+07 7082.4 6.30784e+06 45645.4 48989.3 5797.56 1.67936e+07 53847.3 5725.47 1.88908e+07 4386.2 17291.3 19701.3 4001.42 1.67936e+07 17082.4 14871.8 10051.9 40964.4 822024 1.17786e+06 8.15592e+06 3.10807e+07
78319 20231102.17 27989.4 2.30851e+07 0.793434 5616.9 8.59996e+07 13956 1.88908e+07 14087.7 1.05021e+07 15500.2 1.46964e+07 1432 1.25993e+07 83397.2 17142.8 6839.82 1.67936e+07 6924.1 6.30784e+06 45692.3 48014.1 5801.1 1.67936e+07 53896.9 5739.65 1.67936e+07 4359.7 17057.3 19245.9 3972.71 1.67936e+07 17127.5 14800.7 10296.3 45008.6 834976 1.18569e+06 8.12273e+06 3.07789e+07

mku-TraceAlias

build_id build_number pi_basic_mt_sgx_cft^ pi_basic_mt_sgx_cft_mem Commit latency factor tpcc_sgx_cft^ tpcc_sgx_cft_mem pi_basic_mt_virtual_cft^ tpcc_virtual_cft^ ls_sgx_cft^ ls_sgx_cft_mem ls_virtual_cft^ pi_ls_sgx_cft^ pi_ls_sgx_cft_mem pi_ls_virtual_cft^ pi_basic_virtual_cft^ pi_basic_sgx_cft^ pi_basic_sgx_cft_mem pi_basic_js_virtual_cft^ ls_jwt_virtual_cft^ pi_ls_jwt_virtual_cft^ ls_js_virtual_cft^ pi_basic_js_sgx_cft^ pi_basic_js_sgx_cft_mem ls_full_js_virtual_cft^ ls_jwt_sgx_cft^ ls_jwt_sgx_cft_mem ls_js_jwt_virtual_cft^ 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 hist_sgx_cft^ ls_js_jwt_sgx_cft^ ls_js_jwt_sgx_cft_mem RB put (/s)^ CHAMP put (/s)^ RB get (/s)^ CHAMP get (/s)^
78354 20231103.1 28341.6 2.30851e+07 0.808764 5561.57 8.59996e+07 87437 17294.1 14062.1 1.88908e+07 45567.5 14153 1.05021e+07 48191.6 54860.8 15620.7 1.46964e+07 4401.1 17059.4 19076 14906.3 1436.2 1.25993e+07 14787 7250.4 1.67936e+07 10286.4 6927.2 6.30784e+06 5809.21 1.67936e+07 5725.52 1.88908e+07 46959 3992.04 1.67936e+07 834777 1.1783e+06 8.15348e+06 3.15572e+07

images

@lemmy lemmy merged commit fdba7d5 into main Nov 3, 2023
32 checks passed
@lemmy lemmy deleted the mku-TraceAlias branch November 3, 2023 09:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@heidihoward heidihoward heidihoward approved these changes

Assignees
No one assigned
Labels
tla TLA+ specifications
Projects
None yet
Milestone
TLA+ Trace Validation (Consensus)
Development

Successfully merging this pull request may close these issues.
2 participants
@lemmy @heidihoward