|
|
@ -8,71 +8,70 @@ |
|
|
|
#include <fstream>
|
|
|
|
#include <iostream>
|
|
|
|
#include <string>
|
|
|
|
// TODO clean-up includes after doing all other todos
|
|
|
|
|
|
|
|
|
|
|
|
/*!
|
|
|
|
* Parses the arguments to storm-gspn |
|
|
|
* The read data is stored in the different arguments (e.g., inputFile, formula, ...) |
|
|
|
* |
|
|
|
* @param argc number of arguments passed to storm-gspn |
|
|
|
* @param argv array of arguments |
|
|
|
* @param begin pointer to the first argument passed to storm-gspn |
|
|
|
* @param end pointer to one past the last argument passed to storm-gspn |
|
|
|
* @param inputFile the input file is stored in this object |
|
|
|
* @param formula the formula is stored in this object |
|
|
|
* @param outputFile the output file is stored in this object |
|
|
|
* @param outputType the output type is stored in this object |
|
|
|
* @return false if the help flag is set or the input file is missing |
|
|
|
*/ |
|
|
|
bool parseArguments(const int argc, const char **argv, std::string &inputFile, std::string &formula, |
|
|
|
bool parseArguments(const char **begin, const char **end, std::string &inputFile, std::string &formula, |
|
|
|
std::string &outputFile, std::string &outputType) { |
|
|
|
auto end = argv + argc; |
|
|
|
bool result = false; |
|
|
|
|
|
|
|
for (auto it = argv; it != end; ++it) { |
|
|
|
std::string currentArg = *it; |
|
|
|
for (; begin != end; ++begin) { |
|
|
|
std::string currentArg = *begin; |
|
|
|
|
|
|
|
// parse input file argument
|
|
|
|
if (currentArg == "--input_file" || currentArg == "-i") { |
|
|
|
auto next = it + 1; |
|
|
|
auto next = begin + 1; |
|
|
|
if (next != end) { |
|
|
|
inputFile = *next; |
|
|
|
result = true; |
|
|
|
} else { |
|
|
|
return -1; |
|
|
|
} |
|
|
|
break; |
|
|
|
continue; |
|
|
|
} |
|
|
|
|
|
|
|
// parse formula argument
|
|
|
|
if (currentArg == "--formula" || currentArg == "-f") { |
|
|
|
auto next = it + 1; |
|
|
|
auto next = begin + 1; |
|
|
|
if (next != end) { |
|
|
|
formula = *next; |
|
|
|
} else { |
|
|
|
return -1; |
|
|
|
} |
|
|
|
break; |
|
|
|
continue; |
|
|
|
} |
|
|
|
|
|
|
|
// parse output file argument
|
|
|
|
if (currentArg == "--output_file" || currentArg == "-o") { |
|
|
|
auto next = it + 1; |
|
|
|
auto next = begin + 1; |
|
|
|
if (next != end) { |
|
|
|
outputFile = *next; |
|
|
|
} else { |
|
|
|
return -1; |
|
|
|
} |
|
|
|
break; |
|
|
|
continue; |
|
|
|
} |
|
|
|
|
|
|
|
// parse output file type argument
|
|
|
|
if (currentArg == "--output_type" || currentArg == "-ot") { |
|
|
|
auto next = it + 1; |
|
|
|
auto next = begin + 1; |
|
|
|
if (next != end) { |
|
|
|
outputType = *next; |
|
|
|
} else { |
|
|
|
return -1; |
|
|
|
} |
|
|
|
break; |
|
|
|
continue; |
|
|
|
} |
|
|
|
|
|
|
|
// parse help argument
|
|
|
@ -94,12 +93,12 @@ void printHelp() { |
|
|
|
std::cout << "-f, --formula: formula which should be checked on the gspn" << std::endl; |
|
|
|
std::cout << "-o, -output_file: file in which the gspn/markov automaton should be stored" << std::endl |
|
|
|
<< " requires the option -ot to be set" << std::endl; |
|
|
|
std::cout << "-ot, --output_type: possible output types are: pnml, pnpro or ma" << std::endl; |
|
|
|
std::cout << "-ot, --output_type: possible output types are: pnml, pnpro, dot or ma" << std::endl; |
|
|
|
} |
|
|
|
|
|
|
|
int main(const int argc, const char **argv) { |
|
|
|
std::string inputFile, formula, outputFile, outputType; |
|
|
|
if (!parseArguments(argc, argv, inputFile, formula, outputFile, outputType)) { |
|
|
|
if (!parseArguments(argv+1, argv+argc, inputFile, formula, outputFile, outputType)) { |
|
|
|
printHelp(); |
|
|
|
return 1; |
|
|
|
} |
|
|
@ -107,40 +106,36 @@ int main(const int argc, const char **argv) { |
|
|
|
try { |
|
|
|
storm::utility::setUp(); |
|
|
|
|
|
|
|
// parse GSPN from file
|
|
|
|
// parse gspn from file
|
|
|
|
auto parser = storm::parser::GspnParser(); |
|
|
|
auto gspn = parser.parse(inputFile); |
|
|
|
|
|
|
|
// todo ------[marker]
|
|
|
|
std::cout << "valid? = " << gspn.isValid() << std::endl; |
|
|
|
/*
|
|
|
|
storm::gspn::GspnBuilder builder2; |
|
|
|
builder2.addPlace(2); |
|
|
|
if (!gspn.isValid()) { |
|
|
|
STORM_LOG_ERROR("The gspn is not valid."); |
|
|
|
} |
|
|
|
|
|
|
|
//
|
|
|
|
//std::ofstream file;
|
|
|
|
//file.open("/Users/thomas/Desktop/storm.dot");
|
|
|
|
//gspn.writeDotToStream(file);
|
|
|
|
//file.close();
|
|
|
|
// construct ma
|
|
|
|
auto builder = storm::builder::ExplicitGspnModelBuilder<>(); |
|
|
|
auto ma = builder.translateGspn(gspn, formula); |
|
|
|
|
|
|
|
// write gspn into output file
|
|
|
|
if (!outputFile.empty()) { |
|
|
|
std::ofstream file; |
|
|
|
file.open("/Users/thomas/Desktop/gspn.pnpro"); |
|
|
|
file.open(outputFile); |
|
|
|
if (outputType == "pnml") { |
|
|
|
gspn.toPnml(file); |
|
|
|
} |
|
|
|
if (outputType == "pnpro") { |
|
|
|
gspn.toPnpro(file); |
|
|
|
} |
|
|
|
if (outputType == "dot") { |
|
|
|
gspn.writeDotToStream(file); |
|
|
|
} |
|
|
|
if (outputType == "ma") { |
|
|
|
ma.writeDotToStream(file); |
|
|
|
} |
|
|
|
file.close(); |
|
|
|
|
|
|
|
std::cout << "Parsing complete!" << std::endl; |
|
|
|
|
|
|
|
|
|
|
|
// Construct MA
|
|
|
|
auto builder = storm::builder::ExplicitGspnModelBuilder<>(); |
|
|
|
auto ma = builder.translateGspn(gspn, argv[2]); |
|
|
|
std::cout << "Markov Automaton: " << std::endl; |
|
|
|
std::cout << "number of states: " << ma.getNumberOfStates() << std::endl; |
|
|
|
std::cout << "number of transitions: " << ma.getNumberOfTransitions() << std::endl << std::endl; |
|
|
|
|
|
|
|
*/ |
|
|
|
|
|
|
|
|
|
|
|
} |
|
|
|
|
|
|
|
// All operations have now been performed, so we clean up everything and terminate.
|
|
|
|
storm::utility::cleanUp(); |
|
|
|