diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h
index 8b151c834..7e57fff60 100644
--- a/src/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h
@@ -1016,7 +1016,7 @@ namespace storm {
// Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape.
double bound = probBoundFormula->getBound();
- std::shared_ptr<storm::property::prctl::AbstractPathFormula<double>> pathFormula = probBoundFormula->getPathFormula();
+ std::shared_ptr<storm::property::prctl::AbstractPathFormula<double>> pathFormula = probBoundFormula->getChild();
storm::storage::BitVector phiStates;
storm::storage::BitVector psiStates;
storm::modelchecker::prctl::SparseMdpPrctlModelChecker<T> modelchecker(labeledMdp);
diff --git a/src/counterexamples/PathBasedSubsystemGenerator.h b/src/counterexamples/PathBasedSubsystemGenerator.h
index 94a7cc955..2713643bf 100644
--- a/src/counterexamples/PathBasedSubsystemGenerator.h
+++ b/src/counterexamples/PathBasedSubsystemGenerator.h
@@ -402,7 +402,7 @@ public:
return model.getSubDtmc(subSys);
}
T bound = boundOperator->getBound();
- std::shared_ptr<storm::property::prctl::AbstractPathFormula<T>> pathFormula = boundOperator->getPathFormula();;
+ std::shared_ptr<storm::property::prctl::AbstractPathFormula<T>> pathFormula = boundOperator->getChild();
// get "init" labeled states
storm::storage::BitVector initStates = model.getLabeledStates("init");
diff --git a/src/formula/actions/FormulaAction.h b/src/formula/actions/FormulaAction.h
index c22f8d7a0..9ac3ad861 100644
--- a/src/formula/actions/FormulaAction.h
+++ b/src/formula/actions/FormulaAction.h
@@ -80,7 +80,7 @@ public:
*
*/
virtual std::string toString() const override {
- std::string out = "states(";
+ std::string out = "formula(";
if(prctlFormula.get() != nullptr) {
out += prctlFormula->toString();
} else if(cslFormula.get() != nullptr) {
diff --git a/src/formula/actions/RangeAction.h b/src/formula/actions/RangeAction.h
index ccb66fe00..382492d49 100644
--- a/src/formula/actions/RangeAction.h
+++ b/src/formula/actions/RangeAction.h
@@ -87,16 +87,16 @@ private:
uint_fast64_t end = to - from;
// Safety check for access bounds.
- if(from > result.stateMap.size()) {
+ if(from >= result.stateMap.size()) {
LOG4CPLUS_WARN(logger, "Range begins behind the end of the states by " << to - result.stateMap.size() << ". No state was selected.");
std::cout << "Range begins behind the end of the states by " << to - result.stateMap.size() << ". No state was selected." << std::endl;
return Result(out, result.stateMap, result.pathResult, result.stateResult);
}
- if(to > result.stateMap.size()) {
+ if(to >= result.stateMap.size()) {
- end = result.selection.size() - from;
+ end = result.selection.size() - from - 1;
LOG4CPLUS_WARN(logger, "Range ends behind the end of the states by " << to - result.stateMap.size() << ". The range has been cut at the last state.");
std::cout << "Range ends behind the end of the states by " << to - result.stateMap.size() << ". The range has been cut at the last state." << std::endl;
diff --git a/src/formula/actions/SortAction.h b/src/formula/actions/SortAction.h
index 35bc31026..ea676dfd4 100644
--- a/src/formula/actions/SortAction.h
+++ b/src/formula/actions/SortAction.h
@@ -65,7 +65,7 @@ public:
*
*/
virtual std::string toString() const override {
- std::string out = "sort, ";
+ std::string out = "sort(";
switch (category) {
case INDEX:
out += "index";
@@ -79,7 +79,7 @@ public:
break;
}
out += ", ";
- out += ascending ? "ascending" : "descending";
+ out += ascending ? "ascending)" : "descending)";
return out;
}
diff --git a/src/formula/prctl/Next.h b/src/formula/prctl/Next.h
index 3cff6892a..49b66c062 100644
--- a/src/formula/prctl/Next.h
+++ b/src/formula/prctl/Next.h
@@ -113,10 +113,8 @@ public:
* @returns a string representation of the formula
*/
virtual std::string toString() const override {
- std::string result = "(";
- result += " X ";
+ std::string result = "X ";
result += child->toString();
- result += ")";
return result;
}
diff --git a/src/formula/prctl/PrctlFilter.h b/src/formula/prctl/PrctlFilter.h
index 2f45b0ba3..161a9d3f8 100644
--- a/src/formula/prctl/PrctlFilter.h
+++ b/src/formula/prctl/PrctlFilter.h
@@ -65,6 +65,11 @@ public:
LOG4CPLUS_INFO(logger, "Model checking formula\t" << this->toString());
std::cout << "Model checking formula:\t" << this->toString() << std::endl;
+ writeOut(evaluate(modelchecker), modelchecker);
+ }
+
+ Result evaluate(storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
+
Result result;
try {
@@ -78,13 +83,9 @@ public:
} 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.");
- std::cout << std::endl << "-------------------------------------------" << std::endl;
-
- return;
}
- writeOut(result, modelchecker);
-
+ return result;
}
virtual std::string toString() const override {
@@ -239,12 +240,14 @@ private:
return evaluateActions(result, modelchecker);
}
- Result evaluateActions(Result result, storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
+ Result evaluateActions(Result const & input, storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
// Init the state selection and state map vectors.
- result.selection = storm::storage::BitVector(result.stateResult.size(), true);
- result.stateMap = std::vector<uint_fast64_t>(result.selection.size());
- for(uint_fast64_t i = 0; i < result.selection.size(); i++) {
+ Result result = input;
+ uint_fast64_t size = result.stateResult.size() == 0 ? result.pathResult.size() : result.stateResult.size();
+ result.selection = storm::storage::BitVector(size, true);
+ result.stateMap = std::vector<uint_fast64_t>(size);
+ for(uint_fast64_t i = 0; i < size; i++) {
result.stateMap[i] = i;
}
@@ -258,6 +261,13 @@ private:
void writeOut(Result const & result, storm::modelchecker::prctl::AbstractModelChecker<T> const & modelchecker) const {
+ // Test if there is anything to write out.
+ // The selection size should only be 0 if an error occurred during the evaluation (since a model with 0 states is invalid).
+ if(result.selection.size() == 0) {
+ std::cout << std::endl << "-------------------------------------------" << std::endl;
+ return;
+ }
+
// Test for the kind of result. Values or states.
if(!result.pathResult.empty()) {
diff --git a/src/formula/prctl/ProbabilisticBoundOperator.h b/src/formula/prctl/ProbabilisticBoundOperator.h
index 0fbe1339c..e1557ce04 100644
--- a/src/formula/prctl/ProbabilisticBoundOperator.h
+++ b/src/formula/prctl/ProbabilisticBoundOperator.h
@@ -60,7 +60,7 @@ public:
/*!
* Empty constructor
*/
- ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), pathFormula(nullptr) {
+ ProbabilisticBoundOperator() : comparisonOperator(LESS), bound(0), child(nullptr) {
// Intentionally left empty.
}
@@ -69,10 +69,10 @@ public:
*
* @param comparisonOperator The relation for the bound.
* @param bound The bound for the probability
- * @param pathFormula The child node
+ * @param child The child node
*/
- ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractPathFormula<T>> const & pathFormula)
- : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
+ ProbabilisticBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractPathFormula<T>> const & child)
+ : comparisonOperator(comparisonOperator), bound(bound), child(child) {
// Intentionally left empty.
}
@@ -96,7 +96,7 @@ public:
std::shared_ptr<ProbabilisticBoundOperator<T>> result(new ProbabilisticBoundOperator<T>());
result->setComparisonOperator(comparisonOperator);
result->setBound(bound);
- result->setPathFormula(pathFormula->clone());
+ result->setChild(child->clone());
return result;
}
@@ -120,7 +120,7 @@ public:
* @return true iff the subtree conforms to some logic.
*/
virtual bool validate(AbstractFormulaChecker<T> const & checker) const override {
- return checker.validate(pathFormula);
+ return checker.validate(child);
}
/*!
@@ -137,7 +137,7 @@ public:
result += " ";
result += std::to_string(bound);
result += " (";
- result += pathFormula->toString();
+ result += child->toString();
result += ")";
return result;
}
@@ -145,25 +145,25 @@ public:
/*!
* @returns the child node (representation of a formula)
*/
- std::shared_ptr<AbstractPathFormula<T>> const & getPathFormula () const {
- return pathFormula;
+ std::shared_ptr<AbstractPathFormula<T>> const & getChild () const {
+ return child;
}
/*!
* Sets the child node
*
- * @param pathFormula the path formula that becomes the new child node
+ * @param child the path formula that becomes the new child node
*/
- void setPathFormula(std::shared_ptr<AbstractPathFormula<T>> const & pathFormula) {
- this->pathFormula = pathFormula;
+ void setChild(std::shared_ptr<AbstractPathFormula<T>> const & child) {
+ this->child = child;
}
/*!
*
* @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
*/
- bool pathFormulaIsSet() const {
- return pathFormula.get() != nullptr;
+ bool childIsSet() const {
+ return child.get() != nullptr;
}
/*!
@@ -206,7 +206,7 @@ public:
private:
storm::property::ComparisonType comparisonOperator;
T bound;
- std::shared_ptr<AbstractPathFormula<T>> pathFormula;
+ std::shared_ptr<AbstractPathFormula<T>> child;
};
} //namespace prctl
diff --git a/src/formula/prctl/RewardBoundOperator.h b/src/formula/prctl/RewardBoundOperator.h
index 15fbd5886..cfebea0d6 100644
--- a/src/formula/prctl/RewardBoundOperator.h
+++ b/src/formula/prctl/RewardBoundOperator.h
@@ -58,7 +58,7 @@ public:
/*!
* Empty constructor
*/
- RewardBoundOperator() : comparisonOperator(LESS), bound(0), pathFormula(nullptr){
+ RewardBoundOperator() : comparisonOperator(LESS), bound(0), child(nullptr){
// Intentionally left empty
}
@@ -67,10 +67,10 @@ public:
*
* @param comparisonOperator The relation for the bound.
* @param bound The bound for the probability
- * @param pathFormula The child node
+ * @param child The child node
*/
- RewardBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractRewardPathFormula<T>> const & pathFormula)
- : comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
+ RewardBoundOperator(storm::property::ComparisonType comparisonOperator, T bound, std::shared_ptr<AbstractRewardPathFormula<T>> const & child)
+ : comparisonOperator(comparisonOperator), bound(bound), child(child) {
// Intentionally left empty
}
@@ -94,7 +94,7 @@ public:
std::shared_ptr<RewardBoundOperator<T>> result(new RewardBoundOperator<T>());
result->setComparisonOperator(comparisonOperator);
result->setBound(bound);
- result->setPathFormula(pathFormula->clone());
+ result->setChild(child->clone());
return result;
}
@@ -118,7 +118,7 @@ public:
* @return true iff the subtree conforms to some logic.
*/
virtual bool validate(AbstractFormulaChecker<T> const & checker) const override {
- return checker.validate(this->pathFormula);
+ return checker.validate(this->child);
}
/*!
@@ -135,7 +135,7 @@ public:
result += " ";
result += std::to_string(bound);
result += " (";
- result += pathFormula->toString();
+ result += child->toString();
result += ")";
return result;
}
@@ -143,25 +143,25 @@ public:
/*!
* @returns the child node (representation of a formula)
*/
- std::shared_ptr<AbstractRewardPathFormula<T>> const & getPathFormula () const {
- return pathFormula;
+ std::shared_ptr<AbstractRewardPathFormula<T>> const & getChild () const {
+ return child;
}
/*!
* Sets the child node
*
- * @param pathFormula the path formula that becomes the new child node
+ * @param child the path formula that becomes the new child node
*/
- void setPathFormula(std::shared_ptr<AbstractRewardPathFormula<T>> const & pathFormula) {
- this->pathFormula = pathFormula;
+ void setChild(std::shared_ptr<AbstractRewardPathFormula<T>> const & child) {
+ this->child = child;
}
/*!
*
* @return True if the path formula is set, i.e. it does not point to nullptr; false otherwise
*/
- bool pathFormulaIsSet() const {
- return pathFormula.get() != nullptr;
+ bool childIsSet() const {
+ return child.get() != nullptr;
}
/*!
@@ -204,7 +204,7 @@ public:
private:
storm::property::ComparisonType comparisonOperator;
T bound;
- std::shared_ptr<AbstractRewardPathFormula<T>> pathFormula;
+ std::shared_ptr<AbstractRewardPathFormula<T>> child;
};
} //namespace prctl
diff --git a/src/modelchecker/prctl/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h
index 7158ee9ff..f33cd8952 100644
--- a/src/modelchecker/prctl/AbstractModelChecker.h
+++ b/src/modelchecker/prctl/AbstractModelChecker.h
@@ -189,7 +189,7 @@ public:
*/
virtual storm::storage::BitVector checkProbabilisticBoundOperator(storm::property::prctl::ProbabilisticBoundOperator<Type> const& formula) const {
// First, we need to compute the probability for satisfying the path formula for each state.
- std::vector<Type> quantitativeResult = formula.getPathFormula()->check(*this, false);
+ std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false);
// Create resulting bit vector that will hold the yes/no-answer for every state.
storm::storage::BitVector result(quantitativeResult.size());
@@ -213,7 +213,7 @@ public:
*/
virtual storm::storage::BitVector checkRewardBoundOperator(const storm::property::prctl::RewardBoundOperator<Type>& formula) const {
// First, we need to compute the probability for satisfying the path formula for each state.
- std::vector<Type> quantitativeResult = formula.getPathFormula()->check(*this, false);
+ std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false);
// Create resulting bit vector that will hold the yes/no-answer for every state.
storm::storage::BitVector result(quantitativeResult.size());
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
index 23613d185..239a0a37f 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
@@ -87,7 +87,7 @@ namespace storm {
}
// First, we need to compute the probability for satisfying the path formula for each state.
- std::vector<Type> quantitativeResult = formula.getPathFormula()->check(*this, false);
+ std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false);
//Remove the minimizing operator entry from the stack.
this->minimumOperatorStack.pop();
@@ -124,7 +124,7 @@ namespace storm {
}
// First, we need to compute the probability for satisfying the path formula for each state.
- std::vector<Type> quantitativeResult = formula.getPathFormula()->check(*this, false);
+ std::vector<Type> quantitativeResult = formula.getChild()->check(*this, false);
//Remove the minimizing operator entry from the stack.
this->minimumOperatorStack.pop();
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index 6f3dc8812..35036ffcf 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -79,11 +79,10 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
atomicProposition = (freeIdentifierName)[qi::_val =
MAKE(prctl::Ap<double>, qi::_1)];
atomicProposition.name("atomic proposition");
- probabilisticBoundOperator = ((qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val =
+ probabilisticBoundOperator = ((qi::lit("P") >> comparisonType > qi::double_ > pathFormula)[qi::_val =
MAKE(prctl::ProbabilisticBoundOperator<double>, qi::_1, qi::_2, qi::_3)]);
-
probabilisticBoundOperator.name("probabilistic bound operator");
- rewardBoundOperator = ((qi::lit("R") >> comparisonType > qi::double_ > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val =
+ rewardBoundOperator = ((qi::lit("R") >> comparisonType > qi::double_ > rewardPathFormula)[qi::_val =
MAKE(prctl::RewardBoundOperator<double>, qi::_1, qi::_2, qi::_3)]);
rewardBoundOperator.name("reward bound operator");
@@ -92,22 +91,22 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
pathFormula.name("path formula");
boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
MAKE(prctl::BoundedEventually<double>, qi::_2, qi::_1)];
- boundedEventually.name("path formula (for probabilistic operator)");
+ boundedEventually.name("bounded eventually");
eventually = (qi::lit("F") > stateFormula)[qi::_val =
MAKE(prctl::Eventually<double>, qi::_1)];
- eventually.name("path formula (for probabilistic operator)");
+ eventually.name("eventually");
next = (qi::lit("X") > stateFormula)[qi::_val =
MAKE(prctl::Next<double>, qi::_1)];
- next.name("path formula (for probabilistic operator)");
+ next.name("next");
globally = (qi::lit("G") > stateFormula)[qi::_val =
MAKE(prctl::Globally<double>, qi::_1)];
- globally.name("path formula (for probabilistic operator)");
+ globally.name("globally");
boundedUntil = (stateFormula[qi::_a = qi::_1] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > stateFormula)[qi::_val =
MAKE(prctl::BoundedUntil<double>, qi::_a, qi::_3, qi::_2)];
- boundedUntil.name("path formula (for probabilistic operator)");
+ boundedUntil.name("boundedUntil");
until = (stateFormula[qi::_a = qi::_1] >> qi::lit("U") > stateFormula)[qi::_val =
MAKE(prctl::Until<double>, qi::_a, qi::_2)];
- until.name("path formula (for probabilistic operator)");
+ until.name("until");
// This block defines rules for parsing reward path formulas.
rewardPathFormula = (cumulativeReward | reachabilityReward | instantaneousReward | steadyStateReward | qi::lit("(") >> rewardPathFormula >> qi::lit(")") | qi::lit("[") >> rewardPathFormula >> qi::lit("]"));
@@ -175,16 +174,16 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
rangeAction.name("range action");
sortAction = (
- (qi::lit("sort") > qi::lit("(") >> sortingCategory >> qi::lit(")"))[qi::_val =
+ (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(")"))[qi::_val =
phoenix::new_<storm::property::action::SortAction<double>>(qi::_1)] |
- (qi::lit("sort") > qi::lit("(") >> sortingCategory >> qi::lit(", ") >> qi::lit("asc") > qi::lit(")"))[qi::_val =
+ (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("ascending") | qi::lit("asc")) > qi::lit(")"))[qi::_val =
phoenix::new_<storm::property::action::SortAction<double>>(qi::_1, true)] |
- (qi::lit("sort") > qi::lit("(") >> sortingCategory >> qi::lit(", ") >> qi::lit("desc") > qi::lit(")"))[qi::_val =
+ (qi::lit("sort") >> qi::lit("(") >> sortingCategory >> qi::lit(", ") >> (qi::lit("descending") | qi::lit("desc")) > qi::lit(")"))[qi::_val =
phoenix::new_<storm::property::action::SortAction<double>>(qi::_1, false)]
);
sortAction.name("sort action");
- abstractAction = (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (qi::eps | qi::lit(";"));
+ abstractAction = (boundAction | invertAction | formulaAction | rangeAction | sortAction) >> (qi::lit(";") | qi::eps);
abstractAction.name("filter action");
filter = (qi::lit("filter") >> qi::lit("[") >> +abstractAction >> qi::lit("]") > qi::lit("(") >> formula >> qi::lit(")"))[qi::_val =
@@ -200,7 +199,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, std::shared_ptr<storm::
filter.name("PRCTL formula filter");
start = (((filter) > (comment | qi::eps))[qi::_val = qi::_1] | comment[qi::_val = MAKE(prctl::PrctlFilter<double>, nullptr)]) > qi::eoi;
- start.name("PRCTL formula filter");
+ start.name("start");
}
diff --git a/test/functional/parser/ActionTest.cpp b/test/functional/modelchecker/ActionTest.cpp
similarity index 100%
rename from test/functional/parser/ActionTest.cpp
rename to test/functional/modelchecker/ActionTest.cpp
diff --git a/test/functional/modelchecker/FilterTest.cpp b/test/functional/modelchecker/FilterTest.cpp
new file mode 100644
index 000000000..e8ce4b156
--- /dev/null
+++ b/test/functional/modelchecker/FilterTest.cpp
@@ -0,0 +1,83 @@
+/*
+ * FilterTest.cpp
+ *
+ * Created on: Aug 6, 2014
+ * Author: Manuel Sascha Weiand
+ */
+
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/models/Dtmc.h"
+#include "src/parser/DeterministicModelParser.h"
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "src/solver/GmmxxLinearEquationSolver.h"
+#include "src/formula/prctl/PrctlFilter.h"
+#include "src/formula/csl/CslFilter.h"
+#include "src/formula/ltl/LtlFilter.h"
+#include "src/parser/PrctlParser.h"
+
+#include <regex>
+
+typedef typename storm::property::prctl::PrctlFilter<double>::Result Result;
+
+TEST(PrctlFilterTest, generalFunctionality) {
+ // Test filter queries of increasing complexity.
+
+ // Setup model and modelchecker.
+ storm::models::Dtmc<double> model = storm::parser::DeterministicModelParser::parseDtmc(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_actionTest.tra", STORM_CPP_TESTS_BASE_PATH "/functional/parser/lab_files/dtmc_actionTest.lab");
+ storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<double> mc(model, new storm::solver::GmmxxLinearEquationSolver<double>());
+
+ // Find the best valued state to finally reach a 'b' state.
+ std::string input = "filter[sort(value, descending); range(0,0)](F b)";
+ std::shared_ptr<storm::property::prctl::PrctlFilter<double>> formula(nullptr);
+ ASSERT_NO_THROW(
+ formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+ );
+
+ // Here we test if the check method gives the correct result.
+ // To capture the output, redirect cout and test the written buffer content.
+ std::stringstream buffer;
+ std::streambuf *sbuf = std::cout.rdbuf();
+ std::cout.rdbuf(buffer.rdbuf());
+
+ formula->check(mc);
+
+ std::string output = buffer.str();
+ ASSERT_NE(std::string::npos, output.find("\t6: 1"));
+
+ // Reset cout to the original buffer.
+ std::cout.rdbuf(sbuf);
+
+ // The remaining queries use evaluate directly as its easier to work with in a test environment.
+ // Get the probability to reach a b state for all states but those that cannot reach a 'b' state or are 'b' states themselves.
+ // Sorted by value; highest first.
+ input = "filter[formula(P<=0(F b) | b); invert; sort(value, desc)](F b)";
+ ASSERT_NO_THROW(
+ formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+ );
+
+ Result result = formula->evaluate(mc);
+
+ // Test the selection.
+ ASSERT_EQ(5, result.selection.getNumberOfSetBits());
+ ASSERT_TRUE(result.selection[0]);
+ ASSERT_TRUE(result.selection[1]);
+ ASSERT_TRUE(result.selection[2]);
+ ASSERT_TRUE(result.selection[3]);
+ ASSERT_TRUE(result.selection[4]);
+ ASSERT_FALSE(result.selection[5]);
+ ASSERT_FALSE(result.selection[6]);
+ ASSERT_FALSE(result.selection[7]);
+
+ // Test the sorting.
+ ASSERT_EQ(3, result.stateMap[0]);
+ ASSERT_EQ(4, result.stateMap[1]);
+ ASSERT_EQ(1, result.stateMap[2]);
+ ASSERT_EQ(0, result.stateMap[3]);
+ ASSERT_EQ(2, result.stateMap[4]);
+ ASSERT_EQ(5, result.stateMap[5]);
+ ASSERT_EQ(6, result.stateMap[6]);
+ ASSERT_EQ(7, result.stateMap[7]);
+}
+
+
diff --git a/test/functional/parser/PrctlParserTest.cpp b/test/functional/parser/PrctlParserTest.cpp
index 1d5e59349..7f482f63e 100644
--- a/test/functional/parser/PrctlParserTest.cpp
+++ b/test/functional/parser/PrctlParserTest.cpp
@@ -10,6 +10,11 @@
#include "storm-config.h"
#include "src/parser/PrctlParser.h"
#include "src/exceptions/WrongFormatException.h"
+#include "src/formula/actions/FormulaAction.h"
+#include "src/formula/actions/InvertAction.h"
+#include "src/formula/actions/SortAction.h"
+#include "src/formula/actions/RangeAction.h"
+#include "src/formula/actions/BoundAction.h"
namespace prctl = storm::property::prctl;
@@ -41,6 +46,35 @@ TEST(PrctlParserTest, parsePropositionalFormulaTest) {
ASSERT_EQ("(!(a & b) | (a & !c))", formula->toString());
}
+TEST(PrctlParserTest, parsePathFormulaTest) {
+ std::string input = "X( P<0.9 (a U b))";
+ std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
+ ASSERT_NO_THROW(
+ formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+ );
+
+ // The parser did not falsely recognize the input as a comment.
+ ASSERT_NE(formula, nullptr);
+
+ // The input was parsed correctly.
+ ASSERT_NE(std::dynamic_pointer_cast<prctl::Next<double>>(formula->getChild()).get(), nullptr);
+ auto nextFormula = std::dynamic_pointer_cast<prctl::Next<double>>(formula->getChild());
+ ASSERT_NE(std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(nextFormula->getChild()).get(), nullptr);
+ auto probBoundFormula = std::dynamic_pointer_cast<prctl::ProbabilisticBoundOperator<double>>(nextFormula->getChild());
+ ASSERT_NE(std::dynamic_pointer_cast<prctl::Until<double>>(probBoundFormula->getChild()).get(), nullptr);
+ auto untilFormula = std::dynamic_pointer_cast<prctl::Until<double>>(probBoundFormula->getChild());
+ ASSERT_NE(std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getLeft()).get(), nullptr);
+ ASSERT_NE(std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getRight()).get(), nullptr);
+ ASSERT_EQ("a", std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getLeft())->getAp());
+ ASSERT_EQ("b", std::dynamic_pointer_cast<prctl::Ap<double>>(untilFormula->getRight())->getAp());
+ ASSERT_EQ(0.9, probBoundFormula->getBound());
+ ASSERT_EQ(storm::property::LESS, probBoundFormula->getComparisonOperator());
+
+
+ // The string representation is also correct.
+ ASSERT_EQ("P = ? (X P < 0.900000 (a U b))", formula->toString());
+}
+
TEST(PrctlParserTest, parseProbabilisticFormulaTest) {
std::string input = "P > 0.5 [ F a ]";
std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
@@ -124,6 +158,45 @@ TEST(PrctlParserTest, parseComplexFormulaTest) {
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());
}
+TEST(PrctlParserTest, parsePrctlFilterTest) {
+ std::string input = "filter[formula(b); invert; bound(<, 0.5); sort(value); range(0,3)](F a)";
+ std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
+ ASSERT_NO_THROW(
+ formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+ );
+
+ // The parser did not falsely recognize the input as a comment.
+ ASSERT_NE(formula, nullptr);
+
+ ASSERT_EQ(5, formula->getActionCount());
+ ASSERT_NE(dynamic_cast<storm::property::action::FormulaAction<double>*>(formula->getAction(0)), nullptr);
+ ASSERT_NE(dynamic_cast<storm::property::action::InvertAction<double>*>(formula->getAction(1)), nullptr);
+ ASSERT_NE(dynamic_cast<storm::property::action::BoundAction<double>*>(formula->getAction(2)), nullptr);
+ ASSERT_NE(dynamic_cast<storm::property::action::SortAction<double>*>(formula->getAction(3)), nullptr);
+ ASSERT_NE(dynamic_cast<storm::property::action::RangeAction<double>*>(formula->getAction(4)), nullptr);
+
+ // The input was parsed correctly.
+ ASSERT_EQ("filter[formula(b); invert; bound(<, 0.500000); sort(value, ascending); range(0, 3)](F a)", formula->toString());
+}
+
+TEST(PrctlParserTest, commentTest) {
+ std::string input = "// This is a comment. And this is a commented out formula: R = ? [ F a ]";
+ std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);
+ ASSERT_NO_THROW(
+ formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+ );
+
+ // The parser recognized the input as a comment.
+ ASSERT_NE(nullptr, formula.get());
+
+ // Test if the parser recognizes the comment at the end of a line.
+ input = "R = ? [ F a ] // This is a comment.";
+ ASSERT_NO_THROW(
+ formula = storm::parser::PrctlParser::parsePrctlFormula(input)
+ );
+ ASSERT_EQ("R = ? (F a)", formula->toString());
+}
+
TEST(PrctlParserTest, wrongProbabilisticFormulaTest) {
std::shared_ptr<prctl::PrctlFilter<double>> formula(nullptr);