Module biodivine_sketchbook::algorithms::eval_dynamic::encode

Encode data and template properties into HCTL.

Functions

• encode_dataset_hctl_str
  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, …).
• encode_multiple_observations_str 🔒
  Encode several observation vectors with conjunction formulae, one by one. Also see encode_observation_str for details.
• encode_observation_str 🔒
  Encode binarized observation with a formula depicting the corresponding state/sub-space. Using binarized values and proposition names, creates a conjunction of literals describing that observation.
• mk_formula_attractor
  Create HCTL formula describing that given sub-space (observation) must contain a state that is part of an attractor.
• mk_formula_attractor_list
  Create HCTL formula describing that each sub-space (observation) in a list must contain a state that is part of an attractor. It is essentially a conjunction of “attractor formulas” (see mk_formula_attractor).
• mk_formula_attractor_specific
  Create HCTL formula describing that given specific state is part of an attractor.
• mk_formula_exclusive_attractors
  Create HCTL formula describing that 1) each sub-space (observation) in a list must contain a state that is part of an attractor and 2) prohibits existence of any additional attractor that does not contain a state from some of these sub-spaces.
• mk_formula_exclusive_fixed_points
  Create HCTL formula describing that 1) each sub-space (observation) in a list must contain a steady state and 2) prohibits existence of any additional steady states outside of these sub-spaces.
• mk_formula_fixed_point
  Create HCTL formula describing that given sub-space (observation) must contain a steady state (fixed-point).
• mk_formula_fixed_point_list
  Create HCTL formula describing that each sub-space (observation) in a list must contain a steady state (fixed-point). It is essentially a conjunction of “fixed-point formulas” (see mk_formula_fixed_point).
• mk_formula_fixed_point_specific
  Create HCTL formula describing that given state is a steady state (fixed-point).
• mk_formula_forbid_other_attractors
  Create HCTL formula that prohibits existence of any attractor apart from the ones that contain some states from some of the specified sub-spaces (observations).
• mk_formula_forbid_other_fixed_points
  Create HCTL formula that prohibits existence of any steady state apart from the ones that contained in the specified sub-spaces (observations).
• mk_formula_reachability_chain
  Create a formula describing the existence of path between any states of every two consecutive sub-spaces from the states_sequence, starting with the first one.
• mk_formula_reachability_pair
  Create HCTL formula describing that there is (not) a path between (any) states of two sub-spaces.
• mk_formula_trap_space
  Create a formula describing that a sub-space (observation) is a trap space.
• mk_formula_trap_space_list
  Create a formula describing that each sub-space (observation) in a given list is a trap space. It essentially is a conjunction of “trap-space formulas” (see mk_formula_trap_space).
• try_encode_multiple_observations
  Encode each of the several observations, one by one. For details, see try_encode_observation.
• try_encode_observation
  Encode an observation by a (propositional) formula depicting the corresponding state/sub-space. The observation’s binary values are used to create a conjunction of literals. The var_names are used as propositions names in the formula.