sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Added more classes to IR. Extended PRISM-format parser.

tempestpy_adaptions
dehnert 12 years ago
parent
a4b7b27829
commit
b381321653
22 changed files with 501 additions and 838 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 2
      CMakeLists.txt
  2. 466
      FindPantheios.cmake
  3. 56
      FindSTLSoft.cmake
  4. 35
      src/ir/Assignment.h
  5. 43
      src/ir/BooleanVariable.h
  6. 40
      src/ir/Command.h
  7. 22
      src/ir/IR.h
  8. 51
      src/ir/IntegerVariable.h
  9. 41
      src/ir/Module.h
  10. 41
      src/ir/Program.h
  11. 33
      src/ir/Update.h
  12. 45
      src/ir/Variable.h
  13. 10
      src/ir/expressions/BinaryBooleanFunctionExpression.h
  14. 10
      src/ir/expressions/BinaryNumericalFunctionExpression.h
  15. 10
      src/ir/expressions/BinaryRelationExpression.h
  16. 1
      src/ir/expressions/Expressions.h
  17. 6
      src/ir/expressions/UnaryBooleanFunctionExpression.h
  18. 6
      src/ir/expressions/UnaryNumericalFunctionExpression.h
  19. 147
      src/parser/PrctlParser.cpp
  20. 33
      src/parser/PrctlParser.h
  21. 237
      src/parser/PrismParser.h
  22. 4
      src/storm.cpp

2
CMakeLists.txt
View File

@ -76,7 +76,7 @@ elseif(MSVC)
else(CLANG)
# Set standard flags for clang
set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable")
set (CMAKE_CXX_FLAGS "-std=c++11 -stdlib=libc++ -Wall -Werror -pedantic -Wno-unused-variable -DBOOST_RESULT_OF_USE_TR1 -DBOOST_NO_DECLTYPE")
# Turn on popcnt instruction if desired (yes by default)
if (USE_POPCNT)

466
FindPantheios.cmake
View File

@ -1,466 +0,0 @@
# Locate the Pantheois Logging Framework.
#
# Defines the following variables:
#
# PANTHEIOS_FOUND - Found the Pantheios Logging Framework
# PANTHEIOS_INCLUDE_DIRS - Include directories
#
# Accepts the following variables as input:
#
# PANTHEIOS_ROOT - (as a CMake or environment variable)
# The root directory of the pantheios install prefix
#
# PANTHEIOS_USE_DYNAMIC_RUNTIME
#
# If you want to use splitting, specify LRSplit and than preface the components with L and R, so e.g. LRSplit LFile RSyslog
# To use more than one BackEnd, specify NBackEnd followed by a list of components. NBackEnd requires the NFrontEnd.
#
# Possible Components for BackEnd:
# ACELogger
# COMErrorObject
# File
# FileCallback
# FPrintf
# FPrintfCallback
# Null
# Speech
# Syslog
# WindowsConsole
# WindowsConsoleCallback
# WindowsDebugger
# WindowsDebuggerCallback
# WindowsEventLog
# WindowsMessageBox
# WindowsSyslog
# WindowsSyslogCallback
#
# Possible components for FrontEnd:
# NoFrontEnd
# SimpleFrontEnd
# NFrontEnd
#
#
#=============================================================================
# Copyright 2012 Philipp Berger <admin@philippberger.de>
#
# Distributed under the OSI-approved BSD License (the "License");
# see accompanying file Copyright.txt for details.
#
# 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.
#=============================================================================
# (To distribute this file outside of CMake, substitute the full
# License text for the above reference.)
#
# Credits:
#
# HUGE thanks to Michael Wild
# Additional thanks to:
# Mateusz Loskot
# Rolf Eike Beer
# default for WideString option
set(PANTHEIOS_WIDESTRING 0)
# default for Front- and BackEnd
set(PANTHEIOS_FRONTEND "simple")
set(PANTHEIOS_BACKEND "file")
set(PANTHEIOS_BACKEND_L OFF)
set(PANTHEIOS_BACKEND_R OFF)
set(PANTHEIOS_BACKEND_LIST)
# Use FIND_PACKAGE( Pantheios COMPONENTS ... ) to enable modules
if( Pantheios_FIND_COMPONENTS )
list(FIND Pantheios_FIND_COMPONENTS "LRSplit" PANTHEIOS_use_lrsplit)
list(FIND Pantheios_FIND_COMPONENTS "NFrontEnd" PANTHEIOS_use_nfe)
list(FIND Pantheios_FIND_COMPONENTS "NBackEnd" PANTHEIOS_use_nbe)
list(FIND Pantheios_FIND_COMPONENTS "WideString" PANTHEIOS_use_ws)
list(REMOVE_ITEM Pantheios_FIND_COMPONENTS "LRSplit" "NFrontEnd" "NBackEnd" "WideString")
if (NOT PANTHEIOS_use_ws EQUAL -1)
# Use WideString
set(PANTHEIOS_WIDESTRING 1)
endif()
if (NOT PANTHEIOS_use_lrsplit EQUAL -1)
# Found LRSplit
set(PANTHEIOS_BACKEND "lrsplit")
if (NOT PANTHEIOS_use_nbe EQUAL -1)
# Also found NBe
message(FATAL_ERROR "Pantheios: Use either LRSplit or NBackEnd, not both.")
endif()
if (NOT PANTHEIOS_use_nfe EQUAL -1)
# Also found NFe
message(FATAL_ERROR "Pantheios: Use either LRSplit or NFrontEnd, not both.")
endif()
foreach( component ${Pantheios_FIND_COMPONENTS} )
# LRSplit L BackEnds
string(SUBSTRING ${component} 0 1 _sub_comp_head)
string(LENGTH ${component} _length_comp)
math(EXPR _length_comp_tail "${_length_comp} - 1")
string(SUBSTRING ${component} 1 ${_length_comp_tail} _sub_comp_tail)
if ((_sub_comp_tail STREQUAL "ACELogger") OR (_sub_comp_tail STREQUAL "COMErrorObject") OR (_sub_comp_tail STREQUAL "File") OR (_sub_comp_tail STREQUAL "FileCallback") OR (_sub_comp_tail STREQUAL "FPrintf") OR (_sub_comp_tail STREQUAL "FPrintfCallback") OR (_sub_comp_tail STREQUAL "Null") OR (_sub_comp_tail STREQUAL "Speech") OR (_sub_comp_tail STREQUAL "Syslog") OR (_sub_comp_tail STREQUAL "WindowsConsole") OR (_sub_comp_tail STREQUAL "WindowsConsoleCallback") OR (_sub_comp_tail STREQUAL "WindowsDebugger") OR (_sub_comp_tail STREQUAL "WindowsDebuggerCallback") OR (_sub_comp_tail STREQUAL "WindowsEventLog") OR (_sub_comp_tail STREQUAL "WindowsMessageBox") OR (_sub_comp_tail STREQUAL "WindowsSyslog") OR (_sub_comp_tail STREQUAL "WindowsSyslogCallback"))
if ((_sub_comp_head STREQUAL L) OR (_sub_comp_head STREQUAL R))
message(STATUS "Pantheios: Setting LRSplit BackEnd ${_sub_comp_head} to ${_sub_comp_tail}")
string(TOLOWER ${_sub_comp_tail} _sub_comp_tail_low)
set(PANTHEIOS_BACKEND_${_sub_comp_head} "${_sub_comp_tail_low}")
else ()
message(FATAL_ERROR "Pantheios: Internal Parsing Error")
endif()
# FrontEnds
elseif (component STREQUAL "NoFrontEnd")
message(STATUS "Pantheios: Setting FrontEnd to NoFrontEnd")
set(PANTHEIOS_FRONTEND "null")
elseif (component STREQUAL "SimpleFrontEnd")
message(STATUS "Pantheios: Setting FrontEnd to SimpleFrontEnd")
set(PANTHEIOS_FRONTEND "simple")
else ()
message(FATAL_ERROR "Unknown Component: ${component}")
endif ()
endforeach(component)
elseif (NOT PANTHEIOS_use_nbe EQUAL -1)
# Found NBackEnd
if (PANTHEIOS_use_nfe EQUAL -1)
message(FATAL_ERROR "Pantheios: Usage of NBackEnd requires the NFrontEnd.")
endif()
set(PANTHEIOS_BACKEND "N")
set(PANTHEIOS_FRONTEND "N")
foreach( component ${Pantheios_FIND_COMPONENTS} )
# Std BackEnds
if ((component STREQUAL "ACELogger") OR (component STREQUAL "COMErrorObject") OR (component STREQUAL "File") OR (component STREQUAL "FileCallback") OR (component STREQUAL "FPrintf") OR (component STREQUAL "FPrintfCallback") OR (component STREQUAL "Null") OR (component STREQUAL "Speech") OR (component STREQUAL "Syslog") OR (component STREQUAL "WindowsConsole") OR (component STREQUAL "WindowsConsoleCallback") OR (component STREQUAL "WindowsDebugger") OR (component STREQUAL "WindowsDebuggerCallback") OR (component STREQUAL "WindowsEventLog") OR (component STREQUAL "WindowsMessageBox") OR (component STREQUAL "WindowsSyslog") OR (component STREQUAL "WindowsSyslogCallback"))
message(STATUS "Pantheios: Adding BackEnd ${component}")
string(TOLOWER ${component} _low_comp)
list(APPEND PANTHEIOS_BACKEND_LIST ${_low_comp})
else ()
message(FATAL_ERROR "Unknown Component: ${component}")
endif ()
endforeach(component)
else ()
# Simple, one FE, one BE
foreach( component ${Pantheios_FIND_COMPONENTS} )
if ((component STREQUAL "ACELogger") OR (component STREQUAL "COMErrorObject") OR (component STREQUAL "File") OR (component STREQUAL "FileCallback") OR (component STREQUAL "FPrintf") OR (component STREQUAL "FPrintfCallback") OR (component STREQUAL "Null") OR (component STREQUAL "Speech") OR (component STREQUAL "Syslog") OR (component STREQUAL "WindowsConsole") OR (component STREQUAL "WindowsConsoleCallback") OR (component STREQUAL "WindowsDebugger") OR (component STREQUAL "WindowsDebuggerCallback") OR (component STREQUAL "WindowsEventLog") OR (component STREQUAL "WindowsMessageBox") OR (component STREQUAL "WindowsSyslog") OR (component STREQUAL "WindowsSyslogCallback"))
message(STATUS "Pantheios: Setting BackEnd to ${component}")
string(TOLOWER ${component} _low_comp)
set(PANTHEIOS_BACKEND ${_low_comp})
# FrontEnds
elseif (component STREQUAL "NoFrontEnd")
message(STATUS "Pantheios: Setting FrontEnd to NoFrontEnd")
set(PANTHEIOS_FRONTEND "null")
elseif (component STREQUAL "SimpleFrontEnd")
message(STATUS "Pantheios: Setting FrontEnd to SimpleFrontEnd")
set(PANTHEIOS_FRONTEND "simple")
else ()
message(FATAL_ERROR "Unknown Component: ${component}")
endif ()
endforeach(component)
endif ()
endif(Pantheios_FIND_COMPONENTS)
if (PANTHEIOS_USE_DYNAMIC_RUNTIME)
set(PANTHEIOS_LIB_LINKTYPE "dll")
else ()
set(PANTHEIOS_LIB_LINKTYPE "mt")
endif ()
if(PANTHEIOS_INCLUDE_DIR)
if (NOT PANTHEIOS_ROOT)
get_filename_component(PANTHEIOS_ROOT "${PANTHEIOS_INCLUDE_DIR}" PATH)
endif()
get_filename_component(PANTHEIOS_ROOT_HINT "${PANTHEIOS_INCLUDE_DIR}" PATH)
endif()
find_path(PANTHEIOS_INCLUDE_DIR pantheios/pantheios.h
PATH_SUFFIXES include
HINTS ${PANTHEIOS_ROOT} ${PANTHEIOS_ROOT_HINT}
ENV PANTHEIOS_ROOT
)
# No idea what the stuff for ICC et. al. is, so I don't handle it here...
set(_P_COMP_TAG)
set(_P_OS_TAG)
set(_P_ARCH_TAG)
if(MSVC)
if(MSVC60)
set(_P_COMP_TAG vc6)
elseif(MSVC70)
set(_P_COMP_TAG vc7)
elseif(MSVC71)
set(_P_COMP_TAG vc71)
elseif(MSVC80)
set(_P_COMP_TAG vc8)
if(CMAKE_SIZEOF_VOID_P EQUAL 8)
set(_P_ARCH_TAG .x64)
endif()
elseif(MSVC90)
set(_P_COMP_TAG vc9)
if(CMAKE_SIZEOF_VOID_P EQUAL 8)
set(_P_ARCH_TAG .x64)
endif()
elseif(MSVC10)
set(_P_COMP_TAG vc10)
if(CMAKE_SIZEOF_VOID_P EQUAL 8)
set(_P_ARCH_TAG .x64)
endif()
elseif(MSVC11)
set(_P_COMP_TAG vc11)
if(CMAKE_SIZEOF_VOID_P EQUAL 8)
set(_P_ARCH_TAG .x64)
endif()
endif()
elseif(CMAKE_COMPILER_IS_GNUCC)
execute_process(COMMAND ${CMAKE_C_COMPILER} -dumpversion OUTPUT_VARIABLE GCC_VERSION)
string(REGEX MATCHALL "[0-9]+" GCC_VERSION_COMPONENTS ${GCC_VERSION})
list(GET GCC_VERSION_COMPONENTS 0 GCC_MAJOR)
list(GET GCC_VERSION_COMPONENTS 1 GCC_MINOR)
set(_P_COMP_TAG gcc${GCC_MAJOR}${GCC_MINOR})
if(CMAKE_SIZEOF_VOID_P EQUAL 8)
set(_P_ARCH_TAG .file64bit)
endif()
else()
message(FATAL_ERROR "Pantheios: Your compiler/environment is currently unsupported.")
endif()
set(_P_LIB_TAG ${_P_COMP_TAG}${_P_OS_TAG}${_P_ARCH_TAG})
# Is this the right way?
set(PANTHEIOS_INCLUDE_DIRS ${PANTHEIOS_INCLUDE_DIR})
set(_P_REQUIRED_LIBVARS)
set(PANTHEIOS_LIBRARIES)
set(PANTHEIOS_LIBRARIES_DEBUG)
set(PANTHEIOS_LIBRARIES_RELEASE)
#core and util libraries
foreach(l core util)
find_library(PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_DEBUG_LIBRARY
pantheios.1.${l}.${_P_LIB_TAG}.${PANTHEIOS_LIB_LINKTYPE}.debug
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
find_library(PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY
pantheios.1.${l}.${_P_LIB_TAG}.${PANTHEIOS_LIB_LINKTYPE}
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
list(APPEND _P_REQUIRED_LIBVARS
PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_DEBUG_LIBRARY
PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY
)
list(APPEND PANTHEIOS_LIBRARIES
debug ${PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_DEBUG_LIBRARY}
optimized ${PANTHEIOS_${l}_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY}
)
endforeach()
# set PANTHEIOS_LIBRARY_DIRS
get_filename_component(PANTHEIOS_LIBRARY_DIRS ${PANTHEIOS_core_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY} PATH)
# backend libraries (split, sole, local, remote and common)
set(_P_LT ${PANTHEIOS_LIB_LINKTYPE})
set(_P_BE ${PANTHEIOS_BACKEND})
find_library(PANTHEIOS_be_${_P_BE}_${_P_LT}_DEBUG_LIBRARY
pantheios.1.be.${_P_BE}.${_P_LIB_TAG}.${_P_LT}.debug
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
find_library(PANTHEIOS_be_${_P_BE}_${_P_LT}_LIBRARY
pantheios.1.be.${_P_BE}.${_P_LIB_TAG}.${_P_LT}
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
list(APPEND _P_REQUIRED_LIBVARS
PANTHEIOS_be_${_P_BE}_${_P_LT}_DEBUG_LIBRARY
PANTHEIOS_be_${_P_BE}_${_P_LT}_LIBRARY
)
list(APPEND PANTHEIOS_LIBRARIES
debug ${PANTHEIOS_be_${_P_BE}_${_P_LT}_DEBUG_LIBRARY}
optimized ${PANTHEIOS_be_${_P_BE}_${_P_LT}_LIBRARY}
)
if (_P_BE STREQUAL N)
# N Backend, go through list
message(STATUS "Pantheios: Dbg: Lib-n")
foreach (blib PANTHEIOS_BACKEND_LIST)
find_library(PANTHEIOS_bec_${blib}_${_P_LT}_DEBUG_LIBRARY
pantheios.1.bec.${blib}.${_P_LIB_TAG}.${_P_LT}.debug
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
find_library(PANTHEIOS_bec_${blib}_${_P_LT}_LIBRARY
pantheios.1.bec.${blib}.${_P_LIB_TAG}.${_P_LT}
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
list(APPEND _P_REQUIRED_LIBVARS
PANTHEIOS_bec_${blib}_${_P_LT}_DEBUG_LIBRARY
PANTHEIOS_bec_${blib}_${_P_LT}_LIBRARY
)
list(APPEND PANTHEIOS_LIBRARIES
debug ${PANTHEIOS_bec_${blib}_${_P_LT}_DEBUG_LIBRARY}
optimized ${PANTHEIOS_bec_${blib}_${_P_LT}_LIBRARY}
)
endforeach()
elseif (_P_BE STREQUAL lrsplit)
# LRSplit
message(STATUS "Pantheios: Dbg: Lib-lrsplit")
# Left side
foreach (t bec bel)
find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_DEBUG_LIBRARY
pantheios.1.${t}.${PANTHEIOS_BACKEND_L}.${_P_LIB_TAG}.${_P_LT}.debug
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_LIBRARY
pantheios.1.${t}.${PANTHEIOS_BACKEND_L}.${_P_LIB_TAG}.${_P_LT}
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
list(APPEND _P_REQUIRED_LIBVARS
PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_DEBUG_LIBRARY
PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_LIBRARY
)
list(APPEND PANTHEIOS_LIBRARIES
debug ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_DEBUG_LIBRARY}
optimized ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND_L}_${_P_LT}_LIBRARY}
)
endforeach()
# Right side
foreach (t bec ber)
find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_DEBUG_LIBRARY
pantheios.1.${t}.${PANTHEIOS_BACKEND_R}.${_P_LIB_TAG}.${_P_LT}.debug
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_LIBRARY
pantheios.1.${t}.${PANTHEIOS_BACKEND_R}.${_P_LIB_TAG}.${_P_LT}
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
list(APPEND _P_REQUIRED_LIBVARS
PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_DEBUG_LIBRARY
PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_LIBRARY
)
list(APPEND PANTHEIOS_LIBRARIES
debug ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_DEBUG_LIBRARY}
optimized ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND_R}_${_P_LT}_LIBRARY}
)
endforeach()
else ()
# normal
message(STATUS "Pantheios: Dbg: Lib-normal")
foreach (t bec)
find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_DEBUG_LIBRARY
pantheios.1.${t}.${PANTHEIOS_BACKEND}.${_P_LIB_TAG}.${_P_LT}.debug
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
find_library(PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_LIBRARY
pantheios.1.${t}.${PANTHEIOS_BACKEND}.${_P_LIB_TAG}.${_P_LT}
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
list(APPEND _P_REQUIRED_LIBVARS
PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_DEBUG_LIBRARY
PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_LIBRARY
)
list(APPEND PANTHEIOS_LIBRARIES
debug ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_DEBUG_LIBRARY}
optimized ${PANTHEIOS_${t}_${PANTHEIOS_BACKEND}_${_P_LT}_LIBRARY}
)
endforeach()
endif()
# frontent libraries
set(PANTHEIOS_fe_DEBUG_LIBRARY)
set(PANTHEIOS_fe_LIBRARY)
if(NOT PANTHEIOS_FRONTENT STREQUAL null)
set(_P_FE ${PANTHEIOS_FRONTEND})
find_library(PANTHEIOS_${_P_FE}_${_P_LT}_DEBUG_LIBRARY
pantheios.1.fe.${_P_FE}.${_P_LIB_TAG}.${_P_LT}.debug
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
find_library(PANTHEIOS_${_P_FE}_${_P_LT}_LIBRARY
pantheios.1.fe.${_P_FE}.${_P_LIB_TAG}.${_P_LT}
PATH_SUFFIXES lib
HINTS ${PANTHEIOS_ROOT_HINT} ${PANTHEIOS_ROOT}
ENV PANTHEIOS_ROOT
)
list(APPEND _P_REQUIRED_LIBVARS
PANTHEIOS_${_P_FE}_${_P_LT}_DEBUG_LIBRARY
PANTHEIOS_${_P_FE}_${_P_LT}_LIBRARY
)
list(APPEND PANTHEIOS_LIBRARIES
debug ${PANTHEIOS_${_P_FE}_${_P_LT}_DEBUG_LIBRARY}
optimized ${PANTHEIOS_${_P_FE}_${_P_LT}_LIBRARY}
)
endif()
# gcc needs the core library mentioned a second time at the end
# (see Pantheios FAQ Q/A8)
# At this point, the core has to be found already,
# so only the additions to the lists are repeated here...
if(CMAKE_COMPILER_IS_GNUCC)
list(APPEND _P_REQUIRED_LIBVARS
PANTHEIOS_core_${PANTHEIOS_LIB_LINKTYPE}_DEBUG_LIBRARY
PANTHEIOS_core_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY
)
list(APPEND PANTHEIOS_LIBRARIES
debug ${PANTHEIOS_core_${PANTHEIOS_LIB_LINKTYPE}_DEBUG_LIBRARY}
optimized ${PANTHEIOS_core_${PANTHEIOS_LIB_LINKTYPE}_LIBRARY}
)
endif()
# copy to NAME_LIBS
set(PANTHEIOS_LIBS ${PANTHEIOS_LIBRARIES})
# handle the QUIETLY and REQUIRED arguments and set Pantheios_FOUND to TRUE if
# all listed variables are TRUE
include(FindPackageHandleStandardArgs)
FIND_PACKAGE_HANDLE_STANDARD_ARGS(Pantheios
REQUIRED_VARS PANTHEIOS_INCLUDE_DIR ${_P_REQUIRED_LIBVARS}
)
message(STATUS ${PANTHEIOS_INCLUDE_DIR} ${PANTHEIOS_LIBRARIES})
mark_as_advanced(PANTHEIOS_INCLUDE_DIR PANTHEIOS_LIBRARIES)

56
FindSTLSoft.cmake
View File

@ -1,56 +0,0 @@
# Locate the STLSoft Headers.
#
# Defines the following variables:
#
# STLSOFT_FOUND - Found the Pantheios Logging Framework
# STLSOFT_INCLUDE_DIRS - Include directories
#
# Accepts the following variables as input:
#
# STLSOFT_ROOT - (as a CMake or environment variable)
# The root directory of the STLSoft install prefix
#
#
#=============================================================================
# Copyright 2012 Philipp Berger <admin@philippberger.de>
#
# Distributed under the OSI-approved BSD License (the "License");
# see accompanying file Copyright.txt for details.
#
# 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.
#=============================================================================
# (To distribute this file outside of CMake, substitute the full
# License text for the above reference.)
#
if(STLSOFT_INCLUDE_DIR)
if (NOT STLSOFT_ROOT)
get_filename_component(STLSOFT_ROOT "${STLSOFT_INCLUDE_DIR}" PATH)
endif()
get_filename_component(STLSOFT_ROOT_HINT "${STLSOFT_INCLUDE_DIR}" PATH)
endif()
find_path(STLSOFT_INCLUDE_DIR stlsoft/stlsoft.h
PATH_SUFFIXES include
HINTS ${STLSOFT_ROOT} ${STLSOFT_ROOT_HINT}
ENV STLSOFT_ROOT
)
set(STLSOFT_INCLUDE_DIRS ${STLSOFT_INCLUDE_DIR})
# handle the QUIETLY and REQUIRED arguments and set STLSOFT_FOUND to TRUE if
# all listed variables are TRUE
include(FindPackageHandleStandardArgs)
FIND_PACKAGE_HANDLE_STANDARD_ARGS(STLSoft
REQUIRED_VARS STLSOFT_INCLUDE_DIR
)
mark_as_advanced(STLSOFT_INCLUDE_DIR)

35
src/ir/Assignment.h
View File

@ -0,0 +1,35 @@
/*
* Assignment.h
*
* Created on: 06.01.2013
* Author: chris
*/
#ifndef ASSIGNMENT_H_
#define ASSIGNMENT_H_
#include "expressions/Expressions.h"
#include <boost/fusion/include/adapt_struct.hpp>
namespace storm {
namespace ir {
class Assignment {
public:
std::string variableName;
std::shared_ptr<storm::ir::expressions::BaseExpression> expression;
};
}
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::Assignment,
(std::string, variableName)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, expression)
)
#endif /* ASSIGNMENT_H_ */

43
src/ir/BooleanVariable.h
View File

@ -0,0 +1,43 @@
/*
* BooleanVariable.h
*
* Created on: 08.01.2013
* Author: chris
*/
#ifndef BOOLEANVARIABLE_H_
#define BOOLEANVARIABLE_H_
namespace storm {
namespace ir {
class BooleanVariable : public Variable {
public:
BooleanVariable() {
}
BooleanVariable(std::string variableName) : Variable(variableName) {
}
virtual ~BooleanVariable() {
}
virtual std::string toString() {
return variableName + ": bool;";
}
};
}
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::BooleanVariable,
(std::string, variableName)
)
#endif /* BOOLEANVARIABLE_H_ */

40
src/ir/Command.h
View File

@ -0,0 +1,40 @@
/*
* Command.h
*
* Created on: 06.01.2013
* Author: chris
*/
#ifndef COMMAND_H_
#define COMMAND_H_
#include "IR.h"
namespace storm {
namespace ir {
class Command {
public:
std::string commandName;
std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression;
std::vector<storm::ir::Update> updates;
std::string toString() {
return "command!";
}
};
}
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::Command,
(std::string, commandName)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, guardExpression)
(std::vector<storm::ir::Update>, updates)
)
#endif /* COMMAND_H_ */

22
src/ir/IR.h
View File

@ -0,0 +1,22 @@
/*
* IR.h
*
* Created on: 06.01.2013
* Author: chris
*/
#ifndef IR_H_
#define IR_H_
#include "expressions/Expressions.h"
#include "Assignment.h"
#include "Update.h"
#include "Command.h"
#include "Variable.h"
#include "BooleanVariable.h"
#include "IntegerVariable.h"
#include "Module.h"
#include "RewardModel.h"
#include "Program.h"
#endif /* IR_H_ */

51
src/ir/IntegerVariable.h
View File

@ -0,0 +1,51 @@
/*
* IntegerVariable.h
*
* Created on: 08.01.2013
* Author: chris
*/
#ifndef INTEGERVARIABLE_H_
#define INTEGERVARIABLE_H_
#include "Variable.h"
namespace storm {
namespace ir {
class IntegerVariable : public Variable {
public:
IntegerVariable() {
}
IntegerVariable(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound) : Variable(variableName), lowerBound(lowerBound), upperBound(upperBound) {
}
virtual ~IntegerVariable() {
}
virtual std::string toString() {
return variableName + ": int[];";
}
void setLowerBound(std::shared_ptr<storm::ir::expressions::BaseExpression>& lowerBound) {
this->lowerBound = lowerBound;
}
void setUpperBound(std::shared_ptr<storm::ir::expressions::BaseExpression>& upperBound) {
this->upperBound = upperBound;
}
std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound;
std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound;
};
}
}
#endif /* INTEGERVARIABLE_H_ */

41
src/ir/Module.h
View File

@ -8,11 +8,47 @@
#ifndef MODULE_H_
#define MODULE_H_
#include "IR.h"
namespace storm {
namespace ir {
class Module {
public:
Module() {
}
std::string toString() {
std::string result = "module " + moduleName + "\n";
for (auto variable : booleanVariables) {
result += "\t" + variable.toString() + "\n";
}
result += "\n";
for (auto variable : integerVariables) {
result += "\t" + variable.toString() + "\n";
}
for (auto command : commands) {
result += "\t" + command.toString() + "\n";
}
result += "endmodule\n";
return result;
}
void addBooleanVariable(storm::ir::BooleanVariable variable) {
booleanVariables.push_back(variable);
}
void addIntegerVariable(storm::ir::IntegerVariable variable) {
integerVariables.push_back(variable);
}
std::string moduleName;
std::vector<storm::ir::BooleanVariable> booleanVariables;
std::vector<storm::ir::IntegerVariable> integerVariables;
std::vector<storm::ir::Command> commands;
};
@ -20,5 +56,10 @@ class Module {
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::Module,
(std::string, moduleName)
(std::vector<storm::ir::Command>, commands)
)
#endif /* MODULE_H_ */

41
src/ir/Program.h
View File

@ -19,12 +19,44 @@ namespace ir {
class Program {
public:
enum ModelType {DTMC, CTMC, MDP, CTMDP} modelType;
std::map<std::string, storm::ir::expressions::ConstantExpression> undefinedConstantExpressions;
std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions;
std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions;
std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions;
std::vector<storm::ir::Module> modules;
std::map<std::string, storm::ir::RewardModel> rewards;
std::string toString() {
return std::string("prog!");
std::string result = "";
for (auto element : booleanUndefinedConstantExpressions) {
result += "const bool " + element.first + ";\n";
}
for (auto element : integerUndefinedConstantExpressions) {
result += "const int " + element.first + ";\n";
}
for (auto element : doubleUndefinedConstantExpressions) {
result += "const double " + element.first + ";\n";
}
for (auto mod : modules) {
result += mod.toString();
}
return result;
}
void addBooleanUndefinedConstantExpression(std::string constantName, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression> constantExpression) {
booleanUndefinedConstantExpressions[constantName] = constantExpression;
}
void addIntegerUndefinedConstantExpression(std::string constantName, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression> constantExpression) {
integerUndefinedConstantExpressions[constantName] = constantExpression;
}
void addDoubleUndefinedConstantExpression(std::string constantName, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression> constantExpression) {
doubleUndefinedConstantExpressions[constantName] = constantExpression;
}
void setModules(std::vector<storm::ir::Module> modules) {
this->modules = modules;
}
};
@ -32,4 +64,9 @@ public:
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::Program,
(std::vector<storm::ir::Module>, modules)
)
#endif /* PROGRAM_H_ */

33
src/ir/Update.h
View File

@ -0,0 +1,33 @@
/*
* Update.h
*
* Created on: 06.01.2013
* Author: chris
*/
#ifndef UPDATE_H_
#define UPDATE_H_
#include "IR.h"
namespace storm {
namespace ir {
class Update {
public:
std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
std::vector<storm::ir::Assignment> assignments;
};
}
}
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::Update,
(std::shared_ptr<storm::ir::expressions::BaseExpression>, likelihoodExpression)
(std::vector<storm::ir::Assignment>, assignments)
)
#endif /* UPDATE_H_ */

45
src/ir/Variable.h
View File

@ -0,0 +1,45 @@
/*
* Variable.h
*
* Created on: 06.01.2013
* Author: chris
*/
#ifndef VARIABLE_H_
#define VARIABLE_H_
namespace storm {
namespace ir {
class Variable {
public:
std::string variableName;
Variable() {
}
Variable(std::string variableName) : variableName(variableName) {
}
virtual ~Variable() {
}
virtual std::string toString() {
return variableName;
}
void setVariableName(std::string variableName) {
this->variableName = variableName;
}
};
}
}
#endif /* VARIABLE_H_ */

10
src/ir/expressions/BinaryBooleanFunctionExpression.h
View File

@ -20,10 +20,10 @@ namespace expressions {
class BinaryBooleanFunctionExpression : public BaseExpression {
public:
enum FunctorType {AND, OR, XOR, IMPLIES} functor;
BaseExpression* left;
BaseExpression* right;
std::shared_ptr<storm::ir::expressions::BaseExpression> left;
std::shared_ptr<BaseExpression> right;
BinaryBooleanFunctionExpression(BaseExpression* left, BaseExpression* right, FunctorType functor) {
BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctorType functor) {
this->left = left;
this->right = right;
this->functor = functor;
@ -55,8 +55,8 @@ public:
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::BinaryBooleanFunctionExpression,
(storm::ir::expressions::BaseExpression*, left)
(storm::ir::expressions::BaseExpression*, right)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, left)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, right)
(storm::ir::expressions::BinaryBooleanFunctionExpression::FunctorType, functor)
)

10
src/ir/expressions/BinaryNumericalFunctionExpression.h
View File

@ -18,11 +18,11 @@ namespace expressions {
class BinaryNumericalFunctionExpression : public BaseExpression {
public:
BaseExpression* left;
BaseExpression* right;
std::shared_ptr<BaseExpression> left;
std::shared_ptr<BaseExpression> right;
enum FunctorType {PLUS, MINUS, TIMES, DIVIDE} functor;
BinaryNumericalFunctionExpression(BaseExpression* left, BaseExpression* right, FunctorType functor) {
BinaryNumericalFunctionExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, FunctorType functor) {
this->left = left;
this->right = right;
this->functor = functor;
@ -55,8 +55,8 @@ public:
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::BinaryNumericalFunctionExpression,
(storm::ir::expressions::BaseExpression*, left)
(storm::ir::expressions::BaseExpression*, right)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, left)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, right)
(storm::ir::expressions::BinaryNumericalFunctionExpression::FunctorType, functor)
)

10
src/ir/expressions/BinaryRelationExpression.h
View File

@ -18,11 +18,11 @@ namespace expressions {
class BinaryRelationExpression : public BaseExpression {
public:
BaseExpression* left;
BaseExpression* right;
std::shared_ptr<BaseExpression> left;
std::shared_ptr<BaseExpression> right;
enum RelationType {EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL} relation;
BinaryRelationExpression(BaseExpression* left, BaseExpression* right, RelationType relation) {
BinaryRelationExpression(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right, RelationType relation) {
this->left = left;
this->right = right;
this->relation = relation;
@ -56,8 +56,8 @@ public:
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::BinaryRelationExpression,
(storm::ir::expressions::BaseExpression*, left)
(storm::ir::expressions::BaseExpression*, right)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, left)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, right)
(storm::ir::expressions::BinaryRelationExpression::RelationType, relation)
)

1
src/ir/expressions/Expressions.h
View File

@ -8,6 +8,7 @@
#ifndef EXPRESSIONS_H_
#define EXPRESSIONS_H_
#include "BaseExpression.h"
#include "BinaryBooleanFunctionExpression.h"
#include "BinaryNumericalFunctionExpression.h"
#include "BinaryRelationExpression.h"

6
src/ir/expressions/UnaryBooleanFunctionExpression.h
View File

@ -18,10 +18,10 @@ namespace expressions {
class UnaryBooleanFunctionExpression : public BaseExpression {
public:
BaseExpression* child;
std::shared_ptr<BaseExpression> child;
enum FunctorType {NOT} functor;
UnaryBooleanFunctionExpression(BaseExpression* child, FunctorType functor) {
UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctorType functor) {
this->child = child;
this->functor = functor;
}
@ -49,7 +49,7 @@ public:
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::UnaryBooleanFunctionExpression,
(storm::ir::expressions::BaseExpression*, child)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, child)
(storm::ir::expressions::UnaryBooleanFunctionExpression::FunctorType, functor)
)

6
src/ir/expressions/UnaryNumericalFunctionExpression.h
View File

@ -18,10 +18,10 @@ namespace expressions {
class UnaryNumericalFunctionExpression : public BaseExpression {
public:
BaseExpression* child;
std::shared_ptr<BaseExpression> child;
enum FunctorType {MINUS} functor;
UnaryNumericalFunctionExpression(BaseExpression* child, FunctorType functor) {
UnaryNumericalFunctionExpression(std::shared_ptr<BaseExpression> child, FunctorType functor) {
this->child = child;
this->functor = functor;
}
@ -49,7 +49,7 @@ public:
BOOST_FUSION_ADAPT_STRUCT(
storm::ir::expressions::UnaryNumericalFunctionExpression,
(storm::ir::expressions::BaseExpression*, child)
(std::shared_ptr<storm::ir::expressions::BaseExpression>, child)
(storm::ir::expressions::UnaryNumericalFunctionExpression::FunctorType, functor)
)

147
src/parser/PrctlParser.cpp
View File

@ -1,147 +0,0 @@
#include "src/parser/PrctlParser.h"
#include <iostream>
#include <map>
//#include <pair>
#include <boost/spirit/include/classic_core.hpp>
#include <boost/spirit/include/qi_grammar.hpp>
#include <boost/spirit/include/qi_rule.hpp>
#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix_operator.hpp>
#include <boost/spirit/include/qi_char_class.hpp>
#include <boost/bind.hpp>
namespace bs = boost::spirit;
namespace
{
using namespace bs;
using namespace bs::qi;
using namespace bs::standard;
struct SpiritParser : public grammar< char const* >
{
typedef rule< char const* > rule_none;
typedef rule< char const*, double() > rule_double;
typedef rule< char const*, std::string() > rule_string;
/*!
* @brief Generic Nonterminals.
*/
rule_none ws;
rule_string variable;
rule_double value;
/*!
* @brief Nonterminals for file header.
*/
rule< char const* > varDef;
rule_none type;
/*!
* @brief Nonterminals for formula.
*/
rule_none formula, opP;
/*!
* @brief Nonterminals for high-level file structure.
*/
rule_none file, header;
/*!
* @brief Variable assignments.
*/
std::map<std::string, double> variables;
/*!
* @brief Resulting formula.
*/
storm::formula::PctlFormula<double>* result;
struct dump
{
void print(double const& i, std::string& s)
{
std::cout << s << " = " << i << std::endl;
}
void operator()(double const& a, unused_type, unused_type) const
{
std::cout << a << std::endl;
}
void operator()(std::string const& a, unused_type, unused_type) const
{
std::cout << a << std::endl;
}
void operator()(utree const& a, unused_type, unused_type) const
{
std::cout << &a << std::endl;
}
};
SpiritParser() : SpiritParser::base_type(file, "PRCTL parser")
{
variable %= alnum;
ws = *( space );
value %= ( double_ | int_ ); // double_ must be *before* int_
type = string("int") | string("double");
/*
* Todo:
* Use two arguments at one point in the code, e.g. do something like
* this->variables[ variable ] = value
*
* You can have local variables in rules, but somehow does not work.
* You can also (somehow) let a rule return some arbitrary class and let boost magically collect the arguments for the constructor.
* No idea how this can possibly work, did not get this to work.
* You can also generate a syntax tree and do this manually (-> utree)... somehow.
*
* Attention: spirit had some major upgrades in the last few releases. 1.48 already lacks some features that might be useful.
*
* The rules parse the const definitions of
* http://www.prismmodelchecker.org/manual/PropertySpecification/PropertiesFiles
* We actually do not need them, but the problems I described above are fairly generic.
* We will not be able to parse the formulas if we don't solve them...
*
* Example input:
* const int k = 7;
* const double T = 9;
* const double p = 0.01;
*
* Parser can be run via ./storm --test-prctl <filename> foo bar
* foo and bar are necessary, otherwise the option parser fails...
*/
varDef =
string("const") >> ws >>
type >> ws >>
variable >> ws >>
string("=") >> ws >>
value >> ws >>
string(";");
header = +( varDef >> ws );
file = header;
}
};
}
storm::parser::PrctlParser::PrctlParser(const char* filename)
{
SpiritParser p;
storm::parser::MappedFile file(filename);
char* data = file.data;
if (bs::qi::parse< char const* >(data, file.dataend, p))
{
std::cout << "File was parsed" << std::endl;
std::string rest(data, file.dataend);
std::cout << "Rest: " << rest << std::endl;
this->formula = p.result;
}
else this->formula = NULL;
}

33
src/parser/PrctlParser.h
View File

@ -1,33 +0,0 @@
#ifndef STORM_PARSER_PRCTLPARSER_H_
#define STORM_PARSER_PRCTLPARSER_H_
#include "src/formula/PctlFormula.h"
#include "src/parser/Parser.h"
namespace storm {
namespace parser {
/*!
* @brief Load PRCTL file
*/
class PrctlParser : Parser
{
public:
PrctlParser(const char * filename);
/*!
* @brief return formula object parsed from file.
*/
storm::formula::PctlFormula<double>* getFormula()
{
return this->formula;
}
private:
storm::formula::PctlFormula<double>* formula;
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_PRCTLPARSER_H_ */

237
src/parser/PrismParser.h
View File

@ -13,8 +13,7 @@
#include <boost/fusion/include/adapt_struct.hpp>
#include <boost/fusion/include/io.hpp>
#include "src/ir/expressions/Expressions.h"
#include "src/ir/Program.h"
#include "src/ir/IR.h"
namespace storm {
@ -28,35 +27,28 @@ class PrismParser {
public:
void test() {
std::string testInput = "";
// storm::ir::Program* result = getProgram(testInput);
std::string testInput = "" \
"" \
"const bool d; const int c; const double x;" \
"module test " \
" a : bool;" \
"endmodule" \
"module test2 endmodule";
getProgram(testInput);
/* std::cout << "Resulting program:" << std::endl;
std::cout << "-------------------------\n";
std::cout << result->toString() << std::endl;
std::cout << "-------------------------\n"; */
}
void getProgram(std::string inputString) {
using qi::_val;
using qi::int_;
using qi::_r1;
using qi::_1;
using phoenix::ref;
using phoenix::val;
prismGrammar<std::string::const_iterator> grammar;
storm::ir::Program result;
prismGrammar<std::string::const_iterator> grammar(result);
std::string::const_iterator it = inputString.begin();
std::string::const_iterator end = inputString.end();
storm::ir::Program result;
int resultInt = 0;
std::string input = "asdf";
bool r = phrase_parse(it, end, grammar(phoenix::val(input)), ascii::space, resultInt);
storm::ir::Program realResult;
bool r = phrase_parse(it, end, grammar, ascii::space, realResult);
if (r && it == end) {
std::cout << "Parsing successful!" << std::endl;
std::cout << realResult.toString() << std::endl;
} else {
std::string rest(it, end);
std::cout << "-------------------------\n";
@ -68,127 +60,146 @@ public:
private:
template<typename Iterator>
struct prismGrammar : qi::grammar<Iterator, int(std::string), ascii::space_type> {
struct prismGrammar : qi::grammar<Iterator, storm::ir::Program(), ascii::space_type> {
prismGrammar() : prismGrammar::base_type(start) {
using qi::_val;
using qi::int_;
using qi::_r1;
using qi::_1;
using phoenix::ref;
prismGrammar(storm::ir::Program& program) : prismGrammar::base_type(start), program(program) {
freeIdentifierName %= qi::lexeme[(qi::alpha >> *(qi::alnum)) - allVariables_ - allConstants_];
// start = constantDefinitionList(phoenix::ref(qi::_r1), phoenix::ref(qi::_r1));
start = qi::lit(qi::_r1) >> int_;
constantDefinitionList = qi::int_;
booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BooleanLiteral>(qi::_1))];
integerLiteralExpression = qi::int_[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::IntegerLiteral>(qi::_1))];
doubleLiteralExpression = qi::double_[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::DoubleLiteral>(qi::_1))];
literalExpression %= (booleanLiteralExpression | integerLiteralExpression | doubleLiteralExpression);
variableDefinition %= (booleanVariableDefinition | integerVariableDefinition);
booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") >> qi::lit(";"))[phoenix::bind(booleanVariables_.add, qi::_1, phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(allVariables_.add, qi::_1, phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), qi::_val = phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)];
integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") >> integerConstantExpression >> qi::lit("..") >> integerConstantExpression >> qi::lit("]") >> qi::lit(";"))[phoenix::bind(integerVariables_.add, qi::_1, phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(allVariables_.add, qi::_1, phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), qi::_val = phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)];
integerVariableExpression = integerVariables_;
booleanVariableExpression = booleanVariables_;
variableExpression = (integerVariableExpression | booleanVariableExpression);
constantDefinition %= (definedConstantDefinition | undefinedConstantDefinition);
definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
undefinedConstantDefinition %= (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition);
definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") >> booleanLiteralExpression >> qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") >> integerLiteralExpression >> qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") >> doubleLiteralExpression >> qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, phoenix::new_<storm::ir::expressions::BooleanConstantExpression>(qi::_1)), phoenix::bind(allConstants_.add, qi::_1, phoenix::new_<storm::ir::expressions::BooleanConstantExpression>(qi::_1)), qi::_val = phoenix::new_<storm::ir::expressions::BooleanConstantExpression>(qi::_1)];
undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, phoenix::new_<storm::ir::expressions::IntegerConstantExpression>(qi::_1)), phoenix::bind(allConstants_.add, qi::_1, phoenix::new_<storm::ir::expressions::IntegerConstantExpression>(qi::_1)), qi::_val = phoenix::new_<storm::ir::expressions::IntegerConstantExpression>(qi::_1)];
undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, phoenix::new_<storm::ir::expressions::DoubleConstantExpression>(qi::_1)), phoenix::bind(allConstants_.add, qi::_1, phoenix::new_<storm::ir::expressions::DoubleConstantExpression>(qi::_1)), qi::_val = phoenix::new_<storm::ir::expressions::DoubleConstantExpression>(qi::_1)];
booleanConstantExpression %= (booleanConstants_ | booleanLiteralExpression);
integerConstantExpression %= (integerConstants_ | integerLiteralExpression);
doubleConstantExpression %= (doubleConstants_ | doubleLiteralExpression);
constantExpression %= (booleanConstantExpression | integerConstantExpression | doubleConstantExpression);
expression %= (booleanExpression | integerExpression | doubleExpression);
atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression);
integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
integerExpression %= integerPlusExpression;
booleanExpression %= orExpression;
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR)];
andExpression = atomicBooleanExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> atomicBooleanExpression)[qi::_val = phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND)];
atomicDoubleExpression %= (qi::lit("(") >> doubleExpression >> qi::lit(")") | doubleConstantExpression);
doubleMultExpression %= atomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicDoubleExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES))];
doublePlusExpression %= doubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> doubleMultExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS))];
doubleExpression %= doublePlusExpression;
relativeExpression = (integerExpression >> relations_ >> integerExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryRelationExpression>(qi::_1, qi::_3, qi::_2))];
atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression);
relativeExpression = (integerExpression >> relations_ >> integerExpression)[qi::_val = phoenix::new_<storm::ir::expressions::BinaryRelationExpression>(qi::_1, qi::_3, qi::_2)];
andExpression = atomicBooleanExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> atomicBooleanExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::AND))];
orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BaseExpression>>(phoenix::new_<storm::ir::expressions::BinaryBooleanFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryBooleanFunctionExpression::OR))];
booleanExpression %= orExpression;
integerExpression %= integerPlusExpression;
integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> integerMultExpression)[qi::_val = phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS)];
integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES)];
atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression);
expression %= (booleanExpression | integerExpression | doubleExpression);
doubleExpression %= doublePlusExpression;
doublePlusExpression = doubleMultExpression[qi::_val = qi::_1] >> *(qi::lit("+") >> doubleMultExpression)[qi::_val = phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS)];
doubleMultExpression %= atomicDoubleExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicDoubleExpression)[qi::_val = phoenix::new_<storm::ir::expressions::BinaryNumericalFunctionExpression>(qi::_val, qi::_1, storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES)];
atomicDoubleExpression %= (qi::lit("(") >> doubleExpression >> qi::lit(")") | doubleConstantExpression);
booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::BooleanVariable>(qi::_1), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a)];
integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") >> integerConstantExpression >> qi::lit("..") >> integerConstantExpression >> qi::lit("]") >> qi::lit(";"))[qi::_val = phoenix::construct<storm::ir::IntegerVariable>(qi::_1, qi::_2, qi::_3), qi::_a = phoenix::construct<std::shared_ptr<storm::ir::expressions::VariableExpression>>(phoenix::new_<storm::ir::expressions::VariableExpression>(qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(allVariables_.add, qi::_1, qi::_a), phoenix::bind(&storm::ir::IntegerVariable::setVariableName, qi::_val, qi::_1), phoenix::bind(&storm::ir::IntegerVariable::setLowerBound, qi::_val, qi::_2), phoenix::bind(&storm::ir::IntegerVariable::setUpperBound, qi::_val, qi::_3)];
variableDefinition = (booleanVariableDefinition[phoenix::bind(&storm::ir::Module::addBooleanVariable, qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::bind(&storm::ir::Module::addIntegerVariable, qi::_r1, qi::_1)]);
literalExpression %= (booleanLiteralExpression | integerLiteralExpression | doubleLiteralExpression);
booleanLiteralExpression = qi::bool_[qi::_val = phoenix::new_<storm::ir::expressions::BooleanLiteral>(qi::_1)];
integerLiteralExpression = qi::int_[qi::_val = phoenix::new_<storm::ir::expressions::IntegerLiteral>(qi::_1)];
doubleLiteralExpression = qi::double_[qi::_val = phoenix::new_<storm::ir::expressions::DoubleLiteral>(qi::_1)];
definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") >> booleanLiteralExpression >> qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") >> integerLiteralExpression >> qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") >> doubleLiteralExpression >> qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstants_.add, qi::_1, qi::_2), qi::_val = qi::_2];
undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit(";"))[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>>(phoenix::new_<storm::ir::expressions::BooleanConstantExpression>(qi::_1)), phoenix::bind(booleanConstants_.add, qi::_1, qi::_val), phoenix::bind(allConstants_.add, qi::_1, qi::_val), phoenix::bind(&storm::ir::Program::addBooleanUndefinedConstantExpression, program, qi::_1, qi::_val)];
undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit(";"))[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>>(phoenix::new_<storm::ir::expressions::IntegerConstantExpression>(qi::_1)), phoenix::bind(integerConstants_.add, qi::_1, qi::_val), phoenix::bind(allConstants_.add, qi::_1, qi::_val), phoenix::bind(&storm::ir::Program::addIntegerUndefinedConstantExpression, program, qi::_1, qi::_val)];
undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit(";"))[qi::_val = phoenix::construct<std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>>(phoenix::new_<storm::ir::expressions::DoubleConstantExpression>(qi::_1)), phoenix::bind(doubleConstants_.add, qi::_1, qi::_val), phoenix::bind(allConstants_.add, qi::_1, qi::_val), phoenix::bind(&storm::ir::Program::addDoubleUndefinedConstantExpression, program, qi::_1, qi::_val)];
definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
undefinedConstantDefinition %= (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition);
constantDefinition %= (definedConstantDefinition | undefinedConstantDefinition);
constantExpression %= (booleanConstantExpression | integerConstantExpression | doubleConstantExpression);
booleanConstantExpression %= (booleanConstants_ | booleanLiteralExpression);
integerConstantExpression %= (integerConstants_ | integerLiteralExpression);
doubleConstantExpression %= (doubleConstants_ | doubleLiteralExpression);
constantDefinitionList = +constantDefinition;
variableExpression = (integerVariableExpression | booleanVariableExpression);
integerVariableExpression = integerVariables_;
booleanVariableExpression = booleanVariables_;
integerVariableName %= integerVariableNames_;
booleanVariableName %= booleanVariableNames_;
freeIdentifierName %= qi::lexeme[(qi::alpha >> *(qi::alnum)) - allVariables_ - allConstants_];
assignmentDefinition = qi::lit("(") >> integerVariableName >> qi::lit("'") >> integerExpression >> qi::lit(")") | qi::lit("(") >> booleanVariableName >> qi::lit("'") >> booleanExpression >> qi::lit(")");
assignmentDefinitionList %= assignmentDefinition % "&";
updateDefinition %= doubleConstantExpression >> qi::lit(":") >> assignmentDefinitionList;
updateListDefinition = +updateDefinition;
commandDefinition %= qi::lit("[") >> freeIdentifierName >> qi::lit("]") >> booleanExpression >> qi::lit("->") >> updateListDefinition >> qi::lit(";");
moduleDefinition %= qi::lit("module") >> freeIdentifierName >> *variableDefinition(qi::_val) >> *commandDefinition >> qi::lit("endmodule");
moduleDefinitionList = +moduleDefinition;
start = constantDefinitionList >> moduleDefinitionList;
}
// The starting point of the grammar.
qi::rule<Iterator, int(std::string), ascii::space_type> start;
qi::rule<Iterator, storm::ir::Program(), ascii::space_type> start;
qi::rule<Iterator, qi::unused_type(), ascii::space_type> constantDefinitionList;
qi::rule<Iterator, std::vector<storm::ir::Module>(), ascii::space_type> moduleDefinitionList;
qi::rule<Iterator, storm::ir::Module(), ascii::space_type> moduleDefinition;
qi::rule<Iterator, qi::unused_type(storm::ir::Module&), ascii::space_type> variableDefinition;
qi::rule<Iterator, storm::ir::BooleanVariable(), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>>, ascii::space_type> booleanVariableDefinition;
qi::rule<Iterator, storm::ir::IntegerVariable(), qi::locals<std::shared_ptr<storm::ir::expressions::VariableExpression>>, ascii::space_type> integerVariableDefinition;
qi::rule<Iterator, storm::ir::Command(), ascii::space_type> commandDefinition;
qi::rule<Iterator, int(), ascii::space_type> constantDefinitionList;
qi::rule<Iterator, std::vector<storm::ir::Update>(), ascii::space_type> updateListDefinition;
qi::rule<Iterator, storm::ir::Update(), ascii::space_type> updateDefinition;
qi::rule<Iterator, std::vector<storm::ir::Assignment>(), ascii::space_type> assignmentDefinitionList;
qi::rule<Iterator, storm::ir::Assignment(), ascii::space_type> assignmentDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> variableDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> booleanVariableDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> integerVariableDefinition;
qi::rule<Iterator, std::string(), ascii::space_type> integerVariableName;
qi::rule<Iterator, std::string(), ascii::space_type> booleanVariableName;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> constantDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> undefinedConstantDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> definedConstantDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> undefinedBooleanConstantDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> undefinedIntegerConstantDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> undefinedDoubleConstantDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> definedBooleanConstantDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> definedIntegerConstantDefinition;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> definedDoubleConstantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> constantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> undefinedConstantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> definedConstantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>(), ascii::space_type> undefinedBooleanConstantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>(), ascii::space_type> undefinedIntegerConstantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>(), ascii::space_type> undefinedDoubleConstantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> definedBooleanConstantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> definedIntegerConstantDefinition;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> definedDoubleConstantDefinition;
qi::rule<Iterator, std::string(), ascii::space_type> freeIdentifierName;
// The starting point for arbitrary expressions.
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> expression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> expression;
// Rules with boolean result type.
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> booleanExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> orExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> andExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> atomicBooleanExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> relativeExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> booleanExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> orExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> andExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> atomicBooleanExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> relativeExpression;
// Rules with integer result type.
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> integerExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> integerPlusExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> integerMultExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> atomicIntegerExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerPlusExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerMultExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> atomicIntegerExpression;
// Rules with double result type.
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> doubleExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> doublePlusExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> doubleMultExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> atomicDoubleExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> doubleExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> doublePlusExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> doubleMultExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> atomicDoubleExpression;
// Rules for variable recognition.
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> variableExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> booleanVariableExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> integerVariableExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> variableExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> booleanVariableExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerVariableExpression;
// Rules for constant recognition.
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> constantExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> booleanConstantExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> integerConstantExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> doubleConstantExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> constantExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> booleanConstantExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerConstantExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> doubleConstantExpression;
// Rules for literal recognition.
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> literalExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> booleanLiteralExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> integerLiteralExpression;
qi::rule<Iterator, storm::ir::expressions::BaseExpression*(), ascii::space_type> doubleLiteralExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> literalExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> booleanLiteralExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> integerLiteralExpression;
qi::rule<Iterator, std::shared_ptr<storm::ir::expressions::BaseExpression>(), ascii::space_type> doubleLiteralExpression;
struct keywordsStruct : qi::symbols<char, unsigned> {
keywordsStruct() {
@ -222,17 +233,23 @@ private:
}
} relations_;
struct variablesStruct : qi::symbols<char, storm::ir::expressions::BaseExpression*> {
struct variablesStruct : qi::symbols<char, std::shared_ptr<storm::ir::expressions::BaseExpression>> {
// Intentionally left empty. This map is filled during parsing.
} integerVariables_, booleanVariables_, allVariables_ ;
} integerVariables_, booleanVariables_, allVariables_;
struct constantsStruct : qi::symbols<char, storm::ir::expressions::BaseExpression*> {
struct variableNamesStruct : qi::symbols<char, std::string> {
// Intentionally left empty. This map is filled during parsing.
} integerVariableNames_, booleanVariableNames_;
struct constantsStruct : qi::symbols<char, std::shared_ptr<storm::ir::expressions::BaseExpression>> {
// Intentionally left empty. This map is filled during parsing.
} integerConstants_, booleanConstants_, doubleConstants_, allConstants_;
struct modulesStruct : qi::symbols<char, unsigned> {
// Intentionally left empty. This map is filled during parsing.
} modules_;
storm::ir::Program& program;
};
};

4
src/storm.cpp
View File

@ -25,7 +25,7 @@
#include "src/modelChecker/EigenDtmcPrctlModelChecker.h"
#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h"
#include "src/parser/DtmcParser.h"
#include "src/parser/PrctlParser.h"
// #include "src/parser/PrctlParser.h"
#include "src/solver/GraphAnalyzer.h"
#include "src/utility/Settings.h"
#include "src/formula/Formulas.h"
@ -111,7 +111,7 @@ bool parseOptions(const int argc, const char* argv[]) {
return false;
}
if (s->isSet("test-prctl")) {
storm::parser::PrctlParser parser(s->getString("test-prctl").c_str());
// storm::parser::PrctlParser parser(s->getString("test-prctl").c_str());
delete s;
return false;
}

Write Preview
Loading…
Cancel
Save