venice icon indicating copy to clipboard operation
venice copied to clipboard
verified publisher icon linkedin

[specs][doc] FizzBee spec for the Venice's LeaderFollower protocol

Open jayaprabhakar opened this issue 1 year ago • 2 comments

Summary, imperative, start upper case, don't end with a period

FizzBee spec for the Venice's LeaderFollower protocol, a one-to-one translation from the TLA+ syntax to the FizzBee syntax.

How was this PR tested?

Manually run it with the fizz model checker.

fizz specs/fizzbee/LeaderFollower/VeniceLeaderFollower.fizz

Does this PR introduce any user-facing changes?

  • [x] No. You can skip the rest of this section.
  • [ ] Yes. Make sure to explain your proposed changes and call out the behavior change.

jayaprabhakar avatar Apr 23 '24 16:04 jayaprabhakar

Looks great! Could I also trouble you to include a readme file with the PR for how to run the spec/install fizz?

ZacAttack avatar Apr 23 '24 18:04 ZacAttack

Sure. Added the README file pointing to the instructions at. https://github.com/fizzbee-io/fizzbee

At present, there is no precompiled binary, I have the full instructions to compile from source that I have tested in MacBook and Ubuntu on EC2.

jayaprabhakar avatar Apr 23 '24 18:04 jayaprabhakar

@FelixGV @ZacAttack I have made the changes you asked for in this commit: https://github.com/linkedin/venice/pull/958/commits/c721c5ee3de1b6e7c31663f9e5e89a1c35a7690b

Please take a look and let me know.

jayaprabhakar avatar May 20 '24 23:05 jayaprabhakar