fix: forgot to take current_state (or rather set of current states) i…

…nto account)

dot_output.dot

@@ -1,31 +1,13 @@
 digraph G {
 init__ [label="", style=invis, height=0, width=0];
-init__ -> 4;
+init__ -> 0;
 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;
+init__ -> 0;
 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];
 }

src/prototype/smart_system_update_fn.rs

@@ -499,9 +499,9 @@ mod tests {
         };
 
         let (
-            // force_empty_succs_dot,
+            force_empty_succs_dot,
             force_whole_succs_dot,
-            // force_empty_succs_bdd,
+            force_empty_succs_bdd,
             force_whole_succs_bdd,
         ) = {
             let mut xml = xml::reader::EventReader::new(std::io::BufReader::new(
@@ -516,24 +516,22 @@ mod tests {
             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 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 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(&empty_succs),
                 force_system_update_fn.bdd_to_dot_string(&whole_succs),
-                // empty_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!(
@@ -549,7 +547,13 @@ mod tests {
 
         assert_eq!(smart_whole_succs_dot, force_whole_succs_dot);
 
-        std::fs::write("dot_output.dot", the_two_whole).expect("cannot write to file");
+        assert_eq!(smart_empty_succs_dot, force_empty_succs_dot);
+
+        // let the_two_whole = format!("{}\n{}", smart_whole_succs_dot, force_whole_succs_dot);
+        let the_two_empty = format!("{}\n{}", smart_empty_succs_dot, force_empty_succs_dot);
+
+        // std::fs::write("dot_output.dot", the_two_whole).expect("cannot write to file");
+        std::fs::write("dot_output.dot", the_two_empty).expect("cannot write to file");
     }
 
     // #[test]

src/prototype/system_update_fn.rs

@@ -270,9 +270,12 @@ impl<D: SymbolicDomain<u8>> SystemUpdateFn<D, u8> {
                     states_capable_of_transitioning_into_given_value.is_true()
                 );
 
+                let states_from_current_state_set_capable_of_transitioning_into_given_value =
+                    current_state.and(&states_capable_of_transitioning_into_given_value);
+
                 // this restriction should "perform the transition"
                 let states_forgot_the_value_of_target_sym_var =
-                    states_capable_of_transitioning_into_given_value
+                    states_from_current_state_set_capable_of_transitioning_into_given_value
                         // .restrict(&vars_and_their_bits[..]);
                         .exists(
                             &vars_and_their_bits