sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Further work on explicit MarkovAutomaton parser. 

Former-commit-id: 19fbff695b
tempestpy_adaptions
dehnert 11 years ago
parent
77cabe1948
commit
873373eb4e
2 changed files with 93 additions and 157 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 155
      src/parser/MarkovAutomataSparseTransitionParser.cpp
  2. 7
      src/parser/MarkovAutomataSparseTransitionParser.h

155
src/parser/MarkovAutomataSparseTransitionParser.cpp
View File

@ -3,56 +3,43 @@
namespace storm { namespace storm {
namespace parser { namespace parser {
MarkovAutomataSparseTransitionParser::FirstPassResult MarkovAutomataSparseTransitionParser::performFirstPass(char* buf, SupportedLineEndingsEnum lineEndings, RewardMatrixInformationStruct* rewardMatrixInformation) {
MarkovAutomataSparseTransitionParser::FirstPassResult MarkovAutomataSparseTransitionParser::firstPass(char* buf, SupportedLineEndingsEnum lineEndings, RewardMatrixInformationStruct* rewardMatrixInformation) {
bool isRewardFile = rewardMatrixInformation != nullptr; bool isRewardFile = rewardMatrixInformation != nullptr;
MarkovAutomataSparseTransitionParser::FirstPassResult result; MarkovAutomataSparseTransitionParser::FirstPassResult result;
/*
* Check file header and extract number of transitions.
*/
if (!isRewardFile) {
// skip format hint
// Skip the format hint.
buf = storm::parser::forwardToNextLine(buf, lineEndings); buf = storm::parser::forwardToNextLine(buf, lineEndings);
}
/* /*
* Read all transitions. * Read all transitions.
*/ */
int_fast64_t source, target, choice, lastchoice = -1;
int_fast64_t source, target = -1;
int_fast64_t lastsource = -1; int_fast64_t lastsource = -1;
uint_fast64_t nonzero = 0;
double val;
result.numberOfChoices = 0;
result.numberOfStates = 0;
bool isMarkovianChoice = false;
char actionNameBuffer[20];
char star[20];
bool encounteredEOF = false; bool encounteredEOF = false;
while (buf[0] != '\0') {
while (buf[0] != '\0' && !encounteredEOF) {
/* /*
* Read source state and choice. * Read source state and choice.
*/ */
source = checked_strtol(buf, &buf); source = checked_strtol(buf, &buf);
// Check if we encountered a state index that is bigger than all previously seen ones and record it if necessary. // Check if we encountered a state index that is bigger than all previously seen ones and record it if necessary.
if (source > result.numberOfStates) {
result.numberOfStates = source;
if (source > result.highestStateIndex) {
result.highestStateIndex = source;
} }
if (isRewardFile) {
// FIXME: Fill this
} else {
// If we have skipped some states, we need to reserve the space for the self-loop insertion in the second pass. // If we have skipped some states, we need to reserve the space for the self-loop insertion in the second pass.
if (source > lastsource + 1) { if (source > lastsource + 1) {
nonzero += source - lastsource - 1;
result.numberOfNonzeroEntries += source - lastsource - 1;
result.numberOfChoices += source - lastsource - 1; result.numberOfChoices += source - lastsource - 1;
} else if (source != lastsource) {
// If we have switched the source state, we need to reserve one row more.
} else {
++result.numberOfChoices; ++result.numberOfChoices;
} }
}
// Record that the current source was the last source.
lastsource = source;
char actionNameBuffer[20];
#ifdef WINDOWS #ifdef WINDOWS
int length = sscanf_s(buf, "%20s\n", actionNameBuffer, 20); int length = sscanf_s(buf, "%20s\n", actionNameBuffer, 20);
#else #else
@ -69,6 +56,7 @@ namespace storm {
} }
// Depending on the action name, the choice is either a probabilitic one or a markovian one. // Depending on the action name, the choice is either a probabilitic one or a markovian one.
bool isMarkovianChoice = false;
if (strcmp(actionNameBuffer, "!") == 0) { if (strcmp(actionNameBuffer, "!") == 0) {
isMarkovianChoice = true; isMarkovianChoice = true;
} else { } else {
@ -96,12 +84,17 @@ namespace storm {
// 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. // 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.
bool hasSuccessorState = false; bool hasSuccessorState = false;
bool encounteredNewDistribution = 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. // 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 {
// Now parse the next symbol to see whether there is another target state for the current choice
// or not.
char star[1];
#ifdef WINDOWS #ifdef WINDOWS
length = sscanf_s(buf, "%20s\n", star, 20);
length = sscanf_s(buf, "%1s\n", star, 1);
#else #else
length = sscanf(buf, "%20s\n", star);
length = sscanf(buf, "%1s\n", star);
#endif #endif
// If the number of arguments filled is not one, there was an error. // If the number of arguments filled is not one, there was an error.
@ -117,83 +110,29 @@ namespace storm {
LOG4CPLUS_ERROR(logger, "Parsing error."); LOG4CPLUS_ERROR(logger, "Parsing error.");
throw storm::exceptions::WrongFormatException() << "Parsing error."; throw storm::exceptions::WrongFormatException() << "Parsing error.";
} else if (strcmp(star, "*") == 0) { } else if (strcmp(star, "*") == 0) {
// We need to record that we found at least one successor state for the current choice.
hasSuccessorState = true;
// As we have encountered a "*", we know that there is an additional successor state for the current choice. // As we have encountered a "*", we know that there is an additional successor state for the current choice.
++result.numberOfNonzeroEntries;
buf += strlen(star); buf += strlen(star);
} 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.
}
std::cout << "Got here! " << isMarkovianChoice << " // " << actionNameBuffer << " // " << strlen(actionNameBuffer) << std::endl;
if (isRewardFile) {
// If we have switched the source state, we possibly need to insert the rows of the last
// last source state.
if (source != lastsource && lastsource != -1) {
result.numberOfChoices += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
}
// If we skipped some states, we need to reserve empty rows for all their nondeterministic
// choices.
for (int_fast64_t i = lastsource + 1; i < source; ++i) {
result.numberOfChoices += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
}
// If we advanced to the next state, but skipped some choices, we have to reserve rows for them.
if (source != lastsource) {
result.numberOfChoices += choice + 1;
} else if (choice != lastchoice) {
result.numberOfChoices += choice - lastchoice;
}
} else {
// If we have skipped some states, we need to reserve the space for the self-loop insertion
// in the second pass.
if (source > lastsource + 1) {
nonzero += source - lastsource - 1;
result.numberOfChoices += source - lastsource - 1;
} else if (source != lastsource || choice != lastchoice) {
// If we have switched the source state or the nondeterministic choice, we need to
// reserve one row more.
++result.numberOfChoices;
}
}
// Read target and check if we encountered a state index that is bigger than all previously
// seen.
// Now we need to read the successor state and check if we already saw a higher state index.
target = checked_strtol(buf, &buf); target = checked_strtol(buf, &buf);
if (target > result.numberOfStates) {
result.numberOfStates = target;
if (target > result.highestStateIndex) {
result.highestStateIndex = target;
} }
// Read value and check whether it's positive.
val = checked_strtod(buf, &buf);
if (val < 0.0) {
LOG4CPLUS_ERROR(logger, "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".");
throw storm::exceptions::InvalidArgumentException() << "Expected a positive probability but got \"" << std::string(buf, 0, 16) << "\".";
// And the corresponding probability/rate.
double val = checked_strtod(buf, &buf);
if (val <= 0.0) {
LOG4CPLUS_ERROR(logger, "Illegal probability/rate value " << val << ".");
throw storm::exceptions::WrongFormatException() << "Illegal probability/rate value " << val << ".";
} }
lastchoice = choice;
lastsource = source;
/*
* Increase number of non-zero values.
*/
nonzero++;
// The PRISM output format lists the name of the transition in the fourth column,
// but omits the fourth column if it is an internal action. In either case, however, the third column
// is followed by a space. We need to skip over that space first (instead of trimming whitespaces),
// before we can skip to the line end, because trimming the white spaces will proceed to the next line
// in case there is no action label in the fourth column.
if (buf[0] == ' ') {
++buf;
}
// As we found a new successor, we need to increase the number of nonzero entries.
++result.numberOfNonzeroEntries;
/*
* Proceed to beginning of next line.
*/
// Proceed to beginning of next line.
switch (lineEndings) { switch (lineEndings) {
case SupportedLineEndingsEnum::SlashN: case SupportedLineEndingsEnum::SlashN:
buf += strcspn(buf, " \t\n"); buf += strcspn(buf, " \t\n");
@ -206,22 +145,17 @@ namespace storm {
break; break;
default: default:
case storm::parser::SupportedLineEndingsEnum::Unsupported: case storm::parser::SupportedLineEndingsEnum::Unsupported:
// This Line will never be reached as the Parser would have thrown already.
// This line will never be reached as the parser would have thrown already.
throw; throw;
break; break;
} }
buf = trimWhitespaces(buf); buf = trimWhitespaces(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.
encounteredNewDistribution = true;
} }
if (isRewardFile) {
// If not all rows were filled for the last state, we need to insert them.
result.numberOfChoices += lastchoice - ((*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[lastsource] - 1);
// If we skipped some states, we need to reserve empty rows for all their nondeterministic
// choices.
for (uint_fast64_t i = lastsource + 1; i < rewardMatrixInformation->nondeterministicChoiceIndices->size() - 1; ++i) {
result.numberOfChoices += ((*rewardMatrixInformation->nondeterministicChoiceIndices)[i + 1] - (*rewardMatrixInformation->nondeterministicChoiceIndices)[i]);
}
} while (!encounteredEOF && !encounteredNewDistribution);
} }
exit(-1); exit(-1);
@ -229,6 +163,10 @@ namespace storm {
return result; return result;
} }
MarkovAutomataSparseTransitionParser::ResultType MarkovAutomataSparseTransitionParser::secondPass(char* buf, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult, RewardMatrixInformationStruct* rewardMatrixInformation) {
return ResultType();
}
MarkovAutomataSparseTransitionParser::ResultType MarkovAutomataSparseTransitionParser::parseMarkovAutomataTransitions(std::string const& filename, RewardMatrixInformationStruct* rewardMatrixInformation) { MarkovAutomataSparseTransitionParser::ResultType MarkovAutomataSparseTransitionParser::parseMarkovAutomataTransitions(std::string const& filename, RewardMatrixInformationStruct* rewardMatrixInformation) {
/* /*
* Enforce locale where decimal point is '.'. * Enforce locale where decimal point is '.'.
@ -253,10 +191,7 @@ namespace storm {
MappedFile file(filename.c_str()); MappedFile file(filename.c_str());
char* buf = file.data; char* buf = file.data;
FirstPassResult firstPassResult = performFirstPass(buf, lineEndings, rewardMatrixInformation);
return ResultType();
return secondPass(buf, lineEndings, firstPass(buf, lineEndings, rewardMatrixInformation), rewardMatrixInformation);
} }
} }

7
src/parser/MarkovAutomataSparseTransitionParser.h
View File

@ -19,19 +19,20 @@ namespace storm {
struct FirstPassResult { struct FirstPassResult {
FirstPassResult() : numberOfNonzeroEntries(0), numberOfStates(0), numberOfChoices(0) {
FirstPassResult() : numberOfNonzeroEntries(0), highestStateIndex(0), numberOfChoices(0) {
// Intentionally left empty. // Intentionally left empty.
} }
uint_fast64_t numberOfNonzeroEntries; uint_fast64_t numberOfNonzeroEntries;
uint_fast64_t numberOfStates;
uint_fast64_t highestStateIndex;
uint_fast64_t numberOfChoices; uint_fast64_t numberOfChoices;
}; };
static ResultType parseMarkovAutomataTransitions(std::string const& filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr); static ResultType parseMarkovAutomataTransitions(std::string const& filename, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
private: private:
static FirstPassResult performFirstPass(char* buf, SupportedLineEndingsEnum lineEndings, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
static FirstPassResult firstPass(char* buf, SupportedLineEndingsEnum lineEndings, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
static ResultType secondPass(char* buf, SupportedLineEndingsEnum lineEndings, FirstPassResult const& firstPassResult, RewardMatrixInformationStruct* rewardMatrixInformation = nullptr);
}; };
} // namespace parser } // namespace parser

Write Preview
Loading…
Cancel
Save