MACHINE basic_machine
SEES
    basic_ctx
VARIABLES
    current_value
INVARIANTS
    @inv1 current_value >= min_value
    @inv2 current_value <= max_value
EVENTS
    EVENT INITIALISATION
    THEN
        current_value := default_value
    END

    EVENT increase
    WHERE
        @grd1 current_value < max_value
    THEN
        current_value := current_value + 1
    END

    EVENT decrease
    WHERE
        @grd1 current_value > min_value
    THEN
        current_value := current_value - 1
    END

    EVENT reset
    THEN
        current_value := default_value
    END
END
