|
Storm 1.11.1.1
A Modern Probabilistic Model Checker
|
#include <carl/formula/Constraint.h>#include <memory>#include <string>#include "storm-config.h"#include "storm-pars/api/region.h"#include "storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h"#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h"#include "storm-pars/transformer/BinaryDtmcTransformer.h"#include "storm-parsers/parser/AutoParser.h"#include "storm-parsers/parser/FormulaParser.h"#include "storm/adapters/RationalFunctionAdapter.h"#include "storm/adapters/RationalNumberAdapter.h"#include "storm/api/bisimulation.h"#include "storm/api/builder.h"#include "storm/environment/Environment.h"#include "storm/modelchecker/CheckTask.h"#include "storm/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"#include "storm/models/sparse/Dtmc.h"#include "storm/models/sparse/Model.h"#include "storm/solver/OptimizationDirection.h"#include "storm/storage/bisimulation/BisimulationType.h"#include "storm/storage/prism/Program.h"#include "storm/utility/prism.h"#include "test/storm_gtest.h"#include "storm-parsers/api/storm-parsers.h"#include "storm/utility/constants.h"#include "storm/utility/logging.h"#include "storm/utility/macros.h"
Go to the source code of this file.
Classes | |
| class | BinaryDtmcTransformer |
Functions | |
| void | testModelB (std::string programFile, std::string formulaAsString, std::string constantsAsString) |
| TEST_F (BinaryDtmcTransformer, Crowds) | |
| TEST_F (BinaryDtmcTransformer, Nand) | |
| TEST_F (BinaryDtmcTransformer, Brp) | |
| TEST_F | ( | BinaryDtmcTransformer | , |
| Brp | |||
| ) |
Definition at line 157 of file BinaryDtmcTransformerTest.cpp.
| TEST_F | ( | BinaryDtmcTransformer | , |
| Crowds | |||
| ) |
Definition at line 145 of file BinaryDtmcTransformerTest.cpp.
| TEST_F | ( | BinaryDtmcTransformer | , |
| Nand | |||
| ) |
Definition at line 151 of file BinaryDtmcTransformerTest.cpp.
| void testModelB | ( | std::string | programFile, |
| std::string | formulaAsString, | ||
| std::string | constantsAsString | ||
| ) |
Definition at line 33 of file BinaryDtmcTransformerTest.cpp.