ivy/test/oddeven2.ivy

#lang ivy1.7

object nat = {
    type this

    relation even(N:nat), odd(N:nat)

    axiom even(0) & (even(N) -> odd(N+1))
    axiom odd(1) & (odd(N) -> even(N+1))
}

object evens = {
    var number : nat
    after init {
        number := 0
    }

    action step = {
        call odds.put(number + 1)
    }

    action put(n:nat) = {
        number := n;
    }

    invariant number.even

}

object odds = {
    var number : nat
    after init {
        number := 1
    }

    action step = {
        call evens.put(number + 1)
    }

    action put(n:nat) = {
        number := n;
    }

    invariant number.odd

}

export evens.step
export odds.step