Skip to content
Permalink
Browse files

New Evaluation Scripts

  • Loading branch information...
joleuger committed Jan 16, 2018
1 parent ac5e094 commit 8e5fd01cec9d8ccdc403a88244bde972d0d1ef74
@@ -35,9 +35,15 @@

# include functionality per Dot-Sourcing
. $PSScriptRoot\func_benchmarkTestCases.ps1
# include test cases per Dot-Sourcing
. $PSScriptRoot\evaluation2_HeightControlOriginalParameterized_tests.ps1


# HeightControl
AddTest -Testname "HeightControl_Parametric" -TestAssembly "SafetySharp.CaseStudies.HeightControl.dll" -TestMethod "SafetySharp.CaseStudies.HeightControl.Analysis.HazardProbabilityTests.ParametricLbInOriginalDesign" -TestNunitCategory "" -TestCategories @("Parametric","HeightControl")

$global_selected_tests = $global_tests | Where { $_.TestCategories.Contains("Parametric") -and $_.TestCategories.Contains("HeightControl") }

AddTestValuation -Name "HeightControlParametric" -Script "copy -Force $PSScriptRoot\HeightControlNormal.json $global_compilate_directory\Analysis\heightcontrol_probabilities.json" -ResultDir "$PSScriptRoot\HeightControlParametric" -FilesOfTestValuation @("$global_compilate_directory\Analysis\heightcontrol_probabilities.json")

Foreach ($testvaluation in $global_testValuations) {
ExecuteTestValuation -TestValuation $testvaluation -Tests $global_selected_tests
}
}

Large diffs are not rendered by default.

@@ -0,0 +1,68 @@
# The MIT License (MIT)
#
# Copyright (c) 2014-2016, 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.
#
# Sources:
# * https://www.nunit.org/index.php?p=guiCommandLine&r=2.4
# * https://www.nunit.org/index.php?p=nunit-console&r=2.4
# * https://msdn.microsoft.com/en-us/powershell/scripting/getting-started/cookbooks/managing-current-location
# * https://msdn.microsoft.com/en-us/powershell/reference/5.1/microsoft.powershell.management/start-process
# * https://www.safaribooksonline.com/library/view/windows-powershell-cookbook/9780596528492/ch11s02.html
# * http://www.get-blog.com/?p=82

# Note: You must run the following command first
# Set-ExecutionPolicy -ExecutionPolicy RemoteSigned -Scope CurrentUser
# To Undo
# Set-ExecutionPolicy -ExecutionPolicy Restricted -Scope CurrentUser

# Example nunit-console.exe D:\Repositories\Universität\ssharp\Binaries\Release\SafetySharp.CaseStudies.PressureTank.dll /run=SafetySharp.CaseStudies.PressureTank.Analysis.HazardProbabilityTests.CalculateHazardIsDepleted"

# include functionality per Dot-Sourcing
. $PSScriptRoot\func_benchmarkTestCases.ps1
# include test cases per Dot-Sourcing
. $PSScriptRoot\func_testCases.ps1

New-Variable -Force -Name global_selected_tests -Option AllScope -Value @()
$global_testValuations = @()



AddTest -Testname "DeadReckoning" -TestAssembly "SafetySharp.CaseStudies.SmallModels.exe" -TestMethod "SafetySharp.CaseStudies.SmallModels.DeadReckoning.BayesianAnalysis.CalculateHazardProbability" -TestNunitCategory "" -TestCategories @("VariousEvaluations","DeadReckoning")
AddTest -Testname "DegradedMode" -TestAssembly "SafetySharp.CaseStudies.SmallModels.exe" -TestMethod "SafetySharp.CaseStudies.SmallModels.DegradedMode.ExampleAnalysis.CalculateHazardProbability" -TestNunitCategory "" -TestCategories @("VariousEvaluations","DegradedMode")
AddTest -Testname "RailroadCrossing" -TestAssembly "SafetySharp.CaseStudies.RailroadCrossing.dll" -TestMethod "SafetySharp.CaseStudies.RailroadCrossing.HazardProbabilityTests.Calculate" -TestNunitCategory "" -TestCategories @("VariousEvaluations","RailroadCrossing")
AddTest -Testname "LustrePressureTank" -TestAssembly "SafetyLustre.CaseStudies.LustreModels.dll" -TestMethod "Lustre_Models.ModelCheckingTests.TankRupture" -TestNunitCategory "" -TestCategories @("VariousEvaluations","LustrePressureTank")
AddTest -Testname "HemodialysisMachine_Unsuccessful" -TestAssembly "SafetySharp.CaseStudies.HemodialysisMachine.exe" -TestMethod "SafetySharp.CaseStudies.HemodialysisMachine.HazardProbabilityTests.DialysisFinishedAndBloodNotCleaned" -TestNunitCategory "" -TestCategories @("VariousEvaluations","HemodialysisMachine")
AddTest -Testname "HemodialysisMachine_Contamination" -TestAssembly "SafetySharp.CaseStudies.HemodialysisMachine.exe" -TestMethod "SafetySharp.CaseStudies.HemodialysisMachine.HazardProbabilityTests.IncomingBloodIsContaminated" -TestNunitCategory "" -TestCategories @("VariousEvaluations","HemodialysisMachine")
AddTest -Testname "HeightControl_Collision" -TestAssembly "SafetySharp.CaseStudies.HeightControl.dll" -TestMethod "SafetySharp.CaseStudies.HeightControl.HazardProbabilityTests.CalculateCollisionInOriginalDesign" -TestNunitCategory "" -TestCategories @("VariousEvaluations","HeightControl")
AddTest -Testname "HeightControl_FalseAlarm" -TestAssembly "SafetySharp.CaseStudies.HeightControl.dll" -TestMethod "SafetySharp.CaseStudies.HeightControl.HazardProbabilityTests.CalculateFalseAlarmInOriginalDesign" -TestNunitCategory "" -TestCategories @("VariousEvaluations","HeightControl")






$global_selected_tests = $global_tests | Where { $_.TestCategories.Contains("VariousEvaluations") }

AddTestValuation -Name "Probabilities" -Script "copy -Force $PSScriptRoot\HeightControlNormal.json $global_compilate_directory\Analysis\heightcontrol_probabilities.json" -ResultDir "$PSScriptRoot\Probabilities" -FilesOfTestValuation @("$global_compilate_directory\Analysis\heightcontrol_probabilities.json")

Foreach ($testvaluation in $global_testValuations) {
ExecuteTestValuation -TestValuation $testvaluation -Tests $global_selected_tests
}
@@ -0,0 +1,57 @@
# The MIT License (MIT)
#
# Copyright (c) 2014-2016, 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.
#
# Sources:
# * https://www.nunit.org/index.php?p=guiCommandLine&r=2.4
# * https://www.nunit.org/index.php?p=nunit-console&r=2.4
# * https://msdn.microsoft.com/en-us/powershell/scripting/getting-started/cookbooks/managing-current-location
# * https://msdn.microsoft.com/en-us/powershell/reference/5.1/microsoft.powershell.management/start-process
# * https://www.safaribooksonline.com/library/view/windows-powershell-cookbook/9780596528492/ch11s02.html
# * http://www.get-blog.com/?p=82

# Note: You must run the following command first
# Set-ExecutionPolicy -ExecutionPolicy RemoteSigned -Scope CurrentUser
# To Undo
# Set-ExecutionPolicy -ExecutionPolicy Restricted -Scope CurrentUser

# Example nunit-console.exe D:\Repositories\Universität\ssharp\Binaries\Release\SafetySharp.CaseStudies.PressureTank.dll /run=SafetySharp.CaseStudies.PressureTank.Analysis.HazardProbabilityTests.CalculateHazardIsDepleted"

# include functionality per Dot-Sourcing
. $PSScriptRoot\func_benchmarkTestCases.ps1
# include test cases per Dot-Sourcing
. $PSScriptRoot\func_testCases.ps1

New-Variable -Force -Name global_selected_tests -Option AllScope -Value @()
$global_testValuations = @()

# Bayesian
AddTest -Testname "DeadReckoning_Bayesian" -TestAssembly "SafetySharp.CaseStudies.SmallModels.exe" -TestMethod "SafetySharp.CaseStudies.SmallModels.DeadReckoning.BayesianAnalysis.TestConstraintBasedLearning" -TestNunitCategory "" -TestCategories @("Bayesian","DeadReckoning","ConstrainedBased")
AddTest -Testname "RailroadCrossing_Bayesian" -TestAssembly "SafetySharp.CaseStudies.RailroadCrossing.dll" -TestMethod "SafetySharp.CaseStudies.RailroadCrossing.Analysis.BayesianAnalysis.ConstraintBased" -TestNunitCategory "" -TestCategories @("Bayesian","RailroadCrossing","ConstrainedBased")


$global_selected_tests = $global_tests | Where { $_.TestCategories.Contains("Bayesian") }

AddTestValuation -Name "Bayesian" -Script "" -ResultDir "$PSScriptRoot\Bayesian" -FilesOfTestValuation @()

Foreach ($testvaluation in $global_testValuations) {
ExecuteTestValuation -TestValuation $testvaluation -Tests $global_selected_tests
}
@@ -285,7 +285,7 @@ public void CreateFaultAwareMarkovChainTwoFaults()
}

[Test]
public void CalculateSingleCore()
public void CalculateHazardSingleCore()
{
var model = Model.CreateOriginal();
SetProbabilities(model);
@@ -209,7 +209,7 @@ public void CreateFaultAwareMarkovChainAllFaults()
}

[Test]
public void CalculateSingleCore()
public void CalculateHazardSingleCore()
{
var model = new Model();
SetProbabilities(model);
@@ -100,7 +100,7 @@ public void CalculateHazardProbability()
SafetySharpModelChecker.TraversalConfiguration = tc;

var model = new DeadReckoningModel();
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 20);
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 10);

Console.WriteLine($"Probability of hazard in model: {result}");
}
@@ -96,7 +96,7 @@ public void CreateMarkovChainWithHazards()

var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 50);
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 10);
markovChainGenerator.Configuration.UseCompactStateStorage = true;
var markovChain = markovChainGenerator.GenerateMarkovChain();
}
@@ -155,7 +155,7 @@ public void CreateMarkovChainWithHazardFaultsInState()

var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 50);
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 10);
foreach (var fault in model.Faults)
{
var faultFormula = new FaultFormula(fault);
@@ -182,7 +182,7 @@ public void CreateFaultAwareMarkovChainAllFaults()
var faultFormula = new FaultFormula(fault);
markovChainGenerator.AddFormulaToCheck(faultFormula);
}
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 50);
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 10);
markovChainGenerator.Configuration.UseCompactStateStorage = true;
var markovChain = markovChainGenerator.GenerateMarkovChain();
}
@@ -193,7 +193,7 @@ public void CalculateHazardSingleCore()
var model = new DeadReckoningModel();

SafetySharpModelChecker.TraversalConfiguration.CpuCount = 1;
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 50);
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 10);
SafetySharpModelChecker.TraversalConfiguration.CpuCount = Int32.MaxValue;
Console.Write($"Probability of hazard: {result}");
}
@@ -206,7 +206,7 @@ public void CalculateHazardWithoutEarlyTermination()
var model = new DeadReckoningModel();

SafetySharpModelChecker.TraversalConfiguration.EnableEarlyTermination = false;
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 50);
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 10);
SafetySharpModelChecker.TraversalConfiguration.EnableEarlyTermination = true;
Console.Write($"Probability of hazard: {result}");
}
@@ -121,6 +121,14 @@ public sealed class DegradedModeModel : ModelBase

public class ExampleAnalysis
{
[Test]
public void CalculateHazardProbability()
{
var model = new DegradedModeModel();
var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.System.HazardActive, 50);
Console.Write($"Probability of hazard: {result}");
}

[Test]
public void CalculateHazardProbabilityWhenF1AlwaysOccurs()
{

0 comments on commit 8e5fd01

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