1#include "storm-config.h"
31enum class CtmcEngine { PrismSparse, JaniSparse, PrismHybrid, JaniHybrid };
33class SparseGmmxxGmresIluEnvironment {
36 static const CtmcEngine engine = CtmcEngine::PrismSparse;
37 static const bool isExact =
false;
50class JaniSparseGmmxxGmresIluEnvironment {
53 static const CtmcEngine engine = CtmcEngine::JaniSparse;
54 static const bool isExact =
false;
67class SparseEigenDGmresEnvironment {
70 static const CtmcEngine engine = CtmcEngine::PrismSparse;
71 static const bool isExact =
false;
84class SparseEigenDoubleLUEnvironment {
87 static const CtmcEngine engine = CtmcEngine::PrismSparse;
88 static const bool isExact =
false;
99class SparseNativeSorEnvironment {
102 static const CtmcEngine engine = CtmcEngine::PrismSparse;
103 static const bool isExact =
false;
117class HybridCuddGmmxxGmresEnvironment {
120 static const CtmcEngine engine = CtmcEngine::PrismHybrid;
121 static const bool isExact =
false;
133class JaniHybridCuddGmmxxGmresEnvironment {
136 static const CtmcEngine engine = CtmcEngine::JaniHybrid;
137 static const bool isExact =
false;
149class HybridSylvanGmmxxGmresEnvironment {
152 static const CtmcEngine engine = CtmcEngine::PrismHybrid;
153 static const bool isExact =
false;
165template<
typename TestType>
166class CtmcCslModelCheckerTest :
public ::testing::Test {
168 typedef typename TestType::ValueType
ValueType;
172 CtmcCslModelCheckerTest() : _environment(TestType::createEnvironment()) {}
174 void SetUp()
override {
176 GTEST_SKIP() <<
"Z3 not available.";
184 return storm::utility::convertNumber<ValueType>(input);
189 bool isSparseModel()
const {
190 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
192 bool isSymbolicModel()
const {
193 return std::is_same<typename TestType::ModelType, SymbolicModelType>::value;
195 CtmcEngine getEngine()
const {
196 return TestType::engine;
199 template<
typename MT =
typename TestType::ModelType>
200 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
201 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
202 buildModelFormulas(std::string
const& pathToPrismFile, std::string
const& formulasAsString, std::string
const& constantDefinitionString =
"")
const {
203 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
206 if (TestType::engine == CtmcEngine::PrismSparse) {
208 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
209 }
else if (TestType::engine == CtmcEngine::JaniSparse) {
211 janiData.first.substituteFunctions();
213 result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second)->template as<MT>();
218 template<
typename MT =
typename TestType::ModelType>
219 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
220 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
221 buildModelFormulas(std::string
const& pathToPrismFile, std::string
const& formulasAsString, std::string
const& constantDefinitionString =
"")
const {
222 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
225 if (TestType::engine == CtmcEngine::PrismHybrid) {
227 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(program, result.second)->template as<MT>();
228 }
else if (TestType::engine == CtmcEngine::JaniHybrid) {
230 janiData.first.substituteFunctions();
232 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
237 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
238 std::vector<std::shared_ptr<storm::logic::Formula const>>
const& formulas)
const {
239 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
240 for (
auto const& f : formulas) {
241 result.emplace_back(*f);
246 template<
typename MT =
typename TestType::ModelType>
247 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type createModelChecker(
248 std::shared_ptr<MT>
const& model)
const {
249 if (TestType::engine == CtmcEngine::PrismSparse || TestType::engine == CtmcEngine::JaniSparse) {
250 return std::make_shared<storm::modelchecker::SparseCtmcCslModelChecker<SparseModelType>>(*model);
254 template<
typename MT =
typename TestType::ModelType>
255 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
256 createModelChecker(std::shared_ptr<MT>
const& model)
const {
257 if (TestType::engine == CtmcEngine::PrismHybrid || TestType::engine == CtmcEngine::JaniHybrid) {
258 return std::make_shared<storm::modelchecker::HybridCtmcCslModelChecker<SymbolicModelType>>(*model);
262 template<
typename MT =
typename TestType::ModelType>
263 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
void>::type execute(std::shared_ptr<MT>
const& model,
264 std::function<
void()>
const& f)
const {
268 template<
typename MT =
typename TestType::ModelType>
269 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
void>::type execute(std::shared_ptr<MT>
const& model,
270 std::function<
void()>
const& f)
const {
271 model->getManager().execute(f);
275 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
277 result->filter(*filter);
278 return result->asQualitativeCheckResult().forallTrue();
282 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
284 result->filter(*filter);
285 return result->asQuantitativeCheckResult<
ValueType>().getMin();
292 if (isSparseModel()) {
293 return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
295 return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(
296 model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
301typedef ::testing::Types<
303 SparseGmmxxGmresIluEnvironment, JaniSparseGmmxxGmresIluEnvironment, HybridCuddGmmxxGmresEnvironment, JaniHybridCuddGmmxxGmresEnvironment,
304 HybridSylvanGmmxxGmresEnvironment,
306 SparseNativeSorEnvironment, SparseEigenDGmresEnvironment, SparseEigenDoubleLUEnvironment>
312 std::string formulasString =
"P=? [ F<=100 !\"minimum\"]";
313 formulasString +=
"; P=? [ F[100,100] !\"minimum\"]";
314 formulasString +=
"; P=? [ F[100,2000] !\"minimum\"]";
315 formulasString +=
"; P=? [ \"minimum\" U<=10 \"premium\"]";
316 formulasString +=
"; P=? [ !\"minimum\" U>=1 \"minimum\"]";
317 formulasString +=
"; P=? [ \"minimum\" U>=1 !\"minimum\"]";
318 formulasString +=
"; R=? [C<=100]";
320 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ctmc/cluster2.sm", formulasString);
321 auto model = std::move(modelFormulas.first);
322 auto tasks = this->getTasks(modelFormulas.second);
323 this->execute(model, [&]() {
324 EXPECT_EQ(276ul, model->getNumberOfStates());
325 EXPECT_EQ(1120ul, model->getNumberOfTransitions());
327 auto checker = this->createModelChecker(model);
328 std::unique_ptr<storm::modelchecker::CheckResult> result;
330 result = checker->check(this->env(), tasks[0]);
333 result = checker->check(this->env(), tasks[1]);
336 result = checker->check(this->env(), tasks[2]);
339 result = checker->check(this->env(), tasks[3]);
342 result = checker->check(this->env(), tasks[4]);
345 result = checker->check(this->env(), tasks[5]);
348 result = checker->check(this->env(), tasks[6]);
353TYPED_TEST(CtmcCslModelCheckerTest, Embedded) {
354 std::string formulasString =
"P=? [ F<=10000 \"down\"]";
355 formulasString +=
"; P=? [ !\"down\" U<=10000 \"fail_actuators\"]";
356 formulasString +=
"; P=? [ !\"down\" U<=10000 \"fail_io\"]";
357 formulasString +=
"; P=? [ !\"down\" U<=10000 \"fail_sensors\"]";
358 formulasString +=
"; R{\"up\"}=? [C<=10000]";
360 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ctmc/embedded2.sm", formulasString);
361 auto model = std::move(modelFormulas.first);
362 auto tasks = this->getTasks(modelFormulas.second);
363 this->execute(model, [&]() {
364 EXPECT_EQ(3478ul, model->getNumberOfStates());
365 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
367 auto checker = this->createModelChecker(model);
368 std::unique_ptr<storm::modelchecker::CheckResult> result;
370 result = checker->check(this->env(), tasks[0]);
373 result = checker->check(this->env(), tasks[1]);
376 result = checker->check(this->env(), tasks[2]);
379 result = checker->check(this->env(), tasks[3]);
382 result = checker->check(this->env(), tasks[4]);
388 std::string formulasString =
"P=? [ F<=10 \"network_full\" ]";
389 formulasString +=
"; P=? [ F<=10 \"first_queue_full\" ]";
390 formulasString +=
"; P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]";
391 formulasString +=
"; R=? [I=10]";
392 formulasString +=
"; R=? [C<=10]";
393 formulasString +=
"; R=? [F \"first_queue_full\"&\"second_queue_full\"]";
395 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ctmc/tandem5.sm", formulasString);
396 auto model = std::move(modelFormulas.first);
397 auto tasks = this->getTasks(modelFormulas.second);
398 this->execute(model, [&]() {
399 EXPECT_EQ(66ul, model->getNumberOfStates());
400 EXPECT_EQ(189ul, model->getNumberOfTransitions());
402 auto checker = this->createModelChecker(model);
403 std::unique_ptr<storm::modelchecker::CheckResult> result;
405 result = checker->check(this->env(), tasks[0]);
408 result = checker->check(this->env(), tasks[1]);
411 result = checker->check(this->env(), tasks[2]);
414 result = checker->check(this->env(), tasks[3]);
417 result = checker->check(this->env(), tasks[4]);
420 result = checker->check(this->env(), tasks[5]);
426 std::string formulasString =
"P=? [ F<=0.5 x=1 ]";
427 formulasString +=
"; R=? [ C<=0.1 ]";
428 formulasString +=
"; R=? [ C<=1 ]";
429 formulasString +=
"; R=? [ C<=10 ]";
431 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ctmc/simple1.sm", formulasString);
432 auto model = std::move(modelFormulas.first);
433 auto tasks = this->getTasks(modelFormulas.second);
434 this->execute(model, [&]() {
435 EXPECT_EQ(2ul, model->getNumberOfStates());
436 EXPECT_EQ(2ul, model->getNumberOfTransitions());
438 auto checker = this->createModelChecker(model);
439 std::unique_ptr<storm::modelchecker::CheckResult> result;
441 uint64_t propertyIndex = 0;
443 result = checker->check(this->env(), tasks[propertyIndex++]);
447 result = checker->check(this->env(), tasks[propertyIndex++]);
451 result = checker->check(this->env(), tasks[propertyIndex++]);
455 result = checker->check(this->env(), tasks[propertyIndex++]);
461 std::string formulasString =
"R{\"rew1\"}=? [ C ]";
462 formulasString +=
"; R{\"rew2\"}=? [ C ]";
464 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ctmc/simple2.sm", formulasString);
465 auto model = std::move(modelFormulas.first);
466 auto tasks = this->getTasks(modelFormulas.second);
467 EXPECT_EQ(5ul, model->getNumberOfStates());
468 EXPECT_EQ(8ul, model->getNumberOfTransitions());
470 auto checker = this->createModelChecker(model);
471 std::unique_ptr<storm::modelchecker::CheckResult> result;
474 if (this->isSparseModel()) {
475 result = checker->check(this->env(), tasks[0]);
478 result = checker->check(this->env(), tasks[1]);
481 EXPECT_FALSE(checker->canHandle(tasks[0]));
485TEST(CtmcCslModelCheckerTest, TransientProbabilities) {
492 std::vector<double> exitRates = {3, 2};
494 initialStates.set(0);
498 std::vector<double> result =
501 EXPECT_NEAR(0.404043, result[0], 1e-6);
502 EXPECT_NEAR(0.595957, result[1], 1e-6);
505TYPED_TEST(CtmcCslModelCheckerTest, LtlProbabilitiesEmbedded) {
506#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
507 std::string formulasString =
"P=? [ X F (!\"down\" U \"fail_sensors\") ]";
508 formulasString +=
"; P=? [ (! \"down\" U ( F \"fail_actuators\" U \"fail_io\")) ]";
509 formulasString +=
"; P=? [ F \"down\" & X G \"fail_sensors\" ]";
510 formulasString +=
"; P<1 [ F \"down\" & X G \"fail_sensors\" ]";
511 formulasString +=
"; P>0.9 [ F \"down\" & X G \"fail_sensors\" ]";
512 formulasString +=
"; P=? [ ( X X X X X X !\"down\") ]";
514 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ctmc/embedded2.sm", formulasString);
515 auto model = std::move(modelFormulas.first);
516 auto tasks = this->getTasks(modelFormulas.second);
517 EXPECT_EQ(3478ul, model->getNumberOfStates());
518 EXPECT_EQ(14639ul, model->getNumberOfTransitions());
521 auto checker = this->createModelChecker(model);
522 std::unique_ptr<storm::modelchecker::CheckResult> result;
523 if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse) {
524 result = checker->check(this->env(), tasks[0]);
528 result = checker->check(this->env(), tasks[1]);
530 "18202096756782580932452575931626387221032158256811408997544247061630654697057679936888914805428640014003923523854237983369404268771063"
531 "94069377761908861354080901656982334306495936806479819524633477460248734957778578143867737103318041699906745291007545836953677741618755"
532 "07044994661278270139591275881461260070117701448841596602041739425021618556458197240253807881255308059191194657575523127649292873946401"
533 "60070574497678932806876628747257457080365284815733250063282059801375609508589060775771365121570763916254686586313389233475877585811662"
534 "0357147078085971884542677483086820336410289852315689173054718889915988181632722920483222289764504589120520736097022590652379/"
535 "20728856609142464902872005939672257918093593973189631748243740034008572994831983832074458796252899535111673563261006250198416596416082"
536 "47438209685029840433936315271626219407003724379672398699027456844707912472180250116299363836831808191736954813578721274144593836954580"
537 "34829702750095798077157671737142972112983783526417917830063407814131534204102733837172200651731758231462705370319722286895248244604663"
538 "52533471344327110886363060826404895467465893956592712512371350202090241564215213495275079722307576230931018615138366081056985311311073"
539 "6677679624520398243456708277522978182665363672039087497825748539279661186260492946647251487454498033763681938956076478285935"),
542 result = checker->check(this->env(), tasks[2]);
545 result = checker->check(this->env(), tasks[3]);
546 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
548 result = checker->check(this->env(), tasks[4]);
549 EXPECT_TRUE(this->getQualitativeResultAtInitialState(model, result));
551 result = checker->check(this->env(), tasks[5]);
553 this->
parseNumber(
"12029468814241604838132837548112161585296814078767944885625781581320425536116175992062768102403002605220660026092168995568067825"
554 "92159369214025808794108439870476812421358247413140536419394633974952856222783873484713998841710951907938016323396243234904692402"
555 "52961677855027461283258094829047603758584033514598048083454101721311299129841296115907033485846297142252703801497367159453680266"
556 "24792167429109658151655487647994259314643886424142766790442953987818429468012101992798588110824350651761547347356873144826620057"
557 "74077569191240855183945543277103593833128730289929192543135438680962528094118605758445585995100073617/"
558 "12029720509287104832319318812972923934077469133245668896466828391759984671516390780365666074295318137833660807349293929200056244"
559 "56488274509559191073647430577878963431232759904608946782891839010213213206349818700590576273106941528872428420715245020013732520"
560 "85567053299253798937031071047697289051751242127258744937438520681995840650837777808189738580512102669860241858552660166073849086"
561 "67980634152813607901785527175246314720373131268228013598128613517599905951566964079825880226357974174647948493893065216449623389"
562 "15119549986021747121828809226061546105390273235103310319147341214480736689719855550298904337697187500"),
566 EXPECT_FALSE(checker->canHandle(tasks[0]));
573TYPED_TEST(CtmcCslModelCheckerTest, LtlProbabilitiesPolling) {
574#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
575 std::string formulasString =
"P=? [ X X !(s=1 & a=1) U (s=2 & a=1) ]";
576 formulasString +=
"; P=? [ X (( !(s=1) U (a=1)) U (s=1)) ]";
578 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ctmc/polling2.sm", formulasString);
579 auto model = std::move(modelFormulas.first);
580 auto tasks = this->getTasks(modelFormulas.second);
581 EXPECT_EQ(12ul, model->getNumberOfStates());
582 EXPECT_EQ(22ul, model->getNumberOfTransitions());
585 auto checker = this->createModelChecker(model);
586 std::unique_ptr<storm::modelchecker::CheckResult> result;
588 if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse) {
589 result = checker->check(this->env(), tasks[0]);
592 result = checker->check(this->env(), tasks[1]);
596 EXPECT_FALSE(checker->canHandle(tasks[0]));
603TYPED_TEST(CtmcCslModelCheckerTest, HOAProbabilitiesPolling) {
605 std::string formulasString =
"; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR
"/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> \"target\", \"p1\" -> (s=1) }]";
607 formulasString +=
"; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR
"/hoa/automaton_UXp0p1.hoa\", \"p0\" -> !(s=1) , \"p1\" -> \"target\" }]";
609 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ctmc/polling2.sm", formulasString);
610 auto model = std::move(modelFormulas.first);
611 auto tasks = this->getTasks(modelFormulas.second);
612 EXPECT_EQ(12ul, model->getNumberOfStates());
613 EXPECT_EQ(22ul, model->getNumberOfTransitions());
615 auto checker = this->createModelChecker(model);
616 std::unique_ptr<storm::modelchecker::CheckResult> result;
619 if (TypeParam::engine == CtmcEngine::PrismSparse || TypeParam::engine == CtmcEngine::JaniSparse) {
620 result = checker->check(tasks[0]);
623 result = checker->check(tasks[1]);
626 EXPECT_FALSE(checker->canHandle(tasks[0]));
std::unique_ptr< storm::modelchecker::QualitativeCheckResult > getInitialStateFilter(std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model)
double getQuantitativeResultAtInitialState(std::shared_ptr< storm::models::sparse::Model< storm::Interval > > const &model, std::unique_ptr< storm::modelchecker::CheckResult > &result)
void setPrecision(storm::RationalNumber value)
void setPreconditioner(storm::solver::EigenLinearEquationSolverPreconditioner value)
void setMethod(storm::solver::EigenLinearEquationSolverMethod value)
SolverEnvironment & solver()
void setMethod(storm::solver::GmmxxLinearEquationSolverMethod value)
void setPrecision(storm::RationalNumber value)
void setPreconditioner(storm::solver::GmmxxLinearEquationSolverPreconditioner value)
void setMaximalNumberOfIterations(uint64_t value)
void setMethod(storm::solver::NativeLinearEquationSolverMethod value)
void setRelativeTerminationCriterion(bool value)
void setPrecision(storm::RationalNumber value)
void setLinearEquationSolverType(storm::solver::EquationSolverType const &value, bool isSetFromDefault=false)
EigenSolverEnvironment & eigen()
NativeSolverEnvironment & native()
GmmxxSolverEnvironment & gmmxx()
static std::vector< ValueType > computeAllTransientProbabilities(Environment const &env, storm::storage::SparseMatrix< ValueType > const &rateMatrix, storm::storage::BitVector const &initialStates, storm::storage::BitVector const &phiStates, storm::storage::BitVector const &psiStates, std::vector< ValueType > const &exitRates, double timeBound)
This class represents a continuous-time Markov chain.
This class represents a continuous-time Markov chain.
A bit vector that is internally represented as a vector of 64-bit values.
A class that can be used to build a sparse matrix by adding value by value.
void addNextValue(index_type row, index_type column, value_type const &value)
Sets the matrix entry at the given row and column to the given value.
SparseMatrix< value_type > build(index_type overriddenRowCount=0, index_type overriddenColumnCount=0, index_type overriddenRowGroupCount=0)
A class that holds a possibly non-square matrix in the compressed row storage format.
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
storm::prism::Program parseProgram(std::string const &filename, bool prismCompatibility, bool simplify)
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
std::pair< storm::jani::Model, std::vector< storm::jani::Property > > convertPrismToJani(storm::prism::Program const &program, storm::converter::PrismToJaniConverterOptions options)
SFTBDDChecker::ValueType ValueType
NumberType parseNumber(std::string const &value)
Parse number from string.
storm::prism::Program preprocess(storm::prism::Program const &program, std::map< storm::expressions::Variable, storm::expressions::Expression > const &constantDefinitions)
storm::storage::BitVector filter(std::vector< T > const &values, std::function< bool(T const &value)> const &function)
Retrieves a bit vector containing all the indices for which the value at this position makes the give...
bool isInfinity(ValueType const &a)
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes