Skip to content

Commit

Permalink
feat: something works
Browse files Browse the repository at this point in the history
  • Loading branch information
Lukáš Chudíček committed Oct 25, 2023
1 parent 40725a0 commit f4c7222
Show file tree
Hide file tree
Showing 4 changed files with 340 additions and 17 deletions.
63 changes: 63 additions & 0 deletions data/manual/basic_transition.sbml
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,63 @@
<?xml version='1.0' encoding='UTF-8' standalone='no'?>
<!-- basis system of one entity;
the entity only has two states - 0 & 1
the only transition is from 0 to 1 (condition being true)
so for states tarting in the {(0)} set of states, the successors shall be {(1)}
for states starting in the {(1)} set of states, the successors shall be {(1)}
for the states starting in the {(0), (1)} set of states, the successors shall be {(1)} -->
<sbml xmlns="http://www.sbml.org/sbml/level3/version1/core" layout:required="false" level="3"
qual:required="true" xmlns:layout="http://www.sbml.org/sbml/level3/version1/layout/version1"
version="1" xmlns:qual="http://www.sbml.org/sbml/level3/version1/qual/version1">
<model metaid="_174907b7-8e1c-47f3-9a50-bb8e4c6ebd0d" id="model_id">
<qual:listOfTransitions xmlns:qual="http://www.sbml.org/sbml/level3/version1/qual/version1">
<qual:transition qual:id="the_only_variable">
<qual:listOfInputs>
<qual:input qual:qualitativeSpecies="the_only_variable"
qual:transitionEffect="none"
qual:sign="negative" qual:id="tr_p53_in_2" />
<!-- <qual:input qual:qualitativeSpecies="renamed" qual:transitionEffect="none"
qual:sign="negative" qual:id="tr_p53_in_2" />
<qual:input qual:qualitativeSpecies="renamed" qual:transitionEffect="none"
qual:sign="negative" qual:id="tr_p53_in_2" /> -->
</qual:listOfInputs>
<qual:listOfOutputs>
<qual:output qual:qualitativeSpecies="the_only_variable"
qual:transitionEffect="assignmentLevel"
qual:id="tr_p53_out" />
</qual:listOfOutputs>
<qual:listOfFunctionTerms>
<!-- 255 is the maximum accepted value; limit of u8 -->
<qual:defaultTerm qual:resultLevel="3">
</qual:defaultTerm>
<!-- <qual:functionTerm qual:resultLevel="0">
<math xmlns="http://www.w3.org/1998/Math/MathML">
<apply>
<eq />
<ci> renamed </ci>
<cn type="integer"> 0 </cn>
</apply>
</math>
</qual:functionTerm>
<qual:functionTerm qual:resultLevel="1">
<math xmlns="http://www.w3.org/1998/Math/MathML">
<apply>
<eq />
<ci> renamed </ci>
<cn type="integer"> 1 </cn>
</apply>
</math>
</qual:functionTerm>
<qual:functionTerm qual:resultLevel="2">
<math xmlns="http://www.w3.org/1998/Math/MathML">
<apply>
<eq />
<ci> renamed </ci>
<cn type="integer"> 2 </cn>
</apply>
</math>
</qual:functionTerm> -->
</qual:listOfFunctionTerms>
</qual:transition>
</qual:listOfTransitions>
</model>
</sbml>
31 changes: 31 additions & 0 deletions dot_output.dot
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,31 @@
digraph G {
init__ [label="", style=invis, height=0, width=0];
init__ -> 4;
0 [shape=box, label="0", style=filled, shape=box, height=0.3, width=0.3];
1 [shape=box, label="1", style=filled, shape=box, height=0.3, width=0.3];
2[label="the_only_variable_v3"];
2 -> 1 [style=filled];
2 -> 0 [style=dotted];
3[label="the_only_variable_v2"];
3 -> 2 [style=filled];
3 -> 0 [style=dotted];
4[label="the_only_variable_v1"];
4 -> 3 [style=filled];
4 -> 0 [style=dotted];
}

digraph G {
init__ [label="", style=invis, height=0, width=0];
init__ -> 4;
0 [shape=box, label="0", style=filled, shape=box, height=0.3, width=0.3];
1 [shape=box, label="1", style=filled, shape=box, height=0.3, width=0.3];
2[label="the_only_variable_v3"];
2 -> 1 [style=filled];
2 -> 0 [style=dotted];
3[label="the_only_variable_v2"];
3 -> 2 [style=filled];
3 -> 0 [style=dotted];
4[label="the_only_variable_v1"];
4 -> 3 [style=filled];
4 -> 0 [style=dotted];
}
101 changes: 101 additions & 0 deletions src/prototype/smart_system_update_fn.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -451,6 +451,107 @@ mod tests {
})
}

#[test]
fn test_handmade_basic() {
let (
smart_empty_succs_dot,
smart_whole_succs_dot,
smart_empty_succs_bdd,
smart_whole_succs_bdd,
) = {
let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
std::fs::File::open("data/manual/basic_transition.sbml")
.expect("cannot open the file"),
));

crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list");

let smart_system_update_fn: SmartSystemUpdateFn<UnaryIntegerDomain, u8> =
SmartSystemUpdateFn::try_from_xml(&mut xml)
.expect("cannot load smart system update fn");

println!(
"smart const false: {}",
smart_system_update_fn.get_empty_state_subset()
);
println!(
"smart const true: {}",
smart_system_update_fn.get_whole_state_space_subset()
);

let empty_subset = smart_system_update_fn.get_empty_state_subset();
let whole_subset = smart_system_update_fn.get_whole_state_space_subset();

let empty_succs = smart_system_update_fn
.transition_under_variable("the_only_variable", &empty_subset);
let whole_succs = smart_system_update_fn
.transition_under_variable("the_only_variable", &whole_subset);

let whole_succs =
smart_system_update_fn.transition_under_variable("the_only_variable", &whole_succs);

(
smart_system_update_fn.bdd_to_dot_string(&empty_succs),
smart_system_update_fn.bdd_to_dot_string(&whole_succs),
empty_succs,
whole_succs,
)
};

let (
// force_empty_succs_dot,
force_whole_succs_dot,
// force_empty_succs_bdd,
force_whole_succs_bdd,
) = {
let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
std::fs::File::open("data/manual/basic_transition.sbml")
.expect("cannot open the file"),
));

println!("---force");

crate::find_start_of(&mut xml, "listOfTransitions").expect("cannot find list");

let force_system_update_fn: SystemUpdateFn<UnaryIntegerDomain, u8> =
SystemUpdateFn::try_from_xml(&mut xml).expect("cannot load smart system update fn");

// let empty_subset = force_system_update_fn.get_empty_state_subset();
let whole_subset = force_system_update_fn.get_whole_state_space_subset();

// let empty_succs = force_system_update_fn
// .transition_under_variable("the_only_variable", &empty_subset);
let whole_succs = force_system_update_fn
.transition_under_variable("the_only_variable", &whole_subset);

(
// force_system_update_fn.bdd_to_dot_string(&empty_succs),
force_system_update_fn.bdd_to_dot_string(&whole_succs),
// empty_succs,
whole_succs,
)
};

let the_two_whole = format!("{}\n{}", smart_whole_succs_dot, force_whole_succs_dot);

// write the dot strings to files

println!(
"smart whole is true: {}, is false: {}",
smart_whole_succs_bdd.is_true(),
smart_whole_succs_bdd.is_false()
);
println!(
"force whole is true: {}, is false: {}",
force_whole_succs_bdd.is_true(),
force_whole_succs_bdd.is_false()
);

assert_eq!(smart_whole_succs_dot, force_whole_succs_dot);

std::fs::write("dot_output.dot", the_two_whole).expect("cannot write to file");
}

// #[test]
// fn test_all_bigger_with_debug_xml_reader() {
// std::fs::read_dir("data/faulty")
Expand Down
162 changes: 145 additions & 17 deletions src/prototype/system_update_fn.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -142,38 +142,166 @@ impl<D: SymbolicDomain<u8>> SystemUpdateFn<D, u8> {
domain
.get_all_possible_values(&self.variable_set)
.into_iter()
.fold(const_false, |acc, possible_var_val| {
.fold(const_false.clone(), |acc, possible_var_val| {
let bits_of_the_encoded_value = domain.encode_bits_into_vec(possible_var_val);

println!("possible value {}", possible_var_val);

let vars_and_their_bits = domain
.symbolic_variables()
.into_iter()
.zip(bits_of_the_encoded_value.clone())
.collect::<Vec<_>>();

let const_true = current_state.or(&current_state.not());
let any_where_var_has_target_value = const_true.restrict(&vars_and_their_bits);
// let any_where_var_has_target_value = const_true.restrict(&vars_and_their_bits);
// todo whaaat? ^this is wrong; `restrict` does not do what i thought it should
// let any_where_var_has_target_value = const_true.var_select(variable, value)
let any_where_var_has_target_value = vars_and_their_bits
.iter()
.fold(const_true, |acc, (var, bit)| {
acc.var_select(var.to_owned(), bit.to_owned())
});

let states_capable_of_transitioning_into_given_value = var_upd_fn
// let fold_base = current_state.and(&any_where_var_has_target_value.not());
// let fold_base = current_state.clone();

let vars_and_their_updating_bdds = var_upd_fn
.bit_answering_bdds
.iter()
.map(|(bit_answering_bdd, _)| bit_answering_bdd)
.zip(bits_of_the_encoded_value.iter().cloned())
.fold(
current_state.and(&any_where_var_has_target_value.not()),
|acc, (ith_bit_answering_bdd, ith_expected_bit)| {
if ith_expected_bit {
acc.and(ith_bit_answering_bdd)
} else {
acc.and(&ith_bit_answering_bdd.not())
}
},
);
.map(|(bdd, variable)| (variable, bdd))
.collect::<HashMap<_, _>>();

// must order the bit-answering bdds the way the variables are ordered in the domain
let correctly_ordered_bit_answered_bdds = vars_and_their_bits
.iter()
.map(|(bdd_variable, _)| {
vars_and_their_updating_bdds.get(bdd_variable).unwrap()
})
.collect::<Vec<_>>();

let const_true = current_state.or(&current_state.not());

let states_capable_of_transitioning_into_given_value =
correctly_ordered_bit_answered_bdds
.iter()
.zip(bits_of_the_encoded_value.iter().cloned())
.fold(
const_true,
|acc, (ith_bit_answering_bdd, ith_expected_bit)| {
println!("ith expected bit {}", ith_expected_bit);
println!(
" acc currently: is false: {}, is true: {}",
acc.is_false(),
acc.is_true()
);

let new_acc = if ith_expected_bit {
acc.and(ith_bit_answering_bdd)
} else {
acc.and(&ith_bit_answering_bdd.not())
};

println!(
" ith_bit_answering_bdd is true: {}, is false: {}",
ith_bit_answering_bdd.is_true(),
ith_bit_answering_bdd.is_false()
);

// let new_acc = acc.and(ith_bit_answering_bdd);

println!(
" updated acc: is false: {}, is true: {}",
new_acc.is_false(),
new_acc.is_true()
);

new_acc
},
);

// let states_capable_of_transitioning_into_given_value = var_upd_fn
// .bit_answering_bdds
// .iter()
// .map(|(bit_answering_bdd, _)| bit_answering_bdd)
// .zip(bits_of_the_encoded_value.iter().cloned())
// .fold(
// const_true,
// |acc, (ith_bit_answering_bdd, ith_expected_bit)| {
// println!("ith expected bit {}", ith_expected_bit);
// println!(
// " acc currently: is false: {}, is true: {}",
// acc.is_false(),
// acc.is_true()
// );

// let new_acc = if ith_expected_bit {
// acc.and(ith_bit_answering_bdd)
// } else {
// acc.and(&ith_bit_answering_bdd.not())
// };

// println!(
// " ith_bit_answering_bdd is true: {}",
// ith_bit_answering_bdd.is_true()
// );

// // let new_acc = acc.and(ith_bit_answering_bdd);

// println!(
// " updated acc: is false: {}, is true: {}",
// new_acc.is_false(),
// new_acc.is_true()
// );

// new_acc
// },
// );

println!(
"intermediate_fold: is false: {}, is true: {}",
states_capable_of_transitioning_into_given_value.is_false(),
states_capable_of_transitioning_into_given_value.is_true()
);

println!(
"states_capable_of_transitioning_into_given_value: is false: {}, is true: {}",
states_capable_of_transitioning_into_given_value.is_false(),
states_capable_of_transitioning_into_given_value.is_true()
);

// this restriction should "perform the transition"
let states_transitioned_into_given_value =
let states_forgot_the_value_of_target_sym_var =
states_capable_of_transitioning_into_given_value
.restrict(&vars_and_their_bits[..]);
// .restrict(&vars_and_their_bits[..]);
.exists(
&vars_and_their_bits
.iter()
.cloned()
.map(|(var, _bit)| var)
.collect::<Vec<_>>()[..],
);

println!(
"states_forgot_the_value_of_target_sym_var: is false: {}, is true: {}",
states_forgot_the_value_of_target_sym_var.is_false(),
states_forgot_the_value_of_target_sym_var.is_true()
);

let states_transitioned_into_given_value =
any_where_var_has_target_value.and(&states_forgot_the_value_of_target_sym_var);

println!(
"-+------ any where var has target value: is false: {}, is true: {}",
any_where_var_has_target_value.is_false(),
any_where_var_has_target_value.is_true()
);

println!(
"states_transitioned_into_given_value: is false: {}, is true: {}",
states_transitioned_into_given_value.is_false(),
states_transitioned_into_given_value.is_true()
);

acc.or(&states_transitioned_into_given_value)
})
Expand Down

0 comments on commit f4c7222

Please sign in to comment.