reenabled parametric solving after merge

Former-commit-id: 6e81008932

CMakeLists.txt

@@ -32,7 +32,7 @@ set(Z3_ROOT "" CACHE STRING "The root directory of Z3 (if available).")
 set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.")
 set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.")
 set(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory.")
-option(PARAMETRIC_SYSTEMS "Sets whether models with parameters are supported." OFF)
+option(PARAMETRIC_SYSTEMS "Sets whether models with parameters are supported." ON)
 #############################################################
 ##
 ##	Inclusion of required libraries
@@ -341,6 +341,11 @@ add_library(storm ${STORM_SOURCES_WITHOUT_MAIN} ${STORM_HEADERS})
 add_executable(storm-main ${STORM_MAIN_FILE})
 target_link_libraries(storm-main storm)
 set_target_properties(storm-main PROPERTIES OUTPUT_NAME "storm")
+if(PARAMETRIC_SYSTEMS)
+	add_executable(storm-main-param ${STORM_PARAMETRIC_MAIN_FILE})
+	target_link_libraries(storm-main-param storm)
+	set_target_properties(storm-main-param PROPERTIES OUTPUT_NAME "pstorm")
+endif()
 add_executable(storm-functional-tests ${STORM_FUNCTIONAL_TEST_MAIN_FILE} ${STORM_FUNCTIONAL_TEST_FILES})
 target_link_libraries(storm-functional-tests storm)
 add_executable(storm-performance-tests ${STORM_PERFORMANCE_TEST_MAIN_FILE} ${STORM_PERFORMANCE_TEST_FILES})

src/stormParametric.cpp

@@ -7,6 +7,8 @@
 #include "src/utility/macros.h"
 #include "src/utility/cli.h"
 
+#include "src/modelchecker/reachability/SparseSccModelChecker.h"
+#include "src/storage/parameters.h"
 /*!
  * Main entry point of the executable storm.
  */
@@ -20,7 +22,27 @@ int main(const int argc, const char** argv) {
         }
         
         // From this point on we are ready to carry out the actual computations.
-        
+        // Program Translation Time Measurement, Start
+        std::chrono::high_resolution_clock::time_point programTranslationStart = std::chrono::high_resolution_clock::now();
+
+        // First, we build the model using the given symbolic model description and constant definitions.
+        std::string const& programFile = storm::settings::generalSettings().getSymbolicModelFilename();
+        std::string const& constants = storm::settings::generalSettings().getConstantDefinitionString();
+        storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
+        std::shared_ptr<storm::models::AbstractModel<storm::RationalFunction>> model = storm::adapters::ExplicitModelAdapter<storm::RationalFunction>::translateProgram(program, constants);
+
+        // Program Translation Time Measurement, End
+        std::chrono::high_resolution_clock::time_point programTranslationEnd = std::chrono::high_resolution_clock::now();
+        std::cout << "Parsing and translating the Symbolic Input took " << std::chrono::duration_cast<std::chrono::milliseconds>(programTranslationEnd - programTranslationStart).count() << " milliseconds." << std::endl;
+
+        storm::modelchecker::reachability::SparseSccModelChecker<storm::RationalFunction> modelChecker;
+        storm::storage::BitVector trueStates(model->getNumberOfStates(), true);
+        storm::storage::BitVector targetStates = model->getLabeledStates("observe0Greater1");
+//            storm::storage::BitVector targetStates = model->getLabeledStates("one");
+//            storm::storage::BitVector targetStates = model->getLabeledStates("elected");
+        storm::RationalFunction value = modelChecker.computeReachabilityProbability(*model->as<storm::models::Dtmc<storm::RationalFunction>>(), trueStates, targetStates);
+        std::cout << "computed value " << value << std::endl;
+
         // All operations have now been performed, so we clean up everything and terminate.
         storm::utility::cli::cleanUp();
         return 0;
@@ -31,9 +53,6 @@ int main(const int argc, const char** argv) {
     }
 }
 
-
-
-
 //#include <memory>
 //#include <stdint.h>
 //

src/utility/cli.h

@@ -49,6 +49,7 @@ log4cplus::Logger logger;
 
 // Headers related to exception handling.
 #include "src/exceptions/InvalidSettingsException.h"
+#include "src/exceptions/InvalidTypeException.h"
 
 namespace storm {
     namespace utility {