This is super cool! As someone who is interested but unfamiliar with formal verification, how "powerful" or "complete" would you say FizzBee is compared to the conventional tools such as TLA+? I'm unsure if I framed this correctly but can you do everything in Fizzbee that TLA+ supports?
Yes, that's the intended goal. To do everything tla+ does (behavioral modeling) but not stop there.
The second biggest area that's missing in tla+ but indispensable is performance modeling that will be integrated. (PRISM model checker does it, but with a unwieldy complex language not suitable for more than a few dozen states)
The performance modeling is work in progress, you can still try it, but you need to download and use the command line tool at present.
The third goal is to make it suitable as a design documentation tool. I haven't started, but I would love to share the plan to get early feedback.
Comments
This is super cool! As someone who is interested but unfamiliar with formal verification, how "powerful" or "complete" would you say FizzBee is compared to the conventional tools such as TLA+? I'm unsure if I framed this correctly but can you do everything in Fizzbee that TLA+ supports?
Yes, that's the intended goal. To do everything tla+ does (behavioral modeling) but not stop there. The second biggest area that's missing in tla+ but indispensable is performance modeling that will be integrated. (PRISM model checker does it, but with a unwieldy complex language not suitable for more than a few dozen states) The performance modeling is work in progress, you can still try it, but you need to download and use the command line tool at present.
The third goal is to make it suitable as a design documentation tool. I haven't started, but I would love to share the plan to get early feedback.