Trivial l2s example fails with stack trace

[nano-o]

temporal property globally true
proof {
    tactic l2s
}

[kenmcmil]

Thanks. Fix in commit 11dd4d7.

By the way, the proof of globally true using l2s is less trivial than you might think:

#lang ivy1.7

temporal property globally true
proof {
    tactic l2s with
    invariant ~globally true
    invariant ($was$ true) -> (~$happened$ ~true)
}

This is because l2s doesn't know any tautologies of temporal logic. It uses proof by contradiction, so it assumes initially that globally true is false. Since true is never false, this means that ~globally true is invariantly true (i.e., true is always false in the future). But to show there is no fair cycle (one in which true is infinitely often false) we also need the invariant that, when in the cycle, ~true never happened in the past.

Personally, I find this much too confusing for a proof of globally true!

[nano-o]

Interesting! I did not know about $was$ and $happened$. Are there examples showing how to use them?

Here is a liveness proof of an example I used before. If you have some feedback on the style I'd be interested to hear it.

#lang ivy1.7

type node
type value
type quorum
relation member(N:node, Q:quorum)
axiom exists N . member(N,Q1) & member(N,Q2)
relation proposal(N:node,V:value)
relation decision(N:node,V:value)
relation received(N:node,M:node,V:value)
after init {
  proposal(N,V) := false;
  decision(N,V) := false;
  received(N,M,V) := false;
  l2s_d(N:node) := true; # there is a fixed number of nodes
}
export action propose(n:node, v:value) = {
    assume ~proposal(n,V); # never proposed before
    proposal(n,v) := true;
}
export action receive(n:node, m:node, v:value) = {
    assume proposal(m,v);
    received(n,m,v) := true;
    if exists Q . forall N . member(N,Q) -> received(n,N,v) {
        decision(n,v) := true;
    }
}
export action no_op = {} # Is l2s sound without this? I.e. when there are no infinite executions.

# safety proof:
invariant [safety] decision(N1,V1) & decision(N2,V2) -> V1 = V2
invariant proposal(N,V1) & proposal(N,V2) -> V1 = V2
invariant received(N,M,V) -> proposal(M,V)
invariant (exists N1 . decision(N1,V)) -> exists Q . forall N . member(N,Q) -> proposal(N,V)
# liveness property:
# witnesses:
individual q:quorum
individual v:value
individual n:node
temporal property (
    (forall N,V . globally (member(N,q) & proposal(N,V) -> V = v)) &
    (forall N . member(N,q) -> eventually proposal(N,v)) &
    (forall N,M,V . globally (proposal(N,V) -> eventually received(M,N,V))) &
    ((exists N . globally ~decision(N,v)) -> globally ~decision(n,v)) # TODO: q and v like that
) -> forall N . eventually decision(N,v)
proof {
    tactic l2s with
        invariant l2s_d(N:node) & l2s_d(v) & l2s_d(q)
        invariant exists N . globally ~decision (N,v) # negation of the goal
        invariant globally ~decision (n,v) # witness
        invariant globally (member(N,q) & proposal(N,V) -> V = v)
        invariant globally (proposal(N,V) -> eventually received(M,N,V))
        invariant member(N,q) -> eventually proposal(N,v)
        invariant member(N,q) -> ($l2s_w N . proposal(N,v))(N) | proposal(N,v)
        invariant V = v -> ($l2s_w M,N,V . received(M,N,V))(M,N,V) | (globally ~received(M,N,V)) | received(M,N,V)
        invariant (forall N . member(N,q) -> received(n,N,v)) -> decision(n,v) # contradiction with the negation of the goal
}

[kenmcmil]

Well, $was$ phi(V) is an abbreviation for l2s_saved & ($l2s_s V.phi(V))(V), meaning that phi(V) held at the beginning of the cycle (the save point) while $happened$ phi(V) is an abbreviation for l2s_saved & ~($l2s_w V.phi(V))(V) meaning that phi(V) was true at some time during the cycle.