Browse Source

export gspns to ctmcs/mdps if no intermediate/timed transitions occur.

tempestpy_adaptions
TimQu 6 years ago
parent
commit
ad88992ba2
  1. 8
      src/storm-gspn/builder/JaniGSPNBuilder.cpp

8
src/storm-gspn/builder/JaniGSPNBuilder.cpp

@ -9,7 +9,13 @@ namespace storm {
namespace builder { namespace builder {
storm::jani::Model* JaniGSPNBuilder::build(std::string const& automatonName, bool buildStandardProperties) { storm::jani::Model* JaniGSPNBuilder::build(std::string const& automatonName, bool buildStandardProperties) {
storm::jani::Model* model = new storm::jani::Model(gspn.getName(), storm::jani::ModelType::MA, janiVersion, expressionManager);
storm::jani::ModelType modelType = storm::jani::ModelType::MA;
if (gspn.getNumberOfTimedTransitions() == 0) {
storm::jani::ModelType modelType = storm::jani::ModelType::MDP;
} else if (gspn.getNumberOfImmediateTransitions() == 0) {
storm::jani::ModelType modelType = storm::jani::ModelType::CTMC;
}
storm::jani::Model* model = new storm::jani::Model(gspn.getName(), modelType, janiVersion, expressionManager);
storm::jani::Automaton mainAutomaton(automatonName, expressionManager->declareIntegerVariable("loc")); storm::jani::Automaton mainAutomaton(automatonName, expressionManager->declareIntegerVariable("loc"));
addVariables(model); addVariables(model);
uint64_t locId = addLocation(mainAutomaton); uint64_t locId = addLocation(mainAutomaton);

Loading…
Cancel
Save