diff --git a/resources/examples/testfiles/ctmc/steadystatetest.jani b/resources/examples/testfiles/ctmc/steadystatetest.jani new file mode 100644 index 000000000..8f9b4cf03 --- /dev/null +++ b/resources/examples/testfiles/ctmc/steadystatetest.jani @@ -0,0 +1,221 @@ +{ + "actions": [], + "automata": [ + { + "edges": [ + { + "destinations": [ + { + "location": "scc1-2", + "probability": { + "exp": 1 + } + } + ], + "guard": { + "exp": true + }, + "location": "scc1-1", + "rate": { + "exp": 3 + } + }, + { + "destinations": [ + { + "location": "scc1-1", + "probability": { + "exp": 0.5 + } + }, + { + "location": "l-2", + "probability": { + "exp": 0.5 + } + } + ], + "guard": { + "exp": true + }, + "location": "scc1-2", + "rate": { + "exp": 1 + } + }, + { + "destinations": [ + { + "location": "bscc1", + "probability": { + "exp": 0.5 + } + }, + { + "location": "bscc3-1", + "probability": { + "exp": 0.5 + } + } + ], + "guard": { + "exp": true + }, + "location": "scc1-1", + "rate": { + "exp": 1 + } + }, + { + "destinations": [ + { + "location": "bscc2", + "probability": { + "exp": 0.3 + } + }, + { + "location": "l-2", + "probability": { + "exp": 0.7 + } + } + ], + "guard": { + "exp": true + }, + "location": "l-2", + "rate": { + "exp": 2 + } + }, + { + "destinations": [ + { + "location": "bscc2", + "probability": { + "exp": 1 + } + } + ], + "guard": { + "exp": true + }, + "location": "bscc2", + "rate": { + "exp": 4 + } + }, + { + "destinations": [ + { + "location": "bscc3-1", + "probability": { + "exp": 1 + } + } + ], + "guard": { + "exp": true + }, + "location": "bscc3-3", + "rate": { + "exp": 1 + } + }, + { + "destinations": [ + { + "location": "bscc3-3", + "probability": { + "exp": 1 + } + } + ], + "guard": { + "exp": true + }, + "location": "bscc3-2", + "rate": { + "exp": 2 + } + }, + { + "destinations": [ + { + "location": "bscc3-2", + "probability": { + "exp": 1 + } + } + ], + "guard": { + "exp": true + }, + "location": "bscc3-1", + "rate": { + "exp": 4 + } + } + ], + "initial-locations": [ + "scc1-1" + ], + "locations": [ + { + "name": "scc1-1" + }, + { + "name": "l-2" + }, + { + "name": "bscc3-3" + }, + { + "name": "scc1-2" + }, + { + "name": "bscc2" + }, + { + "name": "bscc1" + }, + { + "name": "bscc3-2" + }, + { + "name": "bscc3-1" + } + ], + "name": "element_name" + } + ], + "features": [ + "derived-operators", + "functions", + "state-exit-rewards" + ], + "jani-version": 1, + "name": "steadystatedistrtest", + "system": { + "elements": [ + { + "automaton": "element_name" + } + ] + }, + "type": "ctmc", + "variables": [ + { + "initial-value": 0, + "name": "x", + "transient": false, + "type": { + "base": "int", + "kind": "bounded", + "lower-bound": 0, + "upper-bound": 1 + } + } + ] +} \ No newline at end of file diff --git a/src/test/storm/modelchecker/csl/SteadyStateCtmcCslModelCheckerTest.cpp b/src/test/storm/modelchecker/csl/SteadyStateCtmcCslModelCheckerTest.cpp new file mode 100755 index 000000000..0ec233754 --- /dev/null +++ b/src/test/storm/modelchecker/csl/SteadyStateCtmcCslModelCheckerTest.cpp @@ -0,0 +1,115 @@ +#include "test/storm_gtest.h" +#include "test/storm_gtest.h" +#include "storm-config.h" + +#include "storm/api/builder.h" +#include "storm-parsers/api/model_descriptions.h" +#include "storm/models/sparse/StandardRewardModel.h" +#include "storm/models/sparse/Ctmc.h" +#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h" +#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" +#include "storm/environment/solver/NativeSolverEnvironment.h" +#include "storm/environment/solver/GmmxxSolverEnvironment.h" +#include "storm/environment/solver/EigenSolverEnvironment.h" + +namespace { + + enum class CtmcEngine {JaniSparse}; + + class SparseGmmxxGmresIluEnvironment { + public: + static const CtmcEngine engine = CtmcEngine::JaniSparse; + static const bool isExact = false; + typedef double ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Gmmxx); + env.solver().gmmxx().setMethod(storm::solver::GmmxxLinearEquationSolverMethod::Gmres); + env.solver().gmmxx().setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner::Ilu); + //env.solver().gmmxx().setPrecision(storm::utility::convertNumber(1e-6)); // Need to increase precision because eq sys yields incorrect results + return env; + } + }; + + class SparseEigenRationalLuEnvironment { + public: + static const CtmcEngine engine = CtmcEngine::JaniSparse; + static const bool isExact = true; + typedef storm::RationalNumber ValueType; + typedef storm::models::sparse::Ctmc ModelType; + static storm::Environment createEnvironment() { + storm::Environment env; + env.solver().setLinearEquationSolverType(storm::solver::EquationSolverType::Eigen); + env.solver().eigen().setMethod(storm::solver::EigenLinearEquationSolverMethod::SparseLU); + env.solver().setForceExact(true); + return env; + } + }; + + template + class SteadyStateCtmcCslModelCheckerTest : public ::testing::Test { + public: + typedef typename TestType::ValueType ValueType; + typedef typename storm::models::sparse::Ctmc SparseModelType; + + SteadyStateCtmcCslModelCheckerTest() : _environment(TestType::createEnvironment()) {} + storm::Environment const& env() const { return _environment; } + ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber(input);} + ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");} + bool isSparseModel() const { return std::is_same::value; } + CtmcEngine getEngine() const { return TestType::engine; } + + template + typename std::enable_if::value, std::shared_ptr>::type + buildJaniModel(std::string const& pathToJaniModel, std::string const& constantDefinitionString = "") const { + auto janiDescr = storm::storage::SymbolicModelDescription(storm::api::parseJaniModel(pathToJaniModel).first); + janiDescr = janiDescr.preprocess(constantDefinitionString); + return storm::api::buildSparseModel(janiDescr, storm::builder::BuilderOptions())->template as(); + } + + template + typename std::enable_if::value, std::shared_ptr>>::type + createModelChecker(std::shared_ptr const& model) const { + if (TestType::engine == CtmcEngine::JaniSparse) { + return std::make_shared>(*model); + } + return nullptr; + } + + private: + storm::Environment _environment; + + }; + + typedef ::testing::Types< + SparseGmmxxGmresIluEnvironment, + SparseEigenRationalLuEnvironment + > TestingTypes; + + TYPED_TEST_SUITE(SteadyStateCtmcCslModelCheckerTest, TestingTypes,); + + TYPED_TEST(SteadyStateCtmcCslModelCheckerTest, steadystatetest) { + typedef typename TestFixture::ValueType ValueType; + + auto model = this->buildJaniModel(STORM_TEST_RESOURCES_DIR "/ctmc/steadystatetest.jani"); + EXPECT_EQ(8ul, model->getNumberOfStates()); + EXPECT_EQ(12ul, model->getNumberOfTransitions()); + ASSERT_EQ(model->getType(), storm::models::ModelType::Ctmc); + auto checker = this->createModelChecker(model); + auto result = checker->computeSteadyStateDistribution(this->env()); + + ASSERT_TRUE(result->isExplicitQuantitativeCheckResult()); + auto resultVector = result->template asExplicitQuantitativeCheckResult().getValueVector(); + auto sortedVector = resultVector; + std::sort(sortedVector.begin(), sortedVector.end()); + EXPECT_EQ(sortedVector[0], storm::utility::zero()) << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << std::endl; + EXPECT_EQ(sortedVector[1], storm::utility::zero()) << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << std::endl; + EXPECT_EQ(sortedVector[2], storm::utility::zero()) << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << std::endl; + EXPECT_NEAR(sortedVector[3], this->parseNumber("1/35"),this->precision()) << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << std::endl; + EXPECT_NEAR(sortedVector[4], this->parseNumber("2/35"),this->precision()) << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << std::endl; + EXPECT_NEAR(sortedVector[5], this->parseNumber("4/35"),this->precision()) << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << std::endl; + EXPECT_NEAR(sortedVector[6], this->parseNumber("1/5"),this->precision()) << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << std::endl; + EXPECT_NEAR(sortedVector[7], this->parseNumber("3/5"),this->precision()) << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << std::endl; + } +}