Fix to grammar to allow for empty probability in updates.

Former-commit-id: d13a5297a9

src/parser/prismparser/PrismGrammar.cpp

@@ -179,7 +179,7 @@ namespace storm {
                 assignmentDefinition.name("assignment");
                 assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
                 assignmentDefinitionList.name("assignment list");
-                updateDefinition = ((ConstDoubleExpressionGrammar::instance(this->state) | qi::attr(phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<storm::ir::expressions::DoubleLiteralExpression>(1)))) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
+                updateDefinition = ((ConstDoubleExpressionGrammar::instance(this->state) | qi::attr(phoenix::construct<std::shared_ptr<BaseExpression>>(phoenix::new_<storm::ir::expressions::DoubleLiteralExpression>(1)))) >> qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
                 updateDefinition.name("update");
                 updateListDefinition = +updateDefinition % "+";
                 updateListDefinition.name("update list");

src/storm.cpp

@@ -355,14 +355,14 @@ int main(const int argc, const char* argv[]) {
             // Enable the following lines to test the SMTMinimalCommandSetGenerator.
             if (model->getType() == storm::models::MDP) {
                 std::shared_ptr<storm::models::Mdp<double>> labeledMdp = model->as<storm::models::Mdp<double>>();
-//                storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
-//                storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
-//                storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
-//                std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true);
+                storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished");
+                storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1");
+                storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States;
+                std::set<uint_fast64_t> labels = storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.4, true);
                 
-                storm::storage::BitVector const& collisionStates = labeledMdp->getLabeledStates("collision_max_backoff");
-                storm::storage::BitVector const& deliveredStates = labeledMdp->getLabeledStates("all_delivered");
-                std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, ~collisionStates, deliveredStates, 0.5, true, true);
+//                storm::storage::BitVector const& collisionStates = labeledMdp->getLabeledStates("collision_max_backoff");
+//                storm::storage::BitVector const& deliveredStates = labeledMdp->getLabeledStates("all_delivered");
+//                std::set<uint_fast64_t> labels = storm::counterexamples::MILPMinimalLabelSetGenerator<double>::getMinimalLabelSet(*labeledMdp, ~collisionStates, deliveredStates, 0.5, true, true);
             }
 		}