Invariants over next states

[ekiwi]

Is there a way to include the next state of a signal in an invariant.

For example, let's say I want to prove termination of a system through the invariant that a counter is always decreasing. Trying to write an invariant like this gives me a syntax error:

invariant counter_decreases : counter < counter';

Is there a different way to express this?

[pramodsu]

One can't refer to the next state, but it is possible to refer to the previous state of the variable n using the expression past(n). This is more or less equivalent. Here a model similar in spirit to what you want to do:

module main
{
    var n : integer;
    var inited : boolean;

    init {
        assume (n > 0);
        inited = false;
    }
    
    next {
        n' = n - 1;
        inited' = true;
    }

    invariant n_decreases: inited ==> (n < past(n));

    control {
        v = unroll(10);
        check;
        v.print_results;
        // v.print_cex(n);
    }
}

Note we need the flag inited because past(v) is undefined in the initial state so it ends up taking unconstrained values.

Also past(v) is just an abbreviation for history(v, 1); history(v, n) returns the value of the variable v, n steps ago. n must be an integer literal. We don't allow history(v, n) where n is a variable of type integer. Like past, it is undefined for the first n - 1 steps of the system.

[ekiwi]

That's great! Thank you pramod!
I wasn't aware of the past and history functions.