@ -194,43 +221,42 @@ int main(const int argc, const char** argv) {
#endif
// Set min or max
boolminimal=true;
std::stringoptimizationDirection="min";
if(dftSettings.isComputeMaximalValue()){
STORM_LOG_THROW(!dftSettings.isComputeMinimalValue(),storm::exceptions::InvalidSettingsException,"Cannot compute minimal and maximal values at the same time.");
minimal=false;
optimizationDirection="max";
}
// Construct pctlFormula
std::stringpctlFormula="";
std::stringoperatorType="";
std::stringtargetFormula="";
// Construct properties to check for
std::vector<std::string>properties;
if(ioSettings.isPropertySet()){
STORM_LOG_THROW(!dftSettings.usePropExpectedTime()&&!dftSettings.usePropProbability()&&!dftSettings.usePropTimebound(),storm::exceptions::InvalidSettingsException,"More than one property given.");
pctlFormula=ioSettings.getProperty();
}elseif(dftSettings.usePropExpectedTime()){
STORM_LOG_THROW(!dftSettings.usePropProbability()&&!dftSettings.usePropTimebound(),storm::exceptions::InvalidSettingsException,"More than one property given.");
operatorType="T";
targetFormula="F \"failed\"";
}elseif(dftSettings.usePropProbability()){
STORM_LOG_THROW(!dftSettings.usePropTimebound(),storm::exceptions::InvalidSettingsException,"More than one property given.");
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc),storm::exceptions::NotSupportedException,"Parallel composition only applicable for CTMCs");
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc),storm::exceptions::NotSupportedException,"Parallel composition only applicable for CTMCs");
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc),storm::exceptions::NotSupportedException,"Parallel composition only applicable for CTMCs");
STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Ctmc),storm::exceptions::NotSupportedException,"Parallel composition only applicable for CTMCs");
STORM_LOG_ASSERT((formula->isTimeOperatorFormula()&&!probabilityFormula)||(!formula->isTimeOperatorFormula()&&probabilityFormula),"Probability formula not initialized correctly");
// TODO Matthias: compute approximation for all properties simultaneously?
STORM_LOG_ASSERT((property->isTimeOperatorFormula()&&!probabilityFormula)||(!property->isTimeOperatorFormula()&&probabilityFormula),"Probability formula not initialized correctly");
size_titeration=0;
do{
// Iteratively build finer models
@ -310,32 +303,30 @@ namespace storm {
// Build model for lower bound
STORM_LOG_INFO("Getting model for lower bound...");
STORM_LOG_ASSERT(iteration==0||!comparator.isLess(newResult,approxResult.first),"New under-approximation "<<newResult<<" is smaller than old result "<<approxResult.first);
approxResult.first=newResult;
// Check lower bounds
newResult=checkModel(model,{property});
STORM_LOG_ASSERT(newResult.size()==1,"Wrong size for result vector.");
STORM_LOG_ASSERT(iteration==0||!comparator.isLess(newResult[0],approxResult.first),"New under-approximation "<<newResult[0]<<" is smaller than old result "<<approxResult.first);
approxResult.first=newResult[0];
// Build model for upper bound
STORM_LOG_INFO("Getting model for upper bound...");
STORM_LOG_ASSERT(iteration==0||!comparator.isLess(approxResult.second,newResult),"New over-approximation "<<newResult<<" is greater than old result "<<approxResult.second);
approxResult.second=newResult;
newResult=checkModel(model,{property});
STORM_LOG_ASSERT(newResult.size()==1,"Wrong size for result vector.");
STORM_LOG_ASSERT(iteration==0||!comparator.isLess(approxResult.second,newResult[0]),"New over-approximation "<<newResult[0]<<" is greater than old result "<<approxResult.second);
approxResult.second=newResult[0];
++iteration;
STORM_LOG_ASSERT(comparator.isLess(approxResult.first,approxResult.second)||comparator.isEqual(approxResult.first,approxResult.second),"Under-approximation "<<approxResult.first<<" is greater than over-approximation "<<approxResult.second);
STORM_LOG_INFO("Result after iteration "<<iteration<<": ("<<std::setprecision(10)<<approxResult.first<<", "<<approxResult.second<<")");
STORM_LOG_THROW((std::is_same<ValueType,storm::RationalFunction>::value),storm::exceptions::NotSupportedException,"Parameters only allowed when using rational functions.");
this->addOption(storm::settings::OptionBuilder(moduleName,symmetryReductionOptionName,false,"Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName,modularisationOptionName,false,"Use modularisation (not applicable for expected time).").build());
this->addOption(storm::settings::OptionBuilder(moduleName,disableDCOptionName,false,"Disable Dont Care propagation.").build());
this->addOption(storm::settings::OptionBuilder(moduleName,firstDependencyOptionName,false,"Avoid non-determinism by always taking the first possible dependency.").build());
this->addOption(storm::settings::OptionBuilder(moduleName,approximationErrorOptionName,false,"Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error","The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,approximationHeuristicOptionName,false,"Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic","Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth","rateratio"})).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,propExpectedTimeOptionName,false,"Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName,propProbabilityOptionName,false,"Compute probability of system failure.").build());
this->addOption(storm::settings::OptionBuilder(moduleName,propTimeBoundOptionName,false,"Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time","The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,propTimeboundOptionName,false,"Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time","The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,propTimepointsOptionName,false,"Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime","The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime","The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc","The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,minValueOptionName,false,"Compute minimal value in case of non-determinism.").build());
this->addOption(storm::settings::OptionBuilder(moduleName,maxValueOptionName,false,"Compute maximal value in case of non-determinism.").build());
#ifdef STORM_HAVE_Z3
this->addOption(storm::settings::OptionBuilder(moduleName,solveWithSmtOptionName,true,"Solve the DFT with SMT.").build());
#endif
this->addOption(storm::settings::OptionBuilder(moduleName,transformToGspnOptionName,false,"Transform DFT to GSPN.").build());
this->addOption(storm::settings::OptionBuilder(moduleName,exportToJsonOptionName,false,"Export the model to the Cytoscape JSON format.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename","The name of the JSON file to export to.").build()).build());
STORM_LOG_THROW(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(settings.isExplicitSet(),storm::exceptions::InvalidStateException,"Unable to build explicit model without model files.");
STORM_LOG_THROW(settings.isExplicitSet()||settings.isExplicitDRNSet(),storm::exceptions::InvalidStateException,"Unable to build explicit model without model files.");
STORM_LOG_THROW(settings.isExplicitSet()||settings.isExplicitDRNSet(),storm::exceptions::InvalidStateException,"Unable to build explicit model without model files.");
//STORM_LOG_THROW((std::is_same<ValueType, storm::RationalFunction>::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions.");
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.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build())
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("labeling filename","The name of the file from which to read the state labeling.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,explicitDrnOptionName,false,"Parses the model given in the DRN format.").setShortName(explicitDrnOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("drn filename","The name of the DRN file containing the model.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build())
.build());
this->addOption(storm::settings::OptionBuilder(moduleName,prismInputOptionName,false,"Parses the model given in the PRISM format.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename","The name of the file from which to read the PRISM input.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,janiInputOptionName,false,"Parses the model given in the JANI format.")
// Ensure that not two symbolic input models were given.
STORM_LOG_THROW(!isJaniInputSet()||!isPrismInputSet(),storm::exceptions::InvalidSettingsException,"Symbolic model ");
// Ensure that not two explicit input models were given.
STORM_LOG_THROW(!isExplicitSet()||!isExplicitDRNSet(),storm::exceptions::InvalidSettingsException,"Explicit model ");
// Ensure that the model was given either symbolically or explicitly.
STORM_LOG_THROW(!isJaniInputSet()||!isPrismInputSet()||!isExplicitSet(),storm::exceptions::InvalidSettingsException,"The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both.");
STORM_LOG_THROW(!isJaniInputSet()||!isPrismInputSet()||!isExplicitSet()||!isExplicitDRNSet(),storm::exceptions::InvalidSettingsException,"The model may be either given in an explicit or a symbolic format (PRISM or JANI), but not both.");
// Make sure PRISM-to-JANI conversion is only set if the actual input is in PRISM format.
STORM_LOG_THROW(!isPrismToJaniSet()||isPrismInputSet(),storm::exceptions::InvalidSettingsException,"For the transformation from PRISM to JANI, the input model must be given in the prism format.");
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.
Matthias Volk
8 years ago