diff --git a/examples/pctmc/polling6.sm b/examples/pctmc/polling6.sm new file mode 100644 index 000000000..686907565 --- /dev/null +++ b/examples/pctmc/polling6.sm @@ -0,0 +1,87 @@ +// polling example [IT90] +// gxn/dxp 26/01/00 + +ctmc + +const int N=6; + +const double mu; +const double gamma; + +//const double mu= 1; +//const double gamma= 200; +//const double lambda= mu/N; + +module server + + s : [1..6]; // station + a : [0..1]; // action: 0=polling, 1=serving + + [loop1a] (s=1)&(a=0) -> gamma : (s'=s+1); + [loop1b] (s=1)&(a=0) -> gamma : (a'=1); + [serve1] (s=1)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop2a] (s=2)&(a=0) -> gamma : (s'=s+1); + [loop2b] (s=2)&(a=0) -> gamma : (a'=1); + [serve2] (s=2)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop3a] (s=3)&(a=0) -> gamma : (s'=s+1); + [loop3b] (s=3)&(a=0) -> gamma : (a'=1); + [serve3] (s=3)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop4a] (s=4)&(a=0) -> gamma : (s'=s+1); + [loop4b] (s=4)&(a=0) -> gamma : (a'=1); + [serve4] (s=4)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop5a] (s=5)&(a=0) -> gamma : (s'=s+1); + [loop5b] (s=5)&(a=0) -> gamma : (a'=1); + [serve5] (s=5)&(a=1) -> mu : (s'=s+1)&(a'=0); + + [loop6a] (s=6)&(a=0) -> gamma : (s'=1); + [loop6b] (s=6)&(a=0) -> gamma : (a'=1); + [serve6] (s=6)&(a=1) -> mu : (s'=1)&(a'=0); + +endmodule + +module station1 + + s1 : [0..1]; + + [loop1a] (s1=0) -> 1 : (s1'=0); + [] (s1=0) -> mu/N : (s1'=1); + [loop1b] (s1=1) -> 1 : (s1'=1); + [serve1] (s1=1) -> 1 : (s1'=0); + +endmodule + +// construct further stations through renaming +module station2 = station1 [s1=s2, loop1a=loop2a, loop1b=loop2b, serve1=serve2] endmodule +module station3 = station1 [s1=s3, loop1a=loop3a, loop1b=loop3b, serve1=serve3] endmodule +module station4 = station1 [s1=s4, loop1a=loop4a, loop1b=loop4b, serve1=serve4] endmodule +module station5 = station1 [s1=s5, loop1a=loop5a, loop1b=loop5b, serve1=serve5] endmodule +module station6 = station1 [s1=s6, loop1a=loop6a, loop1b=loop6b, serve1=serve6] endmodule + +// cumulative rewards + +rewards "waiting" // expected time the station 1 is waiting to be served + s1=1 & !(s=1 & a=1) : 1; +endrewards + +rewards "served" // expected number of times station1 is served + [serve1] true : 1; +endrewards + +label "server1serving" = s=1 & a=1; +label "server5polling" = s=5 & a=0; +label "server5serving" = s=5 & a=1; + +init +s = 1 & +a = 0 & +s1 = 0 & +s2 = 0 & +s3 = 0 & +s4 = 0 & +s5 = 0 & +s6 = 0 +endinit diff --git a/examples/pdtmc/brp/brp.pm b/examples/pdtmc/brp/brp.pm index 897f9909e..031bfe978 100644 --- a/examples/pdtmc/brp/brp.pm +++ b/examples/pdtmc/brp/brp.pm @@ -133,3 +133,6 @@ module channelL [TO_Ack] (l=2) -> (l'=0); endmodule + +label "fatal" = s=5 & T; +label "false_neg" = srep=1 & rrep=3 & recv; diff --git a/examples/pdtmc/brp/brp16_2.pm b/examples/pdtmc/brp/brp16_2.pm index 2e20b7de4..0fc99d05e 100644 --- a/examples/pdtmc/brp/brp16_2.pm +++ b/examples/pdtmc/brp/brp16_2.pm @@ -133,3 +133,5 @@ module channelL [TO_Ack] (l=2) -> (l'=0); endmodule + +label "error" = s=5; diff --git a/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm b/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm index 0b05d22fd..7145a77ae 100644 --- a/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm +++ b/examples/pdtmc/brp_rewards2/brp_rewards16_2.pm @@ -144,3 +144,5 @@ rewards endrewards +label "target" = s=5; + diff --git a/examples/pdtmc/brp_rewards2/brp_rewards2.pm b/examples/pdtmc/brp_rewards2/brp_rewards2.pm index b4cc546e1..a8e5eced1 100644 --- a/examples/pdtmc/brp_rewards2/brp_rewards2.pm +++ b/examples/pdtmc/brp_rewards2/brp_rewards2.pm @@ -143,4 +143,5 @@ rewards [TO_Ack] true : TOAck; endrewards - +label "fatal" = s=5 & T; +label "false_neg" = srep=1 & rrep=3 & recv; diff --git a/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm b/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm index d756a90ec..ff62fea14 100644 --- a/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm +++ b/examples/pdtmc/brp_rewards4/brp_rewards16_2.pm @@ -144,3 +144,5 @@ rewards endrewards + +label "target" = s=5; \ No newline at end of file diff --git a/examples/pdtmc/brp_rewards4/brp_rewards4.pm b/examples/pdtmc/brp_rewards4/brp_rewards4.pm index 5617e839b..223993bc4 100644 --- a/examples/pdtmc/brp_rewards4/brp_rewards4.pm +++ b/examples/pdtmc/brp_rewards4/brp_rewards4.pm @@ -144,3 +144,6 @@ rewards endrewards + +label "fatal" = s=5 & T; +label "false_neg" = srep=1 & rrep=3 & recv; diff --git a/examples/pdtmc/die.pm b/examples/pdtmc/die.pm new file mode 100644 index 000000000..a2a8f57b0 --- /dev/null +++ b/examples/pdtmc/die.pm @@ -0,0 +1,35 @@ +// Knuth's model of a fair die using only fair coins +dtmc + +const double p; +const double q; + +module die + + // local state + s : [0..7] init 0; + // value of the dice + d : [0..6] init 0; + + [] s=0 -> p : (s'=1) + 1-p : (s'=2); + [] s=1 -> q : (s'=3) + 1-q : (s'=4); + [] s=2 -> q : (s'=5) + 1-q : (s'=6); + [] s=3 -> p : (s'=1) + 1-p : (s'=7) & (d'=1); + [] s=4 -> p : (s'=7) & (d'=3) + 1-p : (s'=7) & (d'=2); + [] s=5 -> p : (s'=2) + 1-p : (s'=7) & (d'=4); + [] s=6 -> p : (s'=7) & (d'=6) + 1-p : (s'=7) & (d'=5); + [] s=7 -> 1: (s'=7); + +endmodule + +rewards "coin_flips" + [] s<7 : 1; +endrewards + +label "one" = s=7&d=1; +label "two" = s=7&d=2; +label "three" = s=7&d=3; +label "four" = s=7&d=4; +label "five" = s=7&d=5; +label "six" = s=7&d=6; +label "end" = s=7; diff --git a/examples/pdtmc/twodie.pm b/examples/pdtmc/twodie.pm new file mode 100644 index 000000000..d38f75496 --- /dev/null +++ b/examples/pdtmc/twodie.pm @@ -0,0 +1,44 @@ +// Knuth's model of a fair die using only fair coins +dtmc + +const double p; +const double q; + +module die1 + + // local state + s1 : [0..7] init 0; + // value of the dice + d1 : [0..6] init 0; + + [] s1=0 -> p : (s1'=1) + 1-p : (s1'=2); + [] s1=1 -> q : (s1'=3) + 1-q : (s1'=4); + [] s1=2 -> q : (s1'=5) + 1-q : (s1'=6); + [] s1=3 -> p : (s1'=1) + 1-p : (s1'=7) & (d1'=1); + [] s1=4 -> p : (s1'=7) & (d1'=3) + 1-p : (s1'=7) & (d1'=2); + [] s1=5 -> p : (s1'=2) + 1-p : (s1'=7) & (d1'=4); + [] s1=6 -> p : (s1'=7) & (d1'=6) + 1-p : (s1'=7) & (d1'=5); + [] s1=7 -> 1: (s1'=7); + +endmodule + +module die2 = die1 [ s1=s2, s2=s1, d1=d2 ] endmodule + +rewards "coin_flips" + [] s1<7 | s2<7 : 1; +endrewards + +label "two" = s1=7 & s2=7 & d1+d2=2; +label "three" = s1=7 & s2=7 & d1+d2=3; +label "four" = s1=7 & s2=7 & d1+d2=4; +label "five" = s1=7 & s2=7 & d1+d2=5; +label "six" = s1=7 & s2=7 & d1+d2=6; +label "seven" = s1=7 & s2=7 & d1+d2=7; +label "eight" = s1=7 & s2=7 & d1+d2=8; +label "nine" = s1=7 & s2=7 & d1+d2=9; +label "ten" = s1=7 & s2=7 & d1+d2=10; +label "eleven" = s1=7 & s2=7 & d1+d2=11; +label "twelve" = s1=7 & s2=7 & d1+d2=12; +label "same" = s1=7 & s2=7 & d1=d2; + +label "end" = s1=7 & s2=7; diff --git a/examples/pmdp/brp/brp.pm b/examples/pmdp/brp/brp.pm index 2722cb0ee..0d76e95aa 100644 --- a/examples/pmdp/brp/brp.pm +++ b/examples/pmdp/brp/brp.pm @@ -136,4 +136,6 @@ module channelL endmodule +label "error" = s=5; +label "fatal" = s=5 & T; diff --git a/examples/pmdp/coin2/coin2.pm b/examples/pmdp/coin2/coin2.pm index 8baa365f4..79a25b870 100644 --- a/examples/pmdp/coin2/coin2.pm +++ b/examples/pmdp/coin2/coin2.pm @@ -47,7 +47,10 @@ endmodule module process2 = process1[pc1=pc2,coin1=coin2,p1=p2] endmodule label "finished" = pc1=3 &pc2=3 ; -label "all_coins_equal_1" = coin1=1 &coin2=1 ; +label "all_coins_equal_0" = coin1=0 & coin2=0; +label "all_coins_equal_1" = coin1=1 & coin2=1; +label "agree" = coin1 = coin2; + rewards "steps" true : 1; endrewards diff --git a/examples/pmdp/coin4/coin4.pm b/examples/pmdp/coin4/coin4.pm index bdb4bd877..d3648919f 100644 --- a/examples/pmdp/coin4/coin4.pm +++ b/examples/pmdp/coin4/coin4.pm @@ -53,6 +53,9 @@ module process4 = process1[pc1=pc4,coin1=coin4,p1=p4] endmodule label "finished" = pc1=3 &pc2=3 &pc3=3 &pc4=3; label "all_coins_equal_1" = coin1=1 &coin2=1 &coin3=1 &coin4=1 ; +label "all_coins_equal_0" = coin1=0 & coin2=0 & coin3 = 0 & coin4 = 0; +label "agree" = coin1=coin2 & coin2=coin3 & coin3 = coin4; + rewards "steps" true : 1; endrewards diff --git a/examples/pmdp/zeroconf/zeroconf.pm b/examples/pmdp/zeroconf/zeroconf.pm index 9c71181f2..682db33d4 100644 --- a/examples/pmdp/zeroconf/zeroconf.pm +++ b/examples/pmdp/zeroconf/zeroconf.pm @@ -256,3 +256,14 @@ module host0 [] l=4 -> 1 : true; endmodule + +// reward structure +const double err; // cost associated with using a IP address already in use + +rewards + [time] true : 1; + [send] l=3 & mess=0 & y=CONSEC & probes=1 & ip=1 : err; +endrewards + +label "selected_ip" = l = 4; +label "selected_ip_in_use" = l = 4 & ip = 1; diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt index 244e24057..ffd5fc54c 100644 --- a/resources/3rdparty/CMakeLists.txt +++ b/resources/3rdparty/CMakeLists.txt @@ -330,9 +330,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() diff --git a/resources/cmake/find_modules/FindHwloc.cmake b/resources/cmake/find_modules/FindHwloc.cmake index d1b5b488e..1db759375 100644 --- a/resources/cmake/find_modules/FindHwloc.cmake +++ b/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() \ No newline at end of file diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 8b54e0eba..1b759cfc5 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -895,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; } @@ -1107,7 +1106,8 @@ namespace storm { } // Add the source location and the guard. - transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.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()) { @@ -1124,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); diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 2c5104123..2d0b467aa 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -213,65 +213,92 @@ namespace storm { auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>(); if (ioSettings.isPrismOrJaniInputSet()) { storm::storage::SymbolicModelDescription model; + std::vector<storm::jani::Property> properties; + if (ioSettings.isPrismInputSet()) { model = storm::parseProgram(ioSettings.getPrismInputFilename()); if (ioSettings.isPrismToJaniSet()) { model = model.toJani(true); } } else if (ioSettings.isJaniInputSet()) { - model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first; + auto input = storm::parseJaniModel(ioSettings.getJaniInputFilename()); + model = input.first; + if (ioSettings.isJaniPropertiesSet()) { + for (auto const& propName : ioSettings.getJaniProperties()) { + STORM_LOG_THROW( input.second.count(propName) == 1, storm::exceptions::InvalidArgumentException, "No property with name " << propName << " known."); + properties.push_back(input.second.at(propName)); + } + } + + } + + // Then proceed to parsing the properties (if given), since the model we are building may depend on the property. + uint64_t i = 0; + if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) { + if (model.isJaniModel()) { + for(auto const& formula : storm::parseFormulasForJaniModel(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asJaniModel())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + } + } else { + for(auto const& formula :storm::parseFormulasForPrismProgram(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty(), model.asPrismProgram())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + } + } } 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, formulasInProperties(properties), 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(), formulasInProperties(properties), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); } } + if (ioSettings.isNoBuildModelSet()) { + return; + } + // Get the string that assigns values to the unknown currently undefined constants in the model. 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 - buildAndCheckSymbolicModel<storm::RationalFunction>(model, formulas, true); + buildAndCheckSymbolicModel<storm::RationalFunction>(model, properties, true); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build."); #endif } else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) { #ifdef STORM_HAVE_CARL - buildAndCheckSymbolicModel<storm::RationalNumber>(model, formulas, true); + buildAndCheckSymbolicModel<storm::RationalNumber>(model, properties, true); #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build."); #endif } else { - buildAndCheckSymbolicModel<double>(model, formulas, true); + buildAndCheckSymbolicModel<double>(model, properties, true); } } else if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExplicitSet()) { STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Only the sparse engine supports explicit model input."); // If the model is given in an explicit format, we parse the properties without allowing expressions // in formulas. - std::vector<std::shared_ptr<storm::logic::Formula const>> formulas; + std::vector<storm::jani::Property> properties; if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isPropertySet()) { - formulas = storm::parseFormulasForExplicit(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty()); + uint64_t i = 0; + for(auto const& formula : storm::parseFormulasForExplicit(storm::settings::getModule<storm::settings::modules::GeneralSettings>().getProperty())) { + properties.emplace_back(std::to_string(i), formula); + ++i; + + } } - buildAndCheckExplicitModel<double>(formulas, true); + buildAndCheckExplicitModel<double>(properties, true); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model."); } diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h index f4b009b7e..6cc2453ee 100644 --- a/src/cli/entrypoints.h +++ b/src/cli/entrypoints.h @@ -4,6 +4,7 @@ #include "src/utility/storm.h" #include "src/storage/SymbolicModelDescription.h" +#include "src/utility/ExplicitExporter.h" #include "src/exceptions/NotImplementedException.h" #include "src/exceptions/InvalidSettingsException.h" @@ -12,15 +13,72 @@ namespace storm { namespace cli { template<typename ValueType> - void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); + void applyFilterFunctionAndOutput(std::unique_ptr<storm::modelchecker::CheckResult> const& result, storm::modelchecker::FilterType ft) { + + if(result->isQuantitative()) { + switch(ft) { + case storm::modelchecker::FilterType::VALUES: + std::cout << *result << std::endl; + return; + case storm::modelchecker::FilterType::SUM: + std::cout << result->asQuantitativeCheckResult<ValueType>().sum(); + return; + case storm::modelchecker::FilterType::AVG: + std::cout << result->asQuantitativeCheckResult<ValueType>().average(); + return; + case storm::modelchecker::FilterType::MIN: + std::cout << result->asQuantitativeCheckResult<ValueType>().getMin(); + return; + case storm::modelchecker::FilterType::MAX: + std::cout << result->asQuantitativeCheckResult<ValueType>().getMax(); + return; + case storm::modelchecker::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMAX: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Outputting states is not supported"); + case storm::modelchecker::FilterType::EXISTS: + case storm::modelchecker::FilterType::FORALL: + case storm::modelchecker::FilterType::COUNT: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "FilterType only defined for qualitative results"); + } + } else { + switch(ft) { + case storm::modelchecker::FilterType::VALUES: + std::cout << *result << std::endl; + return; + case storm::modelchecker::FilterType::EXISTS: + std::cout << result->asQualitativeCheckResult().existsTrue(); + return; + case storm::modelchecker::FilterType::FORALL: + std::cout << result->asQualitativeCheckResult().forallTrue(); + return; + case storm::modelchecker::FilterType::COUNT: + std::cout << result->asQualitativeCheckResult().count(); + return; + + case storm::modelchecker::FilterType::ARGMIN: + case storm::modelchecker::FilterType::ARGMAX: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Outputting states is not supported"); + case storm::modelchecker::FilterType::SUM: + case storm::modelchecker::FilterType::AVG: + case storm::modelchecker::FilterType::MIN: + case storm::modelchecker::FilterType::MAX: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "FilterType only defined for quantitative results"); + } + + } + } + + template<typename ValueType> + void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) { + for (auto const& property : properties) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -29,17 +87,18 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { + inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant) { - for (auto const& formula : formulas) { + for (auto const& property : properties) { STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc || model->getType() == storm::models::ModelType::Ctmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs and CTMCs."); - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant)); + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput<storm::RationalFunction>(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -52,24 +111,24 @@ namespace storm { #endif template<storm::dd::DdType DdType> - void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithAbstractionRefinementEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented."); } template<typename ValueType> - void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void verifySymbolicModelWithExplorationEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::InvalidSettingsException, "Exploration engine is currently only applicable to PRISM models."); storm::prism::Program const& program = model.asPrismProgram(); STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs."); - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; bool supportFormula; std::unique_ptr<storm::modelchecker::CheckResult> result; if(program.getModelType() == storm::prism::Program::ModelType::DTMC) { storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Dtmc<ValueType>> checker(program); - storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask<storm::logic::Formula> task(*property.getFilter().getFormula(), onlyInitialStatesRelevant); supportFormula = checker.canHandle(task); if (supportFormula) { @@ -77,7 +136,7 @@ namespace storm { } } else if(program.getModelType() == storm::prism::Program::ModelType::MDP) { storm::modelchecker::SparseExplorationModelChecker<storm::models::sparse::Mdp<ValueType>> checker(program); - storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant); + storm::modelchecker::CheckTask<storm::logic::Formula> task(*property.getFilter().getFormula(), onlyInitialStatesRelevant); supportFormula = checker.canHandle(task); if (supportFormula) { @@ -94,7 +153,8 @@ namespace storm { if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; - std::cout << *result << std::endl; + applyFilterFunctionAndOutput<ValueType>(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -103,22 +163,23 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void verifySymbolicModelWithExplorationEngine<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { + void verifySymbolicModelWithExplorationEngine<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Exploration-based verification does currently not support parametric models."); } #endif template<storm::dd::DdType DdType> - void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, formula, onlyInitialStatesRelevant)); + void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -126,15 +187,16 @@ namespace storm { } template<storm::dd::DdType DdType> - void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { - for (auto const& formula : formulas) { - std::cout << std::endl << "Model checking property: " << *formula << " ..."; - std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, formula, onlyInitialStatesRelevant)); + void verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { + for (auto const& property : formulas) { + std::cout << std::endl << "Model checking property: " << property << " ..."; + std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, property.getFilter().getFormula(), onlyInitialStatesRelevant)); if (result) { std::cout << " done." << std::endl; std::cout << "Result (initial states): "; result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(model->getReachableStates(), model->getInitialStates())); - std::cout << *result << std::endl; + applyFilterFunctionAndOutput<double>(result, property.getFilter().getFilterType()); + std::cout << std::endl; } else { std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl; } @@ -182,23 +244,24 @@ namespace storm { } template<storm::dd::DdType LibraryType> - void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModelWithSymbolicEngine(bool hybrid, storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) { // Start by building the model. - auto markovModel = buildSymbolicModel<double, LibraryType>(model, formulas); + auto markovModel = buildSymbolicModel<double, LibraryType>(model, formulasInProperties(properties)); // Print some information about the model. markovModel->printModelInformationToStream(std::cout); // Then select the correct engine. if (hybrid) { - verifySymbolicModelWithHybridEngine(markovModel, formulas, onlyInitialStatesRelevant); + verifySymbolicModelWithHybridEngine(markovModel, properties, onlyInitialStatesRelevant); } else { - verifySymbolicModelWithDdEngine(markovModel, formulas, onlyInitialStatesRelevant); + verifySymbolicModelWithDdEngine(markovModel, properties, onlyInitialStatesRelevant); } } template<typename ValueType> - void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModelWithSparseEngine(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) { + auto formulas = formulasInProperties(properties); // Start by building the model. std::shared_ptr<storm::models::ModelBase> markovModel = buildSparseModel<ValueType>(model, formulas); @@ -214,12 +277,20 @@ namespace storm { if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isCounterexampleSet()) { generateCounterexamples<ValueType>(model, sparseModel, formulas); } else { - verifySparseModel<ValueType>(sparseModel, formulas, onlyInitialStatesRelevant); + verifySparseModel<ValueType>(sparseModel, properties, onlyInitialStatesRelevant); + } + + // And export if required. + if(storm::settings::getModule<storm::settings::modules::IOSettings>().isExportExplicitSet()) { + std::ofstream ofs; + ofs.open(storm::settings::getModule<storm::settings::modules::IOSettings>().getExportExplicitFilename(), std::ofstream::out); + storm::exporter::explicitExportSparseModel(ofs, sparseModel, model.getParameterNames()); + ofs.close(); } } template<typename ValueType> - void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckSymbolicModel(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant = false) { if (storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) { auto ddlib = storm::settings::getModule<storm::settings::modules::CoreSettings>().getDdLibraryType(); if (ddlib == storm::dd::DdType::CUDD) { @@ -247,35 +318,35 @@ namespace storm { #ifdef STORM_HAVE_CARL template<> - void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { + void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine<storm::RationalNumber>(model, formulas, onlyInitialStatesRelevant); } template<> - void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) { + void buildAndCheckSymbolicModel<storm::RationalFunction>(storm::storage::SymbolicModelDescription const& model, std::vector<storm::jani::Property> const& formulas, bool onlyInitialStatesRelevant) { STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one."); buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(model, formulas, onlyInitialStatesRelevant); } #endif template<typename ValueType> - void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + void buildAndCheckExplicitModel(std::vector<storm::jani::Property> const& properties, bool onlyInitialStatesRelevant = false) { storm::settings::modules::IOSettings const& settings = storm::settings::getModule<storm::settings::modules::IOSettings>(); STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files."); std::shared_ptr<storm::models::ModelBase> model = buildExplicitModel<ValueType>(settings.getTransitionFilename(), settings.getLabelingFilename(), settings.isStateRewardsSet() ? boost::optional<std::string>(settings.getStateRewardsFilename()) : boost::none, settings.isTransitionRewardsSet() ? boost::optional<std::string>(settings.getTransitionRewardsFilename()) : boost::none, settings.isChoiceLabelingSet() ? boost::optional<std::string>(settings.getChoiceLabelingFilename()) : boost::none); // Preprocess the model if needed. - BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulas); + BRANCH_ON_MODELTYPE(model, model, ValueType, storm::dd::DdType::CUDD, preprocessModel, formulasInProperties(properties)); // Print some information about the model. model->printModelInformationToStream(std::cout); // Verify the model, if a formula was given. - if (!formulas.empty()) { + if (!properties.empty()) { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model."); - verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas, onlyInitialStatesRelevant); + verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), properties, onlyInitialStatesRelevant); } } } diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index bc166cba3..80473c2f9 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -188,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; @@ -486,6 +486,8 @@ namespace storm { currentTargetStates = newTargetStates; newTargetStates = new boost::container::flat_map<CompressedState, ValueType>(); } + + ++locationVariableIt; } // At this point, we applied all commands of the current command combination and newTargetStates @@ -541,7 +543,6 @@ namespace storm { // Iterate over all automata. uint64_t automatonIndex = 0; for (auto const& automaton : model.getAutomata()) { - // If the automaton has no edge labeled with the given action, we can skip it. if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) { continue; diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp index c1a00e4e6..3545f1e49 100644 --- a/src/generator/VariableInformation.cpp +++ b/src/generator/VariableInformation.cpp @@ -63,15 +63,19 @@ 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()))); @@ -79,15 +83,19 @@ namespace storm { 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; + } } } diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp index aa86846fa..f5488122c 100644 --- a/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.cpp @@ -70,6 +70,47 @@ namespace storm { return *this; } + + bool ExplicitQualitativeCheckResult::existsTrue() const { + if (this->isResultForAllStates()) { + return !boost::get<vector_type>(truthValues).empty(); + } else { + for (auto& element : boost::get<map_type>(truthValues)) { + if(element.second) { + return true; + } + } + return false; + } + } + bool ExplicitQualitativeCheckResult::forallTrue() const { + if (this->isResultForAllStates()) { + return boost::get<vector_type>(truthValues).full(); + } else { + for (auto& element : boost::get<map_type>(truthValues)) { + if(!element.second) { + return false; + } + } + return true; + } + } + + uint64_t ExplicitQualitativeCheckResult::count() const { + if (this->isResultForAllStates()) { + return boost::get<vector_type>(truthValues).getNumberOfSetBits(); + } else { + uint64_t result = 0; + for (auto& element : boost::get<map_type>(truthValues)) { + if(element.second) { + ++result; + } + } + return result; + } + } + + bool ExplicitQualitativeCheckResult::operator[](storm::storage::sparse::state_type state) const { if (this->isResultForAllStates()) { return boost::get<vector_type>(truthValues).get(state); diff --git a/src/modelchecker/results/ExplicitQualitativeCheckResult.h b/src/modelchecker/results/ExplicitQualitativeCheckResult.h index 665675cfd..afb54b4be 100644 --- a/src/modelchecker/results/ExplicitQualitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQualitativeCheckResult.h @@ -47,6 +47,12 @@ namespace storm { vector_type const& getTruthValuesVector() const; map_type const& getTruthValuesVectorMap() const; + + virtual bool existsTrue() const override; + virtual bool forallTrue() const override; + virtual uint64_t count() const override; + + virtual std::ostream& writeToStream(std::ostream& out) const override; virtual void filter(QualitativeCheckResult const& filter) override; diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp index 6233216d9..87ba9e0fa 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp @@ -3,6 +3,7 @@ #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h" #include "src/storage/BitVector.h" #include "src/utility/macros.h" +#include "src/utility/constants.h" #include "src/utility/vector.h" #include "src/exceptions/InvalidOperationException.h" #include "src/exceptions/InvalidAccessException.h" @@ -81,6 +82,64 @@ namespace storm { } } + template<typename ValueType> + ValueType ExplicitQuantitativeCheckResult<ValueType>::getMin() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + if (this->isResultForAllStates()) { + return storm::utility::minimum(boost::get<vector_type>(values)); + } else { + return storm::utility::minimum(boost::get<map_type>(values)); + } + } + + + template<typename ValueType> + ValueType ExplicitQuantitativeCheckResult<ValueType>::getMax() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + if (this->isResultForAllStates()) { + return storm::utility::maximum(boost::get<vector_type>(values)); + } else { + return storm::utility::maximum(boost::get<map_type>(values)); + } + } + + template<typename ValueType> + ValueType ExplicitQuantitativeCheckResult<ValueType>::sum() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + ValueType sum = storm::utility::zero<ValueType>(); + if (this->isResultForAllStates()) { + for (auto& element : boost::get<vector_type>(values)) { + sum += element; + } + } else { + for (auto& element : boost::get<map_type>(values)) { + sum += element.second; + } + } + return sum; + } + + template<typename ValueType> + ValueType ExplicitQuantitativeCheckResult<ValueType>::average() const { + STORM_LOG_THROW(!values.empty(),storm::exceptions::InvalidOperationException, "Minimum of empty set is not defined"); + + ValueType sum = storm::utility::zero<ValueType>(); + if (this->isResultForAllStates()) { + for (auto& element : boost::get<vector_type>(values)) { + sum += element; + } + return sum / boost::get<vector_type>(values).size(); + } else { + for (auto& element : boost::get<map_type>(values)) { + sum += element.second; + } + return sum / boost::get<map_type>(values).size(); + } + } + template<typename ValueType> bool ExplicitQuantitativeCheckResult<ValueType>::hasScheduler() const { return static_cast<bool>(scheduler); diff --git a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h index 639da4fa7..d2bb9f711 100644 --- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.h +++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.h @@ -53,6 +53,12 @@ namespace storm { virtual void oneMinus() override; + + virtual ValueType getMin() const override; + virtual ValueType getMax() const override; + virtual ValueType average() const override; + virtual ValueType sum() const override; + bool hasScheduler() const; void setScheduler(std::unique_ptr<storm::storage::Scheduler>&& scheduler); storm::storage::Scheduler const& getScheduler() const; diff --git a/src/modelchecker/results/FilterType.cpp b/src/modelchecker/results/FilterType.cpp new file mode 100644 index 000000000..3a15c8169 --- /dev/null +++ b/src/modelchecker/results/FilterType.cpp @@ -0,0 +1,32 @@ +#include "FilterType.h" + + +namespace storm { + namespace modelchecker { + + std::string toString(FilterType ft) { + switch(ft) { + case FilterType::ARGMAX: + return "the argmax"; + case FilterType::ARGMIN: + return "the argmin"; + case FilterType::AVG: + return "the average"; + case FilterType::COUNT: + return "the number of"; + case FilterType::EXISTS: + return "whether there exists a state in"; + case FilterType::FORALL: + return "whether for all states in"; + case FilterType::MAX: + return "the maximum"; + case FilterType::MIN: + return "the minumum"; + case FilterType::SUM: + return "the sum"; + case FilterType::VALUES: + return "the values"; + } + } + } +} \ No newline at end of file diff --git a/src/modelchecker/results/FilterType.h b/src/modelchecker/results/FilterType.h new file mode 100644 index 000000000..040b09084 --- /dev/null +++ b/src/modelchecker/results/FilterType.h @@ -0,0 +1,14 @@ +#pragma once +#include <string> + +namespace storm { + namespace modelchecker { + + enum class StateFilter { ARGMIN, ARGMAX }; + + enum class FilterType { MIN, MAX, SUM, AVG, COUNT, FORALL, EXISTS, ARGMIN, ARGMAX, VALUES }; + + std::string toString(FilterType); + bool isStateFilter(FilterType); + } +} \ No newline at end of file diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp index a32095e40..2aeab204f 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.cpp @@ -5,9 +5,12 @@ #include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/exceptions/InvalidOperationException.h" + +#include "src/exceptions/NotImplementedException.h" #include "src/utility/macros.h" #include "src/utility/constants.h" + namespace storm { namespace modelchecker { template<storm::dd::DdType Type, typename ValueType> @@ -54,7 +57,7 @@ namespace storm { template<storm::dd::DdType Type, typename ValueType> bool HybridQuantitativeCheckResult<Type, ValueType>::isResultForAllStates() const { - return true; + return (symbolicStates || explicitStates) == reachableStates; } template<storm::dd::DdType Type, typename ValueType> @@ -164,6 +167,20 @@ namespace storm { return max; } + template<storm::dd::DdType Type, typename ValueType> + ValueType HybridQuantitativeCheckResult<Type, ValueType>::sum() const { + ValueType sum = symbolicValues.sumAbstract(symbolicValues.getContainedMetaVariables()).getValue(); + for (auto const& value : explicitValues) { + sum += value; + } + return sum; + } + + template<storm::dd::DdType Type, typename ValueType> + ValueType HybridQuantitativeCheckResult<Type, ValueType>::average() const { + return this->sum() / (symbolicStates || explicitStates).getNonZeroCount(); + } + template<storm::dd::DdType Type, typename ValueType> void HybridQuantitativeCheckResult<Type, ValueType>::oneMinus() { storm::dd::Add<Type> one = symbolicValues.getDdManager().template getAddOne<ValueType>(); @@ -175,8 +192,9 @@ namespace storm { } } + // Explicitly instantiate the class. template class HybridQuantitativeCheckResult<storm::dd::DdType::CUDD>; template class HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan>; } -} \ No newline at end of file +} diff --git a/src/modelchecker/results/HybridQuantitativeCheckResult.h b/src/modelchecker/results/HybridQuantitativeCheckResult.h index 8b7db1cea..43b1a39a4 100644 --- a/src/modelchecker/results/HybridQuantitativeCheckResult.h +++ b/src/modelchecker/results/HybridQuantitativeCheckResult.h @@ -46,9 +46,13 @@ namespace storm { virtual void filter(QualitativeCheckResult const& filter) override; - virtual ValueType getMin() const; + virtual ValueType getMin() const override; - virtual ValueType getMax() const; + virtual ValueType getMax() const override; + + virtual ValueType sum() const override; + + virtual ValueType average() const override; virtual void oneMinus() override; @@ -74,4 +78,4 @@ namespace storm { } } -#endif /* STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_HYBRIDQUANTITATIVECHECKRESULT_H_ */ diff --git a/src/modelchecker/results/QualitativeCheckResult.h b/src/modelchecker/results/QualitativeCheckResult.h index 608e2c0d1..f4a89665b 100644 --- a/src/modelchecker/results/QualitativeCheckResult.h +++ b/src/modelchecker/results/QualitativeCheckResult.h @@ -12,6 +12,10 @@ namespace storm { virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other); virtual void complement(); + virtual bool existsTrue() const = 0; + virtual bool forallTrue() const = 0; + virtual uint64_t count() const = 0; + virtual bool isQualitative() const override; }; } diff --git a/src/modelchecker/results/QuantitativeCheckResult.h b/src/modelchecker/results/QuantitativeCheckResult.h index bb268ae3f..2e9abe6a9 100644 --- a/src/modelchecker/results/QuantitativeCheckResult.h +++ b/src/modelchecker/results/QuantitativeCheckResult.h @@ -1,5 +1,4 @@ -#ifndef STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ -#define STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ +#pragma once #include "src/modelchecker/results/CheckResult.h" @@ -14,9 +13,16 @@ namespace storm { virtual void oneMinus() = 0; + + virtual ValueType getMin() const = 0; + + virtual ValueType getMax() const = 0; + + virtual ValueType average() const = 0; + virtual ValueType sum() const = 0; + virtual bool isQuantitative() const override; }; } } -#endif /* STORM_MODELCHECKER_QUANTITATIVECHECKRESULT_H_ */ \ No newline at end of file diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp index 2275b942f..da97a38da 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.cpp @@ -3,10 +3,12 @@ #include "src/utility/macros.h" #include "src/exceptions/InvalidOperationException.h" +#include "src/exceptions/NotImplementedException.h" + namespace storm { namespace modelchecker { template <storm::dd::DdType Type> - SymbolicQualitativeCheckResult<Type>::SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& truthValues) : reachableStates(reachableStates), truthValues(truthValues) { + SymbolicQualitativeCheckResult<Type>::SymbolicQualitativeCheckResult(storm::dd::Bdd<Type> const& reachableStates, storm::dd::Bdd<Type> const& truthValues) : reachableStates(reachableStates), states(reachableStates), truthValues(truthValues) { // Intentionally left empty. } @@ -17,7 +19,7 @@ namespace storm { template <storm::dd::DdType Type> bool SymbolicQualitativeCheckResult<Type>::isResultForAllStates() const { - return true; + return reachableStates == states; } template <storm::dd::DdType Type> @@ -46,7 +48,22 @@ namespace storm { template <storm::dd::DdType Type> storm::dd::Bdd<Type> const& SymbolicQualitativeCheckResult<Type>::getTruthValuesVector() const { - return truthValues; + return this->truthValues; + } + + template <storm::dd::DdType Type> + bool SymbolicQualitativeCheckResult<Type>::existsTrue() const { + return !this->truthValues.isZero(); + } + + template <storm::dd::DdType Type> + bool SymbolicQualitativeCheckResult<Type>::forallTrue() const { + return this->truthValues == this->states; + } + + template <storm::dd::DdType Type> + uint64_t SymbolicQualitativeCheckResult<Type>::count() const { + return this->truthValues.getNonZeroCount(); } template <storm::dd::DdType Type> @@ -63,9 +80,10 @@ namespace storm { void SymbolicQualitativeCheckResult<Type>::filter(QualitativeCheckResult const& filter) { STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter symbolic check result with non-symbolic filter."); this->truthValues &= filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector(); + this->states &= filter.asSymbolicQualitativeCheckResult<Type>().getTruthValuesVector(); } template class SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>; template class SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>; } -} \ No newline at end of file +} diff --git a/src/modelchecker/results/SymbolicQualitativeCheckResult.h b/src/modelchecker/results/SymbolicQualitativeCheckResult.h index 3e94f5ee8..db3ee1ab5 100644 --- a/src/modelchecker/results/SymbolicQualitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQualitativeCheckResult.h @@ -30,6 +30,12 @@ namespace storm { virtual QualitativeCheckResult& operator|=(QualitativeCheckResult const& other) override; virtual void complement() override; + + virtual bool existsTrue() const override; + virtual bool forallTrue() const override; + virtual uint64_t count() const override; + + storm::dd::Bdd<Type> const& getTruthValuesVector() const; virtual std::ostream& writeToStream(std::ostream& out) const override; @@ -39,11 +45,14 @@ namespace storm { private: // The set of all reachable states. storm::dd::Bdd<Type> reachableStates; - + + // The set of states for which this check result contains values. + storm::dd::Bdd<Type> states; + // The values of the qualitative check result. storm::dd::Bdd<Type> truthValues; }; } } -#endif /* STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ */ \ No newline at end of file +#endif /* STORM_MODELCHECKER_SYMBOLICQUALITATIVECHECKRESULT_H_ */ diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp index 57f68bdf1..5bc712d2d 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.cpp @@ -5,6 +5,8 @@ #include "src/storage/dd/cudd/CuddAddIterator.h" #include "src/exceptions/InvalidOperationException.h" + +#include "src/exceptions/NotImplementedException.h" #include "src/utility/macros.h" #include "src/utility/constants.h" @@ -89,6 +91,16 @@ namespace storm { return this->values.getMax(); } + template<storm::dd::DdType Type, typename ValueType> + ValueType SymbolicQuantitativeCheckResult<Type, ValueType>::average() const { + return this->sum() / this->states.getNonZeroCount(); + } + + template<storm::dd::DdType Type, typename ValueType> + ValueType SymbolicQuantitativeCheckResult<Type, ValueType>::sum() const { + return this->values.sumAbstract(this->values.getContainedMetaVariables()).getValue(); + } + template<storm::dd::DdType Type, typename ValueType> void SymbolicQuantitativeCheckResult<Type, ValueType>::oneMinus() { storm::dd::Add<Type> one = values.getDdManager().template getAddOne<ValueType>(); @@ -99,4 +111,4 @@ namespace storm { template class SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD>; template class SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan>; } -} \ No newline at end of file +} diff --git a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h index fd03da786..36b0c4cce 100644 --- a/src/modelchecker/results/SymbolicQuantitativeCheckResult.h +++ b/src/modelchecker/results/SymbolicQuantitativeCheckResult.h @@ -35,9 +35,12 @@ namespace storm { virtual void filter(QualitativeCheckResult const& filter) override; - virtual ValueType getMin() const; + virtual ValueType getMin() const override; - virtual ValueType getMax() const; + virtual ValueType getMax() const override; + + virtual ValueType average() const override; + virtual ValueType sum() const override; virtual void oneMinus() override; diff --git a/src/parser/CSVParser.cpp b/src/parser/CSVParser.cpp new file mode 100644 index 000000000..04e26a3fa --- /dev/null +++ b/src/parser/CSVParser.cpp @@ -0,0 +1,23 @@ +#include "src/parser/CSVParser.h" +#include <boost/any.hpp> + +#include <boost/algorithm/string.hpp> +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + + +namespace storm { + namespace parser { + + std::vector<std::string> parseCommaSeperatedValues(std::string const& input) { + std::vector<std::string> values; + std::vector<std::string> definitions; + boost::split(definitions, input, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + values.push_back(definition); + } + return values; + } + } +} \ No newline at end of file diff --git a/src/parser/CSVParser.h b/src/parser/CSVParser.h new file mode 100644 index 000000000..ec21f2e80 --- /dev/null +++ b/src/parser/CSVParser.h @@ -0,0 +1,12 @@ +#include <vector> +#include <string> + +namespace storm { + namespace parser { + /** + * Given a string seperated by commas, returns the values. + */ + std::vector<std::string> parseCommaSeperatedValues(std::string const& input); + + } +} \ No newline at end of file diff --git a/src/parser/JaniParser.cpp b/src/parser/JaniParser.cpp index a49ab5548..a149a9e92 100644 --- a/src/parser/JaniParser.cpp +++ b/src/parser/JaniParser.cpp @@ -5,9 +5,12 @@ #include "src/storage/jani/ParallelComposition.h" #include "src/exceptions/FileIoException.h" #include "src/exceptions/InvalidJaniException.h" + +#include "src/exceptions/NotSupportedException.h" #include "src/exceptions/NotImplementedException.h" #include "src/storage/jani/ModelType.h" +#include "src/modelchecker/results/FilterType.h" #include <iostream> #include <sstream> @@ -49,7 +52,7 @@ namespace storm { } - std::pair<storm::jani::Model, std::vector<storm::jani::Property>> JaniParser::parse(std::string const& path) { + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> JaniParser::parse(std::string const& path) { JaniParser parser; parser.readFile(path); return parser.parseModel(); @@ -75,7 +78,7 @@ namespace storm { file.close(); } - std::pair<storm::jani::Model, std::vector<storm::jani::Property>> JaniParser::parseModel(bool parseProperties) { + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> JaniParser::parseModel(bool parseProperties) { //jani-version STORM_LOG_THROW(parsedStructure.count("jani-version") == 1, storm::exceptions::InvalidJaniException, "Jani-version must be given exactly once."); uint64_t version = getUnsignedInt(parsedStructure.at("jani-version"), "jani version"); @@ -110,21 +113,322 @@ 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); STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given"); - PropertyVector properties; + std::map<std::string, storm::jani::Property> properties; if (parseProperties && parsedStructure.count("properties") == 1) { STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array"); for(auto const& propertyEntry : parsedStructure.at("properties")) { - properties.push_back(this->parseProperty(propertyEntry)); + try { + auto prop = this->parseProperty(propertyEntry); + properties.emplace(prop.getName(), prop); + } catch (storm::exceptions::NotSupportedException const& ex) { + STORM_LOG_WARN("Cannot handle property " << ex.what()); + } catch (storm::exceptions::NotImplementedException const& ex) { + STORM_LOG_WARN("Cannot handle property " << ex.what()); + } } } return {model, properties}; } + + std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser::parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context) { + STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting operand for operator " << opstring << " in " << context); + return { parseFormula(propertyStructure.at("exp"), formulaContext, "Operand of operator " + opstring) }; + } + + + std::vector<std::shared_ptr<storm::logic::Formula const>> JaniParser::parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context) { + STORM_LOG_THROW(propertyStructure.count("left") == 1, storm::exceptions::InvalidJaniException, "Expecting left operand for operator " << opstring << " in " << context); + STORM_LOG_THROW(propertyStructure.count("right") == 1, storm::exceptions::InvalidJaniException, "Expecting right operand for operator " << opstring << " in " << context); + return { parseFormula(propertyStructure.at("left"), formulaContext, "Operand of operator " + opstring), parseFormula(propertyStructure.at("right"), formulaContext, "Operand of operator " + opstring) }; + } + + storm::jani::PropertyInterval JaniParser::parsePropertyInterval(json const& piStructure) { + storm::jani::PropertyInterval pi; + if (piStructure.count("lower") > 0) { + pi.lowerBound = parseExpression(piStructure.at("lower"), "Lower bound for property interval"); + // TODO substitute constants. + STORM_LOG_THROW(!pi.lowerBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as lower bounds"); + + + } + if (piStructure.count("lower-exclusive") > 0) { + STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); + pi.lowerBoundStrict = piStructure.at("lower-exclusive"); + + } + if (piStructure.count("upper") > 0) { + pi.upperBound = parseExpression(piStructure.at("upper"), "Upper bound for property interval"); + // TODO substitute constants. + STORM_LOG_THROW(!pi.upperBound.containsVariables(), storm::exceptions::NotSupportedException, "Only constant expressions are supported as upper bounds"); + + } + if (piStructure.count("upper-exclusive") > 0) { + STORM_LOG_THROW(pi.lowerBound.isInitialized(), storm::exceptions::InvalidJaniException, "Lower-exclusive can only be set if a lower bound is present"); + pi.lowerBoundStrict = piStructure.at("upper-exclusive"); + } + STORM_LOG_THROW(pi.lowerBound.isInitialized() || pi.upperBound.isInitialized(), storm::exceptions::InvalidJaniException, "Bounded operators must be bounded"); + return pi; + + + } + + + std::shared_ptr<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound) { + if (propertyStructure.is_boolean()) { + return std::make_shared<storm::logic::BooleanLiteralFormula>(propertyStructure.get<bool>()); + } + if (propertyStructure.is_string()) { + if (labels.count(propertyStructure.get<std::string>()) > 0) { + return std::make_shared<storm::logic::AtomicLabelFormula>(propertyStructure.get<std::string>()); + } + } + storm::expressions::Expression expr = parseExpression(propertyStructure, "expression in property", {}, true); + if(expr.isInitialized()) { + assert(bound == boost::none); + return std::make_shared<storm::logic::AtomicExpressionFormula>(expr); + } else if(propertyStructure.count("op") == 1) { + std::string opString = getString(propertyStructure.at("op"), "Operation description"); + + if(opString == "Pmin" || opString == "Pmax") { + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, storm::logic::FormulaContext::Probability, opString, ""); + assert(args.size() == 1); + storm::logic::OperatorInformation opInfo; + opInfo.optimalityType = opString == "Pmin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; + opInfo.bound = bound; + return std::make_shared<storm::logic::ProbabilityOperatorFormula>(args[0], opInfo); + + } else if (opString == "∀" || opString == "∃") { + assert(bound == boost::none); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Forall and Exists are currently not supported"); + } else if (opString == "Emin" || opString == "Emax") { + bool time=false; + STORM_LOG_THROW(propertyStructure.count("exp") == 1, storm::exceptions::InvalidJaniException, "Expecting reward-expression for operator " << opString << " in " << context); + storm::expressions::Expression rewExpr = parseExpression(propertyStructure.at("exp"), "Reward expression in " + context); + if (rewExpr.isVariable()) { + time = false; + } else { + time = true; + } + std::shared_ptr<storm::logic::Formula const> reach; + if (propertyStructure.count("reach") > 0) { + reach = parseFormula(propertyStructure.at("reach"), time ? storm::logic::FormulaContext::Time : storm::logic::FormulaContext::Reward, "Reach-expression of operator " + opString); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Total reward is currently not supported"); + } + storm::logic::OperatorInformation opInfo; + opInfo.optimalityType = opString == "Emin" ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize; + opInfo.bound = bound; + + bool accTime = false; + bool accSteps = false; + if (propertyStructure.count("accumulate") > 0) { + STORM_LOG_THROW(propertyStructure.at("accumulate").is_array(), storm::exceptions::InvalidJaniException, "Accumulate should be an array"); + for(auto const& accEntry : propertyStructure.at("accumulate")) { + if (accEntry == "steps") { + accSteps = true; + } else if (accEntry == "time") { + accTime = true; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "One may only accumulate either 'steps' or 'time', got " << accEntry.dump() << " in " << context); + } + } + } + STORM_LOG_THROW(!(accTime && accSteps), storm::exceptions::NotSupportedException, "Storm does not allow to accumulate over both time and steps"); + + + if (propertyStructure.count("step-instant") > 0) { + storm::expressions::Expression stepInstantExpr = parseExpression(propertyStructure.at("step-instant"), "Step instant in " + context); + STORM_LOG_THROW(!stepInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant step-instants"); + int64_t stepInstant = stepInstantExpr.evaluateAsInt(); + STORM_LOG_THROW(stepInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative step-instants are allowed"); + if(!accTime && !accSteps) { + if (rewExpr.isVariable()) { + std::string rewardName = rewExpr.getVariables().begin()->getName(); + return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(static_cast<uint64_t>(stepInstant)), rewardName, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); + } + } else { + if (rewExpr.isVariable()) { + std::string rewardName = rewExpr.getVariables().begin()->getName(); + return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(static_cast<uint64_t>(stepInstant)), rewardName, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); + } + } + } else if (propertyStructure.count("time-instant") > 0) { + storm::expressions::Expression timeInstantExpr = parseExpression(propertyStructure.at("time-instant"), "time instant in " + context); + STORM_LOG_THROW(!timeInstantExpr.containsVariables(), storm::exceptions::NotSupportedException, "Storm only allows constant time-instants"); + double timeInstant = timeInstantExpr.evaluateAsDouble(); + STORM_LOG_THROW(timeInstant >= 0, storm::exceptions::InvalidJaniException, "Only non-negative time-instants are allowed"); + if(!accTime && !accSteps) { + if (rewExpr.isVariable()) { + std::string rewardName = rewExpr.getVariables().begin()->getName(); + return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::InstantaneousRewardFormula>(timeInstant), rewardName, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); + } + } else { + if (rewExpr.isVariable()) { + std::string rewardName = rewExpr.getVariables().begin()->getName(); + return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(timeInstant), rewardName, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported"); + } + } + } else if (propertyStructure.count("reward-instants") > 0) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Instant/Cumul. Reward for reward constraints not supported currently."); + } + + //STORM_LOG_THROW(!accTime && !accSteps, storm::exceptions::NotSupportedException, "Storm only allows accumulation if a step- or time-bound is given."); + + if (rewExpr.isVariable()) { + std::string rewardName = rewExpr.getVariables().begin()->getName(); + return std::make_shared<storm::logic::RewardOperatorFormula>(reach, rewardName, opInfo); + } else if (!rewExpr.containsVariables()) { + if(rewExpr.hasIntegerType()) { + if (rewExpr.evaluateAsInt() == 1) { + + return std::make_shared<storm::logic::TimeOperatorFormula>(reach, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expected steps/time only works with constant one."); + } + } else if (rewExpr.hasRationalType()){ + if (rewExpr.evaluateAsDouble() == 1.0) { + + return std::make_shared<storm::logic::TimeOperatorFormula>(reach, opInfo); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Expected steps/time only works with constant one."); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Only numerical reward expressions are allowed"); + } + + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex reward expressions are supported at the moment"); + } + + + } else if (opString == "Smin" || opString == "Smax") { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Smin and Smax are currently not supported"); + } else if (opString == "U" || opString == "F") { + assert(bound == boost::none); + std::vector<std::shared_ptr<storm::logic::Formula const>> args; + if (opString == "U") { + args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, ""); + } else { + assert(opString == "F"); + args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, ""); + args.push_back(args[0]); + args[0] = storm::logic::BooleanLiteralFormula::getTrueFormula(); + } + if (propertyStructure.count("step-bounds") > 0) { + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("step-bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports step-bounded until with an upper bound"); + if(pi.hasLowerBound()) { + STORM_LOG_THROW(pi.lowerBound.evaluateAsInt() == 0, storm::exceptions::NotSupportedException, "Storm only supports step-bounded until without a (non-trivial) lower-bound"); + } + int64_t upperBound = pi.upperBound.evaluateAsInt(); + if(pi.upperBoundStrict) { + upperBound--; + } + STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "Step-bounds cannot be negative"); + return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], upperBound); + } else if (propertyStructure.count("time-bounds") > 0) { + storm::jani::PropertyInterval pi = parsePropertyInterval(propertyStructure.at("time-bounds")); + STORM_LOG_THROW(pi.hasUpperBound(), storm::exceptions::NotSupportedException, "Storm only supports time-bounded until with an upper bound."); + double lowerBound = 0.0; + if(pi.hasLowerBound()) { + lowerBound = pi.lowerBound.evaluateAsDouble(); + } + double upperBound = pi.upperBound.evaluateAsDouble(); + STORM_LOG_THROW(lowerBound >= 0, storm::exceptions::InvalidJaniException, "(Lower) time-bounds cannot be negative"); + STORM_LOG_THROW(upperBound >= 0, storm::exceptions::InvalidJaniException, "(Upper) time-bounds cannot be negative"); + return std::make_shared<storm::logic::BoundedUntilFormula const>(args[0], args[1], upperBound); + + } else if (propertyStructure.count("reward-bounds") > 0 ) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); + } + if (args[0]->isTrueFormula()) { + return std::make_shared<storm::logic::EventuallyFormula const>(args[1], storm::logic::FormulaContext::Reward); + } else { + return std::make_shared<storm::logic::UntilFormula const>(args[0], args[1]); + } + } else if (opString == "G") { + assert(bound == boost::none); + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, "Subformula of globally operator " + context); + if (propertyStructure.count("step-bounds") > 0) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and step-bounds are not supported currently"); + } else if (propertyStructure.count("time-bounds") > 0) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Globally and time bounds are not supported by Storm"); + } else if (propertyStructure.count("reward-bounds") > 0 ) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Reward bounded properties are not supported by Storm"); + } + return std::make_shared<storm::logic::GloballyFormula const>(args[1]); + } else if (opString == "W") { + assert(bound == boost::none); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Weak until is not supported"); + } else if (opString == "R") { + assert(bound == boost::none); + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Release is not supported"); + } else if (opString == "∧" || opString == "∨") { + assert(bound == boost::none); + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseBinaryFormulaArguments(propertyStructure, formulaContext, opString, ""); + assert(args.size() == 2); + storm::logic::BinaryBooleanStateFormula::OperatorType oper = opString == "∧" ? storm::logic::BinaryBooleanStateFormula::OperatorType::And : storm::logic::BinaryBooleanStateFormula::OperatorType::Or; + return std::make_shared<storm::logic::BinaryBooleanStateFormula const>(oper, args[0], args[1]); + } else if (opString == "¬") { + assert(bound == boost::none); + std::vector<std::shared_ptr<storm::logic::Formula const>> args = parseUnaryFormulaArgument(propertyStructure, formulaContext, opString, ""); + assert(args.size() == 1); + return std::make_shared<storm::logic::UnaryBooleanStateFormula const>(storm::logic::UnaryBooleanStateFormula::OperatorType::Not, args[0]); + + } else if (opString == "≥" || opString == "≤" || opString == "<" || opString == ">") { + assert(bound == boost::none); + storm::logic::ComparisonType ct; + if(opString == "≥") { + ct = storm::logic::ComparisonType::GreaterEqual; + } else if (opString == "≤") { + ct = storm::logic::ComparisonType::LessEqual; + } else if (opString == "<") { + ct = storm::logic::ComparisonType::Less; + } else if (opString == ">") { + ct = storm::logic::ComparisonType::Greater; + } + if (propertyStructure.at("left").count("op") > 0 && (propertyStructure.at("left").at("op") == "Pmin" || propertyStructure.at("left").at("op") == "Pmax" || propertyStructure.at("left").at("op") == "Emin" || propertyStructure.at("left").at("op") == "Emax" || propertyStructure.at("left").at("op") == "Smin" || propertyStructure.at("left").at("op") == "Smax")) { + auto expr = parseExpression(propertyStructure.at("right"), "Threshold for operator " + propertyStructure.at("left").at("op").get<std::string>()); + STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); + // TODO evaluate this expression directly as rational number + return parseFormula(propertyStructure.at("left"), formulaContext, "", storm::logic::Bound<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble()))); + } else if(propertyStructure.at("right").count("op") > 0 && (propertyStructure.at("right").at("op") == "Pmin" || propertyStructure.at("right").at("op") == "Pmax" || propertyStructure.at("right").at("op") == "Emin" || propertyStructure.at("right").at("op") == "Emax" || propertyStructure.at("right").at("op") == "Smin" || propertyStructure.at("right").at("op") == "Smax")) { + auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get<std::string>()); + STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported"); + // TODO evaluate this expression directly as rational number + return parseFormula(propertyStructure.at("right"),formulaContext, "", storm::logic::Bound<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble()))); + + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex comparisons are allowed."); + } + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opString); + } + } + + } + storm::jani::Property JaniParser::parseProperty(json const& propertyStructure) { STORM_LOG_THROW(propertyStructure.count("name") == 1, storm::exceptions::InvalidJaniException, "Property must have a name"); // TODO check unique name @@ -133,8 +437,46 @@ namespace storm { if (propertyStructure.count("comment") > 0) { comment = getString(propertyStructure.at("comment"), "comment for property named '" + name + "'."); } + STORM_LOG_THROW(propertyStructure.count("expression") == 1, storm::exceptions::InvalidJaniException, "Property must have an expression"); + // Parse filter expression. + json const& expressionStructure = propertyStructure.at("expression"); - + STORM_LOG_THROW(expressionStructure.count("op") == 1, storm::exceptions::InvalidJaniException, "Expression in property must have an operation description"); + STORM_LOG_THROW(expressionStructure.at("op") == "filter", storm::exceptions::InvalidJaniException, "Top level operation of a property must be a filter"); + STORM_LOG_THROW(expressionStructure.count("fun") == 1, storm::exceptions::InvalidJaniException, "Filter must have a function descritpion"); + std::string funDescr = getString(expressionStructure.at("fun"), "Filter function in property named " + name); + storm::modelchecker::FilterType ft; + if (funDescr == "min") { + ft = storm::modelchecker::FilterType::MIN; + } else if (funDescr == "max") { + ft = storm::modelchecker::FilterType::MAX; + } else if (funDescr == "sum") { + ft = storm::modelchecker::FilterType::SUM; + } else if (funDescr == "avg") { + ft = storm::modelchecker::FilterType::AVG; + } else if (funDescr == "count") { + ft = storm::modelchecker::FilterType::COUNT; + } else if (funDescr == "∀") { + ft = storm::modelchecker::FilterType::FORALL; + } else if (funDescr == "∃") { + ft = storm::modelchecker::FilterType::EXISTS; + } else if (funDescr == "argmin") { + ft = storm::modelchecker::FilterType::ARGMIN; + } else if (funDescr == "argmax") { + ft = storm::modelchecker::FilterType::ARGMAX; + } else if (funDescr == "values") { + ft = storm::modelchecker::FilterType::VALUES; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown filter description " << funDescr << " in property named " << name); + } + + STORM_LOG_THROW(expressionStructure.count("states") == 1, storm::exceptions::InvalidJaniException, "Filter must have a states description"); + STORM_LOG_THROW(expressionStructure.at("states").count("op") > 0, storm::exceptions::NotImplementedException, "We only support properties where the filter has initial states"); + std::string statesDescr = getString(expressionStructure.at("states").at("op"), "Filtered states in property named " + name); + STORM_LOG_THROW(statesDescr == "initial", storm::exceptions::NotImplementedException, "Only initial states are allowed as set of states we are interested in."); + STORM_LOG_THROW(expressionStructure.count("values") == 1, storm::exceptions::InvalidJaniException, "Values as input for a filter must be given"); + auto formula = parseFormula(expressionStructure.at("values"), storm::logic::FormulaContext::Undefined, "Values of property " + name); + return storm::jani::Property(name, storm::jani::FilterExpression(formula, ft), comment); } std::shared_ptr<storm::jani::Constant> JaniParser::parseConstant(json const& constantStructure, std::string const& scopeDescription) { @@ -229,7 +571,6 @@ namespace storm { boost::optional<storm::expressions::Expression> initVal; if(variableStructure.at("type").is_string()) { if(variableStructure.at("type") == "real") { - expressionManager->declareRationalVariable(name); if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { initVal = expressionManager->rational(defaultRationalInitialValue); @@ -240,7 +581,8 @@ namespace storm { return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar); } - return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), transientVar); + assert(!transientVar); + return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName)); } else if(variableStructure.at("type") == "bool") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { @@ -249,9 +591,13 @@ namespace storm { initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") "); STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean"); } + if(transientVar) { + labels.insert(name); + } return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar); } - return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), transientVar); + assert(!transientVar); + return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName)); } else if(variableStructure.at("type") == "int") { if(initvalcount == 1) { if(variableStructure.at("initial-value").is_null()) { @@ -316,14 +662,14 @@ namespace storm { STORM_LOG_THROW(expected == actual, storm::exceptions::InvalidJaniException, "Operator " << opstring << " expects " << expected << " arguments, but got " << actual << " in " << errorInfo << "."); } - std::vector<storm::expressions::Expression> JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars); + std::vector<storm::expressions::Expression> JaniParser::parseUnaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("exp"), "Argument of operator " + opstring + " in " + scopeDescription, localVars,returnNoneInitializedOnUnknownOperator); return {left}; } - std::vector<storm::expressions::Expression> JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) { - storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars); - storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, localVars); + std::vector<storm::expressions::Expression> JaniParser::parseBinaryExpressionArguments(json const& expressionDecl, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) { + storm::expressions::Expression left = parseExpression(expressionDecl.at("left"), "Left argument of operator " + opstring + " in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); + storm::expressions::Expression right = parseExpression(expressionDecl.at("right"), "Right argument of operator " + opstring + " in " + scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); return {left, right}; } /** @@ -359,7 +705,7 @@ namespace storm { } } - storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars) { + storm::expressions::Expression JaniParser::parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars, bool returnNoneInitializedOnUnknownOperator) { if(expressionStructure.is_boolean()) { if(expressionStructure.get<bool>()) { return expressionManager->boolean(true); @@ -382,31 +728,50 @@ namespace storm { if(expressionStructure.count("op") == 1) { std::string opstring = getString(expressionStructure.at("op"), scopeDescription); std::vector<storm::expressions::Expression> arguments = {}; - if(opstring == "?:") { + if(opstring == "ite") { + STORM_LOG_THROW(expressionStructure.count("if") == 1, storm::exceptions::InvalidJaniException, "If operator required"); + STORM_LOG_THROW(expressionStructure.count("else") == 1, storm::exceptions::InvalidJaniException, "Else operator required"); + STORM_LOG_THROW(expressionStructure.count("then") == 1, storm::exceptions::InvalidJaniException, "If operator required"); + arguments.push_back(parseExpression(expressionStructure.at("if"), "if-formula in " + scopeDescription)); + arguments.push_back(parseExpression(expressionStructure.at("then"), "then-formula in " + scopeDescription)); + arguments.push_back(parseExpression(expressionStructure.at("else"), "else-formula in " + scopeDescription)); ensureNumberOfArguments(3, arguments.size(), opstring, scopeDescription); assert(arguments.size() == 3); + ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return storm::expressions::ite(arguments[0], arguments[1], arguments[2]); } else if (opstring == "∨") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] || arguments[1]; } else if (opstring == "∧") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return arguments[0] && arguments[1]; } else if (opstring == "⇒") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); - ensureBooleanType(arguments[0], opstring, 1, scopeDescription); + ensureBooleanType(arguments[1], opstring, 1, scopeDescription); return (!arguments[0]) || arguments[1]; } else if (opstring == "¬") { - arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 1); + if(!arguments[0].isInitialized()) { + return storm::expressions::Expression(); + } ensureBooleanType(arguments[0], opstring, 0, scopeDescription); return !arguments[0]; } else if (opstring == "=") { @@ -430,26 +795,38 @@ namespace storm { return arguments[0] != arguments[1]; } } else if (opstring == "<") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] < arguments[1]; } else if (opstring == "≤") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] <= arguments[1]; } else if (opstring == ">") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] > arguments[1]; } else if (opstring == "≥") { - arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars); + arguments = parseBinaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars, returnNoneInitializedOnUnknownOperator); assert(arguments.size() == 2); + if(!arguments[0].isInitialized() || !arguments[1].isInitialized()) { + return storm::expressions::Expression(); + } ensureNumericalType(arguments[0], opstring, 0, scopeDescription); ensureNumericalType(arguments[1], opstring, 1, scopeDescription); return arguments[0] >= arguments[1]; @@ -551,6 +928,9 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Opstring " + opstring + " is not supported by storm"); } else { + if(returnNoneInitializedOnUnknownOperator) { + return storm::expressions::Expression(); + } STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in " << scopeDescription << "."); } } @@ -677,16 +1057,18 @@ namespace storm { std::vector<storm::jani::Assignment> assignments; unsigned assignmentDeclCount = destEntry.count("assignments"); STORM_LOG_THROW(assignmentDeclCount < 2, storm::exceptions::InvalidJaniException, "Destination in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' has multiple assignment lists"); - for(auto const& assignmentEntry : destEntry.at("assignments")) { - // ref - STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one ref field"); - std::string refstring = getString(assignmentEntry.at("ref"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); - storm::jani::Variable const& lhs = getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); - // value - STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field"); - storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars); - // TODO check types - assignments.emplace_back(lhs, assignmentExpr); + if (assignmentDeclCount > 0) { + for (auto const& assignmentEntry : destEntry.at("assignments")) { + // ref + STORM_LOG_THROW(assignmentEntry.count("ref") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one ref field"); + std::string refstring = getString(assignmentEntry.at("ref"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); + storm::jani::Variable const& lhs = getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'"); + // value + STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one value field"); + storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars); + // TODO check types + assignments.emplace_back(lhs, assignmentExpr); + } } edgeDestinations.emplace_back(locIds.at(targetLoc), probExpr, assignments); } @@ -705,7 +1087,7 @@ namespace storm { std::vector<std::string> inputs; for (auto const& syncInput : syncEntry.at("synchronise")) { if(syncInput.is_null()) { - // TODO handle null; + inputs.push_back(storm::jani::SynchronizationVector::NO_ACTION_INPUT); } else { inputs.push_back(syncInput); } diff --git a/src/parser/JaniParser.h b/src/parser/JaniParser.h index 8fa4e8277..438cb93d1 100644 --- a/src/parser/JaniParser.h +++ b/src/parser/JaniParser.h @@ -1,9 +1,11 @@ #pragma once #include <src/storage/jani/Constant.h> -#include <src/logic/Formula.h> +#include "src/logic/Formula.h" +#include "src/logic/Bound.h" #include "src/exceptions/FileIoException.h" #include "src/storage/expressions/ExpressionManager.h" + // JSON parser #include "json.hpp" @@ -16,6 +18,11 @@ namespace storm { class Variable; class Composition; class Property; + class PropertyInterval; + } + + namespace logic { + enum class FormulaContext; } @@ -33,16 +40,16 @@ namespace storm { JaniParser() : expressionManager(new storm::expressions::ExpressionManager()) {} JaniParser(std::string const& jsonstring); - static std::pair<storm::jani::Model, PropertyVector> parse(std::string const& path); + static std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parse(std::string const& path); protected: void readFile(std::string const& path); - std::pair<storm::jani::Model, PropertyVector> parseModel(bool parseProperties = true); + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseModel(bool parseProperties = true); storm::jani::Property parseProperty(json const& propertyStructure); storm::jani::Automaton parseAutomaton(json const& automatonStructure, storm::jani::Model const& parentModel); std::shared_ptr<storm::jani::Variable> parseVariable(json const& variableStructure, std::string const& scopeDescription, bool prefWithScope = false); - storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>()); + storm::expressions::Expression parseExpression(json const& expressionStructure, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), bool returnNoneOnUnknownOpString = false); private: std::shared_ptr<storm::jani::Constant> parseConstant(json const& constantStructure, std::string const& scopeDescription = "global"); @@ -51,13 +58,19 @@ namespace storm { * Helper for parsing the actions of a model. */ void parseActions(json const& actionStructure, storm::jani::Model& parentModel); - std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}); - std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}); - + std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound = boost::none); + std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}, bool returnNoneOnUnknownOpString = false); + + std::vector<std::shared_ptr<storm::logic::Formula const>> parseUnaryFormulaArgument(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context); + std::vector<std::shared_ptr<storm::logic::Formula const>> parseBinaryFormulaArguments(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& opstring, std::string const& context); + storm::jani::PropertyInterval parsePropertyInterval(json const& piStructure); + + std::shared_ptr<storm::jani::Composition> parseComposition(json const& compositionStructure); storm::expressions::Variable getVariableOrConstantExpression(std::string const& ident, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = {}); - + /** * The overall structure currently under inspection. */ @@ -66,6 +79,8 @@ namespace storm { * The expression manager to be used. */ std::shared_ptr<storm::expressions::ExpressionManager> expressionManager; + + std::set<std::string> labels = {}; bool allowRecursion = true; diff --git a/src/parser/KeyValueParser.cpp b/src/parser/KeyValueParser.cpp new file mode 100644 index 000000000..594c8547b --- /dev/null +++ b/src/parser/KeyValueParser.cpp @@ -0,0 +1,32 @@ +#include "KeyValueParser.h" +#include <boost/algorithm/string.hpp> +#include <vector> + +#include "src/utility/macros.h" +#include "src/exceptions/InvalidArgumentException.h" + +namespace storm { + namespace parser { + + std::unordered_map<std::string, std::string> parseKeyValueString(std::string const& keyValueString) { + std::unordered_map<std::string, std::string> keyValueMap; + std::vector<std::string> definitions; + boost::split(definitions, keyValueString, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + + // Check whether the token could be a legal constant definition. + std::size_t positionOfAssignmentOperator = definition.find('='); + STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::InvalidArgumentException, "Illegal key value string: syntax error."); + + // Now extract the variable name and the value from the string. + std::string key = definition.substr(0, positionOfAssignmentOperator); + boost::trim(key); + std::string value = definition.substr(positionOfAssignmentOperator + 1); + boost::trim(value); + keyValueMap.emplace(key, value); + } + return keyValueMap; + } + } +} \ No newline at end of file diff --git a/src/parser/KeyValueParser.h b/src/parser/KeyValueParser.h new file mode 100644 index 000000000..b3005daa5 --- /dev/null +++ b/src/parser/KeyValueParser.h @@ -0,0 +1,11 @@ +#pragma once + +#include <string> +#include <unordered_map> + + +namespace storm { + namespace parser { + std::unordered_map<std::string, std::string> parseKeyValueString(std::string const& keyValueString); + } +} \ No newline at end of file diff --git a/src/settings/modules/IOSettings.cpp b/src/settings/modules/IOSettings.cpp index c174f1f51..84d9b1238 100644 --- a/src/settings/modules/IOSettings.cpp +++ b/src/settings/modules/IOSettings.cpp @@ -7,6 +7,7 @@ #include "src/settings/ArgumentBuilder.h" #include "src/settings/Argument.h" #include "src/exceptions/InvalidSettingsException.h" +#include "src/parser/CSVParser.h" namespace storm { namespace settings { @@ -14,7 +15,7 @@ namespace storm { const std::string IOSettings::moduleName = "io"; const std::string IOSettings::exportDotOptionName = "exportdot"; - const std::string IOSettings::exportMatOptionName = "exportmat"; + const std::string IOSettings::exportExplicitOptionName = "exportexplicit"; const std::string IOSettings::explicitOptionName = "explicit"; const std::string IOSettings::explicitOptionShortName = "exp"; const std::string IOSettings::prismInputOptionName = "prism"; @@ -29,12 +30,17 @@ namespace storm { const std::string IOSettings::constantsOptionShortName = "const"; const std::string IOSettings::prismCompatibilityOptionName = "prismcompat"; const std::string IOSettings::prismCompatibilityOptionShortName = "pc"; + const std::string IOSettings::noBuildOptionName = "nobuild"; + const std::string IOSettings::fullModelBuildOptionName = "buildfull"; + const std::string IOSettings::janiPropertyOptionName = "janiproperty"; + const std::string IOSettings::janiPropertyOptionShortName = "jprop"; + IOSettings::IOSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, prismCompatibilityOptionName, false, "Enables PRISM compatibility. This may be necessary to process some PRISM models.").setShortName(prismCompatibilityOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, "", "If given, the loaded model will be written to the specified file in the dot format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exportMatOptionName, "", "If given, the loaded model will be written to the specified file in the mat format.") + this->addOption(storm::settings::OptionBuilder(moduleName, exportExplicitOptionName, "", "If given, the loaded model will be written to the specified file in the drn format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "the name of the file to which the model is to be writen.").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, explicitOptionName, false, "Parses the model given in an explicit (sparse) representation.").setShortName(explicitOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("transition filename", "The name of the file from which to read the transitions.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) @@ -44,6 +50,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, janiInputOptionName, false, "Parses the model given in the JANI format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the JANI input.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, prismToJaniOptionName, false, "If set, the input PRISM model is transformed to JANI.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, fullModelBuildOptionName, false, "If set, include all rewards and labels.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, noBuildOptionName, false, "If set, do not build the model.").build()); std::vector<std::string> explorationOrders = {"dfs", "bfs"}; this->addOption(storm::settings::OptionBuilder(moduleName, explorationOrderOptionName, false, "Sets which exploration order to use.").setShortName(explorationOrderOptionShortName) @@ -57,6 +65,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the choice labels.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, constantsOptionName, false, "Specifies the constant replacements to use in symbolic models. Note that this requires the model to be given as an symbolic model (i.e., via --" + prismInputOptionName + " or --" + janiInputOptionName + ").").setShortName(constantsOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of constants and their value, e.g. a=1,b=2,c=3.").setDefaultValueString("").build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, janiPropertyOptionName, false, "Specifies the properties from the jani model (given by --" + janiInputOptionName + ") to be checked.").setShortName(janiPropertyOptionShortName) + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of properties to be checked").setDefaultValueString("").build()).build()); } bool IOSettings::isExportDotSet() const { @@ -66,6 +76,14 @@ namespace storm { std::string IOSettings::getExportDotFilename() const { return this->getOption(exportDotOptionName).getArgumentByName("filename").getValueAsString(); } + + bool IOSettings::isExportExplicitSet() const { + return this->getOption(exportExplicitOptionName).getHasOptionBeenSet(); + } + + std::string IOSettings::getExportExplicitFilename() const { + return this->getOption(exportExplicitOptionName).getArgumentByName("filename").getValueAsString(); + } bool IOSettings::isExplicitSet() const { return this->getOption(explicitOptionName).getHasOptionBeenSet(); @@ -153,9 +171,26 @@ namespace storm { return this->getOption(constantsOptionName).getArgumentByName("values").getValueAsString(); } + bool IOSettings::isJaniPropertiesSet() const { + return this->getOption(janiPropertyOptionName).getHasOptionBeenSet(); + } + + std::vector<std::string> IOSettings::getJaniProperties() const { + return storm::parser::parseCommaSeperatedValues(this->getOption(janiPropertyOptionName).getArgumentByName("values").getValueAsString()); + } + + bool IOSettings::isPrismCompatibilityEnabled() const { return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); } + + bool IOSettings::isBuildFullModelSet() const { + return this->getOption(fullModelBuildOptionName).getHasOptionBeenSet(); + } + + bool IOSettings::isNoBuildModelSet() const { + return this->getOption(noBuildOptionName).getHasOptionBeenSet(); + } void IOSettings::finalize() { } diff --git a/src/settings/modules/IOSettings.h b/src/settings/modules/IOSettings.h index ae6ce6831..d2c2bef58 100644 --- a/src/settings/modules/IOSettings.h +++ b/src/settings/modules/IOSettings.h @@ -35,6 +35,22 @@ namespace storm { */ std::string getExportDotFilename() const; + + /*! + * Retrieves whether the export-to-explicit option was set + * + * @return True if the export-to-explicit option was set + */ + bool isExportExplicitSet() const; + + + /*! + * Retrieves thename in which to write the model in explicit format, if the option was set. + * + * @return The name of the file in which to write the exported mode. + */ + std::string getExportExplicitFilename() const; + /*! * Retrieves whether the explicit option was set. * @@ -183,6 +199,10 @@ namespace storm { * @return The string that defines the constants of a symbolic model. */ std::string getConstantDefinitionString() const; + + bool isJaniPropertiesSet() const; + + std::vector<std::string> getJaniProperties() const; /*! * Retrieves whether the PRISM compatibility mode was enabled. @@ -190,6 +210,18 @@ namespace storm { * @return True iff the PRISM compatibility mode was enabled. */ bool isPrismCompatibilityEnabled() const; + + /** + * Retrieves whether no model should be build at all, in case one just want to translate models or parse a file + */ + bool isNoBuildModelSet() const; + + /*! + * Retrieves whether the full model should be build, that is, the model including all labels and rewards. + * + * @return true iff the full model should be build. + */ + bool isBuildFullModelSet() const; bool check() const override; void finalize() override; @@ -200,7 +232,7 @@ namespace storm { private: // Define the string names of the options as constants. static const std::string exportDotOptionName; - static const std::string exportMatOptionName; + static const std::string exportExplicitOptionName; static const std::string explicitOptionName; static const std::string explicitOptionShortName; static const std::string prismInputOptionName; @@ -215,6 +247,10 @@ namespace storm { static const std::string constantsOptionShortName; static const std::string prismCompatibilityOptionName; static const std::string prismCompatibilityOptionShortName; + static const std::string fullModelBuildOptionName; + static const std::string noBuildOptionName; + static const std::string janiPropertyOptionName; + static const std::string janiPropertyOptionShortName; }; } // namespace modules diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp index 4c144eff8..62440992d 100644 --- a/src/storage/SymbolicModelDescription.cpp +++ b/src/storage/SymbolicModelDescription.cpp @@ -57,6 +57,20 @@ namespace storm { return boost::get<storm::prism::Program>(modelDescription.get()); } + std::vector<std::string> SymbolicModelDescription::getParameterNames() const { + std::vector<std::string> result; + if(isJaniModel()) { + for(auto const& c : asJaniModel().getUndefinedConstants()) { + result.push_back(c.get().getName()); + } + } else { + for(auto const& c : asPrismProgram().getUndefinedConstants()) { + result.push_back(c.get().getName()); + } + } + return result; + } + SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const { if (this->isJaniModel()) { return *this; diff --git a/src/storage/SymbolicModelDescription.h b/src/storage/SymbolicModelDescription.h index 8b5b85d88..730578ac4 100644 --- a/src/storage/SymbolicModelDescription.h +++ b/src/storage/SymbolicModelDescription.h @@ -27,6 +27,8 @@ namespace storm { storm::jani::Model const& asJaniModel() const; storm::prism::Program const& asPrismProgram() const; + std::vector<std::string> getParameterNames() const; + SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const; SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const; diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp index cfd43923b..2c57a65ed 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.cpp +++ b/src/storage/bisimulation/BisimulationDecomposition.cpp @@ -231,7 +231,7 @@ namespace storm { template<typename ModelType, typename BlockDataType> void BisimulationDecomposition<ModelType, BlockDataType>::performPartitionRefinement() { // Insert all blocks into the splitter queue as a (potential) splitter. - std::deque<Block<BlockDataType>*> splitterQueue; + std::vector<Block<BlockDataType>*> splitterQueue; std::for_each(partition.getBlocks().begin(), partition.getBlocks().end(), [&] (std::unique_ptr<Block<BlockDataType>> const& block) { block->data().setSplitter(); splitterQueue.push_back(block.get()); } ); // Then perform the actual splitting until there are no more splitters. @@ -242,9 +242,9 @@ namespace storm { // Get and prepare the next splitter. // Sort the splitters according to their sizes to prefer small splitters. That is just a heuristic, but // tends to work well. - std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() < b2->getNumberOfStates(); } ); - Block<BlockDataType>* splitter = splitterQueue.front(); - splitterQueue.pop_front(); + std::sort(splitterQueue.begin(), splitterQueue.end(), [] (Block<BlockDataType> const* b1, Block<BlockDataType> const* b2) { return b1->getNumberOfStates() > b2->getNumberOfStates(); } ); + Block<BlockDataType>* splitter = splitterQueue.back(); + splitterQueue.pop_back(); splitter->data().setSplitter(false); // Now refine the partition using the current splitter. diff --git a/src/storage/bisimulation/BisimulationDecomposition.h b/src/storage/bisimulation/BisimulationDecomposition.h index 6507e3b07..e3322444c 100644 --- a/src/storage/bisimulation/BisimulationDecomposition.h +++ b/src/storage/bisimulation/BisimulationDecomposition.h @@ -1,8 +1,6 @@ #ifndef STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ #define STORM_STORAGE_BISIMULATIONDECOMPOSITION_H_ -#include <deque> - #include "src/settings/SettingsManager.h" #include "src/settings/modules/BisimulationSettings.h" #include "src/storage/sparse/StateType.h" @@ -224,7 +222,7 @@ namespace storm { * @param splitter The splitter to use. * @param splitterQueue The queue into which to insert the newly discovered potential splitters. */ - virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) = 0; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) = 0; /*! * Builds the quotient model based on the previously computed equivalence classes (stored in the blocks diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp index 0b0574737..b030b7cee 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp @@ -157,7 +157,7 @@ namespace storm { } template<typename ModelType> - void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterStrong(std::list<Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterStrong(std::list<Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) { for (auto block : predecessorBlocks) { STORM_LOG_TRACE("Refining predecessor " << block->getId() << " of splitter"); @@ -378,7 +378,7 @@ namespace storm { } template<typename ModelType> - void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) { // First, we need to turn the one-step probabilities to go to the splitter to the conditional probabilities // for all non-silent states. computeConditionalProbabilitiesForNonSilentStates(block); @@ -416,7 +416,7 @@ namespace storm { } template<typename ModelType> - void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition<ModelType>::refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) { for (auto block : predecessorBlocks) { if (*block != splitter) { refinePredecessorBlockOfSplitterWeak(*block, splitterQueue); @@ -439,7 +439,7 @@ namespace storm { } template<typename ModelType> - void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) { + void DeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) { STORM_LOG_TRACE("Refining partition based on splitter " << splitter.getId()); // The outline of the refinement is as follows. diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h index b9f2a2a5a..b4db574cb 100644 --- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.h @@ -39,11 +39,11 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) override; private: // Refines the predecessor blocks wrt. strong bisimulation. - void refinePredecessorBlocksOfSplitterStrong(std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue); + void refinePredecessorBlocksOfSplitterStrong(std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue); /*! * Performs the necessary steps to compute a weak bisimulation on a DTMC. @@ -99,10 +99,10 @@ namespace storm { void updateSilentProbabilitiesBasedOnTransitions(bisimulation::Block<BlockDataType>& block); // Refines the predecessor blocks of the splitter wrt. weak bisimulation in DTMCs. - void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue); + void refinePredecessorBlocksOfSplitterWeak(bisimulation::Block<BlockDataType>& splitter, std::list<bisimulation::Block<BlockDataType>*> const& predecessorBlocks, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue); // Refines the given block wrt to weak bisimulation in DTMCs. - void refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue); + void refinePredecessorBlockOfSplitterWeak(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue); // Converts the one-step probabilities of going into the splitter into the conditional probabilities needed // for weak bisimulation (on DTMCs). @@ -127,4 +127,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_BISIMULATION_DETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp index 547d4dc29..1a82e5976 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp @@ -198,7 +198,7 @@ namespace storm { } template<typename ModelType> - void NondeterministicModelBisimulationDecomposition<ModelType>::updateQuotientDistributionsOfPredecessors(Block<BlockDataType> const& newBlock, Block<BlockDataType> const& oldBlock, std::deque<Block<BlockDataType>*>& splitterQueue) { + void NondeterministicModelBisimulationDecomposition<ModelType>::updateQuotientDistributionsOfPredecessors(Block<BlockDataType> const& newBlock, Block<BlockDataType> const& oldBlock, std::vector<Block<BlockDataType>*>& splitterQueue) { uint_fast64_t lastState = 0; bool lastStateInitialized = false; @@ -332,36 +332,23 @@ namespace storm { } template<typename ModelType> - bool NondeterministicModelBisimulationDecomposition<ModelType>::splitBlockAccordingToCurrentQuotientDistributions(Block<BlockDataType>& block, std::deque<Block<BlockDataType>*>& splitterQueue) { + bool NondeterministicModelBisimulationDecomposition<ModelType>::splitBlockAccordingToCurrentQuotientDistributions(Block<BlockDataType>& block, std::vector<Block<BlockDataType>*>& splitterQueue) { std::list<Block<BlockDataType>*> newBlocks; bool split = this->partition.splitBlock(block, [this] (storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) { bool result = quotientDistributionsLess(state1, state2); -// std::cout << state1 << " is " << (!result ? "not" : "") << " smaller than " << state2 << std::endl; return result; }, [this, &block, &splitterQueue, &newBlocks] (Block<BlockDataType>& newBlock) { newBlocks.push_back(&newBlock); - -// this->checkBlockStable(newBlock); -// this->checkDistributionsDifferent(block, block.getEndIndex()); -// this->checkQuotientDistributions(); }); - // The quotient distributions of the predecessors of block do not need to be updated, since the probability - // will go to the block with the same id as before. - -// std::cout << "partition after split: " << std::endl; -// this->partition.print(); - - // defer updating the quotient distributions until *after* all splits, because + // Defer updating the quotient distributions until *after* all splits, because // it otherwise influences the subsequent splits! for (auto el : newBlocks) { this->updateQuotientDistributionsOfPredecessors(*el, block, splitterQueue); } -// this->checkQuotientDistributions(); - return split; } @@ -369,11 +356,6 @@ namespace storm { bool NondeterministicModelBisimulationDecomposition<ModelType>::quotientDistributionsLess(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) const { STORM_LOG_TRACE("Comparing the quotient distributions of state " << state1 << " and " << state2 << "."); std::vector<uint_fast64_t> nondeterministicChoiceIndices = this->model.getTransitionMatrix().getRowGroupIndices(); - -// std::cout << "distributions of state " << state1 << std::endl; -// this->printDistributions(state1); -// std::cout << "distributions of state " << state2 << std::endl; -// this->printDistributions(state2); auto firstIt = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1]; auto firstIte = orderedQuotientDistributions.begin() + nondeterministicChoiceIndices[state1 + 1]; @@ -405,7 +387,7 @@ namespace storm { } template<typename ModelType> - void NondeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) { + void NondeterministicModelBisimulationDecomposition<ModelType>::refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) { if (!possiblyNeedsRefinement(splitter)) { return; } diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h index 18a6e8e58..6c25d6cf9 100644 --- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h +++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.h @@ -37,7 +37,7 @@ namespace storm { virtual void buildQuotient() override; - virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue) override; + virtual void refinePartitionBasedOnSplitter(bisimulation::Block<BlockDataType>& splitter, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue) override; virtual void initialize() override; @@ -52,7 +52,7 @@ namespace storm { bool possiblyNeedsRefinement(bisimulation::Block<BlockDataType> const& block) const; // Splits the given block according to the current quotient distributions. - bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block<BlockDataType>& block, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue); + bool splitBlockAccordingToCurrentQuotientDistributions(bisimulation::Block<BlockDataType>& block, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue); // Retrieves whether the quotient distributions of state 1 are considered to be less than the ones of state 2. bool quotientDistributionsLess(storm::storage::sparse::state_type state1, storm::storage::sparse::state_type state2) const; @@ -62,7 +62,7 @@ namespace storm { // Updates the quotient distributions of the predecessors of the new block by taking the probability mass // away from the old block. - void updateQuotientDistributionsOfPredecessors(bisimulation::Block<BlockDataType> const& newBlock, bisimulation::Block<BlockDataType> const& oldBlock, std::deque<bisimulation::Block<BlockDataType>*>& splitterQueue); + void updateQuotientDistributionsOfPredecessors(bisimulation::Block<BlockDataType> const& newBlock, bisimulation::Block<BlockDataType> const& oldBlock, std::vector<bisimulation::Block<BlockDataType>*>& splitterQueue); bool checkQuotientDistributions() const; bool checkBlockStable(bisimulation::Block<BlockDataType> const& newBlock) const; @@ -81,4 +81,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_BISIMULATION_NONDETERMINISTICMODELBISIMULATIONDECOMPOSITION_H_ */ diff --git a/src/storage/expressions/ExpressionVisitor.h b/src/storage/expressions/ExpressionVisitor.h index cfe2ce9b6..edbdc5d5a 100644 --- a/src/storage/expressions/ExpressionVisitor.h +++ b/src/storage/expressions/ExpressionVisitor.h @@ -2,6 +2,7 @@ #define STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_ #include <boost/any.hpp> +#include <boost/none.hpp> namespace storm { namespace expressions { @@ -33,4 +34,4 @@ namespace storm { } } -#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_ */ \ No newline at end of file +#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONVISITOR_H_ */ diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 8e99f25c1..8ed71acbc 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -335,7 +335,14 @@ namespace storm { } bool Automaton::hasRestrictedInitialStates() const { - return hasInitialStatesRestriction() && !(getInitialStatesExpression().evaluateAsBool()); + if (!hasInitialStatesRestriction()) { + return false; + } + if (getInitialStatesExpression().containsVariables()) { + return true; + } else { + return !getInitialStatesExpression().evaluateAsBool(); + } } bool Automaton::hasInitialStatesRestriction() const { diff --git a/src/storage/jani/BooleanVariable.cpp b/src/storage/jani/BooleanVariable.cpp index 3eb63780b..ca2934f93 100644 --- a/src/storage/jani/BooleanVariable.cpp +++ b/src/storage/jani/BooleanVariable.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) { + BooleanVariable::BooleanVariable(std::string const& name, storm::expressions::Variable const& variable) : Variable(name, variable) { // Intentionally left empty. } @@ -19,7 +19,8 @@ namespace storm { if (initValue) { return std::make_shared<BooleanVariable>(name, variable, initValue.get(), transient); } else { - return std::make_shared<BooleanVariable>(name, variable, transient); + assert(!transient); + return std::make_shared<BooleanVariable>(name, variable); } } diff --git a/src/storage/jani/BooleanVariable.h b/src/storage/jani/BooleanVariable.h index 7fe9603e0..7eeea85fd 100644 --- a/src/storage/jani/BooleanVariable.h +++ b/src/storage/jani/BooleanVariable.h @@ -11,7 +11,7 @@ namespace storm { /*! * Creates a Boolean variable with initial value */ - BooleanVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); + BooleanVariable(std::string const& name, storm::expressions::Variable const& variable); /*! * Creates a Boolean variable with initial value diff --git a/src/storage/jani/BoundedIntegerVariable.cpp b/src/storage/jani/BoundedIntegerVariable.cpp index 37b458ba4..1d04c8166 100644 --- a/src/storage/jani/BoundedIntegerVariable.cpp +++ b/src/storage/jani/BoundedIntegerVariable.cpp @@ -13,11 +13,7 @@ namespace storm { // Intentionally left empty. } - BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable, transient), lowerBound(lowerBound), upperBound(upperBound) { - // Intentionally left empty. - } - - BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) { + BoundedIntegerVariable::BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound) : Variable(name, variable), lowerBound(lowerBound), upperBound(upperBound) { // Intentionally left empty. } @@ -56,7 +52,8 @@ namespace storm { if (initValue) { return std::make_shared<BoundedIntegerVariable>(name, variable, initValue.get(), transient, lowerBound.get(), upperBound.get()); } else { - return std::make_shared<BoundedIntegerVariable>(name, variable, transient, lowerBound.get(), upperBound.get()); + assert(!transient); + return std::make_shared<BoundedIntegerVariable>(name, variable, lowerBound.get(), upperBound.get()); } } } diff --git a/src/storage/jani/BoundedIntegerVariable.h b/src/storage/jani/BoundedIntegerVariable.h index 733024b3d..9b5350d0e 100644 --- a/src/storage/jani/BoundedIntegerVariable.h +++ b/src/storage/jani/BoundedIntegerVariable.h @@ -16,10 +16,6 @@ namespace storm { * Creates a bounded integer variable with transient set to false and an initial value. */ BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, storm::expressions::Expression const& initValue, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); - /*! - * Creates a bounded integer variable without initial value. - */ - BoundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient, storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound); /*! * Creates a bounded integer variable with transient set to false and no initial value. */ diff --git a/src/storage/jani/JSONExporter.cpp b/src/storage/jani/JSONExporter.cpp index 3493affe4..13512f554 100644 --- a/src/storage/jani/JSONExporter.cpp +++ b/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 { @@ -55,11 +60,7 @@ namespace storm { for (auto const& subcomp : composition.getSubcompositions()) { modernjson::json elemDecl; if (subcomp->isAutomaton()) { - modernjson::json autDecl; - autDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName(); - std::vector<modernjson::json> elements; - elements.push_back(autDecl); - elemDecl["elements"] = elements; + elemDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName(); } else { STORM_LOG_THROW(allowRecursion, storm::exceptions::InvalidJaniException, "Nesting composition " << *subcomp << " is not supported by JANI."); elemDecl = boost::any_cast<modernjson::json>(subcomp->accept(*this, boost::none)); @@ -70,7 +71,14 @@ namespace storm { std::vector<modernjson::json> synElems; for (auto const& syncs : composition.getSynchronizationVectors()) { modernjson::json syncDecl; - syncDecl["synchronise"] = syncs.getInput(); + syncDecl["synchronise"] = std::vector<std::string>(); + for (auto const& syncIn : syncs.getInput()) { + if (syncIn == SynchronizationVector::NO_ACTION_INPUT) { + syncDecl["synchronise"].push_back(nullptr); + } else { + syncDecl["synchronise"].push_back(syncIn); + } + } syncDecl["result"] = syncs.getOutput(); synElems.push_back(syncDecl); } @@ -85,6 +93,295 @@ 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; + numDecl = storm::utility::convertNumber<double>(rn); +// if(carl::isOne(carl::getDenom(rn))) { +// numDecl = modernjson::json(carl::toString(carl::getNum(rn))); +// } else { +// numDecl["op"] = "/"; +// // TODO set json lib to work with arbitrary precision ints. +// assert(carl::toInt<int64_t>(carl::getNum(rn)) == carl::getNum(rn)); +// assert(carl::toInt<int64_t>(carl::getDenom(rn)) == carl::getDenom(rn)); +// numDecl["left"] = carl::toInt<int64_t>(carl::getNum(rn)); +// numDecl["right"] = carl::toInt<int64_t>(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.getLabel()); + 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 { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm currently does not support translating cummulative reward formulae"); + } + + 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; + + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Jani currently does not support conversion of an LRA reward formula"); + } + + 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 +502,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; } @@ -396,10 +694,63 @@ namespace storm { jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction()); jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap()); jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition()); + std::vector<std::string> standardFeatureVector = {"derived-operators"}; + jsonStruct["features"] = standardFeatureVector; } + + std::string janiFilterTypeString(storm::modelchecker::FilterType const& ft) { + switch(ft) { + case storm::modelchecker::FilterType::MIN: + return "min"; + case storm::modelchecker::FilterType::MAX: + return "max"; + case storm::modelchecker::FilterType::SUM: + return "sum"; + case storm::modelchecker::FilterType::AVG: + return "avg"; + case storm::modelchecker::FilterType::COUNT: + return "count"; + case storm::modelchecker::FilterType::EXISTS: + return "∃"; + case storm::modelchecker::FilterType::FORALL: + return "∀"; + case storm::modelchecker::FilterType::ARGMIN: + return "argmin"; + case storm::modelchecker::FilterType::ARGMAX: + return "argmax"; + case storm::modelchecker::FilterType::VALUES: + return "values"; + + } + } + + modernjson::json convertFilterExpression(storm::jani::FilterExpression const& fe, bool continuousModel) { + modernjson::json propDecl; + propDecl["states"]["op"] = "initial"; + propDecl["op"] = "filter"; + 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; + } + + } } diff --git a/src/storage/jani/JSONExporter.h b/src/storage/jani/JSONExporter.h index 604a27a47..2159c26c5 100644 --- a/src/storage/jani/JSONExporter.h +++ b/src/storage/jani/JSONExporter.h @@ -2,10 +2,14 @@ #include "src/storage/expressions/ExpressionVisitor.h" +#include "src/logic/FormulaVisitor.h" #include "Model.h" +#include "src/adapters/NumberAdapter.h" // JSON parser #include "json.hpp" -namespace modernjson = nlohmann; +namespace modernjson { + using json = nlohmann::basic_json<std::map, std::vector, std::string, bool, int64_t, uint64_t, double, std::allocator>; +}; namespace storm { namespace jani { @@ -28,15 +32,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() { diff --git a/src/storage/jani/Property.cpp b/src/storage/jani/Property.cpp index 9b097757d..3e4243a3d 100644 --- a/src/storage/jani/Property.cpp +++ b/src/storage/jani/Property.cpp @@ -1,10 +1,23 @@ #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) + + + + std::ostream& operator<<(std::ostream& os, FilterExpression const& fe) { + return os << "Obtain " << toString(fe.getFilterType()) << " the 'initial'-states with values described by '" << *fe.getFormula() << "'"; + } + + Property::Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment) + : name(name), comment(comment), filterExpression(FilterExpression(formula)) { + } + + Property::Property(std::string const& name, FilterExpression const& fe, std::string const& comment) + : name(name), comment(comment), filterExpression(fe) + { + } std::string const& Property::getName() const { @@ -14,10 +27,15 @@ 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; + + FilterExpression const& Property::getFilter() const { + return this->filterExpression; + } + + std::ostream& operator<<(std::ostream& os, Property const& p) { + return os << "(" << p.getName() << ") : " << p.getFilter(); } + } } \ No newline at end of file diff --git a/src/storage/jani/Property.h b/src/storage/jani/Property.h index 30bddac60..d4baa9d94 100644 --- a/src/storage/jani/Property.h +++ b/src/storage/jani/Property.h @@ -1,10 +1,56 @@ #pragma once -#include "src/logic/formulas.h" +#include "src/modelchecker/results/FilterType.h" +#include "src/logic/Formulas.h" namespace storm { namespace jani { + + /** + * Property intervals as per Jani Specification. + * Currently mainly used to help parsing. + */ + struct PropertyInterval { + storm::expressions::Expression lowerBound; + bool lowerBoundStrict = false; + storm::expressions::Expression upperBound; + bool upperBoundStrict = false; + + bool hasLowerBound() { + return lowerBound.isInitialized(); + } + + bool hasUpperBound() { + return upperBound.isInitialized(); + } + }; + + + class FilterExpression { + public: + explicit FilterExpression(std::shared_ptr<storm::logic::Formula const> formula, storm::modelchecker::FilterType ft = storm::modelchecker::FilterType::VALUES) : values(formula), ft(ft) {} + + + std::shared_ptr<storm::logic::Formula const> const& getFormula() const { + return values; + } + + storm::modelchecker::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; + storm::modelchecker::FilterType ft; + }; + + + std::ostream& operator<<(std::ostream& os, FilterExpression const& fe); + + + class Property { + public: /** * Constructs the property * @param name the name @@ -12,6 +58,13 @@ namespace storm { * @param comment An optional comment */ Property(std::string const& name, std::shared_ptr<storm::logic::Formula const> const& formula, std::string const& comment = ""); + /** + * Constructs the property + * @param name the name + * @param formula the formula representation + * @param comment An optional comment + */ + Property(std::string const& name, FilterExpression const& fe, std::string const& comment = ""); /** * Get the provided name * @return the name @@ -22,17 +75,16 @@ 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; - + + FilterExpression const& getFilter() const; private: std::string name; - std::shared_ptr<storm::logic::Formula const> formula; std::string comment; + FilterExpression filterExpression; }; + + + std::ostream& operator<<(std::ostream& os, Property const& p); } } diff --git a/src/storage/jani/RealVariable.cpp b/src/storage/jani/RealVariable.cpp index 8880a9a0a..f06e87a5c 100644 --- a/src/storage/jani/RealVariable.cpp +++ b/src/storage/jani/RealVariable.cpp @@ -3,7 +3,7 @@ namespace storm { namespace jani { - RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : storm::jani::Variable(name, variable, transient) { + RealVariable::RealVariable(std::string const& name, storm::expressions::Variable const& variable) : storm::jani::Variable(name, variable) { // Intentionally left empty. } diff --git a/src/storage/jani/RealVariable.h b/src/storage/jani/RealVariable.h index 74c337ed9..1783b6fbf 100644 --- a/src/storage/jani/RealVariable.h +++ b/src/storage/jani/RealVariable.h @@ -10,7 +10,7 @@ namespace storm { /*! * Creates a real variable without initial value. */ - RealVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient=false); + RealVariable(std::string const& name, storm::expressions::Variable const& variable); /*! * Creates a real variable with initial value. diff --git a/src/storage/jani/UnboundedIntegerVariable.cpp b/src/storage/jani/UnboundedIntegerVariable.cpp index c646b09b1..6b541054e 100644 --- a/src/storage/jani/UnboundedIntegerVariable.cpp +++ b/src/storage/jani/UnboundedIntegerVariable.cpp @@ -7,7 +7,7 @@ namespace storm { // Intentionally left empty. } - UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable, transient) { + UnboundedIntegerVariable::UnboundedIntegerVariable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : Variable(name, variable) { // Intentionally left empty. } diff --git a/src/storage/jani/Variable.cpp b/src/storage/jani/Variable.cpp index 8551f14df..f2c7217ff 100644 --- a/src/storage/jani/Variable.cpp +++ b/src/storage/jani/Variable.cpp @@ -12,7 +12,7 @@ namespace storm { // Intentionally left empty. } - Variable::Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient) : name(name), variable(variable), transient(transient), init() { + Variable::Variable(std::string const& name, storm::expressions::Variable const& variable) : name(name), variable(variable), transient(false), init() { // Intentionally left empty. } diff --git a/src/storage/jani/Variable.h b/src/storage/jani/Variable.h index cbbe4aa69..2eea79679 100644 --- a/src/storage/jani/Variable.h +++ b/src/storage/jani/Variable.h @@ -25,7 +25,7 @@ namespace storm { /*! * Creates a new variable without initial value construct. */ - Variable(std::string const& name, storm::expressions::Variable const& variable, bool transient = false); + Variable(std::string const& name, storm::expressions::Variable const& variable); virtual ~Variable(); diff --git a/src/storage/ppg/defines.h b/src/storage/ppg/defines.h index 548160ba9..d993e633e 100644 --- a/src/storage/ppg/defines.h +++ b/src/storage/ppg/defines.h @@ -1,6 +1,8 @@ #pragma once #include <cassert> #include <vector> +#include <cstdint> + namespace storm { namespace ppg { class ProgramGraph; diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp index 095ac3e11..0a4347396 100644 --- a/src/storage/prism/Module.cpp +++ b/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)) { diff --git a/src/storage/prism/ToJaniConverter.cpp b/src/storage/prism/ToJaniConverter.cpp index 65289382a..e3bc3c569 100644 --- a/src/storage/prism/ToJaniConverter.cpp +++ b/src/storage/prism/ToJaniConverter.cpp @@ -47,7 +47,7 @@ namespace storm { storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { - storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); + storm::jani::BoundedIntegerVariable const& createdVariable = janiModel.addVariable(storm::jani::BoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.getLowerBoundExpression(), variable.getUpperBoundExpression())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } } @@ -56,7 +56,7 @@ namespace storm { storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), variable.getInitialValueExpression(), false)); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } else { - storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable(), false)); + storm::jani::BooleanVariable const& createdVariable = janiModel.addVariable(storm::jani::BooleanVariable(variable.getName(), variable.getExpressionVariable())); variableToVariableMap.emplace(variable.getExpressionVariable(), createdVariable); } } @@ -100,7 +100,7 @@ namespace storm { std::vector<storm::jani::Assignment> transientLocationAssignments; for (auto const& rewardModel : program.getRewardModels()) { auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName()); - storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName(), newExpressionVariable, true)); + storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "defaultReward" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true)); if (rewardModel.hasStateRewards()) { storm::expressions::Expression transientLocationExpression; diff --git a/src/storm-pgcl.cpp b/src/storm-pgcl.cpp index 99ac1c960..a985e3a7b 100644 --- a/src/storm-pgcl.cpp +++ b/src/storm-pgcl.cpp @@ -37,9 +37,9 @@ void initializeSettings() { void handleJani(storm::jani::Model& model) { if (!storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) { // For now, we have to have a jani file - storm::jani::JsonExporter::toStream(model, std::cout); + storm::jani::JsonExporter::toStream(model, {}, std::cout); } else { - storm::jani::JsonExporter::toFile(model, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); + storm::jani::JsonExporter::toFile(model, {}, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename()); } } diff --git a/src/utility/ExplicitExporter.cpp b/src/utility/ExplicitExporter.cpp new file mode 100644 index 000000000..bf9bcbf29 --- /dev/null +++ b/src/utility/ExplicitExporter.cpp @@ -0,0 +1,138 @@ +#include "ExplicitExporter.h" + +#include "src/adapters/CarlAdapter.h" +#include "src/utility/constants.h" +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" +#include "src/models/sparse/Dtmc.h" +#include "src/models/sparse/Mdp.h" +#include "src/models/sparse/Ctmc.h" +#include "src/models/sparse/MarkovAutomaton.h" + +#include "src/models/sparse/StandardRewardModel.h" + + +namespace storm { + namespace exporter { + template<typename ValueType> + void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters) { + bool embedded = false; + if(sparseModel->getType() == storm::models::ModelType::Ctmc || sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { + STORM_LOG_WARN("This format only supports discrete time models"); + embedded = true; + } + + STORM_LOG_THROW(embedded || sparseModel->getType() == storm::models::ModelType::Mdp || sparseModel->getType() == storm::models::ModelType::Dtmc , storm::exceptions::NotImplementedException, "This functionality is not yet implemented." ); + + std::vector<ValueType> exitRates; // Only for CTMCs and MAs. + if(sparseModel->getType() == storm::models::ModelType::Ctmc) { + exitRates = sparseModel->template as<storm::models::sparse::Ctmc<ValueType>>()->getExitRateVector(); + } else if(sparseModel->getType() == storm::models::ModelType::MarkovAutomaton) { + exitRates = sparseModel->template as<storm::models::sparse::MarkovAutomaton<ValueType>>()->getExitRates(); + } + + os << "// Exported by Storm" << std::endl; + os << "// Original model type: " << sparseModel->getType() << std::endl; + os << "@type: mdp" << std::endl; + os << "@parameters" << std::endl; + for (auto const& p : parameters) { + os << p << " "; + } + os << std::endl; + os << "@nr_states" << std::endl << sparseModel->getNumberOfStates() << std::endl; + os << "@model" << std::endl; + storm::storage::SparseMatrix<ValueType> const& matrix = sparseModel->getTransitionMatrix(); + + for (typename storm::storage::SparseMatrix<ValueType>::index_type group = 0; group < matrix.getRowGroupCount(); ++group) { + os << "state " << group; + + if (!embedded) { + bool first = true; + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; + } + + if(rewardModelEntry.second.hasStateRewards()) { + os << rewardModelEntry.second.getStateRewardVector().at(group); + } else { + os << "0"; + } + } + + if (!first) { + os << "]"; + } + } else { + // We currently only support the expected time. + os << " [" << storm::utility::one<ValueType>()/exitRates.at(group) << "]"; + } + + for(auto const& label : sparseModel->getStateLabeling().getLabelsOfState(group)) { + os << " " << label; + } + os << std::endl; + typename storm::storage::SparseMatrix<ValueType>::index_type start = matrix.hasTrivialRowGrouping() ? group : matrix.getRowGroupIndices()[group]; + typename storm::storage::SparseMatrix<ValueType>::index_type end = matrix.hasTrivialRowGrouping() ? group + 1 : matrix.getRowGroupIndices()[group + 1]; + + + for (typename storm::storage::SparseMatrix<ValueType>::index_type i = start; i < end; ++i) { + // Print the actual row. + os << "\taction " << i - start; + if (!embedded) { + bool first = true; + for (auto const& rewardModelEntry : sparseModel->getRewardModels()) { + if (first) { + os << " ["; + first = false; + } else { + os << ", "; + } + + if(rewardModelEntry.second.hasStateActionRewards()) { + os << storm::utility::to_string(rewardModelEntry.second.getStateActionRewardVector().at(i)); + } else { + os << "0"; + } + + } + if (!first) { + os << "]"; + } + } else { + // We currently only support the expected time. + } + + + + if(sparseModel->hasChoiceLabeling()) { + //TODO + } + os << std::endl; + + + for(auto it = matrix.begin(i); it != matrix.end(i); ++it) { + ValueType prob = it->getValue(); + if(embedded) { + prob = prob / exitRates.at(group); + } + os << "\t\t" << it->getColumn() << " : "; + os << storm::utility::to_string(prob) << std::endl; + } + + } + } + + } + + + + template void explicitExportSparseModel<double>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<double>> sparseModel, std::vector<std::string> const& parameters); + + template void explicitExportSparseModel<storm::RationalNumber>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> sparseModel, std::vector<std::string> const& parameters); + template void explicitExportSparseModel<storm::RationalFunction>(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> sparseModel, std::vector<std::string> const& parameters); + } +} \ No newline at end of file diff --git a/src/utility/ExplicitExporter.h b/src/utility/ExplicitExporter.h new file mode 100644 index 000000000..fd158f001 --- /dev/null +++ b/src/utility/ExplicitExporter.h @@ -0,0 +1,15 @@ +#pragma once +#include <iostream> +#include <memory> + +#include "src/models/sparse/Model.h" + +namespace storm { + namespace exporter { + + template<typename ValueType> + void explicitExportSparseModel(std::ostream& os, std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel, std::vector<std::string> const& parameters); + + + } +} \ No newline at end of file diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index c7ba2142e..2739bfa1f 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -5,7 +5,10 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/exceptions/InvalidArgumentException.h" + #include "src/adapters/CarlAdapter.h" +#include "src/utility/macros.h" namespace storm { namespace utility { @@ -56,7 +59,31 @@ namespace storm { bool isInteger(uint_fast64_t const& number) { return true; } - + + template<typename ValueType> + std::string to_string(ValueType const& value) { + std::stringstream ss; + ss << value; + return ss.str(); + } + + template<> + std::string to_string(RationalFunction const& f) { + std::stringstream ss; + if (f.isConstant()) { + if (f.denominator().isOne()) { + ss << f.nominatorAsNumber(); + } else { + ss << f.nominatorAsNumber() << "/" << f.denominatorAsNumber(); + } + } else if (f.denominator().isOne()) { + ss << f.nominatorAsPolynomial().coefficient() * f.nominatorAsPolynomial().polynomial(); + } else { + ss << "(" << f.nominatorAsPolynomial() << ")/(" << f.denominatorAsPolynomial() << ")"; + } + return ss.str(); + } + #ifdef STORM_HAVE_CARL template<> bool isOne(storm::RationalNumber const& a) { @@ -142,6 +169,80 @@ namespace storm { return std::fabs(number); } + template<> + storm::RationalFunction minimum(std::vector<storm::RationalFunction> const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); + } + + template<typename ValueType> + ValueType minimum(std::vector<ValueType> const& values) { + assert(!values.empty()); + ValueType min = values.front(); + for (auto const& vt : values) { + if (vt < min) { + min = vt; + } + } + return min; + } + + template<> + storm::RationalFunction maximum(std::vector<storm::RationalFunction> const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); + } + + + template<typename ValueType> + ValueType maximum(std::vector<ValueType> const& values) { + assert(!values.empty()); + ValueType max = values.front(); + for (auto const& vt : values) { + if (vt > max) { + max = vt; + } + } + return max; + } + + template<> + storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Minimum for rational functions is not defined"); + } + + template< typename K, typename ValueType> + ValueType minimum(std::map<K, ValueType> const& values) { + assert(!values.empty()); + ValueType min = values.begin()->second; + for (auto const& vt : values) { + if (vt.second < min) { + min = vt.second; + } + } + return min; + } + + template<> + storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const& values) + { + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Maximum for rational functions is not defined"); + } + + + template<typename K, typename ValueType> + ValueType maximum(std::map<K, ValueType> const& values) { + assert(!values.empty()); + ValueType max = values.begin()->second; + for (auto const& vt : values) { + if (vt.second > max) { + max = vt.second; + } + } + return max; + } + #ifdef STORM_HAVE_CARL template<> RationalFunction& simplify(RationalFunction& value); @@ -275,6 +376,11 @@ namespace storm { template bool isInteger(float const& number); template float simplify(float value); + + template std::string to_string(float const& value); + template std::string to_string(double const& value); + template std::string to_string(storm::RationalNumber const& value); + template std::string to_string(storm::RationalFunction const& value); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry); @@ -318,6 +424,24 @@ namespace storm { template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry); template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry); + + template double minimum(std::vector<double> const&); + template double maximum(std::vector<double> const&); + + template storm::RationalNumber minimum(std::vector<storm::RationalNumber> const&); + template storm::RationalNumber maximum(std::vector<storm::RationalNumber> const&); + + template storm::RationalFunction minimum(std::vector<storm::RationalFunction> const&); + template storm::RationalFunction maximum(std::vector<storm::RationalFunction> const&); + + template double minimum(std::map<uint64_t, double> const&); + template double maximum(std::map<uint64_t, double> const&); + + template storm::RationalNumber minimum(std::map<uint64_t, storm::RationalNumber> const&); + template storm::RationalNumber maximum(std::map<uint64_t, storm::RationalNumber> const&); + + template storm::RationalFunction minimum(std::map<uint64_t, storm::RationalFunction> const&); + template storm::RationalFunction maximum(std::map<uint64_t, storm::RationalFunction> const&); #ifdef STORM_HAVE_CARL // Instantiations for rational number. template bool isOne(storm::RationalNumber const& value); diff --git a/src/utility/constants.h b/src/utility/constants.h index b1a766bc9..c384a4312 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -11,6 +11,10 @@ #include <limits> #include <cstdint> +#include <string> + +#include <vector> +#include <map> namespace storm { @@ -45,6 +49,19 @@ namespace storm { template<typename ValueType> ValueType simplify(ValueType value); + template<typename ValueType> + ValueType minimum(std::vector<ValueType> const& values); + + template<typename ValueType> + ValueType maximum(std::vector<ValueType> const& values); + + template< typename K, typename ValueType> + ValueType minimum(std::map<K, ValueType> const& values); + + template<typename K, typename ValueType> + ValueType maximum(std::map<K, ValueType> const& values); + + template<typename IndexType, typename ValueType> storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry); @@ -59,6 +76,9 @@ namespace storm { template<typename ValueType> bool isInteger(ValueType const& number); + + template<typename ValueType> + std::string to_string(ValueType const& value); } } diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index 2154761c3..8febcbc85 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -7,7 +7,16 @@ #include "src/utility/macros.h" #include "src/storage/jani/Property.h" -namespace storm { +namespace storm{ + + std::vector<std::shared_ptr<storm::logic::Formula const>> formulasInProperties(std::vector<storm::jani::Property> const& properties) { + + std::vector<std::shared_ptr<storm::logic::Formula const>> formulas; + for (auto const& prop : properties) { + formulas.push_back(prop.getFilter().getFormula()); + } + return formulas; + } storm::prism::Program parseProgram(std::string const& path) { storm::prism::Program program = storm::parser::PrismParser::parse(path).simplify().simplify(); @@ -16,8 +25,8 @@ namespace storm { return program; } - std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path) { - std::pair<storm::jani::Model, std::vector<storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(path); + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path) { + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(path); modelAndFormulae.first.checkValid(); return modelAndFormulae; } diff --git a/src/utility/storm.h b/src/utility/storm.h index 7217ca19f..3ce01c028 100644 --- a/src/utility/storm.h +++ b/src/utility/storm.h @@ -100,7 +100,8 @@ namespace storm { return storm::parser::AutoParser<>::parseModel(transitionsFile, labelingFile, stateRewardsFile ? stateRewardsFile.get() : "", transitionRewardsFile ? transitionRewardsFile.get() : "", choiceLabelingFile ? choiceLabelingFile.get() : "" ); } - std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path); + std::vector<std::shared_ptr<storm::logic::Formula const>> formulasInProperties(std::vector<storm::jani::Property> const& properties); + std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& path); storm::prism::Program parseProgram(std::string const& path); std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForExplicit(std::string const& inputString); std::vector<std::shared_ptr<storm::logic::Formula const>> parseFormulasForPrismProgram(std::string const& inputString, storm::prism::Program const& program); @@ -108,7 +109,15 @@ namespace storm { template<typename ValueType> std::shared_ptr<storm::models::sparse::Model<ValueType>> buildSparseModel(storm::storage::SymbolicModelDescription const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) { + + storm::generator::NextStateGeneratorOptions options(formulas); + + + if (storm::settings::getModule<storm::settings::modules::IOSettings>().isBuildFullModelSet()) { + options.setBuildAllLabels(); + options.setBuildAllRewardModels(); + } // Generate command labels if we are going to build a counterexample later. if (storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isMinimalCommandSetGenerationSet()) {