# 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