Skip to content

Installation and Setup

Axel Habermaier edited this page May 13, 2016 · 2 revisions

This page shows you how to get started using S#. Installation and setup are relatively straightforward if you have any experience in .NET development. In any case, the necessary steps and prerequisites are explained in detail in the following.

Review S#'s Case Studies

  1. Clone the S# repository: git clone https://github.com/isse-augsburg/ssharp.git.

  2. Open the S# solution SafetySharp.sln with Visual Studio 2015 Update 2.

  3. For LTL model checking, be sure to follow the [LTSMin compilation instructions](Compiling LTSMin). Otherwise, LTL model checking and all test cases using LTL model checking will fail.

  4. In the "Solution Explorer", open the Models node; each of the case studies is located in its own S# project.

In each project, there are several NUnit-based tests that conduct [safety analyses](Safety Analysis), [model check](Model Checking) properties, or run simulations.

To run the tests, open the Test Explorer by selecting "Test -> Windows -> Test Explorer", then right-click the tests you want to execute. For this to work, you must first install the NUnit Test Adapter extension for Visual Studio.

Note: Be sure to force the tests to run in x64 mode. To do so, select "Tests -> Test Settings -> Default Processor Architecture -> X64".

Note: Always use "Release" builds for model checking; "Debug" builds are significantly slower.

Hint: Click the icon next to the "Search" field in the "Test Explorer" in order to group by "Project".

  1. In the solution explorer, the visualizations projects under the Models node contains the visualizations for the case studies.

Right click on the Visualizations project and select "Debug -> Start new instance" to run the visualization. The visualizations of the case studies are located in separate tabs at the top; use the controls to start, stop, fast-forward, rewind simulations. You can change the simulation speed and load counter examples for replaying. For more details, see the "Visualizations" section of the simulations page.

Model and Analyze your own Case Studies with S#

  1. Open Visual Studio 2015 Update 2.

  2. Create a new C# project by choosing "File -> New -> Project"; in the dialog, choose a solution name and select the "Class Library" template found under the "Visual C#" category.

  3. Import the S# runtime and compiler into the project.

    1. Right-click the project name in the "Solution Explorer" and choose "Manage NuGet Packages..."

    2. In the "Browse" tab, search for ISSE.SafetySharp.

    3. Select the ISSE.SafetySharp package and click "Install".

  4. Add the NUnit package to your project (optional; only used to write tests).

  5. Right-click the project name in the "Solution Explorer" and choose "Manage NuGet Packages..."

  6. In the "Browse" tab, search for NUnit.

  7. Select the NUnit package, choose a version < 3 (for instance, 2.6.4), and click "Install".

  8. Replace the code in Class1.cs with the following:

using NUnit.Framework; using SafetySharp.Analysis; using SafetySharp.Modeling;

class FirstSafetySharpModel { [Test] public void Test() { var result = ModelChecker.CheckInvariant(new Model(), true); Assert.IsTrue(result.FormulaHolds); } }

class Model : ModelBase { [Root(RootKind.Controller)] public C C = new C(); }

class C : Component { } ```

  1. To run the test, open the "Test Explorer" by selecting "Test -> Windows -> Test Explorer" and click "Run All". For this to work, you must first install the NUnit Test Adapter extension for Visual Studio. The test executes and the exemplary empty model is model checked.

Note: Be sure to force the tests to run in x64 mode. To do so, select "Tests -> Test Settings -> Default Processor Architecture -> X64".

Note: Always use "Release" builds for model checking; "Debug" builds are significantly slower.

  1. You are now ready to model and analyze your own case study.

  2. For LTL model checking, be sure to follow the [LTSMin compilation instructions](Compiling LTSMin).

You can’t perform that action at this time.