pub fn read_aut(reader: impl Read, hidden_labels: Vec<String>) -> Result<LabelledTransitionSystem<String>, MercError> {

    info!("Reading LTS in .aut format...");

    let mut lines = LineIterator::new(reader);

    lines.advance();

    let header = lines

        .get()

        .ok_or(IOError::InvalidHeader("The first line should be the header"))?;

    let header_regex = Regex::new(r#"des\s*\(\s*([0-9]*)\s*,\s*([0-9]*)\s*,\s*([0-9]*)\s*\)\s*"#)

        .expect("Regex compilation should not fail");

    let (_, [initial_txt, num_of_transitions_txt, num_of_states_txt]) = header_regex

        .captures(header)

        .ok_or(IOError::InvalidHeader(

            "does not match des (<init>, <num_of_transitions>, <num_of_states>)",

        ))?

        .extract();

    let initial_state = StateIndex::new(initial_txt.parse()?);

    let num_of_transitions: usize = num_of_transitions_txt.parse()?;

    let num_of_states: usize = num_of_states_txt.parse()?;

    let mut builder = LtsBuilder::with_capacity(Vec::new(), hidden_labels, num_of_states, 16, num_of_transitions);

    let progress = TimeProgress::new(|percentage: usize| info!("Reading transitions {}%...", percentage), 1);

    while let Some(line) = lines.next() {

        let (from_txt, label_txt, to_txt) =

            read_transition(line).ok_or_else(|| IOError::InvalidTransition(line.clone()))?;

        let from = StateIndex::new(from_txt.parse()?);

        let to = StateIndex::new(to_txt.parse()?);

        debug_trace!("Read transition {from} --[{label_txt}]-> {to}");

        builder.add_transition(from, label_txt, to);

        progress.print(builder.num_of_transitions() * 100 / num_of_transitions);

    info!("Finished reading LTS");

    Ok(builder.finish(initial_state))

}

pub fn write_aut(writer: &mut impl Write, lts: &impl LTS) -> Result<(), MercError> {

    let mut writer = BufWriter::new(writer);

    writeln!(

        writer,

        lts.initial_state_index(),

        lts.num_of_transitions(),

        lts.num_of_states()

    let progress = TimeProgress::new(|percentage: usize| info!("Writing transitions {}%...", percentage), 1);

    let mut transitions_written = 0usize;

    for state_index in lts.iter_states() {

        for transition in lts.outgoing_transitions(state_index) {

            writeln!(

                writer,

                lts.labels()[transition.label.value()],

            progress.print(transitions_written * 100 / lts.num_of_transitions());

            transitions_written += 1;

    Ok(())

}

fn read_transition(input: &str) -> Option<(&str, &str, &str)> {

    let start_paren = input.find('(')?;

    let start_comma = input.find(',')?;

    let start_second_comma = input.rfind(',')?;

    let end_paren = input.rfind(')')?;

    let from = input.get(start_paren + 1..start_comma)?.trim();

    let label = input.get(start_comma + 1..start_second_comma)?.trim();

    let to = input.get(start_second_comma + 1..end_paren)?.trim();

    if label.starts_with('"') && label.ends_with('"') {

        return Some((from, &label[1..label.len() - 1], to));

}

    fn is_tau_label(&self) -> bool {

        self == "tau"

    }

    fn tau_label() -> Self {

        "tau".to_string()

    }

    fn from_index(i: usize) -> Self {

        char::from_digit(i as u32, 36)

            .expect("Radix is less than 37, so should not panic")

            .to_string()

    }

        random_test(100, |rng| {

            let lts = random_lts_monolithic::<String>(rng, 100, 3, 20);

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

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

            let lts_read = read_aut(&buffer[0..], vec![]).unwrap();

            println!("LTS labels: {:?}", lts.labels());

            println!("Read LTS labels: {:?}", lts_read.labels());

            let mapping = lts

                .labels()

                .iter()

                .enumerate()

                .map(|(_i, label)| lts_read.labels().iter().position(|l| l == label))

                .collect::<Vec<_>>();

            for (i, m) in mapping.iter().enumerate() {

                println!("Label {} mapped to {:?}", i, m);

            }

            assert_eq!(lts.num_of_states(), lts_read.num_of_states());

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

            for state_index in lts.iter_states() {

                let transitions: Vec<_> = lts.outgoing_transitions(state_index).collect();

                let transitions_read: Vec<_> = lts_read.outgoing_transitions(state_index).collect();

                transitions.iter().for_each(|t| {

                    let mapped_label = mapping[t.label.value()].expect(&format!("Label {} should be found", t.label));

                    assert!(

                        transitions_read

                            .iter()

                            .any(|tr| tr.to == t.to && tr.label.value() == mapped_label)

                });

        })