STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine()==storm::settings::modules::CoreSettings::Engine::Sparse,storm::exceptions::InvalidSettingsException,"Only the sparse engine supports explicit model input.");
// If the model is given in an explicit format, we parse the properties without allowing expressions
STORM_LOG_THROW(model->getType()==storm::models::ModelType::Dtmc||model->getType()==storm::models::ModelType::Ctmc,storm::exceptions::InvalidSettingsException,"Currently parametric verification is only available for DTMCs and CTMCs.");
STORM_LOG_THROW(model.isPrismProgram(),storm::exceptions::InvalidSettingsException,"Exploration engine is currently only applicable to PRISM models.");
STORM_LOG_THROW(program.getModelType()==storm::prism::Program::ModelType::DTMC||program.getModelType()==storm::prism::Program::ModelType::MDP,storm::exceptions::InvalidSettingsException,"Currently exploration-based verification is only available for DTMCs and MDPs.");
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine()==storm::settings::modules::CoreSettings::Engine::Sparse,storm::exceptions::InvalidSettingsException,"Cannot use this data type with an engine different than the sparse one.");
STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine()==storm::settings::modules::CoreSettings::Engine::Sparse,storm::exceptions::InvalidSettingsException,"Cannot use this data type with an engine different than the sparse one.");
STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(),storm::exceptions::InvalidOperationException,"Cannot filter symbolic check result with non-symbolic filter.");
STORM_LOG_THROW(parsedStructure.at("restrict-initial").count("exp")==1,storm::exceptions::InvalidJaniException,"Model needs an expression inside the initial restricion");
initialValueRestriction=parseExpression(parsedStructure.at("restrict-initial").at("exp"),"Initial value restriction for automaton "+name);
STORM_LOG_THROW(propertyStructure.count("exp")==1,storm::exceptions::InvalidJaniException,"Expecting operand for operator "<<opstring<<" in "<<context);
return{parseFormula(propertyStructure.at("exp"),formulaContext,"Operand of operator "+opstring)};
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"),formulaContext,"Operand of operator "+opstring),parseFormula(propertyStructure.at("right"),formulaContext,"Operand of operator "+opstring)};
pi.lowerBound=parseExpression(piStructure.at("lower"),"Lower bound for property interval");
// TODO substitute constants.
STORM_LOG_THROW(!pi.lowerBound.containsVariables(),storm::exceptions::NotSupportedException,"Only constant expressions are supported as lower bounds");
}
if(piStructure.count("lower-exclusive")>0){
STORM_LOG_THROW(pi.lowerBound.isInitialized(),storm::exceptions::InvalidJaniException,"Lower-exclusive can only be set if a lower bound is present");
pi.upperBound=parseExpression(piStructure.at("upper"),"Upper bound for property interval");
// TODO substitute constants.
STORM_LOG_THROW(!pi.upperBound.containsVariables(),storm::exceptions::NotSupportedException,"Only constant expressions are supported as upper bounds");
}
if(piStructure.count("upper-exclusive")>0){
STORM_LOG_THROW(pi.lowerBound.isInitialized(),storm::exceptions::InvalidJaniException,"Lower-exclusive can only be set if a lower bound is present");
STORM_LOG_THROW(pi.lowerBound.isInitialized()||pi.upperBound.isInitialized(),storm::exceptions::InvalidJaniException,"Bounded operators must be bounded");
STORM_LOG_THROW(false,storm::exceptions::NotImplementedException,"Forall and Exists are currently not supported");
}elseif(opString=="Emin"||opString=="Emax"){
booltime=false;
STORM_LOG_THROW(propertyStructure.count("exp")==1,storm::exceptions::InvalidJaniException,"Expecting reward-expression for operator "<<opString<<" in "<<context);
storm::expressions::ExpressionrewExpr=parseExpression(propertyStructure.at("exp"),"Reward expression in "+context);
if(rewExpr.isVariable()){
time=false;
}else{
time=true;
}
std::shared_ptr<storm::logic::Formulaconst>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);
}else{
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Total reward is currently not supported");
STORM_LOG_THROW(false,storm::exceptions::InvalidJaniException,"One may only accumulate either 'steps' or 'time', got "<<accEntry.dump()<<" in "<<context);
}
}
}
STORM_LOG_THROW(!(accTime&&accSteps),storm::exceptions::NotSupportedException,"Storm does not allow to accumulate over both time and steps");
if(propertyStructure.count("step-instant")>0){
storm::expressions::ExpressionstepInstantExpr=parseExpression(propertyStructure.at("step-instant"),"Step instant in "+context);
STORM_LOG_THROW(!stepInstantExpr.containsVariables(),storm::exceptions::NotSupportedException,"Storm only allows constant step-instants");
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Instant/Cumul. Reward for reward constraints not supported currently.");
}
//STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given.");
STORM_LOG_THROW(pi.hasUpperBound(),storm::exceptions::NotSupportedException,"Storm only supports step-bounded until with an upper bound");
if(pi.hasLowerBound()){
STORM_LOG_THROW(pi.lowerBound.evaluateAsInt()==0,storm::exceptions::NotSupportedException,"Storm only supports step-bounded until without a (non-trivial) lower-bound");
}
int64_tupperBound=pi.upperBound.evaluateAsInt();
if(pi.upperBoundStrict){
upperBound--;
}
STORM_LOG_THROW(upperBound>=0,storm::exceptions::InvalidJaniException,"Step-bounds cannot be negative");
std::vector<std::shared_ptr<storm::logic::Formulaconst>>args=parseUnaryFormulaArgument(propertyStructure,formulaContext,opString,"Subformula of globally operator "+context);
if(propertyStructure.count("step-bounds")>0){
STORM_LOG_THROW(false,storm::exceptions::NotSupportedException,"Globally and step-bounds are not supported currently");
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::stringfunDescr=getString(expressionStructure.at("fun"),"Filter function in property named "+name);
storm::modelchecker::FilterTypeft;
if(funDescr=="min"){
ft=storm::modelchecker::FilterType::MIN;
}elseif(funDescr=="max"){
ft=storm::modelchecker::FilterType::MAX;
}elseif(funDescr=="sum"){
ft=storm::modelchecker::FilterType::SUM;
}elseif(funDescr=="avg"){
ft=storm::modelchecker::FilterType::AVG;
}elseif(funDescr=="count"){
ft=storm::modelchecker::FilterType::COUNT;
}elseif(funDescr=="∀"){
ft=storm::modelchecker::FilterType::FORALL;
}elseif(funDescr=="∃"){
ft=storm::modelchecker::FilterType::EXISTS;
}elseif(funDescr=="argmin"){
ft=storm::modelchecker::FilterType::ARGMIN;
}elseif(funDescr=="argmax"){
ft=storm::modelchecker::FilterType::ARGMAX;
}elseif(funDescr=="values"){
ft=storm::modelchecker::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").count("op")>0,storm::exceptions::NotImplementedException,"We only support properties where the filter has initial states");
std::stringstatesDescr=getString(expressionStructure.at("states").at("op"),"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");
autoformula=parseFormula(expressionStructure.at("values"),storm::logic::FormulaContext::Undefined,"Values of property "+name);
initVal=parseExpression(variableStructure.at("initial-value"),"Initial value for variable "+name+" (scope: "+scopeDescription+") ");
STORM_LOG_THROW(initVal.get().hasBooleanType(),storm::exceptions::InvalidJaniException,"Initial value for integer variable "+name+"(scope "+scopeDescription+") should be a Boolean");
STORM_LOG_THROW(expected==actual,storm::exceptions::InvalidJaniException,"Operator "<<opstring<<" expects "<<expected<<" arguments, but got "<<actual<<" in "<<errorInfo<<".");
storm::expressions::Expressionleft=parseExpression(expressionDecl.at("exp"),"Argument of operator "+opstring+" in "+scopeDescription,localVars,returnNoneInitializedOnUnknownOperator);
storm::expressions::Expressionleft=parseExpression(expressionDecl.at("left"),"Left argument of operator "+opstring+" in "+scopeDescription,localVars);
storm::expressions::Expressionright=parseExpression(expressionDecl.at("right"),"Right argument of operator "+opstring+" in "+scopeDescription,localVars);
storm::expressions::Expressionleft=parseExpression(expressionDecl.at("left"),"Left argument of operator "+opstring+" in "+scopeDescription,localVars,returnNoneInitializedOnUnknownOperator);
storm::expressions::Expressionright=parseExpression(expressionDecl.at("right"),"Right argument of operator "+opstring+" in "+scopeDescription,localVars,returnNoneInitializedOnUnknownOperator);
STORM_LOG_THROW(assignmentDeclCount<2,storm::exceptions::InvalidJaniException,"Destination in edge from '"<<sourceLoc<<"' to '"<<targetLoc<<"' in automaton '"<<name<<"' has multiple assignment lists");
STORM_LOG_THROW(assignmentEntry.count("ref")==1,storm::exceptions::InvalidJaniException,"Assignment in edge from '"<<sourceLoc<<"' to '"<<targetLoc<<"' in automaton '"<<name<<"' must have one ref field");
std::stringrefstring=getString(assignmentEntry.at("ref"),"assignment in edge from '"+sourceLoc+"' to '"+targetLoc+"' in automaton '"+name+"'");
storm::jani::Variableconst&lhs=getLValue(refstring,parentModel.getGlobalVariables(),automaton.getVariables(),"Assignment variable in edge from '"+sourceLoc+"' to '"+targetLoc+"' in automaton '"+name+"'");
// value
STORM_LOG_THROW(assignmentEntry.count("value")==1,storm::exceptions::InvalidJaniException,"Assignment in edge from '"<<sourceLoc<<"' to '"<<targetLoc<<"' in automaton '"<<name<<"' must have one value field");
storm::expressions::ExpressionassignmentExpr=parseExpression(assignmentEntry.at("value"),"assignment in edge from '"+sourceLoc+"' to '"+targetLoc+"' in automaton '"+name+"'",localVars);
STORM_LOG_THROW(assignmentEntry.count("ref")==1,storm::exceptions::InvalidJaniException,"Assignment in edge from '"<<sourceLoc<<"' to '"<<targetLoc<<"' in automaton '"<<name<<"' must have one ref field");
std::stringrefstring=getString(assignmentEntry.at("ref"),"assignment in edge from '"+sourceLoc+"' to '"+targetLoc+"' in automaton '"+name+"'");
storm::jani::Variableconst&lhs=getLValue(refstring,parentModel.getGlobalVariables(),automaton.getVariables(),"Assignment variable in edge from '"+sourceLoc+"' to '"+targetLoc+"' in automaton '"+name+"'");
// value
STORM_LOG_THROW(assignmentEntry.count("value")==1,storm::exceptions::InvalidJaniException,"Assignment in edge from '"<<sourceLoc<<"' to '"<<targetLoc<<"' in automaton '"<<name<<"' must have one value field");
storm::expressions::ExpressionassignmentExpr=parseExpression(assignmentEntry.at("value"),"assignment in edge from '"+sourceLoc+"' to '"+targetLoc+"' in automaton '"+name+"'",localVars);
this->addOption(storm::settings::OptionBuilder(moduleName,prismCompatibilityOptionName,false,"Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName,exportDotOptionName,"","If given, the loaded model will be written to the specified file in the dot format.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename","The name of the file to which the model is to be written.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,exportMatOptionName,"","If given, the loaded model will be written to the specified file in the mat format.")
this->addOption(storm::settings::OptionBuilder(moduleName,exportExplicitOptionName,"","If given, the loaded model will be written to the specified file in the drn format.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename","the name of the file to which the model is to be writen.").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,explicitOptionName,false,"Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename","The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build())
@ -44,6 +50,8 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName,janiInputOptionName,false,"Parses the model given in the JANI format.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename","The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,prismToJaniOptionName,false,"If set, the input PRISM model is transformed to JANI.").build());
this->addOption(storm::settings::OptionBuilder(moduleName,fullModelBuildOptionName,false,"If set, include all rewards and labels.").build());
this->addOption(storm::settings::OptionBuilder(moduleName,noBuildOptionName,false,"If set, do not build the model.").build());
this->addOption(storm::settings::OptionBuilder(moduleName,explorationOrderOptionName,false,"Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
@ -57,6 +65,8 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename","The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,constantsOptionName,false,"Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --"+prismInputOptionName+" or --"+janiInputOptionName+").").setShortName(constantsOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("values","A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,janiPropertyOptionName,false,"Specifies the properties from the jani model (given by --"+janiInputOptionName+") to be checked.").setShortName(janiPropertyOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("values","A comma separated list of properties to be checked").setDefaultValueString("").build()).build());
STORM_LOG_WARN("This format only supports discrete time models");
embedded=true;
}
STORM_LOG_THROW(embedded||sparseModel->getType()==storm::models::ModelType::Mdp||sparseModel->getType()==storm::models::ModelType::Dtmc,storm::exceptions::NotImplementedException,"This functionality is not yet implemented.");
std::vector<ValueType>exitRates;// Only for CTMCs and MAs.
sjunges
9 years ago
xxxxxxxxxx