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

Model building works again (more or less) 

Former-commit-id: fa6843fcdc
main
dehnert 11 years ago
parent
8ec362bb7d
commit
231d2223a9
8 changed files with 70 additions and 40 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 35
      src/adapters/ExplicitModelAdapter.h
  2. 18
      src/parser/PrismParser.cpp
  3. 2
      src/storage/BitVector.cpp
  4. 1
      src/storage/BitVectorHashMap.cpp
  5. 3
      src/storage/expressions/ExprtkExpressionEvaluator.cpp
  6. 48
      src/storage/expressions/ToExprtkStringVisitor.cpp
  7. 2
      src/storage/prism/Assignment.cpp
  8. 1
      src/storage/prism/Update.cpp

35
src/adapters/ExplicitModelAdapter.h
View File

@ -194,14 +194,11 @@ namespace storm {
private:
static void unpackStateIntoEvaluator(storm::storage::BitVector const& currentState, VariableInformation const& variableInformation, storm::expressions::ExprtkExpressionEvaluator& evaluator) {
std::cout << "unpacking state... " << std::endl;
for (auto const& booleanVariable : variableInformation.booleanVariables) {
evaluator.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset));
std::cout << booleanVariable.variable.getName() << " -> " << currentState.get(booleanVariable.bitOffset) << std::endl;
}
for (auto const& integerVariable : variableInformation.integerVariables) {
evaluator.setIntegerValue(integerVariable.variable, currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
std::cout << integerVariable.variable.getName() << " -> " << currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound << std::endl;
}
}
@ -335,6 +332,7 @@ namespace storm {
result.get().push_back(std::move(commands));
}
return result;
}
@ -371,11 +369,13 @@ namespace storm {
uint32_t stateIndex = getOrAddStateIndex(applyUpdate(variableInformation, currentState, update, evaluator), stateInformation, stateQueue);
// Update the choice by adding the probability/target state to it.
choice.addProbability(stateIndex, evaluator.asDouble(update.getLikelihoodExpression()));
ValueType probability = evaluator.asDouble(update.getLikelihoodExpression());
choice.addProbability(stateIndex, probability);
probabilitySum += probability;
}
// Check that the resulting distribution is in fact a distribution.
STORM_LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "'.");
STORM_LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "' (actually sum to " << probabilitySum << ").");
}
}
@ -445,13 +445,11 @@ namespace storm {
for (auto const& stateProbabilityPair : *newTargetStates) {
uint32_t actualIndex = getOrAddStateIndex(stateProbabilityPair.first, stateInformation, stateQueue);
choice.addProbability(actualIndex, stateProbabilityPair.second);
probabilitySum += stateProbabilityPair.second;
}
// Check that the resulting distribution is in fact a distribution.
if (std::abs(1 - probabilitySum) > storm::settings::generalSettings().getPrecision()) {
LOG4CPLUS_ERROR(logger, "Sum of update probabilities do not some to one for some command.");
throw storm::exceptions::WrongFormatException() << "Sum of update probabilities do not some to one for some command.";
}
STORM_LOG_THROW(std::abs(1 - probabilitySum) <= storm::settings::generalSettings().getPrecision(), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
// Dispose of the temporary maps.
delete currentTargetStates;
@ -507,10 +505,10 @@ namespace storm {
for (auto const& integerVariable : variableInformation.integerVariables) {
initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(integerVariable.initialValue - integerVariable.lowerBound));
}
std::cout << "initial state: " << initialState << std::endl;
// Insert the initial state in the global state to index mapping and state queue.
getOrAddStateIndex(initialState, stateInformation, stateQueue);
uint32_t stateIndex = getOrAddStateIndex(initialState, stateInformation, stateQueue);
stateInformation.initialStateIndices.push_back(stateIndex);
// Now explore the current state until there is no more reachable state.
uint_fast64_t currentRow = 0;
@ -520,7 +518,6 @@ namespace storm {
std::size_t currentStateBucket = stateQueue.front();
std::pair<storm::storage::BitVector, uint32_t> stateValuePair = stateInformation.stateToIndexMap.getBucketAndValue(currentStateBucket);
storm::storage::BitVector const& currentState = stateValuePair.first;
std::cout << "current state: " << initialState << std::endl;
unpackStateIntoEvaluator(currentState, variableInformation, evaluator);
// Retrieve all choices for the current state.
@ -679,7 +676,7 @@ namespace storm {
for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound)));
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth);
bitOffset += bitwidth;
variableInformation.integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1;
@ -693,7 +690,7 @@ namespace storm {
for (auto const& integerVariable : module.getIntegerVariables()) {
int_fast64_t lowerBound = integerVariable.getLowerBoundExpression().evaluateAsInt();
int_fast64_t upperBound = integerVariable.getUpperBoundExpression().evaluateAsInt();
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound)));
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
variableInformation.integerVariables.emplace_back(integerVariable.getExpressionVariable(), integerVariable.getInitialValueExpression().evaluateAsInt(), lowerBound, upperBound, bitOffset, bitwidth);
bitOffset += bitwidth;
variableInformation.integerVariableToIndexMap[integerVariable.getExpressionVariable()] = variableInformation.integerVariables.size() - 1;
@ -702,7 +699,6 @@ namespace storm {
// Create the structure for storing the reachable state space.
uint64_t bitsPerState = ((bitOffset / 64) + 1) * 64;
std::cout << "states have " << bitsPerState << " bits" << std::endl;
StateInformation stateInformation(bitsPerState);
// Determine whether we have to combine different choices to one or whether this model can have more than
@ -747,9 +743,8 @@ namespace storm {
result.addAtomicProposition(label.getName());
}
for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getBucketAndValue(stateInformation.reachableStates[index]).first, variableInformation, evaluator);
for (auto const& label : labels) {
unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getValue(stateInformation.reachableStates[index]), variableInformation, evaluator);
// Add label to state, if the corresponding expression is true.
if (evaluator.asBool(label.getStatePredicateExpression())) {
result.addAtomicPropositionToState(label.getName(), index);
@ -759,7 +754,7 @@ namespace storm {
// Also label the initial state with the special label "init".
result.addAtomicProposition("init");
for (auto const& index : stateInformation.initialStateIndices) {
for (auto index : stateInformation.initialStateIndices) {
result.addAtomicPropositionToState("init", index);
}
@ -778,9 +773,9 @@ namespace storm {
std::vector<ValueType> result(stateInformation.reachableStates.size());
for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
result[index] = ValueType(0);
result[index] = storm::utility::zero<ValueType>();
unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getBucketAndValue(stateInformation.reachableStates[index]).first, variableInformation, evaluator);
for (auto const& reward : rewards) {
unpackStateIntoEvaluator(stateInformation.stateToIndexMap.getValue(stateInformation.reachableStates[index]), variableInformation, evaluator);
// Add this reward to the state if the state is included in the state reward.
if (evaluator.asBool(reward.getStatePredicateExpression())) {

18
src/parser/PrismParser.cpp
View File

@ -357,7 +357,13 @@ namespace storm {
storm::prism::Command PrismParser::createCommand(std::string const& actionName, storm::expressions::Expression guardExpression, std::vector<storm::prism::Update> const& updates, GlobalProgramInformation& globalProgramInformation) const {
++globalProgramInformation.currentCommandIndex;
return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, globalProgramInformation.actionIndices[actionName], actionName, guardExpression, updates, this->getFilename());
if (!actionName.empty()) {
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(actionName);
if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
globalProgramInformation.actionIndices[actionName] = globalProgramInformation.actionIndices.size();
}
}
return storm::prism::Command(globalProgramInformation.currentCommandIndex - 1, actionName.empty() ? 0 : globalProgramInformation.actionIndices[actionName], actionName, guardExpression, updates, this->getFilename());
}
storm::prism::Command PrismParser::createCommand(std::string const& actionName, GlobalProgramInformation& globalProgramInformation) const {
@ -490,12 +496,14 @@ namespace storm {
newActionName = renamingPair->second;
}
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
globalProgramInformation.actionIndices[newActionName] = globalProgramInformation.actionIndices.size();
if (!newActionName.empty()) {
auto const& nameIndexPair = globalProgramInformation.actionIndices.find(newActionName);
if (nameIndexPair == globalProgramInformation.actionIndices.end()) {
globalProgramInformation.actionIndices[newActionName] = globalProgramInformation.actionIndices.size();
}
}
commands.emplace_back(globalProgramInformation.currentCommandIndex, globalProgramInformation.actionIndices[newActionName], newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1));
commands.emplace_back(globalProgramInformation.currentCommandIndex, newActionName.empty() ? 0 : globalProgramInformation.actionIndices[newActionName], newActionName, command.getGuardExpression().substitute(expressionRenaming), updates, this->getFilename(), get_line(qi::_1));
++globalProgramInformation.currentCommandIndex;
}

2
src/storage/BitVector.cpp
View File

@ -441,7 +441,7 @@ namespace storm {
}
void BitVector::setFromInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits, uint64_t value) {
STORM_LOG_ASSERT((value >> numberOfBits) == 0, "Integer value to large to fit in the given number of bits.");
STORM_LOG_ASSERT((value >> numberOfBits) == 0, "Integer value too large to fit in the given number of bits.");
uint64_t bucket = bitIndex >> 6;
uint64_t bitIndexInBucket = bitIndex & mod64mask;

1
src/storage/BitVectorHashMap.cpp
View File

@ -81,6 +81,7 @@ namespace storm {
template<class ValueType, class Hash1, class Hash2>
ValueType BitVectorHashMap<ValueType, Hash1, Hash2>::getValue(storm::storage::BitVector const& key) const {
std::cout << "calling getValue with key " << key << std::endl;
std::pair<bool, std::size_t> flagBucketPair = this->findBucket(key);
STORM_LOG_ASSERT(flagBucketPair.first, "Unknown key.");
return flagBucketPair.second;

3
src/storage/expressions/ExprtkExpressionEvaluator.cpp
View File

@ -1,6 +1,8 @@
#include "src/storage/expressions/ExprtkExpressionEvaluator.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/utility/macros.h"
namespace storm {
namespace expressions {
ExprtkExpressionEvaluator::ExprtkExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : manager(manager.getSharedPointer()), booleanValues(manager.getNumberOfBooleanVariables()), integerValues(manager.getNumberOfIntegerVariables()), rationalValues(manager.getNumberOfRationalVariables()) {
@ -52,6 +54,7 @@ namespace storm {
CompiledExpressionType& compiledExpression = result.first->second;
compiledExpression.register_symbol_table(symbolTable);
bool parsingOk = parser.compile(ToExprtkStringVisitor().toString(expression), compiledExpression);
STORM_LOG_ASSERT(parsingOk, "Expression was not properly parsed by ExprTk.");
return compiledExpression;
}

48
src/storage/expressions/ToExprtkStringVisitor.cpp
View File

@ -26,37 +26,37 @@ namespace storm {
boost::any ToExprtkStringVisitor::visit(BinaryBooleanFunctionExpression const& expression) {
switch (expression.getOperatorType()) {
case BinaryBooleanFunctionExpression::OperatorType::And:
stream << "and(";
expression.getFirstOperand()->accept(*this);
stream << ",";
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << " and ";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryBooleanFunctionExpression::OperatorType::Or:
stream << "or(";
expression.getFirstOperand()->accept(*this);
stream << ",";
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << " or ";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryBooleanFunctionExpression::OperatorType::Xor:
stream << "xor(";
expression.getFirstOperand()->accept(*this);
stream << ",";
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << " xor ";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryBooleanFunctionExpression::OperatorType::Implies:
stream << "or(not(";
expression.getFirstOperand()->accept(*this);
stream << "),";
stream << "(not(";
expression.getFirstOperand()->accept(*this);
stream << ") or ";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryBooleanFunctionExpression::OperatorType::Iff:
expression.getFirstOperand()->accept(*this);
stream << "==";
expression.getFirstOperand()->accept(*this);
expression.getSecondOperand()->accept(*this);
break;
}
return boost::any();
@ -65,29 +65,39 @@ namespace storm {
boost::any ToExprtkStringVisitor::visit(BinaryNumericalFunctionExpression const& expression) {
switch (expression.getOperatorType()) {
case BinaryNumericalFunctionExpression::OperatorType::Plus:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << "+";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Minus:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << "-";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Times:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << "*";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Divide:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << "/";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Power:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << "^";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryNumericalFunctionExpression::OperatorType::Max:
stream << "max(";
@ -110,34 +120,46 @@ namespace storm {
boost::any ToExprtkStringVisitor::visit(BinaryRelationExpression const& expression) {
switch (expression.getRelationType()) {
case BinaryRelationExpression::RelationType::Equal:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << "==";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryRelationExpression::RelationType::NotEqual:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << "!=";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryRelationExpression::RelationType::Less:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << "<";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryRelationExpression::RelationType::LessOrEqual:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << "<=";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryRelationExpression::RelationType::Greater:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << ">";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
case BinaryRelationExpression::RelationType::GreaterOrEqual:
stream << "(";
expression.getFirstOperand()->accept(*this);
stream << ">=";
expression.getSecondOperand()->accept(*this);
stream << ")";
break;
}
return boost::any();

2
src/storage/prism/Assignment.cpp
View File

@ -19,7 +19,7 @@ namespace storm {
}
Assignment Assignment::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
return Assignment(this->getVariable(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
return Assignment(this->getVariable(), this->getExpression().substitute(substitution).simplify(), this->getFilename(), this->getLineNumber());
}
std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) {

1
src/storage/prism/Update.cpp
View File

@ -48,6 +48,7 @@ namespace storm {
newAssignments.emplace_back(assignment.substitute(substitution));
}
// FIXME: The expression could be simplified, but 1/K (where K is an int) is then resolved to 0, which is incorrect (for probabilities).
return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute(substitution), newAssignments, this->getFilename(), this->getLineNumber());
}

Write Preview
Loading…
Cancel
Save