Liveness mc1

This file contains a simple liveness proof, also shown in figure 3 in the tool paper submission.

To verify this file, run:

$ ivy_check liveness.ivy
...
OK

include mc_schemata

module signal = {
    action raise

    specification {
        relation now
        after init { now := false; }
        before raise {
            now := true;
            now := false;
        }
    }
}

isolate bar = {
    finite type t
    action step(x:t)
    var last : t        # history variable

    specification {
        relation pending(X:t)
        after init {
            pending(X) := true;
        }
        instance enter : signal

        before step {
            require pending(x);
            call enter.raise;
            pending(x) := false;
            last := x;
        }

        temporal property
            (globally eventually enter.now) ->
            eventually forall X.~pending(X)
        proof {
            tactic l2s_full proof {let L = last}
            showgoals
            tactic mc
            showgoals
        }
    }
}

export bar.step