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

fixes in reach expression parsing for expected reward 

Former-commit-id: d9f5e887d8 [formerly 02cea9bff2]
Former-commit-id: dd387c2595
tempestpy_adaptions
sjunges 8 years ago
parent
42fccfeb08
commit
1fd89f3922
3 changed files with 26 additions and 22 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. 4
      src/parser/JaniParser.cpp
  2. 34
      src/storage/jani/JSONExporter.cpp
  3. 8
      src/storage/jani/JSONExporter.h

4
src/parser/JaniParser.cpp
View File

@ -223,7 +223,7 @@ namespace storm {
}
std::shared_ptr<storm::logic::Formula const> reach;
if (propertyStructure.count("reach") > 0) {
reach = parseFormula(propertyStructure.at("reach"), time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward, "Reach-expression of operator " + opString);
reach = std::make_shared<storm::logic::EventuallyFormula>(parseFormula(propertyStructure.at("reach"), time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward, "Reach-expression of operator " + opString));
} else {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Total reward is currently not supported");
}
@ -425,6 +425,8 @@ namespace storm {
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opString);
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Looking for operator for formula " << propertyStructure.dump() << ", but did not find one");
}
}

34
src/storage/jani/JSONExporter.cpp
View File

@ -139,8 +139,8 @@ namespace storm {
return iDecl;
}
modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, bool continuousTime) {
FormulaToJaniJson translator(continuousTime);
modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, storm::jani::Model const& model) {
FormulaToJaniJson translator(model);
return boost::any_cast<modernjson::json>(formula.accept(translator));
}
@ -334,35 +334,37 @@ namespace storm {
boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
std::vector<std::string> accvec;
if(continuous) {
accvec.push_back("time");
} else {
if(model.isDiscreteTimeModel()) {
accvec.push_back("steps");
} else {
accvec.push_back("time");
}
if(f.hasBound()) {
auto bound = f.getBound();
opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
if(f.hasOptimalityType()) {
opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none));
} else {
opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin";
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none));
}
opDecl["left"]["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT";
STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion");
opDecl["left"]["exp"] = f.getRewardModelName();
opDecl["left"]["accumulate"] = modernjson::json(accvec);
opDecl["right"] = numberToJson(bound.threshold);
} else {
if(f.hasOptimalityType()) {
opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none));
} else {
// TODO add checks
opDecl["op"] = "Emin";
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().asEventuallyFormula().getSubformula().accept(*this, boost::none));
}
opDecl["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT";
STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion");
opDecl["exp"] = f.getRewardModelName();
opDecl["accumulate"] = modernjson::json(accvec);
}
return opDecl;
@ -520,7 +522,7 @@ namespace storm {
}
JsonExporter exporter;
exporter.convertModel(janiModel);
exporter.convertProperties(formulas, !janiModel.isDiscreteTimeModel());
exporter.convertProperties(formulas, janiModel);
os << exporter.finalize().dump(4) << std::endl;
}
@ -732,23 +734,23 @@ namespace storm {
}
}
modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) {
modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, storm::jani::Model const& model) {
modernjson::json propDecl;
propDecl["states"]["op"] = "initial";
propDecl["op"] = "filter";
propDecl["fun"] = janiFilterTypeString(fe.getFilterType());
propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel);
propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), model);
return propDecl;
}
void JsonExporter::convertProperties( std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool continuousModel) {
void JsonExporter::convertProperties( std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::jani::Model const& model) {
std::vector<modernjson::json> properties;
uint64_t index = 0;
for(auto const& f : formulas) {
modernjson::json propDecl;
propDecl["name"] = "prop" + std::to_string(index);
propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), continuousModel);
propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), model);
++index;
properties.push_back(propDecl);
}

8
src/storage/jani/JSONExporter.h
View File

@ -35,7 +35,7 @@ namespace storm {
class FormulaToJaniJson : public storm::logic::FormulaVisitor {
public:
static modernjson::json translate(storm::logic::Formula const& formula, bool continuousTime);
static modernjson::json translate(storm::logic::Formula const& formula, storm::jani::Model const& modeln);
virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const;
@ -56,8 +56,8 @@ namespace storm {
virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const;
private:
FormulaToJaniJson(bool continuousModel) : continuous(continuousModel) { }
bool continuous;
FormulaToJaniJson(storm::jani::Model const& model) : model(model) { }
storm::jani::Model const& model;
};
class JsonExporter {
@ -69,7 +69,7 @@ namespace storm {
private:
void convertModel(storm::jani::Model const& model);
void convertProperties(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool timeContinuousModel);
void convertProperties(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::jani::Model const& model);
void appendVariableDeclaration(storm::jani::Variable const& variable);
modernjson::json finalize() {

Write Preview
Loading…
Cancel
Save