From d7ec0b65e8e11b4e763fa7dfcdea6715d9317a0e Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 9 Oct 2018 16:33:06 +0200 Subject: [PATCH] Conversion of Prism PTAs to Jani PTAs --- src/storm/storage/prism/ToJaniConverter.cpp | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index a780200f2..855ece20c 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -38,6 +38,8 @@ namespace storm { break; case Program::ModelType::MA: modelType = storm::jani::ModelType::MA; break; + case Program::ModelType::PTA: modelType = storm::jani::ModelType::PTA; + break; default: modelType = storm::jani::ModelType::UNDEFINED; } storm::jani::Model janiModel("jani_from_prism", modelType, 1, manager); @@ -359,12 +361,29 @@ namespace storm { STORM_LOG_INFO("Variable " << variable.getName() << " is declared but never used."); } } + for (auto const& variable : module.getClockVariables()) { + storm::jani::ClockVariable newClockVariable = *storm::jani::makeClockVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false); + auto findRes = variablesToMakeGlobal.find(variable.getExpressionVariable()); + if (findRes != variablesToMakeGlobal.end()) { + bool makeVarGlobal = findRes->second; + storm::jani::ClockVariable const& createdVariable = makeVarGlobal ? janiModel.addVariable(newClockVariable) : automaton.addVariable(newClockVariable); + variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); + } else { + STORM_LOG_INFO("Variable " << variable.getName() << " is declared but never used."); + } + } + automaton.setInitialStatesRestriction(manager->boolean(true)); // Create a single location that will have all the edges. uint64_t onlyLocationIndex = automaton.addLocation(storm::jani::Location("l")); automaton.addInitialLocation(onlyLocationIndex); + if (module.hasInvariant()) { + storm::jani::Location& onlyLocation = automaton.getLocation(onlyLocationIndex); + onlyLocation.setTimeProgressInvariant(module.getInvariant()); + } + // If we are translating the first module that has the action, we need to add the transient assignments to the location. // However, in standard compliant JANI, there are no state rewards if (firstModule) {