lemmy / ewd998 Goto Github PK

Distributed termination detection on a ring, due to Shmuel Safra: https://www.cs.utexas.edu/users/EWD/ewd09xx/EWD998.PDF

License: MIT License

Shell 4.55% TLA 95.45%

tlaplus specification model-checking theorem-proving safety liveness refinement

ewd998's Introduction

Repository Has Moved

IMPORTANT NOTICE:

As of May 2022, this repository has been migrated to a new location. The development, maintenance, and distribution of the project will now be done from the new repository at https://github.com/tlaplus-workshops/ewd998/.

Please update your bookmarks, clones, and remotes to the new repository location.

ewd998

Experience TLA+ in action by specifying distributed termination detection on a ring, due to Shmuel Safra. Each git commit introduces a new TLA+ concept. Go back to the very first commit to follow along!

v00: IDE

Click either one of the buttons to launch a zero-install IDE to give the TLA+ specification language a try:

(=> Screencast how to create the TLA+ Codespace)

v01: Problem statement - Termination detection in a ring

v01a: Termination of pleasingly parallel

For this tutorial, we assume that the distributed system nodes are organized as a ring, with one the (unique) leader[^1]. If we further assume that nodes execute independent computations, (global) termination detection becomes trivial--the leader initiates a token transfer around the ring, and each node passes the token to its next neighbor, iff the node finished its computation. When the initiator receives back the token, it knows that all (other) nodes have terminated.

This problem is too simple, and we don't need TLA+ to model it.

[^1] Perhaps by some leader election algorithm.

v01b: Termination of collaborative computation

A more interesting problem is to look at a "collaborative" computation, which implies that nodes can re-activate each other. For example, the result of a computation at node 23 is (atomically!) sent to and further processed at node 42. With the previous protocol, node 42 might have already passed on the token, causing the initiator to eventually detect (global) termination; a bug that is at least difficult to reproduce with testing! A solution is offered in EWD840:

Initiator sends a "stateful" token around the ring
Each node remembers if it activated another node
Activation taints the token (when the activator gets the token)
Initiator keeps running rounds until it receives an untainted token

v01c: Termination detection with asynchronous message delivery

What happens if we loosen the restriction that message delivery is atomic (it seldom is)? Clearly, we are back at square one:

Node 23 sends a message to 42
23 taints the token
Initiator starts a new round
Node 42 received the fresh token before receiving the activation message from 23
Boom!

The fix proposed in Shmuel Safra's EWD998, is to count in-flight messages. But will this work?

Throughout the chapters of this tutorial, we will use the TLA+ specification language to model EWD998, and check interesting properties.

v02: High-level spec AsyncTerminationDetection

TLA+ is all about abstraction, and, as we will later see, has first-class support to connect different levels of abstraction. Let's use this and write a basic spec that either falsifies our design above, or gives us sufficient confidence to invest in writing a more detailed spec.

(Credit: Stephan Merz wrote AsyncTerminationDetection)

v02a: Spec skeleton

Instead of modeling message channels, let alone modeling the transport layer, we will write a spec that models:

A ring of N nodes
The activation status of each node
The number of messages pending[^2] at a node
A send action
A receive action
A terminate action
The initial configuration of the system

Please switch to AsyncTerminationDetection.tla and read its comments. From here on, the tutorial continues there...

[^2] It's difficult to (efficiently) count pending messages in an implementation. In a TLA+ spec, we don't care about that notion of efficiency. Also, all variables are global.

ewd998's People

Contributors

Stargazers

Watchers

Forkers

pron kgusakov tsafin lalo gageames akosyakov calin-teodorescu indirapriyadarshini zjianwu avmi jakedern-msft sanderleung

ewd998's Issues

Codetour via VSCode extension

https://marketplace.visualstudio.com/items?itemName=vsls-contrib.codetour
CodeTour Github Action Watcher: https://github.com/marketplace/actions/codetour-watch

[Notes] Checking `EWD998` with TLC and Apalache for various values of the spec's constant `N`.

N=3

root@sv-c2-large-arm-01:~/ewd998# java -XX:+UseParallelGC -jar ../tla2tools.jar -workers 32 -deadlock -noTE MCEWD998
TLC2 Version 2.16 of Day Month 20?? (rev: d3e1b30)
Running breadth-first search Model-Checking with fp 101 and seed -3028980532272467495 with 32 workers on 32 cores with 27305MB heap and 64MB offheap memory [pid: 5481] (Linux 5.4.0-40-generic aarch64, Private Build 14.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /root/ewd998/MCEWD998.tla
Parsing file /root/ewd998/EWD998.tla
Parsing file /tmp/Integers.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/Naturals.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /root/ewd998/AsyncTerminationDetection.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module AsyncTerminationDetection
Semantic processing of module EWD998
Semantic processing of module MCEWD998
Starting... (2021-06-10 18:10:57)
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Finished computing initial states: 64 distinct states generated at 2021-06-10 18:10:57.
Progress(12) at 2021-06-10 18:11:00: 358,163 states generated (358,163 s/min), 63,369 distinct states found (63,369 ds/min), 14,485 states left on queue.
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 = 1.3E-8
  based on the actual fingerprints:  val = 2.8E-11
1368083 states generated, 197886 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 43.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 9 and the 95th percentile is 3).
Finished in 06s at (2021-06-10 18:11:02)

N=4

root@sv-c2-large-arm-01:~/ewd998# java -XX:+UseParallelGC -jar ../tla2tools.jar -workers 32 -deadlock -noTE MCEWD998
TLC2 Version 2.16 of Day Month 20?? (rev: d3e1b30)
Running breadth-first search Model-Checking with fp 38 and seed -5994353240307551040 with 32 workers on 32 cores with 27305MB heap and 64MB offheap memory [pid: 5586] (Linux 5.4.0-40-generic aarch64, Private Build 14.0.2 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /root/ewd998/MCEWD998.tla
Parsing file /root/ewd998/EWD998.tla
Parsing file /tmp/Integers.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/Naturals.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /root/ewd998/AsyncTerminationDetection.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module AsyncTerminationDetection
Semantic processing of module EWD998
Semantic processing of module MCEWD998
Starting... (2021-06-10 18:11:12)
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Computed 128 initial states...
Finished computing initial states: 256 distinct states generated at 2021-06-10 18:11:13.
Progress(6) at 2021-06-10 18:11:16: 561,245 states generated (561,245 s/min), 115,930 distinct states found (115,930 ds/min), 73,767 states left on queue.
Progress(17) at 2021-06-10 18:12:16: 58,504,734 states generated (57,943,489 s/min), 6,219,064 distinct states found (6,103,134 ds/min), 829,938 states left on queue.
Progress(27) at 2021-06-10 18:13:16: 114,973,568 states generated (56,468,834 s/min), 11,632,002 distinct states found (5,412,938 ds/min), 429,693 states left on queue.
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 = 1.3E-4
  based on the actual fingerprints:  val = 4.4E-8
162930570 states generated, 15951962 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 74.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 14 and the 95th percentile is 3).
Finished in 02min 58s at (2021-06-10 18:14:09)

N=5

root@sv-c2-large-arm-01:~/ewd998# java -XX:MaxDirectMemorySize=64g -Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.OffHeapDiskFPSet -XX:+UseParallelGC -jar ../tla2tools.jar -workers 32 -deadlock -noTE MCEWD998
TLC2 Version 2.16 of Day Month 20?? (rev: d3e1b30)
Running breadth-first search Model-Checking with fp 38 and seed -997024432319326617 with 32 workers on 32 cores with 27305MB heap and 65536MB offheap memory [pid: 5997] (Linux 5.4.0-40-generic aarch64, Private Build 14.0.2 x86_64, OffHeapDiskFPSet, DiskStateQueue).
Parsing file /root/ewd998/MCEWD998.tla
Parsing file /root/ewd998/EWD998.tla
Parsing file /tmp/Integers.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/Naturals.tla (jar:file:/root/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /root/ewd998/AsyncTerminationDetection.tla
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module AsyncTerminationDetection
Semantic processing of module EWD998
Semantic processing of module MCEWD998
Starting... (2021-06-10 18:22:10)
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Computed 128 initial states...
Computed 256 initial states...
Computed 512 initial states...
Finished computing initial states: 1024 distinct states generated at 2021-06-10 18:22:48.
Progress(4) at 2021-06-10 18:22:51: 662,461 states generated (662,461 s/min), 199,953 distinct states found (199,953 ds/min), 158,402 states left on queue.
Progress(7) at 2021-06-10 18:23:51: 59,651,689 states generated (58,989,228 s/min), 6,826,129 distinct states found (6,626,176 ds/min), 3,636,297 states left on queue.
Progress(8) at 2021-06-10 18:24:51: 119,151,059 states generated (59,499,370 s/min), 11,961,095 distinct states found (5,134,966 ds/min), 5,532,873 states left on queue.
Progress(9) at 2021-06-10 18:25:51: 179,142,411 states generated (59,991,352 s/min), 16,883,375 distinct states found (4,922,280 ds/min), 7,276,583 states left on queue.
Progress(9) at 2021-06-10 18:26:51: 238,676,159 states generated (59,533,748 s/min), 21,202,656 distinct states found (4,319,281 ds/min), 8,265,445 states left on queue.
Progress(10) at 2021-06-10 18:27:51: 298,079,029 states generated (59,402,870 s/min), 25,901,294 distinct states found (4,698,638 ds/min), 9,588,050 states left on queue.
Progress(10) at 2021-06-10 18:28:51: 357,674,172 states generated (59,595,143 s/min), 30,276,947 distinct states found (4,375,653 ds/min), 10,539,671 states left on queue.
Progress(11) at 2021-06-10 18:29:51: 417,083,286 states generated (59,409,114 s/min), 34,155,648 distinct states found (3,878,701 ds/min), 11,208,241 states left on queue.
Progress(11) at 2021-06-10 18:30:51: 476,541,228 states generated (59,457,942 s/min), 39,327,619 distinct states found (5,171,971 ds/min), 12,771,900 states left on queue.
Progress(11) at 2021-06-10 18:31:51: 535,414,119 states generated (58,872,891 s/min), 43,602,570 distinct states found (4,274,951 ds/min), 13,504,665 states left on queue.
Progress(11) at 2021-06-10 18:32:51: 594,809,322 states generated (59,395,203 s/min), 47,335,701 distinct states found (3,733,131 ds/min), 14,052,900 states left on queue.
Progress(12) at 2021-06-10 18:33:51: 652,176,420 states generated (57,367,098 s/min), 52,758,449 distinct states found (5,422,748 ds/min), 15,602,218 states left on queue.
Progress(12) at 2021-06-10 18:34:51: 711,206,658 states generated (59,030,238 s/min), 57,195,344 distinct states found (4,436,895 ds/min), 16,647,530 states left on queue.
Progress(12) at 2021-06-10 18:35:51: 768,671,960 states generated (57,465,302 s/min), 61,525,043 distinct states found (4,329,699 ds/min), 17,426,507 states left on queue.
Progress(12) at 2021-06-10 18:36:51: 827,097,371 states generated (58,425,411 s/min), 65,221,261 distinct states found (3,696,218 ds/min), 17,960,972 states left on queue.
Progress(13) at 2021-06-10 18:37:51: 883,240,074 states generated (56,142,703 s/min), 70,408,154 distinct states found (5,186,893 ds/min), 19,255,784 states left on queue.
Progress(13) at 2021-06-10 18:38:51: 940,983,170 states generated (57,743,096 s/min), 75,155,463 distinct states found (4,747,309 ds/min), 20,556,345 states left on queue.
Progress(13) at 2021-06-10 18:39:51: 998,926,537 states generated (57,943,367 s/min), 79,461,656 distinct states found (4,306,193 ds/min), 21,303,843 states left on queue.
Progress(13) at 2021-06-10 18:40:51: 1,056,432,462 states generated (57,505,925 s/min), 83,760,266 distinct states found (4,298,610 ds/min), 22,058,371 states left on queue.
Progress(13) at 2021-06-10 18:41:51: 1,114,481,515 states generated (58,049,053 s/min), 87,483,790 distinct states found (3,723,524 ds/min), 22,602,185 states left on queue.
Progress(14) at 2021-06-10 18:42:51: 1,170,513,662 states generated (56,032,147 s/min), 92,447,989 distinct states found (4,964,199 ds/min), 23,670,958 states left on queue.
Progress(14) at 2021-06-10 18:43:51: 1,227,758,377 states generated (57,244,715 s/min), 97,359,134 distinct states found (4,911,145 ds/min), 24,897,936 states left on queue.
Progress(14) at 2021-06-10 18:44:51: 1,286,013,181 states generated (58,254,804 s/min), 101,508,530 distinct states found (4,149,396 ds/min), 25,698,062 states left on queue.
Progress(14) at 2021-06-10 18:45:51: 1,343,140,947 states generated (57,127,766 s/min), 105,802,514 distinct states found (4,293,984 ds/min), 26,373,027 states left on queue.
Progress(14) at 2021-06-10 18:46:51: 1,400,185,345 states generated (57,044,398 s/min), 110,045,160 distinct states found (4,242,646 ds/min), 27,018,082 states left on queue.
Progress(14) at 2021-06-10 18:47:51: 1,457,325,549 states generated (57,140,204 s/min), 113,944,392 distinct states found (3,899,232 ds/min), 27,615,590 states left on queue.
Progress(15) at 2021-06-10 18:48:51: 1,513,123,568 states generated (55,798,019 s/min), 118,080,775 distinct states found (4,136,383 ds/min), 28,185,680 states left on queue.
Progress(15) at 2021-06-10 18:49:51: 1,569,160,717 states generated (56,037,149 s/min), 122,784,996 distinct states found (4,704,221 ds/min), 29,026,295 states left on queue.
Progress(15) at 2021-06-10 18:50:51: 1,625,615,273 states generated (56,454,556 s/min), 127,478,765 distinct states found (4,693,769 ds/min), 30,155,457 states left on queue.
Progress(15) at 2021-06-10 18:51:51: 1,682,156,731 states generated (56,541,458 s/min), 131,353,785 distinct states found (3,875,020 ds/min), 30,693,346 states left on queue.
Checkpointing of run states/21-06-10-18-22-08
Checkpointing completed at (2021-06-10 18:52:51)
Progress(15) at 2021-06-10 18:52:51: 1,738,919,983 states generated (56,763,252 s/min), 135,263,510 distinct states found (3,909,725 ds/min), 31,229,850 states left on queue.
Progress(15) at 2021-06-10 18:53:51: 1,794,805,385 states generated (55,885,402 s/min), 139,644,071 distinct states found (4,380,561 ds/min), 31,845,298 states left on queue.
Progress(15) at 2021-06-10 18:54:51: 1,851,496,737 states generated (56,691,352 s/min), 143,657,819 distinct states found (4,013,748 ds/min), 32,384,308 states left on queue.
Progress(15) at 2021-06-10 18:55:51: 1,908,169,743 states generated (56,673,006 s/min), 147,188,660 distinct states found (3,530,841 ds/min), 32,610,575 states left on queue.
Progress(16) at 2021-06-10 18:56:51: 1,963,377,843 states generated (55,208,100 s/min), 151,388,332 distinct states found (4,199,672 ds/min), 33,070,491 states left on queue.
Progress(16) at 2021-06-10 18:57:51: 2,018,947,217 states generated (55,569,374 s/min), 156,043,980 distinct states found (4,655,648 ds/min), 33,845,197 states left on queue.
Progress(16) at 2021-06-10 18:58:51: 2,075,184,036 states generated (56,236,819 s/min), 160,440,242 distinct states found (4,396,262 ds/min), 34,652,451 states left on queue.
Progress(16) at 2021-06-10 18:59:51: 2,131,422,324 states generated (56,238,288 s/min), 164,428,408 distinct states found (3,988,166 ds/min), 35,153,381 states left on queue.
Progress(16) at 2021-06-10 19:00:51: 2,187,252,722 states generated (55,830,398 s/min), 167,955,304 distinct states found (3,526,896 ds/min), 35,347,307 states left on queue.
Progress(16) at 2021-06-10 19:01:51: 2,243,021,376 states generated (55,768,654 s/min), 171,994,151 distinct states found (4,038,847 ds/min), 35,784,647 states left on queue.
Progress(16) at 2021-06-10 19:02:51: 2,299,080,487 states generated (56,059,111 s/min), 176,208,105 distinct states found (4,213,954 ds/min), 36,286,623 states left on queue.
Progress(16) at 2021-06-10 19:03:51: 2,355,667,535 states generated (56,587,048 s/min), 180,048,523 distinct states found (3,840,418 ds/min), 36,602,034 states left on queue.
Progress(16) at 2021-06-10 19:04:51: 2,412,059,687 states generated (56,392,152 s/min), 183,530,590 distinct states found (3,482,067 ds/min), 36,704,178 states left on queue.
Progress(17) at 2021-06-10 19:05:51: 2,466,849,043 states generated (54,789,356 s/min), 187,519,941 distinct states found (3,989,351 ds/min), 36,954,165 states left on queue.
Progress(17) at 2021-06-10 19:06:51: 2,522,249,632 states generated (55,400,589 s/min), 192,065,043 distinct states found (4,545,102 ds/min), 37,611,513 states left on queue.
Progress(17) at 2021-06-10 19:07:51: 2,578,205,762 states generated (55,956,130 s/min), 196,215,219 distinct states found (4,150,176 ds/min), 38,000,566 states left on queue.
Progress(17) at 2021-06-10 19:08:51: 2,634,462,340 states generated (56,256,578 s/min), 200,311,533 distinct states found (4,096,314 ds/min), 38,566,696 states left on queue.
Progress(17) at 2021-06-10 19:09:51: 2,690,033,319 states generated (55,570,979 s/min), 203,981,891 distinct states found (3,670,358 ds/min), 38,738,093 states left on queue.
Progress(17) at 2021-06-10 19:10:51: 2,745,175,936 states generated (55,142,617 s/min), 207,170,003 distinct states found (3,188,112 ds/min), 38,543,925 states left on queue.
Progress(17) at 2021-06-10 19:11:51: 2,800,620,790 states generated (55,444,854 s/min), 211,296,575 distinct states found (4,126,572 ds/min), 38,889,823 states left on queue.
Progress(17) at 2021-06-10 19:12:51: 2,856,827,996 states generated (56,207,206 s/min), 215,446,443 distinct states found (4,149,868 ds/min), 39,339,313 states left on queue.
Progress(17) at 2021-06-10 19:13:51: 2,912,873,131 states generated (56,045,135 s/min), 219,167,575 distinct states found (3,721,132 ds/min), 39,471,240 states left on queue.
Progress(17) at 2021-06-10 19:14:51: 2,968,775,742 states generated (55,902,611 s/min), 222,485,824 distinct states found (3,318,249 ds/min), 39,347,920 states left on queue.
Progress(18) at 2021-06-10 19:15:51: 3,023,586,451 states generated (54,810,709 s/min), 226,437,547 distinct states found (3,951,723 ds/min), 39,489,789 states left on queue.
Progress(18) at 2021-06-10 19:16:51: 3,078,753,441 states generated (55,166,990 s/min), 230,640,177 distinct states found (4,202,630 ds/min), 39,802,763 states left on queue.
Progress(18) at 2021-06-10 19:17:51: 3,134,523,266 states generated (55,769,825 s/min), 234,882,395 distinct states found (4,242,218 ds/min), 40,147,726 states left on queue.
Progress(18) at 2021-06-10 19:18:51: 3,190,390,208 states generated (55,866,942 s/min), 238,803,388 distinct states found (3,920,993 ds/min), 40,509,189 states left on queue.
Progress(18) at 2021-06-10 19:19:51: 3,246,334,472 states generated (55,944,264 s/min), 242,473,216 distinct states found (3,669,828 ds/min), 40,615,001 states left on queue.
Progress(18) at 2021-06-10 19:20:51: 3,301,235,528 states generated (54,901,056 s/min), 245,811,046 distinct states found (3,337,830 ds/min), 40,425,257 states left on queue.
Progress(18) at 2021-06-10 19:21:51: 3,355,615,639 states generated (54,380,111 s/min), 249,063,433 distinct states found (3,252,387 ds/min), 40,087,637 states left on queue.
Checkpointing of run states/21-06-10-18-22-08
Checkpointing completed at (2021-06-10 19:22:57)
Progress(18) at 2021-06-10 19:22:57: 3,416,714,215 states generated (61,098,576 s/min), 253,648,880 distinct states found (4,585,447 ds/min), 40,416,628 states left on queue.
Progress(18) at 2021-06-10 19:23:57: 3,472,852,793 states generated (56,138,578 s/min), 257,582,509 distinct states found (3,933,629 ds/min), 40,634,388 states left on queue.
Progress(18) at 2021-06-10 19:24:57: 3,528,603,792 states generated (55,750,999 s/min), 261,050,831 distinct states found (3,468,322 ds/min), 40,538,711 states left on queue.
Progress(19) at 2021-06-10 19:25:57: 3,583,401,487 states generated (54,797,695 s/min), 264,230,475 distinct states found (3,179,644 ds/min), 40,176,473 states left on queue.
Progress(19) at 2021-06-10 19:26:57: 3,638,273,971 states generated (54,872,484 s/min), 268,432,405 distinct states found (4,201,930 ds/min), 40,292,410 states left on queue.
Progress(19) at 2021-06-10 19:27:57: 3,694,316,978 states generated (56,043,007 s/min), 272,920,640 distinct states found (4,488,235 ds/min), 40,944,468 states left on queue.
Progress(19) at 2021-06-10 19:28:57: 3,749,692,494 states generated (55,375,516 s/min), 276,824,388 distinct states found (3,903,748 ds/min), 40,997,582 states left on queue.
Progress(19) at 2021-06-10 19:29:57: 3,805,096,294 states generated (55,403,800 s/min), 280,399,212 distinct states found (3,574,824 ds/min), 40,949,913 states left on queue.
Progress(19) at 2021-06-10 19:30:57: 3,860,269,826 states generated (55,173,532 s/min), 283,825,570 distinct states found (3,426,358 ds/min), 40,771,692 states left on queue.
Progress(19) at 2021-06-10 19:31:57: 3,914,411,188 states generated (54,141,362 s/min), 286,872,678 distinct states found (3,047,108 ds/min), 40,201,965 states left on queue.
Progress(19) at 2021-06-10 19:32:57: 3,969,805,958 states generated (55,394,770 s/min), 290,948,119 distinct states found (4,075,441 ds/min), 40,418,214 states left on queue.
Progress(19) at 2021-06-10 19:33:57: 4,025,576,912 states generated (55,770,954 s/min), 294,842,298 distinct states found (3,894,179 ds/min), 40,499,635 states left on queue.
Progress(19) at 2021-06-10 19:34:57: 4,081,426,051 states generated (55,849,139 s/min), 298,609,464 distinct states found (3,767,166 ds/min), 40,524,966 states left on queue.
Progress(19) at 2021-06-10 19:35:57: 4,136,555,497 states generated (55,129,446 s/min), 301,844,634 distinct states found (3,235,170 ds/min), 40,065,836 states left on queue.
Progress(20) at 2021-06-10 19:36:57: 4,192,012,439 states generated (55,456,942 s/min), 305,709,308 distinct states found (3,864,674 ds/min), 40,111,168 states left on queue.
Progress(20) at 2021-06-10 19:37:57: 4,246,833,655 states generated (54,821,216 s/min), 309,624,485 distinct states found (3,915,177 ds/min), 40,027,727 states left on queue.
Progress(20) at 2021-06-10 19:38:57: 4,302,973,025 states generated (56,139,370 s/min), 313,869,916 distinct states found (4,245,431 ds/min), 40,464,464 states left on queue.
Progress(20) at 2021-06-10 19:39:57: 4,358,008,381 states generated (55,035,356 s/min), 317,531,501 distinct states found (3,661,585 ds/min), 40,253,907 states left on queue.
Progress(20) at 2021-06-10 19:40:57: 4,412,812,380 states generated (54,803,999 s/min), 320,921,893 distinct states found (3,390,392 ds/min), 39,928,560 states left on queue.
Progress(20) at 2021-06-10 19:41:57: 4,467,272,755 states generated (54,460,375 s/min), 324,159,487 distinct states found (3,237,594 ds/min), 39,508,063 states left on queue.
Progress(20) at 2021-06-10 19:42:57: 4,521,070,761 states generated (53,798,006 s/min), 327,201,685 distinct states found (3,042,198 ds/min), 38,772,805 states left on queue.
Progress(20) at 2021-06-10 19:43:57: 4,577,424,246 states generated (56,353,485 s/min), 331,687,974 distinct states found (4,486,289 ds/min), 39,287,677 states left on queue.
Progress(20) at 2021-06-10 19:44:57: 4,633,264,804 states generated (55,840,558 s/min), 335,469,920 distinct states found (3,781,946 ds/min), 39,330,662 states left on queue.
Progress(20) at 2021-06-10 19:45:57: 4,688,759,639 states generated (55,494,835 s/min), 339,040,221 distinct states found (3,570,301 ds/min), 39,109,718 states left on queue.
Progress(21) at 2021-06-10 19:46:57: 4,742,953,384 states generated (54,193,745 s/min), 342,161,064 distinct states found (3,120,843 ds/min), 38,472,723 states left on queue.
Progress(21) at 2021-06-10 19:47:57: 4,799,137,799 states generated (56,184,415 s/min), 346,524,439 distinct states found (4,363,375 ds/min), 38,754,732 states left on queue.
Progress(21) at 2021-06-10 19:48:57: 4,854,734,586 states generated (55,596,787 s/min), 350,478,251 distinct states found (3,953,812 ds/min), 38,855,570 states left on queue.
Progress(21) at 2021-06-10 19:49:57: 4,910,005,881 states generated (55,271,295 s/min), 354,152,901 distinct states found (3,674,650 ds/min), 38,593,368 states left on queue.
Progress(21) at 2021-06-10 19:50:57: 4,964,840,241 states generated (54,834,360 s/min), 357,735,861 distinct states found (3,582,960 ds/min), 38,390,978 states left on queue.
Progress(21) at 2021-06-10 19:51:57: 5,018,583,443 states generated (53,743,202 s/min), 360,825,701 distinct states found (3,089,840 ds/min), 37,650,818 states left on queue.
Checkpointing of run states/21-06-10-18-22-08
Checkpointing completed at (2021-06-10 19:53:03)
Progress(21) at 2021-06-10 19:53:03: 5,077,582,457 states generated (58,999,014 s/min), 364,362,621 distinct states found (3,536,920 ds/min), 37,051,237 states left on queue.
Progress(21) at 2021-06-10 19:54:03: 5,133,960,422 states generated (56,377,965 s/min), 368,831,361 distinct states found (4,468,740 ds/min), 37,518,757 states left on queue.
Progress(21) at 2021-06-10 19:55:03: 5,189,527,989 states generated (55,567,567 s/min), 372,599,068 distinct states found (3,767,707 ds/min), 37,486,203 states left on queue.
Progress(21) at 2021-06-10 19:56:03: 5,244,758,475 states generated (55,230,486 s/min), 376,186,236 distinct states found (3,587,168 ds/min), 37,220,003 states left on queue.
Progress(22) at 2021-06-10 19:57:03: 5,299,506,933 states generated (54,748,458 s/min), 379,614,835 distinct states found (3,428,599 ds/min), 36,828,679 states left on queue.
Progress(22) at 2021-06-10 19:58:03: 5,355,571,299 states generated (56,064,366 s/min), 383,743,964 distinct states found (4,129,129 ds/min), 36,879,894 states left on queue.
Progress(22) at 2021-06-10 19:59:03: 5,411,284,608 states generated (55,713,309 s/min), 387,606,542 distinct states found (3,862,578 ds/min), 36,885,448 states left on queue.
Progress(22) at 2021-06-10 20:00:03: 5,466,183,529 states generated (54,898,921 s/min), 391,143,845 distinct states found (3,537,303 ds/min), 36,407,996 states left on queue.
Progress(22) at 2021-06-10 20:01:03: 5,520,375,644 states generated (54,192,115 s/min), 394,516,617 distinct states found (3,372,772 ds/min), 35,908,439 states left on queue.
Progress(22) at 2021-06-10 20:02:03: 5,573,902,070 states generated (53,526,426 s/min), 397,646,895 distinct states found (3,130,278 ds/min), 35,212,978 states left on queue.
Progress(22) at 2021-06-10 20:03:03: 5,629,719,623 states generated (55,817,553 s/min), 401,722,747 distinct states found (4,075,852 ds/min), 35,416,278 states left on queue.
Progress(22) at 2021-06-10 20:04:03: 5,685,357,100 states generated (55,637,477 s/min), 406,007,925 distinct states found (4,285,178 ds/min), 35,680,418 states left on queue.
Progress(22) at 2021-06-10 20:05:03: 5,740,456,254 states generated (55,099,154 s/min), 409,673,051 distinct states found (3,665,126 ds/min), 35,362,926 states left on queue.
Progress(22) at 2021-06-10 20:06:03: 5,795,317,351 states generated (54,861,097 s/min), 413,220,881 distinct states found (3,547,830 ds/min), 35,140,922 states left on queue.
Progress(23) at 2021-06-10 20:07:03: 5,852,625,525 states generated (57,308,174 s/min), 417,291,812 distinct states found (4,070,931 ds/min), 35,283,815 states left on queue.
Progress(23) at 2021-06-10 20:08:03: 5,907,561,634 states generated (54,936,109 s/min), 421,121,147 distinct states found (3,829,335 ds/min), 35,091,354 states left on queue.
Progress(23) at 2021-06-10 20:09:03: 5,962,427,211 states generated (54,865,577 s/min), 424,665,562 distinct states found (3,544,415 ds/min), 34,588,672 states left on queue.
Progress(23) at 2021-06-10 20:10:03: 6,016,684,353 states generated (54,257,142 s/min), 428,144,008 distinct states found (3,478,446 ds/min), 34,105,799 states left on queue.
Progress(23) at 2021-06-10 20:11:03: 6,069,831,903 states generated (53,147,550 s/min), 431,227,790 distinct states found (3,083,782 ds/min), 33,256,505 states left on queue.
Progress(23) at 2021-06-10 20:12:03: 6,126,542,993 states generated (56,711,090 s/min), 435,581,048 distinct states found (4,353,258 ds/min), 33,731,117 states left on queue.
Progress(23) at 2021-06-10 20:13:03: 6,182,037,656 states generated (55,494,663 s/min), 440,025,062 distinct states found (4,444,014 ds/min), 34,106,603 states left on queue.
Progress(23) at 2021-06-10 20:14:03: 6,237,058,393 states generated (55,020,737 s/min), 443,895,095 distinct states found (3,870,033 ds/min), 33,925,411 states left on queue.
Progress(24) at 2021-06-10 20:15:03: 6,292,064,215 states generated (55,005,822 s/min), 447,506,650 distinct states found (3,611,555 ds/min), 33,805,757 states left on queue.
Progress(24) at 2021-06-10 20:16:03: 6,349,501,518 states generated (57,437,303 s/min), 451,518,698 distinct states found (4,012,048 ds/min), 33,826,842 states left on queue.
Progress(24) at 2021-06-10 20:17:03: 6,404,465,857 states generated (54,964,339 s/min), 455,367,470 distinct states found (3,848,772 ds/min), 33,607,522 states left on queue.
Progress(24) at 2021-06-10 20:18:03: 6,458,619,589 states generated (54,153,732 s/min), 458,982,647 distinct states found (3,615,177 ds/min), 33,015,056 states left on queue.
Progress(24) at 2021-06-10 20:19:03: 6,512,242,165 states generated (53,622,576 s/min), 462,357,908 distinct states found (3,375,261 ds/min), 32,474,725 states left on queue.
Progress(24) at 2021-06-10 20:20:03: 6,567,408,836 states generated (55,166,671 s/min), 466,288,149 distinct states found (3,930,241 ds/min), 32,614,077 states left on queue.
Progress(24) at 2021-06-10 20:21:03: 6,623,399,472 states generated (55,990,636 s/min), 470,829,699 distinct states found (4,541,550 ds/min), 33,020,520 states left on queue.
Progress(24) at 2021-06-10 20:22:03: 6,678,615,467 states generated (55,215,995 s/min), 475,094,854 distinct states found (4,265,155 ds/min), 33,273,403 states left on queue.
Checkpointing of run states/21-06-10-18-22-08
Checkpointing completed at (2021-06-10 20:23:09)
Progress(24) at 2021-06-10 20:23:09: 6,739,473,832 states generated (60,858,365 s/min), 479,416,444 distinct states found (4,321,590 ds/min), 33,189,242 states left on queue.
Progress(25) at 2021-06-10 20:24:09: 6,796,182,005 states generated (56,708,173 s/min), 483,070,845 distinct states found (3,654,401 ds/min), 33,090,304 states left on queue.
Progress(25) at 2021-06-10 20:25:09: 6,851,408,522 states generated (55,226,517 s/min), 487,229,276 distinct states found (4,158,431 ds/min), 33,040,819 states left on queue.
Progress(25) at 2021-06-10 20:26:09: 6,905,574,897 states generated (54,166,375 s/min), 490,865,938 distinct states found (3,636,662 ds/min), 32,453,570 states left on queue.
Progress(25) at 2021-06-10 20:27:09: 6,959,280,862 states generated (53,705,965 s/min), 494,448,915 distinct states found (3,582,977 ds/min), 32,091,649 states left on queue.
Progress(25) at 2021-06-10 20:28:09: 7,014,473,164 states generated (55,192,302 s/min), 498,400,584 distinct states found (3,951,669 ds/min), 32,266,775 states left on queue.
Progress(25) at 2021-06-10 20:29:09: 7,070,091,210 states generated (55,618,046 s/min), 503,081,534 distinct states found (4,680,950 ds/min), 32,774,375 states left on queue.
Progress(25) at 2021-06-10 20:30:09: 7,125,257,636 states generated (55,166,426 s/min), 507,493,886 distinct states found (4,412,352 ds/min), 33,169,986 states left on queue.
Progress(25) at 2021-06-10 20:31:09: 7,180,327,280 states generated (55,069,644 s/min), 511,631,444 distinct states found (4,137,558 ds/min), 33,274,785 states left on queue.
Progress(26) at 2021-06-10 20:32:09: 7,235,955,029 states generated (55,627,749 s/min), 515,200,764 distinct states found (3,569,320 ds/min), 33,118,881 states left on queue.
Progress(26) at 2021-06-10 20:33:09: 7,291,502,982 states generated (55,547,953 s/min), 519,355,244 distinct states found (4,154,480 ds/min), 33,044,529 states left on queue.
Progress(26) at 2021-06-10 20:34:09: 7,345,974,457 states generated (54,471,475 s/min), 523,209,157 distinct states found (3,853,913 ds/min), 32,622,280 states left on queue.
Progress(26) at 2021-06-10 20:35:09: 7,399,764,658 states generated (53,790,201 s/min), 526,907,511 distinct states found (3,698,354 ds/min), 32,364,135 states left on queue.
Progress(26) at 2021-06-10 20:36:09: 7,455,486,291 states generated (55,721,633 s/min), 530,892,850 distinct states found (3,985,339 ds/min), 32,551,613 states left on queue.
Progress(26) at 2021-06-10 20:37:09: 7,511,010,571 states generated (55,524,280 s/min), 535,518,429 distinct states found (4,625,579 ds/min), 32,973,392 states left on queue.
Progress(26) at 2021-06-10 20:38:09: 7,566,255,095 states generated (55,244,524 s/min), 540,088,413 distinct states found (4,569,984 ds/min), 33,469,486 states left on queue.
Progress(26) at 2021-06-10 20:39:09: 7,621,339,194 states generated (55,084,099 s/min), 544,430,636 distinct states found (4,342,223 ds/min), 33,656,255 states left on queue.
Progress(27) at 2021-06-10 20:40:09: 7,676,803,321 states generated (55,464,127 s/min), 548,023,662 distinct states found (3,593,026 ds/min), 33,638,005 states left on queue.

Apalache N = 5

(main)$ apalache-mc check --inv=InvA --config=MCEWD998.cfg APEWD998
# Tool home: /home/mkuppe/ewd998/tools/apalache
# Package:   /home/mkuppe/ewd998/tools/apalache/mod-distribution/target/apalache-pkg-0.15.6-full.jar
# JVM args:  -Xmx4096m -DTLA-Library=/home/mkuppe/ewd998/tools/apalache/src/tla
#
# APALACHE version 0.15.6 build 1679f94
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]
# 
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Checker options: filename=APEWD998, init=, next=, inv=InvA        I@14:47:11.428
Tuning:                                                           I@14:47:11.909
PASS #0: SanyParser                                               I@14:47:11.910
Parsing file /home/mkuppe/ewd998/APEWD998.tla
Parsing file /home/mkuppe/ewd998/EWD998.tla
Parsing file /tmp/Integers.tla
Parsing file /tmp/Naturals.tla
Parsing file /home/mkuppe/ewd998/AsyncTerminationDetection.tla
Substitution of LEADS_TO needs care. The current implementation may fail to work. W@14:47:12.466
Substitution of ENABLED needs care. The current implementation may fail to work. W@14:47:12.470
Substitution of ENABLED needs care. The current implementation may fail to work. W@14:47:12.480
Substitution of LEADS_TO needs care. The current implementation may fail to work. W@14:47:12.536
Substitution of LEADS_TO needs care. The current implementation may fail to work. W@14:47:12.537
Substitution of ENABLED needs care. The current implementation may fail to work. W@14:47:12.561
Substitution of ENABLED needs care. The current implementation may fail to work. W@14:47:12.561
Substitution of ENABLED needs care. The current implementation may fail to work. W@14:47:12.582
Substitution of ENABLED needs care. The current implementation may fail to work. W@14:47:12.582
PASS #1: TypeCheckerSnowcat                                       I@14:47:12.993
 > Running Snowcat .::.                                           I@14:47:12.993
 > Your types are great!                                          I@14:47:13.494
 > All expressions are typed                                      I@14:47:13.494
PASS #2: ConfigurationPass                                        I@14:47:13.599
  > MCEWD998.cfg: Loading TLC configuration                       I@14:47:13.602
Fairness constraints are ignored by Apalache: WF_vars()(System()) W@14:47:13.653
  > MCEWD998.cfg: Using SPECIFICATION Spec                        I@14:47:13.654
  > Using the init predicate Init from the TLC config             I@14:47:13.654
  > Using the next predicate Next from the TLC config             I@14:47:13.654
  > MCEWD998.cfg: found INVARIANTS: TypeOK, Inv                   I@14:47:13.654
  > Overriding with command line arguments: --inv InvA            W@14:47:13.654
  > MCEWD998.cfg: PROPERTY ATDSpec is ignored. Only INVARIANTS are supported. W@14:47:13.655
  > Set the initialization predicate to Init                      I@14:47:13.656
  > Set the transition predicate to Next                          I@14:47:13.656
  > Set an invariant to InvA                                      I@14:47:13.657
  > Set a temporal property to ATDSpec                            I@14:47:13.657
  > Replaced CONSTANT N with 5                                    I@14:47:13.660
PASS #3: DesugarerPass                                            I@14:47:13.747
  > Desugaring...                                                 I@14:47:13.747
PASS #4: UnrollPass                                               I@14:47:13.842
  > Unroller                                                      I@14:47:13.871
PASS #5: PrimingPass                                              I@14:47:13.936
  > Introducing InitPrimed for Init'                              I@14:47:13.940
PASS #6: CoverAnalysisPass                                        I@14:47:13.996
PASS #7: InlinePass                                               I@14:47:13.996
  > InlinerOfUserOper                                             I@14:47:13.997
  > LetInExpander                                                 I@14:47:14.024
  > InlinerOfUserOper                                             I@14:47:14.032
Leaving only relevant operators: ATDSpec, CInitPrimed, Init, InitPrimed, InvA, Next I@14:47:14.036
PASS #8: VCGen                                                    I@14:47:14.096
  > Producing verification conditions from the invariant InvA     I@14:47:14.096
  > VCGen produced 2 verification condition(s)                    I@14:47:14.104
PASS #9: PreprocessingPass                                        I@14:47:14.164
  > Before preprocessing: unique renaming                         I@14:47:14.164
 > Applying standard transformations:                             I@14:47:14.171
  > PrimePropagation                                              I@14:47:14.171
  > Desugarer                                                     I@14:47:14.234
  > UniqueRenamer                                                 I@14:47:14.301
  > Normalizer                                                    I@14:47:14.374
  > Keramelizer                                                   I@14:47:14.443
  > After preprocessing: UniqueRenamer                            I@14:47:14.518
PASS #10: TransitionFinderPass                                    I@14:47:14.587
  > Found 1 initializing transitions                              I@14:47:14.606
  > Found 5 transitions                                           I@14:47:14.626
  > No constant initializer                                       I@14:47:14.626
  > Applying unique renaming                                      I@14:47:14.627
PASS #11: OptimizationPass                                        I@14:47:14.667
 > Applying optimizations:                                        I@14:47:14.671
  > ConstSimplifier                                               I@14:47:14.672
  > ExprOptimizer                                                 I@14:47:14.681
  > ConstSimplifier                                               I@14:47:14.688
PASS #12: AnalysisPass                                            I@14:47:14.732
 > Marking skolemizable existentials and sets to be expanded...   I@14:47:14.734
  > SkolemizationMarker                                           I@14:47:14.734
  > ExpansionMarker                                               I@14:47:14.735
 > Running analyzers...                                           I@14:47:14.741
  > Introduced expression grades                                  I@14:47:14.784
  > Introduced 4 formula hints                                    I@14:47:14.785
PASS #13: PostTypeCheckerSnowcat                                  I@14:47:14.785
 > Running Snowcat .::.                                           I@14:47:14.785
 > Your types are great!                                          I@14:47:15.140
 > All expressions are typed                                      I@14:47:15.141
PASS #14: BoundedChecker                                          I@14:47:15.191
State 0: Checking 2 state invariants                              I@14:47:15.523
Step 0: picking a transition out of 1 transition(s)               I@14:47:15.731
State 1: Checking 1 state invariants                              I@14:47:15.746
Step 1: Transition #1 is disabled                                 I@14:47:15.857
State 1: Checking 1 state invariants                              I@14:47:15.869
Step 1: Transition #3 is disabled                                 I@14:47:15.974
State 1: Checking 2 state invariants                              I@14:47:15.991
Step 1: picking a transition out of 3 transition(s)               I@14:47:16.153
State 2: Checking 1 state invariants                              I@14:47:16.189
State 2: Checking 1 state invariants                              I@14:47:16.297
State 2: Checking 1 state invariants                              I@14:47:16.403
State 2: Checking 2 state invariants                              I@14:47:16.514
State 2: Checking 2 state invariants                              I@14:47:16.685
Step 2: picking a transition out of 5 transition(s)               I@14:47:17.091
State 3: Checking 1 state invariants                              I@14:47:17.130
State 3: Checking 1 state invariants                              I@14:47:17.207
State 3: Checking 1 state invariants                              I@14:47:17.323
State 3: Checking 2 state invariants                              I@14:47:17.428
State 3: Checking 2 state invariants                              I@14:47:18.413
Step 3: picking a transition out of 5 transition(s)               I@14:47:25.998
State 4: Checking 1 state invariants                              I@14:47:26.046
State 4: Checking 1 state invariants                              I@14:47:26.159
State 4: Checking 1 state invariants                              I@14:47:26.384
State 4: Checking 2 state invariants                              I@14:47:26.550
State 4: Checking 2 state invariants                              I@14:48:37.613
Step 4: picking a transition out of 5 transition(s)               I@15:06:37.928
State 5: Checking 1 state invariants                              I@15:06:37.988
State 5: Checking 1 state invariants                              I@15:06:38.088
State 5: Checking 1 state invariants                              I@15:06:38.925
State 5: Checking 2 state invariants                              I@15:06:39.445
State 5: Checking 2 state invariants                              I@17:16:11.600
^CPremature termination requested. Killing apalache-mc (pid 9054)
(main)$ date
Thu 10 Jun 2021 09:03:44 PM PDT

Agenda/Outline

Part A

Basics
Actions
Invariants
Implication
Implied Init & Box/Always
[A]_v
Temporal Formual: Spec
ENABLED
<<A>>_v
Diamond/Eventually (liveness)
Stuttering
<>[] and []<>
Fairness
Weak Fairness
Leads-to

Basics ..v02b09

CONSTANT, VARIABLES, definitions
set-theory refresher
Initial predicates and actions
Functions (arrays), boolean connectives (lists), unchanged and prime
Predicate logic/FOL - Quantification and non-determinism
deadlocks, state-space explosion, and small-model hypothesis
Specs vs. model-checking (MCInit)

TLA

First invariant TypeOK ..v02b10

Find bug in Wakeup action: @-2
Variable terminationDetected , priming operators

Property Stable (Implication, Implied Inits and Box) ..v02b13

Introduce Implication
P: Rewrite terminated to FALSE and check with TLC to show vacuously true formulas (pitfall)
P: Revert to original terminated and show that it holds
V: Add FALSE to MCInit and show that it doesn't actually hold because the current formula is just an Implied Init
Verification doesn't find the bug unless the faulty state is an initial state
This is why we need the box operator to say that Stable holds in every state of a behavior; not just the initial states

Property Stable (Box to Box Box) ..v02b18

V: [](t => td)
- violated by a behavior of two states (this is an invariant and checked as such)
V: [](t => []td)
- we strengthen Stable to turn the invariant into a property to show that TLC checks it differently and hint at "stuttering"
Have we found flaw?
P: [](td => []t
- No, reverse td and t , which is what we actually meant

Be suspicious of success aka non-properties, and Spec ..v02b20

Run simulation mode to find bogus action constraint (Always be suspicious of success)
Property OnlyTerminates (subscript of [N]_v <=> N \/ v'=v)
- Every step is a Termiation step
These commits bridge to Spec by adding the disjunct of all actions
Once we arrive at Init /\ [][Next]_vars, we will revisit the implied inits and why it is useful

ENABLED ..v02b30

P: []ENABLED Next
- because DetectTermination is permanently enabled and allows vars to remain unchanged)
V: []ENABLED Next
- Violation after enablement of DetectTermination is changed
P: []ENABLED [Next]_v
- This is a tautology
V: []ENABLED <<Next>>_vars
- Violated even with UNCHANGED vars because vars don't change anymore which is stipulated by "Angle A sub variables"
- This property is violated even with the original definition of DetectTermination that allowed infinite stuttering.

Diamond operator <>, fairness, and machine closure (prophecy) ..v02b35

V: <>terminationDetected and <>terminated
- both violated because of lack of fairness
- Talk about comibining <> and [] into []<> and <>[] to grok (weak fairness below)
P: F == <>t /\ <>td
- Turn both properties into fairness properties (not machine closed)
V: <>[](ENABLED <<Next>>_vars) => []<><<Next>>_vars
- because fairness is on Next causing a lasso between Send and Wakeup
V: WF_vars(Next)
- just syntactic sugar for previous property. The liveness properties are too strong, because we want to allow infinite computations, no?

Leads-to ..v02b37

P: [](terminated => <>terminationDetected
P: terminated ~> terminationDetected
- just syntactic sugar

Inductive invariant ..v02e03

Validate TypeOK with Apalache
Prove TypeOK
Validate Stable with Apalache
Prove Stable

Part B

Simulate real modeling

Records ..v03a08

IF-THEN-ELSE ..v03a10

CHOOSE ..v03a14

Refinement ..v03b10

CHOOSE again! ..v03c04

Meet the TLA+ debugger

Safra's inductive invariant ..03d02

Recursion functions vs. operators and folds (community modules) ..v03d05

Part C

Validating inductive invariants (again) ..v03d07

Sketch a real Prove ..v03d08

Proof of refinement of ATD => STD (which is implemented by EWD480) ..v03e01

Refinement proof EWD998 => AsyncTerminationDetection (inspired by https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840_proof.tla)

Part D

Multiple nodes terminate simultaneously ..v04a02

Part E

Shiviz/ICG (trace expressions)

EWD998 in Shiviz (Upstream PR at DistributedClocks/shiviz#169)
EWD998ChanID_export
Screencast EWD840 Json
(EWD840_json.tla)

Channels

Singleton
refinement can
- deconstruct variables (token changed from a (record) variable to a message kept in an inbox variable)
- drop state (payload messages)
Seq in [Node -> Seq(Message)]

Executing spec with PlusPy & TLC

TLA+ statistics with EWD840

Description

The goal of this workshop/tutorial is to show developers of concurrent and distributed systems how to model algorithms with TLA+. Inspired by Safra's EWD998, we will design and verify a termination detection algorithm. The focus is on applying TLA+ rather than the TLA+ language itself. In other words, the workshop will follow Lamport's video course style and introduce TLA+ as we go. At the end of the workshop, attendees will have written a specification of EWD998, checked safety and liveness properties, stated fairness constraints, and encountered refinement.

This is a hands-on, interactive workshop for programmers who wish to get familiar with TLA+. The format of the workshop will be similar to https://youtu.be/wjsI0lTSjIo, enriched with hands-on exercises. Familiarity with logic is not a prerequisite (if you've been using Coq, Isabelle, Lean, ..., this workshop is likely not for you).

Setup instructions

Dear TLA+ enthusiast,

welcome to the TLA+ in Action workshop. The workshop's material is already available online at https://github.com/lemmy/ewd998 (please consider starring the repository).

For the workshop to run smoothly, we are going to use a browser-based TLA+ IDE. Before starting on Wednesday, please open https://gitpod.io/#https://github.com/lemmy/ewd998 and go through the Gitpod login process with your Github account (Gitlab and Bitbucket won't work). Afterward, you will be greeted by the TLA+ IDE with the workshop material open.

See you on Wednesday,
Markus Kuppe

Background participants Hydra

Please report issues at https://github.com/tlaplus-workshops/ewd998

https://github.com/tlaplus-workshops/ewd998

Recommend Projects

React

A declarative, efficient, and flexible JavaScript library for building user interfaces.
Vue.js

🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
Typescript

TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
TensorFlow

An Open Source Machine Learning Framework for Everyone
Django

The Web framework for perfectionists with deadlines.
Laravel

A PHP framework for web artisans
D3

Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

javascript

JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
web

Some thing interesting about web. New door for the world.
server

A server is a program made to process requests and deliver data to clients.
Machine learning

Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Visualization

Some thing interesting about visualization, use data art
Game

Some thing interesting about game, make everyone happy.

Recommend Org

Facebook

We are working to build community through open source technology. NB: members must have two-factor auth.
Microsoft

Open source projects and samples from Microsoft.
Google

Google ❤️ Open Source for everyone.
Alibaba

Alibaba Open Source for everyone
D3

Data-Driven Documents codes.
Tencent

China tencent open source team.