Installation and Setup
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.
-
Clone the S# repository:
git clone https://github.com/isse-augsburg/ssharp.git
. -
Open the S# solution
SafetySharp.sln
with Visual Studio 2015 Update 2. -
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.
-
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".
- In the solution explorer, the
visualizations
projects under theModels
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.
-
Open Visual Studio 2015 Update 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.
-
Import the S# runtime and compiler into the project.
-
Right-click the project name in the "Solution Explorer" and choose "Manage NuGet Packages..."
-
In the "Browse" tab, search for
ISSE.SafetySharp
. -
Select the
ISSE.SafetySharp
package and click "Install".
-
-
Add the NUnit package to your project (optional; only used to write tests).
-
Right-click the project name in the "Solution Explorer" and choose "Manage NuGet Packages..."
-
In the "Browse" tab, search for
NUnit
. -
Select the
NUnit
package, choose a version < 3 (for instance, 2.6.4), and click "Install". -
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 { } ```
- 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.
-
You are now ready to model and analyze your own case study.
-
For LTL model checking, be sure to follow the [LTSMin compilation instructions](Compiling LTSMin).