Models

Once the individual components constituting a model have been modeled, they have to be composed together into a ModelBase instance, which can subsequently be analyzed with S#. Models contain a set of root components that constitute the environment of the analyzed system as well as the actual analyzed system itself. Models can be composed together using arbitrary C# code; how a model is constructed is of no interest to S#.

Declaring S# Models

The model for the [pressure tank case study](Pressure Tank Case Study), for instance, is composed as follows:

// 1
class Model : ModelBase
{
	// 2
	public const int PressureLimit = 60;
	public const int SensorFullPressure = 55;
	public const int SensorEmptyPressure = 0;
	public const int Timeout = 59;

	// 3
	[Root(RootKind.Plant)]
	public Tank Tank { get; } = new Tank();

	// 4
	[Root(RootKind.Controller)]
	public Controller Controller { get; }

	// 5
	public PressureSensor Sensor => Controller.Sensor;
	public Pump Pump => Controller.Pump;
	public Timer Timer => Controller.Timer;

	public Model()
	{
		// 6
		Controller = new Controller
		{
			Sensor = new PressureSensor(),
			Pump = new Pump(),
			Timer = new Timer()
		};

		// 7
		Bind(nameof(Sensor.PhysicalPressure), nameof(Tank.PressureLevel));
		Bind(nameof(Tank.IsBeingFilled), nameof(Pump.IsEnabled));
	}
}

1. S# models are classes derived from ModelBase. They are assumed to have a specific structure (explained below), but are otherwise free to contain arbitrary C# code. In particular, they can flexibly compose together different variants of a model. For the pressure tank case study, however, there is only one variant that is of interest; consequently, there is no complicated model initialization logic.

2. Models often define a set of constant values that parameterize certain aspects of the model's components. This is not always possible, however, namely when different variants of a model make use of different constant values. In that case, the model has to pass the constants via constructors to its components, for example.

3. A property is declared that stores the model's Tank instance. Note how in idiomatic C# and S#, properties are often named the same as their types. The declaration is a getter-only auto property that is inline-initialized with a new Tank instance. Every call to the property therefore returns the Tank instance automatically created during the construction of the Model instance.

The Tank property is marked with the [Root(RootKind.Plant)] attribute; the attribute can be applied to properties and fields of an IComponent-implementing type as well as parameterless methods returning an IComponent-implementing type. The attribute indicates to the S# runtime that the instance stored in the Tank property is part of the analyzed system's [plant](Systematic Modeling of Safety-Critical Systems).

4. A property is declared that stores the model's Controller instance. No new instance is instantiated inline; instead, there is a constructor defined below that initializes the property. All reads of the property return the instance set in the constructor.

The Controller property is marked with the [Root(RootKind.Controller)] attribute. The attribute indicates to the S# runtime that the Controller property contains a component instance that is part of the system to be analyzed.

5. For convenience, the model declares a couple of other properties that allow access to other Component instances used within the model. These shorthands are often useful to make simulation- or model checking-based analyses more readable but are otherwise not required.

The properties are getter-only properties implemented with expression bodies using C#'s => syntactic shorthand. Whenever such a property is read, the expression to the right of => is evaluated and the generated value is returned. For the Sensor property, for instance, the PressureSensor instance stored in the Controller property's Sensor property is returned.

6. In the model's constructor, the Controller property is initialized using C#'s object initialization syntax. As the case study is pretty simple, the model only initializes the controller's component references to the pump, timer, and sensor. If more complex model initialization logic is required, the constructor could have parameters that somehow affect model initialization, make use of helper methods, connect to a database to read model configuration parameters, use dependency injection, etc.

7. The port bindings are established between the tank and the senor as well as between the tank and the pump.

Using S# Models

When a ModelBase instance is passed to S# for analysis, the root components are automatically determined based on the model's properties, fields, and methods marked with the Root attribute. Root components marked with Role.Plant are always executed before roots marked with Role.Controller during analyses. Be sure to familiarize yourself with S#'s [model life-cycle](Model Life-Cycle) before attempting to analyze a model using simulations, general [model checking](Model Checking), or fully automated [safety analyses](Safety Analysis).

The ModelBase class defines a couple of helper properties and methods that are often useful when analyzing a model:

• ModelBase.Roots returns all IComponent instances that constitute the model's roots. For instance, the property would return the Controller and Tank instances of the pressure tank model.

• ModelBase.Components returns all IComponent instances the model consists of. These always include the roots, obviously, and all transitively referenced components. For the pressure tank case study, the controller, tank, timer, pressure sensor, and pump components would be returned.

• ModelBase.Faults returns all Fault instances referenced by the model. This is especially useful to disable or enforce certain fault activations during analyses. The property would return the four faults declared by the components of the pressure tank case study, for example.

• ModelBase.VisitPreOrder(Action<IComponent> action) executes action for all IComponent instances referenced by the model in pre-order, while ModelBase.VisitPostOrder(Action<IComponent> action) executes action for all IComponent instances referenced by the model in post-order.