Skip to content

Commit

Permalink
docs: some todos i do not want to do now
Browse files Browse the repository at this point in the history
  • Loading branch information
Lukáš Chudíček committed Dec 9, 2023
1 parent 641f56b commit 7380387
Showing 1 changed file with 42 additions and 1 deletion.
43 changes: 42 additions & 1 deletion src/update/update_fn.rs
Original file line number Diff line number Diff line change
Expand Up @@ -388,7 +388,6 @@ where
})
.collect::<Vec<_>>();

// todo not each variable has transition function (namely primed ones do not have)
let variables_transition_relation_and_domain = named_symbolic_domains
.into_iter()
.zip(relations)
Expand Down Expand Up @@ -440,6 +439,26 @@ where
})
}

/// Like `successors_async`, but a state that "transitions" to itself under
/// given transition variable is not considered to be a proper successor,
/// therefore is not included in the result (unless it is a proper successor
/// of another state from `source_states`).
pub fn successors_async_exclude_loops(
&self,
_transition_variable_name: &str,
_source_states: &Bdd,
) -> Bdd {
// todo better to directly construct the specific no_loop_transition_bdd during construction
// todo probably have some common, underlying method that would accept the transition bdd
// todo the two public methods would then just pass in the proper transition bdd
// self.successors_async(
// transition_variable_name,
// &source_states
// .and(&self.those_states_capable_of_transitioning_under(transition_variable_name)),
// )
todo!()
}

pub fn predecessors_async(
&self,
transition_variable_name: &str,
Expand Down Expand Up @@ -468,13 +487,35 @@ where
source_states_transition_relation.exists(primed_domain.raw_bdd_variables().as_slice())
}

/// Like `predecessors_async`, but a state that "transitions" to itself under
/// given transition variable is not considered to be a proper predecessor,
/// therefore is not included in the result (unless it is a proper predecessor
/// of another state from `source_states`).
pub fn predecessors_async_exclude_loops(
&self,
_transition_variable_name: &str, // todo naming of those
_source_states: &Bdd,
) -> Bdd {
// todo better to directly construct the specific no_loop_transition_bdd during construction
// todo probably have some common, underlying method that would accept the transition bdd
// todo the two public methods would then just pass in the proper transition bdd
// self.predecessors_async(transition_variable_name, source_states)
// .and(&self.those_states_capable_of_transitioning_under(transition_variable_name))
todo!()
}

fn get_transition_relation_and_domain(&self, variable_name: &str) -> Option<&VarInfo<DO, T>> {
// todo optimize using the hashtable mapper
self.variables_transition_relation_and_domain
.iter()
.find(|(maybe_variable_name, _)| maybe_variable_name == variable_name)
.map(|(_, update_fn_and_domain)| update_fn_and_domain)
}

fn those_states_capable_of_transitioning_under(&self, _variable_name: &str) -> Bdd {
// todo this should be stored in a field; built during construction
todo!()
}
}

fn find_bdd_variables_prime<D, T>(
Expand Down

0 comments on commit 7380387

Please sign in to comment.