Skip to content
Permalink
Browse files

Created project for small S# examples

  • Loading branch information...
joleuger committed May 24, 2017
1 parent 890e29f commit ce06719c0b62f7add38f02d51c01c00b3c00184b
@@ -0,0 +1,6 @@
<?xml version="1.0" encoding="utf-8" ?>
<configuration>
<startup>
<supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.5.2" />
</startup>
</configuration>
@@ -0,0 +1,79 @@
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace Small_Models
{
using ISSE.SafetyChecking.Formula;
using ISSE.SafetyChecking.MinimalCriticalSetAnalysis;
using ISSE.SafetyChecking.Modeling;
using NUnit.Framework;
using SafetySharp.Analysis;
using SafetySharp.ModelChecking;
using SafetySharp.Modeling;


public class Model1Component : Component
{
public Model1Component()
{
F1 = new TransientFault();
F1.ProbabilityOfOccurrence = new Probability(0.3);
}

public Fault F1;


public bool HazardActive = false;

public override void Update()
{
}


[FaultEffect(Fault = nameof(F1)), Priority(0)]
public class F1Effect : Model1Component
{
public override void Update()
{
HazardActive = true;
}
}
}


public sealed class Model1ModelBase : ModelBase
{
[Root(RootKind.Controller)]
public Model1Component Model1Component { get; } = new Model1Component();
}


public class Model1Analysis
{
[Test]
public void CalculateProbability()
{
var model = new Model1ModelBase();

var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Model1Component.HazardActive, 50);
Console.Write($"Probability of hazard: {result}");
}


[Test]
public void CalculateDcca()
{
var model = new Model1ModelBase();

var analysis = new SafetySharpSafetyAnalysis { Backend = SafetyAnalysisBackend.FaultOptimizedOnTheFly, Heuristics = { new MaximalSafeSetHeuristic(model.Faults) } };
var result = analysis.ComputeMinimalCriticalSets(model, model.Model1Component.HazardActive);
//result.SaveCounterExamples("counter examples/height control/dcca/collision/original");

var orderResult = SafetySharpOrderAnalysis.ComputeOrderRelationships(result);
Console.WriteLine(orderResult);
}
}
}
@@ -0,0 +1,113 @@
using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using System.Threading.Tasks;

namespace Small_Models
{
using ISSE.SafetyChecking.Formula;
using ISSE.SafetyChecking.MinimalCriticalSetAnalysis;
using ISSE.SafetyChecking.Modeling;
using NUnit.Framework;
using SafetySharp.Analysis;
using SafetySharp.ModelChecking;
using SafetySharp.Modeling;


public class Model2Component : Component
{
public Model2Component()
{
F1 = new TransientFault();
F1.ProbabilityOfOccurrence = new Probability(0.003);


F2 = new TransientFault();
F2.ProbabilityOfOccurrence = new Probability(0.0001);
}

public Fault F1;
public Fault F2;

public int Step = 0;

public int Value = 0;

public bool LoopRequestBug = false;

public override void Update()
{
if (Step > 10)
return;
Step++;

if (Step==1)
Request();
if (Step== 5 || LoopRequestBug)
SetValueTo2();
}

public virtual void Request()
{
}

public virtual void SetValueTo2()
{
Value = 2;
}


[FaultEffect(Fault = nameof(F1)), Priority(0)]
public class F1Effect : Model2Component
{
public override void Request()
{
LoopRequestBug = true;
}
}

[FaultEffect(Fault = nameof(F2)), Priority(0)]
public class F2Effect : Model2Component
{
public override void SetValueTo2()
{
Value = 3;
}
}
}


public sealed class Model2ModelBase : ModelBase
{
[Root(RootKind.Controller)]
public Model2Component Model2Component { get; } = new Model2Component();
}


public class Model2Analysis
{
[Test]
public void CalculateProbability()
{
var model = new Model2ModelBase();

var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Model2Component.Value==3, 50);
Console.Write($"Probability of hazard: {result}");
}


[Test]
public void CalculateDcca()
{
var model = new Model2ModelBase();

var analysis = new SafetySharpSafetyAnalysis { Backend = SafetyAnalysisBackend.FaultOptimizedOnTheFly, Heuristics = { new MaximalSafeSetHeuristic(model.Faults) } };
var result = analysis.ComputeMinimalCriticalSets(model, model.Model2Component.Value == 3);
//result.SaveCounterExamples("counter examples/height control/dcca/collision/original");

var orderResult = SafetySharpOrderAnalysis.ComputeOrderRelationships(result);
Console.WriteLine(orderResult);
}
}
}
@@ -0,0 +1,25 @@
// The MIT License (MIT)
//
// Copyright (c) 2014-2017, Institute for Software & Systems Engineering
//
// Permission is hereby granted, free of charge, to any person obtaining a copy
// of this software and associated documentation files (the "Software"), to deal
// in the Software without restriction, including without limitation the rights
// to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
// copies of the Software, and to permit persons to whom the Software is
// furnished to do so, subject to the following conditions:
//
// The above copyright notice and this permission notice shall be included in
// all copies or substantial portions of the Software.
//
// THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
// IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
// FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
// AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
// LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
// OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
// THE SOFTWARE.

using System.Reflection;

[assembly: AssemblyTitle("S# Small Models")]
@@ -0,0 +1,98 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="14.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<Import Project="$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props" Condition="Exists('$(MSBuildExtensionsPath)\$(MSBuildToolsVersion)\Microsoft.Common.props')" />
<Import Project="../../Source/SafetySharp.props" />
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
<ProjectGuid>{6F3CABAC-A40E-4AFE-AC5B-5989D278F64C}</ProjectGuid>
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>SafetySharp.CaseStudies.SmallModels</RootNamespace>
<AssemblyName>SafetySharp.CaseStudies.SmallModels</AssemblyName>
<TargetFrameworkVersion>v4.5</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<TargetFrameworkProfile />
<NuGetPackageImportStamp>
</NuGetPackageImportStamp>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
<OutputPath>..\..\Binaries\Debug\</OutputPath>
<DefineConstants>DEBUG;TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<NoWarn>0626</NoWarn>
<Prefer32Bit>false</Prefer32Bit>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
<OutputPath>..\..\Binaries\Release\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
<NoWarn>0626</NoWarn>
<Prefer32Bit>false</Prefer32Bit>
</PropertyGroup>
<PropertyGroup>
<RunPostBuildEvent>Always</RunPostBuildEvent>
</PropertyGroup>
<PropertyGroup>
<StartupObject />
</PropertyGroup>
<ItemGroup>
<Reference Include="FluentAssertions, Version=4.1.1.0, Culture=neutral, PublicKeyToken=33f2691a05b67b6a, processorArchitecture=MSIL">
<HintPath>..\..\Dependencies\FluentAssertions.4.1.1\lib\net45\FluentAssertions.dll</HintPath>
<Private>True</Private>
</Reference>
<Reference Include="FluentAssertions.Core, Version=4.1.1.0, Culture=neutral, PublicKeyToken=33f2691a05b67b6a, processorArchitecture=MSIL">
<HintPath>..\..\Dependencies\FluentAssertions.4.1.1\lib\net45\FluentAssertions.Core.dll</HintPath>
<Private>True</Private>
</Reference>
<Reference Include="Newtonsoft.Json, Version=9.0.0.0, Culture=neutral, PublicKeyToken=30ad4fe6b2a6aeed, processorArchitecture=MSIL">
<HintPath>..\..\Dependencies\Newtonsoft.Json.9.0.1\lib\net45\Newtonsoft.Json.dll</HintPath>
<Private>True</Private>
</Reference>
<Reference Include="nunit.framework">
<HintPath>..\..\Dependencies\NUnit.2.6.3\lib\nunit.framework.dll</HintPath>
</Reference>
<Reference Include="System" />
<Reference Include="System.Core" />
<Reference Include="Microsoft.CSharp" />
<Reference Include="System.Xml" />
<Reference Include="System.Xml.Linq" />
</ItemGroup>
<ItemGroup>
<Compile Include="..\..\Source\SharedAssemblyInfo.cs">
<Link>Properties\SharedAssemblyInfo.cs</Link>
</Compile>
<Compile Include="Model2.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
<Compile Include="Model1.cs" />
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\..\Source\SafetyChecking\SafetyChecking.csproj">
<Project>{a91cb8af-8a4c-4f69-848e-b3962f9a94f9}</Project>
<Name>SafetyChecking</Name>
</ProjectReference>
<ProjectReference Include="..\..\Source\SafetySharp\SafetySharp.csproj">
<Project>{9b6c1fb4-3f1b-43ac-a0e0-eaed4088bf37}</Project>
<Name>SafetySharp</Name>
</ProjectReference>
</ItemGroup>
<ItemGroup>
<Analyzer Include="$(OutDir)\SafetySharp.Modeling.dll" />
<Analyzer Include="$(OutDir)\SafetySharp.Compiler.dll" />
</ItemGroup>
<ItemGroup>
<None Include="packages.config" />
</ItemGroup>
<ItemGroup>
<Service Include="{82A7F48D-3B50-4B1E-B82E-3ADA8210C358}" />
</ItemGroup>
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<Import Project="../../Source/SafetySharp.targets" />
</Project>
@@ -0,0 +1,6 @@
<?xml version="1.0" encoding="utf-8"?>
<packages>
<package id="FluentAssertions" version="4.1.1" targetFramework="net46" />
<package id="Newtonsoft.Json" version="9.0.1" targetFramework="net45" />
<package id="NUnit" version="2.6.3" targetFramework="net45" />
</packages>
@@ -69,6 +69,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SafetyCheckingTests", "Safe
{A91CB8AF-8A4C-4F69-848E-B3962F9A94F9} = {A91CB8AF-8A4C-4F69-848E-B3962F9A94F9}
EndProjectSection
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Small Models", "Models\Small Models\Small Models.csproj", "{6F3CABAC-A40E-4AFE-AC5B-5989D278F64C}"
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|Any CPU = Debug|Any CPU
@@ -127,6 +129,10 @@ Global
{BDCD5EA9-61C8-415D-ADDA-F3A70D3EFA1D}.Debug|Any CPU.Build.0 = Debug|Any CPU
{BDCD5EA9-61C8-415D-ADDA-F3A70D3EFA1D}.Release|Any CPU.ActiveCfg = Release|Any CPU
{BDCD5EA9-61C8-415D-ADDA-F3A70D3EFA1D}.Release|Any CPU.Build.0 = Release|Any CPU
{6F3CABAC-A40E-4AFE-AC5B-5989D278F64C}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
{6F3CABAC-A40E-4AFE-AC5B-5989D278F64C}.Debug|Any CPU.Build.0 = Debug|Any CPU
{6F3CABAC-A40E-4AFE-AC5B-5989D278F64C}.Release|Any CPU.ActiveCfg = Release|Any CPU
{6F3CABAC-A40E-4AFE-AC5B-5989D278F64C}.Release|Any CPU.Build.0 = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
@@ -145,5 +151,6 @@ Global
{07DEADE8-4700-4F51-AF54-EE88878C0127} = {C6B04010-51F6-49C0-8F58-FEA7D30541E2}
{A91CB8AF-8A4C-4F69-848E-B3962F9A94F9} = {64793805-8DC9-4A61-B41B-3369490319CD}
{BDCD5EA9-61C8-415D-ADDA-F3A70D3EFA1D} = {64793805-8DC9-4A61-B41B-3369490319CD}
{6F3CABAC-A40E-4AFE-AC5B-5989D278F64C} = {C6B04010-51F6-49C0-8F58-FEA7D30541E2}
EndGlobalSection
EndGlobal

0 comments on commit ce06719

Please sign in to comment.
You can’t perform that action at this time.