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(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"),"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"),"Operand of operator "+opstring),parseFormula(propertyStructure.at("right"),"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(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");
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"),"Values of property "+name);
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);
this->addOption(storm::settings::OptionBuilder(moduleName,prismCompatibilityOptionName,false,"Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build());
@ -60,7 +64,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());
sjunges
8 years ago