Automated model extraction from non-deterministic c-code to active objects (for-reviewers only)

We provide here some material for the reviewers: