diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index 97fc467e5..bc094f197 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -5,6 +5,8 @@ #include "src/storage/jani/ParallelComposition.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/InvalidJaniException.h" + +#include "src/exceptions/NotSupportedException.h" #include "src/exceptions/NotImplementedException.h" #include "src/storage/jani/ModelType.h" @@ -49,7 +51,7 @@ namespace storm { } - std::pair> JaniParser::parse(std::string const& path) { + std::pair> JaniParser::parse(std::string const& path) { JaniParser parser; parser.readFile(path); return parser.parseModel(); @@ -75,7 +77,7 @@ namespace storm { file.close(); } - std::pair> JaniParser::parseModel(bool parseProperties) { + std::pair> JaniParser::parseModel(bool parseProperties) { //jani-version STORM_LOG_THROW(parsedStructure.count("jani-version") == 1, storm::exceptions::InvalidJaniException, "Jani-version must be given exactly once."); uint64_t version = getUnsignedInt(parsedStructure.at("jani-version"), "jani version"); @@ -121,17 +123,87 @@ namespace storm { std::shared_ptr composition = parseComposition(parsedStructure.at("system")); model.setSystemComposition(composition); STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given"); - PropertyVector properties; + std::map properties; if (parseProperties && parsedStructure.count("properties") == 1) { STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array"); for(auto const& propertyEntry : parsedStructure.at("properties")) { - properties.push_back(this->parseProperty(propertyEntry)); + try { + auto prop = this->parseProperty(propertyEntry); + properties.emplace(prop.getName(), prop); + } catch (storm::exceptions::NotSupportedException const& ex) { + STORM_LOG_WARN("Cannot handle property " << ex.what()); + } catch (storm::exceptions::NotImplementedException const& ex) { + STORM_LOG_WARN("Cannot handle property " << ex.what()); + } } } return {model, properties}; } + + std::vector> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context) { + STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << context); + return { parseFormula(propertyStructure.at("exp"), "Operand of operator " + opstring) }; + } + + + std::vector> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context) { + STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << context); + STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << context); + return { parseFormula(propertyStructure.at("left"), "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), "Operand of operator " + opstring) }; + } + + + std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, std::string const& context) { + storm::expressions::Expression expr = parseExpression(propertyStructure, "Expression in property", {}, true); + if(expr.isInitialized()) { + return std::make_shared(expr); + } else if(propertyStructure.count("op") == 1) { + std::string opString = getString(propertyStructure.at("op"), "Operation description"); + + if(opString == "Pmin" || opString == "Pmax") { + std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + assert(args.size() == 1); + storm::logic::OperatorInformation opInfo; + opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; + return std::make_shared(args[0], opInfo); + + } else if (opString == "∀" || opString == "∃") { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); + } else if (opString == "Emin" || opString == "Emax") { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Emin and Emax are currently not supported"); + } else if (opString == "Smin" || opString == "Smax") { + std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); + } else if (opString == "U") { + std::vector> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + if (propertyStructure.count("step-bounds") > 0) { + + } else if (propertyStructure.count("time-bounds") > 0) { + + } else if (propertyStructure.count("reward-bounds") > 0 ) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); + } + return std::make_shared(args[0], args[1]); + } else if (opString == "W") { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Weak until is not supported"); + } else if (opString == "∧" || opString == "∨") { + std::vector> args = parseBinaryFormulaArguments(propertyStructure, opString, ""); + assert(args.size() == 2); + storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; + return std::make_shared(oper, args[0], args[1]); + } else if (opString == "¬") { + std::vector> args = parseUnaryFormulaArgument(propertyStructure, opString, ""); + assert(args.size() == 1); + return std::make_shared(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); + + } + + } + + } + storm::jani::Property JaniParser::parseProperty(json const& propertyStructure) { STORM_LOG_THROW(propertyStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Property must have a name"); // TODO check unique name @@ -140,8 +212,46 @@ namespace storm { if (propertyStructure.count("comment") > 0) { comment = getString(propertyStructure.at("comment"), "comment for property named '" + name + "'."); } + STORM_LOG_THROW(propertyStructure.count("expression") == 1, storm::exceptions::InvalidJaniException, "Property must have an expression"); + // Parse filter expression. + json const& expressionStructure = propertyStructure.at("expression"); - + STORM_LOG_THROW(expressionStructure.count("op") == 1, storm::exceptions::InvalidJaniException, "Expression in property must have an operation description"); + STORM_LOG_THROW(expressionStructure.at("op") == "filter", storm::exceptions::InvalidJaniException, "Top level operation of a property must be a filter"); + STORM_LOG_THROW(expressionStructure.count("fun") == 1, storm::exceptions::InvalidJaniException, "Filter must have a function descritpion"); + std::string funDescr = getString(expressionStructure.at("fun"), "Filter function in property named " + name); + storm::jani::FilterType ft; + if (funDescr == "min") { + ft = storm::jani::FilterType::MIN; + } else if (funDescr == "max") { + ft = storm::jani::FilterType::MAX; + } else if (funDescr == "sum") { + ft = storm::jani::FilterType::SUM; + } else if (funDescr == "avg") { + ft = storm::jani::FilterType::AVG; + } else if (funDescr == "count") { + ft = storm::jani::FilterType::COUNT; + } else if (funDescr == "∀") { + ft = storm::jani::FilterType::FORALL; + } else if (funDescr == "∃") { + ft = storm::jani::FilterType::EXISTS; + } else if (funDescr == "argmin") { + ft = storm::jani::FilterType::ARGMIN; + } else if (funDescr == "argmax") { + ft = storm::jani::FilterType::ARGMAX; + } else if (funDescr == "values") { + ft = storm::jani::FilterType::VALUES; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown filter description " << funDescr << " in property named " << name); + } + + STORM_LOG_THROW(expressionStructure.count("states") == 1, storm::exceptions::InvalidJaniException, "Filter must have a states description"); + STORM_LOG_THROW(expressionStructure.at("states").is_string(), storm::exceptions::NotImplementedException, "We only support properties where the filter has a non-complex description of the states"); + std::string statesDescr = getString(expressionStructure.at("states"), "Filtered states in property named " + name); + STORM_LOG_THROW(statesDescr == "initial", storm::exceptions::NotImplementedException, "Only initial states are allowed as set of states we are interested in."); + STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); + auto formula = parseFormula(expressionStructure.at("values"), "Values of property " + name); + return storm::jani::Property(name, formula, comment); } std::shared_ptr JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) { @@ -236,7 +346,6 @@ namespace storm { boost::optional initVal; if(variableStructure.at("type").is_string()) { if(variableStructure.at("type") == "real") { - expressionManager->declareRationalVariable(name); if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { initVal = expressionManager->rational(defaultRationalInitialValue); @@ -247,7 +356,8 @@ namespace storm { return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); } - return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName), transientVar); + assert(!transientVar); + return std::make_shared(name, expressionManager->declareRationalVariable(exprManagerName)); } else if(variableStructure.at("type") == "bool") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { @@ -258,7 +368,8 @@ namespace storm { } return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar); } - return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName), transientVar); + assert(!transientVar); + return std::make_shared(name, expressionManager->declareBooleanVariable(exprManagerName)); } else if(variableStructure.at("type") == "int") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { @@ -323,14 +434,14 @@ namespace storm { STORM_LOG_THROW(expected == actual, storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects " << expected << " arguments, but got " << actual << " in " << errorInfo << "."); } - std::vector JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars); + std::vector JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, localVars,returnNoneInitializedOnUnknownOperator); return {left}; } - std::vector JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars); - storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, localVars); + std::vector JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); return {left, right}; } /** @@ -366,7 +477,7 @@ namespace storm { } } - storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars) { + storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars, bool returnNoneInitializedOnUnknownOperator) { if(expressionStructure.is_boolean()) { if(expressionStructure.get()) { return expressionManager->boolean(true); @@ -389,31 +500,50 @@ namespace storm { if(expressionStructure.count("op") == 1) { std::string opstring = getString(expressionStructure.at("op"), scopeDescription); std::vector arguments = {}; - if(opstring == "?:") { + if(opstring == "ite") { + STORM_LOG_THROW(expressionStructure.count("if") == 1, storm::exceptions::InvalidJaniException, "If operator required"); + STORM_LOG_THROW(expressionStructure.count("else") == 1, storm::exceptions::InvalidJaniException, "Else operator required"); + STORM_LOG_THROW(expressionStructure.count("then") == 1, storm::exceptions::InvalidJaniException, "If operator required"); + arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription)); + arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription)); + arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription)); ensureNumberOfArguments(3, arguments.size(), opstring, scopeDescription); assert(arguments.size() == 3); + ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::ite(arguments[0], arguments[1], arguments[2]); } else if (opstring == "∨") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] || arguments[1]; } else if (opstring == "∧") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] && arguments[1]; } else if (opstring == "⇒") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); - ensureBooleanType(arguments[0], opstring, 1, scopeDescription); + ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return (!arguments[0]) || arguments[1]; } else if (opstring == "¬") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); + if(!arguments[0].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return !arguments[0]; } else if (opstring == "=") { @@ -558,6 +688,9 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Opstring " + opstring + " is not supported by storm"); } else { + if(returnNoneInitializedOnUnknownOperator) { + return storm::expressions::Expression(); + } STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in " << scopeDescription << "."); } } diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index 8fa4e8277..1e87efe04 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -33,16 +33,16 @@ namespace storm { JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {} JaniParser(std::string const& jsonstring); - static std::pair parse(std::string const& path); + static std::pair> parse(std::string const& path); protected: void readFile(std::string const& path); - std::pair parseModel(bool parseProperties = true); + std::pair> parseModel(bool parseProperties = true); storm::jani::Property parseProperty(json const& propertyStructure); storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel); std::shared_ptr parseVariable(json const& variableStructure, std::string const& scopeDescription, bool prefWithScope = false); - storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>()); + storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>(), bool returnNoneOnUnknownOpString = false); private: std::shared_ptr parseConstant(json const& constantStructure, std::string const& scopeDescription = "global"); @@ -51,13 +51,19 @@ namespace storm { * Helper for parsing the actions of a model. */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); - std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}); - std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}); - + std::shared_ptr parseFormula(json const& propertyStructure, std::string const& context); + std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + + std::vector> parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context); + std::vector> parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context); + + + std::shared_ptr parseComposition(json const& compositionStructure); storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map> const& localVars = {}); - + /** * The overall structure currently under inspection. */ diff --git a/src/storage/jani/BooleanVariable.cpp b/src/storage/jani/BooleanVariable.cpp index 3eb63780b..ca2934f93 100644 --- a/src/storage/jani/BooleanVariable.cpp +++ b/src/storage/jani/BooleanVariable.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) { + BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) { // Intentionally left empty. } @@ -19,7 +19,8 @@ namespace storm { if (initValue) { return std::make_shared(name, variable, initValue.get(), transient); } else { - return std::make_shared(name, variable, transient); + assert(!transient); + return std::make_shared(name, variable); } } diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h index 7fe9603e0..7eeea85fd 100644 --- a/src/storage/jani/BooleanVariable.h +++ b/src/storage/jani/BooleanVariable.h @@ -11,7 +11,7 @@ namespace storm { /*! * Creates a Boolean variable with initial value */ - BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); + BooleanVariable(std::string const& name, storm::expressions::Variable const& variable); /*! * Creates a Boolean variable with initial value diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp index 37b458ba4..1d04c8166 100644 --- a/src/storage/jani/BoundedIntegerVariable.cpp +++ b/src/storage/jani/BoundedIntegerVariable.cpp @@ -13,11 +13,7 @@ namespace storm { // Intentionally left empty. } - BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable, transient), lowerBound(lowerBound), upperBound(upperBound) { - // Intentionally left empty. - } - - BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) { + BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) { // Intentionally left empty. } @@ -56,7 +52,8 @@ namespace storm { if (initValue) { return std::make_shared(name, variable, initValue.get(), transient, lowerBound.get(), upperBound.get()); } else { - return std::make_shared(name, variable, transient, lowerBound.get(), upperBound.get()); + assert(!transient); + return std::make_shared(name, variable, lowerBound.get(), upperBound.get()); } } } diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h index 733024b3d..9b5350d0e 100644 --- a/src/storage/jani/BoundedIntegerVariable.h +++ b/src/storage/jani/BoundedIntegerVariable.h @@ -16,10 +16,6 @@ namespace storm { * Creates a bounded integer variable with transient set to false and an initial value. */ BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); - /*! - * Creates a bounded integer variable without initial value. - */ - BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); /*! * Creates a bounded integer variable with transient set to false and no initial value. */ diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index e6c1e9d60..2eefbb774 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/src/storage/jani/JSONExporter.cpp @@ -140,7 +140,7 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const { - modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + modernjson::json opDecl(f.getLabel()); return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const{ @@ -152,7 +152,7 @@ namespace storm { return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const { - modernjson::json opDecl(f.isTrueFormula() ? "true" : "false"); + modernjson::json opDecl(f.isTrueFormula() ? true : false); return opDecl; } boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const { @@ -173,7 +173,7 @@ namespace storm { } boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const { - + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cummulative reward formulae"); } boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const { @@ -718,6 +718,7 @@ namespace storm { modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) { modernjson::json propDecl; propDecl["states"] = "initial"; + propDecl["op"] = "filter"; propDecl["fun"] = janiFilterTypeString(fe.getFilterType()); propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel); return propDecl; diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index bde51865e..be35820a4 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -31,6 +31,7 @@ namespace storm { class Property { + public: /** * Constructs the property * @param name the name diff --git a/src/storage/jani/RealVariable.cpp b/src/storage/jani/RealVariable.cpp index 8880a9a0a..f06e87a5c 100644 --- a/src/storage/jani/RealVariable.cpp +++ b/src/storage/jani/RealVariable.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : storm::jani::Variable(name, variable, transient) { + RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable) : storm::jani::Variable(name, variable) { // Intentionally left empty. } diff --git a/src/storage/jani/RealVariable.h b/src/storage/jani/RealVariable.h index 74c337ed9..1783b6fbf 100644 --- a/src/storage/jani/RealVariable.h +++ b/src/storage/jani/RealVariable.h @@ -10,7 +10,7 @@ namespace storm { /*! * Creates a real variable without initial value. */ - RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); + RealVariable(std::string const& name, storm::expressions::Variable const& variable); /*! * Creates a real variable with initial value. diff --git a/src/storage/jani/UnboundedIntegerVariable.cpp b/src/storage/jani/UnboundedIntegerVariable.cpp index c646b09b1..6b541054e 100644 --- a/src/storage/jani/UnboundedIntegerVariable.cpp +++ b/src/storage/jani/UnboundedIntegerVariable.cpp @@ -7,7 +7,7 @@ namespace storm { // Intentionally left empty. } - UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) { + UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable) { // Intentionally left empty. } diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp index 8551f14df..f2c7217ff 100644 --- a/src/storage/jani/Variable.cpp +++ b/src/storage/jani/Variable.cpp @@ -12,7 +12,7 @@ namespace storm { // Intentionally left empty. } - Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : name(name), variable(variable), transient(transient), init() { + Variable::Variable(std::string const& name, storm::expressions::Variable const& variable) : name(name), variable(variable), transient(false), init() { // Intentionally left empty. } diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h index cbbe4aa69..2eea79679 100644 --- a/src/storage/jani/Variable.h +++ b/src/storage/jani/Variable.h @@ -25,7 +25,7 @@ namespace storm { /*! * Creates a new variable without initial value construct. */ - Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient = false); + Variable(std::string const& name, storm::expressions::Variable const& variable); virtual ~Variable(); diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp index 65289382a..e3bc3c569 100644 --- a/src/storage/prism/ToJaniConverter.cpp +++ b/src/storage/prism/ToJaniConverter.cpp @@ -47,7 +47,7 @@ namespace storm { storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } } @@ -56,7 +56,7 @@ namespace storm { storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false)); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { - storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), false)); + storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } } @@ -100,7 +100,7 @@ namespace storm { std::vector transientLocationAssignments; for (auto const& rewardModel : program.getRewardModels()) { auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName()); - storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName(), newExpressionVariable, true)); + storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "defaultReward" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true)); if (rewardModel.hasStateRewards()) { storm::expressions::Expression transientLocationExpression; diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index d4fb44290..5e1b8104e 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -15,8 +15,8 @@ namespace storm { return program; } - std::pair> parseJaniModel(std::string const& path) { - std::pair> modelAndFormulae = storm::parser::JaniParser::parse(path); + std::pair> parseJaniModel(std::string const& path) { + std::pair> modelAndFormulae = storm::parser::JaniParser::parse(path); modelAndFormulae.first.checkValid(); return modelAndFormulae; } diff --git a/src/utility/storm.h b/src/utility/storm.h index c5df89d64..336d6e399 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -100,7 +100,7 @@ namespace storm { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } - std::pair> parseJaniModel(std::string const& path); + std::pair> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); std::vector> parseFormulasForExplicit(std::string const& inputString); std::vector> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program);