Struct biodivine_sketchbook::inference::inference_solver::InferenceSolver

pub struct InferenceSolver {
    bn: Option<BooleanNetwork>,
    graph: Option<SymbolicAsyncGraph>,
    start_time: Option<SystemTime>,
    static_props: Option<Vec<ProcessedStatProp>>,
    dynamic_props: Option<Vec<ProcessedDynProp>>,
    raw_sat_colors: Option<GraphColors>,
    status_updates: Vec<InferenceStatusReport>,
    should_stop: Arc<AtomicBool>,
    sender_channel: Sender<String>,
    results: Option<InferenceResults>,
    error_message: Option<String>,
}

Object encompassing the process of the BN inference computation.

It tracks the intermediate results and low-level structures, and it provides hooks to the actual algorithms.

By tracking the intermediate results, we may be able to observe the computation, and potentially “fork” or re-use parts of the computation in future. The computation is made to be run asynchronously itself on a special thread, and the solver reports on progress via a special channel.

Fields

bn: Option<BooleanNetwork>

Boolean Network instance (once processed).

graph: Option<SymbolicAsyncGraph>

Symbolic transition graph for the system. Its set of unit colors is gradually updated during computation, and it consists of currently remaining valid candidate colors.

start_time: Option<SystemTime>

Start time of the computation (once started).

static_props: Option<Vec<ProcessedStatProp>>

Static properties (once processed).

dynamic_props: Option<Vec<ProcessedDynProp>>

Dynamic properties (once processed).

raw_sat_colors: Option<GraphColors>

Set of final satisfying colors ((if computation finishes successfully).

status_updates: Vec<InferenceStatusReport>

Vector with all time-stamped status updates. The last is the latest status.

should_stop: Arc<AtomicBool>

Flag to signal cancellation.

sender_channel: Sender<String>

Channel to send updates regarding the computation.

results: Option<InferenceResults>

Potential processed results (if computation finishes successfully).

error_message: Option<String>

Potential error message (if computation finishes with error).

Implementations

impl InferenceSolver

Basic utilities, constructors, getters, and so on.

pub fn new(sender_channel: Sender<String>) -> InferenceSolver

Prepares new “empty” InferenceSolver instance that can be later used to run the computation.

Currently, the computation can be started by the run_inference_async method.

pub fn bn(&self) -> Result<&BooleanNetwork, String>

Reference getter for a Boolean network.

pub fn graph(&self) -> Result<&SymbolicAsyncGraph, String>

Reference getter for a transition graph.

pub fn stat_props(&self) -> Result<&Vec<ProcessedStatProp>, String>

Reference getter for a vector of formulas for static properties.

pub fn dyn_props(&self) -> Result<&Vec<ProcessedDynProp>, String>

Reference getter for a vector of formulas for dynamic properties.

pub fn final_sat_colors(&self) -> Result<&GraphColors, String>

Reference getter for a set of satisfying graph colors.

pub fn current_candidate_colors(&self) -> Result<GraphColors, String>

Get a current set of valid candidate colors. This can be used to get intermediate results and is gradually updated during computation.

pub fn start_time(&self) -> Result<SystemTime, String>

Get a start time of the actual computation.

pub fn total_duration(&self) -> Result<Duration, String>

Get a total duration of the actual inference computation.

fn update_status(&mut self, status: InferenceStatus)

Update the status of the solver, and send a progress message to the InferenceState instance (that started this solver).

If the channel for progress updates no longer exists (because inference is supposed to be reset, the window was closed, or some other reason), we instead forcibly stop the computation. Destroying the channel can thus actually be used as another way to stop the asynchronous computation, since one does not need to acquire lock over the whole solver.

fn format_status_message( &self, status: &InferenceStatus, comp_time: u128, num_candidates: Option<u128>, ) -> String

Format a computation status message.

fn check_cancellation(&self) -> Result<(), String>

Utility to check whether the cancellation flag was set. If it is set, the function returns error. Otherwise, nothing happens.

fn check_if_finished_unsat( &mut self, update_status: bool, ) -> Result<bool, String>

Utility to check whether the sketch (during computation) is already found to be unsatisfiable.

If arg `update_status`` is true and sketch is unsat, the status is update with InferenceStatus::DetectedUnsat.

This method only makes sense when the computation is already on the way.

pub fn to_finished_solver(&self) -> Result<FinishedInferenceSolver, String>

If computation successfully finished, transform into FinishedInferenceSolver. Otherwise, return the error with the error message that caused inference fail.

pub fn is_finished(&self) -> bool

Check if computation finished (by success or error).

pub fn num_finished_dyn_props(&self) -> u64

Number of dynamic properties that were already successfully evaluated.

pub fn num_finished_stat_props(&self) -> u64

Number of static properties that were already successfully evaluated.

impl InferenceSolver

Methods for asynchronous manipulation of InferenceSolver (starting/cancelling inference).

pub async fn run_inference_async( solver: Arc<RwLock<InferenceSolver>>, sketch: Sketch, inference_type: InferenceType, ) -> Result<InferenceResults, String>

Run the prototype version of the inference using the given solver. This wraps the Self::run_inference_modular to also log potential errors.

The argument inference_type specifies which kind of inference should be used. Currently, we support full inference with all properties, and partial inferences with only static or only dynamic properties.

The results are saved to specific fields of the provided solver and can be retrieved later. They are also returned, which is now used for logging later.

pub fn cancel(&self)

Set the cancellation flag. The actual cancellation does not happen immediately, we currently only allow cancelling only at certain checkpoints during computation.

impl InferenceSolver

Methods related to actual inference computation.

fn extract_bn(sketch: &Sketch) -> Result<BooleanNetwork, String>

Extract and process BN component from the sketch.

fn eval_static(&mut self, base_var_name: &str) -> Result<(), String>

Evaluate previously collected static properties, and restrict the unit set of the graph to the set of valid colors.

If we discover that sketch is unsat early, skip the rest.

fn eval_dynamic(&mut self) -> Result<(), String>

Evaluate previously collected dynamic properties, and restrict the unit set of the graph to the set of valid colors.

If we discover that sketch is unsat early, skip the rest.

pub fn run_inference_modular( &mut self, inference_type: InferenceType, sketch: Sketch, use_static: bool, use_dynamic: bool, ) -> Result<InferenceResults, String>

A modular variant of the inference. You can choose which parts to select. For example, you can only consider static properties, only dynamic properties, or all.