speck ConditionalToggle {

    state {
        isOn: Bool
        count: Nat
    }

    init {
        isOn == false
        count == 0
    }

    invariant SwitchConsistent {
        isOn in {true, false}
    }

    action Toggle {
        require true
        if (isOn) {
            isOn := false
        } else {
            isOn := true
        }
        count := count + 1
        return isOn
    }

    next: Toggle
}