sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

more work to enable storm to use rational arithmetic 

Former-commit-id: 72933b5184
main
dehnert 9 years ago
parent
af35a4c3ed
commit
d3de111b3b
5 changed files with 276 additions and 288 deletions
Unified View
  1. 356
      src/cli/cli.cpp
  2. 117
      src/cli/entrypoints.h
  3. 31
      src/utility/prism.cpp
  4. 2
      src/utility/prism.h
  5. 58
      src/utility/storm.h

356
src/cli/cli.cpp
View File

@ -10,7 +10,6 @@
#include "src/utility/storm-version.h" #include "src/utility/storm-version.h"
// Includes for the linked libraries and versions header. // Includes for the linked libraries and versions header.
#ifdef STORM_HAVE_INTELTBB #ifdef STORM_HAVE_INTELTBB
# include "tbb/tbb_stddef.h" # include "tbb/tbb_stddef.h"
@ -37,212 +36,221 @@
#endif #endif
namespace storm { namespace storm {
namespace cli { namespace cli {
std::string getCurrentWorkingDirectory() { std::string getCurrentWorkingDirectory() {
char temp[512]; char temp[512];
return (GetCurrentDir(temp, 512 - 1) ? std::string(temp) : std::string("")); 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 << storm::utility::StormVersion::longVersionString() << std::endl;
std::cout << name << std::endl;
std::cout << "---------------" << std::endl << std::endl;
std::cout << storm::utility::StormVersion::longVersionString() << std::endl;
#ifdef STORM_HAVE_INTELTBB #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 #endif
#ifdef STORM_HAVE_GLPK #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 #endif
#ifdef STORM_HAVE_GUROBI #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 #endif
#ifdef STORM_HAVE_Z3 #ifdef STORM_HAVE_Z3
unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber; unsigned int z3Major, z3Minor, z3BuildNumber, z3RevisionNumber;
Z3_get_version(&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; std::cout << "Linked with Microsoft Z3 Optimizer v" << z3Major << "." << z3Minor << " Build " << z3BuildNumber << " Rev " << z3RevisionNumber << "." << std::endl;
#endif #endif
#ifdef STORM_HAVE_MSAT #ifdef STORM_HAVE_MSAT
char* msatVersion = msat_get_version(); char* msatVersion = msat_get_version();
std::cout << "Linked with " << msatVersion << "." << std::endl; std::cout << "Linked with " << msatVersion << "." << std::endl;
msat_free(msatVersion); msat_free(msatVersion);
#endif #endif
#ifdef STORM_HAVE_SMTRAT #ifdef STORM_HAVE_SMTRAT
std::cout << "Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl; std::cout << "Linked with SMT-RAT " << SMTRAT_VERSION << "." << std::endl;
#endif #endif
#ifdef STORM_HAVE_CARL #ifdef STORM_HAVE_CARL
std::cout << "Linked with CARL." << std::endl; std::cout << "Linked with CARL." << std::endl;
// TODO get version string // TODO get version string
#endif #endif
#ifdef STORM_HAVE_CUDA #ifdef STORM_HAVE_CUDA
int deviceCount = 0; int deviceCount = 0;
cudaError_t error_id = cudaGetDeviceCount(&deviceCount); cudaError_t error_id = cudaGetDeviceCount(&deviceCount);
if (error_id == cudaSuccess)
if (error_id == cudaSuccess) {
{ std::cout << "Compiled with CUDA support, ";
std::cout << "Compiled with CUDA support, "; // This function call returns 0 if there are no CUDA capable devices.
// This function call returns 0 if there are no CUDA capable devices. if (deviceCount == 0)
if (deviceCount == 0) {
{ std::cout<< "but there are no available device(s) that support CUDA." << std::endl;
std::cout<< "but there are no available device(s) that support CUDA." << std::endl; } else
} else {
{ std::cout << "detected " << deviceCount << " CUDA Capable device(s):" << std::endl;
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] << " ";
} }
std::cout << "Command line arguments: " << commandStream.str() << std::endl; int dev, driverVersion = 0, runtimeVersion = 0;
std::cout << "Current working directory: " << getCurrentWorkingDirectory() << std::endl << std::endl; 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.
void printUsage() { 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 #ifndef WINDOWS
struct rusage ru; struct rusage ru;
getrusage(RUSAGE_SELF, &ru); getrusage(RUSAGE_SELF, &ru);
std::cout << "===== Statistics ==============================" << std::endl;
std::cout << "===== Statistics ==============================" << std::endl; std::cout << "peak memory usage: " << ru.ru_maxrss/1024/1024 << "MB" << 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 << "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;
std::cout << "===============================================" << std::endl;
#else #else
HANDLE hProcess = GetCurrentProcess (); HANDLE hProcess = GetCurrentProcess ();
FILETIME ftCreation, ftExit, ftUser, ftKernel; FILETIME ftCreation, ftExit, ftUser, ftKernel;
PROCESS_MEMORY_COUNTERS pmc; PROCESS_MEMORY_COUNTERS pmc;
if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) { if (GetProcessMemoryInfo( hProcess, &pmc, sizeof(pmc))) {
std::cout << "Memory Usage: " << std::endl; std::cout << "Memory Usage: " << std::endl;
std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl; std::cout << "\tPageFaultCount: " << pmc.PageFaultCount << std::endl;
std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl; std::cout << "\tPeakWorkingSetSize: " << pmc.PeakWorkingSetSize << std::endl;
std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl; std::cout << "\tWorkingSetSize: " << pmc.WorkingSetSize << std::endl;
std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl; std::cout << "\tQuotaPeakPagedPoolUsage: " << pmc.QuotaPeakPagedPoolUsage << std::endl;
std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl; std::cout << "\tQuotaPagedPoolUsage: " << pmc.QuotaPagedPoolUsage << std::endl;
std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl; std::cout << "\tQuotaPeakNonPagedPoolUsage: " << pmc.QuotaPeakNonPagedPoolUsage << std::endl;
std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl; std::cout << "\tQuotaNonPagedPoolUsage: " << pmc.QuotaNonPagedPoolUsage << std::endl;
std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl; std::cout << "\tPagefileUsage:" << pmc.PagefileUsage << std::endl;
std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl; std::cout << "\tPeakPagefileUsage: " << pmc.PeakPagefileUsage << std::endl;
} }
GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser);
GetProcessTimes (hProcess, &ftCreation, &ftExit, &ftKernel, &ftUser); ULARGE_INTEGER uLargeInteger;
uLargeInteger.LowPart = ftKernel.dwLowDateTime;
ULARGE_INTEGER uLargeInteger; uLargeInteger.HighPart = ftKernel.dwHighDateTime;
uLargeInteger.LowPart = ftKernel.dwLowDateTime; double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds
uLargeInteger.HighPart = ftKernel.dwHighDateTime; uLargeInteger.LowPart = ftUser.dwLowDateTime;
double kernelTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; // 100 ns Resolution to milliseconds uLargeInteger.HighPart = ftUser.dwHighDateTime;
uLargeInteger.LowPart = ftUser.dwLowDateTime; double userTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0;
uLargeInteger.HighPart = ftUser.dwHighDateTime; std::cout << "CPU Time: " << std::endl;
double userTime = static_cast<double>(uLargeInteger.QuadPart) / 10000.0; std::cout << "\tKernel Time: " << std::setprecision(5) << kernelTime << "ms" << std::endl;
std::cout << "\tUser Time: " << std::setprecision(5) << userTime << "ms" << std::endl;
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 #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[]) { if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isHelpSet()) {
try { storm::settings::manager().printHelp(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getHelpModuleName());
storm::settings::mutableManager().setFromCommandLine(argc, argv); return false;
} catch (storm::exceptions::OptionParserException& e) { }
storm::settings::manager().printHelp(); if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isVersionSet()) {
throw e; storm::settings::manager().printVersion();
return false; 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()); if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isTraceSet()) {
return false; 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()) { // Get the string that assigns values to the unknown currently undefined constants in the model.
storm::settings::manager().printVersion(); std::string constantDefinitionString = storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString();
return false; 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()) { // Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
STORM_GLOBAL_LOGLEVEL_INFO(); std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
} if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isDebugSet()) { formulas = storm::parseFormulasForProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), preprocessedProgram);
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();
} }
return 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.
std::vector<std::shared_ptr<storm::logic::Formula const>> preprocessedFormulas;
void processOptions() { for (auto const& formula : formulas) {
if (storm::settings::getModule<storm::settings::modules::DebugSettings>().isLogfileSet()) { preprocessedFormulas.emplace_back(formula->substitute(constantsSubstitution));
storm::utility::initializeFileLogging();
} }
// If we have to build the model from a symbolic representation, we need to parse the representation first. if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
boost::optional<storm::prism::Program> program; buildAndCheckSymbolicModel<storm::RationalFunction>(preprocessedProgram, preprocessedFormulas, true);
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isSymbolicSet()) { } else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
std::string const& programFile = storm::settings::getModule<storm::settings::modules::IOSettings>().getSymbolicModelFilename(); buildAndCheckSymbolicModel<storm::RationalNumber>(preprocessedProgram, preprocessedFormulas, true);
program = storm::parseProgram(programFile); } 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. // If the model is given in an explicit format, we parse the properties without allowing expressions
std::vector<std::shared_ptr<storm::logic::Formula const>> parsedFormulas; // in formulas.
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) { if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
std::string properties = storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(); formulas = storm::parseFormulasForExplicit(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty());
if(program) {
parsedFormulas = storm::parseFormulasForProgram(properties, program.get());
} else {
parsedFormulas = storm::parseFormulasForExplicit(properties);
}
} }
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas(parsedFormulas.begin(), parsedFormulas.end());
if (storm::settings::getModule<storm::settings::modules::IOSettings>().isSymbolicSet()) { buildAndCheckExplicitModel<double>(formulas, true);
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) { } else {
buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formulas, true); STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
} 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.");
}
} }
} }
} }
}

117
src/cli/entrypoints.h
View File

@ -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."); 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::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); storm::modelchecker::SparseExplorationModelChecker<ValueType> checker(program);
std::shared_ptr<storm::logic::Formula> substitutedFormula = formula->substitute(constantsSubstitution); storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
storm::modelchecker::CheckTask<storm::logic::Formula> task(*substitutedFormula, onlyInitialStatesRelevant);
std::unique_ptr<storm::modelchecker::CheckResult> result; std::unique_ptr<storm::modelchecker::CheckResult> result;
if (checker.canHandle(task)) { if (checker.canHandle(task)) {
result = checker.check(task); result = checker.check(task);
@ -109,7 +104,7 @@ namespace storm {
} }
template<storm::dd::DdType DdType> 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) { for (auto const& formula : formulas) {
std::cout << std::endl << "Model checking property: " << *formula << " ..."; std::cout << std::endl << "Model checking property: " << *formula << " ...";
std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, formula, onlyInitialStatesRelevant)); 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> #define BRANCH_ON_SPARSE_MODELTYPE(result, model, value_type, function, ...) \
void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { 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) { 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) { } else if (storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine() == storm::settings::modules::MarkovChainSettings::Engine::Exploration) {
verifySymbolicModelWithExplorationEngine<ValueType>(program, formulas, onlyInitialStatesRelevant); verifySymbolicModelWithExplorationEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
} else { } else {
storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas); auto engine = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getEngine();
STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException, if (engine == storm::settings::modules::MarkovChainSettings::Engine::Dd || engine == storm::settings::modules::MarkovChainSettings::Engine::Hybrid) {
"Model could not be constructed for an unknown reason."); auto ddlib = storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().getDdLibraryType();
if (ddlib == storm::dd::DdType::CUDD) {
// Preprocess the model if needed. buildAndCheckSymbolicModelWithSymbolicEngine<storm::dd::DdType::CUDD>(engine == storm::settings::modules::MarkovChainSettings::Engine::Hybrid, program, formulas, onlyInitialStatesRelevant);
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);
}
} else { } 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> template<typename ValueType>
void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {

31
src/utility/prism.cpp
View File

@ -13,37 +13,14 @@ namespace storm {
namespace utility { namespace utility {
namespace prism { 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 preprocess(storm::prism::Program const& program, std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) {
storm::prism::Program result = program.defineUndefinedConstants(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(); result = result.substituteConstants();
return result; return result;
} }
template<typename ValueType>
storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString) { 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) { 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; 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);
} }
} }
} }

2
src/utility/prism.h
View File

@ -22,10 +22,8 @@ namespace storm {
std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString); 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); 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); storm::prism::Program preprocess(storm::prism::Program const& program, std::string const& constantDefinitionString);
} // namespace prism } // namespace prism

58
src/utility/storm.h
View File

@ -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>> parseFormulasForExplicit(std::string const& inputString);
std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program); std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForProgram(std::string const& inputString, storm::prism::Program const& program);
template<typename ValueType>
template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD> 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::storage::ModelFormulasPair buildSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) { storm::generator::NextStateGeneratorOptions options(formulas);
storm::storage::ModelFormulasPair result;
// Get the string that assigns values to the unknown currently undefined constants in the model. // Generate command labels if we are going to build a counterexample later.
std::string constantDefinitionString = storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString(); if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {
storm::prism::Program preprocessedProgram = storm::utility::prism::preprocess<ValueType>(program, constantDefinitionString); options.setBuildChoiceLabels(true);
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);
} }
// There may be constants of the model appearing in the formulas, so we replace all their occurrences std::shared_ptr<storm::generator::NextStateGenerator<ValueType, uint32_t>> generator = std::make_shared<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>>(program, options);
// by their definitions in the translated program. storm::builder::ExplicitModelBuilder<ValueType> builder(generator);
for (auto const& formula : formulas) { return builder.build();
result.formulas.emplace_back(formula->substitute(constantsSubstitution)); }
} template<typename ValueType, storm::dd::DdType LibraryType = storm::dd::DdType::CUDD>
return result; 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> 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> 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) { 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()) { if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {

Write Preview
|||||||
100:0
Loading…
Cancel
Save