# Fizzbee model checker

invariants:
always value <= 3 # This statement is always true
always eventually value == 0 # The value can be anything, but always come back to 0
eventually always value >= 0 # The value will reach 0 eventually, and stay >= 0


action Init:
value = -2


atomic fair action Add:
if value < 3:
value += 1
else:
value = 0


Output States Graph Error Graph Error Formatted Communication Diagram Explorer