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

Merge remote-tracking branch 'origin/future' into future 

Former-commit-id: 5a4d4248be [formerly acb4fca937]
Former-commit-id: 933bfd5907
main
TimQu 9 years ago
parent
f0943d57bc 2f100f2721
commit
278f33b7e4
2116 changed files with 55475 additions and 454611 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. 293
      CMakeLists.txt
  2. 49
      README.md
  3. 4
      examples/dft/and.dft
  4. 5
      examples/dft/and_approx.dft
  5. 6
      examples/dft/and_approx_param.dft
  6. 5
      examples/dft/and_param.dft
  7. 5
      examples/dft/approx.dft
  8. 4
      examples/dft/be_nonfail.dft
  9. 21
      examples/dft/cardiac.dft
  10. 24
      examples/dft/cas.dft
  11. 22
      examples/dft/cm2.dft
  12. 41
      examples/dft/cm4.dft
  13. 26
      examples/dft/cps.dft
  14. 16
      examples/dft/deathegg.dft
  15. 8
      examples/dft/fdep.dft
  16. 5
      examples/dft/fdep2.dft
  17. 5
      examples/dft/fdep3.dft
  18. 7
      examples/dft/fdep4.dft
  19. 129
      examples/dft/ftpp_complex.dft
  20. 63
      examples/dft/ftpp_large.dft
  21. 53
      examples/dft/ftpp_standard.dft
  22. 58
      examples/dft/mas.dft
  23. 22
      examples/dft/mcs.dft
  24. 26
      examples/dft/mdcs.dft
  25. 19
      examples/dft/mdcs2.dft
  26. 7
      examples/dft/mp.dft
  27. 6
      examples/dft/nonmonoton.dft
  28. 8
      examples/dft/nonmonoton_param.dft
  29. 4
      examples/dft/or.dft
  30. 4
      examples/dft/pand.dft
  31. 6
      examples/dft/pand_param.dft
  32. 12
      examples/dft/pdep.dft
  33. 9
      examples/dft/pdep2.dft
  34. 5
      examples/dft/pdep3.dft
  35. 7
      examples/dft/pdep4.dft
  36. 11
      examples/dft/pdep_symmetry.dft
  37. 5
      examples/dft/por.dft
  38. 5
      examples/dft/seq.dft
  39. 6
      examples/dft/seq2.dft
  40. 6
      examples/dft/seq3.dft
  41. 7
      examples/dft/seq4.dft
  42. 9
      examples/dft/seq5.dft
  43. 5
      examples/dft/spare.dft
  44. 8
      examples/dft/spare2.dft
  45. 10
      examples/dft/spare3.dft
  46. 9
      examples/dft/spare4.dft
  47. 9
      examples/dft/spare5.dft
  48. 7
      examples/dft/spare6.dft
  49. 5
      examples/dft/spare7.dft
  50. 7
      examples/dft/spare8.dft
  51. 5
      examples/dft/spare_cold.dft
  52. 9
      examples/dft/spare_param.dft
  53. 9
      examples/dft/spare_symmetry.dft
  54. 8
      examples/dft/symmetry.dft
  55. 8
      examples/dft/symmetry2.dft
  56. 12
      examples/dft/symmetry3.dft
  57. 12
      examples/dft/symmetry4.dft
  58. 21
      examples/dft/symmetry5.dft
  59. 10
      examples/dft/symmetry_param.dft
  60. 7
      examples/dft/symmetry_shared.dft
  61. 8
      examples/dft/tripple_and1.dft
  62. 8
      examples/dft/tripple_and2.dft
  63. 6
      examples/dft/tripple_and2_c.dft
  64. 7
      examples/dft/tripple_and_c.dft
  65. 9
      examples/dft/tripple_or.dft
  66. 8
      examples/dft/tripple_or2.dft
  67. 6
      examples/dft/tripple_or2_c.dft
  68. 7
      examples/dft/tripple_or_c.dft
  69. 9
      examples/dft/tripple_pand.dft
  70. 8
      examples/dft/tripple_pand2.dft
  71. 6
      examples/dft/tripple_pand2_c.dft
  72. 7
      examples/dft/tripple_pand_c.dft
  73. 5
      examples/dft/voting.dft
  74. 5
      examples/dft/voting2.dft
  75. 41034
      examples/gspn/HypercubeGrid/hc3k4p4b12.pnml
  76. 87274
      examples/gspn/HypercubeGrid/hc4k3p3b12.pnml
  77. 1
      examples/gspn/HypercubeGrid/hc5k3p3b15.pnml.REMOVED.git-id
  78. 5554
      examples/gspn/ibm319/IBM319.pnml
  79. 14
      examples/gspn/pnpro_test1/project01.PNPRO
  80. 148
      examples/gspn/tiny/tiny01.pnml
  81. 1236
      examples/gspn/workflow_cluster/workflow_cluster.pnml
  82. 58
      examples/pgcl/coupon/coupon10-classic.pgcl
  83. 60
      examples/pgcl/coupon/coupon10-cost.pgcl
  84. 62
      examples/pgcl/coupon/coupon10-observe.pgcl
  85. 60
      examples/pgcl/coupon/coupon10.pgcl
  86. 24
      examples/pgcl/coupon/coupon3-classic.pgcl
  87. 28
      examples/pgcl/coupon/coupon3-cost.pgcl
  88. 30
      examples/pgcl/coupon/coupon3-observe.pgcl
  89. 28
      examples/pgcl/coupon/coupon3.pgcl
  90. 34
      examples/pgcl/coupon/coupon4-observe.pgcl
  91. 32
      examples/pgcl/coupon/coupon5-classic.pgcl
  92. 36
      examples/pgcl/coupon/coupon5-cost.pgcl
  93. 38
      examples/pgcl/coupon/coupon5-observe.pgcl
  94. 36
      examples/pgcl/coupon/coupon5.pgcl
  95. 40
      examples/pgcl/coupon/coupon7-classic.pgcl
  96. 44
      examples/pgcl/coupon/coupon7-cost.pgcl
  97. 46
      examples/pgcl/coupon/coupon7-observe.pgcl
  98. 44
      examples/pgcl/coupon/coupon7.pgcl
  99. 35
      examples/pgcl/crowds/crowds100-100-observeOther.pgcl
  100. 34
      examples/pgcl/crowds/crowds100-100.pgcl

293
CMakeLists.txt
View File

@ -1,5 +1,6 @@
cmake_minimum_required (VERSION 2.8.6)
cmake_policy(VERSION 3.2)
# Set project name
project (storm CXX C)
@ -7,28 +8,26 @@ project (storm CXX C)
include_directories("${PROJECT_SOURCE_DIR}")
include_directories("${PROJECT_SOURCE_DIR}/src")
# Add the resources/cmake folder to Module Search Path for FindTBB.cmake
set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmake/find_modules" "${PROJECT_SOURCE_DIR}/resources/cmake/macros")
include(ExternalProject)
include(RegisterSourceGroup)
#############################################################
##
## CMake options of StoRM
## CMake options of Storm
##
#############################################################
option(STORM_DEVELOPER "Sets whether the development mode is used" OFF)
option(STORM_DEVELOPER "Sets whether the development mode is used." OFF)
option(STORM_ALLWARNINGS "Compile with even more warnings" OFF)
option(STORM_PORTABLE_RELEASE "Sets whether a release build needs to be portable to another machine. This is only effective for release builds in non-development mode." OFF)
MARK_AS_ADVANCED(STORM_PORTABLE_RELEASE)
option(STORM_USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON)
MARK_AS_ADVANCED(STORM_USE_POPCNT)
option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." ON)
option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." OFF)
option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF)
option(STORM_USE_GUROBI "Sets whether Gurobi should be used." OFF)
option(STORM_USE_COTIRE "Sets whether Cotire should be used (for building precompiled headers)." OFF)
option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF)
option(USE_LIBCXX "Sets whether the standard library is libc++." OFF)
option(USE_CARL "Sets whether carl should be included." ON)
option(USE_SMTRAT "Sets whether SMT-RAT should be included." OFF)
option(USE_HYPRO "Sets whether HyPro should be included." OFF)
@ -55,23 +54,27 @@ mark_as_advanced(CMAKE_OSX_ARCHITECTURES)
mark_as_advanced(CMAKE_OSX_SYSROOT)
mark_as_advanced(CMAKE_OSX_DEPLOYMENT_TARGET)
# If the STORM_DEVELOPER option was turned on, we will target a debug version.
# By default, we build a release version.
if (NOT CMAKE_BUILD_TYPE)
set(CMAKE_BUILD_TYPE "RELEASE")
endif()
# If the STORM_DEVELOPER option was turned on, we target a debug version.
if (STORM_DEVELOPER)
message(STATUS "StoRM - Using development mode")
set(CMAKE_BUILD_TYPE "DEBUG" CACHE STRING "Set the build type" FORCE)
set(CMAKE_BUILD_TYPE "DEBUG")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DSTORM_DEV")
endif()
message(STATUS "StoRM - Building ${CMAKE_BUILD_TYPE} version.")
message(STATUS "Storm - Building ${CMAKE_BUILD_TYPE} version.")
if(STORM_COMPILE_WITH_CCACHE)
find_program(CCACHE_FOUND ccache)
mark_as_advanced(CCACHE_FOUND)
if(CCACHE_FOUND)
message(STATUS "StoRM - Using ccache")
message(STATUS "Storm - Using ccache")
set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache)
set_property(GLOBAL PROPERTY RULE_LAUNCH_LINK ccache)
else()
message(STATUS "Could not find ccache")
message(STATUS "Storm - Could not find ccache.")
endif()
endif()
@ -100,8 +103,7 @@ else()
set(OPERATING_SYSTEM "Linux")
set(LINUX 1)
ENDIF()
message(STATUS "Operating system: ${OPERATING_SYSTEM}")
message(STATUS "Storm - Detected operating system ${OPERATING_SYSTEM}.")
set(DYNAMIC_EXT ".so")
set(STATIC_EXT ".a")
@ -115,161 +117,160 @@ endif()
message(STATUS "Assuming extension for shared libraries: ${DYNAMIC_EXT}")
message(STATUS "Assuming extension for static libraries: ${STATIC_EXT}")
#############################################################
##
## Compiler specific settings and definitions
## Compiler detection and initial configuration
##
#############################################################
# Path to the no-strict-aliasing target
set(CONVERSIONHELPER_TARGET "${PROJECT_SOURCE_DIR}/src/utility/ConversionHelper.cpp")
if(CMAKE_COMPILER_IS_GNUCC)
set(STORM_COMPILED_BY "GCC")
# Set standard flags for GCC
set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops")
set(CMAKE_C_FLAGS_RELEASE "${CMAKE_C_FLAGS_RELEASE} -funroll-loops")
# TODO: remove forcing the old version of optional as soon as the related Spirit bug is fixed:
# https://svn.boost.org/trac/boost/ticket/12349
# Fix thanks to: https://github.com/freeorion/freeorion/issues/777
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE -DBOOST_OPTIONAL_CONFIG_USE_OLD_IMPLEMENTATION_OF_OPTIONAL)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs -Wno-unknown-pragmas")
set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations")
if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 5.0)
message(FATAL_ERROR "GCC version must be at least 5.0!")
endif()
# Turn on popcnt instruction if desired (yes by default)
if (STORM_USE_POPCNT)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt")
endif(STORM_USE_POPCNT)
# Set the no-strict-aliasing target for GCC
set_source_files_properties(${CONVERSIONHELPER_TARGET} PROPERTIES COMPILE_FLAGS " -fno-strict-aliasing")
elseif(MSVC)
set(STORM_COMPILED_BY "MSVC")
# required for GMM to compile, ugly error directive in their code
add_definitions(/D_SCL_SECURE_NO_DEPRECATE /D_CRT_SECURE_NO_WARNINGS)
# required as the PRCTL Parser bloats object files (COFF) beyond their maximum size (see http://msdn.microsoft.com/en-us/library/8578y171(v=vs.110).aspx)
add_definitions(/bigobj)
# required by GTest and PrismGrammar::createIntegerVariable
add_definitions(/D_VARIADIC_MAX=10)
# Windows.h breaks GMM in gmm_except.h because of its macro definition for min and max
add_definitions(/DNOMINMAX)
# Boost Defs, required for using boost's transform iterator
add_definitions(/DBOOST_RESULT_OF_USE_DECLTYPE)
# since nobody cares at the moment
add_definitions(/wd4250)
# MSVC does not do strict-aliasing, so no option needed
else(CLANG)
set(STORM_COMPILED_BY "Clang (LLVM)")
# As CLANG is not set as a variable, we need to set it in case we have not matched another compiler.
set (CLANG ON)
# Set standard flags for clang
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3")
if(UNIX AND NOT APPLE)
if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 3.2)
message(FATAL_ERROR "Clang version must be at least 3.2!")
endif()
if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang")
# using Clang
if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 3.2)
message(FATAL_ERROR "Clang version must be at least 3.2.")
endif()
if(UNIX AND APPLE)
if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 7.3)
message(FATAL_ERROR "Clang version must be at least 7.3!")
endif()
set(STORM_COMPILER_CLANG ON)
set(CLANG ON)
set(STORM_COMPILER_ID "clang")
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
# using GCC
if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 7.3)
message(FATAL_ERROR "AppleClang version must be at least 7.3.")
endif()
if(UNIX AND NOT APPLE AND NOT USE_LIBCXX)
set(CLANG_STDLIB libstdc++)
message(STATUS "StoRM - Linking against libstdc++")
else()
set(CLANG_STDLIB libc++)
message(STATUS "StoRM - Linking against libc++")
# Disable Cotire
set(STORM_USE_COTIRE OFF)
# Set up some Xcode specific settings
set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LANGUAGE_STANDARD "c++11")
set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LIBRARY "libc++")
endif()
# TODO: remove forcing the old version of optional as soon as the related Spirit bug is fixed:
# https://svn.boost.org/trac/boost/ticket/12349
# Fix thanks to: https://github.com/freeorion/freeorion/issues/777
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE -DBOOST_OPTIONAL_CONFIG_USE_OLD_IMPLEMENTATION_OF_OPTIONAL)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -stdlib=${CLANG_STDLIB} -Wall -pedantic -Wno-newline-eof -Wno-mismatched-tags -Wno-unused-local-typedefs -ftemplate-depth=1024 -Wno-parentheses-equality")
if(FORCE_COLOR)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics")
endif()
# Turn on popcnt instruction if desired (yes by default)
if (STORM_USE_POPCNT)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt")
endif(STORM_USE_POPCNT)
set(STORM_COMPILER_APPLECLANG ON)
set(CLANG ON)
set(STORM_COMPILER_ID "AppleClang")
set(CMAKE_MACOSX_RPATH ON)
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
# using GCC
if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 5.0)
message(FATAL_ERROR "gcc version must be at least 5.0.")
endif()
# Set the no-strict-aliasing target for Clang
set_source_files_properties(${CONVERSIONHELPER_TARGET} PROPERTIES COMPILE_FLAGS " -fno-strict-aliasing ")
set(STORM_COMPILER_GCC ON)
set(STORM_COMPILER_ID "gcc")
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Intel")
message(FATAL_ERROR "Intel compiler is currently not supported.")
elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
message(FATAL_ERROR "Visual Studio compiler is currently not supported.")
endif()
if(CCACHE_FOUND)
set(STORM_COMPILED_BY "${STORM_COMPILED_BY} (ccache)")
set(STORM_COMPILER_ID "${STORM_COMPILER_ID} (ccache)")
endif()
message(STATUS "StoRM - Using Compiler Configuration: ${STORM_COMPILED_BY}")
#############################################################
#############################################################
##
## Inclusion of required libraries
## Compiler independent settings
##
#############################################################
#############################################################
if (STORM_USE_POPCNT)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt")
endif()
# TODO: remove forcing the old version of optional as soon as the related Spirit bug is fixed:
# https://svn.boost.org/trac/boost/ticket/12349
# Fix thanks to: https://github.com/freeorion/freeorion/issues/777
add_definitions(-DBOOST_RESULT_OF_USE_DECLTYPE -DBOOST_OPTIONAL_CONFIG_USE_OLD_IMPLEMENTATION_OF_OPTIONAL)
#############################################################
##
## Include the targets for non-system resources
## Compiler specific settings
##
#############################################################
if (STORM_COMPILER_CLANG OR STORM_COMPILER_APPLECLANG)
if(FORCE_COLOR)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -fcolor-diagnostics")
endif()
if (LINUX)
set(CLANG_STDLIB libstdc++)
else()
set(CLANG_STDLIB libc++)
endif()
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14 -stdlib=${CLANG_STDLIB} -ftemplate-depth=1024")
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto -ffast-math -fno-finite-math-only")
set (CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -Wl,-export_dynamic")
set (CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,-export_dynamic")
elseif (STORM_COMPILER_GCC)
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++14")
set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -flto -fprefetch-loop-arrays -ffast-math -fno-finite-math-only")
set(CMAKE_SHARED_LINKER_FLAGS "${CMAKE_SHARED_LINKER_FLAGS} -rdynamic")
set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -rdynamic")
endif ()
# In release mode, we turn on even more optimizations if we do not have to provide a portable binary.
if (NOT STORM_PORTABLE_RELEASE)
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -march=native")
endif ()
# In 3rdparty, targets are being defined that can be used
# in the the system does not have a library
include(resources/3rdparty/CMakeLists.txt)
if (STORM_DEVELOPER)
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -pedantic")
if (STORM_ALLWARNINGS)
if (CLANG)
# Enable strictly every warning and then disable selected ones.
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Weverything")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-c++98-compat -Wno-c++98-compat-pedantic")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-old-style-cast")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-reserved-id-macro")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-newline-eof")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-documentation")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-weak-vtables")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-global-constructors")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-exit-time-destructors")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-switch-enum")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-covered-switch-default")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-padded")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-float-equal")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-unused-local-typedef")
set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-missing-variable-declarations")
endif ()
else ()
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wextra")
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-unknown-pragmas")
set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-unused-local-typedefs")
endif ()
else()
set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fomit-frame-pointer")
endif()
#############################################################
##
## Cotire
## Generator specific settings
##
#############################################################
message (STATUS "StoRM - Using Cotire: ${STORM_USE_COTIRE}")
if (STORM_USE_COTIRE)
# Include Cotire for PCH Generation
set (CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/resources/cmake")
include(cotire)
if ("${CMAKE_GENERATOR}" STREQUAL "Xcode")
set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LANGUAGE_STANDARD "c++11")
set(CMAKE_XCODE_ATTRIBUTE_CLANG_CXX_LIBRARY "libc++")
endif()
cotire(storm)
target_link_libraries(storm_unity ${Boost_LIBRARIES})
#cotire(storm-functional-tests)
#cotire(storm-performance-tests)
# Display information about build configuration.
message(STATUS "Storm - Using compiler configuration ${STORM_COMPILER_ID}.")
if (STORM_DEVELOPER)
message(STATUS "Storm - CXX Flags: ${CMAKE_CXX_FLAGS}")
message(STATUS "Storm - CXX Debug Flags: ${CMAKE_CXX_FLAGS_DEBUG}")
message(STATUS "Storm - CXX Release Flags: ${CMAKE_CXX_FLAGS_RELEASE}")
message(STATUS "Storm - Build type: ${CMAKE_BUILD_TYPE}")
endif()
#############################################################
#############################################################
##
## Inclusion of required libraries
##
#############################################################
#############################################################
#############################################################
##
## libc++abi
## Include the targets for non-system resources
##
#############################################################
# Link against libc++abi if requested. May be needed to build on Linux systems using clang.
if (LINK_LIBCXXABI)
message (STATUS "StoRM - Linking against libc++abi.")
target_link_libraries(storm "c++abi")
endif(LINK_LIBCXXABI)
# In 3rdparty, targets are being defined that can be used
# in the the system does not have a library
include(resources/3rdparty/CMakeLists.txt)
#############################################################
##
@ -290,16 +291,14 @@ endif(DOXYGEN_FOUND)
#############################################################
##
## CMake-generated Config File for StoRM
## CMake-generated Config File for Storm
##
#############################################################
#
# Make a version file containing the current version from git.
#
include(GetGitRevisionDescription)
git_describe_checkout(STORM_GIT_VERSION_STRING)
message(STATUS "STORM_GIT_VERSION_STRING: ${STORM_GIT_VERSION_STRING}")
message(STATUS "Storm -- Git version string is ${STORM_GIT_VERSION_STRING}.")
# Parse the git Tag into variables
string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_CPP_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}")
string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_CPP_VERSION_MINOR "${STORM_GIT_VERSION_STRING}")
@ -312,7 +311,7 @@ if ("${STORM_CPP_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
else()
set(STORM_CPP_VERSION_DIRTY 0)
endif()
message(STATUS "StoRM - Version information: ${STORM_CPP_VERSION_MAJOR}.${STORM_CPP_VERSION_MINOR}.${STORM_CPP_VERSION_PATCH} (${STORM_CPP_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CPP_VERSION_HASH} (Dirty: ${STORM_CPP_VERSION_DIRTY})")
message(STATUS "Storm - Version is ${STORM_CPP_VERSION_MAJOR}.${STORM_CPP_VERSION_MINOR}.${STORM_CPP_VERSION_PATCH} (${STORM_CPP_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CPP_VERSION_HASH} (Dirty: ${STORM_CPP_VERSION_DIRTY}).")
# Configure a header file to pass some of the CMake settings to the source code
configure_file (
@ -334,18 +333,4 @@ include_directories("${PROJECT_BINARY_DIR}/include")
add_subdirectory(src)
add_subdirectory(test)
#############################################################
##
## memcheck targets
##
#############################################################
add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm -v --fix-deadlocks ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab DEPENDS storm)
add_custom_target(memcheck-functional-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-functional-tests -v --fix-deadlocks DEPENDS storm-functional-tests)
add_custom_target(memcheck-performance-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-performance-tests -v --fix-deadlocks DEPENDS storm-performance-tests)
set(CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams)
add_custom_target(style python resources/3rdparty/cpplint/cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp" `)
include(StormCPackConfig.cmake)

49
README.md
View File

@ -1 +1,50 @@
Storm
==============================
For more instructions, check out the documentation found in [Getting Started](doc/getting-started.md)
Benchmarks
----------------------------
Some examples can be found in the example folder:
Further example input files for storm can be found in the following repositories:
* **Prism files** (DTMC, MDP, CTMC):
http://www.prismmodelchecker.org/benchmarks/
* **Jani files** (DTMC, MDP, CTMC, MA):
http://jani-spec.org/
* MRMC style **tra** files:
(private, contact: dehnert@cs.rwth-aachen.d)
* **GSPN**s:
(private, contact: sebastian.junges@cs.rwth-aachen.de)
* **DFT**s:
https://github.com/moves-rwth/dft-examples
* **PGCL**:
(private, contact: sebastian.junges@cs.rwth-aachen.de)
Authors
-----------------------------
Storm has been developed at RWTH Aachen University
###### Principal developers
* Christian Dehnert
* Joost-Pieter Katoen
* Sebastian Junges
* Matthias Volk
###### Developers (lexicographical order)
* Philipp Berger
* David Korzeniewski
* Tim Quatmann
###### Contributors (lexicographical order)
* Dimitri Bohlender
* Harold Bruintjes
* Thomas Heinemann
* Thomas Henn
* Tom Janson
* Gereon Kremer
* Manuel Sascha Weiand
* Lukas Westhofen

4
examples/dft/and.dft
View File

@ -1,4 +0,0 @@
toplevel "A";
"A" and "B" "C";
"B" lambda=0.5 dorm=0.3;
"C" lambda=0.5 dorm=0.3;

5
examples/dft/and_approx.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" and "B" "C" "D";
"B" lambda=1 dorm=0;
"C" lambda=100 dorm=0;
"D" lambda=50 dorm=0;

6
examples/dft/and_approx_param.dft
View File

@ -1,6 +0,0 @@
param x;
toplevel "A";
"A" and "B" "C" "D";
"B" lambda=1 dorm=0;
"C" lambda=100 dorm=0;
"D" lambda=100*x dorm=0;

5
examples/dft/and_param.dft
View File

@ -1,5 +0,0 @@
param x;
toplevel "A";
"A" and "B" "C";
"B" lambda=0.5 dorm=0.3;
"C" lambda=x dorm=0.3;

5
examples/dft/approx.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" and "B" "C" "D";
"B" lambda=0.1 dorm=0;
"C" lambda=10 dorm=0;
"D" lambda=0.1 dorm=0;

4
examples/dft/be_nonfail.dft
View File

@ -1,4 +0,0 @@
toplevel "A";
"A" and "B" "C";
"B" lambda=0 dorm=0.3;
"C" lambda=0.5 dorm=0.3;

21
examples/dft/cardiac.dft
View File

@ -1,21 +0,0 @@
toplevel "SYSTEM";
"SYSTEM" or "FDEP" "CPU" "MOTOR" "PUMPS";
"FDEP" fdep "TRIGGER" "P" "B";
"TRIGGER" or "CS" "SS";
"CPU" wsp "P" "B";
"MOTOR" or "SWITCH" "MOTORS";
"SWITCH" pand "MS" "MA";
"MOTORS" csp "MA" "MB";
"PUMPS" and "PUMP1" "PUMP2";
"PUMP1" csp "PA" "PS";
"PUMP2" csp "PB" "PS";
"P" lambda=5.0e-5 dorm=0;
"B" lambda=5.0e-5 dorm=0.5;
"CS" lambda=2.0e-5 dorm=0;
"SS" lambda=2.0e-5 dorm=0;
"MS" lambda=1.0e-6 dorm=0;
"MA" lambda=1.0e-4 dorm=0;
"MB" lambda=1.0e-4 dorm=0;
"PA" lambda=1.0e-4 dorm=0;
"PB" lambda=1.0e-4 dorm=0;
"PS" lambda=1.0e-4 dorm=0;

24
examples/dft/cas.dft
View File

@ -1,24 +0,0 @@
toplevel "System";
"System" or "CPUfdep" "CPUunit" "Motorunit" "Pumpunit";
"CPUfdep" fdep "trigger" "P" "B";
"trigger" or "CS" "SS";
"CS" lambda=0.2 dorm=0;
"SS" lambda=0.2 dorm=0;
"CPUunit" wsp "P" "B";
"P" lambda=0.5 dorm=0;
"B" lambda=0.5 dorm=0.5;
"Motorunit" or "MP" "Motors";
"MP" pand "MS" "MA";
"Motors" csp "MA" "MB";
"MS" lambda=0.01 dorm=0;
"MA" lambda=1 dorm=0;
"MB" lambda=1 dorm=0;
"Pumpunit" and "PumpA" "PumpB";
"PumpA" csp "PA" "PS";
"PumpB" csp "PB" "PS";
"PA" lambda=1 dorm=0;
"PB" lambda=1 dorm=0;
"PS" lambda=1 dorm=0;

22
examples/dft/cm2.dft
View File

@ -1,22 +0,0 @@
toplevel "System";
"System" or "BUS" "CM";
"CM" and "CM1" "CM2";
"CM1" or "DISK1" "POWER1" "MEMORY1";
"CM2" or "DISK2" "POWER2" "MEMORY2";
"DISK1" wsp "D11" "D12";
"DISK2" wsp "D21" "D22";
"POWER1" or "P1" "PS";
"POWER2" or "P2" "PS";
"MEMORY1" wsp "M1" "M3";
"MEMORY2" wsp "M2" "M3";
"BUS" lambda=0.0002 dorm=0;
"P1" lambda=0.05 dorm=0;
"P2" lambda=0.05 dorm=0;
"PS" lambda=0.6 dorm=0;
"D11" lambda=8.0 dorm=0;
"D12" lambda=8.0 dorm=0.5;
"D21" lambda=8.0 dorm=0;
"D22" lambda=8.0 dorm=0.5;
"M1" lambda=0.003 dorm=0;
"M2" lambda=0.003 dorm=0;
"M3" lambda=0.003 dorm=0.5;

41
examples/dft/cm4.dft
View File

@ -1,41 +0,0 @@
toplevel "System";
"System" or "BUS" "CM";
"CM" and "CM1" "CM2" "CM3" "CM4";
"CM1" or "DISK1" "POWER1" "MEMORY1";
"CM2" or "DISK2" "POWER2" "MEMORY2";
"CM3" or "DISK3" "POWER3" "MEMORY3";
"CM4" or "DISK4" "POWER4" "MEMORY4";
"DISK1" wsp "D11" "D12";
"DISK2" wsp "D21" "D22";
"DISK3" wsp "D31" "D32";
"DISK4" wsp "D41" "D42";
"POWER1" or "P1" "PS";
"POWER2" or "P2" "PS";
"POWER3" or "P3" "PS2";
"POWER4" or "P4" "PS2";
"MEMORY1" wsp "M1" "M3" "M4";
"MEMORY2" wsp "M2" "M3" "M4";
"MEMORY3" wsp "M31" "M3";
"MEMORY4" wsp "M41" "M4";
"BUS" lambda=0.0002 dorm=0;
"P1" lambda=0.05 dorm=0;
"P2" lambda=0.05 dorm=0;
"P3" lambda=0.05 dorm=0;
"P4" lambda=0.05 dorm=0;
"PS" lambda=0.6 dorm=0;
"PS2" lambda=0.6 dorm=0;
"D11" lambda=8.0 dorm=0;
"D12" lambda=8.0 dorm=0.5;
"D21" lambda=8.0 dorm=0;
"D22" lambda=8.0 dorm=0.5;
"D31" lambda=8.0 dorm=0;
"D32" lambda=8.0 dorm=0.5;
"D41" lambda=8.0 dorm=0;
"D42" lambda=8.0 dorm=0.5;
"M1" lambda=0.003 dorm=0;
"M2" lambda=0.003 dorm=0;
"M31" lambda=0.003 dorm=0;
"M41" lambda=0.003 dorm=0;
"M3" lambda=0.003 dorm=0.5;
"M4" lambda=0.003 dorm=0.5;

26
examples/dft/cps.dft
View File

@ -1,26 +0,0 @@
toplevel "System";
"System" pand "A" "B";
"A" and "AA" "AB" "AC" "AD";
"B" pand "C" "D";
"C" and "CA" "CB" "CC" "CD";
"D" and "DA" "DB" "DC" "DD";
"AA" lambda=1 dorm=0;
"AB" lambda=1 dorm=0;
"AC" lambda=1 dorm=0;
"AD" lambda=1 dorm=0;
"CA" lambda=1 dorm=0;
"CB" lambda=1 dorm=0;
"CC" lambda=1 dorm=0;
"CD" lambda=1 dorm=0;
"DA" lambda=1 dorm=0;
"DB" lambda=1 dorm=0;
"DC" lambda=1 dorm=0;
"DD" lambda=1 dorm=0;

16
examples/dft/deathegg.dft
View File

@ -1,16 +0,0 @@
toplevel "DeathEgg";
"DeathEgg" or "DeathEggProxy" "DeathEggServer" "CampusPowerDependency" "ProxyPowerDependency";
"DeathEggServer" or "CampusNET" "DES_Disks";
"DES_Disks" and "DES_Disks_RAID1" "DES_Disks_RAID2";
"DES_Disks_RAID1" and "DES_Disk_1" "DES_Disk_2";
"DES_Disks_RAID2" and "DES_Disk_3" "DES_Disk_4";
"DeathEggProxy" lambda=0.01 dorm=0;
"DES_Disk_1" lambda=0.01 dorm=0;
"DES_Disk_2" lambda=0.01 dorm=0;
"DES_Disk_3" lambda=0.01 dorm=0;
"DES_Disk_4" lambda=0.01 dorm=0;
"CampusPowerDependency" fdep "CampusPower" "DeathEggServer";
"ProxyPowerDependency" fdep "ProxyPower" "DeathEggProxy";
"CampusPower" lambda=0.01 dorm=0;
"CampusNET" lambda=0.01 dorm=0;
"ProxyPower" lambda=0.01 dorm=0;

8
examples/dft/fdep.dft
View File

@ -1,8 +0,0 @@
toplevel "System";
"System" or "Power" "Machine";
"Power" fdep "B_Power" "P" "B";
"Machine" or "P" "B";
"B_Power" lambda=0.5 dorm=0;
"P" lambda=0.5 dorm=0;
"B" lambda=0.5 dorm=0.5;

5
examples/dft/fdep2.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" and "B" "C";
"F" fdep "B" "C";
"B" lambda=0.5 dorm=0;
"C" lambda=0.5 dorm=0;

5
examples/dft/fdep3.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" and "B" "C" "F";
"F" fdep "B" "C";
"B" lambda=0.4 dorm=0;
"C" lambda=0.8 dorm=0;

7
examples/dft/fdep4.dft
View File

@ -1,7 +0,0 @@
toplevel "A";
"A" or "F" "B";
"F" fdep "E" "C" "D";
"B" wsp "C" "D";
"C" lambda=1 dorm=0;
"D" lambda=1 dorm=0.5;
"E" lambda=0.5 dorm=0;

129
examples/dft/ftpp_complex.dft
View File

@ -1,129 +0,0 @@
toplevel "System";
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD";
"triadA" 2of3 "aA" "bA" "cA";
"aA" csp "TAA" "TAS";
"bA" csp "TAB" "TAS";
"cA" csp "TAC" "TAS";
"triadB" 2of3 "aB" "bB" "cB";
"aB" csp "TBA" "TBS";
"bB" csp "TBB" "TBS";
"cB" csp "TBC" "TBS";
"triadC" 2of3 "aC" "bC" "cC";
"aC" csp "TCA" "TCS";
"bC" csp "TCB" "TCS";
"cC" csp "TCC" "TCS";
"triadD" 2of3 "aD" "bD" "cD";
"aD" csp "TDA" "TDS";
"bD" csp "TDB" "TDS";
"cD" csp "TDC" "TDS";
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA";
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB";
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC";
"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS";
"NEA" lambda=0.017 dorm=1;
"NEB" lambda=0.017 dorm=1;
"NEC" lambda=0.017 dorm=1;
"NED" lambda=0.017 dorm=1;
"TAA" or "cpuAA" "memAA";
"memAA" csp "memAA1" "memAA2";
"cpuAA" lambda=0.11 dorm=0;
"memAA1" lambda=0.11 dorm=0;
"memAA2" lambda=0.11 dorm=0;
"TAB" or "cpuAB" "memAB";
"memAB" csp "memAB1" "memAB2";
"cpuAB" lambda=0.11 dorm=0;
"memAB1" lambda=0.11 dorm=0;
"memAB2" lambda=0.11 dorm=0;
"TAC" or "cpuAC" "memAC";
"memAC" csp "memAC1" "memAC2";
"cpuAC" lambda=0.11 dorm=0;
"memAC1" lambda=0.11 dorm=0;
"memAC2" lambda=0.11 dorm=0;
"TAS" or "cpuAS" "memAS";
"memAS" csp "memAS1" "memAS2";
"cpuAS" lambda=0.11 dorm=0;
"memAS1" lambda=0.11 dorm=0;
"memAS2" lambda=0.11 dorm=0;
"TBA" or "cpuBA" "memBA";
"memBA" csp "memBA1" "memBA2";
"cpuBA" lambda=0.11 dorm=0;
"memBA1" lambda=0.11 dorm=0;
"memBA2" lambda=0.11 dorm=0;
"TBB" or "cpuBB" "memBB";
"memBB" csp "memBB1" "memBB2";
"cpuBB" lambda=0.11 dorm=0;
"memBB1" lambda=0.11 dorm=0;
"memBB2" lambda=0.11 dorm=0;
"TBC" or "cpuBC" "memBC";
"memBC" csp "memBC1" "memBC2";
"cpuBC" lambda=0.11 dorm=0;
"memBC1" lambda=0.11 dorm=0;
"memBC2" lambda=0.11 dorm=0;
"TBS" or "cpuBS" "memBS";
"memBS" csp "memBS1" "memBS2";
"cpuBS" lambda=0.11 dorm=0;
"memBS1" lambda=0.11 dorm=0;
"memBS2" lambda=0.11 dorm=0;
"TCA" or "cpuCA" "memCA";
"memCA" csp "memCA1" "memCA2";
"cpuCA" lambda=0.11 dorm=0;
"memCA1" lambda=0.11 dorm=0;
"memCA2" lambda=0.11 dorm=0;
"TCB" or "cpuCB" "memCB";
"memCB" csp "memCB1" "memCB2";
"cpuCB" lambda=0.11 dorm=0;
"memCB1" lambda=0.11 dorm=0;
"memCB2" lambda=0.11 dorm=0;
"TCC" or "cpuCC" "memCC";
"memCC" csp "memCC1" "memCC2";
"cpuCC" lambda=0.11 dorm=0;
"memCC1" lambda=0.11 dorm=0;
"memCC2" lambda=0.11 dorm=0;
"TCS" or "cpuCS" "memCS";
"memCS" csp "memCS1" "memCS2";
"cpuCS" lambda=0.11 dorm=0;
"memCS1" lambda=0.11 dorm=0;
"memCS2" lambda=0.11 dorm=0;
"TDA" or "cpuDA" "memDA";
"memDA" csp "memDA1" "memDA2";
"cpuDA" lambda=0.11 dorm=0;
"memDA1" lambda=0.11 dorm=0;
"memDA2" lambda=0.11 dorm=0;
"TDB" or "cpuDB" "memDB";
"memDB" csp "memDB1" "memDB2";
"cpuDB" lambda=0.11 dorm=0;
"memDB1" lambda=0.11 dorm=0;
"memDB2" lambda=0.11 dorm=0;
"TDC" or "cpuDC" "memDC";
"memDC" csp "memDC1" "memDC2";
"cpuDC" lambda=0.11 dorm=0;
"memDC1" lambda=0.11 dorm=0;
"memDC2" lambda=0.11 dorm=0;
"TDS" or "cpuDS" "memDS";
"memDS" csp "memDS1" "memDS2";
"cpuDS" lambda=0.11 dorm=0;
"memDS1" lambda=0.11 dorm=0;
"memDS2" lambda=0.11 dorm=0;

63
examples/dft/ftpp_large.dft
View File

@ -1,63 +0,0 @@
toplevel "System";
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD" "fE";
"triadA" 3of4 "aA" "bA" "cA" "dA";
"aA" csp "TAA" "TAS";
"bA" csp "TAB" "TAS";
"cA" csp "TAC" "TAS";
"dA" csp "TAD" "TAS";
"triadB" 3of4 "aB" "bB" "cB" "dB";
"aB" csp "TBA" "TBS";
"bB" csp "TBB" "TBS";
"cB" csp "TBC" "TBS";
"dB" csp "TBD" "TBS";
"triadC" 3of4 "aC" "bC" "cC" "dC";
"aC" csp "TCA" "TCS";
"bC" csp "TCB" "TCS";
"cC" csp "TCC" "TCS";
"dC" csp "TCD" "TCS";
"triadD" 3of4 "aD" "bD" "cD" "dD";
"aD" csp "TDA" "TDS";
"bD" csp "TDB" "TDS";
"cD" csp "TDC" "TDS";
"dD" csp "TDD" "TDS";
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA";
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB";
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC";
"fD" fdep "NED" "TAD" "TBD" "TCD" "TDD";
"fE" fdep "NEE" "TAS" "TBS" "TCS" "TDS";
"NEA" lambda=0.017 dorm=1;
"NEB" lambda=0.017 dorm=1;
"NEC" lambda=0.017 dorm=1;
"NED" lambda=0.017 dorm=1;
"NEE" lambda=0.017 dorm=1;
"TAA" lambda=0.11 dorm=0;
"TAB" lambda=0.11 dorm=0;
"TAC" lambda=0.11 dorm=0;
"TAD" lambda=0.11 dorm=0;
"TAS" lambda=0.11 dorm=0;
"TBA" lambda=0.11 dorm=0;
"TBB" lambda=0.11 dorm=0;
"TBC" lambda=0.11 dorm=0;
"TBD" lambda=0.11 dorm=0;
"TBS" lambda=0.11 dorm=0;
"TCA" lambda=0.11 dorm=0;
"TCB" lambda=0.11 dorm=0;
"TCC" lambda=0.11 dorm=0;
"TCD" lambda=0.11 dorm=0;
"TCS" lambda=0.11 dorm=0;
"TDA" lambda=0.11 dorm=0;
"TDB" lambda=0.11 dorm=0;
"TDC" lambda=0.11 dorm=0;
"TDD" lambda=0.11 dorm=0;
"TDS" lambda=0.11 dorm=0;

53
examples/dft/ftpp_standard.dft
View File

@ -1,53 +0,0 @@
toplevel "System";
"System" or "triadA" "triadB" "triadC" "triadD" "fA" "fB" "fC" "fD";
"triadA" 2of3 "aA" "bA" "cA";
"aA" csp "TAA" "TAS";
"bA" csp "TAB" "TAS";
"cA" csp "TAC" "TAS";
"triadB" 2of3 "aB" "bB" "cB";
"aB" csp "TBA" "TBS";
"bB" csp "TBB" "TBS";
"cB" csp "TBC" "TBS";
"triadC" 2of3 "aC" "bC" "cC";
"aC" csp "TCA" "TCS";
"bC" csp "TCB" "TCS";
"cC" csp "TCC" "TCS";
"triadD" 2of3 "aD" "bD" "cD";
"aD" csp "TDA" "TDS";
"bD" csp "TDB" "TDS";
"cD" csp "TDC" "TDS";
"fA" fdep "NEA" "TAA" "TBA" "TCA" "TDA";
"fB" fdep "NEB" "TAB" "TBB" "TCB" "TDB";
"fC" fdep "NEC" "TAC" "TBC" "TCC" "TDC";
"fD" fdep "NED" "TAS" "TBS" "TCS" "TDS";
"NEA" lambda=0.017 dorm=1;
"NEB" lambda=0.017 dorm=1;
"NEC" lambda=0.017 dorm=1;
"NED" lambda=0.017 dorm=1;
"TAA" lambda=0.11 dorm=0;
"TAB" lambda=0.11 dorm=0;
"TAC" lambda=0.11 dorm=0;
"TAS" lambda=0.11 dorm=0;
"TBA" lambda=0.11 dorm=0;
"TBB" lambda=0.11 dorm=0;
"TBC" lambda=0.11 dorm=0;
"TBS" lambda=0.11 dorm=0;
"TCA" lambda=0.11 dorm=0;
"TCB" lambda=0.11 dorm=0;
"TCC" lambda=0.11 dorm=0;
"TCS" lambda=0.11 dorm=0;
"TDA" lambda=0.11 dorm=0;
"TDB" lambda=0.11 dorm=0;
"TDC" lambda=0.11 dorm=0;
"TDS" lambda=0.11 dorm=0;

58
examples/dft/mas.dft
View File

@ -1,58 +0,0 @@
toplevel "MAS";
"MAS" or "CPU" "DB" "MB" "VMB" "MEM" "VMS";
"CPU" or "CW" "SO1" "SO2" "PG" "SM";
"CW" and "CWA" "CWB";
"SO1" and "SO1A" "SO1B";
"SO2" and "SO2A" "SO2B";
"PG" and "PGA" "PGB";
"SM" and "SMA" "SMB";
"CWA" csp "CWAev" "S1" "S2";
"CWB" csp "CWBev" "S1" "S2";
"SO1A" csp "SO1Aev" "S1" "S2";
"SO1B" csp "SO1Bev" "S1" "S2";
"SO2A" csp "SO2Aev" "S1" "S2";
"SO2B" csp "SO2Bev" "S1" "S2";
"PGA" csp "PGAev" "S1" "S2";
"PGB" csp "PGBev" "S1" "S2";
"SMA" csp "SMAev" "S1" "S2";
"SMB" csp "SMBev" "S1" "S2";
"CWAev" lambda=1.0e-6 dorm=0;
"CWBev" lambda=1.0e-6 dorm=0;
"SO1Aev" lambda=1.0e-6 dorm=0;
"SO1Bev" lambda=1.0e-6 dorm=0;
"SO2Aev" lambda=1.0e-6 dorm=0;
"SO2Bev" lambda=1.0e-6 dorm=0;
"PGAev" lambda=1.0e-6 dorm=0;
"PGBev" lambda=1.0e-6 dorm=0;
"SMAev" lambda=1.0e-6 dorm=0;
"SMBev" lambda=1.0e-6 dorm=0;
"S1" lambda=1.0e-6 dorm=0;
"S2" lambda=1.0e-6 dorm=0;
"DB" and "DB1" "DB2" "DB3";
"DB1" lambda=5.0e-6 dorm=0;
"DB2" lambda=5.0e-6 dorm=0;
"DB3" lambda=5.0e-6 dorm=0;
"MB" and "MB1" "MB2" "MB3";
"MB1" lambda=5.0e-6 dorm=0;
"MB2" lambda=5.0e-6 dorm=0;
"MB3" lambda=5.0e-6 dorm=0;
"VMB" and "VMB1" "VMB2";
"VMB1" lambda=5.0e-6 dorm=0;
"VMB2" lambda=5.0e-6 dorm=0;
"MEM" and "MEM1" "MEM2";
"MEM1" lambda=1.0e-5 dorm=0;
"MEM2" lambda=1.0e-5 dorm=0;
"VMS" or "VM1" "VM2";
"VM1" and "VM1A" "VM1B";
"VM2" and "VM2A" "VM2B";
"VM1A" csp "VM1Aev" "VMS1" "VMS2";
"VM1B" csp "VM1Bev" "VMS1" "VMS2";
"VM2A" csp "VM2Aev" "VMS1" "VMS2";
"VM2B" csp "VM2Bev" "VMS1" "VMS2";
"VM1Aev" lambda=1.0e-6 dorm=0;
"VM1Bev" lambda=1.0e-6 dorm=0;
"VM2Aev" lambda=1.0e-6 dorm=0;
"VM2Bev" lambda=1.0e-6 dorm=0;
"VMS1" lambda=1.0e-6 dorm=0;
"VMS2" lambda=1.0e-6 dorm=0;

22
examples/dft/mcs.dft
View File

@ -1,22 +0,0 @@
toplevel "n12";
"n12" or "n1" "n103" "n7";
"n103" wsp "n106" "n14";
"n7" and "n18" "n26";
"n26" or "n28" "n19" "n23";
"n19" wsp "n16" "n13";
"n23" wsp "n0" "n17";
"n18" or "n15" "n9" "n3";
"n3" wsp "n2" "n17";
"n9" wsp "n8" "n27";
"n16" lambda=8.0 dorm=0.0;
"n0" lambda=0.003 dorm=0.0;
"n13" lambda=8.0 dorm=0.5;
"n2" lambda=0.003 dorm=0.0;
"n17" lambda=0.003 dorm=0.5;
"n15" lambda=0.05 dorm=0.0;
"n106" lambda=1.2 dorm=0.0;
"n14" lambda=0.6 dorm=0.0;
"n1" lambda=2.0E-4 dorm=0.0;
"n27" lambda=8.0 dorm=0.5;
"n8" lambda=8.0 dorm=0.0;
"n28" lambda=0.05 dorm=0.0;

26
examples/dft/mdcs.dft
View File

@ -1,26 +0,0 @@
toplevel "System";
"System" or "S" "N";
"N" lambda=2e-5 dorm=0;
"S" and "CMA" "CMB";
"CMA" or "DiskA" "PA" "MemA";
"DiskA" wsp "DAA" "DAB";
"PA" lambda=500e-5 dorm=0;
"MemA" wsp "MA" "MC";
"DAA" lambda=80000e-5 dorm=0.5;
"DAB" lambda=80000e-5 dorm=0.5;
"MA" lambda=30e-5 dorm=0;
"CMB" or "DiskB" "PB" "MemB";
"DiskB" wsp "DBA" "DBB";
"PB" lambda=500e-5 dorm=0;
"MemB" wsp "MB" "MC";
"DBA" lambda=80000e-5 dorm=0.5;
"DBB" lambda=80000e-5 dorm=0.5;
"MB" lambda=30e-5 dorm=0;
"MC" lambda=30e-5 dorm=0.5;

19
examples/dft/mdcs2.dft
View File

@ -1,19 +0,0 @@
toplevel "System";
"System" or "S" "N";
"N" lambda=0.0000200000 dorm=0.0000000000;
"S" and "CMA" "CMB";
"CMA" or "DiskA" "PA" "MemA";
"DiskA" wsp "DAA" "DAB";
"PA" lambda=0.0049999999 dorm=0.0000000000;
"MemA" wsp "MA" "MC";
"DAA" lambda=0.8000000119 dorm=0.5000000000;
"DAB" lambda=0.8000000119 dorm=0.5000000000;
"MA" lambda=0.0003000000 dorm=0.0000000000;
"CMB" or "DiskB" "PB" "MemB";
"DiskB" wsp "DBA" "DBB";
"PB" lambda=0.0049999999 dorm=0.0000000000;
"MemB" wsp "MB" "MC";
"DBA" lambda=0.8000000119 dorm=0.5000000000;
"DBB" lambda=0.8000000119 dorm=0.5000000000;
"MB" lambda=0.0003000000 dorm=0.0000000000;
"MC" lambda=0.0003000000 dorm=0.5000000000;

7
examples/dft/mp.dft
View File

@ -1,7 +0,0 @@
toplevel "A";
"A" or "B" "C";
"B" or "D" "E";
"C" or "F" "E";
"D" lambda=0.1 dorm=0;
"E" lambda=0.2 dorm=0;
"F" lambda=0.3 dorm=0;

6
examples/dft/nonmonoton.dft
View File

@ -1,6 +0,0 @@
toplevel "A";
"A" or "B" "Z";
"B" pand "D" "S";
"Z" lambda=1 dorm=0;
"D" lambda=100 dorm=0;
"S" lambda=50 dorm=0;

8
examples/dft/nonmonoton_param.dft
View File

@ -1,8 +0,0 @@
param x;
param y;
toplevel "A";
"A" or "B" "Z";
"Z" pand "C" "D";
"B" lambda=y dorm=0;
"C" lambda=100 dorm=0;
"D" lambda=100*x dorm=0;

4
examples/dft/or.dft
View File

@ -1,4 +0,0 @@
toplevel "A";
"A" or "B" "C";
"B" lambda=0.5 dorm=0.3;
"C" lambda=0.5 dorm=0.3;

4
examples/dft/pand.dft
View File

@ -1,4 +0,0 @@
toplevel "A";
"A" pand "B" "C";
"B" lambda=0.4 dorm=0.3;
"C" lambda=0.2 dorm=0.3;

6
examples/dft/pand_param.dft
View File

@ -1,6 +0,0 @@
param x;
param y;
toplevel "A";
"A" pand "B" "C";
"B" lambda=x dorm=0.3;
"C" lambda=y dorm=0.3;

12
examples/dft/pdep.dft
View File

@ -1,12 +0,0 @@
// From Junges2015
// Example 3.19
toplevel "SF";
"SF" or "A" "B" "PDEP";
"A" pand "S" "MA";
"B" and "MA" "MB";
"PDEP" pdep=0.2 "MA" "S";
"S" lambda=0.5 dorm=0;
"MA" lambda=0.5 dorm=0;
"MB" lambda=0.5 dorm=0;

9
examples/dft/pdep2.dft
View File

@ -1,9 +0,0 @@
toplevel "SF";
"SF" or "A" "B" "PDEP";
"A" pand "S" "MA";
"B" and "MA" "MB";
"PDEP" pdep=0.2 "MA" "S" "MB";
"S" lambda=0.5 dorm=0;
"MA" lambda=0.5 dorm=0;
"MB" lambda=0.5 dorm=0;

5
examples/dft/pdep3.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" and "B" "C" "F";
"F" pdep=0.3 "B" "C";
"B" lambda=0.4 dorm=0;
"C" lambda=0.8 dorm=0;

7
examples/dft/pdep4.dft
View File

@ -1,7 +0,0 @@
toplevel "SF";
"SF" pand "S" "A" "B";
"PDEP" pdep=0.2 "S" "A" "B";
"S" lambda=0.5 dorm=0;
"A" lambda=0.5 dorm=0;
"B" lambda=0.5 dorm=0;

11
examples/dft/pdep_symmetry.dft
View File

@ -1,11 +0,0 @@
toplevel "A";
"A" and "B" "B'";
"B" and "C" "D" "PDEP";
"B'" and "C'" "D'" "PDEP'";
"PDEP" pdep=0.6 "C" "D";
"PDEP'" pdep=0.6 "C'" "D'";
"C" lambda=0.5 dorm=0;
"D" lambda=0.5 dorm=0;
"C'" lambda=0.5 dorm=0;
"D'" lambda=0.5 dorm=0;

5
examples/dft/por.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" por "B" "C" "D";
"B" lambda=0.4 dorm=0.0;
"C" lambda=0.2 dorm=0.0;
"D" lambda=0.2 dorm=0.0;

5
examples/dft/seq.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" and "B" "C";
"X" seq "B" "C"
"B" lambda=0.5 dorm=0.3;
"C" lambda=0.5 dorm=0.3;

6
examples/dft/seq2.dft
View File

@ -1,6 +0,0 @@
toplevel "A";
"A" and "B" "C" "D";
"X" seq "B" "C" "D";
"B" lambda=0.5 dorm=0.3;
"C" lambda=0.5 dorm=0.3;
"D" lambda=0.5 dorm=0.3;

6
examples/dft/seq3.dft
View File

@ -1,6 +0,0 @@
toplevel "A";
"A" and "C" "D";
"X" seq "B" "C" "D";
"B" lambda=0.5 dorm=0.3;
"C" lambda=0.5 dorm=0.3;
"D" lambda=0.5 dorm=0.3;

7
examples/dft/seq4.dft
View File

@ -1,7 +0,0 @@
toplevel "A";
"A" and "T1" "B3";
"T1" or "B1" "B2";
"X" seq "B1" "B2" "B3";
"B1" lambda=0.5 dorm=0.3;
"B2" lambda=0.5 dorm=0.3;
"B3" lambda=0.5 dorm=0.3;

9
examples/dft/seq5.dft
View File

@ -1,9 +0,0 @@
toplevel "A";
"A" and "T1" "T2";
"T1" pand "B1" "B2";
"T2" pand "B3" "B4";
"X" seq "B4" "B3";
"B1" lambda=0.7 dorm=0.3;
"B2" lambda=0.5 dorm=0.3;
"B3" lambda=0.5 dorm=0.3;
"B4" lambda=0.7 dorm=0.3;

5
examples/dft/spare.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" wsp "I" "M";
"I" lambda=0.5 dorm=0.3;
"M" lambda=0.5 dorm=0.3;

8
examples/dft/spare2.dft
View File

@ -1,8 +0,0 @@
toplevel "A";
"A" or "B" "C";
"B" wsp "I" "J";
"C" wsp "M" "J";
"I" lambda=0.5 dorm=0.3;
"J" lambda=0.5 dorm=0.3;
"M" lambda=0.5 dorm=0.3;

10
examples/dft/spare3.dft
View File

@ -1,10 +0,0 @@
toplevel "A";
"A" or "B" "C" "D";
"B" wsp "I" "M";
"C" wsp "J" "M";
"D" wsp "K" "M";
"I" lambda=0.5 dorm=0.3;
"J" lambda=0.5 dorm=0.3;
"K" lambda=0.5 dorm=0.3;
"M" lambda=0.5 dorm=0.3;

9
examples/dft/spare4.dft
View File

@ -1,9 +0,0 @@
toplevel "A";
"A" and "B" "C";
"B" wsp "I" "J" "K";
"C" wsp "M" "J";
"I" lambda=0.5 dorm=0.3;
"J" lambda=0.5 dorm=0.3;
"K" lambda=0.5 dorm=0.3;
"M" lambda=0.5 dorm=0.3;

9
examples/dft/spare5.dft
View File

@ -1,9 +0,0 @@
toplevel "A";
"A" wsp "I" "B";
"B" or "C" "J";
"C" or "K" "L";
"I" lambda=0.5 dorm=0;
"J" lambda=0.5 dorm=0;
"K" lambda=0.5 dorm=0;
"L" lambda=0.5 dorm=0;

7
examples/dft/spare6.dft
View File

@ -1,7 +0,0 @@
toplevel "A";
"A" or "I" "B";
"B" wsp "J" "M";
"I" lambda=0.5 dorm=0.5;
"J" lambda=0.5 dorm=0.5;
"M" lambda=0.5 dorm=0.5;

5
examples/dft/spare7.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" wsp "K" "J" "I";
"I" lambda=0.5 dorm=0.5;
"J" lambda=1 dorm=0.5;
"K" lambda=0.5 dorm=0.5;

7
examples/dft/spare8.dft
View File

@ -1,7 +0,0 @@
toplevel "A";
"A" wsp "I" "B";
"B" wsp "J" "K";
"I" lambda=0.5 dorm=0.3;
"J" lambda=0.5 dorm=0.3;
"K" lambda=0.5 dorm=0.3;

5
examples/dft/spare_cold.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" wsp "I" "M";
"I" lambda=0.5 dorm=0.0;
"M" lambda=0.5 dorm=0.0;

9
examples/dft/spare_param.dft
View File

@ -1,9 +0,0 @@
param x;
param y;
toplevel "SF";
"SF" or "FW" "BW";
"FW" wsp "W1" "WS";
"BW" wsp "W2" "WS";
"W1" lambda=x dorm=0;
"W2" lambda=1 dorm=0;
"WS" lambda=y dorm=0;

9
examples/dft/spare_symmetry.dft
View File

@ -1,9 +0,0 @@
toplevel "A";
"A" and "B" "C";
"B" wsp "I" "J";
"C" wsp "K" "L";
"I" lambda=0.5 dorm=0.3;
"J" lambda=0.5 dorm=0.3;
"K" lambda=0.5 dorm=0.3;
"L" lambda=0.5 dorm=0.3;

8
examples/dft/symmetry.dft
View File

@ -1,8 +0,0 @@
toplevel "A";
"A" and "B" "B'";
"B" and "C" "D";
"B'" and "C'" "D'";
"C" lambda=0.5 dorm=0;
"D" lambda=0.5 dorm=0;
"C'" lambda=0.5 dorm=0;
"D'" lambda=0.5 dorm=0;

8
examples/dft/symmetry2.dft
View File

@ -1,8 +0,0 @@
toplevel "A";
"A" and "B" "B'";
"B" and "C" "D";
"B'" and "C'" "D'";
"C" lambda=0.5 dorm=0;
"D" lambda=2 dorm=0;
"C'" lambda=0.5 dorm=0;
"D'" lambda=2 dorm=0;

12
examples/dft/symmetry3.dft
View File

@ -1,12 +0,0 @@
toplevel "A";
"A" and "B" "B'" "B''";
"B" and "C" "D";
"B'" and "C'" "D'";
"B''" and "C''" "D''";
"C" lambda=0.5 dorm=0;
"D" lambda=0.5 dorm=0;
"C'" lambda=0.5 dorm=0;
"D'" lambda=0.5 dorm=0;
"C''" lambda=0.5 dorm=0;
"D''" lambda=0.5 dorm=0;

12
examples/dft/symmetry4.dft
View File

@ -1,12 +0,0 @@
toplevel "A";
"A" and "B" "B'" "C" "C'";
"B" and "D" "E";
"B'" and "D'" "E'";
"C" or "F";
"C'" or "F'";
"D" lambda=0.5 dorm=0;
"E" lambda=0.5 dorm=0;
"D'" lambda=0.5 dorm=0;
"E'" lambda=0.5 dorm=0;
"F" lambda=0.5 dorm=0;
"F'" lambda=0.5 dorm=0;

21
examples/dft/symmetry5.dft
View File

@ -1,21 +0,0 @@
toplevel "A";
"A" and "BA" "BB" "BC" "BD" "BE" "BF";
"BA" and "CA" "DA";
"BB" and "CB" "DB";
"BC" and "CC" "DC";
"BD" and "CD" "DD";
"BE" and "CE" "DE";
"BF" and "CF" "DF";
"CA" lambda=0.5 dorm=0;
"DA" lambda=0.5 dorm=0;
"CB" lambda=0.5 dorm=0;
"DB" lambda=0.5 dorm=0;
"CC" lambda=0.5 dorm=0;
"DC" lambda=0.5 dorm=0;
"CD" lambda=0.5 dorm=0;
"DD" lambda=0.5 dorm=0;
"CE" lambda=0.5 dorm=0;
"DE" lambda=0.5 dorm=0;
"CF" lambda=0.5 dorm=0;
"DF" lambda=0.5 dorm=0;

10
examples/dft/symmetry_param.dft
View File

@ -1,10 +0,0 @@
param x;
param y;
toplevel "A";
"A" and "B" "B'";
"B" and "C" "D";
"B'" and "C'" "D'";
"C" lambda=x dorm=0;
"D" lambda=y dorm=0;
"C'" lambda=x dorm=0;
"D'" lambda=y dorm=0;

7
examples/dft/symmetry_shared.dft
View File

@ -1,7 +0,0 @@
toplevel "A";
"A" and "B" "B'";
"B" wsp "C" "D";
"B'" wsp "C'" "D";
"C" lambda=0.5 dorm=0;
"D" lambda=0.5 dorm=0;
"C'" lambda=0.5 dorm=0;

8
examples/dft/tripple_and1.dft
View File

@ -1,8 +0,0 @@
toplevel "A";
"A" and "B" "C";
"B" and "BE1" "BE2";
"C" and "BE3" "BE4";
"BE1" lambda=0.5 dorm=0.3;
"BE2" lambda=0.5 dorm=0.3;
"BE3" lambda=0.5 dorm=0.3;
"BE4" lambda=0.5 dorm=0.3;

8
examples/dft/tripple_and2.dft
View File

@ -1,8 +0,0 @@
toplevel "A";
"A" and "B" "C";
"B" and "BE1" "BE2";
"C" and "BE2" "BE3";
"BE1" lambda=0.5 dorm=0.3;
"BE2" lambda=0.5 dorm=0.3;
"BE3" lambda=0.5 dorm=0.3;

6
examples/dft/tripple_and2_c.dft
View File

@ -1,6 +0,0 @@
toplevel "A";
"A" and "BE1" "BE2" "BE3";
"BE1" lambda=0.5 dorm=3;
"BE2" lambda=0.5 dorm=3;
"BE3" lambda=0.5 dorm=3;

7
examples/dft/tripple_and_c.dft
View File

@ -1,7 +0,0 @@
toplevel "A";
"A" and "BE1" "BE2" "BE3" "BE4";
"BE1" lambda=0.5 dorm=3;
"BE2" lambda=0.5 dorm=3;
"BE3" lambda=0.5 dorm=3;
"BE4" lambda=0.5 dorm=3;

9
examples/dft/tripple_or.dft
View File

@ -1,9 +0,0 @@
toplevel "A";
"A" or "B" "C";
"B" or "BE1" "BE2";
"C" or "BE3" "BE4";
"BE1" lambda=0.5 dorm=3;
"BE2" lambda=0.5 dorm=3;
"BE3" lambda=0.5 dorm=3;
"BE4" lambda=0.5 dorm=3;

8
examples/dft/tripple_or2.dft
View File

@ -1,8 +0,0 @@
toplevel "A";
"A" or "B" "C";
"B" or "BE1" "BE2";
"C" or "BE2" "BE3";
"BE1" lambda=0.5 dorm=3;
"BE2" lambda=0.5 dorm=3;
"BE3" lambda=0.5 dorm=3;

6
examples/dft/tripple_or2_c.dft
View File

@ -1,6 +0,0 @@
toplevel "A";
"A" or "BE1" "BE2" "BE3";
"BE1" lambda=0.5 dorm=3;
"BE2" lambda=0.5 dorm=3;
"BE3" lambda=0.5 dorm=3;

7
examples/dft/tripple_or_c.dft
View File

@ -1,7 +0,0 @@
toplevel "A";
"A" or "BE1" "BE2" "BE3" "BE4";
"BE1" lambda=0.5 dorm=3;
"BE2" lambda=0.5 dorm=3;
"BE3" lambda=0.5 dorm=3;
"BE4" lambda=0.5 dorm=3;

9
examples/dft/tripple_pand.dft
View File

@ -1,9 +0,0 @@
toplevel "A";
"A" pand "B" "BE4";
"B" pand "C" "BE3";
"C" pand "BE1" "BE2";
"BE1" lambda=0.5 dorm=3;
"BE2" lambda=0.5 dorm=3;
"BE3" lambda=0.5 dorm=3;
"BE4" lambda=0.5 dorm=3;

8
examples/dft/tripple_pand2.dft
View File

@ -1,8 +0,0 @@
toplevel "A";
"A" pand "B" "C";
"B" pand "BE1" "BE2";
"C" pand "BE2" "BE3";
"BE1" lambda=0.5 dorm=3;
"BE2" lambda=0.5 dorm=3;
"BE3" lambda=0.5 dorm=3;

6
examples/dft/tripple_pand2_c.dft
View File

@ -1,6 +0,0 @@
toplevel "A";
"A" pand "BE1" "BE2" "BE3";
"BE1" lambda=0.5 dorm=3;
"BE2" lambda=0.5 dorm=3;
"BE3" lambda=0.5 dorm=3;

7
examples/dft/tripple_pand_c.dft
View File

@ -1,7 +0,0 @@
toplevel "A";
"A" pand "BE1" "BE2" "BE3" "BE4";
"BE1" lambda=0.5 dorm=3;
"BE2" lambda=0.5 dorm=3;
"BE3" lambda=0.5 dorm=3;
"BE4" lambda=0.5 dorm=3;

5
examples/dft/voting.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" 1of3 "B" "C" "D";
"B" lambda=0.1 dorm=0;
"C" lambda=0.2 dorm=0;
"D" lambda=0.3 dorm=0;

5
examples/dft/voting2.dft
View File

@ -1,5 +0,0 @@
toplevel "A";
"A" 1of3 "B" "C" "D";
"B" lambda=0.3 dorm=0;
"C" lambda=0.4 dorm=0;
"D" lambda=1 dorm=0;

41034
examples/gspn/HypercubeGrid/hc3k4p4b12.pnml
File diff suppressed because it is too large
View File

87274
examples/gspn/HypercubeGrid/hc4k3p3b12.pnml
File diff suppressed because it is too large
View File

1
examples/gspn/HypercubeGrid/hc5k3p3b15.pnml.REMOVED.git-id
View File

@ -1 +0,0 @@
1dcc3a0045e4d0f9358f9ee04e70c6f0107929be

5554
examples/gspn/ibm319/IBM319.pnml
File diff suppressed because it is too large
View File

14
examples/gspn/pnpro_test1/project01.PNPRO
View File

@ -1,14 +0,0 @@
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="project01" version="121">
<gspn name="gspn_1_1" show-color-cmd="false" show-fluid-cmd="false">
<nodes>
<place marking="1" name="P0" x="3.0" y="2.0"/>
<transition name="T0" nservers-x="0.5" type="EXP" x="9.55" y="2.0"/>
<place name="P1" x="14.0" y="2.0"/>
</nodes>
<edges>
<arc head="T0" kind="INPUT" tail="P0"/>
<arc head="P1" kind="OUTPUT" tail="T0"/>
</edges>
</gspn>
</project>

148
examples/gspn/tiny/tiny01.pnml
View File

@ -1,148 +0,0 @@
<pnml>
<net id="tiny1">
<place id="p1">
<initialMarking>
<value>Default,1</value>
</initialMarking>
</place>
<place id="p2">
<initialMarking>
<value>Default,1</value>
</initialMarking>
</place>
<place id="p3">
<initialMarking>
<value>Default,0</value>
</initialMarking>
</place>
<place id="p4">
<initialMarking>
<value>Default,0</value>
</initialMarking>
</place>
<place id="p5">
<initialMarking>
<value>Default,0</value>
</initialMarking>
</place>
<place id="p6">
<initialMarking>
<value>Default,0</value>
</initialMarking>
</place>
<place id="p7">
<initialMarking>
<value>Default,0</value>
</initialMarking>
</place>
<transition id="t1">
<rate>
<value>1</value>
</rate>
<timed>
<value>false</value>
</timed>
</transition>
<transition id="t2">
<rate>
<value>2</value>
</rate>
<timed>
<value>false</value>
</timed>
</transition>
<transition id="t3">
<rate>
<value>3</value>
</rate>
<timed>
<value>false</value>
</timed>
</transition>
<transition id="l1">
<rate>
<value>4</value>
</rate>
<timed>
<value>true</value>
</timed>
</transition>
<transition id="l2">
<rate>
<value>5</value>
</rate>
<timed>
<value>true</value>
</timed>
<priority>
<text>2</text>
</priority>
</transition>
<arc id="arc1" source="p1" target="t1">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc2" source="t1" target="p3">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc3" source="p2" target="t2">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc4" source="t2" target="p5">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc5" source="p2" target="t3">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc6" source="p3" target="t3">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc7" source="t3" target="p4">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc8" source="p4" target="l1">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc9" source="l1" target="p6">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc10" source="p5" target="l2">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
<arc id="arc11" source="l2" target="p7">
<inscription>
<value>Default,1</value>
</inscription>
<type value="normal" />
</arc>
</net>
</pnml>

1236
examples/gspn/workflow_cluster/workflow_cluster.pnml
File diff suppressed because it is too large
View File

58
examples/pgcl/coupon/coupon10-classic.pgcl
View File

@ -1,58 +0,0 @@
function coupon10() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int coup5 := 0;
int coup6 := 0;
int coup7 := 0;
int coup8 := 0;
int coup9 := 0;
int coup10 := 0;
int draw := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) {
draw := unif(0,10);
draw2 := unif(0,10);
draw3 := unif(0,10);
numberDraws := numberDraws + 1;
if(draw = 0) {
coup0 := 1;
}
if(draw = 1) {
coup1 := 1;
}
if(draw = 2) {
coup2 := 1;
}
if(draw = 3) {
coup3 := 1;
}
if(draw = 4) {
coup4 := 1;
}
if(draw = 5) {
coup5 := 1;
}
if(draw = 6) {
coup6 := 1;
}
if(draw = 7) {
coup7 := 1;
}
if(draw = 8) {
coup8 := 1;
}
if(draw = 9) {
coup9 := 1;
}
if(draw = 10) {
coup10 := 1;
}
}
}

60
examples/pgcl/coupon/coupon10-cost.pgcl
View File

@ -1,60 +0,0 @@
function coupon10() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int coup5 := 0;
int coup6 := 0;
int coup7 := 0;
int coup8 := 0;
int coup9 := 0;
int coup10 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int cost := 1;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) {
draw1 := unif(0,10);
draw2 := unif(0,10);
draw3 := unif(0,10);
cost := ceil(1.02 * cost);
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
coup3 := 1;
}
if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
coup4 := 1;
}
if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
coup5 := 1;
}
if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
coup6 := 1;
}
if (draw1 = 7 | draw2 = 7 | draw3 = 7) {
coup7 := 1;
}
if (draw1 = 8 | draw2 = 8 | draw3 = 8) {
coup8 := 1;
}
if (draw1 = 9 | draw2 = 9 | draw3 = 9) {
coup9 := 1;
}
if (draw1 = 10 | draw2 = 10 | draw3 = 10) {
coup10 := 1;
}
}
}

62
examples/pgcl/coupon/coupon10-observe.pgcl
View File

@ -1,62 +0,0 @@
function coupon10() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int coup5 := 0;
int coup6 := 0;
int coup7 := 0;
int coup8 := 0;
int coup9 := 0;
int coup10 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) {
draw1 := unif(0,10);
draw2 := unif(0,10);
draw3 := unif(0,10);
numberDraws := numberDraws + 1;
observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3);
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
coup3 := 1;
}
if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
coup4 := 1;
}
if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
coup5 := 1;
}
if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
coup6 := 1;
}
if (draw1 = 7 | draw2 = 7 | draw3 = 7) {
coup7 := 1;
}
if (draw1 = 8 | draw2 = 8 | draw3 = 8) {
coup8 := 1;
}
if (draw1 = 9 | draw2 = 9 | draw3 = 9) {
coup9 := 1;
}
if (draw1 = 10 | draw2 = 10 | draw3 = 10) {
coup10 := 1;
}
}
}

60
examples/pgcl/coupon/coupon10.pgcl
View File

@ -1,60 +0,0 @@
function coupon10() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int coup5 := 0;
int coup6 := 0;
int coup7 := 0;
int coup8 := 0;
int coup9 := 0;
int coup10 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1) | !(coup7 = 1) | !(coup8 = 1) | !(coup9 = 1) | !(coup10 = 1)) {
draw1 := unif(0,10);
draw2 := unif(0,10);
draw3 := unif(0,10);
numberDraws := numberDraws + 1;
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
coup3 := 1;
}
if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
coup4 := 1;
}
if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
coup5 := 1;
}
if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
coup6 := 1;
}
if (draw1 = 7 | draw2 = 7 | draw3 = 7) {
coup7 := 1;
}
if (draw1 = 8 | draw2 = 8 | draw3 = 8) {
coup8 := 1;
}
if (draw1 = 9 | draw2 = 9 | draw3 = 9) {
coup9 := 1;
}
if (draw1 = 10 | draw2 = 10 | draw3 = 10) {
coup10 := 1;
}
}
}

24
examples/pgcl/coupon/coupon3-classic.pgcl
View File

@ -1,24 +0,0 @@
function coupon3() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int draw := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) {
draw := unif(0,2);
numberDraws := numberDraws + 1;
if(draw = 0) {
coup0 := 1;
}
if(draw = 1) {
coup1 := 1;
}
if(draw = 2) {
coup2 := 1;
}
}
}

28
examples/pgcl/coupon/coupon3-cost.pgcl
View File

@ -1,28 +0,0 @@
function coupon3() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int cost := 1;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) {
draw1 := unif(0,2);
draw2 := unif(0,2);
draw3 := unif(0,2);
cost := ceil(1.02 * cost);
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
}
}

30
examples/pgcl/coupon/coupon3-observe.pgcl
View File

@ -1,30 +0,0 @@
function coupon3() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) {
draw1 := unif(0,2);
draw2 := unif(0,2);
draw3 := unif(0,2);
numberDraws := numberDraws + 1;
observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3);
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
}
}

28
examples/pgcl/coupon/coupon3.pgcl
View File

@ -1,28 +0,0 @@
function coupon3() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1)) {
draw1 := unif(0,2);
draw2 := unif(0,2);
draw3 := unif(0,2);
numberDraws := numberDraws + 1;
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
}
}

34
examples/pgcl/coupon/coupon4-observe.pgcl
View File

@ -1,34 +0,0 @@
function coupon4() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1)) {
draw1 := unif(0,4);
draw2 := unif(0,4);
draw3 := unif(0,4);
numberDraws := numberDraws + 1;
observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3);
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
coup3 := 1;
}
}
}

32
examples/pgcl/coupon/coupon5-classic.pgcl
View File

@ -1,32 +0,0 @@
function coupon5() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int draw := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) {
draw := unif(0,4);
numberDraws := numberDraws + 1;
if(draw = 0) {
coup0 := 1;
}
if(draw = 1) {
coup1 := 1;
}
if(draw = 2) {
coup2 := 1;
}
if(draw = 3) {
coup3 := 1;
}
if(draw = 4) {
coup4 := 1;
}
}
}

36
examples/pgcl/coupon/coupon5-cost.pgcl
View File

@ -1,36 +0,0 @@
function coupon5() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int cost := 1;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) {
draw1 := unif(0,4);
draw2 := unif(0,4);
draw3 := unif(0,4);
cost := ceil(1.02 * cost);
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
coup3 := 1;
}
if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
coup4 := 1;
}
}
}

38
examples/pgcl/coupon/coupon5-observe.pgcl
View File

@ -1,38 +0,0 @@
function coupon5() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) {
draw1 := unif(0,4);
draw2 := unif(0,4);
draw3 := unif(0,4);
numberDraws := numberDraws + 1;
observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3);
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
coup3 := 1;
}
if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
coup4 := 1;
}
}
}

36
examples/pgcl/coupon/coupon5.pgcl
View File

@ -1,36 +0,0 @@
function coupon5() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1)) {
draw1 := unif(0,4);
draw2 := unif(0,4);
draw3 := unif(0,4);
numberDraws := numberDraws + 1;
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
coup3 := 1;
}
if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
coup4 := 1;
}
}
}

40
examples/pgcl/coupon/coupon7-classic.pgcl
View File

@ -1,40 +0,0 @@
function coupon7() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int coup5 := 0;
int coup6 := 0;
int draw := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) {
draw := unif(0,6);
numberDraws := numberDraws + 1;
if(draw = 0) {
coup0 := 1;
}
if(draw = 1) {
coup1 := 1;
}
if(draw = 2) {
coup2 := 1;
}
if(draw = 3) {
coup3 := 1;
}
if(draw = 4) {
coup4 := 1;
}
if(draw = 5) {
coup5 := 1;
}
if(draw = 6) {
coup6 := 1;
}
}
}

44
examples/pgcl/coupon/coupon7-cost.pgcl
View File

@ -1,44 +0,0 @@
function coupon7() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int coup5 := 0;
int coup6 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int cost := 1;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) {
draw1 := unif(0,6);
draw2 := unif(0,6);
draw3 := unif(0,6);
cost := ceil(1.02 * cost);
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
coup3 := 1;
}
if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
coup4 := 1;
}
if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
coup5 := 1;
}
if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
coup6 := 1;
}
}
}

46
examples/pgcl/coupon/coupon7-observe.pgcl
View File

@ -1,46 +0,0 @@
function coupon7() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int coup5 := 0;
int coup6 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) {
draw1 := unif(0,6);
draw2 := unif(0,6);
draw3 := unif(0,6);
numberDraws := numberDraws + 1;
observe (draw1 != draw2 & draw1 != draw3 & draw2 != draw3);
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
coup3 := 1;
}
if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
coup4 := 1;
}
if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
coup5 := 1;
}
if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
coup6 := 1;
}
}
}

44
examples/pgcl/coupon/coupon7.pgcl
View File

@ -1,44 +0,0 @@
function coupon7() {
int coup0 := 0;
int coup1 := 0;
int coup2 := 0;
int coup3 := 0;
int coup4 := 0;
int coup5 := 0;
int coup6 := 0;
int draw1 := 0;
int draw2 := 0;
int draw3 := 0;
int numberDraws := 0;
while (!(coup0 = 1) | !(coup1 = 1) | !(coup2 = 1) | !(coup3 = 1) | !(coup4 = 1) | !(coup5= 1) | !(coup6 = 1)) {
draw1 := unif(0,6);
draw2 := unif(0,6);
draw3 := unif(0,6);
numberDraws := numberDraws + 1;
if(draw1 = 0 | draw2 = 0 | draw3 = 0) {
coup0 := 1;
}
if(draw1 = 1 | draw2 = 1 | draw3 = 1) {
coup1 := 1;
}
if(draw1 = 2 | draw2 = 2 | draw3 = 2) {
coup2 := 1;
}
if (draw1 = 3 | draw2 = 3 | draw3 = 3) {
coup3 := 1;
}
if (draw1 = 4 | draw2 = 4 | draw3 = 4) {
coup4 := 1;
}
if (draw1 = 5 | draw2 = 5 | draw3 = 5) {
coup5 := 1;
}
if (draw1 = 6 | draw2 = 6 | draw3 = 6) {
coup6 := 1;
}
}
}

35
examples/pgcl/crowds/crowds100-100-observeOther.pgcl
View File

@ -1,35 +0,0 @@
function crowds() {
int delivered := 0;
int lastSender := 0;
int remainingRuns := 100;
int observeSender := 0;
int observeOther := 0;
while(remainingRuns > 0) {
while(delivered = 0) {
{
if(lastSender = 0) {
observeSender := observeSender + 1;
} else {
observeOther := observeOther + 1;
}
lastSender := 0;
delivered := 1;
} [0.091] {
{
{ lastSender:=0; } [1/100] { lastSender := 1; }
}
[0.8]
{
lastSender := 0;
// When not forwarding, the message is delivered here.
delivered := 1;
}
}
}
delivered := 0;
// Set up new run.
remainingRuns := remainingRuns - 1;
}
observe(observeOther > 25);
}

34
examples/pgcl/crowds/crowds100-100.pgcl
View File

@ -1,34 +0,0 @@
function crowds() {
int delivered := 0;
int lastSender := 0;
int remainingRuns := 100;
int observeSender := 0;
int observeOther := 0;
while(remainingRuns > 0) {
while(delivered = 0) {
{
if(lastSender = 0) {
observeSender := observeSender + 1;
} else {
observeOther := observeOther + 1;
}
lastSender := 0;
delivered := 1;
} [0.091] {
{
{ lastSender:=0; } [1/100] { lastSender := 1; }
}
[0.8]
{
lastSender := 0;
// When not forwarding, the message is delivered here.
delivered := 1;
}
}
}
delivered := 0;
// Set up new run.
remainingRuns := remainingRuns - 1;
}
}

Some files were not shown because too many files changed in this diff

Write Preview
Loading…
Cancel
Save