isaac-defrain / tlaplusfun

TLA+ questions, answers, and experiments

TLA+ (Temporal Logic of Actions)

These specs are inspired by questions that have come up in the TLA+ email group, exercises in the tutorial, strange situations I have personally encountered while using TLA+ and related tools, or things I generally find interesting.

I hope you enjoy :)

tlaplusfun's Issues

GreenLeftOfWhite in Einstein Riddle seems wrong

I think it should be

GreenLeftOfWhite == \E i \in 1..4 : colors[i] = "green" /\ colors[i+1] = “white"

PeerDiscovery liveness violation with four nodes

TLC2 Version 2.18 of Day Month 20?? (rev: 95d980c)
Running breadth-first search Model-Checking with fp 117 and seed 5082471029450774076 with 1 worker on 10 cores with 7282MB heap and 64MB offheap memory [pid: 67426] (Mac OS X 12.3.1 aarch64, Homebrew 18.0.1 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /Users/markus/src/TLA/_specs/TLAplusFun/PeerDiscovery/MC.tla
Parsing file /Users/markus/src/TLA/_specs/TLAplusFun/PeerDiscovery/PeerDiscovery.tla
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-6677445440072312092/TLC.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-6677445440072312092/FiniteSets.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-6677445440072312092/Naturals.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /private/var/folders/7d/4x6z2cc91jl588ysynlc1tfc0000gn/T/tlc-6677445440072312092/Sequences.tla (jar:file:/Applications/TLA+%20Toolbox.app/Contents/Eclipse/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module PeerDiscovery
Semantic processing of module TLC
Semantic processing of module MC
Starting... (2022-05-09 08:59:24)
Implied-temporal checking--satisfiability problem has 2 branches.
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2022-05-09 08:59:24.
Progress(5) at 2022-05-09 08:59:24: 6,501 states generated, 625 distinct states found, 0 states left on queue.
Checking 2 branches of temporal properties for the complete state space with 1250 total distinct states at (2022-05-09 08:59:24)
Error: Temporal properties were violated.

Error: The following behavior constitutes a counter-example:

State 1: <Initial predicate>
/\ dns_request_enabled = <<TRUE, TRUE, TRUE, TRUE>>
/\ peers = <<{}, {}, {}, {}>>

State 2: <Request_DNS line 28, col 5 to line 29, col 21 of module PeerDiscovery>
/\ dns_request_enabled = <<TRUE, TRUE, FALSE, TRUE>>
/\ peers = <<{}, {}, {1, 4}, {}>>

State 3: <Request_DNS line 28, col 5 to line 29, col 21 of module PeerDiscovery>
/\ dns_request_enabled = <<TRUE, FALSE, FALSE, TRUE>>
/\ peers = <<{}, {1, 3, 4}, {1, 4}, {}>>

State 4: <Request_DNS line 28, col 5 to line 29, col 21 of module PeerDiscovery>
/\ dns_request_enabled = <<TRUE, FALSE, FALSE, FALSE>>
/\ peers = <<{}, {1, 3, 4}, {1, 4}, {1, 3}>>

State 5: <Request_DNS line 28, col 5 to line 29, col 21 of module PeerDiscovery>
/\ dns_request_enabled = <<FALSE, FALSE, FALSE, FALSE>>
/\ peers = <<{3, 4}, {1, 3, 4}, {1, 4}, {1, 3}>>

State 6: Stuttering
Finished checking temporal properties in 00s at 2022-05-09 08:59:24
6501 states generated, 625 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 5.
Finished in 00s at (2022-05-09 08:59:24)
Trace exploration spec path: ./MC_TTrace_1652111963.tla

ExternalSeqRecordParser model and ExternalRecordParser model run error，why？

Hello，I am using TLA+ to implement trace verification, and found that you have provided two interfaces ExternalSeqRecordParser and ExternalRecordParser, but I am running these two interfaces and report an error, what is the reason for this, and I look forward to your reply.

ExternalRecordParser
connect.log
a : 42, b : true
a : -1, b : false
a : 0, b : true

ExternalRecordParser
connect.log
a : 42
b : true

Contribute External*Parser to CommunityModules

Hi, we recently added generic (de-)serialization to the IOUtils module of the CommunityModules (tlaplus/CommunityModules#53). Perhaps, you want to contribute your parser to the CommunityModules, too?