)[qi::_val=phoenix::bind(&PrismParser::createDefinedIntegerConstant,phoenix::ref(*this),qi::_1,qi::_2)];// '>>' before freshIdentifier because of the optional 'int'. Otherwise, undefined constant 'const bool b;' would not parse.
undefinedConstantDefinition=(undefinedBooleanConstantDefinition|undefinedDoubleConstantDefinition|undefinedIntegerConstantDefinition);// Due to the 'const N;' syntax, it is important to have integer constants last
// In the second run, we actually need to parse the commands instead of just skipping them,
// so we adapt the rule for parsing commands.
STORM_LOG_THROW(observables.empty(),storm::exceptions::WrongFormatException,"Some variables marked as observable, but never declared, e.g. "<<*observables.begin());
STORM_LOG_THROW(formulas.size()==this->formulaExpressions.size(),storm::exceptions::UnexpectedException,"Unexpected number of formulas and formula expressions");
this->formulaOrder.clear();
@ -397,30 +415,30 @@ namespace storm {
STORM_LOG_THROW(false,storm::exceptions::WrongFormatException,"Unable to parse expression for formula '"<<formulas[unprocessed.getNextSetIndex(0)].getName()<<"'.");
STORM_LOG_THROW(!globalProgramInformation.hasInitialConstruct,storm::exceptions::WrongFormatException,"Parsing error in "<<this->getFilename()<<": Program must not define two initial constructs.");
STORM_LOG_THROW(globalProgramInformation.modelType==storm::prism::Program::ModelType::UNDEFINED,storm::exceptions::WrongFormatException,"Parsing error in "<<this->getFilename()<<": Program must not set model type multiple times.");
STORM_LOG_ASSERT(moduleIndexPair!=globalProgramInformation.moduleToIndexMap.end(),"Parsing error in "<<this->getFilename()<<" for player "<<playerName<<": No module named '"<<moduleName<<"' present.");
STORM_LOG_THROW(moduleNotYetControlled,storm::exceptions::WrongFormatException,"Parsing error in "<<this->getFilename()<<" for player "<<playerName<<": Module '"<<moduleName<<"' already controlled by another player.");
STORM_LOG_ASSERT(actionIndexPair!=globalProgramInformation.actionIndices.end(),"Parsing error in "<<this->getFilename()<<" for player "<<playerName<<": No action named '"<<actionName<<"' present.");
STORM_LOG_THROW(actionNotYetControlled,storm::exceptions::WrongFormatException,"Parsing error in "<<this->getFilename()<<" for player "<<playerName<<": Command '"<<actionName<<"' already controlled by another player.");
// Assert that the module name is already known and has the expected index.
STORM_LOG_ASSERT(!this->secondRun||globalProgramInformation.moduleToIndexMap.count(moduleName)>0,"Module name '"<<moduleName<<"' was not found.");
STORM_LOG_ASSERT(!this->secondRun||globalProgramInformation.moduleToIndexMap[moduleName]==globalProgramInformation.modules.size(),"The index for module '"<<moduleName<<"' does not match the index from the first parsing run.");
STORM_LOG_THROW(moduleIndexPair!=globalProgramInformation.moduleToIndexMap.end(),storm::exceptions::WrongFormatException,"Parsing error in "<<this->getFilename()<<": No module named '"<<oldModuleName<<"' to rename.");
STORM_LOG_THROW(!moduleToRename.isRenamedFromModule(),storm::exceptions::WrongFormatException,"Parsing error in "<<this->getFilename()<<": The module '"<<newModuleName<<"' can not be created from module '"<<oldModuleName<<"' through module renaming because '"<<oldModuleName<<"' is also a renamed module. Create '"<<newModuleName<<"' via a renaming from base module '"<<moduleToRename.getBaseModule()<<"' instead.");
autoconst&renaming=moduleRenaming.getRenaming();
if(!this->secondRun){
// Add a mapping from the new module name to its (future) index.
// Assert that the module name is already known and has the expected index.
STORM_LOG_ASSERT(globalProgramInformation.moduleToIndexMap.count(newModuleName)>0,"Module name '"<<newModuleName<<"' was not found.");
STORM_LOG_ASSERT(globalProgramInformation.moduleToIndexMap[newModuleName]==globalProgramInformation.modules.size(),"The index for module "<<newModuleName<<" does not match the index from the first parsing run.");
// Create a mapping from identifiers to the expressions they need to be replaced with.
STORM_LOG_THROW(!this->stateStorage.initialStateIndices.empty(),storm::exceptions::WrongFormatException,"The model does not have a single initial state.");
STORM_LOG_ASSERT(firstChoiceOfState||stateAndChoiceInformationBuilder.hasStatePlayerIndicationBeenSet(choice.getPlayerIndex(),currentRowGroup),"There is a state where different players have an enabled choice.");// Should have been detected in generator, already
STORM_LOG_ASSERT(_buildChoiceOrigins,"Building ChoiceOrigins was not enabled.");
STORM_LOG_ASSERT(_dataOfChoiceOrigins.size()<=choiceIndex,"Unexpected choice index. Apparently, the choice indices are provided in an incorrect order.");
STORM_LOG_ASSERT(_buildStatePlayerIndications,"Building StatePlayerIndications was not enabled.");
STORM_LOG_ASSERT(_statePlayerIndications.size()<=stateIndex,"Unexpected choice index. Apparently, the choice indices are provided in an incorrect order.");
STORM_LOG_TRACE("Creating next-state generator for PRISM program: "<<program);
STORM_LOG_THROW(!this->program.specifiesSystemComposition(),storm::exceptions::WrongFormatException,"The explicit next-state generator currently does not support custom system compositions.");
// Only after checking validity of the program, we initialize the variable information.
STORM_LOG_THROW(this->program.getNumberOfRewardModels()==1,storm::exceptions::InvalidArgumentException,"Reference to standard reward model is ambiguous.");
}
}
// If no reward model was yet added, but there was one that was given in the options, we try to build the
STORM_LOG_ASSERT(choiceIt->hasPlayerIndex(),"State '"<<this->stateToString(*this->state)<<"' features a choice without player index.");// This should have been catched while creating the choice already
STORM_LOG_ASSERT(statePlayerIndex!=storm::storage::INVALID_PLAYER_INDEX,"State '"<<this->stateToString(*this->state)<<"' features a choice with invalid player index.");// This should have been catched while creating the choice already
STORM_LOG_ASSERT(choiceIt->hasPlayerIndex(),"State '"<<this->stateToString(*this->state)<<"' features a choice without player index.");// This should have been catched while creating the choice already
STORM_LOG_ASSERT(choiceIt->getPlayerIndex()!=storm::storage::INVALID_PLAYER_INDEX,"State '"<<this->stateToString(*this->state)<<"' features a choice with invalid player index.");// This should have been catched while creating the choice already
STORM_LOG_THROW(statePlayerIndex==choiceIt->getPlayerIndex(),storm::exceptions::WrongFormatException,"The player for state '"<<this->stateToString(*this->state)<<"' is not unique. At least one choice is owned by player '"<<statePlayerIndex<<"' while another is owned by player '"<<choiceIt->getPlayerIndex()<<"'.");
STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset,integerIt->bitWidth))+integerIt->lowerBound==assignedValue,"Writing to the bit vector bucket failed (read "<<newState.getAsInt(integerIt->bitOffset,integerIt->bitWidth)<<" but wrote "<<assignedValue<<").");
}
// Check that we processed all assignments.
STORM_LOG_ASSERT(assignmentIt==assignmentIte,"Not all assignments were consumed.");
STORM_LOG_THROW(playerOfModule!=storm::storage::INVALID_PLAYER_INDEX,storm::exceptions::WrongFormatException,"Module "<<module.getName()<<" is not owned by any player but has at least one enabled, unlabeled command.");
choice.setPlayerIndex(playerOfModule);
}
if(this->options.isExplorationChecksSet()){
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(!program.isDiscreteTimeModel()||this->comparator.isOne(probabilitySum),storm::exceptions::WrongFormatException,"Probabilities do not sum to one for command '"<<command<<"' (actually sum to "<<probabilitySum<<").");
STORM_LOG_THROW(playerOfAction!=storm::storage::INVALID_PLAYER_INDEX,storm::exceptions::WrongFormatException,"Action "<<program.getActionName(actionIndex)<<" is not owned by any player but has at least one enabled, unlabeled (synchronized) command.");
choice.setPlayerIndex(playerOfAction);
}
// Remember the choice label and origins only if we were asked to.
// The empty commandset (i.e., the choices without origin) always has to get identifier getIdentifierForChoicesWithNoOrigin() -- which is assumed to be 0
STORM_LOG_ASSERT(storm::storage::sparse::ChoiceOrigins::getIdentifierForChoicesWithNoOrigin()==0,"The no origin identifier is assumed to be zero");
@ -764,7 +800,7 @@ namespace storm {
uint_fast64_tcurrentIdentifier=1;
for(boost::any&originData:dataForChoiceOrigins){
STORM_LOG_ASSERT(originData.empty()||boost::any_cast<CommandSet>(&originData)!=nullptr,"Origin data has unexpected type: "<<originData.type().name()<<".");
STORM_LOG_THROW(false,storm::exceptions::InvalidArgumentException,"The given formula '"<<stateFormula<<"' is invalid.");
}
@ -321,6 +324,11 @@ namespace storm {
STORM_LOG_THROW(false,storm::exceptions::NotImplementedException,"This model checker ("<<getClassName()<<") does not support the formula: "<<checkTask.getFormula()<<".");
STORM_LOG_THROW(false,storm::exceptions::NotImplementedException,"This model checker ("<<getClassName()<<") does not support the formula: "<<checkTask.getFormula()<<".");
STORM_LOG_THROW(stateCount==this->getTransitionMatrix().getRowCount(),storm::exceptions::IllegalArgumentException,"Can not create deterministic model: Number of rows of transition matrix does not match state count.");
STORM_LOG_THROW(stateCount==this->getTransitionMatrix().getColumnCount(),storm::exceptions::IllegalArgumentException,"Can not create deterministic model: Number of columns of transition matrix does not match state count.");
STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(),"Player 1 matrix given for a model that is no stochastic game (will be ignored).");
STORM_LOG_THROW(stateCount==this->getTransitionMatrix().getRowGroupCount(),storm::exceptions::IllegalArgumentException,"Can not create nondeterministic model: Number of row groups ("<<this->getTransitionMatrix().getRowGroupCount()<<") of transition matrix does not match state count ("<<stateCount<<").");
STORM_LOG_THROW(stateCount==this->getTransitionMatrix().getColumnCount(),storm::exceptions::IllegalArgumentException,"Can not create nondeterministic model: Number of columns of transition matrix does not match state count.");
STORM_LOG_ERROR_COND(!components.player1Matrix.is_initialized(),"Player 1 matrix given for a model that is no stochastic game (will be ignored).");
}else{
STORM_LOG_THROW(this->isOfType(ModelType::S2pg),storm::exceptions::IllegalArgumentException,"Invalid model type.");
}elseif(this->isOfType(ModelType::S2pg)){
STORM_LOG_THROW(components.player1Matrix.is_initialized(),storm::exceptions::IllegalArgumentException,"No player 1 matrix given for stochastic game.");
STORM_LOG_ASSERT(components.player1Matrix->isProbabilistic(),"Can not create stochastic game: There is a row in the p1 matrix with not exactly one entry.");
STORM_LOG_THROW(stateCount==components.player1Matrix->getRowGroupCount(),storm::exceptions::IllegalArgumentException,"Can not create stochastic game: Number of row groups of p1 matrix does not match state count.");
STORM_LOG_THROW(this->getTransitionMatrix().getRowGroupCount()==components.player1Matrix->getColumnCount(),storm::exceptions::IllegalArgumentException,"Can not create stochastic game: Number of row groups of p2 matrix does not match column count of p1 matrix.");
}else{
STORM_LOG_THROW(false,storm::exceptions::IllegalArgumentException,"Invalid model type.");
STORM_LOG_THROW(components.rateTransitions||components.exitRates.is_initialized(),storm::exceptions::IllegalArgumentException,"Can not create continuous time model: no rates are given.");
@ -79,6 +80,17 @@ namespace storm {
STORM_LOG_WARN_COND(!components.rateTransitions&&!components.exitRates.is_initialized(),"Rates specified for discrete-time model. The rates will be ignored.");
}
STORM_LOG_WARN_COND(this->isOfType(ModelType::MarkovAutomaton)||!components.markovianStates.is_initialized(),"Markovian states given for a model that is not a Markov automaton (will be ignored).");
// Treat stochastic multiplayer games
if(this->isOfType(ModelType::Smg)){
STORM_LOG_THROW(components.statePlayerIndications.is_initialized(),storm::exceptions::IllegalArgumentException,"Can not create stochastic multiplayer game: Missing player indications.");
// playerNameToIndexMap is optional.
STORM_LOG_THROW(stateCount==components.statePlayerIndications->size(),storm::exceptions::IllegalArgumentException,"Size of state player indications ("<<components.statePlayerIndications->size()<<") of SMG does not match state count ("<<stateCount<<").");
}else{
STORM_LOG_WARN_COND(!components.statePlayerIndications.is_initialized(),"statePlayerIndications given for a model that is not a stochastic multiplayer game (will be ignored).");
STORM_LOG_WARN_COND(!components.playerNameToIndexMap.is_initialized(),"playerNameToIndexMap given for a model that is not a stochastic multiplayer game (will be ignored).");
STORM_LOG_THROW(isJaniModel(),storm::exceptions::InvalidOperationException,"Cannot retrieve JANI model, because the symbolic description has a different type.");
Tim Quatmann
6 years ago