Declarative language for dynamical properties

Declarative language for dynamical properties#

In the scope of a BoNesis(dom, data) object, the following methods are defined.

maps a subset of components to a Boolean value

`O = obs({a:0, b:1,..})`	Observation from partial mapping of components to `0` or `1` (`dict`-like object)
`O = obs("name")`	`data` dictionary

maps each component to a Boolean value

`C = cfg()`	Allocates a fresh configuration
`C = +O`	Fresh configuration matching with the observation `O`
`C = ~O`	Default configuration matching with the observation `O`

S = Some(max_size=k) Represents a mutation of at most k components.
Use S.assignments() to get satisfying valuations.

`C != C'`	The configurations `C` and `C'` differ on at least one component
`C[a] == C'[b] \| 0 \| 1`	The state of the component `a` in the configuration `C` is equal (resp. different) to the state of the component `b` in the configuration `C'` (resp. 0 and 1)
`C[a] != C'[b] \| 0 \| 1`
`C != O`	The configuration `C` does not match with the observation `O`

`fixed(C)`	The configuration `C` is a fixed point
`fixed(O)`	There exists a trap space where observation `O` is fixed
`in_attractor(C)`	The configuration `C` belongs to an attractor

`C >= C'` or `reach(C,C')`	There exists an MP trajectory from the configuration `C` to the configuration `C'`
`C >= O`	... to a configuration matching with the observation `O` (equiv to `C >= +O`)
`C >= fixed(O)`	... to a configuration in a trap space where the observation `O` is fixed
Note: can be composed, e.g., `C1 >= C2 >= fixed(C3)`
`C / _` or `nonreach(C, _)`	Absence of MP trajectory from the configuration `C` to ... (same as reach)

`all_fixpoints({O,O',..})`	All the fixed points match with at least one given observation
`C >> "fixpoints" ^ {O,O',..}`	All the fixed points reachable from the configuration `C` ...

with mutant({a:0,..} | S):
... The properties within the with block are subject to mutation specified by {a:0,..} (resp. S)

`maximize_nodes()`	Maximize the number of nodes in the Boolean network (to be used in conjunction with option `allow_skipping_nodes=True` of `InfluenceGraph`)
`maximize_constants()`	Maximize the number of nodes having a constant Boolean function
`maximize_strong_constants()`	Maximize the number of nodes having a constant Boolean function and being assigned to this constant in all defined configurations.