Evaluations improved

isse-augsburg · Jan 23, 2018 · 545dc3a · 545dc3a
1 parent cfc06a2
commit 545dc3a
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 0 deletions.
diff --git a/Models/Railroad Crossing/Analysis/EvaluationTests.cs b/Models/Railroad Crossing/Analysis/EvaluationTests.cs
@@ -227,6 +227,7 @@ public void CalculateHazardSingleCoreAllFaults()
 			var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
 			markovChainGenerator.Configuration.SuccessorCapacity *= 2;
 			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
+			markovChainGenerator.Configuration.CpuCount = 1;
 			var formulaToCheck = new BoundedUnaryFormula(model.PossibleCollision, UnaryOperator.Finally, 50);
 			markovChainGenerator.AddFormulaToCheck(formulaToCheck);
 			foreach (var fault in model.Faults)
@@ -265,6 +266,7 @@ public void CalculateHazardWithoutEarlyTermination()
 		public void CalculateLtmdpWithoutFaultsWithPruning()
 		{
 			var model = new Model();
+			SetProbabilities(model);
 			model.Channel.MessageDropped.ProbabilityOfOccurrence = null;
 
 			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);
@@ -284,6 +286,7 @@ public void CalculateLtmdpWithoutFaultsWithPruning()
 		public void CalculateLtmdpWithoutStaticPruning()
 		{
 			var model = new Model();
+			SetProbabilities(model);
 			model.Channel.MessageDropped.ProbabilityOfOccurrence = null;
 
 			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);
@@ -308,6 +311,7 @@ public void CalculateLtmdpWithoutStaticPruning()
 		public void CalculateLtmdpWithoutStaticPruningSingleCore()
 		{
 			var model = new Model();
+			SetProbabilities(model);
 			model.Channel.MessageDropped.ProbabilityOfOccurrence = null;
 
 			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);
@@ -317,6 +321,7 @@ public void CalculateLtmdpWithoutStaticPruningSingleCore()
 			markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(3300000L, 1000000000L);
 			markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
 			markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuiltInLtmdp;
+			markovChainGenerator.Configuration.CpuCount = 1;
 			var formulaToCheck = new BoundedUnaryFormula(model.PossibleCollision, UnaryOperator.Finally, 50);
 			markovChainGenerator.AddFormulaToCheck(formulaToCheck);
 			foreach (var fault in model.Faults)
@@ -340,6 +345,7 @@ public void CalculateLtmdpWithoutStaticPruningSingleCore()
 		public void CalculateMdpNewStates()
 		{
 			var model = new Model();
+			SetProbabilities(model);
 			model.Channel.MessageDropped.ProbabilityOfOccurrence = null;
 
 			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);
@@ -366,6 +372,7 @@ public void CalculateMdpNewStates()
 		public void CalculateMdpNewStatesConstant()
 		{
 			var model = new Model();
+			SetProbabilities(model);
 			model.Channel.MessageDropped.ProbabilityOfOccurrence = null;
 
 			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);
@@ -393,6 +400,7 @@ public void CalculateMdpNewStatesConstant()
 		public void CalculateMdpFlattened()
 		{
 			var model = new Model();
+			SetProbabilities(model);
 			model.Channel.MessageDropped.ProbabilityOfOccurrence=null;
 
 			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);
@@ -420,6 +428,7 @@ public void CalculateMdpFlattened()
 		public void CalculateMdpNewStatesWithoutFaults()
 		{
 			var model = new Model();
+			SetProbabilities(model);
 			model.Channel.MessageDropped.ProbabilityOfOccurrence = null;
 
 			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);
@@ -441,6 +450,7 @@ public void CalculateMdpNewStatesWithoutFaults()
 		public void CalculateMdpNewStatesConstantWithoutFaults()
 		{
 			var model = new Model();
+			SetProbabilities(model);
 			model.Channel.MessageDropped.ProbabilityOfOccurrence = null;
 
 			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);
@@ -463,6 +473,7 @@ public void CalculateMdpNewStatesConstantWithoutFaults()
 		public void CalculateMdpFlattenedWithoutFaults()
 		{
 			var model = new Model();
+			SetProbabilities(model);
 			model.Channel.MessageDropped.ProbabilityOfOccurrence = null;
 
 			var createModel = SafetySharpRuntimeModel.CreateExecutedModelFromFormulasCreator(model);

diff --git a/Models/Railroad Crossing/Analysis/HazardProbabilityRangeTests.cs b/Models/Railroad Crossing/Analysis/HazardProbabilityRangeTests.cs
@@ -48,6 +48,8 @@ public void Calculate()
 			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);
+
+			model.Channel.MessageDropped.ProbabilityOfOccurrence = null;
 
 			var result = SafetySharpModelChecker.CalculateProbabilityRangeToReachStateBounded(model, model.PossibleCollision,50);
 			Console.Write($"Probability of hazard in 50 steps: {result}");