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

DFT: load json from string

tempestpy_adaptions
Matthias Volk 6 years ago
parent
856d62513b
commit
369d106f99
7 changed files with 142 additions and 44 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 71
      resources/examples/testfiles/dft/and.json
  2. 4
      src/storm-dft-cli/storm-dft.cpp
  3. 19
      src/storm-dft/api/storm-dft.h
  4. 70
      src/storm-dft/parser/DFTJsonParser.cpp
  5. 6
      src/storm-dft/parser/DFTJsonParser.h
  6. 2
      src/test/storm-dft/api/DftModelCheckerTest.cpp
  7. 12
      src/test/storm-dft/api/DftParserTest.cpp

71
resources/examples/testfiles/dft/and.json
View File

@ -0,0 +1,71 @@
{
"toplevel": "2",
"parameters": {},
"nodes": [
{
"data": {
"id": "0",
"name": "A",
"type": "be",
"rate": "1",
"dorm": "1",
"label": "A (1)"
},
"position": {
"x": 440,
"y": 260
},
"group": "nodes",
"removed": false,
"selected": false,
"selectable": true,
"locked": false,
"grabbable": true,
"classes": "be"
},
{
"data": {
"id": "1",
"name": "B",
"type": "be",
"rate": "1",
"dorm": "1",
"label": "B (1)"
},
"position": {
"x": 548,
"y": 265
},
"group": "nodes",
"removed": false,
"selected": false,
"selectable": true,
"locked": false,
"grabbable": true,
"classes": "be"
},
{
"data": {
"id": "2",
"name": "Z",
"type": "and",
"children": [
"0",
"1"
],
"label": "Z"
},
"position": {
"x": 505,
"y": 119
},
"group": "nodes",
"removed": false,
"selected": false,
"selectable": true,
"locked": false,
"grabbable": true,
"classes": "and"
}
]
}

4
src/storm-dft-cli/storm-dft.cpp
View File

@ -32,10 +32,10 @@ void processOptions() {
std::shared_ptr<storm::storage::DFT<ValueType>> dft;
if (dftIOSettings.isDftJsonFileSet()) {
STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftJsonFilename());
dft = storm::api::loadDFTJson<ValueType>(dftIOSettings.getDftJsonFilename());
dft = storm::api::loadDFTJsonFile<ValueType>(dftIOSettings.getDftJsonFilename());
} else {
STORM_LOG_DEBUG("Loading DFT from file " << dftIOSettings.getDftFilename());
dft = storm::api::loadDFTGalileo<ValueType>(dftIOSettings.getDftFilename());
dft = storm::api::loadDFTGalileoFile<ValueType>(dftIOSettings.getDftFilename());
}
if (dftIOSettings.isDisplayStatsSet()) {

19
src/storm-dft/api/storm-dft.h
View File

@ -23,10 +23,23 @@ namespace storm {
* @return DFT.
*/
template<typename ValueType>
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTGalileo(std::string const& file) {
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTGalileoFile(std::string const& file) {
return std::make_shared<storm::storage::DFT<ValueType>>(storm::parser::DFTGalileoParser<ValueType>::parseDFT(file));
}
/*!
* Load DFT from JSON string.
*
* @param jsonString String containing DFT description in JSON format.
*
* @return DFT.
*/
template<typename ValueType>
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJsonString(std::string const& jsonString) {
storm::parser::DFTJsonParser<ValueType> parser;
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromString(jsonString));
}
/*!
* Load DFT from JSON file.
*
@ -35,9 +48,9 @@ namespace storm {
* @return DFT.
*/
template<typename ValueType>
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJson(std::string const& file) {
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJsonFile(std::string const& file) {
storm::parser::DFTJsonParser<ValueType> parser;
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJson(file));
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromFile(file));
}
/*!

70
src/storm-dft/parser/DFTJsonParser.cpp
View File

@ -15,34 +15,27 @@ namespace storm {
namespace parser {
template<typename ValueType>
storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJson(const std::string& filename) {
readFile(filename);
storm::storage::DFT<ValueType> dft = builder.build();
STORM_LOG_DEBUG("Elements:" << std::endl << dft.getElementsString());
STORM_LOG_DEBUG("Spare Modules:" << std::endl << dft.getSpareModulesString());
return dft;
storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJsonFromFile(std::string const& filename) {
STORM_LOG_DEBUG("Parsing from JSON file");
std::ifstream file;
storm::utility::openFile(filename, file);
json jsonInput;
jsonInput << file;
storm::utility::closeFile(file);
return parseJson(jsonInput);
}
template<typename ValueType>
std::string DFTJsonParser<ValueType>::generateUniqueName(std::string const& id, std::string const& name) {
std::string newId = name;
std::replace(newId.begin(), newId.end(), ' ', '_');
std::replace(newId.begin(), newId.end(), '-', '_');
return newId + "_" + id;
storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJsonFromString(std::string const& jsonString) {
STORM_LOG_DEBUG("Parsing from JSON string");
json jsonInput = json::parse(jsonString);
return parseJson(jsonInput);
}
template<typename ValueType>
void DFTJsonParser<ValueType>::readFile(const std::string& filename) {
STORM_LOG_DEBUG("Parsing from JSON");
std::ifstream file;
storm::utility::openFile(filename, file);
json parsedJson;
parsedJson << file;
storm::utility::closeFile(file);
json parameters = parsedJson.at("parameters");
#ifdef STORM_HAVE_CARL
storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJson(json const& jsonInput) {
// Parse parameters
json parameters = jsonInput.at("parameters");
for (auto it = parameters.begin(); it != parameters.end(); ++it) {
STORM_LOG_THROW((std::is_same<ValueType, storm::RationalFunction>::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions.");
std::string parameter = it.key();
@ -51,18 +44,17 @@ namespace storm {
parser.setIdentifierMapping(identifierMapping);
STORM_LOG_TRACE("Added parameter: " << var.getName());
}
#endif
json nodes = parsedJson.at("nodes");
json nodes = jsonInput.at("nodes");
// Start by building mapping from ids to their unique names
std::map<std::string, std::string> nameMapping;
for (auto& element: nodes) {
for (auto& element : nodes) {
json data = element.at("data");
std::string id = data.at("id");
nameMapping[id] = generateUniqueName(id, data.at("name"));
}
// Parse nodes
for (auto& element : nodes) {
STORM_LOG_TRACE("Parsing: " << element);
bool success = true;
@ -123,10 +115,25 @@ namespace storm {
STORM_LOG_THROW(success, storm::exceptions::FileIoException, "Error while adding element '" << element << "'.");
}
std::string toplevelName = nameMapping[parseJsonNumber(parsedJson.at("toplevel"))];
std::string toplevelName = nameMapping[parseJsonNumber(jsonInput.at("toplevel"))];
if(!builder.setTopLevel(toplevelName)) {
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Top level id unknown.");
}
// Build DFT
storm::storage::DFT<ValueType> dft = builder.build();
STORM_LOG_DEBUG("Elements:" << std::endl << dft.getElementsString());
STORM_LOG_DEBUG("Spare Modules:" << std::endl << dft.getSpareModulesString());
return dft;
}
template<typename ValueType>
std::string DFTJsonParser<ValueType>::generateUniqueName(std::string const& id, std::string const& name) {
std::string newId = name;
std::replace(newId.begin(), newId.end(), ' ', '_');
std::replace(newId.begin(), newId.end(), '-', '_');
return newId + "_" + id;
}
template<typename ValueType>
@ -151,10 +158,6 @@ namespace storm {
return boost::lexical_cast<double>(expr);
}
// Explicitly instantiate the class.
template class DFTJsonParser<double>;
#ifdef STORM_HAVE_CARL
template<>
storm::RationalFunction DFTJsonParser<storm::RationalFunction>::parseRationalExpression(std::string const& expr) {
STORM_LOG_TRACE("Translating expression: " << expr);
@ -165,8 +168,9 @@ namespace storm {
return rationalFunction;
}
template class DFTJsonParser<RationalFunction>;
#endif
// Explicitly instantiate the class.
template class DFTJsonParser<double>;
template class DFTJsonParser<RationalFunction>;
}
}

6
src/storm-dft/parser/DFTJsonParser.h
View File

@ -33,10 +33,12 @@ namespace storm {
DFTJsonParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) {
}
storm::storage::DFT<ValueType> parseJson(std::string const& filename);
storm::storage::DFT<ValueType> parseJsonFromString(std::string const& jsonString);
storm::storage::DFT<ValueType> parseJsonFromFile(std::string const& filename);
private:
void readFile(std::string const& filename);
storm::storage::DFT<ValueType> parseJson(json const& jsonInput);
std::string generateUniqueName(std::string const& id, std::string const& name);

2
src/test/storm-dft/api/DftModelCheckerTest.cpp
View File

@ -63,7 +63,7 @@ namespace {
}
double analyzeMTTF(std::string const& file) {
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileo<double>(file);
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
std::string property = "Tmin=? [F \"failed\"]";
std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, config.useMod, config.useDC, false);

12
src/test/storm-dft/api/DftParserTest.cpp
View File

@ -5,9 +5,17 @@
namespace {
TEST(DftParserTest, LoadFromGalileo) {
TEST(DftParserTest, LoadFromGalileoFile) {
std::string file = STORM_TEST_RESOURCES_DIR "/dft/and.dft";
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileo<double>(file);
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
EXPECT_EQ(3ul, dft->nrElements());
EXPECT_EQ(2ul, dft->nrBasicElements());
}
TEST(DftParserTest, LoadFromJsonFile) {
std::string file = STORM_TEST_RESOURCES_DIR "/dft/and.json";
std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTJsonFile<double>(file);
EXPECT_EQ(3ul, dft->nrElements());
EXPECT_EQ(2ul, dft->nrBasicElements());
}
}
Write Preview
Loading…
Cancel
Save