std::cout<<"Explored "<<numberOfExploredStates<<" states in "<<durationSinceStart<<" seconds (currently "<<statesPerSecond<<" states per second)."<<std::endl;
STORM_LOG_INFO("Preprocessing: "<<statesWithProbability01.first.getNonZeroCount()<<" states with probability 1, "<<statesWithProbability01.second.getNonZeroCount()<<" with probability 0 ("<<maybeStates.getNonZeroCount()<<" states remaining).");
// Check whether we need to compute exact probabilities for some states.
STORM_LOG_INFO("Preprocessing: "<<infinityStates.getNonZeroCount()<<" states with reward infinity, "<<targetStates.getNonZeroCount()<<" target states ("<<maybeStates.getNonZeroCount()<<" states remaining).");
// Check whether we need to compute exact rewards for some states.
STORM_LOG_INFO("Preprocessing: "<<statesWithProbability01.first.getNonZeroCount()<<" states with probability 1, "<<statesWithProbability01.second.getNonZeroCount()<<" with probability 0 ("<<maybeStates.getNonZeroCount()<<" states remaining).");
// Check whether we need to compute exact probabilities for some states.
if(qualitative){
// Set the values for all maybe-states to 0.5 to indicate that their probability values are neither 0 nor 1.
STORM_LOG_INFO("Preprocessing: "<<infinityStates.getNonZeroCount()<<" states with reward infinity, "<<targetStates.getNonZeroCount()<<" target states ("<<maybeStates.getNonZeroCount()<<" states remaining).");
// Check whether we need to compute exact rewards for some states.
if(qualitative){
// Set the values for all maybe-states to 1 to indicate that their reward values
STORM_LOG_THROW(storm::utility::isZero(resultsForNonMaybeStates[state]),storm::exceptions::IllegalArgumentException,"Expected that the result hint specifies probabilities in {0,1} for non-maybe states");
}
}
STORM_LOG_INFO("Preprocessing: "<<statesWithProbability1.getNumberOfSetBits()<<" states with probability 1 ("<<maybeStates.getNumberOfSetBits()<<" states remaining).");
}else{
// Get all states that have probability 0 and 1 of satisfying the until-formula.
STORM_LOG_INFO("Preprocessing: "<<statesWithProbability1.getNumberOfSetBits()<<" states with probability 1, "<<statesWithProbability0.getNumberOfSetBits()<<" with probability 0 ("<<maybeStates.getNumberOfSetBits()<<" states remaining).");
// Set values of resulting vector that are known exactly.
STORM_LOG_INFO("Preprocessing: "<<infinityStates.getNumberOfSetBits()<<" states with reward infinity, "<<targetStates.getNumberOfSetBits()<<" target states ("<<maybeStates.getNumberOfSetBits()<<" states remaining).");
STORM_LOG_INFO("Preprocessing: "<<qualitativeStateSets.statesWithProbability1.getNumberOfSetBits()<<" states with probability 1, "<<qualitativeStateSets.statesWithProbability0.getNumberOfSetBits()<<" with probability 0 ("<<qualitativeStateSets.maybeStates.getNumberOfSetBits()<<" states remaining).");
// Set values of resulting vector that are known exactly.
STORM_LOG_INFO("Preprocessing: "<<qualitativeStateSets.infinityStates.getNumberOfSetBits()<<" states with reward infinity, "<<targetStates.getNumberOfSetBits()<<" target states ("<<qualitativeStateSets.maybeStates.getNumberOfSetBits()<<" states remaining).");
STORM_LOG_INFO("Preprocessing: "<<statesWithProbability01.first.getNonZeroCount()<<" states with probability 1, "<<statesWithProbability01.second.getNonZeroCount()<<" with probability 0 ("<<maybeStates.getNonZeroCount()<<" states remaining).");
// Check whether we need to compute exact probabilities for some states.
STORM_LOG_INFO("Preprocessing: "<<infinityStates.getNonZeroCount()<<" states with reward infinity, "<<targetStates.getNonZeroCount()<<" target states ("<<maybeStates.getNonZeroCount()<<" states remaining).");
// Check whether we need to compute exact rewards for some states.
STORM_LOG_INFO("Preprocessing: "<<statesWithProbability01.first.getNonZeroCount()<<" states with probability 1, "<<statesWithProbability01.second.getNonZeroCount()<<" with probability 0 ("<<maybeStates.getNonZeroCount()<<" states remaining).");
// Check whether we need to compute exact probabilities for some states.
STORM_LOG_INFO("Preprocessing: "<<infinityStates.getNonZeroCount()<<" states with reward infinity, "<<targetStates.getNonZeroCount()<<" target states ("<<maybeStates.getNonZeroCount()<<" states remaining).");
// Check whether we need to compute exact rewards for some states.
if(qualitative){
// Set the values for all maybe-states to 1 to indicate that their reward values
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("hint","A regular expression to show help for all matching entities or 'all' for the complete help.").setDefaultValueString("all").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,versionOptionName,false,"Prints the version information.").build());
this->addOption(storm::settings::OptionBuilder(moduleName,verboseOptionName,false,"Enables more verbose output.").setShortName(verboseOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName,showProgressOptionName,false,"Sets when additional information (if available) about the progress is printed.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("delay","The delay to wait (in seconds) between emitting information (0 means never print progress).").setDefaultValueUnsignedInteger(5).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,precisionOptionName,false,"The internally used precision.").setShortName(precisionOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value","The precision to use.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0,1.0)).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,configOptionName,false,"If given, this file will be read and parsed for additional configuration settings.").setShortName(configOptionShortName)
this->addOption(storm::settings::OptionBuilder(moduleName,explorationOrderOptionName,false,"Sets which exploration order to use.").setShortName(explorationOrderOptionShortName)
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("name","The name of the exploration order to choose.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(explorationOrders)).setDefaultValueString("bfs").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,explorationChecksOptionName,false,"If set, additional checks (if available) are performed during model exploration to debug the model.").setShortName(explorationChecksOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName,explorationShowProgressOptionName,false,"Sets when additional information (if available) about the exploration progress is printed.").setShortName(explorationShowProgressOptionShortName).addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("delay","The delay to wait between emitting information.").setDefaultValueUnsignedInteger(0).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,transitionRewardsOptionName,false,"If given, the transition rewards are read from this file and added to the explicit model. Note that this requires the model to be given as an explicit model (i.e., via --"+explicitOptionName+").")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename","The file from which to read the transition rewards.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build());
STORM_LOG_WARN_COND(actualEquationSolver==EquationSolverType::Native,"Switching to native equation solver to guarantee soundness. To select other solvers, please explicitly specify a solver.");
STORM_LOG_INFO_COND(actualEquationSolver==EquationSolverType::Native,"Switching to native equation solver to guarantee soundness. To select other solvers, please explicitly specify a solver.");
}else{
STORM_LOG_WARN_COND(actualEquationSolver==EquationSolverType::Native,"Switching to native equation solver from explicitly selected solver '"<<storm::solver::toString(actualEquationSolver)<<"' to guarantee soundness.");
STORM_LOG_INFO_COND(actualEquationSolver==EquationSolverType::Native,"Switching to native equation solver from explicitly selected solver '"<<storm::solver::toString(actualEquationSolver)<<"' to guarantee soundness.");
STORM_LOG_WARN("Selecting policy iteration as the solution method to guarantee exact results. If you want to override this, please explicitly specify a different method.");
STORM_LOG_INFO("Selecting policy iteration as the solution method to guarantee exact results. If you want to override this, please explicitly specify a different method.");
dehnert
7 years ago