std::cout<<"Found "<<relevancyInformation.relevantLabels.size()<<" relevant and "<<relevancyInformation.knownLabels.size()<<" known labels."<<std::endl;
std::cout<<"Found "<<relevancyInformation.relevantLabels.size()<<" relevant and "<<relevancyInformation.knownLabels.size()<<" known labels."<<std::endl;
LOG4CPLUS_DEBUG(logger,"Found "<<relevancyInformation.relevantLabels.size()<<" relevant and "<<relevancyInformation.knownLabels.size()<<" known labels.");
STORM_LOG_DEBUG("Found "<<relevancyInformation.relevantLabels.size()<<" relevant and "<<relevancyInformation.knownLabels.size()<<" known labels.");
returnrelevancyInformation;
returnrelevancyInformation;
}
}
@ -350,9 +350,9 @@ namespace storm {
}
}
}
}
LOG4CPLUS_DEBUG(logger,"Successfully gathered data for explicit cuts.");
STORM_LOG_DEBUG("Successfully gathered data for explicit cuts.");
LOG4CPLUS_DEBUG(logger,"Asserting initial combination is taken.");
STORM_LOG_DEBUG("Asserting initial combination is taken.");
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": The supplied Labeling input file does not exist or is not readable by this process.");
STORM_LOG_ERROR("Error while parsing "<<filename<<": The supplied Labeling input file does not exist or is not readable by this process.");
throwstorm::exceptions::FileIoException()<<"Error while parsing "<<filename<<": The supplied Labeling input file does not exist or is not readable by this process.";
throwstorm::exceptions::FileIoException()<<"Error while parsing "<<filename<<": The supplied Labeling input file does not exist or is not readable by this process.";
}
}
@ -68,9 +68,9 @@ namespace storm {
// If #DECLARATION or #END have not been found, the file format is wrong.
// If #DECLARATION or #END have not been found, the file format is wrong.
if(!(foundDecl&&foundEnd)){
if(!(foundDecl&&foundEnd)){
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": File header is corrupted (#DECLARATION or #END missing - case sensitive).");
STORM_LOG_ERROR("Error while parsing "<<filename<<": File header is corrupted (#DECLARATION or #END missing - case sensitive).");
if(!foundDecl)LOG4CPLUS_ERROR(logger,"\tDid not find #DECLARATION token.");
if(!foundDecl)STORM_LOG_ERROR("\tDid not find #DECLARATION token.");
if(!foundEnd)LOG4CPLUS_ERROR(logger,"\tDid not find #END token.");
if(!foundEnd)STORM_LOG_ERROR("\tDid not find #END token.");
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": File header is corrupted (#DECLARATION or #END missing - case sensitive).";
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": File header is corrupted (#DECLARATION or #END missing - case sensitive).";
}
}
@ -99,7 +99,7 @@ namespace storm {
if(cnt>=sizeof(proposition)){
if(cnt>=sizeof(proposition)){
// if token is longer than our buffer, the following strncpy code might get risky...
// if token is longer than our buffer, the following strncpy code might get risky...
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": Atomic proposition with length > "<<(sizeof(proposition)-1)<<" was found.");
STORM_LOG_ERROR("Error while parsing "<<filename<<": Atomic proposition with length > "<<(sizeof(proposition)-1)<<" was found.");
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": Atomic proposition with length > "<<(sizeof(proposition)-1)<<" was found.";
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": Atomic proposition with length > "<<(sizeof(proposition)-1)<<" was found.";
}elseif(cnt>0){
}elseif(cnt>0){
@ -138,7 +138,7 @@ namespace storm {
// If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
// If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": State "<<state<<" was found but has already been read or skipped previously.");
STORM_LOG_ERROR("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.";
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": State "<<state<<" was found but has already been read or skipped previously.";
}
}
@ -159,7 +159,7 @@ namespace storm {
// Has the label been declared in the header?
// Has the label been declared in the header?
if(!labeling.containsLabel(proposition)){
if(!labeling.containsLabel(proposition)){
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": Atomic proposition"<<proposition<<" was found but not declared.");
STORM_LOG_ERROR("Error while parsing "<<filename<<": Atomic proposition"<<proposition<<" was found but not declared.");
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": Atomic proposition"<<proposition<<" was found but not declared.";
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": Atomic proposition"<<proposition<<" was found but not declared.";
LOG4CPLUS_DEBUG(logger,"While parsing "<<filename<<": state "<<lastRow<<" has no transition to itself. Inserted a 0-transition. (3)");
STORM_LOG_DEBUG("While parsing "<<filename<<": state "<<lastRow<<" has no transition to itself. Inserted a 0-transition. (3)");
}else{
}else{
LOG4CPLUS_WARN(logger,"Warning while parsing "<<filename<<": state "<<lastRow<<" has no transition to itself.");
STORM_LOG_WARN("Warning while parsing "<<filename<<": state "<<lastRow<<" has no transition to itself.");
}
}
}
}
@ -200,7 +200,7 @@ namespace storm {
// 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.
// 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.");
STORM_LOG_ERROR("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.";
throwstorm::exceptions::WrongFormatException()<<"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.";
}
}
}elseif(source<lastsource){
}elseif(source<lastsource){
LOG4CPLUS_ERROR(logger,"Illegal state choice order. A choice of state "<<source<<" appears at an illegal position.");
STORM_LOG_ERROR("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.";
throwstorm::exceptions::WrongFormatException()<<"Illegal state choice order. A choice of state "<<source<<" appears at an illegal position.";
}
}
@ -80,11 +80,11 @@ namespace storm {
if(isMarkovianChoice){
if(isMarkovianChoice){
if(stateHasMarkovianChoice){
if(stateHasMarkovianChoice){
LOG4CPLUS_ERROR(logger,"The state "<<source<<" has multiple Markovian choices.");
STORM_LOG_ERROR("The state "<<source<<" has multiple Markovian choices.");
throwstorm::exceptions::WrongFormatException()<<"The state "<<source<<" has multiple Markovian choices.";
throwstorm::exceptions::WrongFormatException()<<"The state "<<source<<" has multiple Markovian choices.";
}
}
if(stateHasProbabilisticChoice){
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.");
STORM_LOG_ERROR("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.";
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;
stateHasMarkovianChoice=true;
@ -106,7 +106,7 @@ namespace storm {
// If the end of the file was reached, we need to abort and check whether we are in a legal state.
// 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(buf[0]=='\0'){
if(!hasSuccessorState){
if(!hasSuccessorState){
LOG4CPLUS_ERROR(logger,"Premature end-of-file. Expected at least one successor state for state "<<source<<".");
STORM_LOG_ERROR("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<<".";
throwstorm::exceptions::WrongFormatException()<<"Premature end-of-file. Expected at least one successor state for state "<<source<<".";
}else{
}else{
// If there was at least one successor for the current choice, this is legal and we need to move on.
// If there was at least one successor for the current choice, this is legal and we need to move on.
LOG4CPLUS_ERROR(logger,"Illegal transition order for source state "<<source<<".");
STORM_LOG_ERROR("Illegal transition order for source state "<<source<<".");
throwstorm::exceptions::WrongFormatException()<<"Illegal transition order for source state "<<source<<".";
throwstorm::exceptions::WrongFormatException()<<"Illegal transition order for source state "<<source<<".";
}
}
// And the corresponding probability/rate.
// And the corresponding probability/rate.
doubleval=checked_strtod(buf,&buf);
doubleval=checked_strtod(buf,&buf);
if(val<0.0){
if(val<0.0){
LOG4CPLUS_ERROR(logger,"Illegal negative probability/rate value for transition from "<<source<<" to "<<target<<": "<<val<<".");
STORM_LOG_ERROR("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<<".";
throwstorm::exceptions::WrongFormatException()<<"Illegal negative probability/rate value for transition from "<<source<<" to "<<target<<": "<<val<<".";
}
}
if(!isMarkovianChoice&&val>1.0){
if(!isMarkovianChoice&&val>1.0){
LOG4CPLUS_ERROR(logger,"Illegal probability value for transition from "<<source<<" to "<<target<<": "<<val<<".");
STORM_LOG_ERROR("Illegal probability value for transition from "<<source<<" to "<<target<<": "<<val<<".");
throwstorm::exceptions::WrongFormatException()<<"Illegal probability value for transition from "<<source<<" to "<<target<<": "<<val<<".";
throwstorm::exceptions::WrongFormatException()<<"Illegal probability value for transition from "<<source<<" to "<<target<<": "<<val<<".";
}
}
@ -191,7 +191,7 @@ namespace storm {
++currentChoice;
++currentChoice;
}
}
}else{
}else{
LOG4CPLUS_ERROR(logger,"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.");
STORM_LOG_ERROR("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.";
throwstorm::exceptions::WrongFormatException()<<"Found deadlock states (e.g. "<<lastsource+1<<") during parsing. Please fix them or set the appropriate flag.";
// The matrix to be build should have as many columns as we have nodes and as many rows as we have choices.
// 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.
// 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.");
STORM_LOG_INFO("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.");
STORM_LOG_WARN("Warning while parsing "<<filename<<": node "<<node<<" has no outgoing transitions. A self-loop was inserted.");
}else{
}else{
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": node "<<node<<" has no outgoing transitions.");
STORM_LOG_ERROR("Error while parsing "<<filename<<": node "<<node<<" has no outgoing transitions.");
}
}
}
}
if(source!=lastSource){
if(source!=lastSource){
@ -194,7 +194,7 @@ namespace storm {
// 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.
// 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,"State index "<<result.highestStateIndex<<" found. This exceeds the highest state index of the model, which is "<<modelInformation.getColumnCount()-1<<" .");
STORM_LOG_ERROR("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<<" .";
throwstorm::exceptions::OutOfRangeException()<<"State index "<<result.highestStateIndex<<" found. This exceeds the highest state index of the model, which is "<<modelInformation.getColumnCount()-1<<" .";
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": File does not exist or is not readable.");
STORM_LOG_ERROR("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.";
throwstorm::exceptions::FileIoException()<<"Error while parsing "<<filename<<": File does not exist or is not readable.";
}
}
@ -47,12 +47,12 @@ namespace storm {
// If the state has already been read or skipped once there might be a problem with the file (doubled lines, or blocks).
// 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).
// 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.");
STORM_LOG_ERROR("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.";
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": State "<<state<<" was found but has already been read or skipped previously.";
}
}
if(stateCount<=state){
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.");
STORM_LOG_ERROR("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<<"\"";
throwstorm::exceptions::OutOfRangeException()<<"Error while parsing "<<filename<<": Found reward for a state of an invalid index \""<<state<<"\"";
}
}
@ -60,7 +60,7 @@ namespace storm {
reward=checked_strtod(buf,&buf);
reward=checked_strtod(buf,&buf);
if(reward<0.0){
if(reward<0.0){
LOG4CPLUS_ERROR(logger,"Error while parsing "<<filename<<": Expected positive reward value but got \""<<reward<<"\".");
STORM_LOG_ERROR("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.";
throwstorm::exceptions::WrongFormatException()<<"Error while parsing "<<filename<<": State reward file specifies illegal reward value.";
LOG4CPLUS_INFO(logger,"Executed "<<globalIterations<<" of max. "<<maximalNumberOfIterations<<" Iterations on GPU.");
STORM_LOG_INFO("Executed "<<globalIterations<<" of max. "<<maximalNumberOfIterations<<" Iterations on GPU.");
boolconverged=false;
boolconverged=false;
if(!result){
if(!result){
converged=false;
converged=false;
LOG4CPLUS_ERROR(logger,"An error occurred in the CUDA Plugin. Can not continue.");
STORM_LOG_ERROR("An error occurred in the CUDA Plugin. Can not continue.");
throwstorm::exceptions::InvalidStateException()<<"An error occurred in the CUDA Plugin. Can not continue.";
throwstorm::exceptions::InvalidStateException()<<"An error occurred in the CUDA Plugin. Can not continue.";
}else{
}else{
converged=true;
converged=true;
@ -120,12 +120,12 @@ namespace storm {
// Check if the solver converged and issue a warning otherwise.
// Check if the solver converged and issue a warning otherwise.
if(converged){
if(converged){
LOG4CPLUS_INFO(logger,"Iterative solver converged after "<<globalIterations<<" iterations.");
STORM_LOG_INFO("Iterative solver converged after "<<globalIterations<<" iterations.");
}else{
}else{
LOG4CPLUS_WARN(logger,"Iterative solver did not converged after "<<globalIterations<<" iterations.");
STORM_LOG_WARN("Iterative solver did not converged after "<<globalIterations<<" iterations.");
}
}
#else
#else
LOG4CPLUS_ERROR(logger,"The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
throwstorm::exceptions::InvalidStateException()<<"The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
throwstorm::exceptions::InvalidStateException()<<"The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
LOG4CPLUS_INFO(logger,"Executed "<<localIterations<<" of max. "<<maximalNumberOfIterations<<" Iterations on GPU.");
STORM_LOG_INFO("Executed "<<localIterations<<" of max. "<<maximalNumberOfIterations<<" Iterations on GPU.");
if(!result){
if(!result){
converged=false;
converged=false;
LOG4CPLUS_ERROR(logger,"An error occurred in the CUDA Plugin. Can not continue.");
STORM_LOG_ERROR("An error occurred in the CUDA Plugin. Can not continue.");
throwstorm::exceptions::InvalidStateException()<<"An error occurred in the CUDA Plugin. Can not continue.";
throwstorm::exceptions::InvalidStateException()<<"An error occurred in the CUDA Plugin. Can not continue.";
}else{
}else{
converged=true;
converged=true;
@ -226,12 +226,12 @@ namespace storm {
}
}
globalIterations+=localIterations;
globalIterations+=localIterations;
#else
#else
LOG4CPLUS_ERROR(logger,"The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
STORM_LOG_ERROR("The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!");
throwstorm::exceptions::InvalidStateException()<<"The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
throwstorm::exceptions::InvalidStateException()<<"The useGpu Flag of a SCC was set, but this version of StoRM does not support CUDA acceleration. Internal Error!";
#endif
#endif
}else{
}else{
//std::cout << "WARNING: Using CPU based TopoSolver! (double)" << std::endl;
//std::cout << "WARNING: Using CPU based TopoSolver! (double)" << std::endl;
LOG4CPLUS_INFO(logger,"Performance Warning: Using CPU based TopoSolver! (double)");
STORM_LOG_INFO("Performance Warning: Using CPU based TopoSolver! (double)");
dehnert
9 years ago
xxxxxxxxxx