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

several improvements towards jani-property support 

Former-commit-id: 3d56f22d99 [formerly 1f527643ab]
Former-commit-id: 75e40a9b69
main
sjunges 9 years ago
parent
b18516668a
commit
3626c044d3
16 changed files with 189 additions and 54 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. 173
      src/parser/JaniParser.cpp
  2. 20
      src/parser/JaniParser.h
  3. 5
      src/storage/jani/BooleanVariable.cpp
  4. 2
      src/storage/jani/BooleanVariable.h
  5. 9
      src/storage/jani/BoundedIntegerVariable.cpp
  6. 4
      src/storage/jani/BoundedIntegerVariable.h
  7. 7
      src/storage/jani/JSONExporter.cpp
  8. 1
      src/storage/jani/Property.h
  9. 2
      src/storage/jani/RealVariable.cpp
  10. 2
      src/storage/jani/RealVariable.h
  11. 2
      src/storage/jani/UnboundedIntegerVariable.cpp
  12. 2
      src/storage/jani/Variable.cpp
  13. 2
      src/storage/jani/Variable.h
  14. 6
      src/storage/prism/ToJaniConverter.cpp
  15. 4
      src/utility/storm.cpp
  16. 2
      src/utility/storm.h

173
src/parser/JaniParser.cpp
View File

@ -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<storm::jani::Model, std::vector<storm::jani::Property>> JaniParser::parse(std::string const& path) {
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> JaniParser::parse(std::string const& path) {
JaniParser parser;
parser.readFile(path);
return parser.parseModel();
@ -75,7 +77,7 @@ namespace storm {
file.close();
}
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> JaniParser::parseModel(bool parseProperties) {
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> 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<storm::jani::Composition> 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<std::string, storm::jani::Property> 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<std::shared_ptr<storm::logic::Formula const>> 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<std::shared_ptr<storm::logic::Formula const>> 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<storm::logic::Formula const> 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<storm::logic::AtomicExpressionFormula>(expr);
} else if(propertyStructure.count("op") == 1) {
std::string opString = getString(propertyStructure.at("op"), "Operation description");
if(opString == "Pmin" || opString == "Pmax") {
std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::logic::ProbabilityOperatorFormula>(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<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, "");
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported");
} else if (opString == "U") {
std::vector<std::shared_ptr<storm::logic::Formula const>> 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<storm::logic::UntilFormula const>(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<std::shared_ptr<storm::logic::Formula const>> 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<storm::logic::BinaryBooleanStateFormula const>(oper, args[0], args[1]);
} else if (opString == "¬") {
std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, opString, "");
assert(args.size() == 1);
return std::make_shared<storm::logic::UnaryBooleanStateFormula const>(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<storm::jani::Constant> JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) {
@ -236,7 +346,6 @@ namespace storm {
boost::optional<storm::expressions::Expression> 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<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar);
}
return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), transientVar);
assert(!transientVar);
return std::make_shared<storm::jani::RealVariable>(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<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar);
}
return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), transientVar);
assert(!transientVar);
return std::make_shared<storm::jani::BooleanVariable>(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<storm::expressions::Expression> JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) {
storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars);
std::vector<storm::expressions::Expression> JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) {
storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, localVars,returnNoneInitializedOnUnknownOperator);
return {left};
}
std::vector<storm::expressions::Expression> JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> 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<storm::expressions::Expression> JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> 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<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) {
storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) {
if(expressionStructure.is_boolean()) {
if(expressionStructure.get<bool>()) {
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<storm::expressions::Expression> 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 << ".");
}
}

20
src/parser/JaniParser.h
View File

@ -33,16 +33,16 @@ namespace storm {
JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {}
JaniParser(std::string const& jsonstring);
static std::pair<storm::jani::Model, PropertyVector> parse(std::string const& path);
static std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parse(std::string const& path);
protected:
void readFile(std::string const& path);
std::pair<storm::jani::Model, PropertyVector> parseModel(bool parseProperties = true);
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> 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<storm::jani::Variable> 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<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>());
storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), bool returnNoneOnUnknownOpString = false);
private:
std::shared_ptr<storm::jani::Constant> 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<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, std::string const& context);
std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, std::string const& opstring, std::string const& context);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, std::string const& opstring, std::string const& context);
std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure);
storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {});
/**
* The overall structure currently under inspection.
*/

5
src/storage/jani/BooleanVariable.cpp
View File

@ -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<BooleanVariable>(name, variable, initValue.get(), transient);
} else {
return std::make_shared<BooleanVariable>(name, variable, transient);
assert(!transient);
return std::make_shared<BooleanVariable>(name, variable);
}
}

2
src/storage/jani/BooleanVariable.h
View File

@ -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

9
src/storage/jani/BoundedIntegerVariable.cpp
View File

@ -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<BoundedIntegerVariable>(name, variable, initValue.get(), transient, lowerBound.get(), upperBound.get());
} else {
return std::make_shared<BoundedIntegerVariable>(name, variable, transient, lowerBound.get(), upperBound.get());
assert(!transient);
return std::make_shared<BoundedIntegerVariable>(name, variable, lowerBound.get(), upperBound.get());
}
}
}

4
src/storage/jani/BoundedIntegerVariable.h
View File

@ -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.
*/

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

@ -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;

1
src/storage/jani/Property.h
View File

@ -31,6 +31,7 @@ namespace storm {
class Property {
public:
/**
* Constructs the property
* @param name the name

2
src/storage/jani/RealVariable.cpp
View File

@ -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.
}

2
src/storage/jani/RealVariable.h
View File

@ -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.

2
src/storage/jani/UnboundedIntegerVariable.cpp
View File

@ -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.
}

2
src/storage/jani/Variable.cpp
View File

@ -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.
}

2
src/storage/jani/Variable.h
View File

@ -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();

6
src/storage/prism/ToJaniConverter.cpp
View File

@ -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<storm::jani::Assignment> 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;

4
src/utility/storm.cpp
View File

@ -15,8 +15,8 @@ namespace storm {
return program;
}
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path) {
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(path);
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path) {
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(path);
modelAndFormulae.first.checkValid();
return modelAndFormulae;
}

2
src/utility/storm.h
View File

@ -100,7 +100,7 @@ namespace storm {
return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" );
}
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path);
std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path);
storm::prism::Program parseProgram(std::string const& path);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program);

Write Preview
Loading…
Cancel
Save