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

    read_aut_impl(reader, AUT_TAU_LABEL)

}

fn read_aut_impl<R: Read>(reader: R, tau_label: &str) -> 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 = LtsBuilderMem::with_capacity(

        Vec::new(),

        vec![tau_label.to_string()],

        num_of_states,

        num_of_transitions,

    builder.require_num_of_states(num_of_states);

    let progress = TimeProgress::new(

    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());

    info!("Finished reading LTS");

    builder.finish(initial_state)

}

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

    write_aut_impl(writer, lts, AUT_TAU_LABEL)

}

fn write_aut_impl<W: Write, L: LTS>(writer: &mut W, lts: &L, tau_label: &str) -> Result<(), MercError> {

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

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

    writeln!(

        writer,

        lts.initial_state_index(),

        lts.num_of_transitions(),

        lts.num_of_states()

    let num_of_transitions = lts.num_of_transitions();

    let progress = TimeProgress::new(

    let mut transitions_written = 0usize;

    for state_index in lts.iter_states() {

        for transition in lts.outgoing_transitions(state_index) {

            if lts.is_hidden_label(transition.label) {

                writeln!(writer, "({}, \"{}\", {})", state_index, tau_label, transition.to)?;

                writeln!(

                    writer,

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

            progress.print(transitions_written);

            transitions_written += 1;

    info!("Finished writing LTS.");

    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));

    }

    Some((from, label, to))

}

    fn is_tau_label(&self) -> bool {

        self == "τ"

    }

    fn tau_label() -> Self {

        "τ".to_string()

    }

    fn matches_label(&self, label: &str) -> bool {

        self == label

    }

    fn from_index(i: usize) -> Self {

        char::from_digit(i as u32 + 10, 36)

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

            .to_string()

    }

    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);

    }

    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());

    }

    fn test_traversal_lts() {

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

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

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

    }

    fn test_writing_lts() {

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

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

        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());

    }

    fn test_random_aut_io() {

        random_test(100, |rng| {

            let lts = random_lts::<String, _>(rng, 1000, 3);

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

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

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

            crate::check_equivalent(&lts, &result_lts);

        })

    }