//! Authors: Maurice Laveaux

//!

//! Implementation of the priority promotion algorithm introduced in:

//!

//! > Massimo Benerecetti, Daniele Dell'Erba, and Fabio Mogavero. Solving

//! > Parity Games via Priority Promotion, pages 270-290. Springer International

//! > Publishing, Cham, 2016.

//!

//! Given the current triple (region_function, strategy, prio), referred to as

//! state, a region R is extracted by means of the query function. An alpha-region

//! is a set of vertices R and a witness strategy sigma. So that for all plays

//! consistent with sigma, they either stay within R and are winning for alpha.

//! Or they escape R via vertices having the highest priority in the game. The

//! initial state is (priority_function, empty_strategy, min(range(priority_function)))

//!

//! If the region R is a dominion in the whole game, the dominion is removed from

//! the game and the algorithm runs on the remaining game. If the extracted region

//! is open in the subgame G >= prio. Which is the subgame with only vertices

//! having greater or equal priority then prio. The next state becomes

//! (region_function\[R -> prio\], strategy\*, min(range(region_function >= prio))).

//!

//! If the alpha-region is a dominion in the subgame G >= prio, the lowest priority

//! region that the opponent can flee to is determined in [`PriorityPromotionSolver::promote_sub_dominion`].

//! And then the next state becomes (region_function\*\[R -> prio\*\], strategy\*, prio\*), and

//! in region_function\* all regions below prio\* are reset to the original priority.

//!

//! The strategy\* was not presented in the paper, but was partially determined

//! by the follow up paper Improving Priority Promotion for parity games. For

//! the attractor for some region R the strategy is determined by the witness

//! that alpha can reach R. For vertices inside the region R a witness core strategy

//! sigma is given. For all vertices inside R where no strategy is defined yet

//! an arbitrary successor inside R is taken to complete the strategy.

use std::collections::VecDeque;

use bitvec::bitvec;

use bitvec::order::Lsb0;

use log::debug;

use log::trace;

use crate::PG;

use crate::Player;

use crate::Pred;

use crate::Predecessors;

use crate::Priority;

use crate::Strat;

use crate::Strategy;

use crate::VertexIndex;

use crate::zielonka::Set;

/// Solves the given parity game using the priority promotion algorithm.

///

/// Returns the winning sets for both players and optionally their strategies.

    } else {

    }

/// Solves the given parity game using the priority promotion algorithm,

/// computing a strategy representation of type `S`.

        "Priority promotion solver requires a total parity game"

    );

            Player::Even => {

            }

            Player::Odd => {

            }

        }

    }

/// Internal solver state for the priority promotion algorithm.

struct PriorityPromotionSolver<'a, G: PG> {

    game: &'a G,

    /// Precomputed predecessors for backward iteration.

    predecessors: Predecessors<'a>,

    /// Maps each vertex to its current region priority.

    /// `None` indicates a solved vertex.

    region_function: Vec<Option<Priority>>,

    /// Stores a list of vertices not yet solved by the algorithm.

    unsolved: Vec<VertexIndex>,

    /// Count the number of vertices per region, to speed up [`Self::next_priority`].

    regions: Vec<usize>,

    /// This is a reused queue with vertices to compute the attractor set from.

    todo: VecDeque<VertexIndex>,

    /// Reused per-vertex counter, used during attractor computation to count the

    /// number of successors of an opponent vertex that can still enter the

    /// region being computed.

    attractor_counters: Vec<usize>,

    /// The number of promotions required.

    promotions: usize,

    /// The number of dominions found.

    dominions: usize,

    /// Records the winning player for each vertex (set when a dominion is found).

    final_winner: Vec<Player>,

}

impl<'a, G: PG> PriorityPromotionSolver<'a, G> {

    /// Creates a new priority promotion solver for the given parity game.

        // The lowest priority in the game (the highest number).

        // Set region_function to the original priorities and initialize the mapping.

        // Initialize all regions that have some vertices.

        }

    /// Compute winning strategies by means of priority promotion, follows the

    /// paper as closely as possible.

    ///

    /// # Details

    ///

    /// Important note: instead of actually repeatedly removing dominions from

    /// the game, the game is kept the same but the region_function is used to

    /// determine which vertices still are not solved. This is done because

    /// removing subgames allocates new memory repeatedly and parity games

    /// can be huge.

        // Find the highest priority in the game.

        // The algorithm was tail recursive so can also be written as iteration.

        loop {

                // Keep the new region_function and substrategy, but go to the next priority.

                // This is a dominion D in the whole game, compute the attractor

                // for this region.

                }

                // Remove the dominion from the game and keep the unsolved vertices, also reset

                // lower priorities and set region of prio to the COMPUTED_REGION.

                // Record the winner for this dominion.

                }

                // Reset the unsolved set and remove all regions, also add one dominion to statistics.

                }

                // Reset the game and find the highest priority in the game.

            } else {

                // The game is a dominion, but only in the subgame, so promote its priority.

            }

        }

            "{} dominions found, and {} promotions required",

            self.dominions, self.promotions

        );

    /// From the state (region_function, strategy, prio) compute the new alpha-region

    /// R and update region_function\[R -> p\]. The strategy will be updated in

    /// [`Self::compute_attractor`]. The unsolved set is used to quickly iterate unsolved vertices.

    /// The todo queue is passed to be reused by [`Self::compute_attractor`].

        // Make sure nothing else is stored in the todo.

        // R* = region_function^-1(prio), this results in the todo for the attractor

        // computation, the initial set essentially.

        }

        // (region_function[R -> prio], strategy*) <- computeAttractor_G(todo, strategy

        // restricted to todo)

    /// Compute the attractor set A for vertices in todo, with alpha being prio mod 2.

    /// `in_subgraph` indicates that only vertices in game <= prio are considered. This

    /// updates region_function\[A -> prio\]. The strategy is changed for alpha for the

    /// attraction witness. The remaining vertices of alpha without a strategy can pick

    /// any vertex inside A as witness.

        // Initialise, for every opponent vertex still under consideration, the

        // number of its outgoing edges that lead to a vertex which can still

        // enter the region with priority `prio` (a "poppable" target: not yet

        // solved, and inside the subgame when `in_subgraph`). The opponent

        // vertex is attracted once all of those targets have been attracted.

        }

        // O(V + E): Compute the attractor set to the alpha-region.

            // Check all predecessors v of w.

                // Skip predecessors that are already in the attractor set, also skip

                // vertices outside the subgame G <= prio. Or vertices that are computed.

                {

                    // One more successor of v (namely w) entered the region. The

                    // opponent vertex v is only attracted once every successor

                    // that could enter the region has actually done so.

                    // For opponent controlled vertices no strategy exists, so

                    // every possible outgoing edge is losing.

                }

                // Add a vertex to their new region and remove from the old one.

                // When this part is reached, all liberties of v are gone or v belongs

                // to alpha, so add vertex v to the attractor set.

            }

        }

        // R \ domain(tau restricted to R*), essentially vertices in R belonging to

        // alpha where no strategy is defined yet. These can pick an arbitrary

        // successor that can reach R \ R*, these already have an attraction

        // strategy so that is always fine.

                        // There exists some (v, w) in E such that w belongs to R (has r[w] == prio).

                }

        }

    /// Determine whether the alpha-region with priority `prio` is open in G, or

    /// in G <= prio (indicated by `in_subgraph`). This means that for all vertices

    /// v with region_function\[v\] equal to prio, this is set R. When v belongs

    /// to alpha, determined by prio mod 2, there is some witness successor in R.

    /// For opponent vertices all successors lead to R, no witness to escape basically.

        // O(V): Loop over unsolved vertices and find vertices belonging to region with prio.

                    // For all (v, u) in E, u should belong to R.

                        // There is an edge from opponent to a vertex in the subgraph or in the whole graph.

                        {

                    }

                } else {

                    // If there exists a (v, u) to R its closed.

                }

        }

    /// Promote a sub dominion D to the minimum region greater than prio that the

    /// opponent can reach. This updates region_function\[D -> prio\*\] and resets

    /// all priorities greater than prio\* to the original priority function. The

    /// strategy is updated by means of [`Self::compute_attractor`]. And lower strategies

    /// are set to `None` (no strategy known).

    ///

    /// # Details

    ///

    /// This is referred to as r\* = bep(R, r) in the paper (best escape priority).

    /// For every opponent vertex this is the highest priority that it can reach.

    /// The region it can reach belongs to alpha,

    /// otherwise it would be attracted in some earlier state.

        // O(V): It is only a dominion in the subgraph, determine lowest p > prio

        // that opponent can escape to.

                // For all (v, u) in E collect the lowest priority larger than prio that opponent can flee to.

                }

        }

        // Here the prio region is promoted to the new priority and all lower positions

        // are reset.

        }

    /// Print the vertices with region_function\[v\] equal to prio, representing the region.

    ///

    /// This costs O(V) so only enable this in debug.

                "alpha-region[{}] = {{ {} }}",

                prio,

            );

    /// Computes max(rng(region_function <= prio)), so the next lower priority,

    /// smaller or equal to prio, that some vertex has.

    ///

    /// Starting from the current priority, find the next region that exists.

    /// This should never go out of bounds as the lowest region will always be a dominion.

        }

}

#[cfg(test)]

mod tests {

    use merc_io::DumpFiles;

    use merc_utilities::random_test;

    use crate::random_parity_game;

    use crate::solve_zielonka;

    use crate::verify_solution;

    use crate::write_pg;

    use super::*;

    #[test]

    #[cfg_attr(miri, ignore)] // Miri is too slow for this test.

    #[test]

    #[cfg_attr(miri, ignore)]

                "Even winning sets differ between priority promotion and Zielonka"

            );

                "Odd winning sets differ between priority promotion and Zielonka"

            );

}