From 014ecd85977b3349653826dd28d803af1817652f Mon Sep 17 00:00:00 2001 From: gereon Date: Sun, 28 Apr 2013 16:01:11 +0200 Subject: [PATCH] Fixed some glitches, producing meaningful error if sum of probabilities for a command is not one --- src/adapters/ExplicitModelAdapter.cpp | 25 +++ src/adapters/ExplicitModelAdapter.h | 2 + src/parser/PrismParser.cpp | 40 +++-- src/parser/PrismParser.h | 153 +++++++++--------- src/parser/PrismParser/BaseGrammar.h | 11 ++ .../PrismParser/BooleanExpressionGrammar.cpp | 11 +- .../PrismParser/BooleanExpressionGrammar.h | 3 +- .../PrismParser/IntegerExpressionGrammar.cpp | 5 + .../PrismParser/IntegerExpressionGrammar.h | 1 + src/parser/PrismParser/VariableState.h | 10 +- 10 files changed, 162 insertions(+), 99 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.cpp b/src/adapters/ExplicitModelAdapter.cpp index 7b496b66d..3a8bc878e 100644 --- a/src/adapters/ExplicitModelAdapter.cpp +++ b/src/adapters/ExplicitModelAdapter.cpp @@ -28,6 +28,8 @@ ExplicitModelAdapter::ExplicitModelAdapter(storm::ir::Program program) : program booleanVariables(), integerVariables(), booleanVariableToIndexMap(), integerVariableToIndexMap(), allStates(), stateToIndexMap(), numberOfTransitions(0), numberOfChoices(0), transitionRewards(nullptr), transitionMap() { this->initializeVariables(); + storm::settings::Settings* s = storm::settings::instance(); + this->precision = s->get("precision"); } ExplicitModelAdapter::~ExplicitModelAdapter() { @@ -57,6 +59,11 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { case storm::ir::Program::DTMC: { std::shared_ptr> matrix = this->buildDeterministicMatrix(); + std::cerr << "Row 2: "; + for (const double* val = matrix->beginConstIterator(2); val != matrix->endConstIterator(2); val++) { + std::cerr << *val << ", "; + } + std::cerr << std::endl; return std::shared_ptr(new storm::models::Dtmc(matrix, stateLabeling, stateRewards, this->transitionRewards)); break; } @@ -306,6 +313,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { // Add a new map and get pointer. res.emplace_back(); std::map* states = &res.back().second; + double probSum = 0; // Iterate over all updates. for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { @@ -313,6 +321,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { storm::ir::Update const& update = command.getUpdate(k); uint_fast64_t newStateId = this->getOrAddStateId(this->applyUpdate(state, update)); + probSum += update.getLikelihoodExpression()->getValueAsDouble(state); // Check, if we already know this state, add up probabilities for every state. auto stateIt = states->find(newStateId); if (stateIt == states->end()) { @@ -322,6 +331,10 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { (*states)[newStateId] += update.getLikelihoodExpression()->getValueAsDouble(state); } } + if (std::abs(1 - probSum) > this->precision) { + LOG4CPLUS_ERROR(logger, "Sum of update probabilities should be one for command:\n\t" << command.toString()); + throw storm::exceptions::WrongFileFormatException() << "Sum of update probabilities should be one for command:\n\t" << command.toString(); + } } } } @@ -349,6 +362,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { // Iterate over all commands within this module. for (storm::ir::Command command : module) { // Iterate over all updates of this command. + double probSum = 0; for (uint_fast64_t k = 0; k < command.getNumberOfUpdates(); ++k) { storm::ir::Update const update = command.getUpdate(k); @@ -356,6 +370,7 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { for (auto it : resultStates) { // Apply the new update and get resulting state. StateType* newState = this->applyUpdate(it.first, update); + probSum += update.getLikelihoodExpression()->getValueAsDouble(it.first); // Insert the new state into newStates array. // Take care of calculation of likelihood, combine identical states. auto s = newStates.find(newState); @@ -366,6 +381,10 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { } } } + if (std::abs(1 - probSum) > this->precision) { + LOG4CPLUS_ERROR(logger, "Sum of update probabilities should be one for command:\n\t" << command.toString()); + throw storm::exceptions::WrongFileFormatException() << "Sum of update probabilities should be one for command:\n\t" << command.toString(); + } } for (auto it: resultStates) { delete it.first; @@ -437,6 +456,12 @@ ExplicitModelAdapter::~ExplicitModelAdapter() { } } } + if (state < 5) { + std::cerr << "From " << state << std::endl; + for (auto it: map) { + std::cerr << "\t" << it.first << ": " << it.second << std::endl; + } + } // Scale probabilities by number of choices. double factor = 1.0 / transitionMap[state].size(); for (auto it : map) { diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index f97f76c5e..272d79c10 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -60,6 +60,8 @@ public: private: + double precision; + // First some generic routines to operate on states. /*! diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 1df11819e..4a9678827 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -56,10 +56,12 @@ namespace parser { mapping[name] = value; } void PrismParser::PrismGrammar::addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { + //std::cout << "Adding int assignment for " << variable << std::endl; this->state->assignedLocalIntegerVariables_.add(variable, variable); mapping[variable] = Assignment(variable, value); } void PrismParser::PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { + //std::cout << "Adding bool assignment for " << variable << std::endl; this->state->assignedLocalBooleanVariables_.add(variable, variable); mapping[variable] = Assignment(variable, value); } @@ -81,6 +83,21 @@ namespace parser { return res; } + void PrismParser::PrismGrammar::createIntegerVariable(const std::string name, std::shared_ptr lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids) { + //std::cout << "Creating int " << name << " = " << init << std::endl; + uint_fast64_t id = this->state->addIntegerVariable(name, lower, upper, init); + vars.emplace_back(id, name, lower, upper, init); + varids[name] = id; + this->state->localIntegerVariables_.add(name, name); + } + void PrismParser::PrismGrammar::createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids) { + //std::cout << "Creating bool " << name << std::endl; + uint_fast64_t id = this->state->addBooleanVariable(name, init); + vars.emplace_back(id, name, init); + varids[name] = id; + this->state->localBooleanVariables_.add(name, name); + } + StateReward createStateReward(std::shared_ptr guard, std::shared_ptr reward) { return StateReward(guard, reward); } @@ -140,7 +157,8 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type assignmentDefinition.name("assignment"); assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; assignmentDefinitionList.name("assignment list"); - updateDefinition = (prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)]; + updateDefinition = ( + prism::ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&createUpdate, qi::_1, qi::_a, qi::_b)]; updateDefinition.name("update"); updateListDefinition = +updateDefinition % "+"; updateListDefinition.name("update list"); @@ -154,22 +172,13 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type // This block defines all entities that are needed for parsing variable definitions. booleanVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > prism::ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) [ - //qi::_a = phoenix::bind(&VariableState::addBooleanVariable, *this->state.get(), qi::_1), - qi::_a = phoenix::bind(&storm::parser::prism::VariableState::addBooleanVariable, *this->state, qi::_1, qi::_b), - phoenix::push_back(qi::_r1, phoenix::construct(qi::_a, phoenix::val(qi::_1), qi::_b)), - phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, qi::_a)), - phoenix::bind(this->state->localBooleanVariables_.add, qi::_1, qi::_1) + phoenix::bind(&PrismParser::PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2) ]; booleanVariableDefinition.name("boolean variable declaration"); - integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; - integerLiteralExpression.name("integer literal"); - integerVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > integerLiteralExpression > qi::lit("..") > integerLiteralExpression > qi::lit("]") > -(qi::lit("init") > prism::ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + integerVariableDefinition = (prism::FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > prism::ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > prism::ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > prism::ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) [ - qi::_a = phoenix::bind(&storm::parser::prism::VariableState::addIntegerVariable, *this->state, qi::_1, qi::_2, qi::_3, qi::_b), - phoenix::push_back(qi::_r1, phoenix::construct(qi::_a, qi::_1, qi::_2, qi::_3, qi::_b)), - phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, qi::_a)), - phoenix::bind(this->state->localIntegerVariables_.add, qi::_1, qi::_1) + phoenix::bind(&PrismParser::PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2) ]; integerVariableDefinition.name("integer variable declaration"); variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4)); @@ -228,6 +237,11 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type void PrismParser::PrismGrammar::prepareForSecondRun() { this->state->prepareForSecondRun(); + prism::BooleanExpressionGrammar::secondRun(); + prism::ConstBooleanExpressionGrammar::secondRun(); + prism::ConstDoubleExpressionGrammar::secondRun(); + prism::ConstIntegerExpressionGrammar::secondRun(); + prism::IntegerExpressionGrammar::secondRun(); } /*! diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 10cdeb895..32a797adf 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -64,82 +64,83 @@ public: private: - std::shared_ptr state; - - // The starting point of the grammar. - qi::rule< - Iterator, - Program(), - qi::locals< - std::map>, - std::map>, - std::map>, - std::map, - std::map> - >, - Skipper> start; - qi::rule modelTypeDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; - qi::rule(), Skipper> moduleDefinitionList; - - // Rules for module definition. - qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; - qi::rule>, Skipper> moduleRenaming; - - // Rules for variable definitions. - qi::rule(), Skipper> integerLiteralExpression; - qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; - qi::rule&, std::map&), qi::locals>, Skipper> booleanVariableDefinition; - qi::rule&, std::map&), qi::locals>, Skipper> integerVariableDefinition; - - // Rules for command definitions. - qi::rule, Skipper> commandDefinition; - qi::rule(), Skipper> updateListDefinition; - qi::rule, std::map>, Skipper> updateDefinition; - qi::rule&, std::map&), Skipper> assignmentDefinitionList; - qi::rule&, std::map&), Skipper> assignmentDefinition; - - // Rules for variable/command names. - qi::rule commandName; - qi::rule unassignedLocalBooleanVariableName; - qi::rule unassignedLocalIntegerVariableName; - - // Rules for reward definitions. - qi::rule&), Skipper> rewardDefinitionList; - qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; - qi::rule stateRewardDefinition; - qi::rule, Skipper> transitionRewardDefinition; - - // Rules for label definitions. - qi::rule>&), Skipper> labelDefinitionList; - qi::rule>&), Skipper> labelDefinition; - - // Rules for constant definitions. - qi::rule(), Skipper> constantDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; - qi::rule(), Skipper> definedConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; - qi::rule(), Skipper> definedBooleanConstantDefinition; - qi::rule(), Skipper> definedIntegerConstantDefinition; - qi::rule(), Skipper> definedDoubleConstantDefinition; - - // Rules for variable recognition. - qi::rule(), Skipper> booleanVariableCreatorExpression; - qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; - - storm::parser::prism::keywordsStruct keywords_; - storm::parser::prism::modelTypeStruct modelType_; - storm::parser::prism::relationalOperatorStruct relations_; - - std::shared_ptr addIntegerConstant(const std::string& name, const std::shared_ptr value); - void addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping); - void addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); - void addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); - Module renameModule(const std::string& name, const std::string& oldname, std::map& mapping); - Module createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands); - + std::shared_ptr state; + + // The starting point of the grammar. + qi::rule< + Iterator, + Program(), + qi::locals< + std::map>, + std::map>, + std::map>, + std::map, + std::map> + >, + Skipper> start; + qi::rule modelTypeDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; + qi::rule(), Skipper> moduleDefinitionList; + + // Rules for module definition. + qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; + qi::rule>, Skipper> moduleRenaming; + + // Rules for variable definitions. + qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; + qi::rule&, std::map&), qi::locals>, Skipper> booleanVariableDefinition; + qi::rule&, std::map&), qi::locals>, Skipper> integerVariableDefinition; + + // Rules for command definitions. + qi::rule, Skipper> commandDefinition; + qi::rule(), Skipper> updateListDefinition; + qi::rule, std::map>, Skipper> updateDefinition; + qi::rule&, std::map&), Skipper> assignmentDefinitionList; + qi::rule&, std::map&), Skipper> assignmentDefinition; + + // Rules for variable/command names. + qi::rule commandName; + qi::rule unassignedLocalBooleanVariableName; + qi::rule unassignedLocalIntegerVariableName; + + // Rules for reward definitions. + qi::rule&), Skipper> rewardDefinitionList; + qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; + qi::rule stateRewardDefinition; + qi::rule, Skipper> transitionRewardDefinition; + + // Rules for label definitions. + qi::rule>&), Skipper> labelDefinitionList; + qi::rule>&), Skipper> labelDefinition; + + // Rules for constant definitions. + qi::rule(), Skipper> constantDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; + qi::rule(), Skipper> definedConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; + qi::rule(), Skipper> definedBooleanConstantDefinition; + qi::rule(), Skipper> definedIntegerConstantDefinition; + qi::rule(), Skipper> definedDoubleConstantDefinition; + + // Rules for variable recognition. + qi::rule(), Skipper> booleanVariableCreatorExpression; + qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; + + storm::parser::prism::keywordsStruct keywords_; + storm::parser::prism::modelTypeStruct modelType_; + storm::parser::prism::relationalOperatorStruct relations_; + + std::shared_ptr addIntegerConstant(const std::string& name, const std::shared_ptr value); + void addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping); + void addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); + void addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); + Module renameModule(const std::string& name, const std::string& oldname, std::map& mapping); + Module createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands); + + void createIntegerVariable(const std::string name, std::shared_ptr lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids); + void createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids); }; private: diff --git a/src/parser/PrismParser/BaseGrammar.h b/src/parser/PrismParser/BaseGrammar.h index bcc5f3d44..0846eb12c 100644 --- a/src/parser/PrismParser/BaseGrammar.h +++ b/src/parser/PrismParser/BaseGrammar.h @@ -24,10 +24,18 @@ namespace prism { static T& instance(std::shared_ptr& state = nullptr) { if (BaseGrammar::instanceObject == nullptr) { BaseGrammar::instanceObject = std::shared_ptr(new T(state)); + if (!state->firstRun) BaseGrammar::instanceObject->secondRun(); } return *BaseGrammar::instanceObject; } + static void secondRun() { + if (BaseGrammar::instanceObject != nullptr) { + BaseGrammar::instanceObject->prepareSecondRun(); + } + + } + std::shared_ptr createBoolLiteral(const bool value) { return std::shared_ptr(new BooleanLiteral(value)); } @@ -70,6 +78,7 @@ namespace prism { return std::shared_ptr(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT)); } std::shared_ptr createAnd(std::shared_ptr left, std::shared_ptr right) { + //std::cerr << "Creating " << left->toString() << " & " << right->toString() << std::endl; return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND)); } std::shared_ptr createOr(std::shared_ptr left, std::shared_ptr right) { @@ -82,11 +91,13 @@ namespace prism { return state->getIntegerVariable(name); } + virtual void prepareSecondRun() {} protected: std::shared_ptr state; private: static std::shared_ptr instanceObject; + static bool inSecondRun; }; template diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.cpp b/src/parser/PrismParser/BooleanExpressionGrammar.cpp index 101db9cce..00ca2fe40 100644 --- a/src/parser/PrismParser/BooleanExpressionGrammar.cpp +++ b/src/parser/PrismParser/BooleanExpressionGrammar.cpp @@ -7,10 +7,10 @@ namespace storm { namespace parser { namespace prism { -BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr& state) - : BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) { + BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr& state) + : BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) { - booleanExpression %= orExpression; + booleanExpression %= orExpression; booleanExpression.name("boolean expression"); orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)]; @@ -32,6 +32,11 @@ BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptrstate->booleanVariables_; + booleanVariableExpression.name("boolean variable"); + } + } } } \ No newline at end of file diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.h b/src/parser/PrismParser/BooleanExpressionGrammar.h index 9d14c5ec3..9e976e64d 100644 --- a/src/parser/PrismParser/BooleanExpressionGrammar.h +++ b/src/parser/PrismParser/BooleanExpressionGrammar.h @@ -22,7 +22,8 @@ namespace prism { class BooleanExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { public: BooleanExpressionGrammar(std::shared_ptr& state); - + virtual void prepareSecondRun(); + private: qi::rule(), Skipper, Unused> booleanExpression; qi::rule(), Skipper> orExpression; diff --git a/src/parser/PrismParser/IntegerExpressionGrammar.cpp b/src/parser/PrismParser/IntegerExpressionGrammar.cpp index 89933aeb3..e0e363030 100644 --- a/src/parser/PrismParser/IntegerExpressionGrammar.cpp +++ b/src/parser/PrismParser/IntegerExpressionGrammar.cpp @@ -26,6 +26,11 @@ namespace prism { integerVariableExpression.name("integer variable"); } + void IntegerExpressionGrammar::prepareSecondRun() { + integerVariableExpression = this->state->integerVariables_; + integerVariableExpression.name("integer variable"); + } + } } } \ No newline at end of file diff --git a/src/parser/PrismParser/IntegerExpressionGrammar.h b/src/parser/PrismParser/IntegerExpressionGrammar.h index 5c253e437..0f44b0d01 100644 --- a/src/parser/PrismParser/IntegerExpressionGrammar.h +++ b/src/parser/PrismParser/IntegerExpressionGrammar.h @@ -22,6 +22,7 @@ namespace prism { class IntegerExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { public: IntegerExpressionGrammar(std::shared_ptr& state); + virtual void prepareSecondRun(); private: qi::rule(), Skipper, Unused> integerExpression; diff --git a/src/parser/PrismParser/VariableState.h b/src/parser/PrismParser/VariableState.h index e6c99d9ab..e94d44056 100644 --- a/src/parser/PrismParser/VariableState.h +++ b/src/parser/PrismParser/VariableState.h @@ -45,13 +45,12 @@ public: localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr init) { - //std::cerr << "adding boolean variable " << name << std::endl; if (firstRun) { std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name)); this->booleanVariables_.add(name, varExpr); this->booleanVariableNames_.add(name, name); this->nextBooleanVariableIndex++; - return this->nextBooleanVariableIndex-1; + return varExpr->getVariableIndex(); } else { std::shared_ptr res = this->booleanVariables_.at(name); if (res != nullptr) { @@ -70,7 +69,7 @@ public: this->integerVariables_.add(name, varExpr); this->integerVariableNames_.add(name, name); this->nextIntegerVariableIndex++; - return this->nextIntegerVariableIndex-1; + return varExpr->getVariableIndex(); } else { std::shared_ptr res = this->integerVariables_.at(name); if (res != nullptr) { @@ -83,7 +82,6 @@ public: } std::shared_ptr getBooleanVariable(const std::string& name) { - //std::cerr << "getting boolen variable " << name << std::endl; std::shared_ptr res = this->booleanVariables_.at(name); if (res != nullptr) { return res; @@ -91,7 +89,7 @@ public: if (firstRun) { return std::shared_ptr(new VariableExpression(BaseExpression::bool_, std::numeric_limits::max(), "bool", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); } else { - std::cerr << "Variable " << name << " was not created in first run" << std::endl; + std::cerr << "bool Variable " << name << " was not created in first run" << std::endl; return std::shared_ptr(nullptr); } } @@ -106,7 +104,7 @@ public: if (firstRun) { return std::shared_ptr(new VariableExpression(BaseExpression::int_, std::numeric_limits::max(), "int", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); } else { - std::cerr << "Variable " << name << " was not created in first run" << std::endl; + std::cerr << "int Variable " << name << " was not created in first run" << std::endl; return std::shared_ptr(nullptr); } }