This type represents the state of the model at any point of the execution. Is the union of the
`dynamic_state()` and `symbolic_state`.