// Description: a module with am input variable and a state variable. We assume the input variable and the state variable are 0 in the init block. We have one invariant that states that the input variable is always 0. We have another invariant that states that the state variable is always 0. The control block is a simple proof by induction.

module main {
    input inp: integer;
    var state: integer;

    init {
        assume (inp == 0);
        assume (state == 0);
    }

    invariant input_is_zero: (inp == 0);
    invariant state_is_zero: (state == 0);

    control {
        induction;
        check;
        print_results();
    }

}
