diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index b8566af22..4207ca722 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -10,7 +10,6 @@
#include "src/utility/storm-version.h"
-
// Includes for the linked libraries and versions header.
#ifdef STORM_HAVE_INTELTBB
# include "tbb/tbb_stddef.h"
@@ -37,212 +36,221 @@
#endif
namespace storm {
- namespace cli {
- std::string getCurrentWorkingDirectory() {
- char temp[512];
- return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string(""));
- }
+ namespace cli {
+ std::string getCurrentWorkingDirectory() {
+ char temp[512];
+ return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string(""));
+ }
+
+ void printHeader(const std::string name, const int argc, const char* argv[]) {
+ std::cout << name << std::endl;
+ std::cout << "---------------" << std::endl << std::endl;
- void printHeader(const std::string name, const int argc, const char* argv[]) {
- std::cout << name << std::endl;
- std::cout << "---------------" << std::endl << std::endl;
-
-
- std::cout << storm::utility::StormVersion::longVersionString() << std::endl;
+
+ std::cout << storm::utility::StormVersion::longVersionString() << std::endl;
#ifdef STORM_HAVE_INTELTBB
- std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
+ std::cout << "Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version " << TBB_INTERFACE_VERSION << ")." << std::endl;
#endif
#ifdef STORM_HAVE_GLPK
- std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl;
+ std::cout << "Linked with GNU Linear Programming Kit v" << GLP_MAJOR_VERSION << "." << GLP_MINOR_VERSION << "." << std::endl;
#endif
#ifdef STORM_HAVE_GUROBI
- std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl;
+ std::cout << "Linked with Gurobi Optimizer v" << GRB_VERSION_MAJOR << "." << GRB_VERSION_MINOR << "." << GRB_VERSION_TECHNICAL << "." << std::endl;
#endif
#ifdef STORM_HAVE_Z3
- unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
- Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
- std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl;
+ unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
+ Z3_get_version(&z3Major, &z3Minor, &z3BuildNumber, &z3RevisionNumber);
+ std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl;
#endif
#ifdef STORM_HAVE_MSAT
- char* msatVersion = msat_get_version();
- std::cout << "Linked with " << msatVersion << "." << std::endl;
- msat_free(msatVersion);
+ char* msatVersion = msat_get_version();
+ std::cout << "Linked with " << msatVersion << "." << std::endl;
+ msat_free(msatVersion);
#endif
#ifdef STORM_HAVE_SMTRAT
- std::cout << "Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl;
-#endif
+ std::cout << "Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl;
+#endif
#ifdef STORM_HAVE_CARL
- std::cout << "Linked with CARL." << std::endl;
- // TODO get version string
+ std::cout << "Linked with CARL." << std::endl;
+ // TODO get version string
#endif
-
+
#ifdef STORM_HAVE_CUDA
- int deviceCount = 0;
- cudaError_t error_id = cudaGetDeviceCount(&deviceCount);
-
- if (error_id == cudaSuccess)
- {
- std::cout << "Compiled with CUDA support, ";
- // This function call returns 0 if there are no CUDA capable devices.
- if (deviceCount == 0)
- {
- std::cout<< "but there are no available device(s) that support CUDA." << std::endl;
- } else
- {
- std::cout << "detected " << deviceCount << " CUDA Capable device(s):" << std::endl;
- }
-
- int dev, driverVersion = 0, runtimeVersion = 0;
-
- for (dev = 0; dev < deviceCount; ++dev)
- {
- cudaSetDevice(dev);
- cudaDeviceProp deviceProp;
- cudaGetDeviceProperties(&deviceProp, dev);
-
- std::cout << "CUDA Device " << dev << ": \"" << deviceProp.name << "\"" << std::endl;
-
- // Console log
- cudaDriverGetVersion(&driverVersion);
- cudaRuntimeGetVersion(&runtimeVersion);
- std::cout << " CUDA Driver Version / Runtime Version " << driverVersion / 1000 << "." << (driverVersion % 100) / 10 << " / " << runtimeVersion / 1000 << "." << (runtimeVersion % 100) / 10 << std::endl;
- std::cout << " CUDA Capability Major/Minor version number: " << deviceProp.major<<"."<<deviceProp.minor <<std::endl;
- }
- std::cout << std::endl;
- }
- else {
- std::cout << "Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl;
- }
-#endif
-
- // "Compute" the command line argument string with which STORM was invoked.
- std::stringstream commandStream;
- for (int i = 1; i < argc; ++i) {
- commandStream << argv[i] << " ";
+ int deviceCount = 0;
+ cudaError_t error_id = cudaGetDeviceCount(&deviceCount);
+
+ if (error_id == cudaSuccess)
+ {
+ std::cout << "Compiled with CUDA support, ";
+ // This function call returns 0 if there are no CUDA capable devices.
+ if (deviceCount == 0)
+ {
+ std::cout<< "but there are no available device(s) that support CUDA." << std::endl;
+ } else
+ {
+ std::cout << "detected " << deviceCount << " CUDA Capable device(s):" << std::endl;
}
- std::cout << "Command line arguments: " << commandStream.str() << std::endl;
- std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
+
+ int dev, driverVersion = 0, runtimeVersion = 0;
+
+ for (dev = 0; dev < deviceCount; ++dev)
+ {
+ cudaSetDevice(dev);
+ cudaDeviceProp deviceProp;
+ cudaGetDeviceProperties(&deviceProp, dev);
+
+ std::cout << "CUDA Device " << dev << ": \"" << deviceProp.name << "\"" << std::endl;
+
+ // Console log
+ cudaDriverGetVersion(&driverVersion);
+ cudaRuntimeGetVersion(&runtimeVersion);
+ std::cout << " CUDA Driver Version / Runtime Version " << driverVersion / 1000 << "." << (driverVersion % 100) / 10 << " / " << runtimeVersion / 1000 << "." << (runtimeVersion % 100) / 10 << std::endl;
+ std::cout << " CUDA Capability Major/Minor version number: " << deviceProp.major<<"."<<deviceProp.minor <<std::endl;
+ }
+ std::cout << std::endl;
}
+ else {
+ std::cout << "Compiled with CUDA support, but an error occured trying to find CUDA devices." << std::endl;
+ }
+#endif
-
- void printUsage() {
+ // "Compute" the command line argument string with which STORM was invoked.
+ std::stringstream commandStream;
+ for (int i = 1; i < argc; ++i) {
+ commandStream << argv[i] << " ";
+ }
+ std::cout << "Command line arguments: " << commandStream.str() << std::endl;
+ std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl;
+ }
+
+
+ void printUsage() {
#ifndef WINDOWS
- struct rusage ru;
- getrusage(RUSAGE_SELF, &ru);
-
- std::cout << "===== Statistics ==============================" << std::endl;
- std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl;
- std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl;
- std::cout << "===============================================" << std::endl;
+ struct rusage ru;
+ getrusage(RUSAGE_SELF, &ru);
+
+ std::cout << "===== Statistics ==============================" << std::endl;
+ std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << std::endl;
+ std::cout << "CPU time: " << ru.ru_utime.tv_sec << "." << std::setw(3) << std::setfill('0') << ru.ru_utime.tv_usec/1000 << " seconds" << std::endl;
+ std::cout << "===============================================" << std::endl;
#else
- HANDLE hProcess = GetCurrentProcess ();
- FILETIME ftCreation, ftExit, ftUser, ftKernel;
- PROCESS_MEMORY_COUNTERS pmc;
- if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
- std::cout << "Memory Usage: " << std::endl;
- std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl;
- std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl;
- std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl;
- std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl;
- std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl;
- std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl;
- std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl;
- std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl;
- std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl;
- }
-
- GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser);
-
- ULARGE_INTEGER uLargeInteger;
- uLargeInteger.LowPart = ftKernel.dwLowDateTime;
- uLargeInteger.HighPart = ftKernel.dwHighDateTime;
- double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
- uLargeInteger.LowPart = ftUser.dwLowDateTime;
- uLargeInteger.HighPart = ftUser.dwHighDateTime;
- double userTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0;
-
- std::cout << "CPU Time: " << std::endl;
- std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl;
- std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl;
+ HANDLE hProcess = GetCurrentProcess ();
+ FILETIME ftCreation, ftExit, ftUser, ftKernel;
+ PROCESS_MEMORY_COUNTERS pmc;
+ if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
+ std::cout << "Memory Usage: " << std::endl;
+ std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl;
+ std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl;
+ std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl;
+ std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl;
+ std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl;
+ std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl;
+ std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl;
+ std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl;
+ std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl;
+ }
+
+ GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser);
+
+ ULARGE_INTEGER uLargeInteger;
+ uLargeInteger.LowPart = ftKernel.dwLowDateTime;
+ uLargeInteger.HighPart = ftKernel.dwHighDateTime;
+ double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
+ uLargeInteger.LowPart = ftUser.dwLowDateTime;
+ uLargeInteger.HighPart = ftUser.dwHighDateTime;
+ double userTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0;
+
+ std::cout << "CPU Time: " << std::endl;
+ std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl;
+ std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl;
#endif
+ }
+
+ bool parseOptions(const int argc, const char* argv[]) {
+ try {
+ storm::settings::mutableManager().setFromCommandLine(argc, argv);
+ } catch (storm::exceptions::OptionParserException& e) {
+ storm::settings::manager().printHelp();
+ throw e;
+ return false;
}
- bool parseOptions(const int argc, const char* argv[]) {
- try {
- storm::settings::mutableManager().setFromCommandLine(argc, argv);
- } catch (storm::exceptions::OptionParserException& e) {
- storm::settings::manager().printHelp();
- throw e;
- return false;
- }
+ if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isHelpSet()) {
+ storm::settings::manager().printHelp(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getHelpModuleName());
+ return false;
+ }
+
+ if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isVersionSet()) {
+ storm::settings::manager().printVersion();
+ return false;
+ }
+
+ if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isVerboseSet()) {
+ STORM_GLOBAL_LOGLEVEL_INFO();
+ }
+ if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isDebugSet()) {
+ STORM_GLOBAL_LOGLEVEL_DEBUG();
- if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isHelpSet()) {
- storm::settings::manager().printHelp(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getHelpModuleName());
- return false;
- }
+ }
+ if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
+ STORM_GLOBAL_LOGLEVEL_TRACE();
+ }
+ if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isLogfileSet()) {
+ storm::utility::initializeFileLogging();
+ }
+ return true;
+ }
+
+ void processOptions() {
+ if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isLogfileSet()) {
+ storm::utility::initializeFileLogging();
+ }
+
+ if (storm::settings::getModule<storm::settings::modules::IOSettings>().isSymbolicSet()) {
+ // If we have to build the model from a symbolic representation, we need to parse the representation first.
+ storm::prism::Program program = storm::parseProgram(storm::settings::getModule<storm::settings::modules::IOSettings>().getSymbolicModelFilename());
- if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isVersionSet()) {
- storm::settings::manager().printVersion();
- return false;
- }
+ // Get the string that assigns values to the unknown currently undefined constants in the model.
+ std::string constantDefinitionString = storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString();
+ storm::prism::Program preprocessedProgram = storm::utility::prism::preprocess(program, constantDefinitionString);
+ std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preprocessedProgram.getConstantsSubstitution();
- if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isVerboseSet()) {
- STORM_GLOBAL_LOGLEVEL_INFO();
- }
- if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isDebugSet()) {
- STORM_GLOBAL_LOGLEVEL_DEBUG();
-
- }
- if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
- STORM_GLOBAL_LOGLEVEL_TRACE();
- }
- if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isLogfileSet()) {
- storm::utility::initializeFileLogging();
+ // Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
+ std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
+ if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
+ formulas = storm::parseFormulasForProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), preprocessedProgram);
}
- return true;
- }
-
- void processOptions() {
- if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isLogfileSet()) {
- storm::utility::initializeFileLogging();
+
+ // There may be constants of the model appearing in the formulas, so we replace all their occurrences
+ // by their definitions in the translated program.
+ std::vector<std::shared_ptr<storm::logic::Formula const>> preprocessedFormulas;
+ for (auto const& formula : formulas) {
+ preprocessedFormulas.emplace_back(formula->substitute(constantsSubstitution));
}
- // If we have to build the model from a symbolic representation, we need to parse the representation first.
- boost::optional<storm::prism::Program> program;
- if (storm::settings::getModule<storm::settings::modules::IOSettings>().isSymbolicSet()) {
- std::string const& programFile = storm::settings::getModule<storm::settings::modules::IOSettings>().getSymbolicModelFilename();
- program = storm::parseProgram(programFile);
+ if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
+ buildAndCheckSymbolicModel<storm::RationalFunction>(preprocessedProgram, preprocessedFormulas, true);
+ } else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
+ buildAndCheckSymbolicModel<storm::RationalNumber>(preprocessedProgram, preprocessedFormulas, true);
+ } else {
+ buildAndCheckSymbolicModel<double>(preprocessedProgram, preprocessedFormulas, true);
}
+ } else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) {
+ STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input.");
- // Then proceed to parsing the property (if given), since the model we are building may depend on the property.
- std::vector<std::shared_ptr<storm::logic::Formula const>> parsedFormulas;
+ // If the model is given in an explicit format, we parse the properties without allowing expressions
+ // in formulas.
+ std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
- std::string properties = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty();
-
- if(program) {
- parsedFormulas = storm::parseFormulasForProgram(properties, program.get());
- } else {
- parsedFormulas = storm::parseFormulasForExplicit(properties);
- }
-
+ formulas = storm::parseFormulasForExplicit(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty());
}
- std::vector<std::shared_ptr<storm::logic::Formula const>> formulas(parsedFormulas.begin(), parsedFormulas.end());
- if (storm::settings::getModule<storm::settings::modules::IOSettings>().isSymbolicSet()) {
- if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
- buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formulas, true);
- } else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
- buildAndCheckSymbolicModel<storm::RationalNumber>(program.get(), formulas, true);
- } else {
- buildAndCheckSymbolicModel<double>(program.get(), formulas, true);
- }
- } else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) {
- STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use explicit input models with this engine.");
- buildAndCheckExplicitModel<double>(formulas, true);
- } else {
- STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
- }
+ buildAndCheckExplicitModel<double>(formulas, true);
+ } else {
+ STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
}
-
+
}
- }
+
+ }
+}
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index a3702875b..41dfd2ab1 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -60,14 +60,9 @@ namespace storm {
STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
std::cout << std::endl << "Model checking property: " << *formula << " ...";
- std::string constantDefinitionString = storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString();
- storm::prism::Program preprocessedProgram = storm::utility::prism::preprocess<ValueType>(program, constantDefinitionString);
- std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preprocessedProgram.getConstantsSubstitution();
-
storm::modelchecker::SparseExplorationModelChecker<ValueType> checker(program);
- std::shared_ptr<storm::logic::Formula> substitutedFormula = formula->substitute(constantsSubstitution);
- storm::modelchecker::CheckTask<storm::logic::Formula> task(*substitutedFormula, onlyInitialStatesRelevant);
+ storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
std::unique_ptr<storm::modelchecker::CheckResult> result;
if (checker.canHandle(task)) {
result = checker.check(task);
@@ -109,7 +104,7 @@ namespace storm {
}
template<storm::dd::DdType DdType>
- void verifySymbolicModelWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+ void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
for (auto const& formula : formulas) {
std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, formula, onlyInitialStatesRelevant));
@@ -150,58 +145,82 @@ namespace storm {
} \
}
- template<typename ValueType, storm::dd::DdType LibraryType>
- void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+#define BRANCH_ON_SPARSE_MODELTYPE(result, model, value_type, function, ...) \
+ STORM_LOG_ASSERT(model->isSparseModel(), "Unknown model type."); \
+ if (model->isOfType(storm::models::ModelType::Dtmc)) { \
+ result = function<storm::models::sparse::Dtmc<value_type>>(model->template as<storm::models::sparse::Dtmc<value_type>>(), __VA_ARGS__); \
+ } else if (model->isOfType(storm::models::ModelType::Ctmc)) { \
+ result = function<storm::models::sparse::Ctmc<value_type>>(model->template as<storm::models::sparse::Ctmc<value_type>>(), __VA_ARGS__); \
+ } else if (model->isOfType(storm::models::ModelType::Mdp)) { \
+ result = function<storm::models::sparse::Mdp<value_type>>(model->template as<storm::models::sparse::Mdp<value_type>>(), __VA_ARGS__); \
+ } else if (model->isOfType(storm::models::ModelType::MarkovAutomaton)) { \
+ result = function<storm::models::sparse::MarkovAutomaton<value_type>>(model->template as<storm::models::sparse::MarkovAutomaton<value_type>>(), __VA_ARGS__); \
+ } else { \
+ STORM_LOG_ASSERT(false, "Unknown model type."); \
+ }
+
+ template<storm::dd::DdType LibraryType>
+ void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+ // Start by building the model.
+ auto model = buildSymbolicModel<double, LibraryType>(program, formulas);
+
+ // Print some information about the model.
+ model->printModelInformationToStream(std::cout);
+
+ // Then select the correct engine.
+ if (hybrid) {
+ verifySymbolicModelWithHybridEngine(model, formulas, onlyInitialStatesRelevant);
+ } else {
+ verifySymbolicModelWithDdEngine(model, formulas, onlyInitialStatesRelevant);
+ }
+ }
+
+ template<typename ValueType>
+ void buildAndCheckSymbolicModelWithSparseEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+ // Start by building the model.
+ auto model = buildSparseModel<ValueType>(program, formulas);
+
+ // Print some information about the model.
+ model->printModelInformationToStream(std::cout);
+ // Preprocess the model.
+ BRANCH_ON_SPARSE_MODELTYPE(model, model, ValueType, preprocessModel, formulas);
+
+ // Finally, treat the formulas.
+ if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isCounterexampleSet()) {
+ generateCounterexamples<ValueType>(program, formulas);
+ } else {
+ verifySparseModel<ValueType>(model, formulas, onlyInitialStatesRelevant);
+ }
+ }
+
+ template<typename ValueType>
+ void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::AbstractionRefinement) {
- verifySymbolicModelWithAbstractionRefinementEngine<LibraryType>(program, formulas, onlyInitialStatesRelevant);
+ auto ddlib = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getDdLibraryType();
+ if (ddlib == storm::dd::DdType::CUDD) {
+ verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::CUDD>(program, formulas, onlyInitialStatesRelevant);
+ } else {
+ verifySymbolicModelWithAbstractionRefinementEngine<storm::dd::DdType::Sylvan>(program, formulas, onlyInitialStatesRelevant);
+ }
} else if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Exploration) {
verifySymbolicModelWithExplorationEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
} else {
- storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
- STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException,
- "Model could not be constructed for an unknown reason.");
-
- // Preprocess the model if needed.
- BRANCH_ON_MODELTYPE(modelFormulasPair.model, modelFormulasPair.model, ValueType, LibraryType, preprocessModel, formulas);
-
- // Print some information about the model.
- modelFormulasPair.model->printModelInformationToStream(std::cout);
-
- // Verify the model, if a formula was given.
- if (!modelFormulasPair.formulas.empty()) {
- if (modelFormulasPair.model->isSparseModel()) {
- if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isCounterexampleSet()) {
- // If we were requested to generate a counterexample, we now do so for each formula.
- for (auto const& formula : modelFormulasPair.formulas) {
- generateCounterexample<ValueType>(program, modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
- }
- } else {
- verifySparseModel<ValueType>(modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), modelFormulasPair.formulas, onlyInitialStatesRelevant);
- }
- } else if (modelFormulasPair.model->isSymbolicModel()) {
- if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) {
- verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(),
- modelFormulasPair.formulas, onlyInitialStatesRelevant);
- } else {
- verifySymbolicModelWithSymbolicEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(),
- modelFormulasPair.formulas, onlyInitialStatesRelevant);
- }
+ auto engine = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine();
+ if (engine == storm::settings::modules::MarkovChainSettings::Engine::Dd || engine == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) {
+ auto ddlib = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getDdLibraryType();
+ if (ddlib == storm::dd::DdType::CUDD) {
+ buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::CUDD>(engine == storm::settings::modules::MarkovChainSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant);
} else {
- STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
+ buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::Sylvan>(engine == storm::settings::modules::MarkovChainSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant);
}
+ } else {
+ STORM_LOG_THROW(engine == storm::settings::modules::MarkovChainSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Illegal engine.");
+
+ buildAndCheckSymbolicModelWithSparseEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
}
}
}
-
- template<typename ValueType>
- void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
- if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getDdLibraryType() == storm::dd::DdType::CUDD) {
- buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::CUDD>(program, formulas, onlyInitialStatesRelevant);
- } else if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getDdLibraryType() == storm::dd::DdType::Sylvan) {
- buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::Sylvan>(program, formulas, onlyInitialStatesRelevant);
- }
- }
template<typename ValueType>
void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
diff --git a/src/utility/prism.cpp b/src/utility/prism.cpp
index 617a5642b..947d7e8a2 100644
--- a/src/utility/prism.cpp
+++ b/src/utility/prism.cpp
@@ -13,37 +13,14 @@ namespace storm {
namespace utility {
namespace prism {
- template<typename ValueType>
storm::prism::Program preprocess(storm::prism::Program const& program, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) {
storm::prism::Program result = program.defineUndefinedConstants(constantDefinitions);
-
- // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
- if (!std::is_same<ValueType, storm::RationalFunction>::value && result.hasUndefinedConstants()) {
- std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = result.getUndefinedConstants();
- std::stringstream stream;
- bool printComma = false;
- for (auto const& constant : undefinedConstants) {
- if (printComma) {
- stream << ", ";
- } else {
- printComma = true;
- }
- stream << constant.get().getName() << " (" << constant.get().getType() << ")";
- }
- stream << ".";
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
- } else if (std::is_same<ValueType, storm::RationalFunction>::value && !result.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
- STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
- }
-
- // Now that the program is fixed, we we need to substitute all constants with their concrete value.
result = result.substituteConstants();
return result;
}
- template<typename ValueType>
storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString) {
- return preprocess<ValueType>(program, parseConstantDefinitionString(program, constantDefinitionString));
+ return preprocess(program, parseConstantDefinitionString(program, constantDefinitionString));
}
std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
@@ -103,12 +80,6 @@ namespace storm {
return constantDefinitions;
}
- template storm::prism::Program preprocess<double>(storm::prism::Program const& program, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions);
- template storm::prism::Program preprocess<storm::RationalFunction>(storm::prism::Program const& program, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions);
-
- template storm::prism::Program preprocess<double>(storm::prism::Program const& program, std::string const& constantDefinitionString);
- template storm::prism::Program preprocess<storm::RationalFunction>(storm::prism::Program const& program, std::string const& constantDefinitionString);
-
}
}
}
\ No newline at end of file
diff --git a/src/utility/prism.h b/src/utility/prism.h
index 610f82bd0..1c94a3395 100644
--- a/src/utility/prism.h
+++ b/src/utility/prism.h
@@ -22,10 +22,8 @@ namespace storm {
std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString);
- template<typename ValueType>
storm::prism::Program preprocess(storm::prism::Program const& program, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions);
- template<typename ValueType>
storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString);
} // namespace prism
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 3e7a5d992..8f0f5b79f 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -96,42 +96,27 @@ namespace storm {
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
-
- template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
- storm::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
- storm::storage::ModelFormulasPair result;
+ template<typename ValueType>
+ std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
+ storm::generator::NextStateGeneratorOptions options(formulas);
- // Get the string that assigns values to the unknown currently undefined constants in the model.
- std::string constantDefinitionString = storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString();
- storm::prism::Program preprocessedProgram = storm::utility::prism::preprocess<ValueType>(program, constantDefinitionString);
- std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = preprocessedProgram.getConstantsSubstitution();
-
- // Customize and perform model-building.
- if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Sparse) {
- storm::generator::NextStateGeneratorOptions options(formulas);
-
- // Generate command labels if we are going to build a counterexample later.
- if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {
- options.setBuildChoiceLabels(true);
- }
-
- std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(preprocessedProgram, options);
- storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
- result.model = builder.build();
- } else if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Dd || storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) {
- typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
- options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
-
- storm::builder::DdPrismModelBuilder<LibraryType> builder;
- result.model = builder.build(program, options);
+ // Generate command labels if we are going to build a counterexample later.
+ if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {
+ options.setBuildChoiceLabels(true);
}
- // There may be constants of the model appearing in the formulas, so we replace all their occurrences
- // by their definitions in the translated program.
- for (auto const& formula : formulas) {
- result.formulas.emplace_back(formula->substitute(constantsSubstitution));
- }
- return result;
+ std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(program, options);
+ storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
+ return builder.build();
+ }
+
+ template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
+ std::shared_ptr<storm::models::symbolic::Model<LibraryType, ValueType>> buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+ typename storm::builder::DdPrismModelBuilder<LibraryType>::Options options;
+ options = typename storm::builder::DdPrismModelBuilder<LibraryType>::Options(formulas);
+
+ storm::builder::DdPrismModelBuilder<LibraryType> builder;
+ return builder.build(program, options);
}
template<typename ModelType>
@@ -214,6 +199,13 @@ namespace storm {
}
+ template<typename ValueType>
+ void generateCounterexamples(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+ for (auto const& formula : formulas) {
+ generateCounterexample(program, model, formula);
+ }
+ }
+
template<typename ValueType>
void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {