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

A tutorial on property-based testing and Apalache-TLC #1831

Closed
wants to merge 42 commits into from
Closed

A tutorial on property-based testing and Apalache-TLC #1831

Show file tree
Hide file tree
Changes from 18 commits
Commits
Show all changes
42 commits
Select commit Hold shift + click to select a range
c56be04
copy the examples
konnov May 25, 2022
80fdfb2
update the test file
konnov May 25, 2022
6577031
work in progress on the tutorial
konnov May 25, 2022
604ba6f
finish on symbolic simulation
konnov May 27, 2022
123a7e6
update the specs
konnov May 27, 2022
e0335b5
an almost complete version
konnov May 27, 2022
08cf416
finished the tutorial
konnov May 28, 2022
5a3d9f2
proof reading
konnov May 28, 2022
836e808
update the figure
konnov May 28, 2022
030c298
fix the figure
konnov May 28, 2022
1581107
update the test
konnov May 28, 2022
67e1318
increasing the number of steps
konnov May 28, 2022
e4587d3
rollback the test parameters
konnov May 28, 2022
c76b2fa
finish the tutorial on Hypothesis, Apalache, and TLC
konnov May 30, 2022
04a1536
bump the required version
konnov May 30, 2022
cb7ff94
add the rendered version
konnov May 30, 2022
1cc94da
add release note
konnov May 30, 2022
288deb5
Merge branch 'unstable' into ik/pbt-tutorial
konnov May 30, 2022
264fb26
Red trails are medium, blue trails are easy
p-offtermatt May 30, 2022
875bd3e
Merge branch 'ik/pbt-tutorial'
konnov May 31, 2022
3b6938f
rename randomized.md to pbt-and-tla.md
konnov May 31, 2022
2d83787
Merge branch 'unstable' into ik/pbt-tutorial
konnov May 31, 2022
340aee1
Merge branch 'unstable' into ik/pbt-tutorial
konnov Jun 1, 2022
a91bec9
comments, p1
Kukovec May 30, 2022
330a809
comments, p2
Kukovec May 30, 2022
6dfedab
math
Kukovec Jun 1, 2022
c9ffa37
update the experiments table
konnov Jun 2, 2022
9b5a28d
update the table again
konnov Jun 2, 2022
eafb52a
typeset math
Kukovec Jun 3, 2022
a38a073
Merge branch 'unstable' into ik/pbt-tutorial
konnov Jun 7, 2022
0d79a29
add a fresh version
konnov Jun 7, 2022
740bbf8
add Jure as a co-author to pdf
konnov Jun 7, 2022
be50058
remove nworkers
konnov Jun 7, 2022
cee2aa2
Apply stylistic fixes
thpani Jun 8, 2022
b161cf9
Replace verbatim with blockquote
thpani Jun 8, 2022
0c7bd1b
Move paragraph to make it a bridge
thpani Jun 8, 2022
1f41fba
Apply stylistic fixes
thpani Jun 8, 2022
38bfec2
Number the math sections
thpani Jun 8, 2022
3817ce7
Apply stylistic fixes
thpani Jun 8, 2022
85b45e2
Stylistic fixes
thpani Jun 8, 2022
20b6754
Wrap some multi-letter identifiers
thpani Jun 8, 2022
8665225
Merge branch 'main' into ik/pbt-tutorial
Jan 3, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions docs/src/SUMMARY.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,6 +9,7 @@
- [Type Checker Tutorial](./tutorials/snowcat-tutorial.md)
- [Checking Pluscal specifications](./tutorials/pluscal-tutorial.md)
- [Apalache trail tips: how to check your specs faster](./tutorials/trail-tips.md)
- [Checking ERC20 with Property-Based Testing and TLA+](./tutorials/randomized.md)
- [Symbolic Model Checking](./tutorials/symbmc.md)

# Apalache User Manual
Expand Down
1 change: 1 addition & 0 deletions docs/src/tutorials/img/controls.drawio
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
<mxfile host="Electron" modified="2022-05-28T17:03:48.602Z" agent="5.0 (Macintosh; Intel Mac OS X 10_15_7) AppleWebKit/537.36 (KHTML, like Gecko) draw.io/18.0.6 Chrome/100.0.4896.143 Electron/18.2.3 Safari/537.36" etag="KiJWgyFXoaWXVTRwAYZe" version="18.0.6" type="device"><diagram id="RHhPhNMYOjOCZQmPz5UX" name="Page-1">7Vxbc5s4FP41nuk+1IMkLvZj7dTNzradzKSdnX3qKEYBJgIxIMdJfv1KBmxAcoxbc4njPCQgJAHnO9+5SWSE5uHTlwTH/jfmEjqChvs0QlcjCAEwbPFHtjxnLRMLZg1eErh5p13DbfBC8kYjb10FLkkrHTljlAdxtXHJoogseaUNJwlbV7vdM1q9a4w9ojTcLjFVW/8NXO7nbwGdXfs1CTy/uDOwp9mVEBed8zdJfeyydakJfR6hecIYz47CpzmhUniFXLJxiz1Xtw+WkIg3GQD/u5lFwPx+tZzS8OGfLy+zX85HOMmmecR0lb/xpxhTvPRJ/tT8uRBFug5CiiNxNrtnEV/gMKAS1WtCHwkPlji/kIMILXGesFXkEvkEQJzl9yIJJ0973wJsZSOUirCQ8ORZdMkHIJSLM9cnMz9d78CBdt7ml4Cxio44VwhvO/VOZuIgF9sxIoSKCP+O4hWXwhOSSEfQpuIhZneJOPLk0YfHAGcqm3Ic8fSvEfqkSFuISPb1eUhz6WEaeJE4puReXpFiFEKnn/LmMHBdOXiWEHFffLeZyBDnMQvETeSs1mxkXcmZVpylGUpy4pQn7IHMGWWJaIlYBnFAab2pBK7RFM5X1G4/yAcxBpYO49YgRgrECl4uTv2NohslbL7iO0JvhKx5wCRGd4xzFmrA4ywuIbwU0iOJRMbHsZw/fPKkeR17oUvHKRUmMYFSpXAiJhfXLUOBcQTRYjGfT6fiCovxMuBSmsDY9SzsGayhvRk5MTY9fRwJpSqDvjVjRo8aAQxLpb2hUQnYmkqYA1eJiX1qlZhOERquSkDH6VslLEUlbjmJN5Z+Jd50nx/4+JGSyOP+xQ0cQLigWNkPoC79gO0MnPRlLr8L1oOpJv7rlPW2GkF/X4V3AjZosHt5x6UEPb2Q+3UgLU2QN9EAiVoD0j5Mbk/kM/FekeQ5aA7LaKtzfyoqUBUVMk1V502NqIBptSQrpOY8iqyqqd/aDzi5FeZHXl0LI1bV+0pCOWdhsBST3WJBG2h8u9Uklr+vlxnOqrD7kyacqoFDEK4ozrzFMXZj6zHesuXYh1A+DRxbNdOhWg7QpeWADSxHr2GBlObbjgoOqETNQgJg9xwVQDVSrEYFyerYkOCsqZ0DZ2uorKvmtUZlBA5T+TfZW4K0QpKKZahSD2g4LhiXsMAdp+uAL/1f8s51etqbHzn2gYg+JTL27GKLacxaYqeGfrrIrzWyIjVx//F1ruA+iPq3bVVlp6mNWlCXE7dW/0ZDT4r1xVHbXiw2JDna+xnGfN5tcTRT0MaplNl3cdRSrehlSeSkGDt9L4kUy7ivsR6ncbYkex88SfaXkdMgUOd3EG7WZssyBnDXfhWEnnh0GtyJ3/hllRD5Sh6JSILF4y/mYljCaDpOH70m7m+/hdjH//bAhjVGazykZY+N8g9QwS+Wok8PvroeJmjLiQRiU+0qqJzgDOULlysJ7OQgmaGurt1e6avB+uYwyPzrmiXBizjB9A3y2jTQ2KkVL3TBrz0u1pLK8Dttwe80SHpaqnweYopTyxSQhiq6Yt2WYqe3fQ2KPUMtfTp7cosepamunijS7DV5cJyxder0YTrtNn3YB3tBsnr6AFSOdZs+qPXwavFsfvNzY3QS8h5raAfgrNVCdQukugJBe8FFA+/SK8XNk9cHhk1wiPomuK0mj99IyMTMFzbX2WxXjfNEpfO0SzY7DfL+fmJFMLhQsbjbmwwV4dBCRVONCi5+5MR+ZA/ogw0UVYJVd1waH1wSH72z8jz8yutYHo4SQad+xVRLUJcF86Nh1IUH3S6gmw3igwHuhTlfK91/tG82+FTisqfiTw2BZdRLy0hdBu50W4WpJv7velvjIQTRtupfAKgx5p1ubASqMb9+jhn3hbClisvZoXEz+6FAOYi9MjXn2PRTUbO1rTJD3yeq3ymDFhaYWb/jG7cjO/ON4HWODe4zwqHntPpo6Xw1Ak37jpaAmtNeEqHDONaiXqT7ZrzbREiBsboF7oLg6wjaGgC7Xbd6m194n5NtRlVv3f+3nupG8bptpsdS+wy2ux0ZdOm+9OzUNKt7TipV44tlPlBR0vnWTk3z0L84cKB+09A52eaaTmgKz6eyzeJ091+yNtdK/2sMff4f</diagram></mxfile>
4 changes: 4 additions & 0 deletions docs/src/tutorials/img/controls.drawio.svg
View file
Open in desktop
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
1 change: 1 addition & 0 deletions docs/src/tutorials/img/erc20.drawio
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
<mxfile host="Electron" modified="2022-05-25T11:31:33.519Z" agent="5.0 (Macintosh; Intel Mac OS X 10_15_7) AppleWebKit/537.36 (KHTML, like Gecko) draw.io/18.0.6 Chrome/100.0.4896.143 Electron/18.2.3 Safari/537.36" etag="DUiKgXPTrs-qWFw8SD77" version="18.0.6" type="device"><diagram name="Page-1" id="13e1069c-82ec-6db2-03f1-153e76fe0fe0">7Zlbb5swFMc/TaTuoZW5J49plm6aVGlapXXamwMOeAXMjHPbp58pNmCctKQhbXrJS+DYPrHP/3eODRlYk2T9hcIsuiYBigcmCNYD6/PANA0DuPyrsGxKy9AxS0NIcSA61YYb/A8JIxDWBQ5QrnRkhMQMZ6rRJ2mKfKbYIKVkpXabk1j91QyGSDPc+DDWrbc4YFG1LlA3fEU4jJhcn2iYQf8upGSRit9LSYrKlgRKN6JrHsGArBomazqwJpQQVl4l6wmKi7DKiJXjrna0VlOmKGVdBuTeTzT/9uP2evZ3if3oz2/jl3HulF6WMF6IUIxj7Isl5GwjA3S/RFR4MgbW5SrCDN1k0C9aVxwJbotYEotmSH0hsQ347ZykbEJiQu9dWeD+U9hxHDfsc/7xC3vOKLlDSoscwT0Jz4bL78XkEWVovTMqRhVrji8iCWJ0w7vIAVIeSa64XTUwkF2iBgG2sEFBXlh5riXgF0KFPRRxNUU0MVDA4RW3hLKIhCSF8bS2NsUoooM56VzXMOW2GWGMJLwBpcG4SJ3CSYbS0iKiO3xQhhoGUIlQzEmRICcL6qPH0esgFUUxZHip+t8WeDH0O8HcYy3xUJXYHba0Y5CGiIlRLfmqaTxdUU9T9DIm/p0fQZy+n0Sz3BNLtOEbSTRNgg655x0l0WzzZRNtpCnK1lyZcTGDLKNkic7E7sb9g0syKy+sT5rwe8o6K/JZ06uZRPYe+u1MIXBhAs9SQmyYWhbJoPdcNQ23JWYJmSbmo1QYo25U1I5kRzKf5+go5MhzaLNGF3i8l+LsghMrzobxjquzAbaLdWBGu+7LlmdZq5T6bD5en82P+tyhPlfP0ofWZ9M5wfpsbUHHKtFhFKb5HNErSpKzCpoGSNMlemUb/Tm4AKanqHJu6iW5J5LadcH0eiLJaiN5CiTZGkk+SRLMzvhZsTc+2kSoB4ceCg1whkMl1s7R8NBUbW/6T8ajzdkBeHAB4KbRIytG5A8sarR9UTvn3u7vKf35RTmDflnV385VrPZXy94yqzboiVXbOh1W5aK6sirnflxW9feWFav9HeDeNKt9PWDbPT5gH8yquyero+dgVX8jy9b2vqfJV/NY8rKnSaev44LT8XH1WU+T+kvkqurZH1WvyzvivnZo94R2aHfPHdo9bIfmt/XfyGX3+m96a/of</diagram></mxfile>
Loading