extract model to its own namespace
call knossos.core/analysis rather than linearizations

analysis can tell us directly whether the history is valid or not,
rather than having to infer using not-empty
Prove that model works sequentially

This also shows that you can use the same model to check behaviour in
sequence, and then use the same model in parallel FOR FREE!!!!1