Sequential logic is generally easier to test (also concurrency testing of linearizable systems). FizzBee specification language is created primarily to express concurrent behavior of non-linearizable systems - like eventual consistency, etc.
Glad you have tried FizzBee before. Do you have any feedback on it?
With TLA+, I mostly see papers and example projects that typically implement model based trace checking solutions in TLA+.
While it works, usually, it will clutter the main code (SUT) with tracing library calls. And in some papers, you'll need to create a separate modified version of spec with the tracing spec.
MongoDB published a paper a while ago comparing model based testing and model based trace checking.
I'll soon list more details.
One issue with the current proponents of formal methods is, they want to claim others who don't use formal methods as "lazy" or "dumb" and want to claim their superiority because they "do the right thing" and "mastered a complex language".
Some of them (not all, I know a few good ones) are, actually one trick pony. For example, ask them about other formal methods systems they learnt or tried in the recent years, they would claim they are "too busy" to learn anything new.
Recent easier to use formal methods:
1. FizzBee (Uses Python dialect, almost reads like pseudo code)
2. Quint: Another formal language with easier to use syntax
3. P: Use syntax similar to C# users.
The author of the posted article himself posted another article that Formal methods solves only half his problems (https://brooker.co.za/blog/2022/06/02/formal.html)
But the problem he mentioned is actually solved by PRISM (It is not new). But Brooker just won'd bother to look around or learn.
Formal methods don't have to be complex. The issue is, most formal methods are designed as an academic exercise to demonstrate a specific topic the professor was interested in. (Or TLA+, that was designed specifically for writing papers)
*Tools like draw.io, Lucidchart, and Excalidraw excel at creating raw diagrams through drag-and-drop interfaces. However, they often become cumbersome when updates are needed, and their outputs are rarely stored in source control, making versioning and collaboration more difficult. While these tools give you full control over the layout and appearance of the diagrams, they require manual effort each time you make changes.
*Mermaid.js, websequencediagrams, and PlantUML, on the other hand, allow you to generate diagrams from a text description. FizzBee builds on this concept by generating these text descriptions directly from your algorithm specification, then leveraging mermaid.js to render sequence diagrams and Graphviz for other diagram types.
*Where FizzBee truly shines is in its ability to automatically generate diagrams for every significant scenario your system might encounter, not just a single use case. For example, with a two-phase commit protocol:
- The 'happy path' where all participants and the coordinator agree to commit, and everything proceeds smoothly.
- A case where the first participant prepares, but the second one aborts.
- Scenarios where both participants prepare but some messages get dropped.
- A situation where both participants prepare, but the coordinator crashes and restarts—how does the system recover?
These are just a few examples. The ability to generate these scenarios automatically means FizzBee pays for itself very quickly compared to manually drawing sequence diagrams for each possible case.
This is in addition to verifying for correctness or clearer communication benefits.
TLA+ is 25 years old. Despite the power it's syntax is too alien to become mainstream.
Have you considered https://FizzBee.io?
Almost Python-like syntax, has more powerful semantics, beautiful visualizations with no extra work, only formal methods system that can do performance analysis.
Putin signed a decree that Russia would welcome foreigners wanting to escape Western liberal ideals.
Applicants may include those from countries unaligned with "Russian spiritual and moral values."
The application process has been simplified, and visas may be issued as soon as next month.
https://fizzbee.io/testing/tutorials/quick-start/#parallel-t...
Sequential logic is generally easier to test (also concurrency testing of linearizable systems). FizzBee specification language is created primarily to express concurrent behavior of non-linearizable systems - like eventual consistency, etc.