Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #30 from pascalpfeil/master
Bachelorarbeit Pascal Pfeil
- Loading branch information
Showing
73 changed files
with
4,879 additions
and
3,446 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,6 +1,14 @@ | ||
| <?xml version="1.0" encoding="utf-8" ?> | ||
| <?xml version="1.0" encoding="utf-8"?> | ||
| <configuration> | ||
| <startup> | ||
| <supportedRuntime version="v4.0" sku=".NETFramework,Version=v4.5.2" /> | ||
| </startup> | ||
| <runtime> | ||
| <assemblyBinding xmlns="urn:schemas-microsoft-com:asm.v1"> | ||
| <dependentAssembly> | ||
| <assemblyIdentity name="System.ValueTuple" publicKeyToken="cc7b13ffcd2ddd51" culture="neutral" /> | ||
| <bindingRedirect oldVersion="0.0.0.0-4.0.3.0" newVersion="4.0.3.0" /> | ||
| </dependentAssembly> | ||
| </assemblyBinding> | ||
| </runtime> | ||
| </configuration> |
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,54 +1,51 @@ | ||
| using System; | ||
| using System.Collections.Generic; | ||
| using System.IO; | ||
| using System.Linq; | ||
| using System.Text; | ||
| using System.Threading.Tasks; | ||
| using ISSE.SafetyChecking.DiscreteTimeMarkovChain; | ||
| using ISSE.SafetyChecking.ExecutedModel; | ||
| using ISSE.SafetyChecking.Formula; | ||
| using ISSE.SafetyChecking.MarkovDecisionProcess.Unoptimized; | ||
| using ISSE.SafetyChecking.Modeling; | ||
| using NUnit.Framework; | ||
| using SafetyLustre; | ||
| using LtmcModelChecker = ISSE.SafetyChecking.LtmcModelChecker; | ||
| using System; | ||
| using System.Collections.Generic; | ||
| using System.IO; | ||
| using static Lustre_Models.TestUtil; | ||
| using LtmdpModelChecker = ISSE.SafetyChecking.LtmdpModelChecker; | ||
|
|
||
| namespace Lustre_Models | ||
| { | ||
| public class HazardProbabilityRangeTests | ||
| { | ||
| [Test] | ||
| public void TankRupture() | ||
| { | ||
| Program.ocExaplesPath = Directory.GetCurrentDirectory() + "\\"; | ||
| Program.modelChecking = true; | ||
| public class HazardProbabilityRangeTests | ||
| { | ||
| [Test] | ||
| public void TankRupture() | ||
| { | ||
| Formula invariant = new LustrePressureBelowThreshold(); | ||
| Formula hazard = new UnaryFormula(invariant, UnaryOperator.Not); | ||
| LustrePressureBelowThreshold.threshold = 60; | ||
| var faults = new List<Fault> | ||
| { | ||
| new TransientFault() { Name = "fault_switch", Identifier = 0, ProbabilityOfOccurrence = new Probability(3.0E-6) }, | ||
| new PermanentFault() { Name = "fault_k1", Identifier = 1, ProbabilityOfOccurrence = new Probability(3.0E-6) }, | ||
| new PermanentFault() { Name = "fault_k2", Identifier = 2, ProbabilityOfOccurrence = null }, | ||
| new PermanentFault() { Name = "fault_timer", Identifier = 3, ProbabilityOfOccurrence = new Probability(1.0E-5) }, | ||
| new PermanentFault() { Name = "fault_sensor", Identifier = 4, ProbabilityOfOccurrence = new Probability(1.0E-5) } | ||
| }; | ||
|
|
||
| Formula invariant = new LustrePressureBelowThreshold(); | ||
| Formula hazard = new UnaryFormula(invariant,UnaryOperator.Not); | ||
| LustrePressureBelowThreshold.threshold = 60; | ||
| var faults = new List<Fault>(); | ||
| faults.Add(new TransientFault() { Name = "fault_switch", Identifier = 0, ProbabilityOfOccurrence = new Probability(3.0E-6) }); | ||
| faults.Add(new PermanentFault() { Name = "fault_k1", Identifier = 1, ProbabilityOfOccurrence = new Probability(3.0E-6) }); | ||
| faults.Add(new PermanentFault() { Name = "fault_k2", Identifier = 2, ProbabilityOfOccurrence = null }); | ||
| faults.Add(new PermanentFault() { Name = "fault_timer", Identifier = 3, ProbabilityOfOccurrence = new Probability(1.0E-5) }); | ||
| faults.Add(new PermanentFault() { Name = "fault_sensor", Identifier = 4, ProbabilityOfOccurrence = new Probability(1.0E-5) }); | ||
| var createModel = LustreExecutableModel.CreateExecutedModelFromFormulasCreator(Path.Combine(AssemblyDirectory, "pressureTank.lus"), "TANK", faults.ToArray()); | ||
|
|
||
| var createModel = LustreExecutableModel.CreateExecutedModelFromFormulasCreator("pressureTank", faults.ToArray()); | ||
| var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<LustreExecutableModel>(createModel); | ||
| markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(10000, 1000000); | ||
| markovChainGenerator.Configuration.SuccessorCapacity *= 2; | ||
| markovChainGenerator.Configuration.EnableStaticPruningOptimization = true; | ||
| markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuiltInLtmdp; | ||
| markovChainGenerator.AddFormulaToCheck(hazard); | ||
| markovChainGenerator.Configuration.UseCompactStateStorage = true; | ||
| markovChainGenerator.Configuration.EnableEarlyTermination = false; | ||
| var markovChain = markovChainGenerator.GenerateLabeledTransitionMarkovDecisionProcess(); | ||
|
|
||
| var markovChainGenerator = new MarkovDecisionProcessFromExecutableModelGenerator<LustreExecutableModel>(createModel); | ||
| markovChainGenerator.Configuration.SuccessorCapacity *= 2; | ||
| markovChainGenerator.Configuration.EnableStaticPruningOptimization = true; | ||
| markovChainGenerator.Configuration.LtmdpModelChecker = LtmdpModelChecker.BuiltInLtmdp; | ||
| markovChainGenerator.AddFormulaToCheck(hazard); | ||
| markovChainGenerator.Configuration.UseCompactStateStorage = true; | ||
| markovChainGenerator.Configuration.EnableEarlyTermination = false; | ||
| var markovChain = markovChainGenerator.GenerateLabeledTransitionMarkovDecisionProcess(); | ||
| var ltmcModelChecker = new ConfigurationDependentLtmdpModelChecker(markovChainGenerator.Configuration, markovChain, Console.Out); | ||
| var finallyHazard = new BoundedUnaryFormula(hazard, UnaryOperator.Finally, 200); | ||
| var result = ltmcModelChecker.CalculateProbabilityRange(finallyHazard); | ||
|
|
||
| var ltmcModelChecker = new ConfigurationDependentLtmdpModelChecker(markovChainGenerator.Configuration, markovChain, Console.Out); | ||
| var finallyHazard = new BoundedUnaryFormula(hazard,UnaryOperator.Finally, 200); | ||
| var result = ltmcModelChecker.CalculateProbabilityRange(finallyHazard); | ||
|
|
||
| Console.Write($"Probability of hazard: {result}"); | ||
| } | ||
| } | ||
| Console.Write($"Probability of hazard: {result}"); | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,85 +1,84 @@ | ||
| using System; | ||
| using System.Collections.Generic; | ||
| using System.IO; | ||
| using System.Linq; | ||
| using System.Text; | ||
| using System.Threading.Tasks; | ||
| using ISSE.SafetyChecking; | ||
| using ISSE.SafetyChecking.DiscreteTimeMarkovChain; | ||
| using ISSE.SafetyChecking.DiscreteTimeMarkovChain; | ||
| using ISSE.SafetyChecking.Formula; | ||
| using ISSE.SafetyChecking.Modeling; | ||
| using NUnit.Framework; | ||
| using SafetyLustre; | ||
| using LtmcModelChecker = ISSE.SafetyChecking.LtmcModelChecker; | ||
| using System; | ||
| using System.Collections.Generic; | ||
| using System.IO; | ||
| using static Lustre_Models.TestUtil; | ||
| using static SafetyLustre.LustreSafetyAnalysis; | ||
|
|
||
| namespace Lustre_Models | ||
| { | ||
| public class HazardProbabilityTests | ||
| { | ||
| [Test] | ||
| public void TankRupture() | ||
| { | ||
| Program.ocExaplesPath = Directory.GetCurrentDirectory() + "\\"; | ||
| public class HazardProbabilityTests | ||
| { | ||
| [Test] | ||
| public void TankRupture() | ||
| { | ||
| Formula invariant = new LustrePressureBelowThreshold(); | ||
| Formula hazard = new UnaryFormula(invariant, UnaryOperator.Not); | ||
| LustrePressureBelowThreshold.threshold = 60; | ||
| var faults = new List<Fault> | ||
| { | ||
| new TransientFault() { Name = "fault_switch", Identifier = 0, ProbabilityOfOccurrence = new Probability(3.0E-6) }, | ||
| new PermanentFault() { Name = "fault_k1", Identifier = 1, ProbabilityOfOccurrence = new Probability(3.0E-6) }, | ||
| new PermanentFault() { Name = "fault_k2", Identifier = 2, ProbabilityOfOccurrence = new Probability(3.0E-6) }, | ||
| new PermanentFault() { Name = "fault_timer", Identifier = 3, ProbabilityOfOccurrence = new Probability(1.0E-5) }, | ||
| new PermanentFault() { Name = "fault_sensor", Identifier = 4, ProbabilityOfOccurrence = new Probability(1.0E-5) } | ||
| }; | ||
| var modelChecker = new LustreMarkovChainFromExecutableModelGenerator(Path.Combine(AssemblyDirectory, "pressureTank.lus"), "TANK", faults); | ||
| modelChecker.AddFormulaToCheck(hazard); | ||
| modelChecker.Configuration.UseCompactStateStorage = true; | ||
| var lmc = modelChecker.GenerateLabeledMarkovChain(); | ||
|
|
||
| var ltmcModelChecker = new BuiltinLtmcModelChecker(lmc, Console.Out); | ||
| var finallyHazard = new BoundedUnaryFormula(hazard, UnaryOperator.Finally, 200); | ||
| var result = ltmcModelChecker.CalculateProbability(finallyHazard); | ||
|
|
||
| Formula invariant = new LustrePressureBelowThreshold(); | ||
| Formula hazard = new UnaryFormula(invariant,UnaryOperator.Not); | ||
| LustrePressureBelowThreshold.threshold = 60; | ||
| var faults = new List<Fault>(); | ||
| faults.Add(new TransientFault() { Name = "fault_switch", Identifier = 0, ProbabilityOfOccurrence = new Probability(3.0E-6) }); | ||
| faults.Add(new PermanentFault() { Name = "fault_k1", Identifier = 1, ProbabilityOfOccurrence = new Probability(3.0E-6) }); | ||
| faults.Add(new PermanentFault() { Name = "fault_k2", Identifier = 2, ProbabilityOfOccurrence = new Probability(3.0E-6) }); | ||
| faults.Add(new PermanentFault() { Name = "fault_timer", Identifier = 3, ProbabilityOfOccurrence = new Probability(1.0E-5) }); | ||
| faults.Add(new PermanentFault() { Name = "fault_sensor", Identifier = 4, ProbabilityOfOccurrence = new Probability(1.0E-5) }); | ||
| var modelChecker = new LustreMarkovChainFromExecutableModelGenerator("pressureTank", faults); | ||
| modelChecker.AddFormulaToCheck(hazard); | ||
| modelChecker.Configuration.UseCompactStateStorage = true; | ||
| var lmc = modelChecker.GenerateLabeledMarkovChain(); | ||
| Console.Write($"Probability of hazard: {result}"); | ||
| } | ||
|
|
||
| var ltmcModelChecker = new BuiltinLtmcModelChecker(lmc, Console.Out); | ||
| var finallyHazard = new BoundedUnaryFormula(hazard,UnaryOperator.Finally, 200); | ||
| var result = ltmcModelChecker.CalculateProbability(finallyHazard); | ||
|
|
||
| Console.Write($"Probability of hazard: {result}"); | ||
| } | ||
| [Test] | ||
| public void Parametric() | ||
| { | ||
| Formula invariant = new LustrePressureBelowThreshold(); | ||
| Formula hazard = new UnaryFormula(invariant, UnaryOperator.Not); | ||
| LustrePressureBelowThreshold.threshold = 60; | ||
| var faultK1 = new PermanentFault() { Name = "fault_k1", Identifier = 1, ProbabilityOfOccurrence = new Probability(3.0E-6) }; | ||
| var faultK2 = new PermanentFault() { Name = "fault_k2", Identifier = 2, ProbabilityOfOccurrence = new Probability(3.0E-6) }; | ||
| var faultSensor = new PermanentFault() { Name = "fault_sensor", Identifier = 4, ProbabilityOfOccurrence = new Probability(1.0E-5) }; | ||
| var faults = new[] { faultK1, faultK2, faultSensor }; | ||
|
|
||
| [Test] | ||
| public void Parametric() | ||
| { | ||
| Program.ocExaplesPath = Directory.GetCurrentDirectory() + "\\"; | ||
| var parameter = new QuantitativeParametricAnalysisParameter | ||
| { | ||
| StateFormula = hazard, | ||
| Bound = null, | ||
| From = 3.0E-7, | ||
| To = 3.0E-5, | ||
| Steps = 25, | ||
| }; | ||
|
|
||
| Formula invariant = new LustrePressureBelowThreshold(); | ||
| Formula hazard = new UnaryFormula(invariant, UnaryOperator.Not); | ||
| LustrePressureBelowThreshold.threshold = 60; | ||
| var faultK1 = new PermanentFault() { Name = "fault_k1", Identifier = 1, ProbabilityOfOccurrence = new Probability(3.0E-6) }; | ||
| var faultK2 = new PermanentFault() { Name = "fault_k2", Identifier = 2, ProbabilityOfOccurrence = new Probability(3.0E-6) }; | ||
| var faultSensor = new PermanentFault() { Name = "fault_sensor", Identifier = 4, ProbabilityOfOccurrence = new Probability(1.0E-5) }; | ||
| var faults = new []{ faultK1, faultK2, faultSensor }; | ||
|
|
||
| var parameter = new QuantitativeParametricAnalysisParameter | ||
| { | ||
| StateFormula = hazard, | ||
| Bound = null, | ||
| From = 3.0E-7, | ||
| To = 3.0E-5, | ||
| Steps = 25, | ||
| UpdateParameterInModel = value => { faultK1.ProbabilityOfOccurrence=new Probability(value); } | ||
| }; | ||
| var result = LustreModelChecker.ConductQuantitativeParametricAnalysis("pressureTank", faults, parameter); | ||
| var fileWriter = new StreamWriter("pressureTank_varyK1.csv", append: false); | ||
| result.ToCsv(fileWriter); | ||
| fileWriter.Close(); | ||
| using (var fileWriter = new StreamWriter(Path.Combine(AssemblyDirectory, "pressureTank_varyK1.csv"), append: false)) | ||
| { | ||
| parameter.UpdateParameterInModel = value => { faultK1.ProbabilityOfOccurrence = new Probability(value); }; | ||
| var result = LustreModelChecker.ConductQuantitativeParametricAnalysis(Path.Combine(AssemblyDirectory, "pressureTank.lus"), "TANK", faults, parameter); | ||
| result.ToCsv(fileWriter); | ||
| } | ||
|
|
||
| parameter.UpdateParameterInModel = value => { faultK2.ProbabilityOfOccurrence = new Probability(value); }; | ||
| result = LustreModelChecker.ConductQuantitativeParametricAnalysis("pressureTank", faults, parameter); | ||
| fileWriter = new StreamWriter("pressureTank_varyK2.csv", append: false); | ||
| result.ToCsv(fileWriter); | ||
| fileWriter.Close(); | ||
| using (var fileWriter = new StreamWriter(Path.Combine(AssemblyDirectory, "pressureTank_varyK2.csv"), append: false)) | ||
| { | ||
| parameter.UpdateParameterInModel = value => { faultK2.ProbabilityOfOccurrence = new Probability(value); }; | ||
| var result = LustreModelChecker.ConductQuantitativeParametricAnalysis(Path.Combine(AssemblyDirectory, "pressureTank.lus"), "TANK", faults, parameter); | ||
| result.ToCsv(fileWriter); | ||
| } | ||
|
|
||
| parameter.UpdateParameterInModel = value => { faultSensor.ProbabilityOfOccurrence = new Probability(value); }; | ||
| result = LustreModelChecker.ConductQuantitativeParametricAnalysis("pressureTank", faults, parameter); | ||
| fileWriter = new StreamWriter("pressureTank_varySensor.csv", append: false); | ||
| result.ToCsv(fileWriter); | ||
| fileWriter.Close(); | ||
| } | ||
| } | ||
| using (var fileWriter = new StreamWriter(Path.Combine(AssemblyDirectory, "pressureTank_varySensor.csv"), append: false)) | ||
| { | ||
| parameter.UpdateParameterInModel = value => { faultSensor.ProbabilityOfOccurrence = new Probability(value); }; | ||
| var result = LustreModelChecker.ConductQuantitativeParametricAnalysis(Path.Combine(AssemblyDirectory, "pressureTank.lus"), "TANK", faults, parameter); | ||
| result.ToCsv(fileWriter); | ||
| } | ||
| } | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.