pub fn translate(lts: &LabelledTransitionSystem<String>, formula: &StateFrm) -> Result<ParityGame, MercError> {

    let labels = lts

        .labels()

        .iter()

        .map(|label| {

            if label.is_tau_label() {

                Ok(MultiAction::tau())

                MultiAction::parse(label)

        })

        .collect::<Result<Vec<MultiAction>, MercError>>()?;

    warn_unknown_action_labels(formula, &labels);

    let mut identifier_generator = FreshStateVarGenerator::new(formula);

    let formula = translate_regular_formulas(formula.clone(), &mut identifier_generator);

    debug!("Translated regular formulas: {}", formula);

    let equation_system = ModalEquationSystem::new(&formula);

    debug!("{}", equation_system);

    let mut algorithm: Translation<'_, _, ()> = Translation::new(lts, &labels, &equation_system);

    algorithm.translate(lts.initial_state_index(), 0, |_| (), |_, _| Ok(()))?;

    let vertices = algorithm.vertices();

    let result = ParityGame::from_edges(

        VertexIndex::new(0),

        vertices.iter().map(|(player, _)| *player).collect(),

        vertices.iter().map(|(_, priority)| *priority).collect(),

        || algorithm.edges.iter().map(|(s, _, t)| (*s, *t)),

    if cfg!(debug_assertions) {

        let (_, reachable_vertices) = compute_reachable(&result);

        debug_assert!(

            reachable_vertices.iter().all(|v| v.is_some()),

    Ok(result)

}

pub fn warn_unknown_action_labels(formula: &StateFrm, labels: &[MultiAction]) {

    visit_statefrm::<(), _>(formula, |statefrm| {

        if let StateFrm::Modality { formula, .. } = statefrm {

            visit_regular_formula::<(), _>(formula, |regfrm| {

                if let RegFrm::Action(act_frm) = regfrm {

                    visit_action_formula::<(), _>(act_frm, |act_frm| {

                        if let ActFrm::MultAct(action) = act_frm

                            && !labels.contains(action)

                        }

                        Ok(ControlFlow::Continue(()))

                    })?;

                }

                Ok(ControlFlow::Continue(()))

            })?;

        }

        Ok(ControlFlow::Continue(()))

    })

    .expect("Failed to visit state formula");

}

pub fn translate_regular_formulas(formula: StateFrm, identifier_generator: &mut FreshStateVarGenerator) -> StateFrm {

    apply_statefrm(formula, |subformula| {

            operator,

            formula,

            expr,

        } = subformula

            return match formula {

                merc_syntax::RegFrm::Action(_action_frm) => Ok(None),

                merc_syntax::RegFrm::Iteration(reg_frm) => {

                    let iteration_var = identifier_generator.generate("I");

                    Ok(Some(translate_regular_formulas(

                        convert_regular_iteration(*operator, reg_frm, iteration_var, operator, expr),

                        identifier_generator,

                    )))

        }

        Ok(None)

    })

    .expect("Failed to visit state formula")

}

fn convert_regular_iteration(

    modality: ModalityOperator,

    reg_frm: &RegFrm,

    iteration_var: String,

    operator: &ModalityOperator,

    expr: &StateFrm,

) -> StateFrm {

        operator: if modality == ModalityOperator::Box {

            FixedPointOperator::Greatest

            FixedPointOperator::Least

        variable: StateVarDecl::new(iteration_var.clone(), Vec::new()),

        body: Box::new(StateFrm::Binary {

            op: if modality == ModalityOperator::Box {

                StateFrmOp::Conjunction

                StateFrmOp::Disjunction

            lhs: Box::new(StateFrm::Modality {

                operator: *operator,

                formula: reg_frm.clone(),

                expr: Box::new(StateFrm::Id(iteration_var, Vec::new())),

            }),

            rhs: Box::new(expr.clone()),

}

    pub(crate) fn new(

        lts: &'a L,

        parsed_labels: &'a Vec<MultiAction>,

        equation_system: &'a ModalEquationSystem,

    ) -> Self {

        let progress: TimeProgress<usize> = TimeProgress::new(

        Self {

            vertex_map: IndexedSet::new(),

            vertices: Vec::new(),

            edges: Vec::new(),

            seen_modality_targets: HashMap::new(),

            queue: Vec::new(),

            lts,

            parsed_labels,

            equation_system,

            progress,

        }

    }

    pub(crate) fn translate<F, C>(

        &mut self,

        initial_state: StateIndex,

        initial_equation_index: usize,

        labelling: F,

        combine_labelling: C,

    ) -> Result<(), MercError>

    where

        F: Fn(Option<Transition>) -> E,

        C: Fn(&mut E, E) -> Result<(), MercError>,

        self.queue = vec![(

            initial_state,

            Formula::Equation(initial_equation_index),

            VertexIndex::new(0),

        )];

        self.vertex_map

            .insert((initial_state, Formula::Equation(initial_equation_index)));

        self.vertices.push(None); // Placeholder for the initial vertex

        while let Some((s, formula, vertex_index)) = self.queue.pop() {

            debug!("Translating vertex {}: (s={}, formula={})", vertex_index, s, formula);

            self.progress.print(self.vertices.len());

            match formula {

                Formula::StateFrm(f) => {

                    self.translate_vertex(s, f, vertex_index, &labelling, &combine_labelling)?;

                Formula::Equation(i) => {

                    self.translate_equation(s, i, vertex_index, &labelling);

                }

        Ok(())

    }

    pub(crate) fn vertices(&self) -> Vec<(Player, Priority)> {

        debug_assert!(

            self.vertices.iter().all(|v| v.is_some()),

        self.vertices

            .iter()

            .filter_map(|vertex| vertex.as_ref().copied())

            .collect()

    }

    pub(crate) fn edges(&self) -> &Vec<(VertexIndex, E, VertexIndex)> {

        &self.edges

    }

    fn translate_vertex<F, C>(

        &mut self,

        s: StateIndex,

        formula: &'a StateFrm,

        vertex_index: VertexIndex,

        labelling: &F,

        combine_labelling: &C,

    ) -> Result<(), MercError>

    where

        F: Fn(Option<Transition>) -> E,

        C: Fn(&mut E, E) -> Result<(), MercError>,

        match formula {

            StateFrm::True => {

                // (s, true) → odd, 0

                self.set_vertex(vertex_index, Player::Odd, Priority::new(0));

            }

            StateFrm::False => {

                // (s, false) → even, 0

                self.set_vertex(vertex_index, Player::Even, Priority::new(0));

            }

            StateFrm::Binary { op, lhs, rhs } => {

                match op {

                    StateFrmOp::Conjunction => {

                        // (s, Ψ_1 ∧ Ψ_2) →_P odd, (s, Ψ_1) and (s, Ψ_2), 0

                        self.set_vertex(vertex_index, Player::Odd, Priority::new(0));

                        let s_psi_1 = self.queue_vertex(s, Formula::StateFrm(lhs));

                        let s_psi_2 = self.queue_vertex(s, Formula::StateFrm(rhs));

                        self.edges.push((vertex_index, labelling(None), s_psi_1));

                        self.edges.push((vertex_index, labelling(None), s_psi_2));

                    }

                    StateFrmOp::Disjunction => {

                        // (s, Ψ_1 ∨ Ψ_2) →_P even, (s, Ψ_1) and (s, Ψ_2), 0

                        self.set_vertex(vertex_index, Player::Even, Priority::new(0));

                        let s_psi_1 = self.queue_vertex(s, Formula::StateFrm(lhs));

                        let s_psi_2 = self.queue_vertex(s, Formula::StateFrm(rhs));

                        self.edges.push((vertex_index, labelling(None), s_psi_1));

                        self.edges.push((vertex_index, labelling(None), s_psi_2));

                    }

            StateFrm::Id(identifier, _args) => {

                let (i, _equation) = self

                    .equation_system

                    .find_equation_by_identifier(identifier)

                    .expect("Variable must correspond to an equation");

                self.set_vertex(vertex_index, Player::Odd, Priority::new(0)); // The priority and owner do not matter here

                let equation_vertex = self.queue_vertex(s, Formula::Equation(i));

                self.edges.push((vertex_index, labelling(None), equation_vertex));

            }

                operator,

                formula,

                expr,

                self.translate_modality_vertex(

                    s,

                    *operator,

                    formula,

                    expr,

                    vertex_index,

                    labelling,

                    combine_labelling,

        Ok(())

    }

    fn translate_modality_vertex<F, C>(

        &mut self,

        s: StateIndex,

        operator: ModalityOperator,

        formula: &'a RegFrm,

        expr: &'a StateFrm,

        vertex_index: VertexIndex,

        labelling: &F,

        combine_labelling: &C,

    ) -> Result<(), MercError>

    where

        F: Fn(Option<Transition>) -> E,

        C: Fn(&mut E, E) -> Result<(), MercError>,

        let player = match operator {

            ModalityOperator::Box => Player::Odd,

            ModalityOperator::Diamond => Player::Even,

        self.set_vertex(vertex_index, player, Priority::new(0));

        self.seen_modality_targets.clear();

        for transition in self.lts.outgoing_transitions(s) {

            let action = &self.parsed_labels[*transition.label];

            if match_regular_formula(formula, action) {

                let s_prime_psi = self.queue_vertex(transition.to, Formula::StateFrm(expr));

                let label = labelling(Some(transition));

                if let Some(edge_index) = self.seen_modality_targets.get(&s_prime_psi).copied() {

                } else {

                    let edge_index = self.edges.len();

                    self.edges.push((vertex_index, label, s_prime_psi));

                    self.seen_modality_targets.insert(s_prime_psi, edge_index);

                }

            }

        Ok(())

    }

    fn translate_equation<F>(&mut self, s: StateIndex, equation_index: usize, vertex_index: VertexIndex, labelling: &F)

    where

        F: Fn(Option<Transition>) -> E,

        let equation = self.equation_system.equation(equation_index);

        match equation.operator() {

            FixedPointOperator::Least => {

                // (s, μ X. Ψ) →_P odd, (s, Ψ[x := μ X. Ψ]), 2 * floor(AD(Ψ)/2) + 1. In Rust division is already floor.

                self.set_vertex(

                    vertex_index,

                    Player::Odd,

                    Priority::new(2 * (self.equation_system.alternation_depth(equation_index) / 2) + 1),

                );

                let s_psi = self.queue_vertex(s, Formula::StateFrm(equation.body()));

                self.edges.push((vertex_index, labelling(None), s_psi));

            }

            FixedPointOperator::Greatest => {

                // (s, ν X. Ψ) →_P even, (s, Ψ[x := ν X. Ψ]), 2 * floor(AD(Ψ)/2). In Rust division is already floor.

                self.set_vertex(

                    vertex_index,

                    Player::Even,

                    Priority::new(2 * (self.equation_system.alternation_depth(equation_index) / 2)),

                );

                let s_psi = self.queue_vertex(s, Formula::StateFrm(equation.body()));

                self.edges.push((vertex_index, labelling(None), s_psi));

            }

    }

    fn set_vertex(&mut self, vertex_index: VertexIndex, player: Player, priority: Priority) {

        debug_assert!(

            self.vertices[vertex_index].is_none(),

        self.vertices[vertex_index] = Some((player, priority));

    }

    fn queue_vertex(&mut self, s: StateIndex, formula: Formula<'a>) -> VertexIndex {

        let (index, inserted) = self.vertex_map.insert((s, formula.clone()));

        let vertex_index = VertexIndex::new(*index);

        if inserted {

            // New vertex, assign placeholder values

            self.vertices.resize(*vertex_index + 1, None);

            self.queue.push((s, formula, vertex_index));

        }

        vertex_index

    }

fn match_regular_formula(formula: &RegFrm, action: &MultiAction) -> bool {

    match formula {

        RegFrm::Action(action_formula) => match_action_formula(action_formula, action),

}

fn match_action_formula(formula: &ActFrm, action: &MultiAction) -> bool {

    match formula {

        ActFrm::MultAct(expected_action) => match_multi_action(expected_action, action),

        ActFrm::Negation(expr) => !match_action_formula(expr, action),

}

fn match_multi_action(expected: &MultiAction, actual: &MultiAction) -> bool {

    if expected.actions.len() != actual.actions.len() {

        return false;

    }

    let mut expected_actions: Vec<_> = expected.actions.iter().collect();

    let mut actual_actions: Vec<_> = actual.actions.iter().collect();

    expected_actions.sort_unstable();

    actual_actions.sort_unstable();

    expected_actions == actual_actions

}

            compute_reachable(&pg).1.iter().all(|v| v.is_some()),