4 ms·
couldn't figure out how to run https://github.com/ongardie/raft.tla https://github.com/ongardie/raft.tla
by awinter-py 9y ago
couldn't figure out how to run https://github.com/ongardie/raft.tla https://github.com/ongardie/raft.tla
- pron 9y agoWhat do you mean by "run"? Check in the TLC model checker? You need to first write a configuration that you want to check. Lamport's Specifying Systems has full documentation for using the model checker from the command line. But if you're a beginner, you might be better off using the IDE, at least at first, as it helps you write a configuration very easily. Also, I would recommend starting with a simpler specification (there are lots of examples available). Otherwise, the checker would just work for a while and spit out "OK", and won't mean much to you.
- hwayne 9y agoI wrote a step-by-step tutorial to using the IDE. Hope it helps! https://learntla.com/pluscal/toolbox/ https://learntla.com/pluscal/toolbox/