#![forbid(unsafe_code)]

use std::borrow::Borrow;

use std::f64::consts::LOG10_2;

use std::hash::Hash;

use std::io::BufWriter;

use std::io::Seek;

use std::io::SeekFrom;

use std::io::Write;

use std::marker::PhantomData;

use merc_utilities::MercError;

use crate::AUT_TAU_LABEL;

use crate::LtsBuilder;

use crate::MCRL2_TAU_LABEL;

use crate::StateIndex;

use crate::TransitionLabel;

/// A stream writer for the AUT format, which allows writing an LTS to a file

/// without keeping the entire LTS in memory. The header of the AUT file is

/// written at the end, after all transitions have been added, to ensure that

/// the correct number of states and transitions is included in the header.

pub struct AutStream<W: Write, L> {

    writer: BufWriter<W>,

    /// The dialect to use when writing tau labels.

    format: AutFormat,

    /// Keep track of the number of transitions added.

    number_of_transitions: usize,

    /// Keep track of the number of states added.

    number_of_states: usize,

    /// Number of bytes reserved for the header line (including its trailing

    /// newline). The real header is padded to exactly this width in

    /// [`AutStream::finish`] so the placeholder is fully overwritten.

    header_len: usize,

    /// Records the label type without affecting the auto traits of the stream:

    /// the labels themselves are never stored, so an `AutStream` stays `Send`

    /// and `Sync` (so it can be wrapped in a [`crate::MutexLtsBuilder`] and shared

    /// across worker threads) even when `L` is neither — for example mCRL2

    /// multi-action labels backed by a thread-local `ATerm`.

    _marker: PhantomData<fn() -> L>,

}

impl<W: Write, L> AutStream<W, L> {

    /// Creates a new AUT stream writer in the standard Aldebaran format

    /// (`i` is used as the tau label).

    ///

    /// Note that the writer is buffered internally using a `BufWriter`. Writing

    /// the placeholder header can fail, so this returns a [`Result`].

    /// Creates a new AUT stream writer in the mCRL2 dialect

    /// (`tau` is used as the tau label).

    /// Creates a new AUT stream writer using the given format.

        // Write a placeholder for the header, which will be filled in later.

        // Reserve enough space for the header using the number of bits of

        // usize. This avoids overwriting transition bytes when the final header

        // is longer.

}

impl<W: Write + Seek, L: TransitionLabel> LtsBuilder<L> for AutStream<W, L> {

    type LTS = ();

    {

        } else {

        }

        // Flush to ensure all buffered transitions are written

        // Seek to the start and overwrite the header. The real header is padded

        // with trailing spaces to fill the entire reserved region (its trailing

        // newline lands as the last reserved byte), so no leftover placeholder

        // spaces remain to form a spurious, invalid transition line on read —

        // which matters in particular when there are no transitions at all.

            "des ({}, {}, {})",

            initial_state, self.number_of_transitions, self.number_of_states

        );

        // Flush the updated header

    /// Returns the number of transitions added to the builder.

    /// Returns the number of states added to the builder.

    /// Sets the number of states to at least the given number. All states

    /// without transitions simply become deadlock states.

}

/// The dialect of the AUT format, which controls the textual label used for

/// internal (tau) transitions.

#[derive(Clone, Copy, Debug, PartialEq, Eq)]

#[cfg_attr(feature = "clap", derive(clap::ValueEnum))]

pub enum AutFormat {

    /// The standard Aldebaran format, which uses `i` for tau transitions.

    Aut,

    /// The mCRL2 dialect of the Aldebaran format, which uses `tau` for tau transitions.

    AutMcrl2,

}

impl AutFormat {

    /// Returns the string that represents the tau label in this format.

        }

}

#[cfg(test)]

mod tests {

    use std::io::Cursor;

    use merc_utilities::random_test;

    use crate::AutStream;

    use crate::LTS;

    use crate::LtsBuilder;

    use crate::random_lts;

    use crate::read_aut;

    #[test]

    #[cfg_attr(miri, ignore)] // Test is too slow under Miri

            {

                // Write all the transitions to the stream.

                }

            }

            // Rewind the buffer to the beginning before reading.

    /// An LTS with no transitions (a single deadlock state) must round-trip:

    /// the header placeholder must be fully overwritten so no line of leftover

    /// padding spaces is left behind for the reader to choke on.

    #[test]

}