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

added filters to parsers

tempestpy_adaptions
dehnert 8 years ago
parent
ad2371fdae
commit
6b931497a2
5 changed files with 71 additions and 23 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. 22
      src/storm/cli/entrypoints.h
  2. 40
      src/storm/parser/FormulaParserGrammar.cpp
  3. 25
      src/storm/parser/FormulaParserGrammar.h
  4. 2
      src/storm/parser/PrismParser.cpp
  5. 5
      src/storm/storage/jani/Property.h

22
src/storm/cli/entrypoints.h
View File

@ -22,20 +22,20 @@ namespace storm {
if (result->isQuantitative()) {
switch (ft) {
case storm::modelchecker::FilterType::VALUES:
STORM_PRINT_AND_LOG(*result << std::endl);
return;
STORM_PRINT_AND_LOG(*result);
break;
case storm::modelchecker::FilterType::SUM:
STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().sum());
return;
break;
case storm::modelchecker::FilterType::AVG:
STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().average());
return;
break;
case storm::modelchecker::FilterType::MIN:
STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().getMin());
return;
break;
case storm::modelchecker::FilterType::MAX:
STORM_PRINT_AND_LOG(result->asQuantitativeCheckResult<ValueType>().getMax());
return;
break;
case storm::modelchecker::FilterType::ARGMIN:
case storm::modelchecker::FilterType::ARGMAX:
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Outputting states is not supported");
@ -48,16 +48,16 @@ namespace storm {
switch (ft) {
case storm::modelchecker::FilterType::VALUES:
STORM_PRINT_AND_LOG(*result << std::endl);
return;
break;
case storm::modelchecker::FilterType::EXISTS:
STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().existsTrue());
return;
break;
case storm::modelchecker::FilterType::FORALL:
STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().forallTrue());
return;
break;
case storm::modelchecker::FilterType::COUNT:
STORM_PRINT_AND_LOG(result->asQualitativeCheckResult().count());
return;
break;
case storm::modelchecker::FilterType::ARGMIN:
case storm::modelchecker::FilterType::ARGMAX:
@ -68,8 +68,8 @@ namespace storm {
case storm::modelchecker::FilterType::MAX:
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "FilterType only defined for quantitative results");
}
}
STORM_PRINT_AND_LOG(std::endl);
}
template<typename ValueType>

40
src/storm/parser/FormulaParserGrammar.cpp
View File

@ -125,7 +125,15 @@ namespace storm {
constantDefinition = (qi::lit("const") > qi::eps[qi::_a = true] > -(qi::lit("int") | qi::lit("double")[qi::_a = false]) >> identifier)[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a)];
constantDefinition.name("constant definition");
start = qi::eps > (((-formulaName >> stateFormula)[phoenix::bind(&FormulaParserGrammar::addProperty, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)] | qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition | qi::eps) % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses"
filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > -(qi::lit(",") > qi::lit("\"init\"") > qi::lit(")")))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterType, phoenix::ref(*this), qi::_1, qi::_2)];
filterProperty.name("filter property");
#pragma clang diagnostic pop
start = ((qi::eps > filterProperty[phoenix::push_back(qi::_val, qi::_1)] | qi::eps(phoenix::bind(&FormulaParserGrammar::areConstantDefinitionsAllowed, phoenix::ref(*this))) >> constantDefinition | qi::eps) % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
start.name("start");
// Enable the following lines to print debug output for most the rules.
@ -197,15 +205,6 @@ namespace storm {
addIdentifierExpression(name, newVariable);
}
void FormulaParserGrammar::addProperty(std::vector<storm::jani::Property>& properties, boost::optional<std::string> const& name, std::shared_ptr<storm::logic::Formula const> const& formula) {
if (name) {
properties.emplace_back(name.get(), formula);
} else {
properties.emplace_back(std::to_string(propertyCount), formula);
}
++propertyCount;
}
bool FormulaParserGrammar::areConstantDefinitionsAllowed() const {
return static_cast<bool>(manager);
}
@ -329,5 +328,26 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas) {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
}
storm::jani::Property FormulaParserGrammar::createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula) {
storm::jani::FilterExpression filterExpression(formula, filterType);
++propertyCount;
if (propertyName) {
return storm::jani::Property(propertyName.get(), filterExpression);
} else {
return storm::jani::Property(std::to_string(propertyCount -1 ), filterExpression);
}
}
storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterType(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula) {
++propertyCount;
if (propertyName) {
return storm::jani::Property(propertyName.get(), formula);
} else {
return storm::jani::Property(std::to_string(propertyCount), formula);
}
}
}
}

25
src/storm/parser/FormulaParserGrammar.h
View File

@ -9,6 +9,8 @@
#include "storm/logic/Formulas.h"
#include "storm/parser/ExpressionParser.h"
#include "storm/modelchecker/results/FilterType.h"
#include "storm/storage/expressions/ExpressionEvaluator.h"
namespace storm {
@ -111,6 +113,25 @@ namespace storm {
// A parser used for recognizing the reward measure types.
rewardMeasureTypeStruct rewardMeasureType_;
struct filterTypeStruct : qi::symbols<char, storm::modelchecker::FilterType> {
filterTypeStruct() {
add
("min", storm::modelchecker::FilterType::MIN)
("max", storm::modelchecker::FilterType::MAX)
("sum", storm::modelchecker::FilterType::SUM)
("avg", storm::modelchecker::FilterType::AVG)
("count", storm::modelchecker::FilterType::COUNT)
("forall", storm::modelchecker::FilterType::FORALL)
("exists", storm::modelchecker::FilterType::EXISTS)
("argmin", storm::modelchecker::FilterType::ARGMIN)
("argmax", storm::modelchecker::FilterType::ARGMAX)
("values", storm::modelchecker::FilterType::VALUES);
}
};
// A parser used for recognizing the filter type.
filterTypeStruct filterType_;
// The manager used to parse expressions.
std::shared_ptr<storm::expressions::ExpressionManager const> constManager;
std::shared_ptr<storm::expressions::ExpressionManager> manager;
@ -135,6 +156,7 @@ namespace storm {
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> timeOperator;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageOperator;
qi::rule<Iterator, storm::jani::Property(), Skipper> filterProperty;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simpleFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> stateFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormula;
@ -201,6 +223,9 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
std::shared_ptr<storm::logic::Formula const> createMultiObjectiveFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula);
storm::jani::Property createPropertyWithDefaultFilterType(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;

2
src/storm/parser/PrismParser.cpp
View File

@ -99,7 +99,7 @@ namespace storm {
definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedBooleanConstantDefinition.name("defined boolean constant declaration");
definedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedIntegerConstantDefinition = ((qi::lit("const") >> -qi::lit("int") >> identifier >> qi::lit("=")) > expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedIntegerConstantDefinition.name("defined integer constant declaration");
definedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)];

5
src/storm/storage/jani/Property.h
View File

@ -28,8 +28,9 @@ namespace storm {
class FilterExpression {
public:
explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {}
FilterExpression() = default;
explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : formula(formula), ft(ft) {}
std::shared_ptr<storm::logic::Formula const> const& getFormula() const {
return formula;
@ -60,6 +61,8 @@ namespace storm {
class Property {
public:
Property() = default;
/**
* Constructs the property
* @param name the name

Write Preview
Loading…
Cancel
Save