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

Changed the Prctl/Csl formula parsers to be static classes. 

- Also fixed up control flow and some tests for new interfaces.
|-> It now compiles again.

Next up: More functionallity in the filter.


Former-commit-id: 21d43e75c4
tempestpy_adaptions
masawei 11 years ago
parent
185c2197cb
commit
4bf0299279
15 changed files with 359 additions and 429 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. 2
      src/formula/Csl/CslFilter.h
  2. 18
      src/formula/Prctl/PrctlFilter.h
  3. 4
      src/parser/CslParser.cpp
  4. 37
      src/parser/CslParser.h
  5. 10
      src/parser/PrctlFileParser.cpp
  6. 19
      src/parser/PrctlFileParser.h
  7. 7
      src/parser/PrctlParser.cpp
  8. 58
      src/parser/PrctlParser.h
  9. 18
      src/storm.cpp
  10. 58
      test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
  11. 155
      test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
  12. 129
      test/functional/parser/CslParserTest.cpp
  13. 131
      test/functional/parser/PrctlParserTest.cpp
  14. 39
      test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
  15. 103
      test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp

2
src/formula/Csl/CslFilter.h
View File

@ -154,7 +154,7 @@ public:
std::string desc = "Filter: ";
desc += "\nActions:";
for(auto action : this->actions) {
desc += "\n\t" + action.toString();
desc += "\n\t" + action->toString();
}
desc += "\nFormula:\n\t" + child->toString();
return desc;

18
src/formula/Prctl/PrctlFilter.h
View File

@ -63,7 +63,7 @@ public:
storm::storage::BitVector result;
try {
result = evaluate(modelchecker, static_cast<AbstractStateFormula<T>*>(child));
result = evaluate(modelchecker, dynamic_cast<AbstractStateFormula<T>*>(child));
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
@ -80,7 +80,7 @@ public:
// Return the results for all states labeled with "init".
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : modelchecker.getModel().getInitialStates()) {
for (auto initialState : modelchecker.template getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result.get(initialState) ? "satisfied" : "not satisfied"));
std::cout << "\t" << initialState << ": " << result.get(initialState) << std::endl;
}
@ -95,7 +95,7 @@ public:
std::vector<T> result;
try {
result = evaluate(modelchecker, static_cast<AbstractPathFormula<T>*>(child));
result = evaluate(modelchecker, dynamic_cast<AbstractPathFormula<T>*>(child));
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
@ -112,7 +112,7 @@ public:
// Return the results for all states labeled with "init".
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : modelchecker.getModel().getInitialStates()) {
for (auto initialState : modelchecker.template getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]);
std::cout << "\t" << initialState << ": " << result[initialState] << std::endl;
}
@ -127,7 +127,7 @@ public:
std::vector<T> result;
try {
result = evaluate(modelchecker, static_cast<AbstractRewardPathFormula<T>*>(child));
result = evaluate(modelchecker, dynamic_cast<AbstractRewardPathFormula<T>*>(child));
} catch (std::exception& e) {
std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
@ -144,7 +144,7 @@ public:
// Return the results for all states labeled with "init".
LOG4CPLUS_INFO(logger, "Result for initial states:");
std::cout << "Result for initial states:" << std::endl;
for (auto initialState : modelchecker.getModel().getInitialStates()) {
for (auto initialState : modelchecker.template getModel<storm::models::AbstractModel<T>>().getInitialStates()) {
LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << result[initialState]);
std::cout << "\t" << initialState << ": " << result[initialState] << std::endl;
}
@ -208,7 +208,7 @@ private:
if(this->getActionCount() != 0 && dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0)) != nullptr) {
// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
result = modelchecker.checkMinMaxOperator(formula, static_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
result = modelchecker.checkMinMaxOperator(*formula, static_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
} else {
result = formula->check(modelchecker);
}
@ -227,7 +227,7 @@ private:
if(this->getActionCount() != 0 && dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0)) != nullptr) {
// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
result = modelchecker.checkMinMaxOperator(formula, static_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
result = modelchecker.checkMinMaxOperator(*formula, dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
} else {
result = formula->check(modelchecker, false);
}
@ -245,7 +245,7 @@ private:
if(this->getActionCount() != 0 && dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0)) != nullptr) {
// If there is an action specifying that min/max probabilities should be computed, call the appropriate method of the model checker.
result = modelchecker.checkMinMaxOperator(formula, static_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
result = modelchecker.checkMinMaxOperator(*formula, dynamic_cast<storm::property::action::MinMaxAction<T>*>(this->getAction(0))->getMinimize());
} else {
result = formula->check(modelchecker, false);
}

4
src/parser/CslParser.cpp
View File

@ -43,7 +43,7 @@ namespace storm {
namespace parser {
template<typename Iterator, typename Skipper>
struct CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFilter<double>*(), Skipper > {
struct CslParser::CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFilter<double>*(), Skipper > {
CslGrammar() : CslGrammar::base_type(start) {
//This block contains helper rules that may be used several times
freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))];
@ -202,7 +202,7 @@ struct CslGrammar : qi::grammar<Iterator, storm::property::csl::CslFilter<double
};
storm::property::csl::CslFilter<double>* CslParser(std::string formulaString) {
storm::property::csl::CslFilter<double>* CslParser::parseCslFormula(std::string formulaString) {
// Prepare iterators to input.
BaseIteratorType stringIteratorBegin = formulaString.begin();
BaseIteratorType stringIteratorEnd = formulaString.end();

37
src/parser/CslParser.h
View File

@ -15,22 +15,29 @@
namespace storm {
namespace parser {
/*!
* Reads a CSL formula from its string representation and parses it into a formula tree, consisting of
* classes in the namespace storm::property.
*
* If the string could not be parsed successfully, it will throw a wrongFormatException.
*
* @param formulaString The string representation of the formula
* @throw wrongFormatException If the input could not be parsed successfully
*/
storm::property::csl::CslFilter<double>* CslParser(std::string formulaString);
class CslParser {
public:
/*!
* Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas.
*/
template<typename Iterator, typename Skipper>
struct CslGrammar;
/*!
* Reads a CSL formula from its string representation and parses it into a formula tree, consisting of
* classes in the namespace storm::property.
*
* If the string could not be parsed successfully, it will throw a wrongFormatException.
*
* @param formulaString The string representation of the formula
* @throw wrongFormatException If the input could not be parsed successfully
*/
static storm::property::csl::CslFilter<double>* parseCslFormula(std::string formulaString);
private:
/*!
* Struct for the CSL grammar, that Boost::Spirit uses to parse the formulas.
*/
template<typename Iterator, typename Skipper>
struct CslGrammar;
};
} /* namespace parser */
} /* namespace storm */

10
src/parser/PrctlFileParser.cpp
View File

@ -14,7 +14,7 @@
namespace storm {
namespace parser {
std::list<storm::property::prctl::PrctlFilter<double>*> PrctlFileParser(std::string filename) {
std::list<storm::property::prctl::PrctlFilter<double>*> PrctlFileParser::parsePrctlFile(std::string filename) {
// Open file
std::ifstream inputFileStream;
inputFileStream.open(filename, std::ios::in);
@ -29,11 +29,11 @@ std::list<storm::property::prctl::PrctlFilter<double>*> PrctlFileParser(std::str
std::string line;
//The while loop reads the input file line by line
while (std::getline(inputFileStream, line)) {
PrctlParser parser(line);
if (!parser.parsedComment()) {
storm::property::prctl::PrctlFilter<double>* formula = PrctlParser::parsePrctlFormula(line);
if (formula != nullptr) {
//lines containing comments will be skipped.
LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + parser.getFormula()->toString() + "\"");
result.push_back(parser.getFormula());
LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + formula->toString() + "\"");
result.push_back(formula);
}
}

19
src/parser/PrctlFileParser.h
View File

@ -16,13 +16,18 @@
namespace storm {
namespace parser {
/*!
* Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
*
* @param filename
* @return The list of parsed formulas
*/
std::list<storm::property::prctl::PrctlFilter<double>*> PrctlFileParser(std::string filename);
class PrctlFileParser {
public:
/*!
* Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
*
* @param filename
* @return The list of parsed formulas
*/
static std::list<storm::property::prctl::PrctlFilter<double>*> parsePrctlFile(std::string filename);
};
} /* namespace parser */
} /* namespace storm */

7
src/parser/PrctlParser.cpp
View File

@ -32,7 +32,6 @@ namespace qi = boost::spirit::qi;
namespace phoenix = boost::phoenix;
namespace storm {
namespace parser {
@ -165,7 +164,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
qi::_1];
filter.name("PRCTL formula filter");
start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment) > qi::eoi;
start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = nullptr]) > qi::eoi;
start.name("PRCTL formula filter");
}
@ -216,7 +215,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl:
} //namespace storm
} //namespace parser
storm::parser::PrctlParser::PrctlParser(std::string formulaString) {
storm::property::prctl::PrctlFilter<double>* storm::parser::PrctlParser::parsePrctlFormula(std::string formulaString) {
// Prepare iterators to input.
BaseIteratorType stringIteratorBegin = formulaString.begin();
BaseIteratorType stringIteratorEnd = formulaString.end();
@ -259,5 +258,5 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) {
throw storm::exceptions::WrongFormatException() << msg.str();
}
formula = result_pointer;
return result_pointer;
}

58
src/parser/PrctlParser.h
View File

@ -17,43 +17,27 @@ namespace parser {
* class PrctlParser). However, it will not delete this object.
*/
class PrctlParser {
public:
/*!
* Reads a PRCTL formula from its string representation and parses it into a formula tree, consisting of
* classes in the namespace storm::property.
*
* If the string could not be parsed successfully, it will throw a wrongFormatException.
*
* @param formulaString The string representation of the formula
* @throw wrongFormatException If the input could not be parsed successfully
*/
PrctlParser(std::string formulaString);
/*!
* @return a pointer to the parsed formula object
*/
storm::property::prctl::PrctlFilter<double>* getFormula() {
return this->formula;
}
/*!
* Checks whether the line which was parsed was a comment line; also returns true if the line was empty (as the semantics are
* the same)
*
* @return True if the parsed line consisted completely of a (valid) comment, false otherwise.
*/
bool parsedComment() {
return (formula == nullptr);
}
private:
storm::property::prctl::PrctlFilter<double>* formula;
/*!
* Struct for the Prctl grammar, that Boost::Spirit uses to parse the formulas.
*/
template<typename Iterator, typename Skipper>
struct PrctlGrammar;
public:
/*!
* Reads a PRCTL formula from its string representation and parses it into a formula tree, consisting of
* classes in the namespace storm::property.
*
* If the string could not be parsed successfully, it will throw a wrongFormatException.
*
* @param formulaString The string representation of the formula
* @throw wrongFormatException If the input could not be parsed successfully
* @return A pointer to the parsed Prctl formula. If the line just contained a comment a nullptr will be returned instead.
*/
static storm::property::prctl::PrctlFilter<double>* parsePrctlFormula(std::string formulaString);
private:
/*!
* Struct for the Prctl grammar, that Boost::Spirit uses to parse the formulas.
*/
template<typename Iterator, typename Skipper>
struct PrctlGrammar;
};

18
src/storm.cpp
View File

@ -285,10 +285,10 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
if (s->isSet("prctl")) {
std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString();
LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << ".");
std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile);
std::list<storm::property::prctl::PrctlFilter<double>*> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile);
for (auto formula : formulaList) {
modelchecker.check(*formula);
formula->check(modelchecker);
delete formula;
}
}
@ -339,7 +339,7 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString();
LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << ".");
std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile);
std::list<storm::property::prctl::PrctlFilter<double>*> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(chosenPrctlFile);
// Test for each formula if a counterexample can be generated for it.
if(formulaList.size() == 0) {
@ -369,13 +369,13 @@ void checkPrctlFormulae(storm::modelchecker::prctl::AbstractModelChecker<double>
for (auto formula : formulaList) {
// First check if it is a formula type for which a counterexample can be generated.
if (dynamic_cast<storm::property::prctl::AbstractStateFormula<double> const*>(formula) == nullptr) {
if (dynamic_cast<storm::property::prctl::AbstractStateFormula<double> const*>(formula->getChild()) == nullptr) {
LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula.");
delete formula;
continue;
}
storm::property::prctl::AbstractStateFormula<double> const& stateForm = static_cast<storm::property::prctl::AbstractStateFormula<double> const&>(*formula);
storm::property::prctl::AbstractStateFormula<double> const& stateForm = static_cast<storm::property::prctl::AbstractStateFormula<double> const&>(*(formula->getChild()));
// Do some output
std::cout << "Generating counterexample for formula " << fIndex << ":" << std::endl;
@ -552,14 +552,14 @@ int main(const int argc, const char* argv[]) {
// Now parse the property file and receive the list of parsed formulas.
std::string const& propertyFile = s->getOptionByLongName("mincmd").getArgumentByName("propertyFile").getValueAsString();
std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = storm::parser::PrctlFileParser(propertyFile);
std::list<storm::property::prctl::PrctlFilter<double>*> formulaList = storm::parser::PrctlFileParser::parsePrctlFile(propertyFile);
// Now generate the counterexamples for each formula.
for (storm::property::prctl::AbstractPrctlFormula<double>* formulaPtr : formulaList) {
for (storm::property::prctl::PrctlFilter<double>* formulaPtr : formulaList) {
if (useMILP) {
storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(program, *mdp, formulaPtr);
storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(program, *mdp, formulaPtr->getChild());
} else {
storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, constants, *mdp, formulaPtr);
storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, constants, *mdp, formulaPtr->getChild());
}
// Once we are done with the formula, delete it.

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

@ -24,43 +24,39 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) {
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("one");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
std::vector<double> result = probFormula->check(mc);
std::vector<double> result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("two");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
result = probFormula->check(mc);
result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
result = probFormula->check(mc);
result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - ((double)1.0/6.0)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
storm::property::prctl::Ap<double>* done = new storm::property::prctl::Ap<double>("done");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(done);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula);
result = rewardFormula->check(mc);
result = reachabilityRewardFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - ((double)11/3)), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
delete reachabilityRewardFormula;
}
TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
@ -73,40 +69,37 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 8607ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460ull);
ASSERT_EQ(8607ull, dtmc->getNumberOfStates());
ASSERT_EQ(22460ull, dtmc->getNumberOfTransitions());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("observe0Greater1");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
std::vector<double> result = probFormula->check(mc);
std::vector<double> result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 0.3328800375801578281), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("observeIGreater1");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
result = probFormula->check(mc);
result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 0.1522194965), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("observeOnlyTrueSender");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
result = probFormula->check(mc);
result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 0.32153724292835045), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
}
TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
@ -118,38 +111,35 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 12400ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894ull);
ASSERT_EQ(12400ull, dtmc->getNumberOfStates());
ASSERT_EQ(28894ull, dtmc->getNumberOfTransitions());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
std::vector<double> result = probFormula->check(mc);
std::vector<double> result = eventuallyFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedUntil<double>* boundedUntilFormula = new storm::property::prctl::BoundedUntil<double>(new storm::property::prctl::Ap<double>("true"), apFormula, 20);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
result = probFormula->check(mc);
result = boundedUntilFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 0.9999965911265462636), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete boundedUntilFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula);
result = rewardFormula->check(mc);
result = reachabilityRewardFormula->check(mc, false);
ASSERT_LT(std::abs(result[0] - 1.044879046), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
delete reachabilityRewardFormula;
}

155
test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
View File

@ -21,81 +21,55 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
std::vector<double> result = mc.checkMinMaxOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("two");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 0.0277777612209320068), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("three");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 0.0555555224418640136), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("four");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("four");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 0.083333283662796020508), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = mc.checkNoBoundOperator(*rewardFormula);
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = mc.checkNoBoundOperator(*rewardFormula);;
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
delete reachabilityRewardFormula;
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.state.rew", "");
@ -107,21 +81,16 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = stateRewardModelChecker.checkNoBoundOperator(*rewardFormula);
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[0] - 7.333329499), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
delete reachabilityRewardFormula;
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.state.rew", STORM_CPP_BASE_PATH "/examples/mdp/two_dice/two_dice.flip.trans.rew");
@ -133,91 +102,67 @@ TEST(SparseMdpPrctlModelCheckerTest, Dice) {
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("done");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = stateAndTransitionRewardModelChecker.checkNoBoundOperator(*rewardFormula);
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[0] - 14.666658998), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
delete reachabilityRewardFormula;
}
TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
storm::settings::Settings* s = storm::settings::Settings::getInstance();
std::shared_ptr<storm::models::AbstractModel<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");
ASSERT_EQ(abstractModel->getType(), storm::models::MDP);
ASSERT_EQ(storm::models::MDP, abstractModel->getType());
std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 3172ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7144ull);
ASSERT_EQ(3172ull, mdp->getNumberOfStates());
ASSERT_EQ(7144ull, mdp->getNumberOfTransitions());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
std::vector<double> result = mc.checkMinMaxOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 1), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*boundedEventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*boundedEventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 0.0625), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete boundedEventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = mc.checkNoBoundOperator(*rewardFormula);;
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = mc.checkNoBoundOperator(*rewardFormula);;
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[0] - 4.285689611), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
delete reachabilityRewardFormula;
}

129
test/functional/parser/CslParserTest.cpp
View File

@ -11,130 +11,153 @@
#include "src/exceptions/WrongFormatException.h"
TEST(CslParserTest, parseApOnlyTest) {
std::string formula = "ap";
storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
std::string input = "ap";
storm::property::csl::CslFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
cslFormula = storm::parser::CslParser(formula);
formula = storm::parser::CslParser::parseCslFormula(input);
);
ASSERT_NE(cslFormula, nullptr);
ASSERT_EQ(cslFormula->toString(), formula);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
delete cslFormula;
// The input was parsed correctly.
ASSERT_EQ(input, formula->toString());
delete formula;
}
TEST(CslParserTest, parsePropositionalFormulaTest) {
std::string formula = "!(a & b) | a & ! c";
storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
std::string input = "!(a & b) | a & ! c";
storm::property::csl::CslFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
cslFormula = storm::parser::CslParser(formula);
formula = storm::parser::CslParser::parseCslFormula(input);
);
ASSERT_NE(cslFormula, nullptr);
ASSERT_EQ(cslFormula->toString(), "(!(a & b) | (a & !c))");
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
// The input was parsed correctly.
ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString());
delete cslFormula;
delete formula;
}
TEST(CslParserTest, parseProbabilisticFormulaTest) {
std::string formula = "P > 0.5 [ F a ]";
storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
std::string input = "P > 0.5 [ F a ]";
storm::property::csl::CslFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
cslFormula = storm::parser::CslParser(formula);
formula = storm::parser::CslParser::parseCslFormula(input);
);
ASSERT_NE(cslFormula, nullptr);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
storm::property::csl::ProbabilisticBoundOperator<double>* op = static_cast<storm::property::csl::ProbabilisticBoundOperator<double>*>(cslFormula);
ASSERT_NE(dynamic_cast<storm::property::csl::ProbabilisticBoundOperator<double>*>(formula->getChild()), nullptr);
storm::property::csl::ProbabilisticBoundOperator<double>* op = static_cast<storm::property::csl::ProbabilisticBoundOperator<double>*>(formula->getChild());
ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator());
ASSERT_EQ(0.5, op->getBound());
ASSERT_EQ(cslFormula->toString(), "P > 0.500000 [F a]");
// Test the string representation for the parsed formula.
ASSERT_EQ("P > 0.500000 [F a]", formula->toString());
delete cslFormula;
delete formula;
}
TEST(CslParserTest, parseSteadyStateBoundFormulaTest) {
std::string formula = "S >= 15 [ P < 0.2 [ a U<=3 b ] ]";
storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
std::string input = "S >= 15 [ P < 0.2 [ a U<=3 b ] ]";
storm::property::csl::CslFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
cslFormula = storm::parser::CslParser(formula);
formula = storm::parser::CslParser::parseCslFormula(input);
);
ASSERT_NE(cslFormula, nullptr);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
storm::property::csl::SteadyStateBoundOperator<double>* op = static_cast<storm::property::csl::SteadyStateBoundOperator<double>*>(cslFormula);
storm::property::csl::SteadyStateBoundOperator<double>* op = static_cast<storm::property::csl::SteadyStateBoundOperator<double>*>(formula->getChild());
ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator());
ASSERT_EQ(15.0, op->getBound());
ASSERT_EQ(cslFormula->toString(), "S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]");
// Test the string representation for the parsed formula.
ASSERT_EQ("S >= 15.000000 [P < 0.200000 [a U[0.000000,3.000000] b]]", formula->toString());
delete cslFormula;
delete formula;
}
TEST(CslParserTest, parseSteadyStateNoBoundFormulaTest) {
std::string formula = "S = ? [ P <= 0.5 [ F<=3 a ] ]";
storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
std::string input = "S = ? [ P <= 0.5 [ F<=3 a ] ]";
storm::property::csl::CslFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
cslFormula = storm::parser::CslParser(formula);
formula = storm::parser::CslParser::parseCslFormula(input);
);
ASSERT_NE(cslFormula, nullptr);
ASSERT_EQ(cslFormula->toString(), "S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]");
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
// The input was parsed correctly.
ASSERT_EQ("S = ? [P <= 0.500000 [F[0.000000,3.000000] a]]", formula->toString());
delete cslFormula;
delete formula;
}
TEST(CslParserTest, parseProbabilisticNoBoundFormulaTest) {
std::string formula = "P = ? [ a U [3,4] b & (!c) ]";
storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
std::string input = "P = ? [ a U [3,4] b & (!c) ]";
storm::property::csl::CslFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
cslFormula = storm::parser::CslParser(formula);
formula = storm::parser::CslParser::parseCslFormula(input);
);
ASSERT_NE(cslFormula, nullptr);
ASSERT_EQ(cslFormula->toString(), "P = ? [a U[3.000000,4.000000] (b & !c)]");
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
delete cslFormula;
// The input was parsed correctly.
ASSERT_EQ("P = ? [a U[3.000000,4.000000] (b & !c)]", formula->toString());
delete formula;
}
TEST(CslParserTest, parseComplexFormulaTest) {
std::string formula = "S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ]) //and a comment";
storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
std::string input = "S<=0.5 [ P <= 0.5 [ a U c ] ] & (P > 0.5 [ G b] | !P < 0.4 [ G P>0.9 [F >=7 a & b] ]) //and a comment";
storm::property::csl::CslFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
cslFormula = storm::parser::CslParser(formula);
formula = storm::parser::CslParser::parseCslFormula(input);
);
ASSERT_NE(cslFormula, nullptr);
ASSERT_EQ(cslFormula->toString(), "(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F>=7.000000 (a & b)]]))");
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
// The input was parsed correctly.
ASSERT_EQ("(S <= 0.500000 [P <= 0.500000 [a U c]] & (P > 0.500000 [G b] | !P < 0.400000 [G P > 0.900000 [F>=7.000000 (a & b)]]))", formula->toString());
delete cslFormula;
delete formula;
}
TEST(CslParserTest, wrongProbabilisticFormulaTest) {
std::string formula = "P > 0.5 [ a ]";
storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
std::string input = "P > 0.5 [ a ]";
storm::property::csl::CslFilter<double>* formula = nullptr;
ASSERT_THROW(
cslFormula = storm::parser::CslParser(formula),
formula = storm::parser::CslParser::parseCslFormula(input),
storm::exceptions::WrongFormatException
);
delete formula;
}
TEST(CslParserTest, wrongFormulaTest) {
std::string formula = "(a | b) & +";
storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
std::string input = "(a | b) & +";
storm::property::csl::CslFilter<double>* formula = nullptr;
ASSERT_THROW(
cslFormula = storm::parser::CslParser(formula),
formula = storm::parser::CslParser::parseCslFormula(input),
storm::exceptions::WrongFormatException
);
delete formula;
}
TEST(CslParserTest, wrongFormulaTest2) {
std::string formula = "P>0 [ F & a ]";
storm::property::csl::AbstractCslFormula<double>* cslFormula = nullptr;
std::string input = "P>0 [ F & a ]";
storm::property::csl::CslFilter<double>* formula = nullptr;
ASSERT_THROW(
cslFormula = storm::parser::CslParser(formula),
formula = storm::parser::CslParser::parseCslFormula(input),
storm::exceptions::WrongFormatException
);
delete formula;
}

131
test/functional/parser/PrctlParserTest.cpp
View File

@ -12,149 +12,158 @@
#include "src/exceptions/WrongFormatException.h"
TEST(PrctlParserTest, parseApOnlyTest) {
std::string ap = "ap";
storm::parser::PrctlParser* prctlParser = nullptr;
std::string input = "ap";
storm::property::prctl::PrctlFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser(ap);
formula = storm::parser::PrctlParser::parsePrctlFormula(input)
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
// The input was parsed correctly.
ASSERT_EQ(input, formula->toString());
ASSERT_EQ(ap, prctlParser->getFormula()->toString());
delete prctlParser->getFormula();
delete prctlParser;
delete formula;
}
TEST(PrctlParserTest, parsePropositionalFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
std::string input = "!(a & b) | a & ! c";
storm::property::prctl::PrctlFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser("!(a & b) | a & ! c")
formula = storm::parser::PrctlParser::parsePrctlFormula(input)
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "(!(a & b) | (a & !c))");
// The input was parsed correctly.
ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString());
delete prctlParser->getFormula();
delete prctlParser;
delete formula;
}
TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
std::string input = "P > 0.5 [ F a ]";
storm::property::prctl::PrctlFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser("P > 0.5 [ F a ]")
formula = storm::parser::PrctlParser::parsePrctlFormula(input)
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
storm::property::prctl::ProbabilisticBoundOperator<double>* op = static_cast<storm::property::prctl::ProbabilisticBoundOperator<double>*>(prctlParser->getFormula());
ASSERT_NE(dynamic_cast<storm::property::prctl::ProbabilisticBoundOperator<double>*>(formula->getChild()), nullptr);
storm::property::prctl::ProbabilisticBoundOperator<double>* op = static_cast<storm::property::prctl::ProbabilisticBoundOperator<double>*>(formula->getChild());
ASSERT_EQ(storm::property::GREATER, op->getComparisonOperator());
ASSERT_EQ(0.5, op->getBound());
ASSERT_EQ(prctlParser->getFormula()->toString(), "P > 0.500000 [F a]");
// Test the string representation for the parsed formula.
ASSERT_EQ("P > 0.500000 [F a]", formula->toString());
delete prctlParser->getFormula();
delete prctlParser;
delete formula;
}
TEST(PrctlParserTest, parseRewardFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
std::string input = "R >= 15 [ I=5 ]";
storm::property::prctl::PrctlFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser("R >= 15 [ I=5 ]")
formula = storm::parser::PrctlParser::parsePrctlFormula(input);
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
storm::property::prctl::RewardBoundOperator<double>* op = static_cast<storm::property::prctl::RewardBoundOperator<double>*>(prctlParser->getFormula());
ASSERT_NE(dynamic_cast<storm::property::prctl::RewardBoundOperator<double>*>(formula->getChild()), nullptr);
storm::property::prctl::RewardBoundOperator<double>* op = static_cast<storm::property::prctl::RewardBoundOperator<double>*>(formula->getChild());
ASSERT_EQ(storm::property::GREATER_EQUAL, op->getComparisonOperator());
ASSERT_EQ(15.0, op->getBound());
ASSERT_EQ("R >= 15.000000 [I=5]", prctlParser->getFormula()->toString());
// Test the string representation for the parsed formula.
ASSERT_EQ("R >= 15.000000 [I=5]", formula->toString());
delete prctlParser->getFormula();
delete prctlParser;
delete formula;
}
TEST(PrctlParserTest, parseRewardNoBoundFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
std::string input = "R = ? [ F a ]";
storm::property::prctl::PrctlFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser("R = ? [ F a ]")
formula = storm::parser::PrctlParser::parsePrctlFormula(input)
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "R = ? [F a]");
delete prctlParser->getFormula();
delete prctlParser;
// The input was parsed correctly.
ASSERT_EQ("R = ? [F a]", formula->toString());
delete formula;
}
TEST(PrctlParserTest, parseProbabilisticNoBoundFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
std::string input = "P = ? [ a U <= 4 b & (!c) ]";
storm::property::prctl::PrctlFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser("P = ? [ a U <= 4 b & (!c) ]")
formula = storm::parser::PrctlParser::parsePrctlFormula(input)
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
ASSERT_EQ(prctlParser->getFormula()->toString(), "P = ? [a U<=4 (b & !c)]");
delete prctlParser->getFormula();
delete prctlParser;
// The input was parsed correctly.
ASSERT_EQ("P = ? [a U<=4 (b & !c)]", formula->toString());
delete formula;
}
TEST(PrctlParserTest, parseComplexFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
std::string input = "R<=0.5 [ S ] & (R > 15 [ C<=0.5 ] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])";
storm::property::prctl::PrctlFilter<double>* formula = nullptr;
ASSERT_NO_THROW(
prctlParser = new storm::parser::PrctlParser("R<=0.5 [ S ] & (R > 15 [ C<=0.5 ] | !P < 0.4 [ G P>0.9 [F<=7 a & b] ])")
formula = storm::parser::PrctlParser::parsePrctlFormula(input)
);
ASSERT_NE(prctlParser->getFormula(), nullptr);
// The parser did not falsely recognize the input as a comment.
ASSERT_NE(formula, nullptr);
ASSERT_EQ("(R <= 0.500000 [S] & (R > 15.000000 [C <= 0.500000] | !P < 0.400000 [G P > 0.900000 [F<=7 (a & b)]]))", prctlParser->getFormula()->toString());
delete prctlParser->getFormula();
delete prctlParser;
// The input was parsed correctly.
ASSERT_EQ("(R <= 0.500000 [S] & (R > 15.000000 [C <= 0.500000] | !P < 0.400000 [G P > 0.900000 [F<=7 (a & b)]]))", formula->toString());
delete formula;
}
TEST(PrctlParserTest, wrongProbabilisticFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
storm::property::prctl::PrctlFilter<double>* formula = nullptr;
ASSERT_THROW(
prctlParser = new storm::parser::PrctlParser("P > 0.5 [ a ]"),
formula = storm::parser::PrctlParser::parsePrctlFormula("P > 0.5 [ a ]"),
storm::exceptions::WrongFormatException
);
delete prctlParser;
delete formula;
}
TEST(PrctlParserTest, wrongFormulaTest) {
storm::parser::PrctlParser* prctlParser = nullptr;
storm::property::prctl::PrctlFilter<double>* formula = nullptr;
ASSERT_THROW(
prctlParser = new storm::parser::PrctlParser("(a | b) & +"),
formula = storm::parser::PrctlParser::parsePrctlFormula("(a | b) & +"),
storm::exceptions::WrongFormatException
);
delete prctlParser;
delete formula;
}
TEST(PrctlParserTest, wrongFormulaTest2) {
storm::parser::PrctlParser* prctlParser = nullptr;
storm::property::prctl::PrctlFilter<double>* formula = nullptr;
ASSERT_THROW(
prctlParser = new storm::parser::PrctlParser("P>0 [ F & a ]"),
formula = storm::parser::PrctlParser::parsePrctlFormula("P>0 [ F & a ]"),
storm::exceptions::WrongFormatException
);
delete prctlParser;
delete formula;
}

39
test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
View File

@ -16,46 +16,43 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 2036647ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 8973900ull);
ASSERT_EQ(2036647ull, dtmc->getNumberOfStates());
ASSERT_EQ(8973900ull, dtmc->getNumberOfTransitions());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("observe0Greater1");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F observe0Greater1] on crowds/crowds20_5...");
std::vector<double> result = probFormula->check(mc);
std::vector<double> result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 0.2296800237), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("observeIGreater1");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeIGreater1] on crowds/crowds20_5...");
result = probFormula->check(mc);
result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 0.05073232193), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("observeOnlyTrueSender");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F observeOnlyTrueSender] on crowds/crowds20_5...");
result = probFormula->check(mc);
result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 0.22742171078), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
}
@ -67,47 +64,43 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
ASSERT_EQ(abstractModel->getType(), storm::models::DTMC);
std::shared_ptr<storm::models::Dtmc<double>> dtmc = abstractModel->as<storm::models::Dtmc<double>>();
ASSERT_EQ(dtmc->getNumberOfStates(), 1312334ull);
ASSERT_EQ(dtmc->getNumberOfTransitions(), 2886810ull);
ASSERT_EQ(1312334ull, dtmc->getNumberOfStates());
ASSERT_EQ(2886810ull, dtmc->getNumberOfTransitions());
storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(*dtmc, new storm::solver::GmmxxLinearEquationSolver<double>());
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F elected] on synchronous_leader/leader6_8...");
std::vector<double> result = probFormula->check(mc);
std::vector<double> result = eventuallyFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedUntil<double>* boundedUntilFormula = new storm::property::prctl::BoundedUntil<double>(new storm::property::prctl::Ap<double>("true"), apFormula, 20);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedUntilFormula);
LOG4CPLUS_WARN(logger, "Model Checking P=? [F<=20 elected] on synchronous_leader/leader6_8...");
result = probFormula->check(mc);
result = boundedUntilFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 0.9993949793), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete boundedUntilFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula);
LOG4CPLUS_WARN(logger, "Model Checking R=? [F elected] on synchronous_leader/leader6_8...");
result = rewardFormula->check(mc);
result = reachabilityRewardFormula->check(mc, false);
LOG4CPLUS_WARN(logger, "Done.");
ASSERT_LT(std::abs(result[0] - 1.025106273), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
delete reachabilityRewardFormula;
}

103
test/performance/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
View File

@ -14,64 +14,49 @@ TEST(SparseMdpPrctlModelCheckerTest, AsynchronousLeader) {
std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 2095783ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 7714385ull);
ASSERT_EQ(2095783ull, mdp->getNumberOfStates());
ASSERT_EQ(7714385ull, mdp->getNumberOfTransitions());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
std::vector<double> result = mc.checkMinMaxOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*boundedEventuallyFormula, true);
ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 25);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*boundedEventuallyFormula, false);
ASSERT_LT(std::abs(result[0] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete boundedEventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = mc.checkNoBoundOperator(*rewardFormula);
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[0] - 6.172433512), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("elected");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = mc.checkNoBoundOperator(*rewardFormula);
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[0] - 6.1724344), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
delete reachabilityRewardFormula;
}
TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
@ -85,87 +70,77 @@ TEST(SparseMdpPrctlModelCheckerTest, Consensus) {
std::shared_ptr<storm::models::Mdp<double>> mdp = abstractModel->as<storm::models::Mdp<double>>();
ASSERT_EQ(mdp->getNumberOfStates(), 63616ull);
ASSERT_EQ(mdp->getNumberOfTransitions(), 213472ull);
ASSERT_EQ(63616ull, mdp->getNumberOfStates());
ASSERT_EQ(213472ull, mdp->getNumberOfTransitions());
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<double> mc(*mdp, std::shared_ptr<storm::solver::NativeNondeterministicLinearEquationSolver<double>>(new storm::solver::NativeNondeterministicLinearEquationSolver<double>()));
storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
storm::property::prctl::ProbabilisticNoBoundOperator<double>* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
std::vector<double> result = mc.checkNoBoundOperator(*probFormula);
std::vector<double> result = mc.checkMinMaxOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[31168] - 1.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::Ap<double>* apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_0");
storm::property::prctl::And<double>* andFormula = new storm::property::prctl::And<double>(apFormula, apFormula2);
eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*eventuallyFormula, true);
ASSERT_LT(std::abs(result[31168] - 0.4374282832), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("finished");
apFormula2 = new storm::property::prctl::Ap<double>("all_coins_equal_1");
andFormula = new storm::property::prctl::And<double>(apFormula, apFormula2);
eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[31168] - 0.5293286369), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("finished");
apFormula2 = new storm::property::prctl::Ap<double>("agree");
storm::property::prctl::Not<double>* notFormula = new storm::property::prctl::Not<double>(apFormula2);
andFormula = new storm::property::prctl::And<double>(apFormula, notFormula);
eventuallyFormula = new storm::property::prctl::Eventually<double>(andFormula);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(eventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*eventuallyFormula, false);
ASSERT_LT(std::abs(result[31168] - 0.10414097), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete eventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::BoundedEventually<double>* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, true);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*boundedEventuallyFormula, true);
ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
apFormula = new storm::property::prctl::Ap<double>("finished");
boundedEventuallyFormula = new storm::property::prctl::BoundedEventually<double>(apFormula, 50ull);
probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator<double>(boundedEventuallyFormula, false);
result = mc.checkNoBoundOperator(*probFormula);
result = mc.checkMinMaxOperator(*boundedEventuallyFormula, false);
ASSERT_LT(std::abs(result[31168] - 0.0), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete probFormula;
delete boundedEventuallyFormula;
apFormula = new storm::property::prctl::Ap<double>("finished");
storm::property::prctl::ReachabilityReward<double>* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
storm::property::prctl::RewardNoBoundOperator<double>* rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, true);
result = mc.checkNoBoundOperator(*rewardFormula);
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, true);
ASSERT_LT(std::abs(result[31168] - 1725.593313), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
apFormula = new storm::property::prctl::Ap<double>("finished");
reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
rewardFormula = new storm::property::prctl::RewardNoBoundOperator<double>(reachabilityRewardFormula, false);
result = mc.checkNoBoundOperator(*rewardFormula);
result = mc.checkMinMaxOperator(*reachabilityRewardFormula, false);
ASSERT_LT(std::abs(result[31168] - 2183.142422), s->getOptionByLongName("precision").getArgument(0).getValueAsDouble());
delete rewardFormula;
delete reachabilityRewardFormula;
}
Write Preview
Loading…
Cancel
Save