From ad88992ba2e2ee6315545508406a94d6a63f882b Mon Sep 17 00:00:00 2001 From: TimQu Date: Thu, 23 Aug 2018 13:44:09 +0200 Subject: [PATCH] export gspns to ctmcs/mdps if no intermediate/timed transitions occur. --- src/storm-gspn/builder/JaniGSPNBuilder.cpp | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index d21ef5c21..744b76eb4 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -9,7 +9,13 @@ namespace storm { namespace builder { 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")); addVariables(model); uint64_t locId = addLocation(mainAutomaton);