From 9c5ac1fa977e71eb17be275487dfb9327665cc40 Mon Sep 17 00:00:00 2001 From: Johannes Leupolz Date: Wed, 17 Jan 2018 17:04:34 +0100 Subject: [PATCH] Improved evaluations --- Models/Lustre Models/EvaluationTests.cs | 6 +++--- Models/Railroad Crossing/Analysis/EvaluationTests.cs | 6 +++--- Models/Small Models/DeadReckoning/EvaluationTests.cs | 6 +++--- Models/Small Models/DegradedMode/EvaluationTests.cs | 6 +++--- 4 files changed, 12 insertions(+), 12 deletions(-) diff --git a/Models/Lustre Models/EvaluationTests.cs b/Models/Lustre Models/EvaluationTests.cs index e739fb63..9c9ad542 100644 --- a/Models/Lustre Models/EvaluationTests.cs +++ b/Models/Lustre Models/EvaluationTests.cs @@ -53,7 +53,7 @@ public void CreateMarkovChainWithHazards() { var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(_createModel) { Configuration = LustreModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; - var result = LustreModelChecker.CalculateProbabilityToReachStateBounded("pressureTank", _faults, _hazard, 25); + markovChainGenerator.AddFormulaToCheck(_hazard); markovChainGenerator.Configuration.UseCompactStateStorage = true; var markovChain = markovChainGenerator.GenerateMarkovChain(); } @@ -100,7 +100,7 @@ public void CreateMarkovChainWithHazardFaultsInState() { var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(_createModel) { Configuration = LustreModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; - var result = LustreModelChecker.CalculateProbabilityToReachStateBounded("pressureTank", _faults, _hazard, 25); + markovChainGenerator.AddFormulaToCheck(_hazard); foreach (var fault in _faults) { var faultFormula = new FaultFormula(fault); @@ -118,12 +118,12 @@ public void CreateFaultAwareMarkovChainAllFaults() var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(_createModel) { Configuration = LustreModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; markovChainGenerator.Configuration.EnableStaticPruningOptimization = false; + markovChainGenerator.AddFormulaToCheck(_hazard); foreach (var fault in _faults) { var faultFormula = new FaultFormula(fault); markovChainGenerator.AddFormulaToCheck(faultFormula); } - var result = LustreModelChecker.CalculateProbabilityToReachStateBounded("pressureTank", _faults, _hazard, 25); markovChainGenerator.Configuration.UseCompactStateStorage = true; var markovChain = markovChainGenerator.GenerateMarkovChain(); } diff --git a/Models/Railroad Crossing/Analysis/EvaluationTests.cs b/Models/Railroad Crossing/Analysis/EvaluationTests.cs index dd9e2950..af817bb2 100644 --- a/Models/Railroad Crossing/Analysis/EvaluationTests.cs +++ b/Models/Railroad Crossing/Analysis/EvaluationTests.cs @@ -80,7 +80,7 @@ public void CreateMarkovChainWithHazards() var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; - var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.PossibleCollision, 50); + markovChainGenerator.AddFormulaToCheck(model.PossibleCollision); markovChainGenerator.Configuration.UseCompactStateStorage = true; var markovChain = markovChainGenerator.GenerateMarkovChain(); } @@ -142,7 +142,7 @@ public void CreateMarkovChainWithHazardFaultsInState() var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; - var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.PossibleCollision, 50); + markovChainGenerator.AddFormulaToCheck(model.PossibleCollision); foreach (var fault in model.Faults) { var faultFormula = new FaultFormula(fault); @@ -165,12 +165,12 @@ public void CreateFaultAwareMarkovChainAllFaults() var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; markovChainGenerator.Configuration.EnableStaticPruningOptimization = false; + markovChainGenerator.AddFormulaToCheck(model.PossibleCollision); foreach (var fault in model.Faults) { var faultFormula = new FaultFormula(fault); markovChainGenerator.AddFormulaToCheck(faultFormula); } - var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.PossibleCollision, 50); markovChainGenerator.Configuration.UseCompactStateStorage = true; var markovChain = markovChainGenerator.GenerateMarkovChain(); } diff --git a/Models/Small Models/DeadReckoning/EvaluationTests.cs b/Models/Small Models/DeadReckoning/EvaluationTests.cs index 16a4d528..e88bbfa0 100644 --- a/Models/Small Models/DeadReckoning/EvaluationTests.cs +++ b/Models/Small Models/DeadReckoning/EvaluationTests.cs @@ -96,7 +96,7 @@ public void CreateMarkovChainWithHazards() var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; - var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 10); + markovChainGenerator.AddFormulaToCheck(model.Component.Hazard); markovChainGenerator.Configuration.UseCompactStateStorage = true; var markovChain = markovChainGenerator.GenerateMarkovChain(); } @@ -155,7 +155,7 @@ public void CreateMarkovChainWithHazardFaultsInState() var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; - var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 10); + markovChainGenerator.AddFormulaToCheck(model.Component.Hazard); foreach (var fault in model.Faults) { var faultFormula = new FaultFormula(fault); @@ -177,12 +177,12 @@ public void CreateFaultAwareMarkovChainAllFaults() var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; markovChainGenerator.Configuration.EnableStaticPruningOptimization = false; + markovChainGenerator.AddFormulaToCheck(model.Component.Hazard); foreach (var fault in model.Faults) { var faultFormula = new FaultFormula(fault); markovChainGenerator.AddFormulaToCheck(faultFormula); } - var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.Component.Hazard, 10); markovChainGenerator.Configuration.UseCompactStateStorage = true; var markovChain = markovChainGenerator.GenerateMarkovChain(); } diff --git a/Models/Small Models/DegradedMode/EvaluationTests.cs b/Models/Small Models/DegradedMode/EvaluationTests.cs index c270d679..5845916b 100644 --- a/Models/Small Models/DegradedMode/EvaluationTests.cs +++ b/Models/Small Models/DegradedMode/EvaluationTests.cs @@ -76,7 +76,7 @@ public void CreateMarkovChainWithHazards() var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; - var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.System.HazardActive, 50); + markovChainGenerator.AddFormulaToCheck(model.System.HazardActive); markovChainGenerator.Configuration.UseCompactStateStorage = true; var markovChain = markovChainGenerator.GenerateMarkovChain(); } @@ -135,7 +135,7 @@ public void CreateMarkovChainWithHazardFaultsInState() var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; - var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.System.HazardActive, 50); + markovChainGenerator.AddFormulaToCheck(model.System.HazardActive); foreach (var fault in model.Faults) { var faultFormula = new FaultFormula(fault); @@ -157,12 +157,12 @@ public void CreateFaultAwareMarkovChainAllFaults() var markovChainGenerator = new MarkovChainFromExecutableModelGenerator(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration }; markovChainGenerator.Configuration.SuccessorCapacity *= 2; markovChainGenerator.Configuration.EnableStaticPruningOptimization = false; + markovChainGenerator.AddFormulaToCheck(model.System.HazardActive); foreach (var fault in model.Faults) { var faultFormula = new FaultFormula(fault); markovChainGenerator.AddFormulaToCheck(faultFormula); } - var result = SafetySharpModelChecker.CalculateProbabilityToReachStateBounded(model, model.System.HazardActive, 50); markovChainGenerator.Configuration.UseCompactStateStorage = true; var markovChain = markovChainGenerator.GenerateMarkovChain(); }