sybila/biodivine-lib-param-bn

Create "network inclusion test"

Closed this issue · 1 comments

Given two networks with the same variables, it would be good to have a test that checks whether one network is more specific/more general. In particular, this could be used to test if a specific (user provided) witness network is part of a larger coloured collection.

In other words, the API should be able available in a SymbolicAsyncGraph (or more likely in the SymbolicContext). It should take the "smaller" Boolean network directly and compute a subset of the current parameter space that only admits the dynamics in the "smaller" network.

In many instances, the networks could be deemed as semantically incompatible. This should be indicated in some other way than returning an empty set. In particular, networks can be incompatible when:

  • They use different variables.
  • The "smaller" network uses different/additional parameters.
  • They use different regulations with different static properties.

Technically, this may not always be necessary for non-essential regulations. But for simplicity, we disregard this for now, as one can easily add the missing non-essential regulations to both networks without modifying the update functions. However, it is a possible topic for further discussion as to how "BN inclusion" should be tested.

In general, testing network "inclusion" is hard, and for now we do not attempt a full semantic check across the whole range of possible networks. Instead, the smaller network must always be "more specific" in that it does not use new parameters and the update functions can be syntactically mapped to the update functions of the larger network (i.e., an uninterpreted function can be replaced with an interpretation, but there can't be any changes to the existing fixed functions or introduction of new uninterpreted functions).

So far, this is resolved in e3842d264edb56270346e0bd821906319d0d3b4a. However, the implementation is rather simplistic. Further improvements could be made to make the operation more useful.