A Dataset for the Synthesis of Linear Ranking Functions

This dataset contains randomly generated linear arithmetic simple while (LASW) programs and the corresponding information on their linear ranking functions (LRF). Three different types/levels of information on LRF are provided: (S1) the type of linear ranking function, trivial, nontrivial, or nonexistent; (S2) in the case that an LASW admits a nontrivial LRF, one nontrivial LRF is provided and is represented by its coefficients; (S3) in the case that an LASW admits nontrivial LRFs, the defining linear system for all LRFs is provided. The Classification subdiretory contains LASW programs and the corresponding information S1. It contains 42 million examples in total, including 2 million examples for 1-variable LASW programs and 10 million examples for each variable setting from 2 to 5.The Generation subdiretory contains LASW programs and the corresponding information S2. It contains 2,452,231 examples in total, including 190,941 examples in 1v_n, 381,961 examples in 1v_d, 788,825 examples in 2v_d_4m2p, 57,737  examples in 2v_n_3m2p, 184,900 examples in 2v_n_4m1p, 331,933 examples in 2v_n_4m2p, 101,514  examples in 2v_n_4m3p, 298,392 examples in 3v_d_6m3p, and 116,028 examples in 3v_n_6m3p.The Elimination subdiretory contains LASW programs and the corresponding information S3. It contains 2, 667, 684 examples in total, including 190,941 examples in 1v_n, 381,961 examples in 1v_d, 676, 084 examples in 2v_n, 331,933 examples in 2v_n_4m2p, 298,392 examples in 3v_d_6m3p, and 331, 481 examples in 3v_n. The details for generating these systems are explained in the following paper: Yuxing Cai, Changbo Chen and Yi Li.

Generating Linear Ranking Functions for Program Termination Using Transformers. 2025 International Conference on Data Science and Intelligent Systems (DSIS), Chengdu, China, 2025, pp. 1-6.More information about the dataset can be found in readme.txt.