Browse Source

Removed old jani file settings

tempestpy_adaptions
Matthias Volk 6 years ago
parent
commit
c136b9c628
  1. 12
      src/storm-conv/settings/modules/JaniExportSettings.h

12
src/storm-conv/settings/modules/JaniExportSettings.h

@ -14,16 +14,6 @@ namespace storm {
*/ */
JaniExportSettings(); JaniExportSettings();
/**
* Retrievew whether the pgcl file option was set
*/
bool isJaniFileSet() const;
/**
* Retrieves the pgcl file name
*/
std::string getJaniFilename() const;
bool isExportAsStandardJaniSet() const; bool isExportAsStandardJaniSet() const;
bool isExportFlattenedSet() const; bool isExportFlattenedSet() const;
@ -42,8 +32,6 @@ namespace storm {
static const std::string moduleName; static const std::string moduleName;
private: private:
static const std::string janiFileOptionName;
static const std::string janiFileOptionShortName;
static const std::string standardCompliantOptionName; static const std::string standardCompliantOptionName;
static const std::string standardCompliantOptionShortName; static const std::string standardCompliantOptionShortName;
static const std::string exportFlattenOptionName; static const std::string exportFlattenOptionName;

Loading…
Cancel
Save