Comments (10)
@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.
from raft.tla.
I've reopened this issue so it's a little more discoverable.
from raft.tla.
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
from raft.tla.
Cool, thanks that looks right.
from raft.tla.
I could seriously use a reminder here, is the config file something you need for TLC, or do other tools need it?
from raft.tla.
@ongardie oh sorry, yes, TLC needs a config otherwise it doesn't know what the CONSTANTS are in the model.
from raft.tla.
@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.
from raft.tla.
hi, I use this, but it used 567G disk capacity, and finally exhausted the disk and stopped, and it didn't finish.
ongardie
from raft.tla.
@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.
from raft.tla.
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.
from raft.tla.
Related Issues (7)
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.
from raft.tla.