use merc_data::DataExpression;

use merc_data::DataSpecification;

use merc_lts::LtsAction;

use merc_lts::LtsMultiAction;

use oxidd::ldd::LDDFunction;

use crate::SummandGroup;

use crate::SymbolicLPS;

use crate::SymbolicLTS;

/// Represents a symbolic LTS encoded by a disjunctive transition relation and a set of states.

pub struct SymbolicLts {

    data_specification: DataSpecification,

    states: LDDFunction,

    /// A singleton LDD representing the initial state.

    initial_state: LDDFunction,

    summand_groups: Vec<SummandGroup>,

    /// The action labels of the LTS, stored as their string representation,

    /// their position corresponds to the LDD values.

    action_labels: Vec<String>,

    /// The possible values for each process parameter, their position

    /// corresponds to the LDD values.

    parameter_values: Vec<Vec<DataExpression>>,

}

impl SymbolicLts {

    /// Creates a new symbolic LTS.

    ///

    /// `states` is the known state space (pass `initial_state.clone()` when the full set is not

    /// yet known, or provide the reachable set computed by [crate::reachability]).

    /// Returns the data specification of the LTS.

}

impl SymbolicLPS for SymbolicLts {

    type Group = SummandGroup;

}

impl SymbolicLTS for SymbolicLts {

}