SC 2

include order

type node

type value
type round

type ballot = struct {
    n:round,
    x:value
}

TODO: this does not seem to work: type statement = {abort, commit}

type statement
individual commit:statement
individual abort:statement
trusted isolate commit_abort_iso = {
    property commit ~= abort
    property X = commit | X = abort
}

isolate abs_actions = {

    relation vote(N:node, B:ballot, S:statement)

}

isolate ballot_protocol = {

    specification {

        relation vote(N:node, B:ballot, S:statement)

        invariant vote(N,B,S) <-> abs_actions.vote(N,B,S)

        action vote_or_accept_prepared_ghost(v:node,b:ballot)

        after vote_or_accept_prepared_ghost
        {
            assume abs_actions.vote(V,B,S) <-> ((old abs_actions.vote(V,B,S)) | (V = v & S = abort & B < b & x(B) ~= x(b) & (S = commit & ~vote(V,B,abort)) | (S = abort & ~vote(V,B,commit))));
        }

        action send_prepare(v:node, b:ballot, p:ballot, pp:ballot, nc:round, nh:round) = {
            call vote_or_accept_prepared_ghost(v,b);
            vote(v, B, abort) := vote(v, B, abort) | (B < b & x(B) ~= x(b) & (~vote(v,B,commit)));

TODO: the assert below passes, while the invariant fails

            assert vote(N,B,S) <-> abs_actions.vote(N,B,S);
        }
    }

    export send_prepare

} with abs_actions, commit_abort_iso