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

reincluded tbb in gmm. fixed missing header. extended formula parser to return multiple formulas 

Former-commit-id: a2849d6534
main
dehnert 10 years ago
parent
63df1f6329
commit
f9f5a4e206
24 changed files with 479 additions and 378 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. 87
      resources/3rdparty/gmm-5.0/include/gmm/gmm_blas.h
  2. 8
      src/models/sparse/Dtmc.cpp
  3. 36
      src/parser/FormulaParser.cpp
  4. 24
      src/parser/FormulaParser.h
  5. 32
      src/utility/ConstantsComparator.h
  6. 4
      src/utility/cli.cpp
  7. 8
      src/utility/constants.cpp
  8. 46
      test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
  9. 38
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  10. 46
      test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
  11. 26
      test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
  12. 32
      test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
  13. 40
      test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
  14. 38
      test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
  15. 38
      test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
  16. 38
      test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
  17. 26
      test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
  18. 32
      test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
  19. 80
      test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
  20. 28
      test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
  21. 26
      test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
  22. 32
      test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
  23. 40
      test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
  24. 52
      test/functional/parser/FormulaParserTest.cpp

87
resources/3rdparty/gmm-5.0/include/gmm/gmm_blas.h
View File

@ -38,6 +38,16 @@
#ifndef GMM_BLAS_H__
#define GMM_BLAS_H__
// This Version of GMM was modified for StoRM.
// To detect whether the usage of TBB is possible, this include is neccessary
#include "storm-config.h"
#ifdef STORM_HAVE_INTELTBB
# include <new> // This fixes a potential dependency ordering problem between GMM and TBB
# include "tbb/tbb.h"
# include <iterator>
#endif
#include "gmm_scaled.h"
#include "gmm_transposed.h"
#include "gmm_conjugated.h"
@ -1680,16 +1690,85 @@ namespace gmm {
if (aux != T(0)) l3[i] = aux;
}
}
#ifdef STORM_HAVE_INTELTBB
/* Official Intel Hint on blocked_range vs. linear iterators: http://software.intel.com/en-us/forums/topic/289505
*/
template <typename IT1, typename IT2>
class forward_range_mult {
IT1 my_begin;
IT1 my_end;
IT2 my_begin_row;
size_t my_size;
public:
IT1 begin() const {return my_begin;}
IT2 begin_row() const {return my_begin_row;}
IT1 end() const {return my_end;}
bool empty() const {return my_begin==my_end;}
bool is_divisible() const {return my_size>1;}
forward_range_mult( IT1 first, IT1 last, IT2 row_first, size_t size ) : my_begin(first), my_end(last), my_begin_row(row_first), my_size(size) {
assert( size==size_t(std::distance( first,last )));
}
forward_range_mult( IT1 first, IT1 last, IT2 row_first) : my_begin(first), my_end(last), my_begin_row(row_first) {
my_size = std::distance( first,last );
}
forward_range_mult( forward_range_mult& r, tbb::split ) {
size_t h = r.my_size/2;
my_end = r.my_end;
my_begin = r.my_begin;
my_begin_row = r.my_begin_row;
std::advance( my_begin, h ); // Might be scaling issue
std::advance( my_begin_row, h );
my_size = r.my_size-h;
r.my_end = my_begin;
r.my_size = h;
}
};
template <typename L1, typename L2, typename L3>
class tbbHelper_mult_by_row {
L2 const* my_l2;
// Typedefs for Iterator Types
typedef typename linalg_traits<L3>::iterator frm_IT1;
typedef typename linalg_traits<L1>::const_row_iterator frm_IT2;
public:
void operator()( const forward_range_mult<frm_IT1, frm_IT2>& r ) const {
L2 const& l2 = *my_l2;
frm_IT1 it = r.begin();
frm_IT1 ite = r.end();
frm_IT2 itr = r.begin_row();
for (; it != ite; ++it, ++itr) {
*it = vect_sp(linalg_traits<L1>::row(itr), l2,
typename linalg_traits<L1>::storage_type(),
typename linalg_traits<L2>::storage_type());
}
}
tbbHelper_mult_by_row(L2 const* l2) :
my_l2(l2)
{}
};
#endif
template <typename L1, typename L2, typename L3>
void mult_by_row(const L1& l1, const L2& l2, L3& l3, abstract_dense) {
typename linalg_traits<L3>::iterator it=vect_begin(l3), ite=vect_end(l3);
typename linalg_traits<L1>::const_row_iterator
itr = mat_row_const_begin(l1);
for (; it != ite; ++it, ++itr)
*it = vect_sp(linalg_traits<L1>::row(itr), l2,
typename linalg_traits<L1>::storage_type(),
typename linalg_traits<L2>::storage_type());
#ifdef STORM_HAVE_INTELTBB
tbb::parallel_for(forward_range_mult<typename linalg_traits<L3>::iterator, typename linalg_traits<L1>::const_row_iterator>(it, ite, itr), tbbHelper_mult_by_row<L1, L2, L3>(&l2));
#else
for (; it != ite; ++it, ++itr)
*it = vect_sp(linalg_traits<L1>::row(itr), l2,
typename linalg_traits<L1>::storage_type(),
typename linalg_traits<L2>::storage_type());
#endif
}
template <typename L1, typename L2, typename L3>

8
src/models/sparse/Dtmc.cpp
View File

@ -3,6 +3,7 @@
#include "src/adapters/CarlAdapter.h"
#include "src/exceptions/NotImplementedException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/utility/constants.h"
namespace storm {
namespace models {
@ -196,19 +197,18 @@ namespace storm {
template <typename ValueType, typename RewardModelType>
void Dtmc<ValueType, RewardModelType>::ConstraintCollector::process(storm::models::sparse::Dtmc<ValueType> const& dtmc) {
storm::utility::ConstantsComparator<ValueType> comparator;
for(uint_fast64_t state = 0; state < dtmc.getNumberOfStates(); ++state) {
ValueType sum = storm::utility::zero<ValueType>();
for (auto const& transition : dtmc.getRows(state)) {
sum += transition.getValue();
if (!comparator.isConstant(transition.getValue())) {
if (!storm::utility::isConstant(transition.getValue())) {
wellformedConstraintSet.emplace(transition.getValue() - 1, storm::CompareRelation::LEQ);
wellformedConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GEQ);
graphPreservingConstraintSet.emplace(transition.getValue(), storm::CompareRelation::GREATER);
}
}
STORM_LOG_ASSERT(!comparator.isConstant(sum) || comparator.isOne(sum), "If the sum is a constant, it must be equal to 1.");
if(!comparator.isConstant(sum)) {
STORM_LOG_ASSERT(!storm::utility::isConstant(sum) || storm::utility::isOne(sum), "If the sum is a constant, it must be equal to 1.");
if(!storm::utility::isConstant(sum)) {
wellformedConstraintSet.emplace(sum - 1, storm::CompareRelation::EQ);
}

36
src/parser/FormulaParser.cpp
View File

@ -1,5 +1,7 @@
#include "src/parser/FormulaParser.h"
#include <fstream>
// If the parser fails due to ill-formed data, this exception is thrown.
#include "src/exceptions/WrongFormatException.h"
@ -98,7 +100,7 @@ namespace storm {
stateFormula = (orStateFormula);
stateFormula.name("state formula");
start = qi::eps > stateFormula >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
start.name("start");
/*!
@ -156,13 +158,41 @@ namespace storm {
this->identifiers_.add(identifier, expression);
}
std::shared_ptr<storm::logic::Formula> FormulaParser::parseFromString(std::string const& formulaString) {
std::shared_ptr<storm::logic::Formula> FormulaParser::parseSingleFormulaFromString(std::string const& formulaString) {
std::vector<std::shared_ptr<storm::logic::Formula>> formulas = parseFromString(formulaString);
STORM_LOG_THROW(formulas.size() == 1, storm::exceptions::WrongFormatException, "Expected exactly one formula, but found " << formulas.size() << " instead.");
return formulas.front();
}
std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromFile(std::string const& filename) {
// Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in);
STORM_LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
std::vector<std::shared_ptr<storm::logic::Formula>> formulas;
// Now try to parse the contents of the file.
try {
std::string fileContent((std::istreambuf_iterator<char>(inputFileStream)), (std::istreambuf_iterator<char>()));
formulas = parseFromString(fileContent);
} catch(std::exception& e) {
// In case of an exception properly close the file before passing exception.
inputFileStream.close();
throw e;
}
// Close the stream in case everything went smoothly and return result.
inputFileStream.close();
return formulas;
}
std::vector<std::shared_ptr<storm::logic::Formula>> FormulaParser::parseFromString(std::string const& formulaString) {
PositionIteratorType first(formulaString.begin());
PositionIteratorType iter = first;
PositionIteratorType last(formulaString.end());
// Create empty result;
std::shared_ptr<storm::logic::Formula> result;
std::vector<std::shared_ptr<storm::logic::Formula>> result;
// Create grammar.
try {

24
src/parser/FormulaParser.h
View File

@ -12,7 +12,7 @@
namespace storm {
namespace parser {
class FormulaParser : public qi::grammar<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> {
class FormulaParser : public qi::grammar<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> {
public:
FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager = std::shared_ptr<storm::expressions::ExpressionManager>(new storm::expressions::ExpressionManager()));
@ -20,9 +20,25 @@ namespace storm {
* Parses the formula given by the provided string.
*
* @param formulaString The formula as a string.
* @return The resulting formula representation.
* @return The resulting formula.
*/
std::shared_ptr<storm::logic::Formula> parseFromString(std::string const& formulaString);
std::shared_ptr<storm::logic::Formula> parseSingleFormulaFromString(std::string const& formulaString);
/*!
* Parses the formula given by the provided string.
*
* @param formulaString The formula as a string.
* @return The contained formulas.
*/
std::vector<std::shared_ptr<storm::logic::Formula>> parseFromString(std::string const& formulaString);
/*!
* Parses the formulas in the given file.
*
* @param filename The name of the file to parse.
* @return The contained formulas.
*/
std::vector<std::shared_ptr<storm::logic::Formula>> parseFromFile(std::string const& filename);
/*!
* Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used
@ -118,7 +134,7 @@ namespace storm {
// they are to be replaced with.
qi::symbols<char, storm::expressions::Expression> identifiers_;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> start;
qi::rule<Iterator, std::vector<std::shared_ptr<storm::logic::Formula>>(), Skipper> start;
qi::rule<Iterator, std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>(), qi::locals<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> probabilityOperator;

32
src/utility/ConstantsComparator.h
View File

@ -68,38 +68,6 @@ namespace storm {
// The precision used for comparisons.
double precision;
};
#ifdef STORM_HAVE_CARL
template<>
class ConstantsComparator<storm::RationalFunction> {
public:
ConstantsComparator();
bool isOne(storm::RationalFunction const& value) const;
bool isZero(storm::RationalFunction const& value) const;
bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const;
bool isConstant(storm::RationalFunction const& value) const;
};
template<>
class ConstantsComparator<storm::Polynomial> {
public:
ConstantsComparator();
bool isOne(storm::Polynomial const& value) const;
bool isZero(storm::Polynomial const& value) const;
bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const;
bool isConstant(storm::Polynomial const& value) const;
};
#endif
}
}

4
src/utility/cli.cpp
View File

@ -223,10 +223,10 @@ namespace storm {
std::shared_ptr<storm::logic::Formula> formula;
if (program) {
storm::parser::FormulaParser formulaParser(program.get().getManager().getSharedPointer());
formula = formulaParser.parseFromString(settings.getProperty());
formula = formulaParser.parseSingleFormulaFromString(settings.getProperty());
} else {
storm::parser::FormulaParser formulaParser;
formula = formulaParser.parseFromString(settings.getProperty());
formula = formulaParser.parseSingleFormulaFromString(settings.getProperty());
}
formulas.push_back(formula);
} else if (settings.isPropertyFileSet()) {

8
src/utility/constants.cpp
View File

@ -203,6 +203,10 @@ namespace storm {
template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
#ifdef STORM_HAVE_CARL
template bool isOne(RationalFunction const& value);
template bool isZero(RationalFunction const& value);
template bool isConstant(RationalFunction const& value);
template RationalFunction one();
template RationalFunction zero();
template storm::RationalFunction infinity();
@ -215,6 +219,10 @@ namespace storm {
template RationalFunction& simplify(RationalFunction& value);
template RationalFunction&& simplify(RationalFunction&& value);
template bool isOne(Interval const& value);
template bool isZero(Interval const& value);
template bool isConstant(Interval const& value);
template Interval one();
template Interval zero();

46
test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp
View File

@ -43,56 +43,56 @@ TEST(GmmxxCtmcCslModelCheckerTest, Cluster) {
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F[100,2000] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=100]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult7 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("LRA=? [\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
@ -126,42 +126,42 @@ TEST(GmmxxCtmcCslModelCheckerTest, Embedded) {
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10000]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("LRA=? [\"fail_sensors\"]");
formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"fail_sensors\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
@ -188,14 +188,14 @@ TEST(GmmxxCtmcCslModelCheckerTest, Polling) {
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]");
formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("LRA=?[\"target\"]");
formula = formulaParser.parseSingleFormulaFromString("LRA=?[\"target\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
@ -235,49 +235,49 @@ TEST(GmmxxCtmcCslModelCheckerTest, Tandem) {
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [I=10]");
formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(262.85103661561755, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("LRA=? [\"first_queue_full\"]");
formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"first_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());

38
test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
View File

@ -18,7 +18,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
@ -29,28 +29,28 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"one\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
@ -64,7 +64,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
@ -73,21 +73,21 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"observe0Greater1\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeIGreater1\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
@ -101,7 +101,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
@ -110,21 +110,21 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F<=20 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
@ -137,7 +137,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(2, 2, 2);
@ -153,7 +153,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRA=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -177,7 +177,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRA=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -201,7 +201,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRA=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -217,7 +217,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
std::shared_ptr<storm::models::sparse::Dtmc<double>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(15, 15, 20, true);
@ -264,7 +264,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRA=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();

46
test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp
View File

@ -45,7 +45,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -54,7 +54,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -63,7 +63,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F[100,2000] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -72,7 +72,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -81,7 +81,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -90,7 +90,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -99,7 +99,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=100]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -108,7 +108,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.8602815057967503, quantitativeCheckResult7.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("LRA=? [\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"minimum\"]");
checkResult = modelchecker.check(*formula);
checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
@ -142,7 +142,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -151,7 +151,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -160,7 +160,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -169,7 +169,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -178,7 +178,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10000]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -187,7 +187,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Embedded) {
EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(2.7745274082080154, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("LRA=? [\"fail_sensors\"]");
formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"fail_sensors\"]");
checkResult = modelchecker.check(*formula);
checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
@ -214,7 +214,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) {
storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]");
formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -223,7 +223,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Polling) {
EXPECT_NEAR(1, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(1, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("LRA=? [\"target\"]");
formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"target\"]");
checkResult = modelchecker.check(*formula);
checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));
@ -265,7 +265,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -274,7 +274,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -283,7 +283,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -292,7 +292,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [I=10]");
formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -301,7 +301,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -310,7 +310,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -319,7 +319,7 @@ TEST(GmmxxHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(262.85103498583413, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("LRA=? [\"first_queue_full\"]");
formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"first_queue_full\"]");
checkResult = modelchecker.check(*formula);
checkResult->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(ctmc->getReachableStates(), ctmc->getInitialStates()));

26
test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp
View File

@ -22,7 +22,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -42,7 +42,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) {
storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"one\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -51,7 +51,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) {
EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -60,7 +60,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) {
EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -69,7 +69,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) {
EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -83,7 +83,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
@ -95,7 +95,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) {
storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"observe0Greater1\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -104,7 +104,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) {
EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeIGreater1\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -113,7 +113,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) {
EXPECT_NEAR(0.1522194965, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.1522194965, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -127,7 +127,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -147,7 +147,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -156,7 +156,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F<=20 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -165,7 +165,7 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));

32
test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp
View File

@ -23,7 +23,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -43,7 +43,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -52,7 +52,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -61,7 +61,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -70,7 +70,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -79,7 +79,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -88,7 +88,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -97,7 +97,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -106,7 +106,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -120,7 +120,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -140,7 +140,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -149,7 +149,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -158,7 +158,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -167,7 +167,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -176,7 +176,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -185,7 +185,7 @@ TEST(GmmxxHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));

40
test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp
View File

@ -19,7 +19,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
@ -30,56 +30,56 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
@ -94,14 +94,14 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
@ -116,14 +116,14 @@ TEST(GmmxxMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
@ -135,7 +135,7 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType());
@ -146,42 +146,42 @@ TEST(GmmxxMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();

38
test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp
View File

@ -41,49 +41,49 @@ TEST(NativeCtmcCslModelCheckerTest, Cluster) {
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F[100,2000] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult6 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=100]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
@ -117,35 +117,35 @@ TEST(NativeCtmcCslModelCheckerTest, Embedded) {
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10000]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
@ -172,7 +172,7 @@ TEST(NativeCtmcCslModelCheckerTest, Polling) {
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]");
formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
@ -213,42 +213,42 @@ TEST(NativeCtmcCslModelCheckerTest, Tandem) {
storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult1 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult2 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult3 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeCheckResult3[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [I=10]");
formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult4 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());
storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeCheckResult5 = checkResult->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5[initialState], storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isExplicitQuantitativeCheckResult());

38
test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
View File

@ -20,7 +20,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Die) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
@ -31,28 +31,28 @@ TEST(SparseDtmcPrctlModelCheckerTest, Die) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"one\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
@ -66,7 +66,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
@ -75,21 +75,21 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"observe0Greater1\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.33288205191646525, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeIGreater1\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.15222066094730619, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
@ -103,7 +103,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
@ -112,21 +112,21 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F<=20 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
@ -139,7 +139,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(2, 2, 2);
@ -155,7 +155,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRA=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -179,7 +179,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRA=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -203,7 +203,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRA=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -219,7 +219,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) {
std::shared_ptr<storm::models::sparse::Dtmc<double>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(15, 15, 20, true);
@ -266,7 +266,7 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) {
storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>(storm::solver::NativeLinearEquationSolver<double>::SolutionMethod::SOR, 0.9)));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRA=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();

38
test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp
View File

@ -44,7 +44,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=100 !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=100 !\"minimum\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -53,7 +53,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(5.5461254704419085E-5, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F[100,100] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,100] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -62,7 +62,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(2.3397873548343415E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F[100,2000] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F[100,2000] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -71,7 +71,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.001105335651670241, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U<=10 \"premium\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -80,7 +80,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(1, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(1, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"minimum\" U[1,inf] \"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -89,7 +89,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(0, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ \"minimum\" U[1,inf] !\"minimum\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -98,7 +98,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) {
EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.9999999033633374, quantitativeCheckResult6.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=100]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=100]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -133,7 +133,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) {
storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10000 \"down\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10000 \"down\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -142,7 +142,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) {
EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.0019216435246119591, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_actuators\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -151,7 +151,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) {
EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(3.7079151806696567E-6, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_io\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -160,7 +160,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) {
EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.001556839327673734, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ !\"down\" U<=10000 \"fail_sensors\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -169,7 +169,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Embedded) {
EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(4.429620626755424E-5, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10000]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10000]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -197,7 +197,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Polling) {
storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=?[ F<=10 \"target\"]");
formula = formulaParser.parseSingleFormulaFromString("P=?[ F<=10 \"target\"]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -239,7 +239,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) {
storm::modelchecker::HybridCtmcCslModelChecker<storm::dd::DdType::CUDD, double> modelchecker(*ctmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
// Start checking properties.
formula = formulaParser.parseFromString("P=? [ F<=10 \"network_full\" ]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"network_full\" ]");
std::unique_ptr<storm::modelchecker::CheckResult> checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -248,7 +248,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.015446370562428037, quantitativeCheckResult1.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [ F<=10 \"first_queue_full\" ]");
formula = formulaParser.parseSingleFormulaFromString("P=? [ F<=10 \"first_queue_full\" ]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -257,7 +257,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(0.999999837225515, quantitativeCheckResult2.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [\"second_queue_full\" U<=1 !\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -266,7 +266,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(1, quantitativeCheckResult3.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(1, quantitativeCheckResult3.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [I=10]");
formula = formulaParser.parseSingleFormulaFromString("R=? [I=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -275,7 +275,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(5.679243850315877, quantitativeCheckResult4.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [C<=10]");
formula = formulaParser.parseSingleFormulaFromString("R=? [C<=10]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());
@ -284,7 +284,7 @@ TEST(NativeHybridCtmcCslModelCheckerTest, Tandem) {
EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMin(), storm::settings::generalSettings().getPrecision());
EXPECT_NEAR(55.44792186036232, quantitativeCheckResult5.getMax(), storm::settings::generalSettings().getPrecision());
formula = formulaParser.parseFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"first_queue_full\"&\"second_queue_full\"]");
checkResult = modelchecker.check(*formula);
ASSERT_TRUE(checkResult->isHybridQuantitativeCheckResult());

26
test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp
View File

@ -23,7 +23,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -43,7 +43,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) {
storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"one\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -52,7 +52,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) {
EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -61,7 +61,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) {
EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -70,7 +70,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) {
EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -84,7 +84,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
@ -96,7 +96,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) {
storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"observe0Greater1\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -105,7 +105,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) {
EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeIGreater1\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -114,7 +114,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) {
EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -128,7 +128,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -148,7 +148,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::modelchecker::HybridDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -157,7 +157,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F<=20 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -166,7 +166,7 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) {
EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));

32
test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp
View File

@ -22,7 +22,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -42,7 +42,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -51,7 +51,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -60,7 +60,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -69,7 +69,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -78,7 +78,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -87,7 +87,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -96,7 +96,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -105,7 +105,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(7.3333294987678528, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -119,7 +119,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -139,7 +139,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::modelchecker::HybridMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -148,7 +148,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -157,7 +157,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -166,7 +166,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -175,7 +175,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -184,7 +184,7 @@ TEST(NativeHybridMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(4.2856896106114934, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));

80
test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
View File

@ -18,7 +18,7 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Mdp);
@ -29,56 +29,56 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult7 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult7[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult8 = result->asExplicitQuantitativeCheckResult<double>();
@ -93,14 +93,14 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult9 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(7.333329499, quantitativeResult9[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult10 = result->asExplicitQuantitativeCheckResult<double>();
@ -115,14 +115,14 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult11 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(14.666658998, quantitativeResult11[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult12 = result->asExplicitQuantitativeCheckResult<double>();
@ -134,7 +134,7 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(storm::models::ModelType::Mdp, abstractModel->getType());
@ -145,42 +145,42 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.0625, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(4.285689611, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
@ -193,7 +193,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(2, 2, 2);
@ -209,7 +209,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRAmax=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -217,7 +217,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmin=? [\"a\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
@ -241,7 +241,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRAmax=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -249,7 +249,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmin=? [\"a\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
@ -282,7 +282,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRAmax=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -291,7 +291,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult1[2], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmin=? [\"a\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
@ -300,7 +300,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
EXPECT_NEAR(0.0, quantitativeResult2[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult2[2], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmax=? [\"b\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
@ -309,7 +309,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
EXPECT_NEAR(0.5, quantitativeResult3[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.5, quantitativeResult3[2], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmin=? [\"b\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
@ -318,7 +318,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
EXPECT_NEAR(1. / 3., quantitativeResult4[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1. / 3., quantitativeResult4[2], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmax=? [\"c\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
@ -327,7 +327,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
EXPECT_NEAR(2. / 3., quantitativeResult5[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(2. / 3., quantitativeResult5[2], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmin=? [\"c\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
@ -343,7 +343,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp;
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
{
matrixBuilder = storm::storage::SparseMatrixBuilder<double>(4, 3, 4, true, true, 3);
@ -368,7 +368,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRAmax=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -377,7 +377,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
EXPECT_NEAR(0.0, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult1[2], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmin=? [\"a\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
@ -386,7 +386,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
EXPECT_NEAR(0.0, quantitativeResult2[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult2[2], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmax=? [\"b\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
@ -395,7 +395,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
EXPECT_NEAR(1.0, quantitativeResult3[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult3[2], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmin=? [\"b\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
@ -404,7 +404,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
EXPECT_NEAR(0.0, quantitativeResult4[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0, quantitativeResult4[2], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmax=? [\"c\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
@ -413,7 +413,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
EXPECT_NEAR(1.0, quantitativeResult5[1], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult5[2], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmin=? [\"c\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
@ -490,7 +490,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> checker(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::NativeMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("LRAmax=? [\"a\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
@ -503,7 +503,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
EXPECT_NEAR(101./200., quantitativeResult1[13], storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(31./60., quantitativeResult1[14], storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("LRAmin=? [\"a\"]");
formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
result = std::move(checker.check(*formula));
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();

28
test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp
View File

@ -16,7 +16,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
@ -27,28 +27,28 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) {
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"one\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::generalSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::generalSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::generalSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
@ -60,7 +60,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
@ -71,35 +71,35 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) {
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"observe0Greater1\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::generalSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeIGreater1\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::generalSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::generalSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observe0Greater1\" || F \"observeIGreater1\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\" || F \"observeIGreater1\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(0.15330064292476167, quantitativeResult4[0], storm::settings::generalSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\" || F \"observe0Greater1\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\" || F \"observe0Greater1\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
@ -111,7 +111,7 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) {
std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc);
std::shared_ptr<storm::models::sparse::Dtmc<double>> dtmc = abstractModel->as<storm::models::sparse::Dtmc<double>>();
@ -121,14 +121,14 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) {
storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc);
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::generalSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();

26
test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp
View File

@ -21,7 +21,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -41,7 +41,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"one\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -50,7 +50,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {
EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -59,7 +59,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {
EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -68,7 +68,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) {
EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -82,7 +82,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::shared_ptr<storm::models::symbolic::Model<storm::dd::DdType::CUDD>> model = storm::builder::DdPrismModelBuilder<storm::dd::DdType::CUDD>::translateProgram(program);
EXPECT_EQ(8607ul, model->getNumberOfStates());
@ -94,7 +94,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) {
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"observe0Greater1\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -103,7 +103,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) {
EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeIGreater1\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -112,7 +112,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) {
EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -126,7 +126,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -146,7 +146,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) {
storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*dtmc, std::unique_ptr<storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("P=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -155,7 +155,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) {
EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("P=? [F<=20 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -164,7 +164,7 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) {
EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("R=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));

32
test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp
View File

@ -21,7 +21,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -41,7 +41,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -50,7 +50,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -59,7 +59,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0277777612209320068, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -68,7 +68,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -77,7 +77,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0555555224418640136, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -86,7 +86,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -95,7 +95,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.083333283662796020508, quantitativeResult6.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -104,7 +104,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, Dice) {
EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(7.3333272933959961, quantitativeResult7.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -118,7 +118,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
// Build the die model with its reward model.
#ifdef WINDOWS
@ -138,7 +138,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::dd::DdType::CUDD, double> checker(*mdp, std::unique_ptr<storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>>(new storm::utility::solver::SymbolicMinMaxLinearEquationSolverFactory<storm::dd::DdType::CUDD, double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -147,7 +147,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(1, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -156,7 +156,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(1, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(1, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -165,7 +165,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(0.0625, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -174,7 +174,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(0.0625, quantitativeResult4.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(0.0625, quantitativeResult4.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));
@ -183,7 +183,7 @@ TEST(SymbolicMdpPrctlModelCheckerTest, AsynchronousLeader) {
EXPECT_NEAR(4.2856890848060498, quantitativeResult5.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision());
EXPECT_NEAR(4.2856890848060498, quantitativeResult5.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = checker.check(*formula);
result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>(model->getReachableStates(), model->getInitialStates()));

40
test/functional/modelchecker/TopologicalValueIterationMdpPrctlModelCheckerTest.cpp
View File

@ -21,50 +21,50 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.tra", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew")->as<storm::models::sparse::Mdp<double>>();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(mdp->getNumberOfStates(), 169ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 436ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"two\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*formula);
ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"two\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
result = mc.check(*formula);
ASSERT_NEAR(0.0277777612209320068, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
result = mc.check(*formula);
ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"three\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
result = mc.check(*formula);
ASSERT_NEAR(0.0555555224418640136, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
result = mc.check(*formula);
ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"four\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
result = mc.check(*formula);
ASSERT_NEAR(0.083333283662796020508, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = mc.check(*formula);
@ -74,7 +74,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = mc.check(*formula);
@ -89,7 +89,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateRewardModelChecker(*stateRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = stateRewardModelChecker.check(*formula);
@ -99,7 +99,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
ASSERT_NEAR(7.33332904, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateRewardModelChecker.check(*formula);
@ -114,7 +114,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
formula = parser.parseFromString("Rmin=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*formula);
@ -123,7 +123,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, Dice) {
#else
ASSERT_NEAR(14.6666581, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
formula = parser.parseFromString("Rmax=? [F \"done\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"done\"]");
result = stateAndTransitionRewardModelChecker.check(*formula);
@ -138,39 +138,39 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::sparse::Mdp<double>> mdp = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.tra", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.lab", "", STORM_CPP_BASE_PATH "/examples/mdp/asynchronous_leader/leader4.trans.rew")->as<storm::models::sparse::Mdp<double>>();
// A parser that we use for conveniently constructing the formulas.
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>> mc(*mdp, std::unique_ptr<storm::utility::solver::MinMaxLinearEquationSolverFactory<double>>(new storm::utility::solver::TopologicalMinMaxLinearEquationSolverFactory<double>()));
std::shared_ptr<storm::logic::Formula> formula = parser.parseFromString("Pmin=? [F \"elected\"]");
std::shared_ptr<storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
std::unique_ptr<storm::modelchecker::CheckResult> result = mc.check(*formula);
ASSERT_LT(std::abs(result->asExplicitQuantitativeCheckResult<double>()[0] - 1),
storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
result = mc.check(*formula);
ASSERT_NEAR(1, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmax=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F<=25 \"elected\"]");
result = mc.check(*formula);
ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Pmin=? [F<=25 \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F<=25 \"elected\"]");
result = mc.check(*formula);
ASSERT_NEAR(0.0625, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
formula = parser.parseFromString("Rmin=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmin=? [F \"elected\"]");
result = mc.check(*formula);
@ -180,7 +180,7 @@ TEST(TopologicalValueIterationMdpPrctlModelCheckerTest, AsynchronousLeader) {
ASSERT_NEAR(4.285701547, result->asExplicitQuantitativeCheckResult<double>()[0], storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision());
#endif
formula = parser.parseFromString("Rmax=? [F \"elected\"]");
formula = formulaParser.parseSingleFormulaFromString("Rmax=? [F \"elected\"]");
result = mc.check(*formula);

52
test/functional/parser/FormulaParserTest.cpp
View File

@ -4,21 +4,21 @@
#include "src/exceptions/WrongFormatException.h"
TEST(FormulaParserTest, LabelTest) {
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::string input = "\"label\"";
std::shared_ptr<storm::logic::Formula> formula(nullptr);
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isAtomicLabelFormula());
}
TEST(FormulaParserTest, ComplexLabelTest) {
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::string input = "!(\"a\" & \"b\") | \"a\" & !\"c\"";
std::shared_ptr<storm::logic::Formula> formula(nullptr);
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isPropositionalFormula());
EXPECT_TRUE(formula->isBinaryBooleanStateFormula());
@ -29,11 +29,11 @@ TEST(FormulaParserTest, ExpressionTest) {
manager->declareBooleanVariable("x");
manager->declareIntegerVariable("y");
storm::parser::FormulaParser parser(manager);
storm::parser::FormulaParser formulaParser(manager);
std::string input = "!(x | y > 3)";
std::shared_ptr<storm::logic::Formula> formula(nullptr);
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isPropositionalFormula());
EXPECT_TRUE(formula->isUnaryBooleanStateFormula());
@ -44,25 +44,25 @@ TEST(FormulaParserTest, LabelAndExpressionTest) {
manager->declareBooleanVariable("x");
manager->declareIntegerVariable("y");
storm::parser::FormulaParser parser(manager);
storm::parser::FormulaParser formulaParser(manager);
std::string input = "!\"a\" | x | y > 3";
std::shared_ptr<storm::logic::Formula> formula(nullptr);
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isPropositionalFormula());
input = "x | y > 3 | !\"a\"";
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isPropositionalFormula());
}
TEST(FormulaParserTest, ProbabilityOperatorTest) {
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::string input = "P<0.9 [\"a\" U \"b\"]";
std::shared_ptr<storm::logic::Formula> formula(nullptr);
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isProbabilityOperatorFormula());
EXPECT_TRUE(formula->asProbabilityOperatorFormula().hasBound());
@ -70,18 +70,18 @@ TEST(FormulaParserTest, ProbabilityOperatorTest) {
}
TEST(FormulaParserTest, RewardOperatorTest) {
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::string input = "Rmin<0.9 [F \"a\"]";
std::shared_ptr<storm::logic::Formula> formula(nullptr);
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isRewardOperatorFormula());
EXPECT_TRUE(formula->asRewardOperatorFormula().hasBound());
EXPECT_TRUE(formula->asRewardOperatorFormula().hasOptimalityType());
input = "R=? [I=10]";
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isRewardOperatorFormula());
EXPECT_FALSE(formula->asRewardOperatorFormula().hasBound());
@ -90,11 +90,11 @@ TEST(FormulaParserTest, RewardOperatorTest) {
}
TEST(FormulaParserTest, ConditionalProbabilityTest) {
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::string input = "P<0.9 [F \"a\" || F \"b\"]";
std::shared_ptr<storm::logic::Formula> formula(nullptr);
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isProbabilityOperatorFormula());
storm::logic::ProbabilityOperatorFormula const& probFormula = formula->asProbabilityOperatorFormula();
@ -102,11 +102,11 @@ TEST(FormulaParserTest, ConditionalProbabilityTest) {
}
TEST(FormulaParserTest, NestedPathFormulaTest) {
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::string input = "P<0.9 [F X \"a\"]";
std::shared_ptr<storm::logic::Formula> formula(nullptr);
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isProbabilityOperatorFormula());
ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isEventuallyFormula());
@ -114,11 +114,11 @@ TEST(FormulaParserTest, NestedPathFormulaTest) {
}
TEST(FormulaParserTest, CommentTest) {
storm::parser::FormulaParser parser;
storm::parser::FormulaParser formulaParser;
std::string input = "// This is a comment. And this is a commented out formula: P<=0.5 [ F \"a\" ] The next line contains the actual formula. \n P<=0.5 [ X \"b\" ] // Another comment \n // And again: another comment.";
std::shared_ptr<storm::logic::Formula> formula(nullptr);
ASSERT_NO_THROW(formula = parser.parseFromString(input));
ASSERT_NO_THROW(formula = formulaParser.parseSingleFormulaFromString(input));
EXPECT_TRUE(formula->isProbabilityOperatorFormula());
ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().isNextFormula());
ASSERT_TRUE(formula->asProbabilityOperatorFormula().getSubformula().asNextFormula().getSubformula().isAtomicLabelFormula());
@ -130,20 +130,20 @@ TEST(FormulaParserTest, WrongFormatTest) {
manager->declareBooleanVariable("x");
manager->declareIntegerVariable("y");
storm::parser::FormulaParser parser(manager);
storm::parser::FormulaParser formulaParser(manager);
std::string input = "P>0.5 [ a ]";
std::shared_ptr<storm::logic::Formula> formula(nullptr);
EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException);
EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P=0.5 [F \"a\"]";
EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException);
EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P>0.5 [F !(x = 0)]";
EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException);
EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P>0.5 [F !y]";
EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException);
EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
input = "P>0.5 [F y!=0)]";
EXPECT_THROW(formula = parser.parseFromString(input), storm::exceptions::WrongFormatException);
EXPECT_THROW(formula = formulaParser.parseSingleFormulaFromString(input), storm::exceptions::WrongFormatException);
}
Write Preview
Loading…
Cancel
Save