File List

Here is a list of all files with brief descriptions:

[detail level 1234567]

▼ src
► storm
► adapters
AddExpressionAdapter.cpp
AddExpressionAdapter.h
DereferenceIteratorAdapter.h
eigen.h
EigenAdapter.cpp
EigenAdapter.h
ExprttkAdapter.h
gmm.h
GmmxxAdapter.cpp
GmmxxAdapter.h
IntelTbbAdapter.h
JsonAdapter.cpp
JsonAdapter.h
JsonForward.h
MathsatExpressionAdapter.cpp
MathsatExpressionAdapter.h
RationalFunctionAdapter.cpp
RationalFunctionAdapter.h
RationalFunctionAdapter_Private.cpp
RationalFunctionAdapter_Private.h
RationalFunctionForward.h
RationalNumberAdapter.h
RationalNumberForward.h
Smt2ExpressionAdapter.h
SpotAdapter.h
sylvan.cpp
sylvan.h
Z3ExpressionAdapter.cpp
Z3ExpressionAdapter.h
► analysis
GraphConditions.cpp
GraphConditions.h
► api
bisimulation.h
builder.h
export.cpp
export.h
properties.cpp
properties.h
storm.h
transformation.h
verification.h
► automata
AcceptanceCondition.cpp
AcceptanceCondition.h
APSet.cpp
APSet.h
DeterministicAutomaton.cpp
DeterministicAutomaton.h
HOAConsumerDA.h
HOAConsumerDAHeader.h
HOAHeader.h
LTL2DeterministicAutomaton.cpp
LTL2DeterministicAutomaton.h
► builder
BuilderOptions.cpp
BuilderOptions.h
BuilderType.cpp
BuilderType.h
DdJaniModelBuilder.cpp
DdJaniModelBuilder.h
DdPrismModelBuilder.cpp
DdPrismModelBuilder.h
ExplicitModelBuilder.cpp
ExplicitModelBuilder.h
ExplorationOrder.cpp
ExplorationOrder.h
ParallelCompositionBuilder.cpp
ParallelCompositionBuilder.h
RewardModelBuilder.cpp
RewardModelBuilder.h
RewardModelInformation.cpp
RewardModelInformation.h
StateAndChoiceInformationBuilder.cpp
StateAndChoiceInformationBuilder.h
TerminalStatesGetter.cpp
TerminalStatesGetter.h
► environment
► modelchecker
AllModelCheckerEnvironments.h
ModelCheckerEnvironment.cpp
ModelCheckerEnvironment.h
MultiObjectiveModelCheckerEnvironment.cpp
MultiObjectiveModelCheckerEnvironment.h
► solver
AllSolverEnvironments.h
EigenSolverEnvironment.cpp
EigenSolverEnvironment.h
GameSolverEnvironment.cpp
GameSolverEnvironment.h
GmmxxSolverEnvironment.cpp
GmmxxSolverEnvironment.h
LongRunAverageSolverEnvironment.cpp
LongRunAverageSolverEnvironment.h
MinMaxLpSolverEnvironment.cpp
MinMaxLpSolverEnvironment.h
MinMaxSolverEnvironment.cpp
MinMaxSolverEnvironment.h
MultiplierEnvironment.cpp
MultiplierEnvironment.h
NativeSolverEnvironment.cpp
NativeSolverEnvironment.h
OviSolverEnvironment.cpp
OviSolverEnvironment.h
SolverEnvironment.cpp
SolverEnvironment.h
TimeBoundedSolverEnvironment.cpp
TimeBoundedSolverEnvironment.h
TopologicalSolverEnvironment.cpp
TopologicalSolverEnvironment.h
Environment.cpp
Environment.h
SubEnvironment.cpp
SubEnvironment.h
► exceptions
AbortException.h
AmbiguousModelException.h
ArgumentUnificationException.h
BaseException.cpp
BaseException.h
ExceptionMacros.h
ExpressionEvaluationException.h
FileIoException.h
FormatUnsupportedBySolverException.h
GurobiLicenseException.h
IllegalArgumentException.h
IllegalArgumentTypeException.h
IllegalArgumentValueException.h
IllegalFunctionCallException.h
InternalException.h
InternalTypeErrorException.h
InvalidAccessException.h
InvalidArgumentException.h
InvalidEnvironmentException.h
InvalidJaniException.h
InvalidModelException.h
InvalidOperationException.h
InvalidOptionException.h
InvalidPropertyException.h
InvalidSettingsException.h
InvalidSolverSettingsException.h
InvalidStateException.h
InvalidTypeException.h
NoConvergenceException.h
NotImplementedException.h
NotSupportedException.h
OptionParserException.h
OptionUnificationException.h
OutOfRangeException.h
PrecisionExceededException.h
UncheckedRequirementException.h
UnexpectedException.h
UnmetRequirementException.h
UnsupportedModelException.h
WrongFormatException.h
► generator
ArrayVariableReplacementInformation.cpp
ArrayVariableReplacementInformation.h
Choice.cpp
Choice.h
CompressedState.cpp
CompressedState.h
Distribution.cpp
Distribution.h
DistributionEntry.cpp
DistributionEntry.h
JaniNextStateGenerator.cpp
JaniNextStateGenerator.h
NextStateGenerator.cpp
NextStateGenerator.h
PrismNextStateGenerator.cpp
PrismNextStateGenerator.h
StateBehavior.cpp
StateBehavior.h
TransientVariableInformation.cpp
TransientVariableInformation.h
VariableInformation.cpp
VariableInformation.h
► io
DDEncodingExporter.cpp
DDEncodingExporter.h
DirectEncodingExporter.cpp
DirectEncodingExporter.h
export.h
file.h
ModelExportFormat.cpp
ModelExportFormat.h
► logic
AtomicExpressionFormula.cpp
AtomicExpressionFormula.h
AtomicLabelFormula.cpp
AtomicLabelFormula.h
BinaryBooleanOperatorType.h
BinaryBooleanPathFormula.cpp
BinaryBooleanPathFormula.h
BinaryBooleanStateFormula.cpp
BinaryBooleanStateFormula.h
BinaryPathFormula.cpp
BinaryPathFormula.h
BinaryStateFormula.cpp
BinaryStateFormula.h
BooleanLiteralFormula.cpp
BooleanLiteralFormula.h
Bound.cpp
Bound.h
BoundedUntilFormula.cpp
BoundedUntilFormula.h
CloneVisitor.cpp
CloneVisitor.h
ComparisonType.cpp
ComparisonType.h
ConditionalFormula.cpp
ConditionalFormula.h
CumulativeRewardFormula.cpp
CumulativeRewardFormula.h
EventuallyFormula.cpp
EventuallyFormula.h
ExpectedTimeToExpectedRewardVisitor.cpp
ExpectedTimeToExpectedRewardVisitor.h
ExpressionSubstitutionVisitor.cpp
ExpressionSubstitutionVisitor.h
ExtractMaximalStateFormulasVisitor.cpp
ExtractMaximalStateFormulasVisitor.h
Formula.cpp
Formula.h
FormulaContext.cpp
FormulaContext.h
FormulaInformation.cpp
FormulaInformation.h
FormulaInformationVisitor.cpp
FormulaInformationVisitor.h
Formulas.h
FormulasForwardDeclarations.h
FormulaVisitor.h
FragmentChecker.cpp
FragmentChecker.h
FragmentSpecification.cpp
FragmentSpecification.h
GameFormula.cpp
GameFormula.h
GloballyFormula.cpp
GloballyFormula.h
HOAPathFormula.cpp
HOAPathFormula.h
InstantaneousRewardFormula.cpp
InstantaneousRewardFormula.h
LabelSubstitutionVisitor.cpp
LabelSubstitutionVisitor.h
LiftableTransitionRewardsVisitor.cpp
LiftableTransitionRewardsVisitor.h
LongRunAverageOperatorFormula.cpp
LongRunAverageOperatorFormula.h
LongRunAverageRewardFormula.cpp
LongRunAverageRewardFormula.h
MultiObjectiveFormula.cpp
MultiObjectiveFormula.h
NextFormula.cpp
NextFormula.h
OperatorFormula.cpp
OperatorFormula.h
PathFormula.cpp
PathFormula.h
PlayerCoalition.cpp
PlayerCoalition.h
ProbabilityOperatorFormula.cpp
ProbabilityOperatorFormula.h
QuantileFormula.cpp
QuantileFormula.h
RewardAccumulation.cpp
RewardAccumulation.h
RewardAccumulationEliminationVisitor.cpp
RewardAccumulationEliminationVisitor.h
RewardModelNameSubstitutionVisitor.cpp
RewardModelNameSubstitutionVisitor.h
RewardOperatorFormula.cpp
RewardOperatorFormula.h
StateFormula.cpp
StateFormula.h
TimeBound.cpp
TimeBound.h
TimeBoundType.h
TimeOperatorFormula.cpp
TimeOperatorFormula.h
ToExpressionVisitor.cpp
ToExpressionVisitor.h
ToPrefixStringVisitor.cpp
ToPrefixStringVisitor.h
TotalRewardFormula.cpp
TotalRewardFormula.h
UnaryBooleanOperatorType.h
UnaryBooleanPathFormula.cpp
UnaryBooleanPathFormula.h
UnaryBooleanStateFormula.cpp
UnaryBooleanStateFormula.h
UnaryPathFormula.cpp
UnaryPathFormula.h
UnaryStateFormula.cpp
UnaryStateFormula.h
UntilFormula.cpp
UntilFormula.h
► modelchecker
► csl
► helper
HybridCtmcCslHelper.cpp
HybridCtmcCslHelper.h
HybridMarkovAutomatonCslHelper.cpp
HybridMarkovAutomatonCslHelper.h
SparseCtmcCslHelper.cpp
SparseCtmcCslHelper.h
SparseMarkovAutomatonCslHelper.cpp
SparseMarkovAutomatonCslHelper.h
SymbolicCtmcCslHelper.cpp
SymbolicCtmcCslHelper.h
HybridCtmcCslModelChecker.cpp
HybridCtmcCslModelChecker.h
HybridMarkovAutomatonCslModelChecker.cpp
HybridMarkovAutomatonCslModelChecker.h
SparseCtmcCslModelChecker.cpp
SparseCtmcCslModelChecker.h
SparseMarkovAutomatonCslModelChecker.cpp
SparseMarkovAutomatonCslModelChecker.h
► exploration
Bounds.cpp
Bounds.h
ExplorationInformation.cpp
ExplorationInformation.h
SparseExplorationModelChecker.cpp
SparseExplorationModelChecker.h
StateGeneration.cpp
StateGeneration.h
Statistics.cpp
Statistics.h
► helper
► finitehorizon
SparseDeterministicStepBoundedHorizonHelper.cpp
SparseDeterministicStepBoundedHorizonHelper.h
SparseNondeterministicStepBoundedHorizonHelper.cpp
SparseNondeterministicStepBoundedHorizonHelper.h
► indefinitehorizon
► visitingtimes
SparseDeterministicVisitingTimesHelper.cpp
SparseDeterministicVisitingTimesHelper.h
► infinitehorizon
► internal
ComponentUtility.h
LraViHelper.cpp
LraViHelper.h
HybridInfiniteHorizonHelper.cpp
HybridInfiniteHorizonHelper.h
SparseDeterministicInfiniteHorizonHelper.cpp
SparseDeterministicInfiniteHorizonHelper.h
SparseInfiniteHorizonHelper.cpp
SparseInfiniteHorizonHelper.h
SparseNondeterministicInfiniteHorizonHelper.cpp
SparseNondeterministicInfiniteHorizonHelper.h
SteadyStateDistributionAlgorithm.h
► ltl
► internal
SparseLTLSchedulerHelper.cpp
SparseLTLSchedulerHelper.h
SparseLTLHelper.cpp
SparseLTLHelper.h
► utility
SetInformationFromCheckTask.h
SetInformationFromOtherHelper.h
ModelCheckerHelper.cpp
ModelCheckerHelper.h
SingleValueModelCheckerHelper.cpp
SingleValueModelCheckerHelper.h
► hints
ExplicitModelCheckerHint.cpp
ExplicitModelCheckerHint.h
ModelCheckerHint.cpp
ModelCheckerHint.h
► lexicographic
► spotHelper
spotProduct.cpp
spotProduct.h
lexicographicModelCheckerHelper.cpp
lexicographicModelCheckerHelper.h
lexicographicModelChecking.cpp
lexicographicModelChecking.h
► multiobjective
► constraintbased
SparseCbAchievabilityQuery.cpp
SparseCbAchievabilityQuery.h
SparseCbQuery.cpp
SparseCbQuery.h
► deterministicScheds
DeterministicSchedsAchievabilityChecker.cpp
DeterministicSchedsAchievabilityChecker.h
DeterministicSchedsLpChecker.cpp
DeterministicSchedsLpChecker.h
DeterministicSchedsObjectiveHelper.cpp
DeterministicSchedsObjectiveHelper.h
DeterministicSchedsParetoExplorer.cpp
DeterministicSchedsParetoExplorer.h
VisitingTimesHelper.cpp
VisitingTimesHelper.h
► pcaa
PcaaWeightVectorChecker.cpp
PcaaWeightVectorChecker.h
RewardBoundedMdpPcaaWeightVectorChecker.cpp
RewardBoundedMdpPcaaWeightVectorChecker.h
SparsePcaaAchievabilityQuery.cpp
SparsePcaaAchievabilityQuery.h
SparsePcaaParetoQuery.cpp
SparsePcaaParetoQuery.h
SparsePcaaQuantitativeQuery.cpp
SparsePcaaQuantitativeQuery.h
SparsePcaaQuery.cpp
SparsePcaaQuery.h
StandardMaPcaaWeightVectorChecker.cpp
StandardMaPcaaWeightVectorChecker.h
StandardMdpPcaaWeightVectorChecker.cpp
StandardMdpPcaaWeightVectorChecker.h
StandardPcaaWeightVectorChecker.cpp
StandardPcaaWeightVectorChecker.h
► preprocessing
SparseMultiObjectivePreprocessor.cpp
SparseMultiObjectivePreprocessor.h
SparseMultiObjectivePreprocessorResult.h
SparseMultiObjectiveRewardAnalysis.cpp
SparseMultiObjectiveRewardAnalysis.h
multiObjectiveModelChecking.cpp
multiObjectiveModelChecking.h
MultiObjectiveModelCheckingMethod.cpp
MultiObjectiveModelCheckingMethod.h
MultiObjectivePostprocessing.cpp
MultiObjectivePostprocessing.h
Objective.h
► prctl
► helper
► rewardbounded
CostLimitClosure.cpp
CostLimitClosure.h
Dimension.h
EpochManager.cpp
EpochManager.h
EpochModel.cpp
EpochModel.h
MemoryStateManager.cpp
MemoryStateManager.h
MultiDimensionalRewardUnfolding.cpp
MultiDimensionalRewardUnfolding.h
ProductModel.cpp
ProductModel.h
QuantileHelper.cpp
QuantileHelper.h
BaierUpperRewardBoundsComputer.cpp
BaierUpperRewardBoundsComputer.h
DsMpiUpperRewardBoundsComputer.cpp
DsMpiUpperRewardBoundsComputer.h
HybridDtmcPrctlHelper.cpp
HybridDtmcPrctlHelper.h
HybridMdpPrctlHelper.cpp
HybridMdpPrctlHelper.h
MDPModelCheckingHelperReturnType.h
SemanticSolutionType.h
SparseDtmcPrctlHelper.cpp
SparseDtmcPrctlHelper.h
SparseMdpEndComponentInformation.cpp
SparseMdpEndComponentInformation.h
SparseMdpPrctlHelper.cpp
SparseMdpPrctlHelper.h
SymbolicDtmcPrctlHelper.cpp
SymbolicDtmcPrctlHelper.h
SymbolicMdpPrctlHelper.cpp
SymbolicMdpPrctlHelper.h
HybridDtmcPrctlModelChecker.cpp
HybridDtmcPrctlModelChecker.h
HybridMdpPrctlModelChecker.cpp
HybridMdpPrctlModelChecker.h
SparseDtmcPrctlModelChecker.cpp
SparseDtmcPrctlModelChecker.h
SparseMdpPrctlModelChecker.cpp
SparseMdpPrctlModelChecker.h
SymbolicDtmcPrctlModelChecker.cpp
SymbolicDtmcPrctlModelChecker.h
SymbolicMdpPrctlModelChecker.cpp
SymbolicMdpPrctlModelChecker.h
► propositional
SparsePropositionalModelChecker.cpp
SparsePropositionalModelChecker.h
SymbolicPropositionalModelChecker.cpp
SymbolicPropositionalModelChecker.h
► reachability
SparseDtmcEliminationModelChecker.cpp
SparseDtmcEliminationModelChecker.h
► results
CheckResult.cpp
CheckResult.h
ExplicitParetoCurveCheckResult.cpp
ExplicitParetoCurveCheckResult.h
ExplicitQualitativeCheckResult.cpp
ExplicitQualitativeCheckResult.h
ExplicitQuantitativeCheckResult.cpp
ExplicitQuantitativeCheckResult.h
FilterType.cpp
FilterType.h
HybridQuantitativeCheckResult.cpp
HybridQuantitativeCheckResult.h
LexicographicCheckResult.cpp
LexicographicCheckResult.h
ParetoCurveCheckResult.cpp
ParetoCurveCheckResult.h
QualitativeCheckResult.cpp
QualitativeCheckResult.h
QuantitativeCheckResult.cpp
QuantitativeCheckResult.h
SymbolicParetoCurveCheckResult.cpp
SymbolicParetoCurveCheckResult.h
SymbolicQualitativeCheckResult.cpp
SymbolicQualitativeCheckResult.h
SymbolicQuantitativeCheckResult.cpp
SymbolicQuantitativeCheckResult.h
► rpatl
SparseSmgRpatlModelChecker.cpp
SparseSmgRpatlModelChecker.h
AbstractModelChecker.cpp
AbstractModelChecker.h
CheckTask.h
► models
► sparse
ChoiceLabeling.cpp
ChoiceLabeling.h
Ctmc.cpp
Ctmc.h
DeterministicModel.cpp
DeterministicModel.h
Dtmc.cpp
Dtmc.h
ItemLabeling.cpp
ItemLabeling.h
MarkovAutomaton.cpp
MarkovAutomaton.h
Mdp.cpp
Mdp.h
Model.cpp
Model.h
NondeterministicModel.cpp
NondeterministicModel.h
Pomdp.cpp
Pomdp.h
Smg.cpp
Smg.h
StandardRewardModel.cpp
StandardRewardModel.h
StateAnnotation.h
StateLabeling.cpp
StateLabeling.h
StochasticTwoPlayerGame.cpp
StochasticTwoPlayerGame.h
► symbolic
Ctmc.cpp
Ctmc.h
DeterministicModel.cpp
DeterministicModel.h
Dtmc.cpp
Dtmc.h
MarkovAutomaton.cpp
MarkovAutomaton.h
Mdp.cpp
Mdp.h
Model.cpp
Model.h
NondeterministicModel.cpp
NondeterministicModel.h
StandardRewardModel.cpp
StandardRewardModel.h
StochasticTwoPlayerGame.cpp
StochasticTwoPlayerGame.h
Model.h
ModelBase.cpp
ModelBase.h
ModelRepresentation.cpp
ModelRepresentation.h
ModelType.cpp
ModelType.h
► parser
CSVParser.cpp
CSVParser.h
► settings
► modules
AbstractionSettings.cpp
AbstractionSettings.h
BisimulationSettings.cpp
BisimulationSettings.h
BuildSettings.cpp
BuildSettings.h
CoreSettings.cpp
CoreSettings.h
CuddSettings.cpp
CuddSettings.h
DebugSettings.cpp
DebugSettings.h
EigenEquationSolverSettings.cpp
EigenEquationSolverSettings.h
EliminationSettings.cpp
EliminationSettings.h
ExplorationSettings.cpp
ExplorationSettings.h
GameSolverSettings.cpp
GameSolverSettings.h
GeneralSettings.cpp
GeneralSettings.h
GlpkSettings.cpp
GlpkSettings.h
GmmxxEquationSolverSettings.cpp
GmmxxEquationSolverSettings.h
GurobiSettings.cpp
GurobiSettings.h
HintSettings.cpp
HintSettings.h
IOSettings.cpp
IOSettings.h
LongRunAverageSolverSettings.cpp
LongRunAverageSolverSettings.h
MinMaxEquationSolverSettings.cpp
MinMaxEquationSolverSettings.h
ModelCheckerSettings.cpp
ModelCheckerSettings.h
ModuleSettings.cpp
ModuleSettings.h
MultiObjectiveSettings.cpp
MultiObjectiveSettings.h
MultiplierSettings.cpp
MultiplierSettings.h
NativeEquationSolverSettings.cpp
NativeEquationSolverSettings.h
OviSolverSettings.cpp
OviSolverSettings.h
ResourceSettings.cpp
ResourceSettings.h
Smt2SmtSolverSettings.cpp
Smt2SmtSolverSettings.h
SylvanSettings.cpp
SylvanSettings.h
TimeBoundedSolverSettings.cpp
TimeBoundedSolverSettings.h
TopologicalEquationSolverSettings.cpp
TopologicalEquationSolverSettings.h
TransformationSettings.cpp
TransformationSettings.h
Argument.cpp
Argument.h
ArgumentBase.cpp
ArgumentBase.h
ArgumentBuilder.h
ArgumentType.cpp
ArgumentType.h
ArgumentTypeInferationHelper.cpp
ArgumentTypeInferationHelper.h
ArgumentValidators.cpp
ArgumentValidators.h
Option.cpp
Option.h
OptionBuilder.h
SettingMemento.cpp
SettingMemento.h
SettingsManager.cpp
SettingsManager.h
► simulator
DiscreteTimeSparseModelSimulator.cpp
DiscreteTimeSparseModelSimulator.h
PrismProgramSimulator.cpp
PrismProgramSimulator.h
► solver
► helper
AcyclicSolverHelper.h
IntervalterationHelper.cpp
IntervalterationHelper.h
OptimisticValueIterationHelper.cpp
OptimisticValueIterationHelper.h
RationalSearchHelper.cpp
RationalSearchHelper.h
SchedulerTrackingHelper.cpp
SchedulerTrackingHelper.h
SoundValueIterationHelper.cpp
SoundValueIterationHelper.h
ValueIterationHelper.cpp
ValueIterationHelper.h
ValueIterationOperator.cpp
ValueIterationOperator.h
ValueIterationOperatorForward.h
► multiplier
GmmxxMultiplier.cpp
GmmxxMultiplier.h
Multiplier.cpp
Multiplier.h
NativeMultiplier.cpp
NativeMultiplier.h
► stateelimination
ConditionalStateEliminator.cpp
ConditionalStateEliminator.h
DynamicStatePriorityQueue.cpp
DynamicStatePriorityQueue.h
EliminatorBase.cpp
EliminatorBase.h
EquationSystemEliminator.cpp
EquationSystemEliminator.h
MultiValueStateEliminator.cpp
MultiValueStateEliminator.h
NondeterministicModelStateEliminator.cpp
NondeterministicModelStateEliminator.h
PrioritizedStateEliminator.cpp
PrioritizedStateEliminator.h
StateEliminator.cpp
StateEliminator.h
StatePriorityQueue.cpp
StatePriorityQueue.h
StaticStatePriorityQueue.cpp
StaticStatePriorityQueue.h
AbstractEquationSolver.cpp
AbstractEquationSolver.h
AcyclicLinearEquationSolver.cpp
AcyclicLinearEquationSolver.h
AcyclicMinMaxLinearEquationSolver.cpp
AcyclicMinMaxLinearEquationSolver.h
EigenLinearEquationSolver.cpp
EigenLinearEquationSolver.h
EliminationLinearEquationSolver.cpp
EliminationLinearEquationSolver.h
GameSolver.cpp
GameSolver.h
GlpkLpSolver.cpp
GlpkLpSolver.h
GmmxxLinearEquationSolver.cpp
GmmxxLinearEquationSolver.h
GurobiLpSolver.cpp
GurobiLpSolver.h
IterativeMinMaxLinearEquationSolver.cpp
IterativeMinMaxLinearEquationSolver.h
LinearEquationSolver.cpp
LinearEquationSolver.h
LinearEquationSolverProblemFormat.cpp
LinearEquationSolverProblemFormat.h
LinearEquationSolverRequirements.cpp
LinearEquationSolverRequirements.h
LpMinMaxLinearEquationSolver.cpp
LpMinMaxLinearEquationSolver.h
LpSolver.cpp
LpSolver.h
MathsatSmtSolver.cpp
MathsatSmtSolver.h
MinMaxLinearEquationSolver.cpp
MinMaxLinearEquationSolver.h
MinMaxLinearEquationSolverRequirements.cpp
MinMaxLinearEquationSolverRequirements.h
MultiplicationStyle.cpp
MultiplicationStyle.h
NativeLinearEquationSolver.cpp
NativeLinearEquationSolver.h
OptimizationDirection.cpp
OptimizationDirection.h
SmtlibSmtSolver.cpp
SmtlibSmtSolver.h
SmtratSmtSolver.cpp
SmtratSmtSolver.h
SmtSolver.cpp
SmtSolver.h
SolveGoal.cpp
SolveGoal.h
SolverGuarantee.cpp
SolverGuarantee.h
SolverRequirement.cpp
SolverRequirement.h
SolverSelectionOptions.cpp
SolverSelectionOptions.h
SolverStatus.cpp
SolverStatus.h
SoplexLpSolver.cpp
SoplexLpSolver.h
StandardGameSolver.cpp
StandardGameSolver.h
StandardMinMaxLinearEquationSolver.cpp
StandardMinMaxLinearEquationSolver.h
SymbolicEliminationLinearEquationSolver.cpp
SymbolicEliminationLinearEquationSolver.h
SymbolicEquationSolver.cpp
SymbolicEquationSolver.h
SymbolicGameSolver.cpp
SymbolicGameSolver.h
SymbolicLinearEquationSolver.cpp
SymbolicLinearEquationSolver.h
SymbolicMinMaxLinearEquationSolver.cpp
SymbolicMinMaxLinearEquationSolver.h
SymbolicNativeLinearEquationSolver.cpp
SymbolicNativeLinearEquationSolver.h
TerminationCondition.cpp
TerminationCondition.h
TopologicalLinearEquationSolver.cpp
TopologicalLinearEquationSolver.h
TopologicalMinMaxLinearEquationSolver.cpp
TopologicalMinMaxLinearEquationSolver.h
Z3LpSolver.cpp
Z3LpSolver.h
Z3SmtSolver.cpp
Z3SmtSolver.h
► storage
► bisimulation
BisimulationDecomposition.cpp
BisimulationDecomposition.h
BisimulationType.h
Block.cpp
Block.h
DeterministicBlockData.cpp
DeterministicBlockData.h
DeterministicModelBisimulationDecomposition.cpp
DeterministicModelBisimulationDecomposition.h
NondeterministicModelBisimulationDecomposition.cpp
NondeterministicModelBisimulationDecomposition.h
Partition.cpp
Partition.h
► dd
► bisimulation
InternalCuddSignatureRefiner.cpp
InternalCuddSignatureRefiner.h
InternalSignatureRefiner.cpp
InternalSignatureRefiner.h
InternalSylvanSignatureRefiner.cpp
InternalSylvanSignatureRefiner.h
NondeterministicModelPartitionRefiner.cpp
NondeterministicModelPartitionRefiner.h
PartialQuotientExtractor.cpp
PartialQuotientExtractor.h
Partition.cpp
Partition.h
PartitionRefiner.cpp
PartitionRefiner.h
PreservationInformation.cpp
PreservationInformation.h
QuotientExtractor.cpp
QuotientExtractor.h
QuotientFormat.h
Signature.cpp
Signature.h
SignatureComputer.cpp
SignatureComputer.h
SignatureMode.h
SignatureRefiner.cpp
SignatureRefiner.h
Status.h
► cudd
CuddAddIterator.cpp
CuddAddIterator.h
InternalCuddAdd.cpp
InternalCuddAdd.h
InternalCuddBdd.cpp
InternalCuddBdd.h
InternalCuddDdManager.cpp
InternalCuddDdManager.h
utility.h
► sylvan
InternalSylvanAdd.cpp
InternalSylvanAdd.h
InternalSylvanBdd.cpp
InternalSylvanBdd.h
InternalSylvanDdManager.cpp
InternalSylvanDdManager.h
SylvanAddIterator.cpp
SylvanAddIterator.h
utility.h
Add.cpp
Add.h
AddIterator.h
Bdd.cpp
Bdd.h
BisimulationDecomposition.cpp
BisimulationDecomposition.h
Dd.cpp
Dd.h
DdManager.cpp
DdManager.h
DdMetaVariable.cpp
DdMetaVariable.h
DdType.h
InternalAdd.h
InternalBdd.h
InternalDdManager.h
MetaVariablePosition.h
Odd.cpp
Odd.h
► expressions
BaseExpression.cpp
BaseExpression.h
BinaryBooleanFunctionExpression.cpp
BinaryBooleanFunctionExpression.h
BinaryExpression.cpp
BinaryExpression.h
BinaryNumericalFunctionExpression.cpp
BinaryNumericalFunctionExpression.h
BinaryRelationExpression.cpp
BinaryRelationExpression.h
BinaryRelationType.h
BooleanLiteralExpression.cpp
BooleanLiteralExpression.h
ChangeManagerVisitor.cpp
ChangeManagerVisitor.h
CheckIfThenElseGuardVisitor.cpp
CheckIfThenElseGuardVisitor.h
CompiledExpression.cpp
CompiledExpression.h
EquivalenceChecker.cpp
EquivalenceChecker.h
Expression.cpp
Expression.h
ExpressionEvaluator.cpp
ExpressionEvaluator.h
ExpressionEvaluatorBase.cpp
ExpressionEvaluatorBase.h
ExpressionManager.cpp
ExpressionManager.h
Expressions.h
ExpressionVisitor.cpp
ExpressionVisitor.h
ExprtkCompiledExpression.cpp
ExprtkCompiledExpression.h
ExprtkExpressionEvaluator.cpp
ExprtkExpressionEvaluator.h
FullPredicateSplitter.cpp
FullPredicateSplitter.h
IfThenElseExpression.cpp
IfThenElseExpression.h
IntegerLiteralExpression.cpp
IntegerLiteralExpression.h
LinearCoefficientVisitor.cpp
LinearCoefficientVisitor.h
LinearityCheckVisitor.cpp
LinearityCheckVisitor.h
OperatorType.cpp
OperatorType.h
PredicateExpression.cpp
PredicateExpression.h
RationalFunctionToExpression.cpp
RationalFunctionToExpression.h
RationalLiteralExpression.cpp
RationalLiteralExpression.h
ReduceNestingVisitor.cpp
ReduceNestingVisitor.h
RestrictSyntaxVisitor.cpp
RestrictSyntaxVisitor.h
SimpleValuation.cpp
SimpleValuation.h
SubstitutionVisitor.cpp
SubstitutionVisitor.h
SyntacticalEqualityCheckVisitor.cpp
SyntacticalEqualityCheckVisitor.h
ToCppVisitor.cpp
ToCppVisitor.h
ToDiceStringVisitor.cpp
ToDiceStringVisitor.h
ToExprtkStringVisitor.cpp
ToExprtkStringVisitor.h
ToRationalFunctionVisitor.cpp
ToRationalFunctionVisitor.h
ToRationalNumberVisitor.cpp
ToRationalNumberVisitor.h
Type.cpp
Type.h
UnaryBooleanFunctionExpression.cpp
UnaryBooleanFunctionExpression.h
UnaryExpression.cpp
UnaryExpression.h
UnaryNumericalFunctionExpression.cpp
UnaryNumericalFunctionExpression.h
Valuation.cpp
Valuation.h
Variable.cpp
Variable.h
VariableExpression.cpp
VariableExpression.h
VariableSetPredicateSplitter.cpp
VariableSetPredicateSplitter.h
► geometry
► nativepolytopeconversion
HyperplaneCollector.cpp
HyperplaneCollector.h
HyperplaneEnumeration.cpp
HyperplaneEnumeration.h
QuickHull.cpp
QuickHull.h
SubsetEnumerator.cpp
SubsetEnumerator.h
coordinates.h
Halfspace.h
Hyperrectangle.h
NativePolytope.cpp
NativePolytope.h
Polytope.cpp
Polytope.h
PolytopeTree.h
ReduceVertexCloud.cpp
ReduceVertexCloud.h
► jani
► eliminator
ArrayEliminator.cpp
ArrayEliminator.h
FunctionEliminator.cpp
FunctionEliminator.h
► expressions
ArrayAccessExpression.cpp
ArrayAccessExpression.h
ArrayExpression.cpp
ArrayExpression.h
ConstructorArrayExpression.cpp
ConstructorArrayExpression.h
FunctionCallExpression.cpp
FunctionCallExpression.h
JaniExpressions.h
TranscendentalNumberLiteralExpression.cpp
TranscendentalNumberLiteralExpression.h
ValueArrayExpression.cpp
ValueArrayExpression.h
► localeliminator
AutomaticAction.cpp
AutomaticAction.h
EliminateAction.cpp
EliminateAction.h
EliminateAutomaticallyAction.cpp
EliminateAutomaticallyAction.h
FinishAction.cpp
FinishAction.h
JaniLocalEliminator.cpp
JaniLocalEliminator.h
RebuildWithoutUnreachableAction.cpp
RebuildWithoutUnreachableAction.h
UnfoldAction.cpp
UnfoldAction.h
UnfoldDependencyGraph.cpp
UnfoldDependencyGraph.h
► traverser
ArrayExpressionFinder.cpp
ArrayExpressionFinder.h
AssignmentLevelFinder.cpp
AssignmentLevelFinder.h
AssignmentsFinder.cpp
AssignmentsFinder.h
FunctionCallExpressionFinder.cpp
FunctionCallExpressionFinder.h
InformationCollector.cpp
InformationCollector.h
JaniTraverser.cpp
JaniTraverser.h
RewardModelInformation.cpp
RewardModelInformation.h
► types
AllJaniTypes.h
ArrayType.cpp
ArrayType.h
BasicType.cpp
BasicType.h
BoundedType.cpp
BoundedType.h
ClockType.cpp
ClockType.h
ContinuousType.cpp
ContinuousType.h
JaniType.cpp
JaniType.h
► visitor
CompositionInformationVisitor.cpp
CompositionInformationVisitor.h
CompositionVisitor.h
JaniExpressionSubstitutionVisitor.cpp
JaniExpressionSubstitutionVisitor.h
JaniExpressionVisitor.h
JaniReduceNestingExpressionVisitor.cpp
JaniReduceNestingExpressionVisitor.h
JaniSyntacticalEqualityCheckVisitor.cpp
JaniSyntacticalEqualityCheckVisitor.h
JSONExporter.cpp
JSONExporter.h
Action.cpp
Action.h
Assignment.cpp
Assignment.h
Automaton.cpp
Automaton.h
AutomatonComposition.cpp
AutomatonComposition.h
Composition.cpp
Composition.h
Compositions.h
Constant.cpp
Constant.h
Edge.cpp
Edge.h
EdgeContainer.cpp
EdgeContainer.h
EdgeDestination.cpp
EdgeDestination.h
FunctionDefinition.cpp
FunctionDefinition.h
JaniLocationExpander.cpp
JaniLocationExpander.h
JaniScopeChanger.cpp
JaniScopeChanger.h
Location.cpp
Location.h
LValue.cpp
LValue.h
Model.cpp
Model.h
ModelFeatures.cpp
ModelFeatures.h
ModelType.cpp
ModelType.h
OrderedAssignments.cpp
OrderedAssignments.h
ParallelComposition.cpp
ParallelComposition.h
Property.cpp
Property.h
TemplateEdge.cpp
TemplateEdge.h
TemplateEdgeContainer.cpp
TemplateEdgeContainer.h
TemplateEdgeDestination.cpp
TemplateEdgeDestination.h
Variable.cpp
Variable.h
VariableSet.cpp
VariableSet.h
VariablesToConstantsTransformer.cpp
VariablesToConstantsTransformer.h
► memorystructure
MemoryStructure.cpp
MemoryStructure.h
MemoryStructureBuilder.cpp
MemoryStructureBuilder.h
NondeterministicMemoryStructure.cpp
NondeterministicMemoryStructure.h
NondeterministicMemoryStructureBuilder.cpp
NondeterministicMemoryStructureBuilder.h
SparseModelMemoryProduct.cpp
SparseModelMemoryProduct.h
SparseModelNondeterministicMemoryProduct.cpp
SparseModelNondeterministicMemoryProduct.h
► prism
Assignment.cpp
Assignment.h
BooleanVariable.cpp
BooleanVariable.h
ClockVariable.cpp
ClockVariable.h
Command.cpp
Command.h
Composition.cpp
Composition.h
Compositions.h
CompositionToJaniVisitor.cpp
CompositionToJaniVisitor.h
CompositionVisitor.h
Constant.cpp
Constant.h
Formula.cpp
Formula.h
HidingComposition.cpp
HidingComposition.h
InitialConstruct.cpp
InitialConstruct.h
IntegerVariable.cpp
IntegerVariable.h
InterleavingParallelComposition.cpp
InterleavingParallelComposition.h
Label.cpp
Label.h
LocatedInformation.cpp
LocatedInformation.h
Module.cpp
Module.h
ModuleComposition.cpp
ModuleComposition.h
ModuleRenaming.cpp
ModuleRenaming.h
OverlappingGuardAnalyser.cpp
OverlappingGuardAnalyser.h
ParallelComposition.cpp
ParallelComposition.h
Player.cpp
Player.h
Program.cpp
Program.h
RenamingComposition.cpp
RenamingComposition.h
RestrictedParallelComposition.cpp
RestrictedParallelComposition.h
RewardModel.cpp
RewardModel.h
StateActionReward.cpp
StateActionReward.h
StateReward.cpp
StateReward.h
SynchronizingParallelComposition.cpp
SynchronizingParallelComposition.h
SystemCompositionConstruct.cpp
SystemCompositionConstruct.h
ToJaniConverter.cpp
ToJaniConverter.h
TransitionReward.cpp
TransitionReward.h
Update.cpp
Update.h
Variable.cpp
Variable.h
► sparse
ChoiceOrigins.cpp
ChoiceOrigins.h
JaniChoiceOrigins.cpp
JaniChoiceOrigins.h
ModelComponents.h
PrismChoiceOrigins.cpp
PrismChoiceOrigins.h
StateStorage.cpp
StateStorage.h
StateType.h
StateValuations.cpp
StateValuations.h
BitVector.cpp
BitVector.h
BitVectorHashMap.cpp
BitVectorHashMap.h
BoostTypes.h
ConsecutiveUint64DynamicPriorityQueue.h
Decomposition.cpp
Decomposition.h
DeterministicTransition.h
Distribution.cpp
Distribution.h
DistributionWithReward.cpp
DistributionWithReward.h
DynamicPriorityQueue.h
ExplicitGameStrategy.cpp
ExplicitGameStrategy.h
ExplicitGameStrategyPair.cpp
ExplicitGameStrategyPair.h
FlexibleSparseMatrix.cpp
FlexibleSparseMatrix.h
IntegerInterval.cpp
IntegerInterval.h
MaximalEndComponent.cpp
MaximalEndComponent.h
MaximalEndComponentDecomposition.cpp
MaximalEndComponentDecomposition.h
ModelFormulasPair.h
PairHash.h
PlayerIndex.h
Qvbs.cpp
Qvbs.h
Scheduler.cpp
Scheduler.h
SchedulerChoice.cpp
SchedulerChoice.h
SchedulerClass.cpp
SchedulerClass.h
SparseMatrix.cpp
SparseMatrix.h
SparseMatrixOperations.cpp
SparseMatrixOperations.h
StateActionPair.h
StateActionTargetTuple.h
StateBlock.cpp
StateBlock.h
StronglyConnectedComponent.cpp
StronglyConnectedComponent.h
StronglyConnectedComponentDecomposition.cpp
StronglyConnectedComponentDecomposition.h
SymbolicModelDescription.cpp
SymbolicModelDescription.h
► transformer
AddUncertainty.cpp
AddUncertainty.h
ChoiceSelector.cpp
ChoiceSelector.h
ContinuousToDiscreteTimeModelTransformer.cpp
ContinuousToDiscreteTimeModelTransformer.h
DAProduct.h
DAProductBuilder.h
EndComponentEliminator.h
GoalStateMerger.cpp
GoalStateMerger.h
MemoryIncorporation.cpp
MemoryIncorporation.h
NonMarkovianChainTransformer.cpp
NonMarkovianChainTransformer.h
Product.h
ProductBuilder.h
StatePermuter.cpp
StatePermuter.h
SubsystemBuilder.cpp
SubsystemBuilder.h
SymbolicToSparseTransformer.cpp
SymbolicToSparseTransformer.h
► utility
AutomaticSettings.cpp
AutomaticSettings.h
bitoperations.h
builder.cpp
builder.h
cli.cpp
cli.h
combinatorics.h
constants.cpp
constants.h
ConstantsComparator.cpp
ConstantsComparator.h
ConstantsComparatorForward.h
dd.cpp
dd.h
Engine.cpp
Engine.h
ExtendSettingEnumWithSelectionField.h
Extremum.cpp
Extremum.h
FilteredRewardModel.h
graph.cpp
graph.h
Hash.h
initialize.cpp
initialize.h
jani.cpp
jani.h
KwekMehlhorn.cpp
KwekMehlhorn.h
logging.h
macros.h
math.h
matrix.h
NumberTraits.h
numerical.cpp
numerical.h
OptionalRef.h
OsDetection.h
permutation.cpp
permutation.h
prism.cpp
prism.h
ProgressMeasurement.cpp
ProgressMeasurement.h
random.cpp
random.h
rationalfunction.h
shortestPaths.cpp
shortestPaths.h
SignalHandler.cpp
SignalHandler.h
solver.cpp
solver.h
stateelimination.cpp
stateelimination.h
Stopwatch.cpp
Stopwatch.h
string.cpp
string.h
threads.cpp
threads.h
vector.h
VectorHelper.cpp
VectorHelper.h
► storm-cli
storm-cli.cpp
► storm-cli-utilities
cli.cpp
cli.h
model-handling.h
print.cpp
print.h
resources.h
► storm-conv
► api
storm-conv.cpp
storm-conv.h
► converter
► options
JaniConversionOptions.cpp
JaniConversionOptions.h
PrismToJaniConverterOptions.cpp
PrismToJaniConverterOptions.h
► settings
► modules
ConversionGeneralSettings.cpp
ConversionGeneralSettings.h
ConversionInputSettings.cpp
ConversionInputSettings.h
ConversionOutputSettings.cpp
ConversionOutputSettings.h
JaniExportSettings.cpp
JaniExportSettings.h
PrismExportSettings.cpp
PrismExportSettings.h
ConvSettings.cpp
ConvSettings.h
► storm-conv-cli
storm-conv.cpp
► storm-counterexamples
► api
counterexamples.cpp
counterexamples.h
► counterexamples
Counterexample.cpp
Counterexample.h
GuaranteedLabelSet.h
HighLevelCounterexample.cpp
HighLevelCounterexample.h
MILPMinimalLabelSetGenerator.h
PathCounterexample.cpp
PathCounterexample.h
SMTMinimalLabelSetGenerator.h
► settings
► modules
CounterexampleGeneratorSettings.cpp
CounterexampleGeneratorSettings.h
► storm-dft
► adapters
SFTBDDPropertyFormulaAdapter.h
► api
storm-dft.cpp
storm-dft.h
► builder
DFTBuilder.cpp
DFTBuilder.h
DftExplorationHeuristic.cpp
DftExplorationHeuristic.h
ExplicitDFTModelBuilder.cpp
ExplicitDFTModelBuilder.h
► generator
DftNextStateGenerator.cpp
DftNextStateGenerator.h
► modelchecker
DFTASFChecker.cpp
DFTASFChecker.h
DFTModelChecker.cpp
DFTModelChecker.h
DftModularizationChecker.cpp
DftModularizationChecker.h
SFTBDDChecker.cpp
SFTBDDChecker.h
SmtConstraint.cpp
SmtConstraint.h
► parser
DFTGalileoParser.cpp
DFTGalileoParser.h
DFTJsonParser.cpp
DFTJsonParser.h
► settings
► modules
DftGspnSettings.cpp
DftGspnSettings.h
DftIOSettings.cpp
DftIOSettings.h
FaultTreeSettings.cpp
FaultTreeSettings.h
DftSettings.cpp
DftSettings.h
► simulator
DFTTraceSimulator.cpp
DFTTraceSimulator.h
ImportanceFunction.cpp
ImportanceFunction.h
► storage
► elements
BEConst.cpp
BEConst.h
BEErlang.cpp
BEErlang.h
BEExponential.cpp
BEExponential.h
BELogNormal.cpp
BELogNormal.h
BEProbability.cpp
BEProbability.h
BESamples.cpp
BESamples.h
BEWeibull.cpp
BEWeibull.h
DFTAnd.h
DFTBE.cpp
DFTBE.h
DFTChildren.h
DFTDependency.h
DFTElement.cpp
DFTElement.h
DFTElements.h
DFTElementType.h
DFTGate.h
DFTMutex.h
DFTOr.h
DFTPand.h
DFTPor.h
DFTRestriction.h
DFTSeq.h
DFTSpare.h
DFTVot.h
BucketPriorityQueue.cpp
BucketPriorityQueue.h
DFT.cpp
DFT.h
DFTElementState.h
DFTIsomorphism.h
DftJsonExporter.cpp
DftJsonExporter.h
DFTLayoutInfo.h
DftModule.cpp
DftModule.h
DFTState.cpp
DFTState.h
DFTStateGenerationInfo.h
DFTStateSpaceGenerationQueues.h
DftSymmetries.cpp
DftSymmetries.h
FailableElements.cpp
FailableElements.h
OrderDFTElementsById.cpp
OrderDFTElementsById.h
SylvanBddManager.h
► transformations
DftInstantiator.cpp
DftInstantiator.h
DftToGspnTransformator.cpp
DftToGspnTransformator.h
DftTransformer.cpp
DftTransformer.h
SftToBddTransformator.h
► utility
DftModularizer.cpp
DftModularizer.h
DftValidator.cpp
DftValidator.h
FailureBoundFinder.cpp
FailureBoundFinder.h
FDEPConflictFinder.cpp
FDEPConflictFinder.h
MTTFHelper.cpp
MTTFHelper.h
RelevantEvents.h
SymmetryFinder.cpp
SymmetryFinder.h
► storm-dft-cli
storm-dft.cpp
► storm-gamebased-ar
► abstraction
► jani
AutomatonAbstractor.cpp
AutomatonAbstractor.h
EdgeAbstractor.cpp
EdgeAbstractor.h
JaniMenuGameAbstractor.cpp
JaniMenuGameAbstractor.h
► prism
CommandAbstractor.cpp
CommandAbstractor.h
ModuleAbstractor.cpp
ModuleAbstractor.h
PrismMenuGameAbstractor.cpp
PrismMenuGameAbstractor.h
AbstractionInformation.cpp
AbstractionInformation.h
BottomStateResult.cpp
BottomStateResult.h
ExplicitQualitativeGameResult.cpp
ExplicitQualitativeGameResult.h
ExplicitQualitativeGameResultMinMax.cpp
ExplicitQualitativeGameResultMinMax.h
ExplicitQualitativeResult.cpp
ExplicitQualitativeResult.h
ExplicitQualitativeResultMinMax.cpp
ExplicitQualitativeResultMinMax.h
ExplicitQuantitativeResult.cpp
ExplicitQuantitativeResult.h
ExplicitQuantitativeResultMinMax.cpp
ExplicitQuantitativeResultMinMax.h
ExpressionTranslator.cpp
ExpressionTranslator.h
GameBddResult.cpp
GameBddResult.h
LocalExpressionInformation.cpp
LocalExpressionInformation.h
MenuGame.cpp
MenuGame.h
MenuGameAbstractor.cpp
MenuGameAbstractor.h
MenuGameRefiner.cpp
MenuGameRefiner.h
QualitativeResult.cpp
QualitativeResult.h
QualitativeResultMinMax.cpp
QualitativeResultMinMax.h
RefinementCommand.cpp
RefinementCommand.h
StateSet.cpp
StateSet.h
StateSetAbstractor.cpp
StateSetAbstractor.h
SymbolicQualitativeGameResult.cpp
SymbolicQualitativeGameResult.h
SymbolicQualitativeGameResultMinMax.cpp
SymbolicQualitativeGameResultMinMax.h
SymbolicQualitativeMdpResult.cpp
SymbolicQualitativeMdpResult.h
SymbolicQualitativeMdpResultMinMax.cpp
SymbolicQualitativeMdpResultMinMax.h
SymbolicQualitativeResult.h
SymbolicQualitativeResultMinMax.cpp
SymbolicQualitativeResultMinMax.h
SymbolicQuantitativeGameResult.cpp
SymbolicQuantitativeGameResult.h
SymbolicQuantitativeGameResultMinMax.cpp
SymbolicQuantitativeGameResultMinMax.h
SymbolicStateSet.cpp
SymbolicStateSet.h
ValidBlockAbstractor.cpp
ValidBlockAbstractor.h
► api
verification.h
► modelchecker
► abstraction
AbstractAbstractionRefinementModelChecker.cpp
AbstractAbstractionRefinementModelChecker.h
BisimulationAbstractionRefinementModelChecker.cpp
BisimulationAbstractionRefinementModelChecker.h
GameBasedMdpModelChecker.cpp
GameBasedMdpModelChecker.h
► storm-gspn
► adapters
XercesAdapter.h
► api
storm-gspn.cpp
storm-gspn.h
► builder
ExplicitGspnModelBuilder.cpp
ExplicitGspnModelBuilder.h
JaniGSPNBuilder.cpp
JaniGSPNBuilder.h
► parser
GreatSpnEditorProjectParser.cpp
GreatSpnEditorProjectParser.h
GspnParser.cpp
GspnParser.h
PnmlParser.cpp
PnmlParser.h
► settings
► modules
GSPNExportSettings.cpp
GSPNExportSettings.h
GSPNSettings.cpp
GSPNSettings.h
► storage
► gspn
GSPN.cpp
GSPN.h
GspnBuilder.cpp
GspnBuilder.h
GspnJsonExporter.cpp
GspnJsonExporter.h
ImmediateTransition.h
Marking.cpp
Marking.h
Place.cpp
Place.h
PlacementInfo.h
TimedTransition.h
Transition.cpp
Transition.h
TransitionPartition.h
► storm-gspn-cli
storm-gspn.cpp
► storm-pars
► analysis
AssumptionChecker.cpp
AssumptionChecker.h
AssumptionMaker.cpp
AssumptionMaker.h
LocalMonotonicityResult.cpp
LocalMonotonicityResult.h
MonotonicityChecker.cpp
MonotonicityChecker.h
MonotonicityHelper.cpp
MonotonicityHelper.h
MonotonicityResult.cpp
MonotonicityResult.h
Order.cpp
Order.h
OrderExtender.cpp
OrderExtender.h
► api
analysis.h
export.h
region.h
storm-pars.h
► derivative
GradientDescentConstraintMethod.h
GradientDescentInstantiationSearcher.cpp
GradientDescentInstantiationSearcher.h
GradientDescentMethod.h
SparseDerivativeInstantiationModelChecker.cpp
SparseDerivativeInstantiationModelChecker.h
► modelchecker
► instantiation
SparseCtmcInstantiationModelChecker.cpp
SparseCtmcInstantiationModelChecker.h
SparseDtmcInstantiationModelChecker.cpp
SparseDtmcInstantiationModelChecker.h
SparseInstantiationModelChecker.cpp
SparseInstantiationModelChecker.h
SparseMdpInstantiationModelChecker.cpp
SparseMdpInstantiationModelChecker.h
► region
RegionCheckEngine.cpp
RegionCheckEngine.h
RegionModelChecker.cpp
RegionModelChecker.h
RegionResult.cpp
RegionResult.h
RegionResultHypothesis.cpp
RegionResultHypothesis.h
SparseDtmcParameterLiftingModelChecker.cpp
SparseDtmcParameterLiftingModelChecker.h
SparseMdpParameterLiftingModelChecker.cpp
SparseMdpParameterLiftingModelChecker.h
SparseParameterLiftingModelChecker.cpp
SparseParameterLiftingModelChecker.h
ValidatingSparseDtmcParameterLiftingModelChecker.cpp
ValidatingSparseDtmcParameterLiftingModelChecker.h
ValidatingSparseMdpParameterLiftingModelChecker.cpp
ValidatingSparseMdpParameterLiftingModelChecker.h
ValidatingSparseParameterLiftingModelChecker.cpp
ValidatingSparseParameterLiftingModelChecker.h
► results
RegionCheckResult.cpp
RegionCheckResult.h
RegionRefinementCheckResult.cpp
RegionRefinementCheckResult.h
► parser
MonotonicityParser.cpp
MonotonicityParser.h
ParameterRegionParser.cpp
ParameterRegionParser.h
► settings
► modules
DerivativeSettings.cpp
DerivativeSettings.h
FeasibilitySettings.cpp
FeasibilitySettings.h
MonotonicitySettings.cpp
MonotonicitySettings.h
ParametricSettings.cpp
ParametricSettings.h
PartitionSettings.cpp
PartitionSettings.h
RegionSettings.cpp
RegionSettings.h
RegionVerificationSettings.cpp
RegionVerificationSettings.h
SamplingSettings.cpp
SamplingSettings.h
ParsSettings.cpp
ParsSettings.h
► storage
ParameterRegion.cpp
ParameterRegion.h
► transformer
BinaryDtmcTransformer.cpp
BinaryDtmcTransformer.h
ParameterLifter.cpp
ParameterLifter.h
SparseParametricDtmcSimplifier.cpp
SparseParametricDtmcSimplifier.h
SparseParametricMdpSimplifier.cpp
SparseParametricMdpSimplifier.h
SparseParametricModelSimplifier.cpp
SparseParametricModelSimplifier.h
TimeTravelling.cpp
TimeTravelling.h
► utility
FeasibilitySynthesisTask.h
ModelInstantiator.cpp
ModelInstantiator.h
parameterlifting.h
parametric.cpp
parametric.h
ParametricMode.cpp
ParametricMode.h
► storm-pars-cli
feasibility.cpp
feasibility.h
monotonicity.cpp
monotonicity.h
print.cpp
print.h
sampling.h
solutionFunctions.h
storm-pars.cpp
► storm-parsers
► api
explicit_models.h
model_descriptions.cpp
model_descriptions.h
properties.cpp
properties.h
storm-parsers.h
► parser
AtomicPropositionLabelingParser.cpp
AtomicPropositionLabelingParser.h
AutoParser.cpp
AutoParser.h
ConstantDataType.cpp
ConstantDataType.h
DeterministicModelParser.cpp
DeterministicModelParser.h
DeterministicSparseTransitionParser.cpp
DeterministicSparseTransitionParser.h
DirectEncodingParser.cpp
DirectEncodingParser.h
ExpressionCreator.cpp
ExpressionCreator.h
ExpressionParser.cpp
ExpressionParser.h
FormulaParser.cpp
FormulaParser.h
FormulaParserGrammar.cpp
FormulaParserGrammar.h
ImcaMarkovAutomatonParser.cpp
ImcaMarkovAutomatonParser.h
ImcaMarkovAutomatonParserGrammar.cpp
ImcaMarkovAutomatonParserGrammar.h
JaniParser.cpp
JaniParser.h
KeyValueParser.cpp
KeyValueParser.h
MappedFile.cpp
MappedFile.h
MarkovAutomatonParser.cpp
MarkovAutomatonParser.h
MarkovAutomatonSparseTransitionParser.cpp
MarkovAutomatonSparseTransitionParser.h
NondeterministicModelParser.cpp
NondeterministicModelParser.h
NondeterministicSparseTransitionParser.cpp
NondeterministicSparseTransitionParser.h
PrismParser.cpp
PrismParser.h
PrismParserGrammar.cpp
PrismParserGrammar.h
ReadValues.h
SparseChoiceLabelingParser.cpp
SparseChoiceLabelingParser.h
SparseItemLabelingParser.cpp
SparseItemLabelingParser.h
SparseStateRewardParser.cpp
SparseStateRewardParser.h
SpiritErrorHandler.h
SpiritParserDefinitions.h
ValueParser.cpp
ValueParser.h
► util
cstring.cpp
cstring.h
► storm-permissive
► analysis
MILPPermissiveSchedulers.h
PermissiveSchedulerComputation.h
PermissiveSchedulerPenalty.h
PermissiveSchedulers.cpp
PermissiveSchedulers.h
SmtBasedPermissiveSchedulers.h
► storm-pomdp
► analysis
FiniteBeliefMdpDetection.h
FormulaInformation.cpp
FormulaInformation.h
IterativePolicySearch.cpp
IterativePolicySearch.h
JaniBeliefSupportMdpGenerator.cpp
JaniBeliefSupportMdpGenerator.h
OneShotPolicySearch.cpp
OneShotPolicySearch.h
QualitativeAnalysis.cpp
QualitativeAnalysis.h
QualitativeAnalysisOnGraphs.cpp
QualitativeAnalysisOnGraphs.h
UniqueObservationStates.cpp
UniqueObservationStates.h
WinningRegion.cpp
WinningRegion.h
WinningRegionQueryInterface.cpp
WinningRegionQueryInterface.h
► api
verification.h
► builder
BeliefMdpExplorer.cpp
BeliefMdpExplorer.h
► generator
BeliefSupportTracker.cpp
BeliefSupportTracker.h
NondeterministicBeliefTracker.cpp
NondeterministicBeliefTracker.h
► modelchecker
BeliefExplorationPomdpModelChecker.cpp
BeliefExplorationPomdpModelChecker.h
BeliefExplorationPomdpModelCheckerOptions.h
PreprocessingPomdpValueBoundsModelChecker.cpp
PreprocessingPomdpValueBoundsModelChecker.h
► storage
BeliefExplorationBounds.cpp
BeliefExplorationBounds.h
BeliefManager.cpp
BeliefManager.h
PomdpMemory.cpp
PomdpMemory.h
► transformer
ApplyFiniteSchedulerToPomdp.cpp
ApplyFiniteSchedulerToPomdp.h
BinaryPomdpTransformer.cpp
BinaryPomdpTransformer.h
GlobalPomdpMecChoiceEliminator.cpp
GlobalPomdpMecChoiceEliminator.h
GlobalPOMDPSelfLoopEliminator.cpp
GlobalPOMDPSelfLoopEliminator.h
KnownProbabilityTransformer.cpp
KnownProbabilityTransformer.h
MakePOMDPCanonic.cpp
MakePOMDPCanonic.h
MakeStateSetObservationClosed.cpp
MakeStateSetObservationClosed.h
ObservationTraceUnfolder.cpp
ObservationTraceUnfolder.h
PomdpMemoryUnfolder.cpp
PomdpMemoryUnfolder.h
► storm-pomdp-cli
► settings
► modules
BeliefExplorationSettings.cpp
BeliefExplorationSettings.h
POMDPSettings.cpp
POMDPSettings.h
QualitativePOMDPAnalysisSettings.cpp
QualitativePOMDPAnalysisSettings.h
ToParametricSettings.cpp
ToParametricSettings.h
PomdpSettings.cpp
PomdpSettings.h
storm-pomdp.cpp
► storm-version-info
storm-version.h
► test
► storm
► adapter
MathsatExpressionAdapterTest.cpp
Z3ExpressionAdapterTest.cpp
► automata
HOAParsingTest.cpp
► builder
DdJaniModelBuilderTest.cpp
DdPrismModelBuilderTest.cpp
ExplicitJaniModelBuilderTest.cpp
ExplicitPrismModelBuilderTest.cpp
► logic
FragmentCheckerTest.cpp
► model
MarkovAutomatonTest.cpp
StateLabelingTest.cpp
► modelchecker
► csl
CtmcCslModelCheckerTest.cpp
ExpectedVisitingTimesCtmcCslModelCheckerTest.cpp
LraCtmcCslModelCheckerTest.cpp
MarkovAutomatonCslModelCheckerTest.cpp
SteadyStateCtmcCslModelCheckerTest.cpp
► exploration
SparseExplorationModelCheckerTest.cpp
► lexicographic
LexicographicModelCheckingTest.cpp
► multiobjective
MultiObjectiveSchedRestModelCheckerTest.cpp
SparseDtmcMultiDimensionalRewardUnfoldingTest.cpp
SparseMaCbMultiObjectiveModelCheckerTest.cpp
SparseMaPcaaMultiObjectiveModelCheckerTest.cpp
SparseMdpCbMultiObjectiveModelCheckerTest.cpp
SparseMdpMultiDimensionalRewardUnfoldingTest.cpp
SparseMdpPcaaMultiObjectiveModelCheckerTest.cpp
► prctl
► dtmc
ConditionalDtmcPrctlModelCheckerTest.cpp
DtmcPrctlModelCheckerTest.cpp
ExplicitDtmcPrctlModelCheckerTest.cpp
LraDtmcPrctlModelCheckerTest.cpp
► mdp
ExplicitMdpPrctlModelCheckerTest.cpp
LraMdpPrctlModelCheckerTest.cpp
MdpPrctlModelCheckerTest.cpp
QuantileQueryTest.cpp
RobustMdpPrctlModelCheckerTest.cpp
SchedulerGenerationMdpPrctlModelCheckerTest.cpp
► reachability
SparseDtmcEliminationModelCheckerTest.cpp
► parser
AutoParserTest.cpp
DeterministicModelParserTest.cpp
DeterministicSparseTransitionParserTest.cpp
DirectEncodingParserTest.cpp
FormulaParserTest.cpp
JaniParserTest.cpp
MappedFileTest.cpp
MarkovAutomatonParserTest.cpp
MarkovAutomatonSparseTransitionParserTest.cpp
NondeterministicModelParserTest.cpp
NondeterministicSparseTransitionParserTest.cpp
PrismParserTest.cpp
SparseItemLabelingParserTest.cpp
SparseStateRewardParserTest.cpp
► simulator
PrismProgramSimulator.cpp
► solver
FullySymbolicGameSolverTest.cpp
GameSolverTest.cpp
LinearEquationSolverTest.cpp
LpSolverTest.cpp
MathsatSmtSolverTest.cpp
MinMaxLinearEquationSolverTest.cpp
MinMaxTechniqueSelectionTest.cpp
MultiplierTest.cpp
Z3SmtSolverTest.cpp
► storage
BitVectorHashMapTest.cpp
BitVectorTest.cpp
DdTest.cpp
DeterministicModelBisimulationDecompositionTest.cpp
ExpressionEvalutionTest.cpp
ExpressionTest.cpp
JaniLocalEliminatorTests.cpp
JaniModelTest.cpp
MaximalEndComponentDecompositionTest.cpp
NondeterministicModelBisimulationDecompositionTest.cpp
PrismProgramTest.cpp
SchedulerTest.cpp
SparseMatrixTest.cpp
StronglyConnectedComponentDecompositionTest.cpp
SylvanDdTest.cpp
SymbolicBisimulationDecompositionTest.cpp
► transformer
AddUncertaintyTest.cpp
DAProductBuilderTest.cpp
EndComponentEliminatorTest.cpp
NonMarkovianChainTransformerTest.cpp
StatePermuterTest.cpp
► utility
FileTest.cpp
GraphTest.cpp
KSPTest.cpp
VectorTest.cpp
storm-test.cpp
► storm-dft
► api
DftApproximationTest.cpp
DftModelBuildingTest.cpp
DftModelCheckerTest.cpp
DftParserTest.cpp
DftSmtTest.cpp
DftValidatorTest.cpp
► bdd
TestBdd.cpp
TestBddModularizer.cpp
► simulator
DftSimulatorTest.cpp
DftTraceGeneratorTest.cpp
ImportanceFunction.cpp
SamplingTest.cpp
► storage
BEDistributionTest.cpp
DftBETest.cpp
DftModuleTest.cpp
SymmetryTest.cpp
► transformations
DftInstantiatorTest.cpp
DftTransformerTest.cpp
storm-test.cpp
► storm-gamebased-ar
► abstraction
GraphTest.cpp
PrismMenuGameTest.cpp
► modelchecker
► abstraction
GameBasedDtmcModelCheckerTest.cpp
GameBasedMdpModelCheckerTest.cpp
storm-test.cpp
► storm-pars
► analysis
AssumptionCheckerTest.cpp
AssumptionMakerTest.cpp
MonotonicityCheckerTest.cpp
MonotonicityHelperTest.cpp
OrderExtenderTest.cpp
OrderTest.cpp
► derivative
GradientDescentInstantiationSearcherTest.cpp
SparseDerivativeInstantiationModelCheckerTest.cpp
► modelchecker
ParametricDtmcPrctlModelCheckerTest.cpp
SparseDtmcParameterLiftingMonotoniciyTest.cpp
SparseDtmcParameterLiftingTest.cpp
SparseMdpParameterLiftingTest.cpp
SymbolicParametricDtmcPrctlModelCheckerTest.cpp
► transformer
BinaryDtmcTransformerTest.cpp
TimeTravellingTest.cpp
► utility
ModelInstantiatorTest.cpp
storm-test.cpp
► storm-permissive
► analysis
MilpPermissiveSchedulerTest.cpp
SmtPermissiveSchedulerTest.cpp
storm-test.cpp
► storm-pomdp
► analysis
QualitativeAnalysisTest.cpp
► api
BeliefExplorationAPITest.cpp
► modelchecker
BeliefExplorationPomdpModelCheckerTest.cpp
► tracking
BeliefSupportTrackingTest.cpp
► transformation
MakeCanonicTest.cpp
storm-test.cpp
storm_gtest.cpp
storm_gtest.h