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

renamed factors for shielding to probabilities

tempestpy_adaptions
Stefan Pranger 3 years ago
parent
1d5eba326d
commit
9b6afac4d7
2 changed files with 30 additions and 28 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 56
      src/storm-parsers/parser/FormulaParserGrammar.cpp
  2. 2
      src/storm-parsers/parser/FormulaParserGrammar.h

56
src/storm-parsers/parser/FormulaParserGrammar.cpp
View File

@ -149,11 +149,11 @@ namespace storm {
qi::lit("Optimal")[qi::_val = storm::logic::ShieldingType::Optimal]) > -qi::lit("Shield"); qi::lit("Optimal")[qi::_val = storm::logic::ShieldingType::Optimal]) > -qi::lit("Shield");
shieldingType.name("shielding type"); shieldingType.name("shielding type");
multiplicativeFactor = qi::double_[qi::_pass = (qi::_1 >= 0) & (qi::_1 <= 1.0), qi::_val = qi::_1 ];
multiplicativeFactor.name("multiplicative factor between 0 and 1");
probability = qi::double_[qi::_pass = (qi::_1 >= 0) & (qi::_1 <= 1.0), qi::_val = qi::_1 ];
probability.name("double between 0 and 1");
shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] | shieldComparison = ((qi::lit("lambda")[qi::_a = storm::logic::ShieldComparison::Relative] |
qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > multiplicativeFactor)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)];
qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > probability)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)];
shieldComparison.name("shield comparison type"); shieldComparison.name("shield comparison type");
stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula); stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula);
@ -182,30 +182,30 @@ namespace storm {
start.name("start"); start.name("start");
// Enable the following lines to print debug output for most the rules. // Enable the following lines to print debug output for most the rules.
// debug(start);
// debug(constantDefinition);
// debug(stateFormula);
// debug(orStateFormula);
// debug(andStateFormula);
// debug(probabilityOperator);
// debug(rewardOperator);
// debug(longRunAverageOperator);
// debug(timeOperator);
// debug(pathFormulaWithoutUntil);
// debug(pathFormula);
// debug(conditionalFormula);
// debug(nextFormula);
// debug(globallyFormula);
// debug(eventuallyFormula);
// debug(atomicStateFormula);
// debug(booleanLiteralFormula);
// debug(labelFormula);
// debug(expressionFormula);
// debug(rewardPathFormula);
// debug(cumulativeRewardFormula);
// debug(totalRewardFormula);
// debug(instantaneousRewardFormula);
// debug(multiFormula);
//debug(start);
//debug(constantDefinition);
//debug(stateFormula);
//debug(orStateFormula);
//debug(andStateFormula);
//debug(probabilityOperator);
//debug(rewardOperator);
//debug(longRunAverageOperator);
//debug(timeOperator);
//debug(pathFormulaWithoutUntil);
//debug(pathFormula);
//debug(conditionalFormula);
//debug(nextFormula);
//debug(globallyFormula);
//debug(eventuallyFormula);
//debug(atomicStateFormula);
//debug(booleanLiteralFormula);
//debug(labelFormula);
//debug(expressionFormula);
//debug(rewardPathFormula);
//debug(cumulativeRewardFormula);
//debug(totalRewardFormula);
//debug(instantaneousRewardFormula);
//debug(multiFormula);
// Enable error reporting. // Enable error reporting.
qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
@ -514,8 +514,10 @@ namespace storm {
std::shared_ptr<storm::logic::ShieldExpression const> FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional<std::pair<storm::logic::ShieldComparison, double>> comparisonStruct) { std::shared_ptr<storm::logic::ShieldExpression const> FormulaParserGrammar::createShieldExpression(storm::logic::ShieldingType type, std::string name, boost::optional<std::pair<storm::logic::ShieldComparison, double>> comparisonStruct) {
if(comparisonStruct.is_initialized()) { if(comparisonStruct.is_initialized()) {
STORM_LOG_WARN_COND(type != storm::logic::ShieldingType::Optimal , "Comparison for optimal shield will be ignored.");
return std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(type, name, comparisonStruct.get().first, comparisonStruct.get().second)); return std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(type, name, comparisonStruct.get().first, comparisonStruct.get().second));
} else { } else {
STORM_LOG_THROW(type == storm::logic::ShieldingType::Optimal , storm::exceptions::WrongFormatException, "Construction of safety shield needs a comparison parameter (lambda or gamma)");
return std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(type, name)); return std::shared_ptr<storm::logic::ShieldExpression>(new storm::logic::ShieldExpression(type, name));
} }
} }

2
src/storm-parsers/parser/FormulaParserGrammar.h
View File

@ -207,7 +207,7 @@ namespace storm {
qi::rule<Iterator, std::shared_ptr<storm::logic::ShieldExpression const>(), Skipper> shieldExpression; qi::rule<Iterator, std::shared_ptr<storm::logic::ShieldExpression const>(), Skipper> shieldExpression;
qi::rule<Iterator, storm::logic::ShieldingType, Skipper> shieldingType; qi::rule<Iterator, storm::logic::ShieldingType, Skipper> shieldingType;
qi::rule<Iterator, double, Skipper> multiplicativeFactor;
qi::rule<Iterator, double, Skipper> probability;
qi::rule<Iterator, std::pair<storm::logic::ShieldComparison, double>, qi::locals<storm::logic::ShieldComparison>, Skipper> shieldComparison; qi::rule<Iterator, std::pair<storm::logic::ShieldComparison, double>, qi::locals<storm::logic::ShieldComparison>, Skipper> shieldComparison;
// Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).

Write Preview
Loading…
Cancel
Save