5 ms·

I'm unable to see the difference between this and TLA. Is it "merely" (*) an alternate syntax? What is the value-add to TLA or PlusCal? For example, fizzbee (h

I'm unable to see the difference between this and TLA. Is it "merely" (*) an alternate syntax? What is the value-add to TLA or PlusCal? For example, fizzbee (https://fizzbee.io https://fizzbee.io) offers python syntax and data structures, which makes it very intuitive. (*) No snark intended; a good syntax can give you joy.

lou1306 2y ago
Indeed it seems that the verification relies on Apalache, which is an alternate (symbolic) model checker for TLA. TLA (well, TLA+) gives access to a richer specification language, as it allows e.g., to express liveness properties (informally defined as "something good happens at some point") as opposed to just safety ("nothing bad ever happens"). But the model checker does not use symbolic techniques so it may suffer on larger systems. Personally I also find Quint to be way more readable/intuitive but your mileage may vary.
- sriram_malhar 2y ago
  Thanks. More readable/intuitive is always welcome. I'll give it a try.
bugarela 2y ago
Two main things: alternative syntax and tooling Some things that a programmer would take for granted are not available in TLA+ tooling, but are for Quint. The biggest examples: syntax and type checking in the IDE as you type, standard CLI with standard error reporting, LSP (Language Server Protocol) support (so you can use "Go To Definition" in your IDE). In addition to that, Quint has a way to define tests (runs) and it makes it so it's easy to execute a specification, which is not normally possible in a natural way. TLA+ has more advanced mathematical expressions that are not supported in Quint. This is on purpose. There are many things you can write in TLA+ but not in Quint, but those are the things that most people would only write by accident and be extremely confused by the results. The people who would write those knowing what they mean will probably like the Mathy syntax of TLA+ much better than Quint, so they should just use TLA+.
- sriram_malhar 2y ago
  Thank you for your explanation.
jayaprabhakar 2y ago
https://FizzBee.io https://FizzBee.io is not just a syntax transpiler, but a complete implementation. It uses starlark language (a Python variant) for specification. In addition to behavioral modeling like TLA+, Quint etc, it supports probabilistic and performance modeling. Generates state and sequence diagrams automatically.

lou1306 2y ago

Indeed it seems that the verification relies on Apalache, which is an alternate (symbolic) model checker for TLA. TLA (well, TLA+) gives access to a richer specification language, as it allows e.g., to express liveness properties (informally defined as "something good happens at some point") as opposed to just safety ("nothing bad ever happens"). But the model checker does not use symbolic techniques so it may suffer on larger systems. Personally I also find Quint to be way more readable/intuitive but your mileage may vary.

sriram_malhar 2y ago
Thanks. More readable/intuitive is always welcome. I'll give it a try.

bugarela 2y ago

Two main things: alternative syntax and tooling Some things that a programmer would take for granted are not available in TLA+ tooling, but are for Quint. The biggest examples: syntax and type checking in the IDE as you type, standard CLI with standard error reporting, LSP (Language Server Protocol) support (so you can use "Go To Definition" in your IDE). In addition to that, Quint has a way to define tests (runs) and it makes it so it's easy to execute a specification, which is not normally possible in a natural way. TLA+ has more advanced mathematical expressions that are not supported in Quint. This is on purpose. There are many things you can write in TLA+ but not in Quint, but those are the things that most people would only write by accident and be extremely confused by the results. The people who would write those knowing what they mean will probably like the Mathy syntax of TLA+ much better than Quint, so they should just use TLA+.

sriram_malhar 2y ago
Thank you for your explanation.

jayaprabhakar 2y ago

https://FizzBee.io https://FizzBee.io is not just a syntax transpiler, but a complete implementation. It uses starlark language (a Python variant) for specification. In addition to behavioral modeling like TLA+, Quint etc, it supports probabilistic and performance modeling. Generates state and sequence diagrams automatically.