use merc_aterm::ATerm;

use merc_data::DataSpecification;

use merc_ldd::Ldd;

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

pub struct SymbolicLts {

    data_specification: DataSpecification,

    states: Ldd,

    /// A singleton LDD representing the initial state.

    initial_state: Ldd,

    summand_groups: Vec<SummandGroup>,

}

impl SymbolicLts {

    /// Creates a new symbolic LTS.

    /// Returns the data specification of the LTS.

    /// Returns the LDD representing the set of states.

    /// Returns the LDD representing the initial state.

    /// Returns an iterator over the summand groups.

}

/// Represents a short vector transition relation for a group of summands.

///

/// # Details

///

/// A short transition vector is part of a transition relation T -> U, where we

/// store T' -> U' with T' being the projection of T on the read parameters and

/// U' the projection of U on the write parameters, as a LDD. Formally,

///

/// (t, u) in (T -> U)  iff  (t', u') in (T' -> U') where t' and u' are the projections

///     of t and u on the read and write parameters respectively.

pub struct SummandGroup {

    read_parameters: Vec<ATerm>,

    write_parameters: Vec<ATerm>,

    /// The transition relation T' -> U' for this summand group.

    relation: Ldd,

}

impl SummandGroup {

    /// Creates a new summand group.

    /// Returns the transition relation LDD for this summand group.

    /// Returns the read parameters for this summand group.

    /// Returns the write parameters for this summand group.

}