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

storm-gspn and storm-dft now use functionalities of storm-conv

main
TimQu 7 years ago
parent
c268926568
commit
4a7a82627f
8 changed files with 53 additions and 32 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. 33
      src/storm-dft/api/storm-dft.cpp
  2. 2
      src/storm-dft/settings/DftSettings.cpp
  3. 8
      src/storm-gspn-cli/storm-gspn.cpp
  4. 2
      src/storm-gspn/CMakeLists.txt
  5. 14
      src/storm-gspn/api/storm-gspn.cpp
  6. 4
      src/storm-gspn/api/storm-gspn.h
  7. 11
      src/storm-gspn/settings/modules/GSPNExportSettings.cpp
  8. 11
      src/storm-gspn/settings/modules/GSPNExportSettings.h

33
src/storm-dft/api/storm-dft.cpp
View File

@ -34,25 +34,20 @@ namespace storm {
storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN();
uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId();
storm::api::handleGSPNExportSettings(*gspn);
std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn->getExpressionManager();
storm::builder::JaniGSPNBuilder builder(*gspn);
storm::jani::Model* model = builder.build();
storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression();
auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(targetExpression);
auto tbFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time));
auto tbUntil = std::make_shared<storm::logic::ProbabilityOperatorFormula>(tbFormula);
auto evFormula = std::make_shared<storm::logic::EventuallyFormula>(evtlFormula, storm::logic::FormulaContext::Time);
auto rewFormula = std::make_shared<storm::logic::TimeOperatorFormula>(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation);
storm::settings::modules::JaniExportSettings const& janiSettings = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
if (janiSettings.isJaniFileSet()) {
storm::api::exportJaniModel(*model, {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)}, janiSettings.getJaniFilename());
}
storm::api::handleGSPNExportSettings(*gspn, [&]std::vector<storm::jani::Property>(storm::builder::JaniGSPNBuilder const& builder) {
std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = gspn->getExpressionManager();
storm::jani::Variable const& topfailedVar = builder.getPlaceVariable(toplevelFailedPlace);
storm::expressions::Expression targetExpression = exprManager->integer(1) == topfailedVar.getExpressionVariable().getExpression();
auto evtlFormula = std::make_shared<storm::logic::AtomicExpressionFormula>(targetExpression);
auto tbFormula = std::make_shared<storm::logic::BoundedUntilFormula>(std::make_shared<storm::logic::BooleanLiteralFormula>(true), evtlFormula, storm::logic::TimeBound(false, exprManager->integer(0)), storm::logic::TimeBound(false, exprManager->integer(10)), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time));
auto tbUntil = std::make_shared<storm::logic::ProbabilityOperatorFormula>(tbFormula);
auto evFormula = std::make_shared<storm::logic::EventuallyFormula>(evtlFormula, storm::logic::FormulaContext::Time);
auto rewFormula = std::make_shared<storm::logic::TimeOperatorFormula>(evFormula, storm::logic::OperatorInformation(), storm::logic::RewardMeasureType::Expectation);
return {storm::jani::Property("time-bounded", tbUntil), storm::jani::Property("mttf", rewFormula)};
}
);
delete model;
delete gspn;

2
src/storm-dft/settings/DftSettings.cpp
View File

@ -19,7 +19,7 @@
#include "storm/settings/modules/GameSolverSettings.h"
#include "storm/settings/modules/BisimulationSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/JaniExportSettings.h"
#include "storm-conv/settings/modules/JaniExportSettings.h"
#include "storm-gspn/settings/modules/GSPNSettings.h"
#include "storm-gspn/settings/modules/GSPNExportSettings.h"

8
src/storm-gspn-cli/storm-gspn.cpp
View File

@ -112,14 +112,8 @@ int main(const int argc, const char **argv) {
gspn->setCapacities(capacities);
}
storm::api::handleGSPNExportSettings(*gspn);
storm::api::handleGSPNExportSettings(*gspn, [&]std::vector<storm::jani::Property>(storm::builder::JaniGSPNBuilder const&) { return properties });
if(storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
storm::jani::Model* model = storm::api::buildJani(*gspn);
storm::api::exportJaniModel(*model, properties, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
delete model;
}
delete gspn;
return 0;

2
src/storm-gspn/CMakeLists.txt
View File

@ -12,7 +12,7 @@ file(GLOB_RECURSE STORM_GSPN_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h)
add_library(storm-gspn SHARED ${STORM_GSPN_SOURCES} ${STORM_GSPN_HEADERS})
list(APPEND STORM_TARGETS storm-gspn)
set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
target_link_libraries(storm-gspn storm ${STORM_GSPN_LINK_LIBRARIES})
target_link_libraries(storm-gspn storm storm-conv ${STORM_GSPN_LINK_LIBRARIES})
# installation
install(TARGETS storm-gspn EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)

14
src/storm-gspn/api/storm-gspn.cpp
View File

@ -3,6 +3,8 @@
#include "storm/settings/SettingsManager.h"
#include "storm/utility/file.h"
#include "storm-gspn/settings/modules/GSPNExportSettings.h"
#include "storm-conv/settings/modules/JaniExportSettings.h"
#include "storm-conv/api/storm-conv.h"
namespace storm {
@ -13,7 +15,7 @@ namespace storm {
return builder.build();
}
void handleGSPNExportSettings(storm::gspn::GSPN const& gspn) {
void handleGSPNExportSettings(storm::gspn::GSPN const& gspn, std::vector<storm::jani::Property> const& properties) {
storm::settings::modules::GSPNExportSettings const& exportSettings = storm::settings::getModule<storm::settings::modules::GSPNExportSettings>();
if (exportSettings.isWriteToDotSet()) {
std::ofstream fs;
@ -55,6 +57,16 @@ namespace storm {
gspn.writeStatsToStream(fs);
storm::utility::closeFile(fs);
}
if (exportSettings.isWriteToJaniSet()) {
auto const& jani = storm::settings::getModule<storm::settings::modules::JaniExportSettings>();
storm::converter::JaniConversionOptions options(jani);
storm::jani::Model* model = storm::api::buildJani(gspn);
storm::api::postprocessJani(*model, options);
storm::api::exportJaniToFile(*model, properties, storm::settings::getModule<storm::settings::modules::GSPNExportSettings>().getWriteToJaniFilename());
delete model;
}
}
}

4
src/storm-gspn/api/storm-gspn.h
View File

@ -12,6 +12,8 @@ namespace storm {
*/
storm::jani::Model* buildJani(storm::gspn::GSPN const& gspn);
void handleGSPNExportSettings(storm::gspn::GSPN const& gspn);
void handleGSPNExportSettings(storm::gspn::GSPN const& gspn,
std::function<std::vector<storm::jani::Property>(storm::builder::JaniGSPNBuilder const&)> const& janiProperyGetter = [](storm::builder::JaniGSPNBuilder const&) { return std::vector<storm::jani::Property>(); });
}
}

11
src/storm-gspn/settings/modules/GSPNExportSettings.cpp
View File

@ -1,5 +1,4 @@
#include "storm-gspn/settings/modules/GSPNExportSettings.h"
#include "storm/settings/modules/JaniExportSettings.h"
#include "storm/settings/SettingsManager.h"
#include "storm/settings/SettingMemento.h"
@ -20,6 +19,7 @@ namespace storm {
const std::string GSPNExportSettings::writeToPnmlOptionName = "to-pnml";
const std::string GSPNExportSettings::writeToPnproOptionName = "to-pnpro";
const std::string GSPNExportSettings::writeToJsonOptionName = "to-json";
const std::string GSPNExportSettings::writeToJaniOptionName = "to-jani";
const std::string GSPNExportSettings::writeStatsOptionName = "to-stats";
const std::string GSPNExportSettings::displayStatsOptionName = "show-stats";
@ -31,6 +31,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, writeToPnmlOptionName, false, "Destination for the pnml output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, writeToPnproOptionName, false, "Destination for the pnpro output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, writeToJsonOptionName, false, "Destination for the json output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, writeToJaniOptionName, false, "Destination for the jani output").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, writeStatsOptionName, false, "Destination for the stats file").addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build());
}
@ -67,6 +68,14 @@ namespace storm {
return this->getOption(writeToJsonOptionName).getArgumentByName("filename").getValueAsString();
}
bool GSPNExportSettings::isWriteToJaniSet() const {
return this->getOption(writeToJaniOptionName).getHasOptionBeenSet();
}
std::string GSPNExportSettings::getWriteToJaniFilename() const {
return this->getOption(writeToJaniOptionName).getArgumentByName("filename").getValueAsString();
}
bool GSPNExportSettings::isDisplayStatsSet() const {
return this->getOption(displayStatsOptionName).getHasOptionBeenSet();
}

11
src/storm-gspn/settings/modules/GSPNExportSettings.h
View File

@ -10,7 +10,7 @@ namespace storm {
class GSPNExportSettings : public ModuleSettings {
public:
/*!
* Creates a new JaniExport setting
* Creates a new GSPNExport setting
*/
GSPNExportSettings();
@ -45,6 +45,14 @@ namespace storm {
*/
std::string getWriteToJsonFilename() const;
bool isWriteToJaniSet() const;
/**
*
*/
std::string getWriteToJaniFilename() const;
bool isDisplayStatsSet() const;
bool isWriteStatsToFileSet() const;
@ -62,6 +70,7 @@ namespace storm {
static const std::string writeToPnmlOptionName;
static const std::string writeToPnproOptionName;
static const std::string writeToJsonOptionName;
static const std::string writeToJaniOptionName;
static const std::string displayStatsOptionName;
static const std::string writeStatsOptionName;

Write Preview
Loading…
Cancel
Save