Pingpong bad

object intf = {
    action ping
    action pong
}

type side_t = {left,right}

object spec = {
    var side : side_t
    init side = left

    before intf.ping {
        assert side = left;
        side := right
    }

    before intf.pong {
        assert side = right;
        side := left
    }
}

object left_player = {
    var ball : bool
    init ball

    action hit = {
        call intf.ping; # forgot to test ball!
        ball := false
    }

    implement intf.pong {
        ball := true
    }

    conjecture left_player.ball -> spec.side = left
}

object right_player = {
    var ball : bool
    init ~ball

    action hit = {
        if ball {
            call intf.pong;
            ball := false
        }
    }

    implement intf.ping {
        ball := true
    }

    conjecture right_player.ball -> spec.side = right
}


export left_player.hit
export right_player.hit

isolate iso_l = left_player with spec
isolate iso_r = right_player with spec