1
- use crate :: symbolic_async_graph:: SymbolicContext ;
1
+ use crate :: symbolic_async_graph:: { RegulationConstraint , SymbolicContext } ;
2
2
use crate :: Monotonicity :: Inhibition ;
3
3
use crate :: {
4
4
BooleanNetwork , FnUpdate , Monotonicity , Parameter , ParameterId , ParameterIdIterator ,
5
- RegulatoryGraph , Variable , VariableId , VariableIdIterator , ID_REGEX ,
5
+ Regulation , RegulatoryGraph , Variable , VariableId , VariableIdIterator , ID_REGEX ,
6
6
} ;
7
- use biodivine_lib_bdd:: bdd;
8
7
use std:: collections:: { HashMap , HashSet } ;
9
8
use std:: ops:: Index ;
10
9
use std:: path:: Path ;
@@ -271,21 +270,28 @@ impl BooleanNetwork {
271
270
}
272
271
273
272
impl BooleanNetwork {
274
- /// Infer a regulatory graph based on the update functions of this `BooleanNetwork`.
273
+ /// Infer a *sufficient* regulatory graph based on the update functions of
274
+ /// this `BooleanNetwork`.
275
275
///
276
276
/// The resulting graph is solely based on the information that can be inferred from the
277
277
/// update functions. In particular, if the BN contains uninterpreted functions,
278
278
/// the monotonicity of variables appearing within these functions is unknown. Overall,
279
- /// this method is typically only useful for fully specified networks with minor errors
279
+ /// the method is typically only useful for fully specified networks with minor errors
280
280
/// in the regulatory graph.
281
281
///
282
282
/// The BN still has to satisfy basic integrity constraints. In particular, every uninterpreted
283
283
/// function must be used, and must be used consistently (i.e. correct arity). Also, every
284
284
/// update function may only use variables declared as regulators. Otherwise, an error
285
285
/// is returned.
286
+ ///
287
+ /// The method can also fail if a non-observable regulator is removed from a partially
288
+ /// specified function, because in such case we cannot always transform the function
289
+ /// in a way that is valid.
286
290
pub fn infer_valid_graph ( & self ) -> Result < BooleanNetwork , String > {
287
291
let ctx = SymbolicContext :: new ( self ) ?;
288
292
293
+ // This should ensure the variable IDs in the old and the new network are compatible,
294
+ // so that we can reuse Regulation and FnUpdate objects.
289
295
let var_names = self
290
296
. variables ( )
291
297
. map ( |id| self . get_variable_name ( id) )
@@ -294,88 +300,68 @@ impl BooleanNetwork {
294
300
295
301
let mut new_rg = RegulatoryGraph :: new ( var_names) ;
296
302
for target_var in self . variables ( ) {
297
- let target_name = self . get_variable_name ( target_var) ;
298
303
if let Some ( function) = self . get_update_function ( target_var) {
299
- // If the update function exists, compute a BDD which describes all satisfying
300
- // inputs to that function, and then infer function properties from this BDD.
301
304
let fn_is_true = ctx. mk_fn_update_true ( function) ;
302
- let fn_is_false = fn_is_true. not ( ) ;
303
-
304
- // All non-trivial code is explained in `impl_regulation_constraint`.
305
-
306
305
for regulator_var in self . as_graph ( ) . regulators ( target_var) {
307
- let regulator_name = self . get_variable_name ( regulator_var) ;
308
-
309
- let regulator = ctx. state_variables ( ) [ regulator_var. 0 ] ;
310
- let regulator_is_true = ctx. bdd_variable_set ( ) . mk_var ( regulator) ;
311
- let regulator_is_false = ctx. bdd_variable_set ( ) . mk_not_var ( regulator) ;
312
-
313
- let observability = {
314
- let fn_x1_to_1 = bdd ! ( fn_is_true & regulator_is_true) . var_exists ( regulator) ;
315
- let fn_x0_to_1 =
316
- bdd ! ( fn_is_true & regulator_is_false) . var_exists ( regulator) ;
317
- bdd ! ( fn_x1_to_1 ^ fn_x0_to_1) . exists ( ctx. state_variables ( ) )
306
+ let Some ( regulation) = RegulationConstraint :: infer_sufficient_regulation (
307
+ & ctx,
308
+ regulator_var,
309
+ target_var,
310
+ & fn_is_true,
311
+ ) else {
312
+ continue ;
318
313
} ;
319
314
320
- if !observability. is_false ( ) {
321
- let activation = {
322
- let fn_x1_to_0 =
323
- bdd ! ( fn_is_false & regulator_is_true) . var_exists ( regulator) ;
324
- let fn_x0_to_1 =
325
- bdd ! ( fn_is_true & regulator_is_false) . var_exists ( regulator) ;
326
- bdd ! ( fn_x0_to_1 & fn_x1_to_0) . exists ( ctx. state_variables ( ) )
327
- }
328
- . not ( ) ;
329
-
330
- let inhibition = {
331
- let fn_x0_to_0 =
332
- bdd ! ( fn_is_false & regulator_is_false) . var_exists ( regulator) ;
333
- let fn_x1_to_1 =
334
- bdd ! ( fn_is_true & regulator_is_true) . var_exists ( regulator) ;
335
- bdd ! ( fn_x0_to_0 & fn_x1_to_1) . exists ( ctx. state_variables ( ) )
336
- }
337
- . not ( ) ;
338
-
339
- let monotonicity = match ( activation. is_false ( ) , inhibition. is_false ( ) ) {
340
- ( false , true ) => Some ( Activation ) ,
341
- ( true , false ) => Some ( Inhibition ) ,
342
- _ => None ,
343
- } ;
344
-
345
- new_rg
346
- . add_regulation ( regulator_name, target_name, true , monotonicity)
347
- . unwrap ( ) ;
348
- }
315
+ new_rg. add_raw_regulation ( regulation) . unwrap ( ) ;
349
316
}
350
317
} else {
351
318
// If the update function is missing, just copy the existing regulators, but
352
319
// remove any monotonicity/observability.
353
- for regulator in self . as_graph ( ) . regulators ( target_var) {
354
- let regulator_name = self . get_variable_name ( regulator) ;
320
+ for regulator_var in self . as_graph ( ) . regulators ( target_var) {
355
321
new_rg
356
- . add_regulation ( regulator_name, target_name, false , None )
322
+ . add_raw_regulation ( Regulation {
323
+ regulator : regulator_var,
324
+ target : target_var,
325
+ observable : false ,
326
+ monotonicity : None ,
327
+ } )
357
328
. unwrap ( ) ;
358
329
}
359
330
}
360
331
}
361
332
362
333
let mut new_bn = BooleanNetwork :: new ( new_rg) ;
334
+
335
+ // Copy over existing parameters
336
+ for parameter_id in self . parameters ( ) {
337
+ let parameter = & self [ parameter_id] ;
338
+ new_bn
339
+ . add_parameter ( & parameter. name , parameter. arity )
340
+ . unwrap ( ) ;
341
+ }
342
+
363
343
for var in self . variables ( ) {
364
344
let name = self . get_variable_name ( var) ;
365
345
if let Some ( update) = self . get_update_function ( var) {
366
- // We first try to just copy the function. If there are no non-observable
367
- // variables this should work. If there is an error, we have to copy the
368
- // function using a string translation.
369
- if new_bn
370
- . set_update_function ( var, Some ( update. clone ( ) ) )
371
- . is_err ( )
372
- {
373
- let fn_bdd = ctx. mk_fn_update_true ( update) ;
374
- let fn_string = fn_bdd
375
- . to_boolean_expression ( ctx. bdd_variable_set ( ) )
376
- . to_string ( ) ;
377
- new_bn. add_string_update_function ( name, & fn_string) . unwrap ( ) ;
378
- }
346
+ // At the moment, there is no way to "fix" the function in a way that
347
+ // works with logical parameters if one of the arguments is non-observable.
348
+ // As such, we first try to copy the function with no change. then we try to
349
+ // run it through a string translation, but this only works on functions without
350
+ // parameters. If this fails, the conversion fails.
351
+ let Err ( _) = new_bn. set_update_function ( var, Some ( update. clone ( ) ) ) else {
352
+ continue ;
353
+ } ;
354
+ let fn_bdd = ctx. mk_fn_update_true ( update) ;
355
+ let fn_string = fn_bdd
356
+ . to_boolean_expression ( ctx. bdd_variable_set ( ) )
357
+ . to_string ( ) ;
358
+ let Err ( _) = new_bn. add_string_update_function ( name, & fn_string) else {
359
+ continue ;
360
+ } ;
361
+ return Err ( format ! (
362
+ "Cannot translate function for variable {} due to elimianted arguments." ,
363
+ name
364
+ ) ) ;
379
365
}
380
366
}
381
367
@@ -768,6 +754,38 @@ mod test {
768
754
assert_eq ! ( expected. as_graph( ) , inferred. as_graph( ) ) ;
769
755
}
770
756
757
+ #[ test]
758
+ fn test_rg_inference_with_parameters ( ) {
759
+ let bn = BooleanNetwork :: try_from (
760
+ r"
761
+ a -> c
762
+ b -| c
763
+ $c: f(a, b)
764
+ " ,
765
+ )
766
+ . unwrap ( ) ;
767
+ let expected = BooleanNetwork :: try_from (
768
+ r"
769
+ a -?? c
770
+ b -?? c
771
+ $c: f(a, b)
772
+ " ,
773
+ )
774
+ . unwrap ( ) ;
775
+
776
+ assert_eq ! ( expected, bn. infer_valid_graph( ) . unwrap( ) ) ;
777
+
778
+ let invalid = BooleanNetwork :: try_from (
779
+ r"
780
+ a -> c
781
+ b -| c
782
+ $c: b & x & (a | !a)
783
+ " ,
784
+ )
785
+ . unwrap ( ) ;
786
+ assert ! ( invalid. infer_valid_graph( ) . is_err( ) ) ;
787
+ }
788
+
771
789
#[ test]
772
790
fn test_input_inlining ( ) {
773
791
let bn = BooleanNetwork :: try_from (
0 commit comments