sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

steadystate: Added a testcase.

tempestpy_adaptions
Tim Quatmann 4 years ago
parent
b73e2e5d1c
commit
818f8cb8ee
2 changed files with 336 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 221
      resources/examples/testfiles/ctmc/steadystatetest.jani
  2. 115
      src/test/storm/modelchecker/csl/SteadyStateCtmcCslModelCheckerTest.cpp

221
resources/examples/testfiles/ctmc/steadystatetest.jani
View File

@ -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
}
}
]
}

115
src/test/storm/modelchecker/csl/SteadyStateCtmcCslModelCheckerTest.cpp
View File

@ -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<ValueType> 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<storm::RationalNumber>(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<ValueType> 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<typename TestType>
class SteadyStateCtmcCslModelCheckerTest : public ::testing::Test {
public:
typedef typename TestType::ValueType ValueType;
typedef typename storm::models::sparse::Ctmc<ValueType> SparseModelType;
SteadyStateCtmcCslModelCheckerTest() : _environment(TestType::createEnvironment()) {}
storm::Environment const& env() const { return _environment; }
ValueType parseNumber(std::string const& input) const { return storm::utility::convertNumber<ValueType>(input);}
ValueType precision() const { return TestType::isExact ? parseNumber("0") : parseNumber("1e-6");}
bool isSparseModel() const { return std::is_same<typename TestType::ModelType, SparseModelType>::value; }
CtmcEngine getEngine() const { return TestType::engine; }
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<MT>>::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<ValueType>(janiDescr, storm::builder::BuilderOptions())->template as<MT>();
}
template <typename MT = typename TestType::ModelType>
typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::SparseCtmcCslModelChecker<MT>>>::type
createModelChecker(std::shared_ptr<MT> const& model) const {
if (TestType::engine == CtmcEngine::JaniSparse) {
return std::make_shared<storm::modelchecker::SparseCtmcCslModelChecker<SparseModelType>>(*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<ValueType>().getValueVector();
auto sortedVector = resultVector;
std::sort(sortedVector.begin(), sortedVector.end());
EXPECT_EQ(sortedVector[0], storm::utility::zero<ValueType>()) << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << std::endl;
EXPECT_EQ(sortedVector[1], storm::utility::zero<ValueType>()) << "Result of steady state computation is " << storm::utility::vector::toString(resultVector) << std::endl;
EXPECT_EQ(sortedVector[2], storm::utility::zero<ValueType>()) << "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;
}
}
Write Preview
Loading…
Cancel
Save