missing config

[joewilliams]

Can you include the TLA+ config you use in this repo?

[ongardie]

I've forgotten what that even means, to be honest. The spec isn't meant to be run in any way.

I have an old config file around there, though it looks like most everything is commented out.

CONSTANTS Server = {r1,r2,r3}
          Value = {v1,v2}
          Follower = Follower
          Candidate = Candidate
          Leader = Leader
          Nil = Nil
          RequestVoteRequest = RequestVoteRequest
          RequestVoteResponse = RequestVoteResponse
          AppendEntriesRequest = AppendEntriesRequest
          AppendEntriesResponse = AppendEntriesResponse
          TLC_MAX_TERM = 3
          TLC_MAX_ENTRY = 1
          TLC_MAX_MESSAGE = 1
\*          PNat = {1,2,3,4,5}
\*          Nat = {0,1,2,3,4,5}
\*SYMMETRY Perms
SPECIFICATION Spec
\*CONSTRAINT TermConstraint
\*CONSTRAINT LogConstraint
\*CONSTRAINT MessageConstraint
\*INVARIANT AtMostOneLeaderPerTerm
\*INVARIANT TermAndIndexDeterminesLogPrefix
\*INVARIANT StateMachineSafety
\*INVARIANT NewLeaderHasCompleteLog
\*INVARIANT CommitInOrder

\*INVARIANT MessageTypeInv
\*INVARIANT TypeInv

[joewilliams]

Cool, thanks that looks right.

[ongardie]

I could seriously use a reminder here, is the config file something you need for TLC, or do other tools need it?

[joewilliams]

@ongardie oh sorry, yes, TLC needs a config otherwise it doesn't know what the CONSTANTS are in the model.

[ongardie]

@joewilliams gotcha, yeah. You'll probably need to tweak the spec before you're able to run with TLC again. I found that if things got too mathy (\exists, for example), they'd slow down TLC severely.

[deardeng]

hi, I use this, but it used 567G disk capacity, and finally exhausted the disk and stopped, and it didn't finish.

ongardie

[ukd1]

@ongardie I know you said in another PR you're not working on this anymore, but linking to this and or putting the config in the repo itself would save a ton of time figuring out how to run the model. Would you accept a PR for this?

Also, do you recalll how long the model took to run with this config? @overhacked and I are working on (for fun) a implemenation, and want to make a change, but verify it using TLA+ if possible.

[ongardie]

@ukd1 if you get a config file to run and submit a PR, I'd be happy to merge it. I just don't want to make non-trivial changes to the core spec at this point.

[ongardie]

Also, do you recalll how long the model took to run with this config?

No, and I think that's the issue. I think the spec probably needs changes to be practically runnable. @deardeng reported running out of space above, for example.

[ongardie]

I've reopened this issue so it's a little more discoverable.