Skip to content
Permalink
Browse files

Increase state space

  • Loading branch information...
joleuger committed Jan 24, 2018
1 parent df5da18 commit f1bd3fc8ef6b3deb5cdd928bbc6f450f812a7c41
Showing with 2 additions and 1 deletion.
  1. +2 −1 Models/Railroad Crossing/Analysis/EvaluationTests.cs
@@ -258,7 +258,7 @@ public void CalculateHazardSingleCoreAllFaultsWithOnce()
var markovChainGenerator = new MarkovChainFromExecutableModelGenerator<SafetySharpRuntimeModel>(createModel) { Configuration = SafetySharpModelChecker.TraversalConfiguration };
markovChainGenerator.Configuration.SuccessorCapacity *= 2;
markovChainGenerator.Configuration.EnableStaticPruningOptimization = false;
markovChainGenerator.Configuration.CpuCount = 1;
markovChainGenerator.Configuration.CpuCount = 3;
var onceFormula = new UnaryFormula(model.PossibleCollision, UnaryOperator.Once);
var onceFault1 = new UnaryFormula(new FaultFormula(model.Channel.MessageDropped), UnaryOperator.Once);
markovChainGenerator.AddFormulaToCheck(onceFault1);
@@ -271,6 +271,7 @@ public void CalculateHazardSingleCoreAllFaultsWithOnce()
markovChainGenerator.AddFormulaToCheck(formulaToCheck);
markovChainGenerator.Configuration.UseCompactStateStorage = true;
markovChainGenerator.Configuration.EnableEarlyTermination = false;
markovChainGenerator.Configuration.ModelCapacity = new ModelCapacityByModelSize(63000000L, 1000000000L);
var markovChain = markovChainGenerator.GenerateLabeledMarkovChain();

using (var modelChecker = new ConfigurationDependentLtmcModelChecker(markovChainGenerator.Configuration, markovChain, markovChainGenerator.Configuration.DefaultTraceOutput))

0 comments on commit f1bd3fc

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