// Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards.
// Since we cannot check if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards.
LOG4CPLUS_ERROR(logger,"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.");
throwstorm::exceptions::WrongFormatException()<<"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.";
}
}elseif(source<lastsource){
LOG4CPLUS_ERROR(logger,"Illegal state choice order. A choice of state "<<source<<" appears at an illegal position.");
throwstorm::exceptions::WrongFormatException()<<"Illegal state choice order. A choice of state "<<source<<" appears at an illegal position.";
}
++result.numberOfChoices;
// If we have moved to the next state, we need to clear the flag that stores whether or not the source has a Markovian or probabilistic choice.
if(source!=lastsource){
stateHasMarkovianChoice=false;
stateHasProbabilisticChoice=false;
}
// Record that the current source was the last source.
lastsource=source;
buf=trimWhitespaces(buf);
// Depending on the action name, the choice is either a probabilitic one or a markovian one.
boolisMarkovianChoice=false;
if(buf[0]=='!'&&skipWord(buf)-buf==1){
isMarkovianChoice=true;
}else{
isMarkovianChoice=false;
}
buf=skipWord(buf);
if(isMarkovianChoice){
if(stateHasMarkovianChoice){
LOG4CPLUS_ERROR(logger,"The state "<<source<<" has multiple Markovian choices.");
throwstorm::exceptions::WrongFormatException()<<"The state "<<source<<" has multiple Markovian choices.";
}
if(stateHasProbabilisticChoice){
LOG4CPLUS_ERROR(logger,"The state "<<source<<" has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.");
throwstorm::exceptions::WrongFormatException()<<"The state "<<source<<" has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.";
}
stateHasMarkovianChoice=true;
}else{
stateHasProbabilisticChoice=true;
}
// Go to the next line where the transitions start.
buf=forwardToNextLine(buf);
// Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates.
boolhasSuccessorState=false;
boolencounteredNewDistribution=false;
uint_fast64_tlastSuccessorState=0;
// At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
do{
buf=trimWhitespaces(buf);
// If the end of the file was reached, we need to abort and check whether we are in a legal state.
if(buf[0]=='\0'){
if(!hasSuccessorState){
LOG4CPLUS_ERROR(logger,"Premature end-of-file. Expected at least one successor state for state "<<source<<".");
throwstorm::exceptions::WrongFormatException()<<"Premature end-of-file. Expected at least one successor state for state "<<source<<".";
}else{
// If there was at least one successor for the current choice, this is legal and we need to move on.
encounteredEOF=true;
}
}elseif(buf[0]=='*'){
// As we have encountered a "*", we know that there is an additional successor state for the current choice.
buf=skipWord(buf);
// Now we need to read the successor state and check if we already saw a higher state index.
LOG4CPLUS_ERROR(logger,"Illegal transition order for source state "<<source<<".");
throwstorm::exceptions::WrongFormatException()<<"Illegal transition order for source state "<<source<<".";
}
// And the corresponding probability/rate.
doubleval=checked_strtod(buf,&buf);
if(val<0.0){
LOG4CPLUS_ERROR(logger,"Illegal negative probability/rate value for transition from "<<source<<" to "<<target<<": "<<val<<".");
throwstorm::exceptions::WrongFormatException()<<"Illegal negative probability/rate value for transition from "<<source<<" to "<<target<<": "<<val<<".";
}
if(!isMarkovianChoice&&val>1.0){
LOG4CPLUS_ERROR(logger,"Illegal probability value for transition from "<<source<<" to "<<target<<": "<<val<<".");
throwstorm::exceptions::WrongFormatException()<<"Illegal probability value for transition from "<<source<<" to "<<target<<": "<<val<<".";
}
// We need to record that we found at least one successor state for the current choice.
hasSuccessorState=true;
lastSuccessorState=target;
// As we found a new successor, we need to increase the number of nonzero entries.
++result.numberOfNonzeroEntries;
buf=forwardToNextLine(buf);
}else{
// If it was not a "*", we have to assume that we encountered the beginning of a new choice definition. In this case, we don't move the pointer
// to the buffer, because we still need to read the new source state.
LOG4CPLUS_ERROR(logger,"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.");
throwstorm::exceptions::WrongFormatException()<<"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.";
}
}
if(source!=lastsource){
// If we skipped to a new state we need to create a new row group for the choices of the new state.
// Record that the current source was the last source.
lastsource=source;
buf=trimWhitespaces(buf);
// Depending on the action name, the choice is either a probabilitic one or a markovian one.
boolisMarkovianChoice=false;
if(buf[0]=='!'&&skipWord(buf)-buf==1){
isMarkovianChoice=true;
// Mark the current state as a Markovian one.
result.markovianStates.set(source,true);
}else{
isMarkovianChoice=false;
}
// Go to the next line where the transitions start.
buf=forwardToNextLine(buf);
// Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates.
boolencounteredNewDistribution=false;
// At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
do{
buf=trimWhitespaces(buf);
// If the end of the file was reached, we need to abort and check whether we are in a legal state.
if(buf[0]=='\0'){
// Under the assumption that the currently open choice has at least one successor (which is given after the first run)
// we may legally stop reading here.
encounteredEOF=true;
}elseif(buf[0]=='*'){
// As we have encountered a "*", we know that there is an additional successor state for the current choice.
buf=skipWord(buf);
// Now we need to read the successor state and check if we already saw a higher state index.
target=checked_strtol(buf,&buf);
// And the corresponding probability/rate.
doubleval=checked_strtod(buf,&buf);
// Record the value as well as the exit rate in case of a Markovian choice.
LOG4CPLUS_ERROR(logger,"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.");
throwstorm::exceptions::WrongFormatException()<<"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.";
}
}elseif(source<lastsource){
LOG4CPLUS_ERROR(logger,"Illegal state choice order. A choice of state "<<source<<" appears at an illegal position.");
throwstorm::exceptions::WrongFormatException()<<"Illegal state choice order. A choice of state "<<source<<" appears at an illegal position.";
}
++result.numberOfChoices;
// If we have moved to the next state, we need to clear the flag that stores whether or not the source has a Markovian or probabilistic choice.
if(source!=lastsource){
stateHasMarkovianChoice=false;
stateHasProbabilisticChoice=false;
}
// Record that the current source was the last source.
lastsource=source;
buf=trimWhitespaces(buf);
// Depending on the action name, the choice is either a probabilitic one or a markovian one.
boolisMarkovianChoice=false;
if(buf[0]=='!'&&skipWord(buf)-buf==1){
isMarkovianChoice=true;
}else{
isMarkovianChoice=false;
}
buf=skipWord(buf);
if(isMarkovianChoice){
if(stateHasMarkovianChoice){
LOG4CPLUS_ERROR(logger,"The state "<<source<<" has multiple Markovian choices.");
throwstorm::exceptions::WrongFormatException()<<"The state "<<source<<" has multiple Markovian choices.";
}
if(stateHasProbabilisticChoice){
LOG4CPLUS_ERROR(logger,"The state "<<source<<" has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.");
throwstorm::exceptions::WrongFormatException()<<"The state "<<source<<" has a probabilistic choice preceding a Markovian choice. The Markovian choice must be the first choice listed.";
}
stateHasMarkovianChoice=true;
}else{
stateHasProbabilisticChoice=true;
}
// Go to the next line where the transitions start.
buf=forwardToNextLine(buf);
// Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates.
boolhasSuccessorState=false;
boolencounteredNewDistribution=false;
uint_fast64_tlastSuccessorState=0;
// At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
do{
buf=trimWhitespaces(buf);
// If the end of the file was reached, we need to abort and check whether we are in a legal state.
if(buf[0]=='\0'){
if(!hasSuccessorState){
LOG4CPLUS_ERROR(logger,"Premature end-of-file. Expected at least one successor state for state "<<source<<".");
throwstorm::exceptions::WrongFormatException()<<"Premature end-of-file. Expected at least one successor state for state "<<source<<".";
}else{
// If there was at least one successor for the current choice, this is legal and we need to move on.
encounteredEOF=true;
}
}elseif(buf[0]=='*'){
// As we have encountered a "*", we know that there is an additional successor state for the current choice.
buf=skipWord(buf);
// Now we need to read the successor state and check if we already saw a higher state index.
LOG4CPLUS_ERROR(logger,"Illegal transition order for source state "<<source<<".");
throwstorm::exceptions::WrongFormatException()<<"Illegal transition order for source state "<<source<<".";
}
// And the corresponding probability/rate.
doubleval=checked_strtod(buf,&buf);
if(val<0.0){
LOG4CPLUS_ERROR(logger,"Illegal negative probability/rate value for transition from "<<source<<" to "<<target<<": "<<val<<".");
throwstorm::exceptions::WrongFormatException()<<"Illegal negative probability/rate value for transition from "<<source<<" to "<<target<<": "<<val<<".";
}
if(!isMarkovianChoice&&val>1.0){
LOG4CPLUS_ERROR(logger,"Illegal probability value for transition from "<<source<<" to "<<target<<": "<<val<<".");
throwstorm::exceptions::WrongFormatException()<<"Illegal probability value for transition from "<<source<<" to "<<target<<": "<<val<<".";
}
// We need to record that we found at least one successor state for the current choice.
hasSuccessorState=true;
lastSuccessorState=target;
// As we found a new successor, we need to increase the number of nonzero entries.
++result.numberOfNonzeroEntries;
buf=forwardToNextLine(buf);
}else{
// If it was not a "*", we have to assume that we encountered the beginning of a new choice definition. In this case, we don't move the pointer
// to the buffer, because we still need to read the new source state.
LOG4CPLUS_ERROR(logger,"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.");
throwstorm::exceptions::WrongFormatException()<<"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.";
}
}
if(source!=lastsource){
// If we skipped to a new state we need to create a new row group for the choices of the new state.
// Record that the current source was the last source.
lastsource=source;
buf=trimWhitespaces(buf);
// Depending on the action name, the choice is either a probabilitic one or a markovian one.
boolisMarkovianChoice=false;
if(buf[0]=='!'&&skipWord(buf)-buf==1){
isMarkovianChoice=true;
// Mark the current state as a Markovian one.
result.markovianStates.set(source,true);
}else{
isMarkovianChoice=false;
}
// Go to the next line where the transitions start.
buf=forwardToNextLine(buf);
// Now that we have the source state and the information whether or not the current choice is probabilistic or Markovian, we need to read the list of successors and the probabilities/rates.
boolencounteredNewDistribution=false;
// At this point, we need to check whether there is an additional successor or we have reached the next choice for the same or a different state.
do{
buf=trimWhitespaces(buf);
// If the end of the file was reached, we need to abort and check whether we are in a legal state.
if(buf[0]=='\0'){
// Under the assumption that the currently open choice has at least one successor (which is given after the first run)
// we may legally stop reading here.
encounteredEOF=true;
}elseif(buf[0]=='*'){
// As we have encountered a "*", we know that there is an additional successor state for the current choice.
buf=skipWord(buf);
// Now we need to read the successor state and check if we already saw a higher state index.
target=checked_strtol(buf,&buf);
// And the corresponding probability/rate.
doubleval=checked_strtod(buf,&buf);
// Record the value as well as the exit rate in case of a Markovian choice.
// The matrix to be build should have as many columns as we have nodes and as many rows as we have choices.
// Those two values, as well as the number of nonzero elements, was been calculated in the first run.
LOG4CPLUS_INFO(logger,"Attempting to create matrix of size "<<firstPass.choices<<" x "<<(firstPass.highestStateIndex+1)<<" with "<<firstPass.numberOfNonzeroEntries<<" entries.");
LOG4CPLUS_WARN(logger,"Warning while parsing "<<filename<<": node "<<node<<" has no outgoing transitions. A self-loop was inserted.");
}else{
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": node "<<node<<" has no outgoing transitions.");
}
}
if(source!=lastSource){
// Add create a new rowGroup for the source, if this is the first choice we encounter for this state.
matrixBuilder.newRowGroup(curRow);
}
}
// Read target and value and write it to the matrix.
target=checked_strtol(buf,&buf);
val=checked_strtod(buf,&buf);
matrixBuilder.addNextValue(curRow,target,val);
lastSource=source;
lastChoice=choice;
// Proceed to beginning of next line in file and next row in matrix.
buf=forwardToLineEnd(buf);
buf=trimWhitespaces(buf);
}
if(dontFixDeadlocks&&hadDeadlocks&&!isRewardFile)throwstorm::exceptions::WrongFormatException()<<"Some of the states do not have outgoing transitions.";
// Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices.
// Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards.
LOG4CPLUS_ERROR(logger,"State index "<<result.highestStateIndex<<" found. This exceeds the highest state index of the model, which is "<<modelInformation.getColumnCount()-1<<" .");
throwstorm::exceptions::OutOfRangeException()<<"State index "<<result.highestStateIndex<<" found. This exceeds the highest state index of the model, which is "<<modelInformation.getColumnCount()-1<<" .";
}
// If we have switched the source state, we possibly need to insert rows for skipped choices of the last
// source state.
if(source!=lastSource){
// number of choices skipped = number of choices of last state - number of choices read
// The matrix to be build should have as many columns as we have nodes and as many rows as we have choices.
// Those two values, as well as the number of nonzero elements, was been calculated in the first run.
LOG4CPLUS_INFO(logger,"Attempting to create matrix of size "<<firstPass.choices<<" x "<<(firstPass.highestStateIndex+1)<<" with "<<firstPass.numberOfNonzeroEntries<<" entries.");
LOG4CPLUS_WARN(logger,"Warning while parsing "<<filename<<": node "<<node<<" has no outgoing transitions. A self-loop was inserted.");
}else{
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": node "<<node<<" has no outgoing transitions.");
}
}
if(source!=lastSource){
// Add create a new rowGroup for the source, if this is the first choice we encounter for this state.
matrixBuilder.newRowGroup(curRow);
}
}
// Read target and value and write it to the matrix.
target=checked_strtol(buf,&buf);
val=checked_strtod(buf,&buf);
matrixBuilder.addNextValue(curRow,target,val);
lastSource=source;
lastChoice=choice;
// Proceed to beginning of next line in file and next row in matrix.
buf=forwardToLineEnd(buf);
buf=trimWhitespaces(buf);
}
if(dontFixDeadlocks&&hadDeadlocks&&!isRewardFile)throwstorm::exceptions::WrongFormatException()<<"Some of the states do not have outgoing transitions.";
// Since we assume the transition rewards are for the transitions of the model, we copy the rowGroupIndices.
// Since we cannot do the testing if each transition for which there is a reward in the reward file also exists in the transition matrix during parsing, we have to do it afterwards.
LOG4CPLUS_ERROR(logger,"State index "<<result.highestStateIndex<<" found. This exceeds the highest state index of the model, which is "<<modelInformation.getColumnCount()-1<<" .");
throwstorm::exceptions::OutOfRangeException()<<"State index "<<result.highestStateIndex<<" found. This exceeds the highest state index of the model, which is "<<modelInformation.getColumnCount()-1<<" .";
}
// If we have switched the source state, we possibly need to insert rows for skipped choices of the last
// source state.
if(source!=lastSource){
// number of choices skipped = number of choices of last state - number of choices read
// If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
// Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting index).
STORM_LOG_THROW(false,storm::exceptions::WrongFormatException,"Error while parsing "<<filename<<": State "<<state<<" was found but has already been read or skipped previously.");
STORM_LOG_THROW(false,storm::exceptions::WrongFormatException,"Error while parsing "<<filename<<": Choice "<<choice<<" was found but has already been read or skipped previously.");
}
if(state>=nondeterministicChoiceIndices.size()){
STORM_LOG_THROW(false,storm::exceptions::WrongFormatException,"Error while parsing "<<filename<<": Illegal state "<<state<<".");
STORM_LOG_THROW(false,storm::exceptions::WrongFormatException,"Error while parsing "<<filename<<": Choice "<<choice<<" is illegal for state "<<state<<", because this state has fewer choices.");
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": File does not exist or is not readable.");
throwstorm::exceptions::FileIoException()<<"Error while parsing "<<filename<<": File does not exist or is not readable.";
}
MappedFilefile(filename.c_str());
charconst*buf=file.getData();
// Create state reward vector with given state count.
std::vector<double>stateRewards(stateCount);
// Now parse state reward assignments.
uint_fast64_tstate=0;
uint_fast64_tlastState=(uint_fast64_t)-1;
uint_fast64_tconststartIndexComparison=lastState;
doublereward;
// Iterate over states.
while(buf[0]!='\0'){
// Parse state number and reward value.
state=checked_strtol(buf,&buf);
// If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
// Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting index).
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": State "<<state<<" was found but has already been read or skipped previously.");
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": State "<<state<<" was found but has already been read or skipped previously.";
}
if(stateCount<=state){
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": Found reward for a state of an invalid index \""<<state<<"\". The model has only "<<stateCount<<" states.");
throwstorm::exceptions::OutOfRangeException()<<"Error while parsing "<<filename<<": Found reward for a state of an invalid index \""<<state<<"\"";
}
reward=checked_strtod(buf,&buf);
if(reward<0.0){
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": Expected positive reward value but got \""<<reward<<"\".");
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": State reward file specifies illegal reward value.";
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": File does not exist or is not readable.");
throwstorm::exceptions::FileIoException()<<"Error while parsing "<<filename<<": File does not exist or is not readable.";
}
MappedFilefile(filename.c_str());
charconst*buf=file.getData();
// Create state reward vector with given state count.
std::vector<double>stateRewards(stateCount);
// Now parse state reward assignments.
uint_fast64_tstate=0;
uint_fast64_tlastState=(uint_fast64_t)-1;
uint_fast64_tconststartIndexComparison=lastState;
doublereward;
// Iterate over states.
while(buf[0]!='\0'){
// Parse state.
state=checked_strtol(buf,&buf);
// If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
// Note: The value -1 shows that lastState has not yet been set, i.e. this is the first run of the loop (state index (2^64)-1 is a really bad starting index).
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": State "<<state<<" was found but has already been read or skipped previously.");
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": State "<<state<<" was found but has already been read or skipped previously.";
}
if(stateCount<=state){
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": Found reward for a state of an invalid index \""<<state<<"\". The model has only "<<stateCount<<" states.");
throwstorm::exceptions::OutOfRangeException()<<"Error while parsing "<<filename<<": Found reward for a state of an invalid index \""<<state<<"\"";
}
// Parse reward value.
reward=checked_strtod(buf,&buf);
if(reward<0.0){
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": Expected positive reward value but got \""<<reward<<"\".");
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": State reward file specifies illegal reward value.";
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename","The file from which to read the transition rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,stateRewardsOptionName,false,"If given, the state 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 state rewards.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,choiceLabelingOptionName,false,"If given, the choice labels 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 choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName,dontFixDeadlockOptionName,false,"If the model contains deadlock states, they need to be fixed by setting this option.").setShortName(dontFixDeadlockOptionShortName).build());
// Test the resilience of the parser against whitespaces.
// Do so by comparing the hash of the matrix resulting from the file without whitespaces with the hash of the matrix resulting from the file with whitespaces.
// Test the resilience of the parser against whitespaces.
// Do so by comparing the hash of the matrix resulting from the file without whitespaces with the hash of the matrix resulting from the file with whitespaces.
sjunges
10 years ago
xxxxxxxxxx