Skip to content

Simulations

Axel Habermaier edited this page Mar 8, 2016 · 1 revision

S#'s simulator executes one single path through a S# model; it is therefore non-exhaustive in contrast to [model checking](Model Checking). Simulations are useful for various purposes: Simulation-based model tests, model visualizations, model debugging, and replaying of model checking counter examples.

Be sure to understand S#'s [model life-cycle](Model Life-Cycle) before continuing.

Simulation-Based Model Tests

Simulation-based model tests ensure that the model or certain parts of it exhibit the intended behavior. In the early stages of development, new design ideas can quickly be tested and tried out, even allowing for a test-driven development of the specification of the system. Tests of individual components, groups of components, or the entire system serve as regression tests whenever changes to the model or to the design of the system become necessary. Tests that check the system's modeled response to certain faults or tests that result in the occurrence of a hazard can also be used as templates for (possibly manual) hardware-in-the-loop tests or simulations of the actual system during later stages of the development.

For the [pressure tank running example](Pressure Tank Case Study), for instance, a simulation can be conducted as follows:

// Instantiate a new instance of the pressure tank model.
var model = new Model();

// Suppress the activations of all faults of the model,
// that is, no faults can ever be activated.
model.Faults.SuppressActivations();

// Force the activations of the sensor's 'is full' and the
// timer's 'timeout' faults, that is, S# always tries to
// activate these two faults.
model.Sensor.SuppressIsFull.ForceActivation();
model.Timer.SuppressTimeout.ForceActivation();

// Create a new Simulator instance for the model
var simulator = new Simulator(model);

// Simulate a single step
simulator.SimulateStep();

// Simulate 120 steps
simulator.FastForward(steps: 120);

// Rewind 10 steps
simulator.Rewind(steps: 10);

// Reset the simulator to the initial states
simulator.Reset();

Visualizations

As S# models are regular C# programs, they can be visualized using various UI frameworks available for C#. The case studies, in particular, use the Windows Presentation Foundation (WPF), a flexible framework with decent designers and Visual Studio integration.

For the time being, the visualizations of S#'s case studies are written in a rather ad hoc fashion, resulting in some convoluted code. We plan to build upon WPF's powerful extensibility and data binding mechanisms to make building visualizations more straightforward. Ideally, we hope to be able to create visualizations solely within Visual Studio's WPF designer without requiring a single line of code, at least for basic visualizations like the one of the [railroad crossing case study](Radio-Controlled Railroad Crossing Case Study) or the [pressure tank case study](Pressure Tank Case Study).

Visualizations can use the RealTimeSimulator class that wraps a Simulator in order to automatically forward the simulation with a certain step count per second:

// Create a model and a simulator for it.
var simulator = new Simulator(new Model());

// Initialize the RealTimeSimulator; the step delay is in milliseconds,
// i.e., it indicates the time to wait between two steps.
var realTimeSimulator = new RealTimeSimulator(simulator, stepDelay: 100);

Similar to the Simulator, RealTimeSimulator can be fast-forwarded or rewound. Additionally, the method Run() automatically executes a step after stepDelay milliseconds have passed whereas Pause() pauses automatic execution; it can be resumed by calling Run() again.

Replaying Counter Examples

Model checking counter examples can be replayed in a simulation in order to visualize the counter example or to debug it using Visual Studio's integrated debugger:

// Load a saved counter example from disk; this method might fail if
// changes have been made to any types referenced in the counter example.
var counterExample = CounterExample.Load("path-to-counterexample");

// Create a Simulator instance for the counter example; the model the
// counter example was generated for can be obtained from the simulator.
var simulator = new Simulator(counterExample);
var model = simulator.Model;

// Use the simulator as shown above.

Further Examples

Further examples for simulations with S# can be found in the case study projects.