fixed gmp dependency (lib), fixed parser to reject formulas that appear later in the PRISM file

resources/3rdparty/CMakeLists.txt

@@ -319,10 +319,11 @@ if (ENABLE_MSAT)
     list(APPEND STORM_LINK_LIBRARIES "mathsat")
     if(GMP_FOUND)
         include_directories("${GMP_INCLUDE_DIR}")
-        list(APPEND STORM_LINK_LIBRARIES "gmp")
+        list(APPEND STORM_LINK_LIBRARIES ${GMP_LIBRARY})
     elseif(MPIR_FOUND)
         include_directories("${GMP_INCLUDE_DIR}")
-        list(APPEND STORM_LINK_LIBRARIES "mpir" "mpirxx")
+        list(APPEND STORM_LINK_LIBRARIES ${GMP_MPIR_LIBRARY})
+        list(APPEND STORM_LINK_LIBRARIES ${GMP_MPIRXX_LIBRARY})
     else(GMP_FOUND)
         message(FATAL_ERROR "GMP is required for MathSAT, but was not found!")
     endif(GMP_FOUND)

src/storm/parser/PrismParser.cpp

@@ -420,11 +420,11 @@ namespace storm {
         }
         
         storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) {
-            if (!this->secondRun) {
+            // Only register formula in second run. This prevents the parser from accepting formulas that depend on future
+            // formulas.
+            if (this->secondRun) {
                 STORM_LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << formulaName << "'.");
                 this->identifiers_.add(formulaName, expression);
-            } else {
-                this->identifiers_.at(formulaName) = expression;
             }
             return storm::prism::Formula(formulaName, expression, this->getFilename());
         }

src/storm/storage/prism/Constant.cpp

@@ -4,11 +4,11 @@
 
 namespace storm {
     namespace prism {
-        Constant::Constant(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), defined(true), expression(expression) {
+        Constant::Constant(storm::expressions::Variable const& variable, storm::expressions::Expression const& expression, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), expression(expression) {
             // Intentionally left empty.
         }
         
-        Constant::Constant(storm::expressions::Variable const& variable, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), defined(false), expression() {
+        Constant::Constant(storm::expressions::Variable const& variable, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), variable(variable), expression() {
             // Intentionally left empty.
         }
         
@@ -25,7 +25,7 @@ namespace storm {
         }
         
         bool Constant::isDefined() const {
-            return this->defined;
+            return this->expression.isInitialized();
         }
         
         storm::expressions::Expression const& Constant::getExpression() const {

src/storm/storage/prism/Constant.h

@@ -90,9 +90,6 @@ namespace storm {
             // The expression variable associated with the constant.
             storm::expressions::Variable variable;
             
-            // A flag that stores whether or not the constant is defined.
-            bool defined;
-            
             // The expression that defines the constant (in case it is defined).
             storm::expressions::Expression expression;
         };

src/storm/storage/prism/Program.cpp

@@ -1292,18 +1292,29 @@ namespace storm {
                     }
                 }
                 
+                for (auto const& variable : module.getBooleanVariables()) {
+                    if (booleanVars.find(variable.getExpressionVariable()) != booleanVars.end()) {
+                        if (variable.hasInitialValue()) {
+                            newConstants.emplace_back(variable.getExpressionVariable(), variable.getInitialValueExpression());
+                        } else {
+                            newBooleanVars.push_back(variable);
+                        }
+                    }
+                }
+                for (auto const& variable : module.getIntegerVariables()) {
+                    if (integerVars.find(variable.getExpressionVariable()) != integerVars.end()) {
+                        if (variable.hasInitialValue()) {
+                            newConstants.emplace_back(variable.getExpressionVariable(), variable.getInitialValueExpression());
+                        } else {
+                            newIntegerVars.push_back(variable);
+                        }
+                    }
+                }
+                
                 newModules.emplace_back(module.getName(), newBooleanVars, newIntegerVars, newCommands);
                 
                 // Determine the set of action indices that have been deleted entirely.
                 std::set_difference(module.getSynchronizingActionIndices().begin(), module.getSynchronizingActionIndices().end(), newModules.back().getSynchronizingActionIndices().begin(), newModules.back().getSynchronizingActionIndices().end(), std::inserter(actionIndicesToDelete, actionIndicesToDelete.begin()));
-                
-                for (auto const& entry : booleanVars) {
-                    newConstants.emplace_back(entry.first, entry.second);
-                }
-                
-                for (auto const& entry : integerVars) {
-                    newConstants.emplace_back(entry.first, entry.second);
-                }
             }
             
             // If we have to delete whole actions, do so now.

src/storm/utility/dd.cpp

@@ -11,6 +11,9 @@ namespace storm {
             
             template <storm::dd::DdType Type>
             storm::dd::Bdd<Type> computeReachableStates(storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& transitions, std::set<storm::expressions::Variable> const& rowMetaVariables, std::set<storm::expressions::Variable> const& columnMetaVariables) {
+
+                STORM_LOG_TRACE("Computing reachable states: transition matrix BDD has " << transitions.getNodeCount() << " node(s) and " << transitions.getNonZeroCount() << " non-zero(s), " << initialStates.getNonZeroCount() << " initial states).");
+
                 auto start = std::chrono::high_resolution_clock::now();
                 storm::dd::Bdd<Type> reachableStates = initialStates;
                 
@@ -30,6 +33,7 @@ namespace storm {
                     reachableStates |= newReachableStates;
 
                     ++iteration;
+                    STORM_LOG_TRACE("Iteration " << iteration << " of reachability computation completed: " << reachableStates.getNonZeroCount() << " reachable states found.");
                 } while (changed);
 
                 auto end = std::chrono::high_resolution_clock::now();