3#include "storm-config.h"
18class SparseDoubleRestartEnvironment {
20 static const bool isExact =
false;
31class SparseDoubleBisectionEnvironment {
33 static const bool isExact =
false;
43class SparseDoubleBisectionAdvancedEnvironment {
45 static const bool isExact =
false;
55class SparseDoublePiEnvironment {
57 static const bool isExact =
false;
67class SparseRationalNumberRestartEnvironment {
69 static const bool isExact =
true;
80class SparseRationalNumberBisectionEnvironment {
82 static const bool isExact =
true;
92class SparseRationalNumberBisectionAdvancedEnvironment {
94 static const bool isExact =
true;
104class SparseRationalNumberPiEnvironment {
106 static const bool isExact =
true;
116template<
typename TestType>
117class ConditionalMdpPrctlModelCheckerTest :
public ::testing::Test {
119 typedef typename TestType::ValueType
ValueType;
122 ConditionalMdpPrctlModelCheckerTest() : _environment(TestType::createEnvironment()) {}
124 void SetUp()
override {
126 GTEST_SKIP() <<
"Z3 not available.";
134 return storm::utility::convertNumber<ValueType>(input);
139 bool isSparseModel()
const {
140 return std::is_same<typename TestType::ModelType, SparseModelType>::value;
143 std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> buildModelFormulas(
144 storm::prism::Program const& inputProgram, std::string
const& formulasAsString, std::string
const& constantDefinitionString =
"")
const {
145 std::pair<std::shared_ptr<SparseModelType>, std::vector<std::shared_ptr<storm::logic::Formula const>>> result;
148 result.first = storm::api::buildSparseModel<ValueType>(program, result.second)->template as<SparseModelType>();
152 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> getTasks(
153 std::vector<std::shared_ptr<storm::logic::Formula const>>
const& formulas)
const {
154 std::vector<storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>> result;
155 for (
auto const& f : formulas) {
156 result.emplace_back(*f,
true);
165typedef ::testing::Types<SparseDoubleRestartEnvironment, SparseDoubleBisectionEnvironment, SparseDoubleBisectionAdvancedEnvironment, SparseDoublePiEnvironment,
166 SparseRationalNumberRestartEnvironment, SparseRationalNumberBisectionEnvironment, SparseRationalNumberBisectionAdvancedEnvironment,
167 SparseRationalNumberPiEnvironment>
172TYPED_TEST(ConditionalMdpPrctlModelCheckerTest, two_dice) {
173 typedef typename TestFixture::ValueType
ValueType;
175 std::string
const formulasString =
176 "Pmax=? [F \"twelve\" || F d1=6];"
177 "Pmin=? [F \"twelve\" || F d1=6];"
178 "Pmax=? [F \"seven\" || F d2=4];"
179 "Pmin=? [F \"seven\" || F d2=4];"
180 "Pmax=? [F \"two\" || F d2=2];"
181 "Pmin=? [F \"two\" || F d2=2];"
182 "Pmax=? [F d1=6 || F \"twelve\"];"
183 "Pmin=? [F d1=6 || F \"twelve\"];";
186 auto modelFormulas = this->buildModelFormulas(program, formulasString);
187 auto model = std::move(modelFormulas.first);
188 auto tasks = this->getTasks(modelFormulas.second);
189 EXPECT_EQ(169ul, model->getNumberOfStates());
190 EXPECT_EQ(436ul, model->getNumberOfTransitions());
192 auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
195 auto result = checker.check(this->env(), tasks[0])->template asExplicitQuantitativeCheckResult<ValueType>();
196 EXPECT_NEAR(this->
parseNumber(
"1/6"), result[*mdp->getInitialStates().begin()], this->precision());
197 result = checker.check(this->env(), tasks[1])->template asExplicitQuantitativeCheckResult<ValueType>();
198 EXPECT_NEAR(this->
parseNumber(
"1/6"), result[*mdp->getInitialStates().begin()], this->precision());
199 result = checker.check(this->env(), tasks[2])->template asExplicitQuantitativeCheckResult<ValueType>();
200 EXPECT_NEAR(this->
parseNumber(
"1/6"), result[*mdp->getInitialStates().begin()], this->precision());
201 result = checker.check(this->env(), tasks[3])->template asExplicitQuantitativeCheckResult<ValueType>();
202 EXPECT_NEAR(this->
parseNumber(
"1/6"), result[*mdp->getInitialStates().begin()], this->precision());
203 result = checker.check(this->env(), tasks[4])->template asExplicitQuantitativeCheckResult<ValueType>();
204 EXPECT_NEAR(this->
parseNumber(
"0"), result[*mdp->getInitialStates().begin()], this->precision());
205 result = checker.check(this->env(), tasks[5])->template asExplicitQuantitativeCheckResult<ValueType>();
206 EXPECT_NEAR(this->
parseNumber(
"0"), result[*mdp->getInitialStates().begin()], this->precision());
207 result = checker.check(this->env(), tasks[6])->template asExplicitQuantitativeCheckResult<ValueType>();
208 EXPECT_NEAR(this->
parseNumber(
"1"), result[*mdp->getInitialStates().begin()], this->precision());
209 result = checker.check(this->env(), tasks[7])->template asExplicitQuantitativeCheckResult<ValueType>();
210 EXPECT_NEAR(this->
parseNumber(
"1"), result[*mdp->getInitialStates().begin()], this->precision());
213TYPED_TEST(ConditionalMdpPrctlModelCheckerTest, consensus) {
214 typedef typename TestFixture::ValueType
ValueType;
216 std::string
const formulasString =
217 "Pmax=? [F \"all_coins_equal_0\" & \"finished\" || F \"agree\" & \"finished\"];"
218 "Pmin=? [F \"all_coins_equal_0\" & \"finished\" || F \"agree\" & \"finished\"];"
219 "Pmax=? [F \"all_coins_equal_1\" & \"finished\" || F \"agree\" & \"finished\"];"
220 "Pmin=? [F \"all_coins_equal_1\" & \"finished\" || F \"agree\" & \"finished\"];";
223 auto modelFormulas = this->buildModelFormulas(program, formulasString);
224 auto model = std::move(modelFormulas.first);
225 auto tasks = this->getTasks(modelFormulas.second);
226 EXPECT_EQ(272ul, model->getNumberOfStates());
227 EXPECT_EQ(492ul, model->getNumberOfTransitions());
229 auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
232 auto result = checker.check(this->env(), tasks[0])->template asExplicitQuantitativeCheckResult<ValueType>();
233 EXPECT_NEAR(this->
parseNumber(
"561/953"), result[*mdp->getInitialStates().begin()], this->precision());
234 result = checker.check(this->env(), tasks[1])->template asExplicitQuantitativeCheckResult<ValueType>();
235 EXPECT_NEAR(this->
parseNumber(
"392/953"), result[*mdp->getInitialStates().begin()], this->precision());
236 result = checker.check(this->env(), tasks[2])->template asExplicitQuantitativeCheckResult<ValueType>();
237 EXPECT_NEAR(this->
parseNumber(
"561/953"), result[*mdp->getInitialStates().begin()], this->precision());
238 result = checker.check(this->env(), tasks[3])->template asExplicitQuantitativeCheckResult<ValueType>();
239 EXPECT_NEAR(this->
parseNumber(
"392/953"), result[*mdp->getInitialStates().begin()], this->precision());
242TYPED_TEST(ConditionalMdpPrctlModelCheckerTest, simple) {
243 typedef typename TestFixture::ValueType
ValueType;
245 std::string
const programAsString = R
"(mdp
248 [] x=0 -> 0.7 : (x'=1) + 0.3 : (x'=2);
249 [] x=1 -> 1 : (x'=1);
250 [] x=2 -> 1 : (x'=1);
254 std::string const formulasString =
255 "Pmin=? [F x=2 || F x=1];"
256 "Pmax=? [F x=2 || F x=1];";
259 auto modelFormulas = this->buildModelFormulas(program, formulasString);
260 auto model = std::move(modelFormulas.first);
261 auto tasks = this->getTasks(modelFormulas.second);
262 EXPECT_EQ(3ul, model->getNumberOfStates());
263 EXPECT_EQ(4ul, model->getNumberOfTransitions());
265 auto mdp = model->template as<storm::models::sparse::Mdp<ValueType>>();
268 auto result = checker.check(this->env(), tasks[0])->template asExplicitQuantitativeCheckResult<ValueType>();
269 EXPECT_NEAR(this->
parseNumber(
"3/10"), result[*mdp->getInitialStates().begin()], this->precision());
270 result = checker.check(this->env(), tasks[1])->template asExplicitQuantitativeCheckResult<ValueType>();
271 EXPECT_NEAR(this->
parseNumber(
"3/10"), result[*mdp->getInitialStates().begin()], this->precision());
SolverEnvironment & solver()
ModelCheckerEnvironment & modelchecker()
void setPrecision(storm::RationalNumber value)
void setConditionalAlgorithmSetting(ConditionalAlgorithmSetting value)
MinMaxSolverEnvironment & minMax()
This class represents a (discrete-time) Markov decision process.
static storm::prism::Program parseFromString(std::string const &input, std::string const &filename, bool prismCompatability=false)
Parses the given input stream into the PRISM storage classes assuming it complies with the PRISM synt...
static storm::prism::Program parse(std::string const &filename, bool prismCompatability=false)
Parses the given file into the PRISM storage classes assuming it complies with the PRISM syntax.
std::vector< storm::jani::Property > parsePropertiesForPrismProgram(std::string const &inputString, storm::prism::Program const &program, boost::optional< std::set< std::string > > const &propertyFilter)
std::vector< std::shared_ptr< storm::logic::Formula const > > extractFormulasFromProperties(std::vector< storm::jani::Property > const &properties)
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)
TYPED_TEST(GraphTestAR, SymbolicProb01StochasticGameDieSmall)
TYPED_TEST_SUITE(GraphTestAR, TestingTypes,)
::testing::Types< Cudd, Sylvan > TestingTypes