Module biodivine_sketchbook::algorithms::eval_dynamic::_attractors::itgr

Interleaved transition guided reduction quickly eliminates most non-attractor states. Interleaved transition guided reduction algorithm.

Implements interleaved transition guided reduction. This technique does not remove all non-attractor states, but can very significantly prune the state space in a very reasonable amount of time.

Modules

• _impl_extended_component_process 🔒
• _impl_fwd_bwd_process 🔒
• _impl_reachable_process 🔒
• _impl_scheduler 🔒

Structs

• BwdProcess 🔒
  (internal) Basic backward reachability process.
• ExtendedComponentProcess 🔒
  (internal) Computes the extended component of a forward-reachable set.
• FwdProcess 🔒
  (internal) Basic forward reachability process.
• ReachableProcess 🔒
  (internal) Computes the set of vertices reachable from states that can perform var_post.
• Scheduler 🔒
  (internal) Scheduler manages work divided into Processes. It keeps a universe of unprocessed vertices and a list of remaining active variables.

Traits

• Process 🔒
  (internal) A process trait is a unit of work that is managed by a Scheduler. Process has a weight that approximates how symbolically hard is to work with its intermediate representation.

Functions

• interleaved_transition_guided_reduction
  Removes from initial as many non-attractor states as possible using interleaved transition guided reduction.