These are results of the experiments for APLAS’19:

Parameter Value
Timeout 300 s
Benchmarks 124
Max states 6088

Data

Method Value
total 124
wins Safra 100
wins Schewe 14
ties 10

Wins Safra

Wins Schewe

Ties

Purging: combined vs. only direct/delayed

Purge vs. Purge+SAT

Comparison of our optimizations with basic Schewe

Comparison of our optimizations with quotioned Schewe

LS0tCnRpdGxlOiAiQnVjaGkgQXV0b21hdGEgQ29tcGxlbWVudGF0aW9uIFJlc3VsdHMgQW5hbHlzaXMiCnBhcmFtczoKICAjZGlyOiAuL3Jlc3VsdHMtMDYtMDUtMjAxOQogICNmaWxlOiBzbm9ydC1maWx0ZXJlZC1yZXN1bHRzLnRzdgpvdXRwdXQ6CiAgaHRtbF9ub3RlYm9vazoKICAgIGNvZGVfZm9sZGluZzogaGlkZQogIHBkZl9kb2N1bWVudDogZGVmYXVsdAogIGh0bWxfZG9jdW1lbnQ6CiAgICBkZl9wcmludDogcGFnZWQKICAgIHRvYzogdHJ1ZQogICAgdG9jX2Zsb2F0OiB0cnVlIAotLS0KClRoZXNlIGFyZSByZXN1bHRzIG9mIHRoZSBleHBlcmltZW50cyBmb3IgQVBMQVMnMTk6CgpgYGB7ciBlY2hvPUZBTFNFfQojIFNFVFRJTkdTCgojIGxvYWQgdGhlIHBsb3R0aW5nIGxpYnJhcnkKc3VwcHJlc3NNZXNzYWdlcyhsaWJyYXJ5KGdncGxvdDIpKQpsaWJyYXJ5KGdyaWQpCmxpYnJhcnkoZ3JpZEV4dHJhKQpsaWJyYXJ5KHRpa3pEZXZpY2UpCgp0aGVtZV9zZXQodGhlbWVfYncoKSkKCm9wdGlvbnMoc2NpcGVuPTk5OSkgICMgdHVybi1vZmYgc2NpZW50aWZpYyBub3RhdGlvbiBsaWtlIDFlKzQ4CgojIHNpemUgb2YgcG9pbnQgZm9yIHNjYXR0ZXJwbG90cwpQT0lOVF9TSVpFPTAuMQoKRklMRVM9YygnZ29hbCcsICdkaXInLCAnZGVsJywgJ2NvbWInLCAnZGlyLXF1b3QnLCAnZGVsLXF1b3QnLCAnY29tYi1xdW90JywgJ2dvYWwtcXVvdCcpCiNGSUxFUz1jKCdnb2FsJywgJ2RpcicsICdkaXIyJywgJ2RlbCcsICdkZWwyJywgJ2NvbWInLCAnY29tYjInLCAnZGlyLXF1b3QnLCAnZGVsLXF1b3QnLCAnY29tYi1xdW90JykKCmBgYAoKCmBgYHtyIGVjaG89RkFMU0V9CgpkZiA9IGRhdGEuZnJhbWUoKQoKcmVhZF9maWxlID0gZnVuY3Rpb24oZikgewogICNwcmludChwYXN0ZTAoJ3Byb2Nlc3NpbmcgJywgZiwgJyAuLi4nKSkKICBwYXRoID0gcGFzdGUwKGYsICcuY3N2JykKICByZWFkLmNzdihwYXRoLCBoZWFkZXI9VFJVRSwgc2VwPSI7IiwgY29tbWVudC5jaGFyPScjJywgbmEuc3RyaW5ncz0nVE8nLCBzdHJpbmdzQXNGYWN0b3JzPUZBTFNFKQp9CgpkZiA9IHJlYWRfZmlsZShGSUxFU1sxXSkKCmZvciAoZiBpbiBGSUxFU1syOmxlbmd0aChGSUxFUyldKSB7CiAgdG1wID0gcmVhZF9maWxlKGYpCiAgZGYgPSBtZXJnZShkZiwgdG1wKQojICBwcmludChwYXN0ZTAoZiwgJzogJywgbnJvdyhkZikpKQp9CgojIGdldCB0aGUgdmFsdWUgdG8gdXNlIGZvciB0aW1lb3V0cwptYXhfc3RhdGVzID0gbWF4KGRmWy0xXSwgbmEucm09VFJVRSkKdGltZW91dF9zdGF0ZXMgPSBtYXhfc3RhdGVzICogMS4xCgojIHNhbml0aXplIHRoZSBpbnB1dApkZltpcy5uYShkZildIDwtIHRpbWVvdXRfc3RhdGVzCgojIHJlbW92ZSB0cml2aWFsIGNhc2VzCmRmID0gZGZbZGYkU2NoZXdlICE9IDAsXQpgYGAKCnwgUGFyYW1ldGVyICAgICAgfCAgVmFsdWUgICAgICAgICB8CnwtLS0tLS0tLS0tLS0tLS0tfC0tLS0tLS0tLS0tLS0tLS18CnwgKipUaW1lb3V0KiogICAgfCAzMDAgcyAgICAgICAgICB8CnwgKipCZW5jaG1hcmtzKiogfCBgciBucm93KGRmKWAgICB8CnwgKipNYXggc3RhdGVzKiogfCBgciBtYXhfc3RhdGVzYCB8CgojIERhdGEKCmBgYHtyIGVjaG89RkFMU0V9CmRmCmBgYAoKCmBgYHtyIGVjaG89RkFMU0V9CnhfYXhpcyA9ICdTYWZyYScKeV9heGlzID0gJ1NjaGV3ZScKCnNjYXQgPSBmdW5jdGlvbihkZiwgeF9heGlzLCB5X2F4aXMpIHsKZ2dwbG90KGRmLCBhZXNfc3RyaW5nKHg9eF9heGlzLCB5PXlfYXhpcykpICsKICBnZW9tX3BvaW50KHNpemU9UE9JTlRfU0laRSkgKwogIGdlb21fYWJsaW5lKHNpemU9MC4xKSArCiAgI3NjYWxlX3hfbG9nMTAoKSArCiAgI3NjYWxlX3lfbG9nMTAoKSArCiAgdGhlbWUoYXhpcy50ZXh0LnkgPSBlbGVtZW50X3RleHQoYW5nbGUgPSA5MCwgaGp1c3QgPSAwLjUpKSArCiAgY29vcmRfZml4ZWQoeGxpbSA9IGMoMS45LCA1MDApLCB5bGltID0gYygxLjksIDUwMCkpICsKICBsYWJzKAojICAgIHRpdGxlPSJUaW1lIiwKIyAgICBzdWJ0aXRsZT0iT3VyIHZzIFVuZm9sZGluZyAodG8gREZBKSIsCiAgICB4PXhfYXhpcywKICAgIHk9eV9heGlzKQp9CgpzY2F0KGRmLCB4X2F4aXMsIHlfYXhpcykKc2NhdChkZiwgJ1NhZnJhLnF1b3QnLCAnU2NoZXdlLnF1b3QnKQoKc2NhdChkZiwgJ1NjaGV3ZScsICdTY2hld2UucXVvdCcpCgpwMSA8LSBzY2F0KGRmLCAnU2NoZXdlJywgJ1JhbXNleScpCnAyIDwtIHNjYXQoZGYsICdTY2hld2UnLCAnU2FmcmEnKQpwMyA8LSBzY2F0KGRmLCAnU2NoZXdlJywgJ1NsaWNlJykKZ3JpZC5hcnJhbmdlKHAxLCBwMiwgcDMsIG5jb2wgPSAzKQoKcDEgPC0gc2NhdChkZiwgJ1NjaGV3ZS5xdW90JywgJ1JhbXNleS5xdW90JykKcDIgPC0gc2NhdChkZiwgJ1NjaGV3ZS5xdW90JywgJ1NhZnJhLnF1b3QnKQpwMyA8LSBzY2F0KGRmLCAnU2NoZXdlLnF1b3QnLCAnU2xpY2UucXVvdCcpCmdyaWQuYXJyYW5nZShwMSwgcDIsIHAzLCBuY29sID0gMykKCnAxIDwtIHNjYXQoZGYsICdTY2hld2UucXVvdC5wdXJnZS5jb21iJywgJ1JhbXNleS5xdW90JykKcDIgPC0gc2NhdChkZiwgJ1NjaGV3ZS5xdW90LnB1cmdlLmNvbWInLCAnU2FmcmEucXVvdCcpCnAzIDwtIHNjYXQoZGYsICdTY2hld2UucXVvdC5wdXJnZS5jb21iJywgJ1NsaWNlLnF1b3QnKQpncmlkLmFycmFuZ2UocDEsIHAyLCBwMywgbmNvbCA9IDMpCgoKYGBgCgpgYGB7ciBlY2hvPUZBTFNFfQoKeF93aW5zID0gZGZbZGZbLHhfYXhpc10gPCBkZlsseV9heGlzXSxdCnlfd2lucyA9IGRmW2RmWyx4X2F4aXNdID4gZGZbLHlfYXhpc10sXQp4eV90aWVzID0gZGZbZGZbLHhfYXhpc10gPT0gZGZbLHlfYXhpc10sXQpgYGAKCnwgTWV0aG9kICAgICAgICAgIHwgVmFsdWUgICAgICAgICAgICAgfAp8LS0tLS0tLS0tLS0tLS0tLS18LS0tLS0tLS0tLS0tLS0tLS0tLXwKfCB0b3RhbCAgICAgICAgICAgfCBgciBucm93KGRmKWAgICAgICB8Cnwgd2lucyBgciB4X2F4aXNgIHwgYHIgbnJvdyh4X3dpbnMpYCAgfAp8IHdpbnMgYHIgeV9heGlzYCB8IGByIG5yb3coeV93aW5zKWAgIHwKfCB0aWVzICAgICAgICAgICAgfCBgciBucm93KHh5X3RpZXMpYCB8CgojIFdpbnMgYHIgeF9heGlzYAoKYGBge3IgZWNobz1GQUxTRX0KeF93aW5zCmBgYAojIFdpbnMgYHIgeV9heGlzYAoKYGBge3IgZWNobz1GQUxTRX0KeV93aW5zCgpzY2F0KHlfd2lucywgeF9heGlzLCB5X2F4aXMpCmBgYAoKIyBUaWVzCgpgYGB7ciBlY2hvPUZBTFNFfQp4eV90aWVzCmBgYAoKIyBQdXJnaW5nOiBjb21iaW5lZCB2cy4gb25seSBkaXJlY3QvZGVsYXllZAoKYGBge3IgZWNobz1GQUxTRX0KcDEgPC0gc2NhdChkZiwgJ1NjaGV3ZS5wdXJnZS5kaXInLCAnU2NoZXdlLnB1cmdlLmNvbWInKQpwMiA8LSBzY2F0KGRmLCAnU2NoZXdlLnB1cmdlLmRlbCcsICdTY2hld2UucHVyZ2UuY29tYicpCmdyaWQuYXJyYW5nZShwMSwgcDIsIG5jb2wgPSAyKQoKcDEgPC0gc2NhdChkZiwgJ1NjaGV3ZS5xdW90LnB1cmdlLmRpcicsICdTY2hld2UucXVvdC5wdXJnZS5jb21iJykKcDIgPC0gc2NhdChkZiwgJ1NjaGV3ZS5xdW90LnB1cmdlLmRlbCcsICdTY2hld2UucXVvdC5wdXJnZS5jb21iJykKZ3JpZC5hcnJhbmdlKHAxLCBwMiwgbmNvbCA9IDIpCmBgYAoKIyBQdXJnZSB2cy4gUHVyZ2UrU0FUCgpgYGB7ciBlY2hvPUZBTFNFfQpwMSA8LSBzY2F0KGRmLCAnU2NoZXdlLnB1cmdlLmRpcicsICdTY2hld2UucHVyZ2Uuc2F0LmRpcicpCnAyIDwtIHNjYXQoZGYsICdTY2hld2UucHVyZ2UuZGVsJywgJ1NjaGV3ZS5wdXJnZS5zYXQuZGVsJykKcDMgPC0gc2NhdChkZiwgJ1NjaGV3ZS5wdXJnZS5jb21iJywgJ1NjaGV3ZS5wdXJnZS5zYXQuY29tYicpCmdyaWQuYXJyYW5nZShwMSwgcDIsIHAzLCBuY29sID0gMykKCnAxIDwtIHNjYXQoZGYsICdTY2hld2UucXVvdC5wdXJnZS5kaXInLCAnU2NoZXdlLnF1b3QucHVyZ2Uuc2F0LmRpcicpCnAyIDwtIHNjYXQoZGYsICdTY2hld2UucXVvdC5wdXJnZS5kZWwnLCAnU2NoZXdlLnF1b3QucHVyZ2Uuc2F0LmRlbCcpCnAzIDwtIHNjYXQoZGYsICdTY2hld2UucXVvdC5wdXJnZS5jb21iJywgJ1NjaGV3ZS5xdW90LnB1cmdlLnNhdC5jb21iJykKZ3JpZC5hcnJhbmdlKHAxLCBwMiwgcDMsIG5jb2wgPSAzKQpgYGAKCiMgQ29tcGFyaXNvbiBvZiBvdXIgb3B0aW1pemF0aW9ucyB3aXRoIGJhc2ljIFNjaGV3ZQoKYGBge3IgZWNobz1GQUxTRX0KcDEgPC0gc2NhdChkZiwgJ1NjaGV3ZScsICdTY2hld2UucHVyZ2UuZGlyJykKcDIgPC0gc2NhdChkZiwgJ1NjaGV3ZScsICdTY2hld2UucHVyZ2UuZGVsJykKcDMgPC0gc2NhdChkZiwgJ1NjaGV3ZScsICdTY2hld2UucHVyZ2UuY29tYicpCmdyaWQuYXJyYW5nZShwMSwgcDIsIHAzLCBuY29sID0gMykKCnAxIDwtIHNjYXQoZGYsICdTY2hld2UnLCAnU2NoZXdlLnB1cmdlLnNhdC5kaXInKQpwMiA8LSBzY2F0KGRmLCAnU2NoZXdlJywgJ1NjaGV3ZS5wdXJnZS5zYXQuZGVsJykKcDMgPC0gc2NhdChkZiwgJ1NjaGV3ZScsICdTY2hld2UucHVyZ2Uuc2F0LmNvbWInKQpncmlkLmFycmFuZ2UocDEsIHAyLCBwMywgbmNvbCA9IDMpCgpgYGAKCiMgQ29tcGFyaXNvbiBvZiBvdXIgb3B0aW1pemF0aW9ucyB3aXRoIHF1b3Rpb25lZCBTY2hld2UKCmBgYHtyIGVjaG89RkFMU0V9CnAxIDwtIHNjYXQoZGYsICdTY2hld2UucXVvdCcsICdTY2hld2UucXVvdC5wdXJnZS5kaXInKQpwMiA8LSBzY2F0KGRmLCAnU2NoZXdlLnF1b3QnLCAnU2NoZXdlLnF1b3QucHVyZ2UuZGVsJykKcDMgPC0gc2NhdChkZiwgJ1NjaGV3ZS5xdW90JywgJ1NjaGV3ZS5xdW90LnB1cmdlLmNvbWInKQpncmlkLmFycmFuZ2UocDEsIHAyLCBwMywgbmNvbCA9IDMpCgpwMSA8LSBzY2F0KGRmLCAnU2NoZXdlLnF1b3QnLCAnU2NoZXdlLnF1b3QucHVyZ2Uuc2F0LmRpcicpCnAyIDwtIHNjYXQoZGYsICdTY2hld2UucXVvdCcsICdTY2hld2UucXVvdC5wdXJnZS5zYXQuZGVsJykKcDMgPC0gc2NhdChkZiwgJ1NjaGV3ZS5xdW90JywgJ1NjaGV3ZS5xdW90LnB1cmdlLnNhdC5jb21iJykKZ3JpZC5hcnJhbmdlKHAxLCBwMiwgcDMsIG5jb2wgPSAzKQoKYGBg