Function biodivine_sketchbook::algorithms::eval_dynamic::encode::encode_dataset_hctl_str

pub fn encode_dataset_hctl_str(
    dataset: &Dataset,
    observation_id: Option<ObservationId>,
    category: DataEncodingType,
) -> Result<String, String>

Encode a dataset of observations as a single HCTL formula. The particular formula template is chosen depending on the type of data (attractor data, fixed-points, …).

a) Fixed-point dataset is encoded with a conjunction of “steady-state formulas” (see mk_formula_fixed_point_list) that ensures each observation correspond to a fixed point. b) Attractor dataset is encoded with a conjunction of “attractor formulas” (see mk_formula_attractor_list) that ensures each observation correspond to an attractor. c) Trap-space dataset is encoded with a conjunction of “trap-space formulas” (see mk_formula_trap_space_list) that ensures each observation correspond to a trap space. d) Time-series dataset is encoded with a “reachability chain” formula, (see mk_formula_reachability_chain) ensuring there is path between each consecutive observations.