#![forbid(unsafe_code)]

use std::io::BufWriter;

use std::io::Read;

use std::io::Write;

use log::info;

use merc_io::LargeFormatter;

use regex::Regex;

use streaming_iterator::StreamingIterator;

use thiserror::Error;

use merc_io::LineIterator;

use merc_io::TimeProgress;

use merc_utilities::MercError;

use merc_utilities::debug_trace;

use crate::LTS;

use crate::LabelledTransitionSystem;

use crate::LtsBuilder;

use crate::LtsBuilderMem;

use crate::StateIndex;

use crate::TransitionLabel;

#[derive(Error, Debug)]

pub enum IOError {

    #[error("Invalid .aut header {0}")]

    InvalidHeader(&'static str),

    #[error("Invalid transition {0}")]

    InvalidTransition(String),

}

/// The label used for internal transitions in the mCRL2 format.

const MCRL2_TAU_LABEL: &str = "tau";

/// The label used for internal transitions in the Aldebaran format.

const AUT_TAU_LABEL: &str = "i";

/// Loads a labelled transition system in the [Aldebaran

/// format](https://cadp.inria.fr/man/aldebaran.html) from the given reader.

///

/// Note that the reader has a buffer in the form of  `BufReader`` internally.

///

/// The Aldebaran format consists of a header: `des (<initial>: Nat,

///     <num_of_transitions>: Nat, <num_of_states>: Nat)`

///     

/// And one line for every transition either one of these cases:

///  `(<from>: Nat, "<label>": Str, <to>: Nat)`

///  `(<from>: Nat, <label>: Str, <to>: Nat)`

/// The same as [read_aut], but with the `tau` as the internal transition, instead of `i`.

/// The implementation of [read_aut] and [read_aut_mcrl2].

///

/// The `tau_label` specifics which label is considered as the internal transition.

    // Regex for des (<initial>: Nat, <num_of_states>: Nat, <num_of_transitions>: Nat)

        16,

    );

                "Read {} transitions {}%...",

            )

        1,

    );

        // Parse the from and to states, with the given label.

    }

/// Write a labelled transition system in plain text in Aldebaran format to the

/// given writer, see [read_aut].

///

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

/// The same as [write_aut], but with the `tau` as the internal transition, instead of `i`.

/// The implementation of [write_aut] and [write_mcrl2_aut].

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

                "Wrote {} transitions {}%...",

            )

        1,

    );

            } else {

                    "({}, \"{}\", {})",

                    state_index,

                    transition.to

            }

        }

    }

/// Dedicated function to parse the following transition formats:

///

/// # Details

///

/// One of the following formats:

///     `(<from>: Nat, "<label>": Str, <to>: Nat)`

///     `(<from>: Nat, <label>: Str, <to>: Nat)`

///

/// This was generally faster than the regex variant, since that one has to backtrack after

    // Find the comma in the second part

    // Handle the special case where it has quotes.

/// A trait for labels that can be used in transitions.

impl TransitionLabel for String {

}

#[cfg(test)]

mod tests {

    use merc_utilities::random_test;

    use test_log::test;

    use crate::LTS;

    use crate::random_lts;

    use crate::read_aut;

    use crate::write_aut;

    #[test]

    fn test_reading_aut() {

        let file = include_str!("../../../examples/lts/abp.aut");

        let lts = read_aut(file.as_bytes()).unwrap();

        assert_eq!(lts.initial_state_index().value(), 0);

        assert_eq!(lts.num_of_transitions(), 92);

    }

    #[test]

    fn test_lts_failure() {

        let wrong_header = "

        des (0,2,                                     

            (0,\"r1(d1)\",1)

            (0,\"r1(d2)\",2)

        ";

        debug_assert!(read_aut(wrong_header.as_bytes()).is_err());

        let wrong_transition = "

        des (0,2,3)                           

            (0,\"r1(d1),1)

            (0,\"r1(d2)\",2)

        ";

        debug_assert!(read_aut(wrong_transition.as_bytes()).is_err());

    }

    #[test]

    fn test_traversal_lts() {

        let file = include_str!("../../../examples/lts/abp.aut");

        let lts = read_aut(file.as_bytes()).unwrap();

        // Check the number of outgoing transitions of the initial state

        assert_eq!(lts.outgoing_transitions(lts.initial_state_index()).count(), 2);

    }

    #[test]

    fn test_writing_lts() {

        let file = include_str!("../../../examples/lts/abp.aut");

        let lts_original = read_aut(file.as_bytes()).unwrap();

        // Check that it can be read after writing, and results in the same LTS.

        let mut buffer: Vec<u8> = Vec::new();

        write_aut(&mut buffer, &lts_original).unwrap();

        let lts = read_aut(&buffer[0..]).unwrap();

        assert!(lts.num_of_states() == lts_original.num_of_states());

        assert!(lts.num_of_labels() == lts_original.num_of_labels());

        assert!(lts.num_of_transitions() == lts_original.num_of_transitions());

    }

    #[test]

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

    fn test_random_aut_io() {

    }

}