4 ms·

So can it spit out C or something? Or something to actually perform the algorithm? Or are you expected to manually translate back and forth between your model s

• Jtsummers 4y ago
  It does not spit out C. TLA+ is aimed at the design/specification level, not the implementation level. You would have to take the information learned from the model checker or proof system (or even just the act of constructing the model can reveal problems) and change your program to address any discovered issues.
• philix001 4y ago
  The spec might not even contain the level of detail necessary for that to be possible. That possibility is what makes modeling easier than implementing the spec. Through a process of manual refinement, you can derive an implementation from the spec and check every step with the checker, but that's is more work than implementing the formal spec manually and is an most likely an overkill in practice.
• mhh__ 4y ago
  In practice it's fuzzy but TLA+ is meant for checking your thinking not your code as per se