1#include "storm-config.h"
29enum class MaEngine { PrismSparse, JaniSparse, JaniHybrid };
31class SparseDoubleValueIterationEnvironment {
34 static const MaEngine engine = MaEngine::PrismSparse;
35 static const bool isExact =
false;
45class JaniSparseDoubleValueIterationEnvironment {
48 static const MaEngine engine = MaEngine::JaniSparse;
49 static const bool isExact =
false;
59class JaniHybridDoubleValueIterationEnvironment {
62 static const MaEngine engine = MaEngine::JaniHybrid;
63 static const bool isExact =
false;
73class SparseDoubleIntervalIterationEnvironment {
76 static const MaEngine engine = MaEngine::PrismSparse;
77 static const bool isExact =
false;
89class SparseRationalPolicyIterationEnvironment {
92 static const MaEngine engine = MaEngine::PrismSparse;
93 static const bool isExact =
true;
102class SparseRationalRationalSearchEnvironment {
105 static const MaEngine engine = MaEngine::PrismSparse;
106 static const bool isExact =
true;
116template<
typename TestType>
117class MarkovAutomatonCslModelCheckerTest :
public ::testing::Test {
119 typedef typename TestType::ValueType
ValueType;
123 MarkovAutomatonCslModelCheckerTest() : _environment(TestType::createEnvironment()) {}
125 void SetUp()
override {
127 GTEST_SKIP() <<
"Z3 not available.";
135 return storm::utility::convertNumber<ValueType>(input);
140 bool isSparseModel()
const {
141 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
143 bool isSymbolicModel()
const {
144 return std::is_same<typename TestType::ModelType, SymbolicModelType>::value;
147 template<
typename MT =
typename TestType::ModelType>
148 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
149 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
150 buildModelFormulas(std::string
const& pathToPrismFile, std::string
const& formulasAsString, std::string
const& constantDefinitionString =
"")
const {
151 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
154 if (TestType::engine == MaEngine::PrismSparse) {
156 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<MT>();
157 }
else if (TestType::engine == MaEngine::JaniSparse) {
160 result.first = storm::api::buildSparseModel<ValueType>(janiData.first, result.second)->template as<MT>();
165 template<
typename MT =
typename TestType::ModelType>
166 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
167 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>>>::type
168 buildModelFormulas(std::string
const& pathToPrismFile, std::string
const& formulasAsString, std::string
const& constantDefinitionString =
"")
const {
169 std::pair<std::shared_ptr<MT>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
174 result.first = storm::api::buildSymbolicModel<TestType::ddType, ValueType>(janiData.first, result.second)->template as<MT>();
178 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
179 std::vector<std::shared_ptr<storm::logic::Formula const>>
const& formulas)
const {
180 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
181 for (
auto const& f : formulas) {
182 result.emplace_back(*f);
187 template<
typename MT =
typename TestType::ModelType>
188 typename std::enable_if<std::is_same<MT, SparseModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type createModelChecker(
189 std::shared_ptr<MT>
const& model)
const {
190 if (TestType::engine == MaEngine::PrismSparse || TestType::engine == MaEngine::JaniSparse) {
191 return std::make_shared<storm::modelchecker::SparseMarkovAutomatonCslModelChecker<SparseModelType>>(*model);
196 template<
typename MT =
typename TestType::ModelType>
197 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value, std::shared_ptr<storm::modelchecker::AbstractModelChecker<MT>>>::type
198 createModelChecker(std::shared_ptr<MT>
const& model)
const {
199 if (TestType::engine == MaEngine::JaniHybrid) {
200 return std::make_shared<storm::modelchecker::HybridMarkovAutomatonCslModelChecker<SymbolicModelType>>(*model);
207 template<
typename MT =
typename TestType::ModelType>
208 typename std::enable_if<std::is_same<MT, SparseModelType>::value,
void>::type execute(std::shared_ptr<MT>
const& model,
209 std::function<
void()>
const& f)
const {
213 template<
typename MT =
typename TestType::ModelType>
214 typename std::enable_if<std::is_same<MT, SymbolicModelType>::value,
void>::type execute(std::shared_ptr<MT>
const& model,
215 std::function<
void()>
const& f)
const {
216 model->getManager().execute(f);
220 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
222 result->filter(*filter);
223 return result->asQualitativeCheckResult().forallTrue();
227 std::unique_ptr<storm::modelchecker::CheckResult>& result) {
229 result->filter(*filter);
230 return result->asQuantitativeCheckResult<
ValueType>().getMin();
237 if (isSparseModel()) {
238 return std::make_unique<storm::modelchecker::ExplicitQualitativeCheckResult>(model->template as<SparseModelType>()->getInitialStates());
240 return std::make_unique<storm::modelchecker::SymbolicQualitativeCheckResult<TestType::ddType>>(
241 model->template as<SymbolicModelType>()->getReachableStates(), model->template as<SymbolicModelType>()->getInitialStates());
246typedef ::testing::Types<SparseDoubleValueIterationEnvironment, JaniSparseDoubleValueIterationEnvironment, JaniHybridDoubleValueIterationEnvironment,
247 SparseDoubleIntervalIterationEnvironment, SparseRationalPolicyIterationEnvironment, SparseRationalRationalSearchEnvironment>
252TYPED_TEST(MarkovAutomatonCslModelCheckerTest, server) {
253 std::string formulasString =
"Tmax=? [F \"error\"]";
254 formulasString +=
"; Pmax=? [F \"processB\"]";
255 formulasString +=
"; Pmax=? [F<1 \"error\"]";
257 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ma/server.ma", formulasString);
258 auto model = std::move(modelFormulas.first);
259 auto tasks = this->getTasks(modelFormulas.second);
260 this->execute(model, [&]() {
261 EXPECT_EQ(6ul, model->getNumberOfStates());
262 EXPECT_EQ(10ul, model->getNumberOfTransitions());
264 auto checker = this->createModelChecker(model);
265 std::unique_ptr<storm::modelchecker::CheckResult> result;
267 result = checker->check(this->env(), tasks[0]);
270 result = checker->check(this->env(), tasks[1]);
274 result = checker->check(this->env(), tasks[2]);
280TYPED_TEST(MarkovAutomatonCslModelCheckerTest, simple) {
281 std::string formulasString =
"Pmin=? [F<1 s>2]";
282 formulasString +=
"; Pmax=? [F<1.3 s=3]";
284 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ma/simple.ma", formulasString);
285 auto model = std::move(modelFormulas.first);
286 auto tasks = this->getTasks(modelFormulas.second);
287 this->execute(model, [&]() {
288 EXPECT_EQ(5ul, model->getNumberOfStates());
289 EXPECT_EQ(8ul, model->getNumberOfTransitions());
291 auto checker = this->createModelChecker(model);
292 std::unique_ptr<storm::modelchecker::CheckResult> result;
295 result = checker->check(this->env(), tasks[0]);
298 result = checker->check(this->env(), tasks[1]);
304TYPED_TEST(MarkovAutomatonCslModelCheckerTest, simple2) {
305 std::string formulasString =
"R{\"rew0\"}max=? [C]";
306 formulasString +=
"; R{\"rew0\"}min=? [C]";
307 formulasString +=
"; R{\"rew1\"}max=? [C]";
308 formulasString +=
"; R{\"rew1\"}min=? [C]";
309 formulasString +=
"; R{\"rew2\"}max=? [C]";
310 formulasString +=
"; R{\"rew2\"}min=? [C]";
311 formulasString +=
"; R{\"rew3\"}min=? [C]";
312 formulasString +=
"; LRAmin=? [s=0 | s=3]";
313 formulasString +=
"; R{\"rew3\"}max=?[ LRA ]";
314 formulasString +=
"; R{\"rew3\"}min=?[ LRA ]";
316 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ma/simple2.ma", formulasString);
317 auto model = std::move(modelFormulas.first);
318 auto tasks = this->getTasks(modelFormulas.second);
319 EXPECT_EQ(6ul, model->getNumberOfStates());
320 EXPECT_EQ(11ul, model->getNumberOfTransitions());
322 auto checker = this->createModelChecker(model);
323 std::unique_ptr<storm::modelchecker::CheckResult> result;
325 if (TypeParam::engine != MaEngine::JaniHybrid) {
328 result = checker->check(this->env(), tasks[0]);
331 result = checker->check(this->env(), tasks[1]);
334 result = checker->check(this->env(), tasks[2]);
337 result = checker->check(this->env(), tasks[3]);
340 result = checker->check(this->env(), tasks[4]);
343 result = checker->check(this->env(), tasks[5]);
346 result = checker->check(this->env(), tasks[6]);
350#ifndef STORM_HAVE_Z3_OPTIMIZE
354 result = checker->check(this->env(), tasks[7]);
357 result = checker->check(this->env(), tasks[8]);
361 result = checker->check(this->env(), tasks[9]);
363#ifndef STORM_HAVE_Z3_OPTIMIZE
368TYPED_TEST(MarkovAutomatonCslModelCheckerTest, LtlSimple) {
369#ifdef STORM_HAVE_LTL_MODELCHECKING_SUPPORT
370 std::string formulasString =
"Pmax=? [X X s=3]";
371 formulasString +=
"; Pmax=? [X X G s>2]";
372 formulasString +=
"; Pmin=? [X X G s>2]";
373 formulasString +=
"; Pmax=? [F ((s=0) U X(s=0) & X(s=2))]";
375 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ma/simple.ma", formulasString);
376 auto model = std::move(modelFormulas.first);
377 auto tasks = this->getTasks(modelFormulas.second);
378 EXPECT_EQ(5ul, model->getNumberOfStates());
379 EXPECT_EQ(8ul, model->getNumberOfTransitions());
381 auto checker = this->createModelChecker(model);
382 std::unique_ptr<storm::modelchecker::CheckResult> result;
385 if (TypeParam::engine == MaEngine::PrismSparse || TypeParam::engine == MaEngine::JaniSparse) {
386 result = checker->check(this->env(), tasks[0]);
389 result = checker->check(this->env(), tasks[1]);
392 result = checker->check(this->env(), tasks[2]);
395 result = checker->check(this->env(), tasks[3]);
399 EXPECT_FALSE(checker->canHandle(tasks[0]));
406TYPED_TEST(MarkovAutomatonCslModelCheckerTest, HOASimple) {
408 std::string formulasString =
"; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR
"/hoa/automaton_Fandp0Xp1.hoa\", \"p0\" -> (s>1), \"p1\" -> !(s=1) }]";
410 formulasString +=
"; P=?[HOA: {\"" STORM_TEST_RESOURCES_DIR
"/hoa/automaton_UXp0p1.hoa\", \"p0\" -> (s=2), \"p1\" -> (s=1) }]";
412 auto modelFormulas = this->buildModelFormulas(STORM_TEST_RESOURCES_DIR
"/ma/simple.ma", formulasString);
413 auto model = std::move(modelFormulas.first);
414 auto tasks = this->getTasks(modelFormulas.second);
415 EXPECT_EQ(5ul, model->getNumberOfStates());
416 EXPECT_EQ(8ul, model->getNumberOfTransitions());
418 auto checker = this->createModelChecker(model);
419 std::unique_ptr<storm::modelchecker::CheckResult> result;
422 if (TypeParam::engine == MaEngine::PrismSparse || TypeParam::engine == MaEngine::JaniSparse) {
423 result = checker->check(tasks[0]);
426 result = checker->check(tasks[1]);
429 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)
SolverEnvironment & solver()
void setPrecision(storm::RationalNumber value)
void setMethod(storm::solver::MinMaxMethod value, bool isSetFromDefault=false)
void setRelativeTerminationCriterion(bool value)
MinMaxSolverEnvironment & minMax()
void setForceSoundness(bool value)
This class represents a Markov automaton.
This class represents a discrete-time Markov decision process.
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 isZero(ValueType const &a)
bool isInfinity(ValueType const &a)
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes