Browse Source

Merge remote-tracking branch 'origin/jani_support' into jani_explicit_jit

Former-commit-id: c1326199f8 [formerly 5037cdd8b7]
Former-commit-id: c52ecdd86c
main
dehnert 8 years ago
parent
commit
1eed49aa38
  1. 6
      resources/3rdparty/CMakeLists.txt
  2. 206
      resources/cmake/find_modules/FindHwloc.cmake
  3. 81
      src/builder/DdJaniModelBuilder.cpp
  4. 20
      src/builder/DdJaniModelBuilder.h
  5. 48
      src/builder/JaniProgramGraphBuilder.cpp
  6. 59
      src/builder/JaniProgramGraphBuilder.h
  7. 24
      src/cli/cli.cpp
  8. 14
      src/generator/CompressedState.cpp
  9. 89
      src/generator/JaniNextStateGenerator.cpp
  10. 2
      src/generator/JaniNextStateGenerator.h
  11. 12
      src/generator/NextStateGenerator.cpp
  12. 2
      src/generator/NextStateGenerator.h
  13. 35
      src/generator/PrismNextStateGenerator.cpp
  14. 41
      src/generator/VariableInformation.cpp
  15. 7
      src/generator/VariableInformation.h
  16. 84
      src/parser/JaniParser.cpp
  17. 2
      src/settings/modules/PGCLSettings.cpp
  18. 2
      src/storage/BitVector.h
  19. 28
      src/storage/IntegerInterval.cpp
  20. 1
      src/storage/IntegerInterval.h
  21. 343
      src/storage/jani/JSONExporter.cpp
  22. 34
      src/storage/jani/JSONExporter.h
  23. 33
      src/storage/jani/Model.cpp
  24. 6
      src/storage/jani/Model.h
  25. 9
      src/storage/jani/Property.cpp
  26. 39
      src/storage/jani/Property.h
  27. 20
      src/storage/jani/VariableSet.cpp
  28. 10
      src/storage/jani/VariableSet.h
  29. 28
      src/storage/ppg/ProgramGraph.h
  30. 2
      src/storage/ppg/defines.h
  31. 4
      src/storage/prism/Module.cpp
  32. 5
      src/storm-pgcl.cpp

6
resources/3rdparty/CMakeLists.txt

@ -357,9 +357,9 @@ add_dependencies(resources sylvan)
if(${OPERATING_SYSTEM} MATCHES "Linux")
find_package(Hwloc QUIET REQUIRED)
if(Hwloc_FOUND)
message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}")
list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES})
if(HWLOC_FOUND)
message(STATUS "StoRM - Linking with hwloc ${HWLOC_VERSION}")
list(APPEND STORM_LINK_LIBRARIES ${HWLOC_LIBRARIES})
else()
message(FATAL_ERROR "HWLOC is required but was not found.")
endif()

206
resources/cmake/find_modules/FindHwloc.cmake

@ -1,179 +1,55 @@
# FindHwloc
# ----------
# Try to find hwloc libraries and headers.
#
# Try to find Portable Hardware Locality (hwloc) libraries.
# http://www.open-mpi.org/software/hwloc
# Usage of this module:
#
# You may declare HWLOC_ROOT environment variable to tell where
# your hwloc library is installed.
# find_package(hwloc)
#
# Once done this will define::
# Variables defined by this module:
#
# Hwloc_FOUND - True if hwloc was found
# Hwloc_INCLUDE_DIRS - include directories for hwloc
# Hwloc_LIBRARIES - link against these libraries to use hwloc
# Hwloc_VERSION - version
# Hwloc_CFLAGS - include directories as compiler flags
# Hwloc_LDLFAGS - link paths and libs as compiler flags
#
#=============================================================================
# Copyright 2014 Mikael Lepistö
#
# Distributed under the OSI-approved BSD License (the "License");
#
# This software is distributed WITHOUT ANY WARRANTY; without even the
# implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
# See the License for more information.
#=============================================================================
if(WIN32)
find_path(Hwloc_INCLUDE_DIR
NAMES
hwloc.h
PATHS
ENV "PROGRAMFILES(X86)"
ENV HWLOC_ROOT
PATH_SUFFIXES
include
)
find_library(Hwloc_LIBRARY
NAMES
libhwloc.lib
PATHS
ENV "PROGRAMFILES(X86)"
ENV HWLOC_ROOT
PATH_SUFFIXES
lib
)
#
# Check if the found library can be used to linking
#
SET (_TEST_SOURCE "${CMAKE_BINARY_DIR}${CMAKE_FILES_DIRECTORY}/linktest.c")
FILE (WRITE "${_TEST_SOURCE}"
"
#include <hwloc.h>
int main()
{
hwloc_topology_t topology;
int nbcores;
hwloc_topology_init(&topology);
hwloc_topology_load(topology);
nbcores = hwloc_get_nbobjs_by_type(topology, HWLOC_OBJ_CORE);
hwloc_topology_destroy(topology);
return 0;
}
"
)
TRY_COMPILE(_LINK_SUCCESS ${CMAKE_BINARY_DIR} "${_TEST_SOURCE}"
CMAKE_FLAGS
"-DINCLUDE_DIRECTORIES:STRING=${Hwloc_INCLUDE_DIR}"
CMAKE_FLAGS
"-DLINK_LIBRARIES:STRING=${Hwloc_LIBRARY}"
)
IF(NOT _LINK_SUCCESS)
if(CMAKE_SIZEOF_VOID_P EQUAL 8)
message(STATUS "You are building 64bit target.")
ELSE()
message(STATUS "You are building 32bit code. If you like to build x64 use e.g. -G 'Visual Studio 12 Win64' generator." )
ENDIF()
message(FATAL_ERROR "Library found, but linking test program failed.")
ENDIF()
#
# Resolve version if some compiled binary found...
#
find_program(HWLOC_INFO_EXECUTABLE
NAMES
hwloc-info
PATHS
ENV HWLOC_ROOT
PATH_SUFFIXES
bin
)
if(HWLOC_INFO_EXECUTABLE)
execute_process(
COMMAND ${HWLOC_INFO_EXECUTABLE} "--version"
OUTPUT_VARIABLE HWLOC_VERSION_LINE
OUTPUT_STRIP_TRAILING_WHITESPACE
)
string(REGEX MATCH "([0-9]+.[0-9]+)$"
Hwloc_VERSION "${HWLOC_VERSION_LINE}")
unset(HWLOC_VERSION_LINE)
endif()
#
# All good
#
set(Hwloc_LIBRARIES ${Hwloc_LIBRARY})
set(Hwloc_INCLUDE_DIRS ${Hwloc_INCLUDE_DIR})
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(
Hwloc
FOUND_VAR Hwloc_FOUND
REQUIRED_VARS Hwloc_LIBRARY Hwloc_INCLUDE_DIR
VERSION_VAR Hwloc_VERSION)
mark_as_advanced(
Hwloc_INCLUDE_DIR
Hwloc_LIBRARY)
foreach(arg ${Hwloc_INCLUDE_DIRS})
set(Hwloc_CFLAGS "${Hwloc_CFLAGS} /I${arg}")
endforeach()
# HWLOC_FOUND System has hwloc libraries and headers
# HWLOC_LIBRARIES The hwloc library
# HWLOC_INCLUDE_DIRS The location of HWLOC headers
set(Hwloc_LDFLAGS "${Hwloc_LIBRARY}")
find_path(
HWLOC_PREFIX
NAMES include/hwloc.h
)
else()
if (NOT HWLOC_PREFIX AND NOT $ENV{HWLOC_BASE} STREQUAL "")
set(HWLOC_PREFIX $ENV{HWLOC_BASE})
endif()
# Find with pkgconfig
find_package(PkgConfig)
message(STATUS "Searching for hwloc library in path " ${HWLOC_PREFIX})
if(HWLOC_ROOT)
set(ENV{PKG_CONFIG_PATH} "${HWLOC_ROOT}/lib/pkgconfig")
else()
foreach(PREFIX ${CMAKE_PREFIX_PATH})
set(PKG_CONFIG_PATH "${PKG_CONFIG_PATH}:${PREFIX}/lib/pkgconfig")
endforeach()
set(ENV{PKG_CONFIG_PATH} "${PKG_CONFIG_PATH}:$ENV{PKG_CONFIG_PATH}")
endif()
find_library(
HWLOC_LIBRARIES
NAMES hwloc
HINTS ${HWLOC_PREFIX}/lib
)
if(hwloc_FIND_REQUIRED)
set(_hwloc_OPTS "REQUIRED")
elseif(hwloc_FIND_QUIETLY)
set(_hwloc_OPTS "QUIET")
else()
set(_hwloc_output 1)
endif()
find_path(
HWLOC_INCLUDE_DIRS
NAMES hwloc.h
HINTS ${HWLOC_PREFIX}/include
)
if(hwloc_FIND_VERSION)
if(hwloc_FIND_VERSION_EXACT)
pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc=${hwloc_FIND_VERSION})
else()
pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc>=${hwloc_FIND_VERSION})
endif()
else()
pkg_check_modules(Hwloc ${_hwloc_OPTS} hwloc)
endif()
include(FindPackageHandleStandardArgs)
if(Hwloc_FOUND)
include(FindPackageHandleStandardArgs)
find_package_handle_standard_args(Hwloc DEFAULT_MSG Hwloc_LIBRARIES)
find_package_handle_standard_args(
HWLOC DEFAULT_MSG
HWLOC_LIBRARIES
HWLOC_INCLUDE_DIRS
)
if(NOT ${Hwloc_VERSION} VERSION_LESS 1.7.0)
set(Hwloc_GL_FOUND 1)
endif()
mark_as_advanced(
HWLOC_LIBRARIES
HWLOC_INCLUDE_DIRS
)
if(_hwloc_output)
message(STATUS
"Found hwloc ${Hwloc_VERSION} in ${Hwloc_INCLUDE_DIRS}:${Hwloc_LIBRARIES}")
endif()
if (HWLOC_FOUND)
if (NOT $ENV{HWLOC_LIB} STREQUAL "")
# set(HWLOC_LIBRARIES "$ENV{HWLOC_LIB}")
endif()
endif()
message(STATUS "hwloc includes: " ${HWLOC_INCLUDE_DIRS})
message(STATUS "hwloc libraries: " ${HWLOC_LIBRARIES})
endif()

81
src/builder/DdJaniModelBuilder.cpp

@ -15,6 +15,8 @@
#include "src/storage/dd/Bdd.h"
#include "src/adapters/AddExpressionAdapter.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/models/symbolic/Dtmc.h"
#include "src/models/symbolic/Ctmc.h"
#include "src/models/symbolic/Mdp.h"
@ -28,6 +30,7 @@
#include "src/utility/dd.h"
#include "src/utility/math.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/InvalidSettingsException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/NotSupportedException.h"
@ -36,7 +39,7 @@ namespace storm {
namespace builder {
template <storm::dd::DdType Type, typename ValueType>
DdJaniModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
DdJaniModelBuilder<Type, ValueType>::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
}
@ -47,7 +50,7 @@ namespace storm {
}
template <storm::dd::DdType Type, typename ValueType>
DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
if (formulas.empty()) {
this->buildAllRewardModels = true;
} else {
@ -75,6 +78,12 @@ namespace storm {
std::set<std::string> referencedRewardModels = formula.getReferencedRewardModels();
rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end());
}
// Extract all the labels used in the formula.
std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas();
for (auto const& formula : atomicLabelFormulas) {
addLabel(formula->getLabel());
}
}
template <storm::dd::DdType Type, typename ValueType>
@ -112,7 +121,18 @@ namespace storm {
bool DdJaniModelBuilder<Type, ValueType>::Options::isBuildAllRewardModelsSet() const {
return buildAllRewardModels;
}
template <storm::dd::DdType Type, typename ValueType>
bool DdJaniModelBuilder<Type, ValueType>::Options::isBuildAllLabelsSet() const {
return buildAllLabels;
}
template <storm::dd::DdType Type, typename ValueType>
void DdJaniModelBuilder<Type, ValueType>::Options::addLabel(std::string const& labelName) {
STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway.");
labelNames.insert(labelName);
}
template <storm::dd::DdType Type, typename ValueType>
struct CompositionVariables {
CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()),
@ -138,8 +158,9 @@ namespace storm {
// All pairs of row/column meta variables.
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
// A mapping from automata to the meta variable encoding their location.
std::map<std::string, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationVariableMap;
// A mapping from automata to the meta variables encoding their location.
std::map<std::string, storm::expressions::Variable> automatonToLocationVariableMap;
std::map<std::string, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationDdVariableMap;
// A mapping from action indices to the meta variables used to encode these actions.
std::map<uint64_t, storm::expressions::Variable> actionVariablesMap;
@ -245,9 +266,14 @@ namespace storm {
for (auto const& automaton : this->model.getAutomata()) {
// Start by creating a meta variable for the location of the automaton.
storm::expressions::Variable locationExpressionVariable = model.getManager().declareFreshIntegerVariable(false, "loc");
result.automatonToLocationVariableMap[automaton.getName()] = locationExpressionVariable;
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1);
result.automatonToLocationVariableMap[automaton.getName()] = variablePair;
result.automatonToLocationDdVariableMap[automaton.getName()] = variablePair;
result.rowColumnMetaVariablePairs.push_back(variablePair);
result.variableToRowMetaVariableMap->emplace(locationExpressionVariable, variablePair.first);
result.variableToColumnMetaVariableMap->emplace(locationExpressionVariable, variablePair.second);
// Add the location variable to the row/column variables.
result.rowMetaVariables.insert(variablePair.first);
@ -277,7 +303,7 @@ namespace storm {
storm::dd::Bdd<Type> range = result.manager->getBddOne();
// Add the identity and ranges of the location variables to the ones of the automaton.
std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationVariableMap[automaton.getName()];
std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationDdVariableMap[automaton.getName()];
storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(locationVariables.first).equals(result.manager->template getIdentity<ValueType>(locationVariables.second)).template toAdd<ValueType>() * result.manager->getRange(locationVariables.first).template toAdd<ValueType>() * result.manager->getRange(locationVariables.second).template toAdd<ValueType>();
identity &= variableIdentity.toBdd();
range &= result.manager->getRange(locationVariables.first);
@ -458,7 +484,7 @@ namespace storm {
}
}
transitions *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd<ValueType>();
transitions *= variables.manager->getEncoding(variables.automatonToLocationDdVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd<ValueType>();
return EdgeDestinationDd<Type, ValueType>(transitions, assignedGlobalVariables);
}
@ -869,7 +895,6 @@ namespace storm {
if (action.isInputEnabled()) {
// If the action is input-enabled, we add self-loops to all states.
transitions *= actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second);
actionGuard.ite(action.transitions, encodeIndex(0, action.getLowestLocalNondeterminismVariable(), action.getHighestLocalNondeterminismVariable() - action.getLowestLocalNondeterminismVariable(), this->variables) * actionIdentityPair.second).exportToDot("this.dot");
} else {
transitions *= action.transitions;
}
@ -1081,7 +1106,8 @@ namespace storm {
}
// Add the source location and the guard.
transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
storm::dd::Add<Type, ValueType> sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
transitions *= sourceLocationAndGuard;
// If we multiply the ranges of global variables, make sure everything stays within its bounds.
if (!globalVariablesInSomeDestination.empty()) {
@ -1098,7 +1124,9 @@ namespace storm {
// Finally treat the transient assignments.
std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
if (!this->transientVariables.empty()) {
performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard] (storm::jani::Assignment const& assignment) { transientEdgeAssignments[assignment.getExpressionVariable()] = guard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); } );
performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guard, &sourceLocationAndGuard] (storm::jani::Assignment const& assignment) {
transientEdgeAssignments[assignment.getExpressionVariable()] = sourceLocationAndGuard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
} );
}
return EdgeDd(isMarkovian, guard, guard * transitions, transientEdgeAssignments, globalVariablesInSomeDestination);
@ -1475,7 +1503,7 @@ namespace storm {
for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) {
auto const& location = automaton.getLocation(locationIndex);
performTransientAssignments(location.getAssignments().getTransientAssignments(), [this,&automatonName,locationIndex,&result] (storm::jani::Assignment const& assignment) {
storm::dd::Add<Type, ValueType> assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automatonName).first, locationIndex).template toAdd<ValueType>() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
storm::dd::Add<Type, ValueType> assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automatonName).first, locationIndex).template toAdd<ValueType>() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
auto it = result.transientLocationAssignments.find(assignment.getExpressionVariable());
if (it != result.transientLocationAssignments.end()) {
it->second += assignedValues;
@ -1557,17 +1585,18 @@ namespace storm {
storm::dd::Bdd<Type> deadlockStates;
storm::dd::Add<Type, ValueType> transitionMatrix;
std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
std::map<std::string, storm::expressions::Expression> labelToExpressionMap;
};
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
if (modelType == storm::jani::ModelType::DTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
} else if (modelType == storm::jani::ModelType::CTMC) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
} else if (modelType == storm::jani::ModelType::MDP) {
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
}
@ -1635,7 +1664,7 @@ namespace storm {
for (auto const& automaton : model.getAutomata()) {
storm::dd::Bdd<Type> initialLocationIndices = variables.manager->getBddZero();
for (auto const& locationIndex : automaton.getInitialLocationIndices()) {
initialLocationIndices |= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, locationIndex);
initialLocationIndices |= variables.manager->getEncoding(variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, locationIndex);
}
initialStates &= initialLocationIndices;
}
@ -1698,7 +1727,7 @@ namespace storm {
std::vector<storm::expressions::Variable> result;
if (options.isBuildAllRewardModelsSet()) {
for (auto const& variable : model.getGlobalVariables()) {
if (variable.isTransient()) {
if (variable.isTransient() && (variable.isRealVariable() || variable.isUnboundedIntegerVariable())) {
result.push_back(variable.getExpressionVariable());
}
}
@ -1709,7 +1738,7 @@ namespace storm {
result.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable());
} else {
STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
}
}
@ -1748,6 +1777,21 @@ namespace storm {
return result;
}
template <storm::dd::DdType Type, typename ValueType>
std::map<std::string, storm::expressions::Expression> buildLabelExpressions(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
std::map<std::string, storm::expressions::Expression> result;
for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
if (variable->isBooleanVariable()) {
if (options.buildAllLabels || options.labelNames.find(variable->getName()) != options.labelNames.end()) {
result[variable->getName()] = model.getLabelExpression(variable->asBooleanVariable(), variables.automatonToLocationVariableMap);
}
}
}
return result;
}
template <storm::dd::DdType Type, typename ValueType>
std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::build(storm::jani::Model const& model, Options const& options) {
if (model.hasUndefinedConstants()) {
@ -1814,6 +1858,9 @@ namespace storm {
// Build the reward models.
modelComponents.rewardModels = buildRewardModels(system, rewardVariables);
// Build the label to expressions mapping.
modelComponents.labelToExpressionMap = buildLabelExpressions(model, variables, options);
// Finally, create the model.
return createModel(model.getModelType(), variables, modelComponents);
}

20
src/builder/DdJaniModelBuilder.h

@ -25,7 +25,7 @@ namespace storm {
/*!
* Creates an object representing the default building options.
*/
Options();
Options(bool buildAllLabels = false, bool buildAllRewardModels = false);
/*! Creates an object representing the suggested building options assuming that the given formula is the
* only one to check. Additional formulas may be preserved by calling <code>preserveFormula</code>.
@ -63,7 +63,23 @@ namespace storm {
* Retrieves the names of the reward models to build.
*/
std::set<std::string> const& getRewardModelNames() const;
/*!
* Adds the given label to the ones that are supposed to be built.
*/
void addLabel(std::string const& labelName);
/*!
* Retrieves whether the flag to build all labels is set.
*/
bool isBuildAllLabelsSet() const;
/// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored.
bool buildAllLabels;
/// A set of labels to build.
std::set<std::string> labelNames;
/*!
* Retrieves whether the flag to build all reward models is set.
*/
@ -98,4 +114,4 @@ namespace storm {
};
}
}
}

48
src/builder/JaniProgramGraphBuilder.cpp

@ -1,16 +1,62 @@
#include "JaniProgramGraphBuilder.h"
#include "src/storage/jani/EdgeDestination.h"
namespace storm {
namespace builder {
unsigned JaniProgramGraphBuilder::janiVersion = 1;
void JaniProgramGraphBuilder::addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton) {
for (auto const& v : programGraph.getVariables()) {
if (isConstant(v.first)) {
storm::jani::Constant constant(v.second.getName(), v.second, programGraph.getInitialValue(v.first));
model.addConstant(constant);
} else if (v.second.hasBooleanType()) {
storm::jani::BooleanVariable* janiVar = new storm::jani::BooleanVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), false);
automaton.addVariable(*janiVar);
variables.emplace(v.first, janiVar);
} else if (isRestrictedVariable(v.first) && !isRewardVariable(v.first)) {
storm::storage::IntegerInterval const& bounds = variableBounds(v.first);
if (bounds.hasLeftBound()) {
if (bounds.hasRightBound()) {
storm::jani::BoundedIntegerVariable* janiVar = new storm::jani::BoundedIntegerVariable (v.second.getName(), v.second, programGraph.getInitialValue(v.first), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get()));
variables.emplace(v.first, janiVar);
automaton.addVariable(*janiVar);
} else {
// Not yet supported.
assert(false);
}
} else {
// Not yet supported.
assert(false);
}
} else {
storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), isRewardVariable(v.first));
if(isRewardVariable(v.first)) {
model.addVariable(*janiVar);
} else {
automaton.addVariable(*janiVar);
}
variables.emplace(v.first, janiVar);
}
}
}
storm::jani::OrderedAssignments JaniProgramGraphBuilder::buildOrderedAssignments(storm::jani::Automaton& automaton, storm::ppg::DeterministicProgramAction const& act) {
std::vector<storm::jani::Assignment> vec;
uint64_t level = 0;
for(auto const& group : act) {
for(auto const& assignment : group) {
vec.emplace_back(*(variables.at(assignment.first)), assignment.second, level);
if(isRewardVariable(assignment.first)) {
std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> eval;
eval.emplace((variables.at(assignment.first))->getExpressionVariable(), expManager->integer(0));
vec.emplace_back(*(variables.at(assignment.first)), assignment.second.substitute(eval).simplify(), level);
} else {
vec.emplace_back(*(variables.at(assignment.first)), assignment.second, level);
}
}
++level;
}

59
src/builder/JaniProgramGraphBuilder.h

@ -1,4 +1,5 @@
#include <string>
#include <unordered_map>
#include "src/storage/ppg/ProgramGraph.h"
#include "src/storage/jani/Model.h"
@ -45,6 +46,10 @@ namespace storm {
void restrictAllVariables(int64_t from, int64_t to) {
restrictAllVariables(storm::storage::IntegerInterval(from, to));
}
void restrictAllVariables(storm::storage::IntegerInterval const& restr) {
for (auto const& v : programGraph.getVariables()) {
if(isConstant(v.first)) {
continue;
@ -53,7 +58,7 @@ namespace storm {
continue; // Currently we ignore user bounds if we have bounded integers;
}
if(v.second.hasIntegerType() ) {
userVariableRestrictions.emplace(v.first, storm::storage::IntegerInterval(from, to));
userVariableRestrictions.emplace(v.first, restr);
}
}
}
@ -63,7 +68,7 @@ namespace storm {
storm::jani::Model* model = new storm::jani::Model(name, storm::jani::ModelType::MDP, janiVersion, expManager);
storm::jani::Automaton mainAutomaton("main");
addProcedureVariables(*model, mainAutomaton);
janiLocId = addProcedureLocations(mainAutomaton);
janiLocId = addProcedureLocations(*model, mainAutomaton);
addVariableOoBLocations(mainAutomaton);
addEdges(mainAutomaton);
model->addAutomaton(mainAutomaton);
@ -117,47 +122,23 @@ namespace storm {
return std::find(constants.begin(), constants.end(), i) != constants.end();
}
void addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton) {
for (auto const& v : programGraph.getVariables()) {
if (isConstant(v.first)) {
storm::jani::Constant constant(v.second.getName(), v.second, programGraph.getInitialValue(v.first));
model.addConstant(constant);
} else if (v.second.hasBooleanType()) {
storm::jani::BooleanVariable* janiVar = new storm::jani::BooleanVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), false);
automaton.addVariable(*janiVar);
variables.emplace(v.first, janiVar);
} else if (isRestrictedVariable(v.first) && !isRewardVariable(v.first)) {
storm::storage::IntegerInterval const& bounds = variableBounds(v.first);
if (bounds.hasLeftBound()) {
if (bounds.hasRightBound()) {
storm::jani::BoundedIntegerVariable* janiVar = new storm::jani::BoundedIntegerVariable (v.second.getName(), v.second, programGraph.getInitialValue(v.first), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get()));
variables.emplace(v.first, janiVar);
automaton.addVariable(*janiVar);
} else {
// Not yet supported.
assert(false);
}
} else {
// Not yet supported.
assert(false);
}
} else {
storm::jani::UnboundedIntegerVariable* janiVar = new storm::jani::UnboundedIntegerVariable(v.second.getName(), v.second, programGraph.getInitialValue(v.first), isRewardVariable(v.first));
if(isRewardVariable(v.first)) {
model.addVariable(*janiVar);
} else {
automaton.addVariable(*janiVar);
}
variables.emplace(v.first, janiVar);
}
}
}
void addProcedureVariables(storm::jani::Model& model, storm::jani::Automaton& automaton);
std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> addProcedureLocations(storm::jani::Automaton& automaton) {
std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> addProcedureLocations(storm::jani::Model& model, storm::jani::Automaton& automaton) {
std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> result;
std::map<std::string, storm::jani::BooleanVariable const*> labelVars;
std::set<std::string> labels = programGraph.getLabels();
for(auto const& label : labels) {
storm::jani::BooleanVariable janiVar(label, expManager->declareBooleanVariable(label), expManager->boolean(false), true);
labelVars.emplace(label, &model.addVariable(janiVar));
}
for (auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) {
storm::jani::Location janiLoc(janiLocationName(it->second.id()));
for(auto const& label : programGraph.getLabels(it->second.id())) {
assert(labelVars.count(label) > 0);
janiLoc.addTransientAssignment(storm::jani::Assignment(*(labelVars.at(label)), expManager->boolean(true)));
}
result[it->second.id()] = automaton.addLocation(janiLoc);
if (it->second.isInitial()) {
automaton.addInitialLocation(result[it->second.id()]);

24
src/cli/cli.cpp

@ -222,13 +222,23 @@ namespace storm {
model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first;
}
// Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
if (model.isJaniModel()) {
formulas = storm::parseFormulasForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel());
} else {
formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram());
}
}
if(model.isJaniModel() && storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) {
storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel());
normalisedModel.makeStandardJaniCompliant();
storm::jani::JsonExporter::toFile(normalisedModel, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
storm::jani::JsonExporter::toFile(normalisedModel, formulas, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
} else {
storm::jani::JsonExporter::toFile(model.asJaniModel(), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
storm::jani::JsonExporter::toFile(model.asJaniModel(), formulas, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
}
}
@ -236,15 +246,7 @@ namespace storm {
std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
model = model.preprocess(constantDefinitionString);
// Then proceed to parsing the properties (if given), since the model we are building may depend on the property.
std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) {
if (model.isJaniModel()) {
formulas = storm::parseFormulasForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel());
} else {
formulas = storm::parseFormulasForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram());
}
}
if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
#ifdef STORM_HAVE_CARL

14
src/generator/CompressedState.cpp

@ -10,6 +10,13 @@ namespace storm {
template<typename ValueType>
void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
for (auto const& locationVariable : variableInformation.locationVariables) {
if (locationVariable.bitWidth != 0) {
evaluator.setIntegerValue(locationVariable.variable, state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth));
} else {
evaluator.setIntegerValue(locationVariable.variable, 0);
}
}
for (auto const& booleanVariable : variableInformation.booleanVariables) {
evaluator.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
}
@ -20,6 +27,13 @@ namespace storm {
storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager) {
storm::expressions::SimpleValuation result(manager.getSharedPointer());
for (auto const& locationVariable : variableInformation.locationVariables) {
if (locationVariable.bitWidth != 0) {
result.setIntegerValue(locationVariable.variable, state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth));
} else {
result.setIntegerValue(locationVariable.variable, 0);
}
}
for (auto const& booleanVariable : variableInformation.booleanVariables) {
result.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
}

89
src/generator/JaniNextStateGenerator.cpp

@ -32,6 +32,9 @@ namespace storm {
this->checkValid();
this->variableInformation = VariableInformation(model);
// Create a proper evalator.
this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(model.getManager());
if (this->options.isBuildAllRewardModelsSet()) {
for (auto const& variable : model.getGlobalVariables()) {
if (variable.isTransient()) {
@ -46,14 +49,22 @@ namespace storm {
rewardVariables.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable());
} else {
STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
}
}
// If no reward model was yet added, but there was one that was given in the options, we try to build the
// standard reward model.
if (rewardVariables.empty() && !this->options.getRewardModelNames().empty()) {
rewardVariables.push_back(globalVariables.getTransientVariables().front()->getExpressionVariable());
bool foundTransientVariable = false;
for (auto const& transientVariable : globalVariables.getTransientVariables()) {
if (transientVariable->isUnboundedIntegerVariable() || transientVariable->isRealVariable()) {
rewardVariables.push_back(transientVariable->getExpressionVariable());
foundTransientVariable = true;
break;
}
}
STORM_LOG_ASSERT(foundTransientVariable, "Expected to find a fitting transient variable.");
}
}
@ -62,11 +73,28 @@ namespace storm {
// If there are terminal states we need to handle, we now need to translate all labels to expressions.
if (this->options.hasTerminalStates()) {
std::map<std::string, storm::expressions::Variable> locationVariables;
auto locationVariableIt = this->variableInformation.locationVariables.begin();
for (auto const& automaton : this->model.getAutomata()) {
locationVariables[automaton.getName()] = locationVariableIt->variable;
++locationVariableIt;
}
for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
if (expressionOrLabelAndBool.first.isExpression()) {
this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
} else {
STORM_LOG_THROW(expressionOrLabelAndBool.first.getLabel() == "init" || expressionOrLabelAndBool.first.getLabel() == "deadlock", storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
// If it's a label, i.e. refers to a transient boolean variable we need to derive the expression
// for the label so we can cut off the exploration there.
if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock") {
STORM_LOG_THROW(model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
storm::jani::Variable const& variable = model.getGlobalVariables().getVariable(expressionOrLabelAndBool.first.getLabel());
STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), locationVariables), expressionOrLabelAndBool.second));
}
}
}
}
@ -116,7 +144,11 @@ namespace storm {
auto resultIt = result.begin();
for (auto it = this->variableInformation.locationVariables.begin(), ite = this->variableInformation.locationVariables.end(); it != ite; ++it, ++resultIt) {
*resultIt = getLocation(state, *it);
if (it->bitWidth == 0) {
*resultIt = 0;
} else {
*resultIt = state.getAsInt(it->bitOffset, it->bitWidth);
}
}
return result;
@ -156,7 +188,7 @@ namespace storm {
blockingExpression = blockingExpression.isInitialized() ? blockingExpression || localBlockingExpression : localBlockingExpression;
initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound));
}
// Gather iterators to the initial locations of all the automata.
std::vector<std::set<uint64_t>::const_iterator> initialLocationsIterators;
uint64_t currentLocationVariable = 0;
@ -221,7 +253,7 @@ namespace storm {
while (assignmentIt->getExpressionVariable() != boolIt->variable) {
++boolIt;
}
newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getAssignedExpression()));
newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getAssignedExpression()));
}
// Iterate over all integer assignments and carry them out.
@ -230,7 +262,7 @@ namespace storm {
while (assignmentIt->getExpressionVariable() != integerIt->variable) {
++integerIt;
}
int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getAssignedExpression());
int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getAssignedExpression());
STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
@ -266,7 +298,7 @@ namespace storm {
// If a terminal expression was set and we must not expand this state, return now.
if (!this->terminalStates.empty()) {
for (auto const& expressionBool : this->terminalStates) {
if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) {
if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) {
return result;
}
}
@ -356,14 +388,14 @@ namespace storm {
}
// Skip the command, if it is not enabled.
if (!this->evaluator.asBool(edge.getGuard())) {
if (!this->evaluator->asBool(edge.getGuard())) {
continue;
}
// Determine the exit rate if it's a Markovian edge.
boost::optional<ValueType> exitRate = boost::none;
if (edge.hasRate()) {
exitRate = this->evaluator.asRational(edge.getRate());
exitRate = this->evaluator->asRational(edge.getRate());
}
result.push_back(Choice<ValueType>(edge.getActionIndex(), static_cast<bool>(exitRate)));
@ -377,7 +409,7 @@ namespace storm {
StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
// Update the choice by adding the probability/target state to it.
ValueType probability = this->evaluator.asRational(destination.getProbability());
ValueType probability = this->evaluator->asRational(destination.getProbability());
probability = exitRate ? exitRate.get() * probability : probability;
choice.addProbability(stateIndex, probability);
probabilitySum += probability;
@ -437,9 +469,9 @@ namespace storm {
// and otherwise insert it.
auto targetStateIt = newTargetStates->find(newTargetState);
if (targetStateIt != newTargetStates->end()) {
targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability());
targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
} else {
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability()));
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()));
}
}
@ -525,7 +557,7 @@ namespace storm {
std::vector<storm::jani::Edge const*> edgePointers;
for (auto const& edge : edges) {
if (this->evaluator.asBool(edge.getGuard())) {
if (this->evaluator->asBool(edge.getGuard())) {
edgePointers.push_back(&edge);
}
}
@ -574,7 +606,32 @@ namespace storm {
template<typename ValueType, typename StateType>
storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, {});
// Prepare a mapping from automata names to the location variables.
std::map<std::string, storm::expressions::Variable> locationVariables;
auto locationVariableIt = this->variableInformation.locationVariables.begin();
for (auto const& automaton : model.getAutomata()) {
locationVariables[automaton.getName()] = locationVariableIt->variable;
++locationVariableIt;
}
// As in JANI we can use transient boolean variable assignments in locations to identify states, we need to
// create a list of boolean transient variables and the expressions that define them.
std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> transientVariableToExpressionMap;
for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
if (variable->isBooleanVariable()) {
if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable->getName()) != this->options.getLabelNames().end()) {
transientVariableToExpressionMap[variable->getExpressionVariable()] = model.getLabelExpression(variable->asBooleanVariable(), locationVariables);
}
}
}
std::vector<std::pair<std::string, storm::expressions::Expression>> transientVariableExpressions;
for (auto const& element : transientVariableToExpressionMap) {
transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second));
}
return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, transientVariableExpressions);
}
template<typename ValueType, typename StateType>
@ -595,7 +652,7 @@ namespace storm {
if (rewardVariableIt == rewardVariableIte) {
break;
} else if (*rewardVariableIt == assignment.getExpressionVariable()) {
callback(ValueType(this->evaluator.asRational(assignment.getAssignedExpression())));
callback(ValueType(this->evaluator->asRational(assignment.getAssignedExpression())));
++rewardVariableIt;
}
}

2
src/generator/JaniNextStateGenerator.h

@ -105,7 +105,7 @@ namespace storm {
* Checks the underlying model for validity for this next-state generator.
*/
void checkValid() const;
/// The model used for the generation of next states.
storm::jani::Model model;

12
src/generator/NextStateGenerator.cpp

@ -224,12 +224,12 @@ namespace storm {
}
template<typename ValueType, typename StateType>
NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(expressionManager), state(nullptr) {
NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(nullptr), state(nullptr) {
// Intentionally left empty.
}
template<typename ValueType, typename StateType>
NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(expressionManager), state(nullptr) {
NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(nullptr), state(nullptr) {
// Intentionally left empty.
}
@ -246,7 +246,7 @@ namespace storm {
template<typename ValueType, typename StateType>
void NextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
// Since almost all subsequent operations are based on the evaluator, we load the state into it now.
unpackStateIntoEvaluator(state, variableInformation, evaluator);
unpackStateIntoEvaluator(state, variableInformation, *evaluator);
// Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
this->state = &state;
@ -257,7 +257,7 @@ namespace storm {
if (expression.isTrue()) {
return true;
}
return evaluator.asBool(expression);
return evaluator->asBool(expression);
}
template<typename ValueType, typename StateType>
@ -282,11 +282,11 @@ namespace storm {
result.addLabel(label.first);
}
for (auto const& stateIndexPair : states) {
unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, this->evaluator);
unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator);
for (auto const& label : labelsAndExpressions) {
// Add label to state, if the corresponding expression is true.
if (evaluator.asBool(label.second)) {
if (evaluator->asBool(label.second)) {
result.addLabelToState(label.first, stateIndexPair.second);
}
}

2
src/generator/NextStateGenerator.h

@ -211,7 +211,7 @@ namespace storm {
VariableInformation variableInformation;
/// An evaluator used to evaluate expressions.
storm::expressions::ExpressionEvaluator<ValueType> evaluator;
std::unique_ptr<storm::expressions::ExpressionEvaluator<ValueType>> evaluator;
/// The currently loaded state.
CompressedState const* state;

35
src/generator/PrismNextStateGenerator.cpp

@ -30,6 +30,9 @@ namespace storm {
this->checkValid();
this->variableInformation = VariableInformation(program);
// Create a proper evalator.
this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(program.getManager());
if (this->options.isBuildAllRewardModelsSet()) {
for (auto const& rewardModel : this->program.getRewardModels()) {
rewardModels.push_back(rewardModel);
@ -186,8 +189,8 @@ namespace storm {
ValueType stateRewardValue = storm::utility::zero<ValueType>();
if (rewardModel.get().hasStateRewards()) {
for (auto const& stateReward : rewardModel.get().getStateRewards()) {
if (this->evaluator.asBool(stateReward.getStatePredicateExpression())) {
stateRewardValue += ValueType(this->evaluator.asRational(stateReward.getRewardValueExpression()));
if (this->evaluator->asBool(stateReward.getStatePredicateExpression())) {
stateRewardValue += ValueType(this->evaluator->asRational(stateReward.getRewardValueExpression()));
}
}
}
@ -197,7 +200,7 @@ namespace storm {
// If a terminal expression was set and we must not expand this state, return now.
if (!this->terminalStates.empty()) {
for (auto const& expressionBool : this->terminalStates) {
if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) {
if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) {
return result;
}
}
@ -252,8 +255,8 @@ namespace storm {
if (rewardModel.get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
for (auto const& choice : allChoices) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
}
}
@ -295,7 +298,7 @@ namespace storm {
while (assignmentIt->getVariable() != boolIt->variable) {
++boolIt;
}
newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getExpression()));
newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getExpression()));
}
// Iterate over all integer assignments and carry them out.
@ -304,7 +307,7 @@ namespace storm {
while (assignmentIt->getVariable() != integerIt->variable) {
++integerIt;
}
int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getExpression());
int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getExpression());
STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
@ -343,7 +346,7 @@ namespace storm {
// Look up commands by their indices and add them if the guard evaluates to true in the given state.
for (uint_fast64_t commandIndex : commandIndices) {
storm::prism::Command const& command = module.getCommand(commandIndex);
if (this->evaluator.asBool(command.getGuardExpression())) {
if (this->evaluator->asBool(command.getGuardExpression())) {
commands.push_back(command);
}
}
@ -376,7 +379,7 @@ namespace storm {
if (command.isLabeled()) continue;
// Skip the command, if it is not enabled.
if (!this->evaluator.asBool(command.getGuardExpression())) {
if (!this->evaluator->asBool(command.getGuardExpression())) {
continue;
}
@ -398,7 +401,7 @@ namespace storm {
StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
// Update the choice by adding the probability/target state to it.
ValueType probability = this->evaluator.asRational(update.getLikelihoodExpression());
ValueType probability = this->evaluator->asRational(update.getLikelihoodExpression());
choice.addProbability(stateIndex, probability);
probabilitySum += probability;
}
@ -408,8 +411,8 @@ namespace storm {
ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
if (rewardModel.get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression()));
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression()));
}
}
}
@ -462,9 +465,9 @@ namespace storm {
// and otherwise insert it.
auto targetStateIt = newTargetStates->find(newTargetState);
if (targetStateIt != newTargetStates->end()) {
targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression());
targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression());
} else {
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression()));
newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression()));
}
}
}
@ -509,8 +512,8 @@ namespace storm {
ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
if (rewardModel.get().hasStateActionRewards()) {
for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression()));
if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) {
stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression()));
}
}
}

41
src/generator/VariableInformation.cpp

@ -2,6 +2,7 @@
#include "src/storage/prism/Program.h"
#include "src/storage/jani/Model.h"
#include "src/storage/expressions/ExpressionManager.h"
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
@ -19,7 +20,7 @@ namespace storm {
// Intentionally left empty.
}
LocationVariableInformation::LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) {
LocationVariableInformation::LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) {
// Intentionally left empty.
}
@ -62,31 +63,39 @@ namespace storm {
}
for (auto const& variable : model.getGlobalVariables().getBooleanVariables()) {
booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true);
++totalBitOffset;
if (!variable.isTransient()) {
booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset, true);
++totalBitOffset;
}
}
for (auto const& variable : model.getGlobalVariables().getBoundedIntegerVariables()) {
int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true);
totalBitOffset += bitwidth;
if (!variable.isTransient()) {
int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth, true);
totalBitOffset += bitwidth;
}
}
for (auto const& automaton : model.getAutomata()) {
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
locationVariables.emplace_back(automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
locationVariables.emplace_back(model.getManager().declareFreshIntegerVariable(false, "loc"), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
totalBitOffset += bitwidth;
for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
++totalBitOffset;
if (!variable.isTransient()) {
booleanVariables.emplace_back(variable.getExpressionVariable(), totalBitOffset);
++totalBitOffset;
}
}
for (auto const& variable : automaton.getVariables().getBoundedIntegerVariables()) {
int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
totalBitOffset += bitwidth;
if (!variable.isTransient()) {
int_fast64_t lowerBound = variable.getLowerBound().evaluateAsInt();
int_fast64_t upperBound = variable.getUpperBound().evaluateAsInt();
uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(upperBound - lowerBound + 1)));
integerVariables.emplace_back(variable.getExpressionVariable(), lowerBound, upperBound, totalBitOffset, bitwidth);
totalBitOffset += bitwidth;
}
}
}

7
src/generator/VariableInformation.h

@ -56,7 +56,10 @@ namespace storm {
// A structure storing information about the location variables of the model.
struct LocationVariableInformation {
LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
// The expression variable for this location.
storm::expressions::Variable variable;
// The highest possible location value.
uint64_t highestValue;
@ -98,4 +101,4 @@ namespace storm {
}
}
#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */
#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */

84
src/parser/JaniParser.cpp

@ -110,6 +110,13 @@ namespace storm {
for (auto const& automataEntry : parsedStructure.at("automata")) {
model.addAutomaton(parseAutomaton(automataEntry, model));
}
STORM_LOG_THROW(parsedStructure.count("restrict-initial") < 2, storm::exceptions::InvalidJaniException, "Model has multiple initial value restrictions");
storm::expressions::Expression initialValueRestriction = expressionManager->boolean(true);
if(parsedStructure.count("restrict-initial") > 0) {
STORM_LOG_THROW(parsedStructure.at("restrict-initial").count("exp") == 1, storm::exceptions::InvalidJaniException, "Model needs an expression inside the initial restricion");
initialValueRestriction = parseExpression(parsedStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name);
}
model.setInitialStatesRestriction(initialValueRestriction);
STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given");
std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system"));
model.setSystemComposition(composition);
@ -586,13 +593,15 @@ namespace storm {
STORM_LOG_THROW(locEntry.count("invariant") == 0, storm::exceptions::InvalidJaniException, "Invariants in locations as in '" + locName + "' in automaton '" + name + "' are not supported");
//STORM_LOG_THROW(locEntry.count("invariant") > 0 && !supportsInvariants(parentModel.getModelType()), storm::exceptions::InvalidJaniException, "Invariants are not supported in the model type " + to_string(parentModel.getModelType()));
std::vector<storm::jani::Assignment> transientAssignments;
for(auto const& transientValueEntry : locEntry.at("transient-values")) {
STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to");
STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value");
storm::jani::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')");
STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
transientAssignments.emplace_back(lhs, rhs);
if(locEntry.count("transient-values") > 0) {
for(auto const& transientValueEntry : locEntry.at("transient-values")) {
STORM_LOG_THROW(transientValueEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one ref that is assigned to");
STORM_LOG_THROW(transientValueEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Transient values in location " << locName << " need exactly one assigned value");
storm::jani::Variable const& lhs = getLValue(transientValueEntry.at("ref"), parentModel.getGlobalVariables(), automaton.getVariables(), "LHS of assignment in location " + locName + " (automaton '" + name + "')");
STORM_LOG_THROW(lhs.isTransient(), storm::exceptions::InvalidJaniException, "Assigned non-transient variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
storm::expressions::Expression rhs = parseExpression(transientValueEntry.at("value"), "Assignment of variable " + lhs.getName() + " in location " + locName + " (automaton: '" + name + "')");
transientAssignments.emplace_back(lhs, rhs);
}
}
uint64_t id = automaton.addLocation(storm::jani::Location(locName, transientAssignments));
locIds.emplace(locName, id);
@ -639,7 +648,8 @@ namespace storm {
STORM_LOG_THROW(edgeEntry.count("rate") < 2, storm::exceptions::InvalidJaniException, "Edge from '" << sourceLoc << "' in automaton '" << name << "' has multiple rates");
storm::expressions::Expression rateExpr;
if(edgeEntry.count("rate") > 0) {
rateExpr = parseExpression(edgeEntry.at("rate"), "rate expression in edge from '" + sourceLoc + "' in automaton '" + name + "'");
STORM_LOG_THROW(edgeEntry.at("rate").count("exp") == 1, storm::exceptions::InvalidJaniException, "Rate in edge from '" << sourceLoc << "' in automaton '" << name << "' must have a defing expression.");
rateExpr = parseExpression(edgeEntry.at("rate").at("exp"), "rate expression in edge from '" + sourceLoc + "' in automaton '" + name + "'");
STORM_LOG_THROW(rateExpr.hasNumericalType(), storm::exceptions::InvalidJaniException, "Rate '" << rateExpr << "' has not a numerical type");
}
// guard
@ -694,24 +704,42 @@ namespace storm {
return automaton;
}
std::vector<storm::jani::SynchronizationVector> parseSyncVectors(json const& syncVectorStructure) {
std::vector<storm::jani::SynchronizationVector> syncVectors;
// TODO add error checks
for (auto const& syncEntry : syncVectorStructure) {
std::vector<std::string> inputs;
for (auto const& syncInput : syncEntry.at("synchronise")) {
if(syncInput.is_null()) {
// TODO handle null;
} else {
inputs.push_back(syncInput);
}
}
std::string syncResult = syncEntry.at("result");
syncVectors.emplace_back(inputs, syncResult);
}
return syncVectors;
}
std::shared_ptr<storm::jani::Composition> JaniParser::parseComposition(json const &compositionStructure) {
if(compositionStructure.count("automaton")) {
return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(compositionStructure.at("automaton").get<std::string>()));
}
STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given");
STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given, got " << compositionStructure.dump());
if (compositionStructure.at("elements").size() == 1) {
if (compositionStructure.count("syncs") == 0) {
// We might have an automaton.
STORM_LOG_THROW(compositionStructure.at("elements").back().count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in composition");
if (compositionStructure.at("elements").back().at("automaton").is_string()) {
std::string name = compositionStructure.at("elements").back().at("automaton");
// TODO check whether name exist?
return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(name));
}
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Nesting parallel composition is not supported");
} else {
// Might be rename or input-enable.
if (compositionStructure.at("elements").size() == 1 && compositionStructure.count("syncs") == 0) {
// We might have an automaton.
STORM_LOG_THROW(compositionStructure.at("elements").back().count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in composition");
if (compositionStructure.at("elements").back().at("automaton").is_string()) {
std::string name = compositionStructure.at("elements").back().at("automaton");
// TODO check whether name exist?
return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(name));
}
STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Trivial nesting parallel composition is not yet supported");
}
std::vector<std::shared_ptr<storm::jani::Composition>> compositions;
@ -725,19 +753,7 @@ namespace storm {
STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once");
std::vector<storm::jani::SynchronizationVector> syncVectors;
if (compositionStructure.count("syncs") > 0) {
// TODO add error checks
for (auto const& syncEntry : compositionStructure.at("syncs")) {
std::vector<std::string> inputs;
for (auto const& syncInput : syncEntry.at("synchronise")) {
if(syncInput.is_null()) {
// TODO handle null;
} else {
inputs.push_back(syncInput);
}
}
std::string syncResult = syncEntry.at("result");
syncVectors.emplace_back(inputs, syncResult);
}
syncVectors = parseSyncVectors(compositionStructure.at("syncs"));
}
return std::shared_ptr<storm::jani::Composition>(new storm::jani::ParallelComposition(compositions, syncVectors));

2
src/settings/modules/PGCLSettings.cpp

@ -28,7 +28,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, pgclFileOptionName, false, "Parses the pgcl program.").setShortName(pgclFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, pgclToJaniOptionName, false, "Transform to JANI.").setShortName(pgclToJaniOptionShortName).build());
this->addOption(storm::settings::OptionBuilder(moduleName, programGraphToDotOptionName, false, "Destination for the program graph dot output.").setShortName(programGraphToDotShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("descriptio", "description of the variable restrictions").build()).build());
this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("description", "description of the variable restrictions").build()).build());
}
bool PGCLSettings::isPgclFileSet() const {

2
src/storage/BitVector.h

@ -472,7 +472,7 @@ namespace storm {
* value is equal to a call to size(), then there is no bit set after the specified position.
*
* @param startingIndex The index at which to start the search for the next bit that is set. The
* bit at this index itself is already considered.
* bit at this index itself is included in the search range.
* @return The index of the next bit that is set after the given index.
*/
uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const;

28
src/storage/IntegerInterval.cpp

@ -1,2 +1,30 @@
#include "IntegerInterval.h"
#include <iostream>
#include <string>
#include "src/utility/macros.h"
#include "src/exceptions/InvalidArgumentException.h"
bool starts_with(const std::string& s1, const std::string& s2) {
return s2.size() <= s1.size() && s1.compare(0, s2.size(), s2) == 0;
}
namespace storm {
namespace storage {
IntegerInterval parseIntegerInterval(std::string const& stringRepr) {
if(starts_with(stringRepr, "[") && stringRepr.at(stringRepr.size()-1) == ']') {
auto split = stringRepr.find(",");
std::string first = stringRepr.substr(1,split-1);
std::string second = stringRepr.substr(split+1, stringRepr.size() - split - 2);
return IntegerInterval(stoi(first), stoi(second));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot parse " << stringRepr << " as integer interval");
}
}
}
}

1
src/storage/IntegerInterval.h

@ -95,5 +95,6 @@ namespace storm {
};
std::ostream& operator<<(std::ostream& os, IntegerInterval const& i);
IntegerInterval parseIntegerInterval(std::string const& stringRepr);
}
}

343
src/storage/jani/JSONExporter.cpp

@ -6,8 +6,10 @@
#include "src/utility/macros.h"
#include "src/exceptions/FileIoException.h"
#include "src/exceptions/NotSupportedException.h"
#include "src/exceptions/InvalidJaniException.h"
#include "src/exceptions/NotImplementedException.h"
#include "src/storage/expressions/RationalLiteralExpression.h"
#include "src/storage/expressions/IntegerLiteralExpression.h"
@ -20,8 +22,11 @@
#include "src/storage/expressions/BinaryRelationExpression.h"
#include "src/storage/expressions/VariableExpression.h"
#include "src/logic/Formulas.h"
#include "src/storage/jani/AutomatonComposition.h"
#include "src/storage/jani/ParallelComposition.h"
#include "src/storage/jani/Property.h"
namespace storm {
namespace jani {
@ -85,6 +90,289 @@ namespace storm {
bool allowRecursion;
};
std::string comparisonTypeToJani(storm::logic::ComparisonType ct) {
switch(ct) {
case storm::logic::ComparisonType::Less:
return "<";
case storm::logic::ComparisonType::LessEqual:
return "";
case storm::logic::ComparisonType::Greater:
return ">";
case storm::logic::ComparisonType::GreaterEqual:
return "";
}
}
modernjson::json numberToJson(storm::RationalNumber rn) {
modernjson::json numDecl;
if(carl::isOne(carl::getDenom(rn))) {
numDecl = modernjson::json(carl::toString(carl::getNum(rn)));
} else {
numDecl["op"] = "/";
numDecl["left"] = carl::toString(carl::getNum(rn));
numDecl["right"] = carl::toString(carl::getDenom(rn));
}
return numDecl;
}
modernjson::json constructPropertyInterval(uint64_t lower, uint64_t upper) {
modernjson::json iDecl;
iDecl["lower"] = lower;
iDecl["upper"] = upper;
return iDecl;
}
modernjson::json constructPropertyInterval(double lower, double upper) {
modernjson::json iDecl;
iDecl["lower"] = lower;
iDecl["upper"] = upper;
return iDecl;
}
modernjson::json FormulaToJaniJson::translate(storm::logic::Formula const& formula, bool continuousTime) {
FormulaToJaniJson translator(continuousTime);
return boost::any_cast<modernjson::json>(formula.accept(translator));
}
boost::any FormulaToJaniJson::visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const {
return ExpressionToJson::translate(f.getExpression());
}
boost::any FormulaToJaniJson::visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const {
modernjson::json opDecl(f.isTrueFormula() ? "true" : "false");
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const{
modernjson::json opDecl;
storm::logic::BinaryBooleanStateFormula::OperatorType op = f.getOperator();
opDecl["op"] = op == storm::logic::BinaryBooleanStateFormula::OperatorType::And ? "" : "";
opDecl["left"] = boost::any_cast<modernjson::json>(f.getLeftSubformula().accept(*this, boost::none));
opDecl["right"] = boost::any_cast<modernjson::json>(f.getRightSubformula().accept(*this, boost::none));
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const {
modernjson::json opDecl(f.isTrueFormula() ? "true" : "false");
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
opDecl["op"] = "U";
opDecl["left"] = boost::any_cast<modernjson::json>(f.getLeftSubformula().accept(*this, boost::none));
opDecl["right"] = boost::any_cast<modernjson::json>(f.getRightSubformula().accept(*this, boost::none));
if(f.hasDiscreteTimeBound()) {
opDecl["step-bounds"] = constructPropertyInterval(0, f.getDiscreteTimeBound());
} else {
opDecl["time-bounds"] = constructPropertyInterval(f.getIntervalBounds().first, f.getIntervalBounds().second);
}
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const {
STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support conditional formulae");
}
boost::any FormulaToJaniJson::visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const {
}
boost::any FormulaToJaniJson::visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
opDecl["op"] = "U";
opDecl["left"] = boost::any_cast<modernjson::json>(f.getTrueFormula()->accept(*this, boost::none));
opDecl["right"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
std::vector<std::string> tvec;
tvec.push_back("time");
if(f.hasBound()) {
auto bound = f.getBound();
opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
if(f.hasOptimalityType()) {
opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
} else {
opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin";
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
}
opDecl["left"]["exp"] = modernjson::json(1);
opDecl["left"]["accumulate"] = modernjson::json(tvec);
opDecl["right"] = numberToJson(bound.threshold);
} else {
if(f.hasOptimalityType()) {
opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
} else {
// TODO add checks
opDecl["op"] = "Pmin";
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
}
opDecl["exp"] = modernjson::json(1);
opDecl["accumulate"] = modernjson::json(tvec);
}
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::GloballyFormula const& f, boost::any const& data) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of a globally formulae");
}
boost::any FormulaToJaniJson::visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const {
STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an instanteneous reward formula");
}
boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
if(f.hasBound()) {
auto bound = f.getBound();
opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
if(f.hasOptimalityType()) {
opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax";
opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
} else {
opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin";
opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
}
opDecl["right"] = numberToJson(bound.threshold);
} else {
if(f.hasOptimalityType()) {
opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax";
opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
} else {
// TODO add checks
opDecl["op"] = "Pmin";
opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
}
}
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const {
// modernjson::json opDecl;
// if(f.()) {
// auto bound = f.getBound();
// opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
// if(f.hasOptimalityType()) {
// opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax";
// opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
// } else {
// opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin";
// opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
// }
// opDecl["right"] = numberToJson(bound.threshold);
// } else {
// if(f.hasOptimalityType()) {
// opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax";
// opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
//
// } else {
// // TODO add checks
// opDecl["op"] = "Pmin";
// opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
// }
// }
// return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::NextFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
opDecl["op"] = "U";
opDecl["left"] = boost::any_cast<modernjson::json>(f.getTrueFormula()->accept(*this, boost::none));
opDecl["right"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
opDecl["step-bounds"] = constructPropertyInterval((uint64_t)1, (uint64_t)1);
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
if(f.hasBound()) {
auto bound = f.getBound();
opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
if(f.hasOptimalityType()) {
opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax";
opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
} else {
opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Pmax" : "Pmin";
opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
}
opDecl["right"] = numberToJson(bound.threshold);
} else {
if(f.hasOptimalityType()) {
opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax";
opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
} else {
// TODO add checks
opDecl["op"] = "Pmin";
opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
}
}
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
std::vector<std::string> accvec;
if(continuous) {
accvec.push_back("time");
} else {
accvec.push_back("steps");
}
if(f.hasBound()) {
auto bound = f.getBound();
opDecl["op"] = comparisonTypeToJani(bound.comparisonType);
if(f.hasOptimalityType()) {
opDecl["left"]["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
} else {
opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Emax" : "Emin";
opDecl["left"]["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
}
opDecl["left"]["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT";
opDecl["left"]["accumulate"] = modernjson::json(accvec);
opDecl["right"] = numberToJson(bound.threshold);
} else {
if(f.hasOptimalityType()) {
opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
} else {
// TODO add checks
opDecl["op"] = "Pmin";
opDecl["reach"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
}
opDecl["exp"] = f.hasRewardModelName() ? f.getRewardModelName() : "DEFAULT";
opDecl["accumulate"] = modernjson::json(accvec);
}
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
storm::logic::UnaryBooleanStateFormula::OperatorType op = f.getOperator();
assert(op == storm::logic::UnaryBooleanStateFormula::OperatorType::Not);
opDecl["op"] = "¬";
opDecl["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
return opDecl;
}
boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const {
modernjson::json opDecl;
opDecl["op"] = "U";
opDecl["left"] = boost::any_cast<modernjson::json>(f.getLeftSubformula().accept(*this, boost::none));
opDecl["right"] = boost::any_cast<modernjson::json>(f.getRightSubformula().accept(*this, boost::none));
return opDecl;
}
std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) {
@ -205,22 +493,23 @@ namespace storm {
void JsonExporter::toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid) {
void JsonExporter::toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid) {
std::ofstream ofs;
ofs.open (filepath, std::ofstream::out );
if(ofs.is_open()) {
toStream(janiModel, ofs, checkValid);
toStream(janiModel, formulas, ofs, checkValid);
} else {
STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath);
}
}
void JsonExporter::toStream(storm::jani::Model const& janiModel, std::ostream& os, bool checkValid) {
void JsonExporter::toStream(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& os, bool checkValid) {
if(checkValid) {
janiModel.checkValid();
}
JsonExporter exporter;
exporter.convertModel(janiModel);
exporter.convertProperties(formulas, !janiModel.isDiscreteTimeModel());
os << exporter.finalize().dump(4) << std::endl;
}
@ -400,6 +689,54 @@ namespace storm {
}
std::string janiFilterTypeString(storm::jani::FilterType const& ft) {
switch(ft) {
case storm::jani::FilterType::MIN:
return "min";
case storm::jani::FilterType::MAX:
return "max";
case storm::jani::FilterType::SUM:
return "sum";
case storm::jani::FilterType::AVG:
return "avg";
case storm::jani::FilterType::COUNT:
return "count";
case storm::jani::FilterType::EXISTS:
return "";
case storm::jani::FilterType::FORALL:
return "";
case storm::jani::FilterType::ARGMIN:
return "argmin";
case storm::jani::FilterType::ARGMAX:
return "argmax";
case storm::jani::FilterType::VALUES:
return "values";
}
}
modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) {
modernjson::json propDecl;
propDecl["states"] = "initial";
propDecl["fun"] = janiFilterTypeString(fe.getFilterType());
propDecl["values"] = FormulaToJaniJson::translate(*fe.getFormula(), continuousModel);
return propDecl;
}
void JsonExporter::convertProperties( std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool continuousModel) {
std::vector<modernjson::json> properties;
uint64_t index = 0;
for(auto const& f : formulas) {
modernjson::json propDecl;
propDecl["name"] = "prop" + std::to_string(index);
propDecl["expression"] = convertFilterExpression(storm::jani::FilterExpression(f), continuousModel);
++index;
properties.push_back(propDecl);
}
jsonStruct["properties"] = properties;
}
}
}

34
src/storage/jani/JSONExporter.h

@ -2,6 +2,7 @@
#include "src/storage/expressions/ExpressionVisitor.h"
#include "src/logic/FormulaVisitor.h"
#include "Model.h"
// JSON parser
#include "json.hpp"
@ -28,15 +29,44 @@ namespace storm {
};
class FormulaToJaniJson : public storm::logic::FormulaVisitor {
public:
static modernjson::json translate(storm::logic::Formula const& formula, bool continuousTime);
virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::ConditionalFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::CumulativeRewardFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::EventuallyFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::TimeOperatorFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::GloballyFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::InstantaneousRewardFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::LongRunAverageOperatorFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::LongRunAverageRewardFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::NextFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::ProbabilityOperatorFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const;
virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const;
private:
FormulaToJaniJson(bool continuousModel) : continuous(continuousModel) { }
bool continuous;
};
class JsonExporter {
JsonExporter() = default;
public:
static void toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid = true);
static void toStream(storm::jani::Model const& janiModel, std::ostream& ostream, bool checkValid = false);
static void toFile(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::string const& filepath, bool checkValid = true);
static void toStream(storm::jani::Model const& janiModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, std::ostream& ostream, bool checkValid = false);
private:
void convertModel(storm::jani::Model const& model);
void convertProperties(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool timeContinuousModel);
void appendVariableDeclaration(storm::jani::Variable const& variable);
modernjson::json finalize() {

33
src/storage/jani/Model.cpp

@ -7,6 +7,7 @@
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidOperationException.h"
#include "src/exceptions/InvalidTypeException.h"
@ -456,7 +457,39 @@ namespace storm {
STORM_LOG_ASSERT(getModelType() != storm::jani::ModelType::UNDEFINED, "Model type not set");
STORM_LOG_ASSERT(!automata.empty(), "No automata set");
STORM_LOG_ASSERT(composition != nullptr, "Composition is not set");
}
storm::expressions::Expression Model::getLabelExpression(BooleanVariable const& transientVariable, std::map<std::string, storm::expressions::Variable> const& automatonToLocationVariableMap) const {
STORM_LOG_THROW(transientVariable.isTransient(), storm::exceptions::InvalidArgumentException, "Expected transient variable.");
storm::expressions::Expression result;
bool negate = transientVariable.getInitExpression().isTrue();
for (auto const& automaton : this->getAutomata()) {
storm::expressions::Variable const& locationVariable = automatonToLocationVariableMap.at(automaton.getName());
for (auto const& location : automaton.getLocations()) {
for (auto const& assignment : location.getAssignments().getTransientAssignments()) {
if (assignment.getExpressionVariable() == transientVariable.getExpressionVariable()) {
auto newExpression = (locationVariable == this->getManager().integer(automaton.getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression());
if (result.isInitialized()) {
result = result || newExpression;
} else {
result = newExpression;
}
}
}
}
}
if (result.isInitialized()) {
if (negate) {
result = !result;
}
} else {
result = this->getManager().boolean(negate);
}
return result;
}
bool Model::hasStandardComposition() const {

6
src/storage/jani/Model.h

@ -326,6 +326,12 @@ namespace storm {
*/
void checkValid() const;
/*!
* Creates the expression that characterizes all states in which the provided transient boolean variable is
* true. The provided location variables are used to encode the location of the automata.
*/
storm::expressions::Expression getLabelExpression(BooleanVariable const& transientVariable, std::map<std::string, storm::expressions::Variable> const& automatonToLocationVariableMap) const;
/*!
* Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.
* That is, undefined constants may only appear in the probability expressions of edge destinations as well

9
src/storage/jani/Property.cpp

@ -1,8 +1,8 @@
#include "Property.h"
namespace storm {
namespace jani {
Property::Property(std::string const& name, std::shared_ptr<const storm::logic::Formula> const& formula, std::string const& comment)
: name(name), formula(formula), comment(comment)
Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment)
: name(name), filterExpression(FilterExpression(formula)), comment(comment)
{
}
@ -14,10 +14,7 @@ namespace storm {
std::string const& Property::getComment() const {
return this->comment;
}
std::shared_ptr<storm::logic::Formula const> const& Property::getFormula() const {
return this->formula;
}
}
}

39
src/storage/jani/Property.h

@ -1,9 +1,35 @@
#pragma once
#include "src/logic/formulas.h"
#include "src/logic/Formulas.h"
namespace storm {
namespace jani {
enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES };
class FilterExpression {
public:
explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula) : values(formula) {}
std::shared_ptr<storm::logic::Formula const> const& getFormula() const {
return values;
}
FilterType getFilterType() const {
return ft;
}
private:
// For now, we assume that the states are always the initial states.
std::shared_ptr<storm::logic::Formula const> values;
FilterType ft = FilterType::VALUES;
};
class Property {
/**
* Constructs the property
@ -22,16 +48,13 @@ namespace storm {
* @return the comment
*/
std::string const& getComment() const;
/**
* Get the formula
* @return the formula
*/
std::shared_ptr<storm::logic::Formula const> const& getFormula() const;
private:
std::string name;
std::shared_ptr<storm::logic::Formula const> formula;
std::string comment;
FilterExpression filterExpression;
};
}
}

20
src/storage/jani/VariableSet.cpp

@ -176,6 +176,26 @@ namespace storm {
return result;
}
uint_fast64_t VariableSet::getNumberOfRealTransientVariables() const {
uint_fast64_t result = 0;
for (auto const& variable : variables) {
if (variable->isTransient() && variable->isRealVariable()) {
++result;
}
}
return result;
}
uint_fast64_t VariableSet::getNumberOfUnboundedIntegerTransientVariables() const {
uint_fast64_t result = 0;
for (auto const& variable : variables) {
if (variable->isTransient() && variable->isUnboundedIntegerVariable()) {
++result;
}
}
return result;
}
std::vector<std::shared_ptr<Variable const>> VariableSet::getTransientVariables() const {
std::vector<std::shared_ptr<Variable const>> result;
for (auto const& variable : variables) {

10
src/storage/jani/VariableSet.h

@ -173,6 +173,16 @@ namespace storm {
*/
uint_fast64_t getNumberOfTransientVariables() const;
/*!
* Retrieves the number of real transient variables in this variable set.
*/
uint_fast64_t getNumberOfRealTransientVariables() const;
/*!
* Retrieves the number of unbounded integer transient variables in this variable set.
*/
uint_fast64_t getNumberOfUnboundedIntegerTransientVariables() const;
/*!
* Retrieves a vector of transient variables in this variable set.
*/

28
src/storage/ppg/ProgramGraph.h

@ -49,10 +49,19 @@ namespace storm {
return &(probabilisticActions.emplace(newId, ProbabilisticProgramAction(this, newId, var, from, to)).first->second);
}
ProgramLocation* addLocation(bool isInitial = false, bool successfulTermination = false, bool aborted = false, std::vector<std::string> const& labels = {}) {
ProgramLocation* addLocation(bool isInitial = false, bool successfulTermination = false, bool observeViolated = false, bool aborted = false, std::vector<std::string> const& labels = {}) {
ProgramLocationIdentifier newId = freeLocationIndex();
assert(!hasLocation(newId));
locationLabels[newId] = labels;
if (successfulTermination) {
locationLabels[newId].push_back(succesfulTerminationLabel);
}
if (observeViolated) {
locationLabels[newId].push_back(observeViolatedLabel);
}
if (aborted) {
locationLabels[newId].push_back(abortLabel);
}
return &(locations.emplace(newId, ProgramLocation(this, newId, isInitial)).first->second);
}
@ -98,7 +107,19 @@ namespace storm {
return res;
}
std::set<std::string> getLabels() const {
std::set<std::string> result;
for(auto const& locEntry : locationLabels) {
for(auto const& label : locEntry.second) {
result.insert(label);
}
}
return result;
}
std::vector<std::string> getLabels(ProgramLocationIdentifier loc) const {
return locationLabels.at(loc);
}
bool hasLabel(ProgramLocationIdentifier loc, std::string const& label) const {
return std::find(locationLabels.at(loc).begin(), locationLabels.at(loc).end(), label) != locationLabels.at(loc).end();
@ -288,8 +309,9 @@ namespace storm {
ProgramEdgeIdentifier newEdgeId = 0;
ProgramActionIdentifier newActionId = 1;
ProgramActionIdentifier noActionId = 0;
std::string succesfulTerminationLabel = "__ret0__";
std::string abortLabel = "__ret1__";
std::string succesfulTerminationLabel = "_ret0_";
std::string abortLabel = "_ret1_";
std::string observeViolatedLabel = "_viol_";
};

2
src/storage/ppg/defines.h

@ -1,6 +1,8 @@
#pragma once
#include <cassert>
#include <vector>
#include <cstdint>
namespace storm {
namespace ppg {
class ProgramGraph;

4
src/storage/prism/Module.cpp

@ -196,12 +196,12 @@ namespace storm {
bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
for (auto const& booleanVariable : this->getBooleanVariables()) {
if (booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
if (booleanVariable.hasInitialValue() && booleanVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
}
for (auto const& integerVariable : this->getIntegerVariables()) {
if (integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
if (integerVariable.hasInitialValue() && integerVariable.getInitialValueExpression().containsVariable(undefinedConstantVariables)) {
return false;
}
if (integerVariable.getLowerBoundExpression().containsVariable(undefinedConstantVariables)) {

5
src/storm-pgcl.cpp

@ -77,6 +77,11 @@ int main(const int argc, const char** argv) {
}
if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isToJaniSet()) {
storm::builder::JaniProgramGraphBuilder builder(*progGraph);
if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isProgramVariableRestrictionSet()) {
// TODO More fine grained control
storm::storage::IntegerInterval restr = storm::storage::parseIntegerInterval(storm::settings::getModule<storm::settings::modules::PGCLSettings>().getProgramVariableRestrictions());
builder.restrictAllVariables(restr);
}
builder.restrictAllVariables(0, 120);
storm::jani::Model* model = builder.build();
delete progGraph;

Loading…
Cancel
Save