To analyze S# models, it is important to understand S#'s model life-cycle. Otherwise, it might be a bit confusing as to what is going on and what C# and S# language features are allowed to be used in which situations. The following table gives a brief overview of the different life-cycle phases and what happens during each of them; detailed descriptions follow below.

Phase	Step	Conducted By	Remarks
Design Time	Model Editing	Modeler	Specification of model element types and model instantiations in a S# project. Basically, S#-enriched C# code is written to model a safety-critical system and any required infrastructure code.
Build Time	Diagnostics	S# Analyzers, C# Compiler	The S# project is checked for syntactic and semantic errors that violate any S# or C# rules.
Build Time	Normalization	S# Normalizers	S#-specific model fragments contained in the S# project are transformed to regular C# code.
Build Time	Compilation	C# Compiler	The S# project is compiled with the standard C# compiler to produce an executable .NET assembly.
Run Time	Model Initialization	User Code	A S# ModelBase instance is initialized in some arbirary way that is of no interest to S#; Component constructors are executed. No nondeterminism is supported.
Run Time	Model Copying	S# Runtime	A deep copy of the ModelBase instance is made. Caution: The next steps work on the copy, leaving the original instance unmodified.
Run Time	Model Execution - Initial States	S# Runtime	Initial states of the model copy are computed. Nondeterminism is supported.
Run Time	Model Execution - Model Steps	S# Runtime	The Update methods of the Component instances contained in the model copy are executed multiple times. Nondeterminism is supported.
Run Time	Clean-Up	.NET Garbage Collector	The model copy is cleaned-up and garbage collected.

During the design time phase, the modeler modifies the C# code constituting the S# model and all supporting infrastructure code. The latter might, for example, instantiate models and execute test cases.

S# models must be valid C# code; they must also satisfy all additional syntactic and semantic constraints imposed on them by S# such as not using certain unsupported language features or incompatible .NET libraries. For instance, S# models should not use random numbers or multi-threaded execution.

While infrastructure code must also be valid C# code, it can use all C# language features and all .NET libraries; it is simply executed to instantiate models and to start up simulations and model checking-based analyses; the code is otherwise of no interest to S#.

Like all C# programs, S# models must be compiled to a .NET assembly before they can be executed, that is, before they can be simulated or model checked. S# extends the usual C# build process, adding two additional steps before the default compilation step. S#'s build process is fully integrated into MSBuild and Visual Studio, requiring no manual user interaction.

S# comes with a set of analyzers that are injected into Visual Studio and the build process. At design time, the analyzers provide immediate diagnostics (i.e., warnings and errors) for any syntactical or semantical issues that are found in the model. At build time, these analyzers are also executed to ensure that no invalid models enter the normalization step of the build process.

S# provides a set of code normalizers that normalize certain S#-specific constructs into regular, executable C# code. Normalizers transform the original model code for fault effects, state machines, and required ports, among others, into semantically equivalent C# code.

There are two reasons for these transformations: The transformations might either be required to implement the intended S# semantics, or they rewrite code to make its execution more efficient; the latter is of high importance for model checking, where the same line of code is potentially executed millions of times, if not more.

The normalized code is finally passed to the standard C# compiler for compilation into a .NET assembly.

At run time, a model is instantiated and executed for simulation or model checking purposes. The run time phase is divided into multiple separate steps:

During the model initialization step, arbitrary C# code is executed that does not interact with S# other than by instantiating Component instances and a ModelBase instance. Constructors of the Component instances are executed. The

Caution: Nondeterminism via any of the Choose functions is not supported at this stage.

When the ModelBase instance is passed to a S# model checker or a S# simulator, a copy of the model is made. The original instance is neither modified nor used by the simulator or model checker. In fact, S# does not even hold on to a reference to the original model in any way. The underlying reasons is that model checkers by default use all available CPU cores to check a model; each core gets its own copy, avoiding any synchronization overhead between the individual cores while executing model code.

While model checking, the ModelBase copy is not accessible until a counter example is generated. For simulations, the copy can be retrieved from the simulator, allowing visualizations, for instance, to visualize the model state during simulation.

The ModelBase copy is a deep copy of the original model, copying the entire object graph of all .NET objects reachable from the original ModelBase instance. Not all .NET types can be copied; generally, primitive types such as int and bool as well as standard types like arrays and delegates are copyable. S# components and other .NET classes such as List<T> that make use of only these types are also copyable. The data of all objects is copied over; no constructors are run on the copies.

Caution: Once the copy is made, all changes to the original model obviously do not affect the copies. It is not possible to reference any newly allocated objects from the copies.

The ModelBase copy is executed either by a simulator or by a model checker. There are two steps involved:

Model execution starts by computing the initial states of the model; simulations compute only one such state, whereas model checkers compute all initial states. In the simplest case, there is only one initial state, namely the state of all objects directly after copying.

If an object wants to execute custom, possibly nondeterministic code to determine its initial states, it has to implement the IInitializable interface: The S# runtime calls the IInitializable.Initialize() method on all objects in the model copy that implement that interface. In particular, Component implements IInitializable and provides the virtual Component.Initialize() method for convenience. Component must therefore simply override Component.Initialize() to participate in the initial state computation.

Note: The family of nondeterministic Choose functions can be used during initial states computation.

Caution: Note that no port bindings should ever be established in Component.Initialize() as only one copy will see the new bindings when model checking.

Once the initial state(s) are known, simulations repeatedly compute one successor state. Model checkers, by contrast, always compute all successor states that exist. There might be multiple successors when the family of nondeterministic Choose functions is used or faults are activated. For simulations, model stepping continues until the simulation is stopped. When model checking, on the other hand, model stepping is aborted as soon as all reachable states are discovered or a violation of the analyzed formula is detected.

Once model execution is completed, i.e., the simulation is aborted or model checking is terminated, the ModelBase copies are eventually cleaned up by .NET's garbage collector.

Even though rarely used, custom clean-up is also supported, where objects are allowed to execute some code before being garbage collected. To do so, the objects the model copies consist of can implement .NET's standard Dispose Pattern. Note that the S# runtime does not call the Dispose methods of the objects contained in the original version of the analyzed model; S# does not keep any reference to original models after model copying.