From cb14f2e771c66864cd580a58badcf7069c56e5eb Mon Sep 17 00:00:00 2001 From: gereon Date: Thu, 23 May 2013 17:52:13 +0200 Subject: [PATCH] Made choiceIndices work in ExplicitModelAdapter, added code to somehow use --symbolic (parse model, show model information) --- src/adapters/ExplicitModelAdapter.cpp | 6 ++++-- src/adapters/ExplicitModelAdapter.h | 1 + src/parser/PrismParser.cpp | 2 +- src/parser/prismparser/PrismGrammar.cpp | 16 ++++++++-------- src/parser/prismparser/PrismGrammar.h | 18 +++++++++--------- src/storm.cpp | 5 ++++- 6 files changed, 27 insertions(+), 21 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 298400acb..177d0f601 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -73,8 +73,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { case storm::ir::Program::MDP: { std::shared_ptr> matrix = this->buildNondeterministicMatrix(); - std::shared_ptr> choiceIndices; - return std::shared_ptr>(new storm::models::Mdp(matrix, stateLabeling, choiceIndices, stateRewards, this->transitionRewards)); + return std::shared_ptr>(new storm::models::Mdp(matrix, stateLabeling, this->choiceIndices, stateRewards, this->transitionRewards)); break; } case storm::ir::Program::CTMDP: @@ -493,9 +492,12 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { this->transitionRewards = std::shared_ptr>(new storm::storage::SparseMatrix(this->numberOfChoices, allStates.size())); this->transitionRewards->initialize(this->numberOfTransitions); } + this->choiceIndices = std::shared_ptr>(new std::vector()); + this->choiceIndices->reserve(allStates.size()); // Build matrix. uint_fast64_t nextRow = 0; for (uint_fast64_t state = 0; state < this->allStates.size(); state++) { + this->choiceIndices->push_back(transitionMap[state].size()); for (auto choice : transitionMap[state]) { for (auto it : choice.second) { result->addNextValue(nextRow, it.first, it.second); diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 1fe2e29a4..d9b66de5f 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -190,6 +190,7 @@ private: std::unordered_map stateToIndexMap; uint_fast64_t numberOfTransitions; uint_fast64_t numberOfChoices; + std::shared_ptr> choiceIndices; std::shared_ptr> transitionRewards; /*! diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 8057eda18..cba3867e7 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -9,7 +9,7 @@ #include "src/utility/OsDetection.h" -#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. #include "src/exceptions/WrongFormatException.h" diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 86f1319b9..ced118dce 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -9,14 +9,14 @@ #include "src/utility/OsDetection.h" -#include "src/parser/PrismParser/Includes.h" -#include "src/parser/PrismParser/BooleanExpressionGrammar.h" -#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h" -#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h" -#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" -#include "src/parser/PrismParser/IntegerExpressionGrammar.h" -#include "src/parser/PrismParser/IdentifierGrammars.h" -#include "src/parser/PrismParser/VariableState.h" +#include "src/parser/prismparser/Includes.h" +#include "src/parser/prismparser/BooleanExpressionGrammar.h" +#include "src/parser/prismparser/ConstBooleanExpressionGrammar.h" +#include "src/parser/prismparser/ConstDoubleExpressionGrammar.h" +#include "src/parser/prismparser/ConstIntegerExpressionGrammar.h" +#include "src/parser/prismparser/IntegerExpressionGrammar.h" +#include "src/parser/prismparser/IdentifierGrammars.h" +#include "src/parser/prismparser/VariableState.h" // Needed for file IO. #include diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index 97033f506..5844659be 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -10,15 +10,15 @@ // All classes of the intermediate representation are used. #include "src/ir/IR.h" -#include "src/parser/PrismParser/Includes.h" -#include "src/parser/PrismParser/Tokens.h" -#include "src/parser/PrismParser/IdentifierGrammars.h" -#include "src/parser/PrismParser/VariableState.h" -#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h" -#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h" -#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" -#include "src/parser/PrismParser/BooleanExpressionGrammar.h" -#include "src/parser/PrismParser/IntegerExpressionGrammar.h" +#include "src/parser/prismparser/Includes.h" +#include "src/parser/prismparser/Tokens.h" +#include "src/parser/prismparser/IdentifierGrammars.h" +#include "src/parser/prismparser/VariableState.h" +#include "src/parser/prismparser/ConstBooleanExpressionGrammar.h" +#include "src/parser/prismparser/ConstDoubleExpressionGrammar.h" +#include "src/parser/prismparser/ConstIntegerExpressionGrammar.h" +#include "src/parser/prismparser/BooleanExpressionGrammar.h" +#include "src/parser/prismparser/IntegerExpressionGrammar.h" // Used for file input. #include diff --git a/src/storm.cpp b/src/storm.cpp index bd2dfff57..76d0f38ca 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -343,7 +343,10 @@ int main(const int argc, const char* argv[]) { } if (s->isSet("symbolic")) { std::string arg = s->getString("symbolic"); - Pr + storm::parser::PrismParser parser; + storm::adapters::ExplicitModelAdapter adapter(parser.parseFile(arg)); + std::shared_ptr> model = adapter.getModel(); + model->printModelInformationToStream(std::cout); } cleanUp();