Browse Source

Fixed errors due to merging.

main
gereon 12 years ago
parent
commit
aafdbf7671
  1. 13
      src/adapters/ExplicitModelAdapter.cpp
  2. 2
      src/adapters/ExplicitModelAdapter.h
  3. 4
      src/adapters/SymbolicModelAdapter.h
  4. 4
      src/parser/PrismParser.cpp
  5. 3
      src/parser/PrismParser/PrismGrammar.cpp
  6. 2
      src/storm.cpp

13
src/adapters/ExplicitModelAdapter.cpp

@ -38,7 +38,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
this->clearInternalState(); this->clearInternalState();
} }
std::shared_ptr<storm::models::AbstractModel> ExplicitModelAdapter::getModel(std::string const & rewardModelName) {
std::shared_ptr<storm::models::AbstractModel<double>> ExplicitModelAdapter::getModel(std::string const & rewardModelName) {
this->buildTransitionMap(); this->buildTransitionMap();
@ -61,24 +61,25 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
case storm::ir::Program::DTMC: case storm::ir::Program::DTMC:
{ {
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildDeterministicMatrix(); std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildDeterministicMatrix();
return std::shared_ptr<storm::models::AbstractModel>(new storm::models::Dtmc<double>(matrix, stateLabeling, stateRewards, this->transitionRewards));
return std::shared_ptr<storm::models::AbstractModel<double>>(new storm::models::Dtmc<double>(matrix, stateLabeling, stateRewards, this->transitionRewards));
break; break;
} }
case storm::ir::Program::CTMC: case storm::ir::Program::CTMC:
{ {
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildDeterministicMatrix(); std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildDeterministicMatrix();
return std::shared_ptr<storm::models::AbstractModel>(new storm::models::Ctmc<double>(matrix, stateLabeling, stateRewards, this->transitionRewards));
return std::shared_ptr<storm::models::AbstractModel<double>>(new storm::models::Ctmc<double>(matrix, stateLabeling, stateRewards, this->transitionRewards));
break; break;
} }
case storm::ir::Program::MDP: case storm::ir::Program::MDP:
{ {
std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildNondeterministicMatrix(); std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = this->buildNondeterministicMatrix();
return std::shared_ptr<storm::models::AbstractModel>(new storm::models::Mdp<double>(matrix, stateLabeling, stateRewards, this->transitionRewards));
std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices;
return std::shared_ptr<storm::models::AbstractModel<double>>(new storm::models::Mdp<double>(matrix, stateLabeling, choiceIndices, stateRewards, this->transitionRewards));
break; break;
} }
case storm::ir::Program::CTMDP: case storm::ir::Program::CTMDP:
// Todo // Todo
//return std::shared_ptr<storm::models::AbstractModel>(new storm::models::Ctmdp<double>(matrix, stateLabeling, stateRewards, transitionRewardMatrix));
//return std::shared_ptr<storm::models::AbstractModel<double>>(new storm::models::Ctmdp<double>(matrix, stateLabeling, stateRewards, transitionRewardMatrix));
break; break;
default: default:
LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: We can't handle this model type."); LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: We can't handle this model type.");
@ -86,7 +87,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() {
break; break;
} }
return std::shared_ptr<storm::models::AbstractModel>(nullptr);
return std::shared_ptr<storm::models::AbstractModel<double>>(nullptr);
} }
void ExplicitModelAdapter::setValue(StateType* const state, uint_fast64_t const index, bool const value) { void ExplicitModelAdapter::setValue(StateType* const state, uint_fast64_t const index, bool const value) {

2
src/adapters/ExplicitModelAdapter.h

@ -56,7 +56,7 @@ public:
ExplicitModelAdapter(storm::ir::Program program); ExplicitModelAdapter(storm::ir::Program program);
~ExplicitModelAdapter(); ~ExplicitModelAdapter();
std::shared_ptr<storm::models::AbstractModel> getModel(std::string const & rewardModelName = "");
std::shared_ptr<storm::models::AbstractModel<double>> getModel(std::string const & rewardModelName = "");
private: private:

4
src/adapters/SymbolicModelAdapter.h

@ -8,7 +8,7 @@
#ifndef STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ #ifndef STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_
#define STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ #define STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_
#include "src/exceptions/WrongFileFormatException.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/utility/CuddUtility.h" #include "src/utility/CuddUtility.h"
#include "SymbolicExpressionAdapter.h" #include "SymbolicExpressionAdapter.h"
@ -255,7 +255,7 @@ private:
storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j); storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j);
uint_fast64_t integerRange = integerVariable.getUpperBound()->getValueAsInt(nullptr) - integerVariable.getLowerBound()->getValueAsInt(nullptr); uint_fast64_t integerRange = integerVariable.getUpperBound()->getValueAsInt(nullptr) - integerVariable.getLowerBound()->getValueAsInt(nullptr);
if (integerRange <= 0) { if (integerRange <= 0) {
throw storm::exceptions::WrongFileFormatException() << "Range of variable "
throw storm::exceptions::WrongFormatException() << "Range of variable "
<< integerVariable.getName() << " is empty or negativ."; << integerVariable.getName() << " is empty or negativ.";
} }
uint_fast64_t numberOfDecisionDiagramVariables = static_cast<uint_fast64_t>(std::ceil(std::log2(integerRange))); uint_fast64_t numberOfDecisionDiagramVariables = static_cast<uint_fast64_t>(std::ceil(std::log2(integerRange)));

4
src/parser/PrismParser.cpp

@ -12,7 +12,7 @@
#include "src/parser/PrismParser/PrismGrammar.h" #include "src/parser/PrismParser/PrismGrammar.h"
// If the parser fails due to ill-formed data, this exception is thrown. // If the parser fails due to ill-formed data, this exception is thrown.
#include "src/exceptions/WrongFileFormatException.h"
#include "src/exceptions/WrongFormatException.h"
// Needed for file IO. // Needed for file IO.
#include <fstream> #include <fstream>
@ -117,7 +117,7 @@ storm::ir::Program PrismParser::parse(std::istream& inputStream, std::string con
grammar.resetGrammars(); grammar.resetGrammars();
// Now propagate exception. // Now propagate exception.
throw storm::exceptions::WrongFileFormatException() << msg.str();
throw storm::exceptions::WrongFormatException() << msg.str();
} }
return result; return result;

3
src/parser/PrismParser/PrismGrammar.cpp

@ -18,9 +18,6 @@
#include "src/parser/PrismParser/IdentifierGrammars.h" #include "src/parser/PrismParser/IdentifierGrammars.h"
#include "src/parser/PrismParser/VariableState.h" #include "src/parser/PrismParser/VariableState.h"
// If the parser fails due to ill-formed data, this exception is thrown.
#include "src/exceptions/WrongFileFormatException.h"
// Needed for file IO. // Needed for file IO.
#include <fstream> #include <fstream>
#include <iomanip> #include <iomanip>

2
src/storm.cpp

@ -27,7 +27,7 @@
#include "src/modelchecker/GmmxxMdpPrctlModelChecker.h" #include "src/modelchecker/GmmxxMdpPrctlModelChecker.h"
#include "src/parser/AutoParser.h" #include "src/parser/AutoParser.h"
#include "src/parser/PrctlParser.h" #include "src/parser/PrctlParser.h"
#include "src/solver/GraphAnalyzer.h"
//#include "src/solver/GraphAnalyzer.h"
#include "src/utility/Settings.h" #include "src/utility/Settings.h"
#include "src/utility/ErrorHandling.h" #include "src/utility/ErrorHandling.h"
#include "src/formula/Prctl.h" #include "src/formula/Prctl.h"

Loading…
Cancel
Save