| [package] | |
| name = "sighandler-study" | |
| version = "0.1.0" | |
| edition = "2021" | |
| # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html | |
| [dependencies] | |
| signal-hook = "0.3.14" | |
| libc = "0.2.126" |
| INIT Init | |
| NEXT Next | |
| CONSTANTS | |
| NULL = NULL | |
| Partitions = {1,2,3} | |
| MaxPendingRecords = 2 | |
| INVARIANTS | |
| NoRecordsAddedMoreThanMaxPendingRecords |
data field in lima.yamllimactl startsudo fdisk /dev/vdbsudo mkfs -t xfs /dev/vdb1sudo xfs_admin -L data /dev/vdb1Changes:
| INIT Init | |
| NEXT Next | |
| INVARIANT NotSolved |
| % This is the excerpt from plain TeX format | |
| % that contains minimal instructions to just print "Hello \TeX". | |
| % catcode definitions | |
| \catcode`\{=1 % left brace is begin-group character | |
| \catcode`\}=2 % right brace is end-group character | |
| \catcode`\$=3 % dollar sign is math shift | |
| \catcode`\&=4 % ampersand is alignment tab | |
| \catcode`\#=6 % hash mark is macro parameter character | |
| \catcode`\^=7 \catcode`\^^K=7 % circumflex and uparrow are for superscripts |
| ---- MODULE BatchingProcessor ---- | |
| EXTENDS Sequences, Integers | |
| CONSTANT BatchSize | |
| (*--algorithm BatchingProcessor | |
| variables | |
| batch = <<>>; | |
| flushTasks = <<>>; | |
| flushedBatchSizeHistory = {}; |
| ----------------------------- MODULE PaxosCommit ---------------------------- | |
| (***************************************************************************) | |
| (* This specification is discussed in "Paxos Commit", Lecture 6 of the *) | |
| (* TLA+ Video Course. *) | |
| (* *) | |
| (* This module specifies the Paxos Commit algorithm. We specify only *) | |
| (* safety properties, not liveness properties. We simplify the *) | |
| (* specification in the following ways. *) | |
| (* *) | |
| (* - As in the specification of module TwoPhase, and for the same *) |
$ for i in `zcat numbers.txt.gz`; do redis-cli PFADD foo $i > /dev/null; done
$ redis-cli PFCOUNT foo
(integer) 1