Skip to content
Permalink
Browse files

Added LustreModelSerializerTests

  • Loading branch information...
pascalpfeil committed Jun 5, 2018
1 parent 4eb7098 commit 2f620a5ede9b4df7108fd54a85f6b8e6cfa2a0b7
@@ -18,7 +18,7 @@
</NuGetPackageImportStamp>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<PlatformTarget>x64</PlatformTarget>
<PlatformTarget>AnyCPU</PlatformTarget>
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>
@@ -17,6 +17,8 @@ Project("{2150E333-8FDC-42A3-9474-1A3956D46DE8}") = "Models", "Models", "{95E3B5
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Lustre Models", "Models\Lustre Models\Lustre Models.csproj", "{7454E37B-B75D-4B8C-8169-0D1F6DD02FCE}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "SafetyLustre.Tests", "Source\SafetyLustre.Tests\SafetyLustre.Tests.csproj", "{2C749D61-8A55-4C9D-9DA7-5181CB692569}"
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Debug|Any CPU = Debug|Any CPU
@@ -43,6 +45,10 @@ Global
{7454E37B-B75D-4B8C-8169-0D1F6DD02FCE}.Debug|Any CPU.Build.0 = Debug|Any CPU
{7454E37B-B75D-4B8C-8169-0D1F6DD02FCE}.Release|Any CPU.ActiveCfg = Release|Any CPU
{7454E37B-B75D-4B8C-8169-0D1F6DD02FCE}.Release|Any CPU.Build.0 = Release|Any CPU
{2C749D61-8A55-4C9D-9DA7-5181CB692569}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
{2C749D61-8A55-4C9D-9DA7-5181CB692569}.Debug|Any CPU.Build.0 = Debug|Any CPU
{2C749D61-8A55-4C9D-9DA7-5181CB692569}.Release|Any CPU.ActiveCfg = Release|Any CPU
{2C749D61-8A55-4C9D-9DA7-5181CB692569}.Release|Any CPU.Build.0 = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
@@ -53,6 +59,7 @@ Global
{A1BF68D6-A34D-4892-9A5C-7DB3A4F2A01D} = {64793805-8DC9-4A61-B41B-3369490319CD}
{A91CB8AF-8A4C-4F69-848E-B3962F9A94F9} = {64793805-8DC9-4A61-B41B-3369490319CD}
{7454E37B-B75D-4B8C-8169-0D1F6DD02FCE} = {95E3B5AE-1A7F-45AA-AA66-1C9D599A47E0}
{2C749D61-8A55-4C9D-9DA7-5181CB692569} = {64793805-8DC9-4A61-B41B-3369490319CD}
EndGlobalSection
GlobalSection(ExtensibilityGlobals) = postSolution
SolutionGuid = {AA5452D7-CDA9-4CD9-B4F9-D1CADC735BF9}
@@ -35,5 +35,6 @@
[assembly: AssemblyVersion("1.0.0.0")]
[assembly: AssemblyFileVersion("1.0.0.0")]

[assembly: InternalsVisibleTo("SafetyLustre.LustreCompiler.Tests")]
[assembly: InternalsVisibleTo("SafetyLustre")]
[assembly: InternalsVisibleTo("SafetyLustre.Tests")]
[assembly: InternalsVisibleTo("SafetyLustre.LustreCompiler.Tests")]
@@ -0,0 +1,26 @@
node TANK(press: bool) returns (level: int);
var k1: bool; k2: bool; sensor: bool; timer: int;
let
sensor = false ->
if (level > 39) then true
else false;

k1 = false ->
if ((pre(k1) or press) and (timer < 10)) then true
else false;

timer = 0 ->
if pre(sensor) then 0
else if (press or pre(k1)) then (pre(timer) + 1)
else 0;

k2 = false ->
if (press or pre(k1)) and not sensor then true
else false;

level = 0 ->
if pre(sensor) or ((pre(timer) > 9) and not press) then 0
else if pre(k2) then pre(level) + 5
else pre(level);

tel
@@ -0,0 +1,47 @@
using ISSE.SafetyChecking.Modeling;
using Microsoft.VisualStudio.TestTools.UnitTesting;
using System;
using System.Collections.Generic;
using System.Linq;

namespace SafetyLustre.Tests
{
[TestClass()]
public unsafe class LustreModelSerializerTests
{
[TestMethod()]
public void TestModelSerialization()
{
//Arrange
var model = new LustreModelBase(@"Examples\pressureTank.lus", "TANK", new List<Fault>());
var memory = stackalloc byte[model.StateVectorSize];
Console.WriteLine($"Allocated {model.StateVectorSize} bytes of memory.");

var bools = model.Runner.Oc5ModelState.Bools;
var ints = model.Runner.Oc5ModelState.Ints;
var strings = model.Runner.Oc5ModelState.Strings;
var floats = model.Runner.Oc5ModelState.Floats;
var doubles = model.Runner.Oc5ModelState.Doubles;
var mappings = model.Runner.Oc5ModelState.Mappings;
var inputMappings = model.Runner.Oc5ModelState.InputMappings;
var outputMappings = model.Runner.Oc5ModelState.OutputMappings;

//Act
var deserializer = LustreModelSerializer.CreateFastInPlaceDeserializer(model);
var serializer = LustreModelSerializer.CreateFastInPlaceSerializer(model);

deserializer(memory);
serializer(memory);

//Assert
Assert.IsTrue(model.Runner.Oc5ModelState.Bools.SequenceEqual(bools));
Assert.IsTrue(model.Runner.Oc5ModelState.Ints.SequenceEqual(ints));
Assert.IsTrue(model.Runner.Oc5ModelState.Strings.SequenceEqual(strings));
Assert.IsTrue(model.Runner.Oc5ModelState.Floats.SequenceEqual(floats));
Assert.IsTrue(model.Runner.Oc5ModelState.Doubles.SequenceEqual(doubles));
Assert.IsTrue(model.Runner.Oc5ModelState.Mappings.SequenceEqual(mappings));
Assert.IsTrue(model.Runner.Oc5ModelState.InputMappings.SequenceEqual(inputMappings));
Assert.IsTrue(model.Runner.Oc5ModelState.OutputMappings.SequenceEqual(outputMappings));
}
}
}
@@ -0,0 +1,20 @@
using System.Reflection;
using System.Runtime.CompilerServices;
using System.Runtime.InteropServices;

[assembly: AssemblyTitle("SafetyLustre.Tests")]
[assembly: AssemblyDescription("")]
[assembly: AssemblyConfiguration("")]
[assembly: AssemblyCompany("")]
[assembly: AssemblyProduct("SafetyLustre.Tests")]
[assembly: AssemblyCopyright("Copyright © 2018")]
[assembly: AssemblyTrademark("")]
[assembly: AssemblyCulture("")]

[assembly: ComVisible(false)]

[assembly: Guid("2c749d61-8a55-4c9d-9da7-5181cb692569")]

// [assembly: AssemblyVersion("1.0.*")]
[assembly: AssemblyVersion("1.0.0.0")]
[assembly: AssemblyFileVersion("1.0.0.0")]
@@ -0,0 +1,85 @@
<?xml version="1.0" encoding="utf-8"?>
<Project ToolsVersion="15.0" DefaultTargets="Build" xmlns="http://schemas.microsoft.com/developer/msbuild/2003">
<Import Project="..\..\Dependencies\MSTest.TestAdapter.1.2.1\build\net45\MSTest.TestAdapter.props" Condition="Exists('..\..\Dependencies\MSTest.TestAdapter.1.2.1\build\net45\MSTest.TestAdapter.props')" />
<PropertyGroup>
<Configuration Condition=" '$(Configuration)' == '' ">Debug</Configuration>
<Platform Condition=" '$(Platform)' == '' ">AnyCPU</Platform>
<ProjectGuid>{2C749D61-8A55-4C9D-9DA7-5181CB692569}</ProjectGuid>
<OutputType>Library</OutputType>
<AppDesignerFolder>Properties</AppDesignerFolder>
<RootNamespace>SafetyLustre.Tests</RootNamespace>
<AssemblyName>SafetyLustre.Tests</AssemblyName>
<TargetFrameworkVersion>v4.5</TargetFrameworkVersion>
<FileAlignment>512</FileAlignment>
<ProjectTypeGuids>{3AC096D0-A1C2-E12C-1390-A8335801FDAB};{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}</ProjectTypeGuids>
<VisualStudioVersion Condition="'$(VisualStudioVersion)' == ''">15.0</VisualStudioVersion>
<VSToolsPath Condition="'$(VSToolsPath)' == ''">$(MSBuildExtensionsPath32)\Microsoft\VisualStudio\v$(VisualStudioVersion)</VSToolsPath>
<ReferencePath>$(ProgramFiles)\Common Files\microsoft shared\VSTT\$(VisualStudioVersion)\UITestExtensionPackages</ReferencePath>
<IsCodedUITest>False</IsCodedUITest>
<TestProjectType>UnitTest</TestProjectType>
<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>
<AllowUnsafeBlocks>true</AllowUnsafeBlocks>
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Release|AnyCPU' ">
<DebugType>pdbonly</DebugType>
<Optimize>true</Optimize>
<OutputPath>bin\Release\</OutputPath>
<DefineConstants>TRACE</DefineConstants>
<ErrorReport>prompt</ErrorReport>
<WarningLevel>4</WarningLevel>
</PropertyGroup>
<ItemGroup>
<Reference Include="Microsoft.VisualStudio.TestPlatform.TestFramework, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
<HintPath>..\..\Dependencies\MSTest.TestFramework.1.2.1\lib\net45\Microsoft.VisualStudio.TestPlatform.TestFramework.dll</HintPath>
</Reference>
<Reference Include="Microsoft.VisualStudio.TestPlatform.TestFramework.Extensions, Version=14.0.0.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a, processorArchitecture=MSIL">
<HintPath>..\..\Dependencies\MSTest.TestFramework.1.2.1\lib\net45\Microsoft.VisualStudio.TestPlatform.TestFramework.Extensions.dll</HintPath>
</Reference>
<Reference Include="System" />
<Reference Include="System.Core" />
</ItemGroup>
<ItemGroup>
<Compile Include="ModelChecking\LustreModelSerializerTests.cs" />
<Compile Include="Properties\AssemblyInfo.cs" />
</ItemGroup>
<ItemGroup>
<None Include="Examples\pressureTank.lus">
<CopyToOutputDirectory>Always</CopyToOutputDirectory>
</None>
<None Include="packages.config" />
</ItemGroup>
<ItemGroup>
<ProjectReference Include="..\SafetyChecking\SafetyChecking.csproj">
<Project>{A91CB8AF-8A4C-4F69-848E-B3962F9A94F9}</Project>
<Name>SafetyChecking</Name>
</ProjectReference>
<ProjectReference Include="..\SafetyLustre.LustreCompiler\SafetyLustre.LustreCompiler.csproj">
<Project>{CFAAFD6C-76B7-400A-A715-2EB0B8EE0899}</Project>
<Name>SafetyLustre.LustreCompiler</Name>
</ProjectReference>
<ProjectReference Include="..\SafetyLustre\SafetyLustre.csproj">
<Project>{cc928659-8ccf-4357-bd4f-224f80c5c79a}</Project>
<Name>SafetyLustre</Name>
</ProjectReference>
</ItemGroup>
<Import Project="$(VSToolsPath)\TeamTest\Microsoft.TestTools.targets" Condition="Exists('$(VSToolsPath)\TeamTest\Microsoft.TestTools.targets')" />
<Import Project="$(MSBuildToolsPath)\Microsoft.CSharp.targets" />
<Target Name="EnsureNuGetPackageBuildImports" BeforeTargets="PrepareForBuild">
<PropertyGroup>
<ErrorText>This project references NuGet package(s) that are missing on this computer. Use NuGet Package Restore to download them. For more information, see http://go.microsoft.com/fwlink/?LinkID=322105. The missing file is {0}.</ErrorText>
</PropertyGroup>
<Error Condition="!Exists('..\..\Dependencies\MSTest.TestAdapter.1.2.1\build\net45\MSTest.TestAdapter.props')" Text="$([System.String]::Format('$(ErrorText)', '..\..\Dependencies\MSTest.TestAdapter.1.2.1\build\net45\MSTest.TestAdapter.props'))" />
<Error Condition="!Exists('..\..\Dependencies\MSTest.TestAdapter.1.2.1\build\net45\MSTest.TestAdapter.targets')" Text="$([System.String]::Format('$(ErrorText)', '..\..\Dependencies\MSTest.TestAdapter.1.2.1\build\net45\MSTest.TestAdapter.targets'))" />
</Target>
<Import Project="..\..\Dependencies\MSTest.TestAdapter.1.2.1\build\net45\MSTest.TestAdapter.targets" Condition="Exists('..\..\Dependencies\MSTest.TestAdapter.1.2.1\build\net45\MSTest.TestAdapter.targets')" />
</Project>
@@ -0,0 +1,5 @@
<?xml version="1.0" encoding="utf-8"?>
<packages>
<package id="MSTest.TestAdapter" version="1.2.1" targetFramework="net45" />
<package id="MSTest.TestFramework" version="1.2.1" targetFramework="net45" />
</packages>
@@ -49,7 +49,7 @@ public LustreModelBase(string lustrePath, string mainNode, IEnumerable<Fault> fa
StateVectorSize =
Runner.Oc5ModelState.Bools.Count * sizeof(bool) +
Runner.Oc5ModelState.Ints.Count * sizeof(int) +
Runner.Oc5ModelState.Strings.Count * sizeof(char) * 30 + //HACK max. legth of string is 30 chars (29 + '\0')
Runner.Oc5ModelState.Strings.Count * sizeof(char) * 30 + //HACK max. length of string is 30 chars (29 + '\0')
Runner.Oc5ModelState.Floats.Count * sizeof(float) +
Runner.Oc5ModelState.Doubles.Count * sizeof(double) +
Runner.Oc5ModelState.Mappings.Count * sizeof(PositionInOc5State) +
@@ -90,11 +90,10 @@ public static Fault ReadFault(BinaryReader reader)

public static void WriteFormula(BinaryWriter writer, Formula formula, Dictionary<Fault, int> faultToIndex)
{
if (formula is LustrePressureBelowThreshold)
if (formula is LustrePressureBelowThreshold lustrePressureBelowThreshold)
{
var innerFormula = (LustrePressureBelowThreshold)formula;
writer.Write(1);
writer.Write(innerFormula.Label);
writer.Write(lustrePressureBelowThreshold.Label);
}
else if (formula is FaultFormula faultFormula)
{
@@ -32,7 +32,7 @@
<TargetFrameworkProfile />
</PropertyGroup>
<PropertyGroup Condition=" '$(Configuration)|$(Platform)' == 'Debug|AnyCPU' ">
<PlatformTarget>x64</PlatformTarget>
<PlatformTarget>AnyCPU</PlatformTarget>
<DebugSymbols>true</DebugSymbols>
<DebugType>full</DebugType>
<Optimize>false</Optimize>

0 comments on commit 2f620a5

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