MODULE main
    -- Model of the switch
    IVAR
        press   : boolean;
    VAR
        mode    : {on, off};
        x       : 0..15;
    ASSIGN
        init(mode) := off;
        next(mode) := case
            mode = off & press              : on;
            mode = on & (press | x >= 10)   : off;
            TRUE                            : mode;
        esac;
        init(x) := 0;
        next(x) := case
            mode = on & next(mode) = off    : 0;
            mode = on & x < 10              : x + 1;
            TRUE                            : x;
        esac;
        
INVARSPEC x <= 10;
INVARSPEC mode = off -> x = 0;
INVARSPEC x < 10;
INVARSPEC mode = off;