new parametric benchmark

Benchmark/evaluation10_RailroadParameterized.ps1

@@ -0,0 +1,49 @@
+# 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
+
+# include functionality per Dot-Sourcing
+. $PSScriptRoot\func_benchmarkTestCases.ps1
+
+
+# HeightControl
+AddTest -Testname "RailroadCrossing" -TestAssembly "SafetySharp.CaseStudies.RailroadCrossing.dll" -TestMethod "SafetySharp.CaseStudies.RailroadCrossing.Analysis.HazardProbabilityTests.Parametric" -TestNunitCategory "" -TestCategories @("Parametric","RailroadCrossing")
+
+$global_selected_tests = $global_tests | Where { $_.TestCategories.Contains("Parametric") -and  $_.TestCategories.Contains("RailroadCrossing") }
+
+AddTestValuation -Name "RailroadParametric"  -Script ""  -ResultDir "$PSScriptRoot\RailroadParametric" -FilesOfTestValuation @()
+
+Foreach ($testvaluation in $global_testValuations) {
+    ExecuteTestValuation -TestValuation $testvaluation -Tests $global_selected_tests
+}

Models/Height Control/Analysis/HazardProbabilityTests.cs

@@ -163,7 +163,7 @@ public void ParametricLbInOriginalDesign()
 			{
 				StateFormula = model.Collision,
 				Bound = 50,
-				From = 0.00001,
+				From = 0.000001,
 				To = 0.01,
 				Steps = 25,
 				UpdateParameterInModel = updateParameterInModel

Models/Railroad Crossing/Analysis/HazardProbabilityTests.cs

@@ -28,13 +28,15 @@
 
 namespace SafetySharp.CaseStudies.RailroadCrossing.Analysis
 {
+	using System.IO;
 	using FluentAssertions;
-	using ISSE.SafetyChecking;
+	using ISSE.SafetyChecking.DiscreteTimeMarkovChain;
 	using ISSE.SafetyChecking.Modeling;
 	using Modeling;
 	using NUnit.Framework;
 	using SafetySharp.Analysis;
 	using SafetySharp.Modeling;
+	using LtmcModelChecker = ISSE.SafetyChecking.LtmcModelChecker;
 
 	class HazardProbabilityTests
 	{
@@ -58,5 +60,56 @@ public void Calculate()
 			var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.PossibleCollision,50);
 			Console.Write($"Probability of hazard in 50 steps: {result}");
 		}
+
+
+
+		[Test]
+		public void Parametric()
+		{
+			var tc = SafetySharpModelChecker.TraversalConfiguration;
+			tc.LtmcModelChecker = LtmcModelChecker.BuiltInLtmc;
+			//tc.UseAtomarPropositionsAsStateLabels = false;
+			SafetySharpModelChecker.TraversalConfiguration = tc;
+
+			var model = new Model();
+			model.Channel.MessageDropped.ProbabilityOfOccurrence = new Probability(0.0001);
+			model.CrossingController.Motor.BarrierMotorStuck.ProbabilityOfOccurrence = new Probability(0.001);
+			model.CrossingController.Sensor.BarrierSensorFailure.ProbabilityOfOccurrence = new Probability(0.00003);
+			model.CrossingController.TrainSensor.ErroneousTrainDetection.ProbabilityOfOccurrence = new Probability(0.0002);
+			model.TrainController.Brakes.BrakesFailure.ProbabilityOfOccurrence = new Probability(0.00002);
+			model.TrainController.Odometer.OdometerPositionOffset.ProbabilityOfOccurrence = new Probability(0.02);
+			model.TrainController.Odometer.OdometerSpeedOffset.ProbabilityOfOccurrence = new Probability(0.02);
+
+			Action<double> updateParameterBsInModel = value =>
+			{
+				model.CrossingController.Sensor.BarrierSensorFailure.ProbabilityOfOccurrence = new Probability(value);
+			};
+
+			Action<double> updateParameterOpInModel = value =>
+			{
+				model.TrainController.Odometer.OdometerPositionOffset.ProbabilityOfOccurrence = new Probability(value);
+			};
+
+			var parameter = new QuantitativeParametricAnalysisParameter
+			{
+				StateFormula = model.PossibleCollision,
+				Bound = 50,
+				From = 0.000001,
+				To = 0.01,
+				Steps = 25,
+				UpdateParameterInModel = updateParameterBsInModel
+			};
+
+			var result = SafetySharpModelChecker.ConductQuantitativeParametricAnalysis(model, parameter);
+			var fileWriter = new StreamWriter("ParametricBsPossibleCollision.csv", append: false);
+			result.ToCsv(fileWriter);
+			fileWriter.Close();
+
+			parameter.UpdateParameterInModel = updateParameterOpInModel;
+			result = SafetySharpModelChecker.ConductQuantitativeParametricAnalysis(model, parameter);
+			fileWriter = new StreamWriter("ParametricOpPossibleCollision.csv", append: false);
+			result.ToCsv(fileWriter);
+			fileWriter.Close();
+		}
 	}
 }