== Model Builder ==
This page describes the procedures of building a model.

* Input: an AST such that
 * all concurrency dialect features are translated using CIVL-C primitives/libraries;
 * side effects are only contained by assignment or function call;
 * all unused code (statically) is removed;
 * the main function doesn't take any parameters.

* Output: a CIVL-C model

* Algorithm
 1. translate AST to CIVL-C model
 1.