diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index a9d9f9400..50a220135 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -139,6 +139,16 @@ foreach(HEADER ${SPARSEPP_HEADERS})
list(APPEND SPARSEPP_BINDIR_HEADERS ${SPARSEPP_BINDIR_DIR}/sparsepp/${HEADER_FILENAME})
endforeach()
+#############################################################
+##
+## cpphoafparser
+##
+#############################################################
+
+# Use the shipped version of cpphoafparser
+message (STATUS "storm - Including cpphoafparser 0.99.2")
+include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/cpphoafparser-0.99.2/include")
+
#############################################################
##
## ModernJSON
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/ChangeLog b/resources/3rdparty/cpphoafparser-0.99.2/ChangeLog
new file mode 100644
index 000000000..bd36b7d72
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/ChangeLog
@@ -0,0 +1,24 @@
+2016-02-26 Joachim Klein
+
+ * Release version 0.99.2: Bugfix release
+
+ * Fix parsing of 't' and 'f' in the extra info of acc-name headers, e.g.,
+ acc-name: undefined t
+ Previously, would lead to an infinite loop.
+
+ * Fix dynamic_bitset::getHighestSetBit
+ Off-by-one error, tries to read potentially uninitialized
+ memory. This could lead to non-deterministic behavior for
+ getHighestSetBit, e.g., erroneous validation errors when
+ parsing when HOAIntermediateCheckValidity is active.
+
+ * Add #include to boolean_expression.hh to
+ have access to std::logical_error, even if not included by
+ the other standard library headers (fix compilation issue
+ with some older GCCs).
+
+
+2015-07-20 Joachim Klein
+
+ * Release version 0.99.1: Initial (preliminary) release
+
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/Doxyfile b/resources/3rdparty/cpphoafparser-0.99.2/Doxyfile
new file mode 100644
index 000000000..5967be7d3
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/Doxyfile
@@ -0,0 +1,2362 @@
+# Doxyfile 1.8.9.1
+
+# This file describes the settings to be used by the documentation system
+# doxygen (www.doxygen.org) for a project.
+#
+# All text after a double hash (##) is considered a comment and is placed in
+# front of the TAG it is preceding.
+#
+# All text after a single hash (#) is considered a comment and will be ignored.
+# The format is:
+# TAG = value [value, ...]
+# For lists, items can also be appended using:
+# TAG += value [value, ...]
+# Values that contain spaces should be placed between quotes (\" \").
+
+#---------------------------------------------------------------------------
+# Project related configuration options
+#---------------------------------------------------------------------------
+
+# This tag specifies the encoding used for all characters in the config file
+# that follow. The default is UTF-8 which is also the encoding used for all text
+# before the first occurrence of this tag. Doxygen uses libiconv (or the iconv
+# built into libc) for the transcoding. See http://www.gnu.org/software/libiconv
+# for the list of possible encodings.
+# The default value is: UTF-8.
+
+DOXYFILE_ENCODING = UTF-8
+
+# The PROJECT_NAME tag is a single word (or a sequence of words surrounded by
+# double-quotes, unless you are using Doxywizard) that should identify the
+# project for which the documentation is generated. This name is used in the
+# title of most generated pages and in a few other places.
+# The default value is: My Project.
+
+PROJECT_NAME = "cpphoafparser library API"
+
+# The PROJECT_NUMBER tag can be used to enter a project or revision number. This
+# could be handy for archiving the generated documentation or if some version
+# control system is used.
+
+PROJECT_NUMBER =
+
+# Using the PROJECT_BRIEF tag one can provide an optional one line description
+# for a project that appears at the top of each page and should give viewer a
+# quick idea about the purpose of the project. Keep the description short.
+
+PROJECT_BRIEF =
+
+# With the PROJECT_LOGO tag one can specify a logo or an icon that is included
+# in the documentation. The maximum height of the logo should not exceed 55
+# pixels and the maximum width should not exceed 200 pixels. Doxygen will copy
+# the logo to the output directory.
+
+PROJECT_LOGO =
+
+# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute) path
+# into which the generated documentation will be written. If a relative path is
+# entered, it will be relative to the location where doxygen was started. If
+# left blank the current directory will be used.
+
+OUTPUT_DIRECTORY = docs
+
+# If the CREATE_SUBDIRS tag is set to YES then doxygen will create 4096 sub-
+# directories (in 2 levels) under the output directory of each output format and
+# will distribute the generated files over these directories. Enabling this
+# option can be useful when feeding doxygen a huge amount of source files, where
+# putting all generated files in the same directory would otherwise causes
+# performance problems for the file system.
+# The default value is: NO.
+
+CREATE_SUBDIRS = NO
+
+# If the ALLOW_UNICODE_NAMES tag is set to YES, doxygen will allow non-ASCII
+# characters to appear in the names of generated files. If set to NO, non-ASCII
+# characters will be escaped, for example _xE3_x81_x84 will be used for Unicode
+# U+3044.
+# The default value is: NO.
+
+ALLOW_UNICODE_NAMES = NO
+
+# The OUTPUT_LANGUAGE tag is used to specify the language in which all
+# documentation generated by doxygen is written. Doxygen will use this
+# information to generate all constant output in the proper language.
+# Possible values are: Afrikaans, Arabic, Armenian, Brazilian, Catalan, Chinese,
+# Chinese-Traditional, Croatian, Czech, Danish, Dutch, English (United States),
+# Esperanto, Farsi (Persian), Finnish, French, German, Greek, Hungarian,
+# Indonesian, Italian, Japanese, Japanese-en (Japanese with English messages),
+# Korean, Korean-en (Korean with English messages), Latvian, Lithuanian,
+# Macedonian, Norwegian, Persian (Farsi), Polish, Portuguese, Romanian, Russian,
+# Serbian, Serbian-Cyrillic, Slovak, Slovene, Spanish, Swedish, Turkish,
+# Ukrainian and Vietnamese.
+# The default value is: English.
+
+OUTPUT_LANGUAGE = English
+
+# If the BRIEF_MEMBER_DESC tag is set to YES, doxygen will include brief member
+# descriptions after the members that are listed in the file and class
+# documentation (similar to Javadoc). Set to NO to disable this.
+# The default value is: YES.
+
+BRIEF_MEMBER_DESC = YES
+
+# If the REPEAT_BRIEF tag is set to YES, doxygen will prepend the brief
+# description of a member or function before the detailed description
+#
+# Note: If both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the
+# brief descriptions will be completely suppressed.
+# The default value is: YES.
+
+REPEAT_BRIEF = YES
+
+# This tag implements a quasi-intelligent brief description abbreviator that is
+# used to form the text in various listings. Each string in this list, if found
+# as the leading text of the brief description, will be stripped from the text
+# and the result, after processing the whole list, is used as the annotated
+# text. Otherwise, the brief description is used as-is. If left blank, the
+# following values are used ($name is automatically replaced with the name of
+# the entity):The $name class, The $name widget, The $name file, is, provides,
+# specifies, contains, represents, a, an and the.
+
+ABBREVIATE_BRIEF =
+
+# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then
+# doxygen will generate a detailed section even if there is only a brief
+# description.
+# The default value is: NO.
+
+ALWAYS_DETAILED_SEC = NO
+
+# If the INLINE_INHERITED_MEMB tag is set to YES, doxygen will show all
+# inherited members of a class in the documentation of that class as if those
+# members were ordinary class members. Constructors, destructors and assignment
+# operators of the base classes will not be shown.
+# The default value is: NO.
+
+INLINE_INHERITED_MEMB = NO
+
+# If the FULL_PATH_NAMES tag is set to YES, doxygen will prepend the full path
+# before files name in the file list and in the header files. If set to NO the
+# shortest path that makes the file name unique will be used
+# The default value is: YES.
+
+FULL_PATH_NAMES = YES
+
+# The STRIP_FROM_PATH tag can be used to strip a user-defined part of the path.
+# Stripping is only done if one of the specified strings matches the left-hand
+# part of the path. The tag can be used to show relative paths in the file list.
+# If left blank the directory from which doxygen is run is used as the path to
+# strip.
+#
+# Note that you can specify absolute paths here, but also relative paths, which
+# will be relative from the directory where doxygen is started.
+# This tag requires that the tag FULL_PATH_NAMES is set to YES.
+
+STRIP_FROM_PATH =
+
+# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of the
+# path mentioned in the documentation of a class, which tells the reader which
+# header file to include in order to use a class. If left blank only the name of
+# the header file containing the class definition is used. Otherwise one should
+# specify the list of include paths that are normally passed to the compiler
+# using the -I flag.
+
+STRIP_FROM_INC_PATH =
+
+# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter (but
+# less readable) file names. This can be useful is your file systems doesn't
+# support long names like on DOS, Mac, or CD-ROM.
+# The default value is: NO.
+
+SHORT_NAMES = NO
+
+# If the JAVADOC_AUTOBRIEF tag is set to YES then doxygen will interpret the
+# first line (until the first dot) of a Javadoc-style comment as the brief
+# description. If set to NO, the Javadoc-style will behave just like regular Qt-
+# style comments (thus requiring an explicit @brief command for a brief
+# description.)
+# The default value is: NO.
+
+JAVADOC_AUTOBRIEF = YES
+
+# If the QT_AUTOBRIEF tag is set to YES then doxygen will interpret the first
+# line (until the first dot) of a Qt-style comment as the brief description. If
+# set to NO, the Qt-style will behave just like regular Qt-style comments (thus
+# requiring an explicit \brief command for a brief description.)
+# The default value is: NO.
+
+QT_AUTOBRIEF = NO
+
+# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make doxygen treat a
+# multi-line C++ special comment block (i.e. a block of //! or /// comments) as
+# a brief description. This used to be the default behavior. The new default is
+# to treat a multi-line C++ comment block as a detailed description. Set this
+# tag to YES if you prefer the old behavior instead.
+#
+# Note that setting this tag to YES also means that rational rose comments are
+# not recognized any more.
+# The default value is: NO.
+
+MULTILINE_CPP_IS_BRIEF = NO
+
+# If the INHERIT_DOCS tag is set to YES then an undocumented member inherits the
+# documentation from any documented member that it re-implements.
+# The default value is: YES.
+
+INHERIT_DOCS = YES
+
+# If the SEPARATE_MEMBER_PAGES tag is set to YES then doxygen will produce a new
+# page for each member. If set to NO, the documentation of a member will be part
+# of the file/class/namespace that contains it.
+# The default value is: NO.
+
+SEPARATE_MEMBER_PAGES = NO
+
+# The TAB_SIZE tag can be used to set the number of spaces in a tab. Doxygen
+# uses this value to replace tabs by spaces in code fragments.
+# Minimum value: 1, maximum value: 16, default value: 4.
+
+TAB_SIZE = 4
+
+# This tag can be used to specify a number of aliases that act as commands in
+# the documentation. An alias has the form:
+# name=value
+# For example adding
+# "sideeffect=@par Side Effects:\n"
+# will allow you to put the command \sideeffect (or @sideeffect) in the
+# documentation, which will result in a user-defined paragraph with heading
+# "Side Effects:". You can put \n's in the value part of an alias to insert
+# newlines.
+
+ALIASES =
+
+# This tag can be used to specify a number of word-keyword mappings (TCL only).
+# A mapping has the form "name=value". For example adding "class=itcl::class"
+# will allow you to use the command class in the itcl::class meaning.
+
+TCL_SUBST =
+
+# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C sources
+# only. Doxygen will then generate output that is more tailored for C. For
+# instance, some of the names that are used will be different. The list of all
+# members will be omitted, etc.
+# The default value is: NO.
+
+OPTIMIZE_OUTPUT_FOR_C = NO
+
+# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java or
+# Python sources only. Doxygen will then generate output that is more tailored
+# for that language. For instance, namespaces will be presented as packages,
+# qualified scopes will look different, etc.
+# The default value is: NO.
+
+OPTIMIZE_OUTPUT_JAVA = NO
+
+# Set the OPTIMIZE_FOR_FORTRAN tag to YES if your project consists of Fortran
+# sources. Doxygen will then generate output that is tailored for Fortran.
+# The default value is: NO.
+
+OPTIMIZE_FOR_FORTRAN = NO
+
+# Set the OPTIMIZE_OUTPUT_VHDL tag to YES if your project consists of VHDL
+# sources. Doxygen will then generate output that is tailored for VHDL.
+# The default value is: NO.
+
+OPTIMIZE_OUTPUT_VHDL = NO
+
+# Doxygen selects the parser to use depending on the extension of the files it
+# parses. With this tag you can assign which parser to use for a given
+# extension. Doxygen has a built-in mapping, but you can override or extend it
+# using this tag. The format is ext=language, where ext is a file extension, and
+# language is one of the parsers supported by doxygen: IDL, Java, Javascript,
+# C#, C, C++, D, PHP, Objective-C, Python, Fortran (fixed format Fortran:
+# FortranFixed, free formatted Fortran: FortranFree, unknown formatted Fortran:
+# Fortran. In the later case the parser tries to guess whether the code is fixed
+# or free formatted code, this is the default for Fortran type files), VHDL. For
+# instance to make doxygen treat .inc files as Fortran files (default is PHP),
+# and .f files as C (default is Fortran), use: inc=Fortran f=C.
+#
+# Note: For files without extension you can use no_extension as a placeholder.
+#
+# Note that for custom extensions you also need to set FILE_PATTERNS otherwise
+# the files are not read by doxygen.
+
+EXTENSION_MAPPING =
+
+# If the MARKDOWN_SUPPORT tag is enabled then doxygen pre-processes all comments
+# according to the Markdown format, which allows for more readable
+# documentation. See http://daringfireball.net/projects/markdown/ for details.
+# The output of markdown processing is further processed by doxygen, so you can
+# mix doxygen, HTML, and XML commands with Markdown formatting. Disable only in
+# case of backward compatibilities issues.
+# The default value is: YES.
+
+MARKDOWN_SUPPORT = YES
+
+# When enabled doxygen tries to link words that correspond to documented
+# classes, or namespaces to their corresponding documentation. Such a link can
+# be prevented in individual cases by putting a % sign in front of the word or
+# globally by setting AUTOLINK_SUPPORT to NO.
+# The default value is: YES.
+
+AUTOLINK_SUPPORT = YES
+
+# If you use STL classes (i.e. std::string, std::vector, etc.) but do not want
+# to include (a tag file for) the STL sources as input, then you should set this
+# tag to YES in order to let doxygen match functions declarations and
+# definitions whose arguments contain STL classes (e.g. func(std::string);
+# versus func(std::string) {}). This also make the inheritance and collaboration
+# diagrams that involve STL classes more complete and accurate.
+# The default value is: NO.
+
+BUILTIN_STL_SUPPORT = YES
+
+# If you use Microsoft's C++/CLI language, you should set this option to YES to
+# enable parsing support.
+# The default value is: NO.
+
+CPP_CLI_SUPPORT = NO
+
+# Set the SIP_SUPPORT tag to YES if your project consists of sip (see:
+# http://www.riverbankcomputing.co.uk/software/sip/intro) sources only. Doxygen
+# will parse them like normal C++ but will assume all classes use public instead
+# of private inheritance when no explicit protection keyword is present.
+# The default value is: NO.
+
+SIP_SUPPORT = NO
+
+# For Microsoft's IDL there are propget and propput attributes to indicate
+# getter and setter methods for a property. Setting this option to YES will make
+# doxygen to replace the get and set methods by a property in the documentation.
+# This will only work if the methods are indeed getting or setting a simple
+# type. If this is not the case, or you want to show the methods anyway, you
+# should set this option to NO.
+# The default value is: YES.
+
+IDL_PROPERTY_SUPPORT = YES
+
+# If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC
+# tag is set to YES then doxygen will reuse the documentation of the first
+# member in the group (if any) for the other members of the group. By default
+# all members of a group must be documented explicitly.
+# The default value is: NO.
+
+DISTRIBUTE_GROUP_DOC = NO
+
+# Set the SUBGROUPING tag to YES to allow class member groups of the same type
+# (for instance a group of public functions) to be put as a subgroup of that
+# type (e.g. under the Public Functions section). Set it to NO to prevent
+# subgrouping. Alternatively, this can be done per class using the
+# \nosubgrouping command.
+# The default value is: YES.
+
+SUBGROUPING = YES
+
+# When the INLINE_GROUPED_CLASSES tag is set to YES, classes, structs and unions
+# are shown inside the group in which they are included (e.g. using \ingroup)
+# instead of on a separate page (for HTML and Man pages) or section (for LaTeX
+# and RTF).
+#
+# Note that this feature does not work in combination with
+# SEPARATE_MEMBER_PAGES.
+# The default value is: NO.
+
+INLINE_GROUPED_CLASSES = NO
+
+# When the INLINE_SIMPLE_STRUCTS tag is set to YES, structs, classes, and unions
+# with only public data fields or simple typedef fields will be shown inline in
+# the documentation of the scope in which they are defined (i.e. file,
+# namespace, or group documentation), provided this scope is documented. If set
+# to NO, structs, classes, and unions are shown on a separate page (for HTML and
+# Man pages) or section (for LaTeX and RTF).
+# The default value is: NO.
+
+INLINE_SIMPLE_STRUCTS = NO
+
+# When TYPEDEF_HIDES_STRUCT tag is enabled, a typedef of a struct, union, or
+# enum is documented as struct, union, or enum with the name of the typedef. So
+# typedef struct TypeS {} TypeT, will appear in the documentation as a struct
+# with name TypeT. When disabled the typedef will appear as a member of a file,
+# namespace, or class. And the struct will be named TypeS. This can typically be
+# useful for C code in case the coding convention dictates that all compound
+# types are typedef'ed and only the typedef is referenced, never the tag name.
+# The default value is: NO.
+
+TYPEDEF_HIDES_STRUCT = NO
+
+# The size of the symbol lookup cache can be set using LOOKUP_CACHE_SIZE. This
+# cache is used to resolve symbols given their name and scope. Since this can be
+# an expensive process and often the same symbol appears multiple times in the
+# code, doxygen keeps a cache of pre-resolved symbols. If the cache is too small
+# doxygen will become slower. If the cache is too large, memory is wasted. The
+# cache size is given by this formula: 2^(16+LOOKUP_CACHE_SIZE). The valid range
+# is 0..9, the default is 0, corresponding to a cache size of 2^16=65536
+# symbols. At the end of a run doxygen will report the cache usage and suggest
+# the optimal cache size from a speed point of view.
+# Minimum value: 0, maximum value: 9, default value: 0.
+
+LOOKUP_CACHE_SIZE = 0
+
+#---------------------------------------------------------------------------
+# Build related configuration options
+#---------------------------------------------------------------------------
+
+# If the EXTRACT_ALL tag is set to YES, doxygen will assume all entities in
+# documentation are documented, even if no documentation was available. Private
+# class members and static file members will be hidden unless the
+# EXTRACT_PRIVATE respectively EXTRACT_STATIC tags are set to YES.
+# Note: This will also disable the warnings about undocumented members that are
+# normally produced when WARNINGS is set to YES.
+# The default value is: NO.
+
+EXTRACT_ALL = NO
+
+# If the EXTRACT_PRIVATE tag is set to YES, all private members of a class will
+# be included in the documentation.
+# The default value is: NO.
+
+EXTRACT_PRIVATE = NO
+
+# If the EXTRACT_PACKAGE tag is set to YES, all members with package or internal
+# scope will be included in the documentation.
+# The default value is: NO.
+
+EXTRACT_PACKAGE = NO
+
+# If the EXTRACT_STATIC tag is set to YES, all static members of a file will be
+# included in the documentation.
+# The default value is: NO.
+
+EXTRACT_STATIC = NO
+
+# If the EXTRACT_LOCAL_CLASSES tag is set to YES, classes (and structs) defined
+# locally in source files will be included in the documentation. If set to NO,
+# only classes defined in header files are included. Does not have any effect
+# for Java sources.
+# The default value is: YES.
+
+EXTRACT_LOCAL_CLASSES = YES
+
+# This flag is only useful for Objective-C code. If set to YES, local methods,
+# which are defined in the implementation section but not in the interface are
+# included in the documentation. If set to NO, only methods in the interface are
+# included.
+# The default value is: NO.
+
+EXTRACT_LOCAL_METHODS = NO
+
+# If this flag is set to YES, the members of anonymous namespaces will be
+# extracted and appear in the documentation as a namespace called
+# 'anonymous_namespace{file}', where file will be replaced with the base name of
+# the file that contains the anonymous namespace. By default anonymous namespace
+# are hidden.
+# The default value is: NO.
+
+EXTRACT_ANON_NSPACES = NO
+
+# If the HIDE_UNDOC_MEMBERS tag is set to YES, doxygen will hide all
+# undocumented members inside documented classes or files. If set to NO these
+# members will be included in the various overviews, but no documentation
+# section is generated. This option has no effect if EXTRACT_ALL is enabled.
+# The default value is: NO.
+
+HIDE_UNDOC_MEMBERS = NO
+
+# If the HIDE_UNDOC_CLASSES tag is set to YES, doxygen will hide all
+# undocumented classes that are normally visible in the class hierarchy. If set
+# to NO, these classes will be included in the various overviews. This option
+# has no effect if EXTRACT_ALL is enabled.
+# The default value is: NO.
+
+HIDE_UNDOC_CLASSES = NO
+
+# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, doxygen will hide all friend
+# (class|struct|union) declarations. If set to NO, these declarations will be
+# included in the documentation.
+# The default value is: NO.
+
+HIDE_FRIEND_COMPOUNDS = NO
+
+# If the HIDE_IN_BODY_DOCS tag is set to YES, doxygen will hide any
+# documentation blocks found inside the body of a function. If set to NO, these
+# blocks will be appended to the function's detailed documentation block.
+# The default value is: NO.
+
+HIDE_IN_BODY_DOCS = NO
+
+# The INTERNAL_DOCS tag determines if documentation that is typed after a
+# \internal command is included. If the tag is set to NO then the documentation
+# will be excluded. Set it to YES to include the internal documentation.
+# The default value is: NO.
+
+INTERNAL_DOCS = NO
+
+# If the CASE_SENSE_NAMES tag is set to NO then doxygen will only generate file
+# names in lower-case letters. If set to YES, upper-case letters are also
+# allowed. This is useful if you have classes or files whose names only differ
+# in case and if your file system supports case sensitive file names. Windows
+# and Mac users are advised to set this option to NO.
+# The default value is: system dependent.
+
+CASE_SENSE_NAMES = NO
+
+# If the HIDE_SCOPE_NAMES tag is set to NO then doxygen will show members with
+# their full class and namespace scopes in the documentation. If set to YES, the
+# scope will be hidden.
+# The default value is: NO.
+
+HIDE_SCOPE_NAMES = NO
+
+# If the HIDE_COMPOUND_REFERENCE tag is set to NO (default) then doxygen will
+# append additional text to a page's title, such as Class Reference. If set to
+# YES the compound reference will be hidden.
+# The default value is: NO.
+
+HIDE_COMPOUND_REFERENCE= NO
+
+# If the SHOW_INCLUDE_FILES tag is set to YES then doxygen will put a list of
+# the files that are included by a file in the documentation of that file.
+# The default value is: YES.
+
+SHOW_INCLUDE_FILES = YES
+
+# If the SHOW_GROUPED_MEMB_INC tag is set to YES then Doxygen will add for each
+# grouped member an include statement to the documentation, telling the reader
+# which file to include in order to use the member.
+# The default value is: NO.
+
+SHOW_GROUPED_MEMB_INC = NO
+
+# If the FORCE_LOCAL_INCLUDES tag is set to YES then doxygen will list include
+# files with double quotes in the documentation rather than with sharp brackets.
+# The default value is: NO.
+
+FORCE_LOCAL_INCLUDES = NO
+
+# If the INLINE_INFO tag is set to YES then a tag [inline] is inserted in the
+# documentation for inline members.
+# The default value is: YES.
+
+INLINE_INFO = YES
+
+# If the SORT_MEMBER_DOCS tag is set to YES then doxygen will sort the
+# (detailed) documentation of file and class members alphabetically by member
+# name. If set to NO, the members will appear in declaration order.
+# The default value is: YES.
+
+SORT_MEMBER_DOCS = YES
+
+# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the brief
+# descriptions of file, namespace and class members alphabetically by member
+# name. If set to NO, the members will appear in declaration order. Note that
+# this will also influence the order of the classes in the class list.
+# The default value is: NO.
+
+SORT_BRIEF_DOCS = NO
+
+# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen will sort the
+# (brief and detailed) documentation of class members so that constructors and
+# destructors are listed first. If set to NO the constructors will appear in the
+# respective orders defined by SORT_BRIEF_DOCS and SORT_MEMBER_DOCS.
+# Note: If SORT_BRIEF_DOCS is set to NO this option is ignored for sorting brief
+# member documentation.
+# Note: If SORT_MEMBER_DOCS is set to NO this option is ignored for sorting
+# detailed member documentation.
+# The default value is: NO.
+
+SORT_MEMBERS_CTORS_1ST = NO
+
+# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the hierarchy
+# of group names into alphabetical order. If set to NO the group names will
+# appear in their defined order.
+# The default value is: NO.
+
+SORT_GROUP_NAMES = NO
+
+# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be sorted by
+# fully-qualified names, including namespaces. If set to NO, the class list will
+# be sorted only by class name, not including the namespace part.
+# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES.
+# Note: This option applies only to the class list, not to the alphabetical
+# list.
+# The default value is: NO.
+
+SORT_BY_SCOPE_NAME = NO
+
+# If the STRICT_PROTO_MATCHING option is enabled and doxygen fails to do proper
+# type resolution of all parameters of a function it will reject a match between
+# the prototype and the implementation of a member function even if there is
+# only one candidate or it is obvious which candidate to choose by doing a
+# simple string match. By disabling STRICT_PROTO_MATCHING doxygen will still
+# accept a match between prototype and implementation in such cases.
+# The default value is: NO.
+
+STRICT_PROTO_MATCHING = NO
+
+# The GENERATE_TODOLIST tag can be used to enable (YES) or disable (NO) the todo
+# list. This list is created by putting \todo commands in the documentation.
+# The default value is: YES.
+
+GENERATE_TODOLIST = YES
+
+# The GENERATE_TESTLIST tag can be used to enable (YES) or disable (NO) the test
+# list. This list is created by putting \test commands in the documentation.
+# The default value is: YES.
+
+GENERATE_TESTLIST = YES
+
+# The GENERATE_BUGLIST tag can be used to enable (YES) or disable (NO) the bug
+# list. This list is created by putting \bug commands in the documentation.
+# The default value is: YES.
+
+GENERATE_BUGLIST = YES
+
+# The GENERATE_DEPRECATEDLIST tag can be used to enable (YES) or disable (NO)
+# the deprecated list. This list is created by putting \deprecated commands in
+# the documentation.
+# The default value is: YES.
+
+GENERATE_DEPRECATEDLIST= YES
+
+# The ENABLED_SECTIONS tag can be used to enable conditional documentation
+# sections, marked by \if ... \endif and \cond
+# ... \endcond blocks.
+
+ENABLED_SECTIONS =
+
+# The MAX_INITIALIZER_LINES tag determines the maximum number of lines that the
+# initial value of a variable or macro / define can have for it to appear in the
+# documentation. If the initializer consists of more lines than specified here
+# it will be hidden. Use a value of 0 to hide initializers completely. The
+# appearance of the value of individual variables and macros / defines can be
+# controlled using \showinitializer or \hideinitializer command in the
+# documentation regardless of this setting.
+# Minimum value: 0, maximum value: 10000, default value: 30.
+
+MAX_INITIALIZER_LINES = 30
+
+# Set the SHOW_USED_FILES tag to NO to disable the list of files generated at
+# the bottom of the documentation of classes and structs. If set to YES, the
+# list will mention the files that were used to generate the documentation.
+# The default value is: YES.
+
+SHOW_USED_FILES = YES
+
+# Set the SHOW_FILES tag to NO to disable the generation of the Files page. This
+# will remove the Files entry from the Quick Index and from the Folder Tree View
+# (if specified).
+# The default value is: YES.
+
+SHOW_FILES = YES
+
+# Set the SHOW_NAMESPACES tag to NO to disable the generation of the Namespaces
+# page. This will remove the Namespaces entry from the Quick Index and from the
+# Folder Tree View (if specified).
+# The default value is: YES.
+
+SHOW_NAMESPACES = YES
+
+# The FILE_VERSION_FILTER tag can be used to specify a program or script that
+# doxygen should invoke to get the current version for each file (typically from
+# the version control system). Doxygen will invoke the program by executing (via
+# popen()) the command command input-file, where command is the value of the
+# FILE_VERSION_FILTER tag, and input-file is the name of an input file provided
+# by doxygen. Whatever the program writes to standard output is used as the file
+# version. For an example see the documentation.
+
+FILE_VERSION_FILTER =
+
+# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed
+# by doxygen. The layout file controls the global structure of the generated
+# output files in an output format independent way. To create the layout file
+# that represents doxygen's defaults, run doxygen with the -l option. You can
+# optionally specify a file name after the option, if omitted DoxygenLayout.xml
+# will be used as the name of the layout file.
+#
+# Note that if you run doxygen from a directory containing a file called
+# DoxygenLayout.xml, doxygen will parse it automatically even if the LAYOUT_FILE
+# tag is left empty.
+
+LAYOUT_FILE =
+
+# The CITE_BIB_FILES tag can be used to specify one or more bib files containing
+# the reference definitions. This must be a list of .bib files. The .bib
+# extension is automatically appended if omitted. This requires the bibtex tool
+# to be installed. See also http://en.wikipedia.org/wiki/BibTeX for more info.
+# For LaTeX the style of the bibliography can be controlled using
+# LATEX_BIB_STYLE. To use this feature you need bibtex and perl available in the
+# search path. See also \cite for info how to create references.
+
+CITE_BIB_FILES =
+
+#---------------------------------------------------------------------------
+# Configuration options related to warning and progress messages
+#---------------------------------------------------------------------------
+
+# The QUIET tag can be used to turn on/off the messages that are generated to
+# standard output by doxygen. If QUIET is set to YES this implies that the
+# messages are off.
+# The default value is: NO.
+
+QUIET = NO
+
+# The WARNINGS tag can be used to turn on/off the warning messages that are
+# generated to standard error (stderr) by doxygen. If WARNINGS is set to YES
+# this implies that the warnings are on.
+#
+# Tip: Turn warnings on while writing the documentation.
+# The default value is: YES.
+
+WARNINGS = YES
+
+# If the WARN_IF_UNDOCUMENTED tag is set to YES then doxygen will generate
+# warnings for undocumented members. If EXTRACT_ALL is set to YES then this flag
+# will automatically be disabled.
+# The default value is: YES.
+
+WARN_IF_UNDOCUMENTED = YES
+
+# If the WARN_IF_DOC_ERROR tag is set to YES, doxygen will generate warnings for
+# potential errors in the documentation, such as not documenting some parameters
+# in a documented function, or documenting parameters that don't exist or using
+# markup commands wrongly.
+# The default value is: YES.
+
+WARN_IF_DOC_ERROR = YES
+
+# This WARN_NO_PARAMDOC option can be enabled to get warnings for functions that
+# are documented, but have no documentation for their parameters or return
+# value. If set to NO, doxygen will only warn about wrong or incomplete
+# parameter documentation, but not about the absence of documentation.
+# The default value is: NO.
+
+WARN_NO_PARAMDOC = NO
+
+# The WARN_FORMAT tag determines the format of the warning messages that doxygen
+# can produce. The string should contain the $file, $line, and $text tags, which
+# will be replaced by the file and line number from which the warning originated
+# and the warning text. Optionally the format may contain $version, which will
+# be replaced by the version of the file (if it could be obtained via
+# FILE_VERSION_FILTER)
+# The default value is: $file:$line: $text.
+
+WARN_FORMAT = "$file:$line: $text"
+
+# The WARN_LOGFILE tag can be used to specify a file to which warning and error
+# messages should be written. If left blank the output is written to standard
+# error (stderr).
+
+WARN_LOGFILE =
+
+#---------------------------------------------------------------------------
+# Configuration options related to the input files
+#---------------------------------------------------------------------------
+
+# The INPUT tag is used to specify the files and/or directories that contain
+# documented source files. You may enter file names like myfile.cpp or
+# directories like /usr/src/myproject. Separate the files or directories with
+# spaces.
+# Note: If this tag is empty the current directory is searched.
+
+INPUT = include
+
+# This tag can be used to specify the character encoding of the source files
+# that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses
+# libiconv (or the iconv built into libc) for the transcoding. See the libiconv
+# documentation (see: http://www.gnu.org/software/libiconv) for the list of
+# possible encodings.
+# The default value is: UTF-8.
+
+INPUT_ENCODING = UTF-8
+
+# If the value of the INPUT tag contains directories, you can use the
+# FILE_PATTERNS tag to specify one or more wildcard patterns (like *.cpp and
+# *.h) to filter out the source-files in the directories. If left blank the
+# following patterns are tested:*.c, *.cc, *.cxx, *.cpp, *.c++, *.java, *.ii,
+# *.ixx, *.ipp, *.i++, *.inl, *.idl, *.ddl, *.odl, *.h, *.hh, *.hxx, *.hpp,
+# *.h++, *.cs, *.d, *.php, *.php4, *.php5, *.phtml, *.inc, *.m, *.markdown,
+# *.md, *.mm, *.dox, *.py, *.f90, *.f, *.for, *.tcl, *.vhd, *.vhdl, *.ucf,
+# *.qsf, *.as and *.js.
+
+FILE_PATTERNS =
+
+# The RECURSIVE tag can be used to specify whether or not subdirectories should
+# be searched for input files as well.
+# The default value is: NO.
+
+RECURSIVE = YES
+
+# The EXCLUDE tag can be used to specify files and/or directories that should be
+# excluded from the INPUT source files. This way you can easily exclude a
+# subdirectory from a directory tree whose root is specified with the INPUT tag.
+#
+# Note that relative paths are relative to the directory from which doxygen is
+# run.
+
+EXCLUDE =
+
+# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or
+# directories that are symbolic links (a Unix file system feature) are excluded
+# from the input.
+# The default value is: NO.
+
+EXCLUDE_SYMLINKS = NO
+
+# If the value of the INPUT tag contains directories, you can use the
+# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude
+# certain files from those directories.
+#
+# Note that the wildcards are matched against the file with absolute path, so to
+# exclude all test directories for example use the pattern */test/*
+
+EXCLUDE_PATTERNS =
+
+# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names
+# (namespaces, classes, functions, etc.) that should be excluded from the
+# output. The symbol name can be a fully qualified name, a word, or if the
+# wildcard * is used, a substring. Examples: ANamespace, AClass,
+# AClass::ANamespace, ANamespace::*Test
+#
+# Note that the wildcards are matched against the file with absolute path, so to
+# exclude all test directories use the pattern */test/*
+
+EXCLUDE_SYMBOLS =
+
+# The EXAMPLE_PATH tag can be used to specify one or more files or directories
+# that contain example code fragments that are included (see the \include
+# command).
+
+EXAMPLE_PATH =
+
+# If the value of the EXAMPLE_PATH tag contains directories, you can use the
+# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp and
+# *.h) to filter out the source-files in the directories. If left blank all
+# files are included.
+
+EXAMPLE_PATTERNS =
+
+# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be
+# searched for input files to be used with the \include or \dontinclude commands
+# irrespective of the value of the RECURSIVE tag.
+# The default value is: NO.
+
+EXAMPLE_RECURSIVE = NO
+
+# The IMAGE_PATH tag can be used to specify one or more files or directories
+# that contain images that are to be included in the documentation (see the
+# \image command).
+
+IMAGE_PATH =
+
+# The INPUT_FILTER tag can be used to specify a program that doxygen should
+# invoke to filter for each input file. Doxygen will invoke the filter program
+# by executing (via popen()) the command:
+#
+#
+#
+# where is the value of the INPUT_FILTER tag, and is the
+# name of an input file. Doxygen will then use the output that the filter
+# program writes to standard output. If FILTER_PATTERNS is specified, this tag
+# will be ignored.
+#
+# Note that the filter must not add or remove lines; it is applied before the
+# code is scanned, but not when the output code is generated. If lines are added
+# or removed, the anchors will not be placed correctly.
+
+INPUT_FILTER =
+
+# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern
+# basis. Doxygen will compare the file name with each pattern and apply the
+# filter if there is a match. The filters are a list of the form: pattern=filter
+# (like *.cpp=my_cpp_filter). See INPUT_FILTER for further information on how
+# filters are used. If the FILTER_PATTERNS tag is empty or if none of the
+# patterns match the file name, INPUT_FILTER is applied.
+
+FILTER_PATTERNS =
+
+# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using
+# INPUT_FILTER) will also be used to filter the input files that are used for
+# producing the source files to browse (i.e. when SOURCE_BROWSER is set to YES).
+# The default value is: NO.
+
+FILTER_SOURCE_FILES = NO
+
+# The FILTER_SOURCE_PATTERNS tag can be used to specify source filters per file
+# pattern. A pattern will override the setting for FILTER_PATTERN (if any) and
+# it is also possible to disable source filtering for a specific pattern using
+# *.ext= (so without naming a filter).
+# This tag requires that the tag FILTER_SOURCE_FILES is set to YES.
+
+FILTER_SOURCE_PATTERNS =
+
+# If the USE_MDFILE_AS_MAINPAGE tag refers to the name of a markdown file that
+# is part of the input, its contents will be placed on the main page
+# (index.html). This can be useful if you have a project on for instance GitHub
+# and want to reuse the introduction page also for the doxygen output.
+
+USE_MDFILE_AS_MAINPAGE =
+
+#---------------------------------------------------------------------------
+# Configuration options related to source browsing
+#---------------------------------------------------------------------------
+
+# If the SOURCE_BROWSER tag is set to YES then a list of source files will be
+# generated. Documented entities will be cross-referenced with these sources.
+#
+# Note: To get rid of all source code in the generated output, make sure that
+# also VERBATIM_HEADERS is set to NO.
+# The default value is: NO.
+
+SOURCE_BROWSER = NO
+
+# Setting the INLINE_SOURCES tag to YES will include the body of functions,
+# classes and enums directly into the documentation.
+# The default value is: NO.
+
+INLINE_SOURCES = NO
+
+# Setting the STRIP_CODE_COMMENTS tag to YES will instruct doxygen to hide any
+# special comment blocks from generated source code fragments. Normal C, C++ and
+# Fortran comments will always remain visible.
+# The default value is: YES.
+
+STRIP_CODE_COMMENTS = YES
+
+# If the REFERENCED_BY_RELATION tag is set to YES then for each documented
+# function all documented functions referencing it will be listed.
+# The default value is: NO.
+
+REFERENCED_BY_RELATION = NO
+
+# If the REFERENCES_RELATION tag is set to YES then for each documented function
+# all documented entities called/used by that function will be listed.
+# The default value is: NO.
+
+REFERENCES_RELATION = NO
+
+# If the REFERENCES_LINK_SOURCE tag is set to YES and SOURCE_BROWSER tag is set
+# to YES then the hyperlinks from functions in REFERENCES_RELATION and
+# REFERENCED_BY_RELATION lists will link to the source code. Otherwise they will
+# link to the documentation.
+# The default value is: YES.
+
+REFERENCES_LINK_SOURCE = YES
+
+# If SOURCE_TOOLTIPS is enabled (the default) then hovering a hyperlink in the
+# source code will show a tooltip with additional information such as prototype,
+# brief description and links to the definition and documentation. Since this
+# will make the HTML file larger and loading of large files a bit slower, you
+# can opt to disable this feature.
+# The default value is: YES.
+# This tag requires that the tag SOURCE_BROWSER is set to YES.
+
+SOURCE_TOOLTIPS = YES
+
+# If the USE_HTAGS tag is set to YES then the references to source code will
+# point to the HTML generated by the htags(1) tool instead of doxygen built-in
+# source browser. The htags tool is part of GNU's global source tagging system
+# (see http://www.gnu.org/software/global/global.html). You will need version
+# 4.8.6 or higher.
+#
+# To use it do the following:
+# - Install the latest version of global
+# - Enable SOURCE_BROWSER and USE_HTAGS in the config file
+# - Make sure the INPUT points to the root of the source tree
+# - Run doxygen as normal
+#
+# Doxygen will invoke htags (and that will in turn invoke gtags), so these
+# tools must be available from the command line (i.e. in the search path).
+#
+# The result: instead of the source browser generated by doxygen, the links to
+# source code will now point to the output of htags.
+# The default value is: NO.
+# This tag requires that the tag SOURCE_BROWSER is set to YES.
+
+USE_HTAGS = NO
+
+# If the VERBATIM_HEADERS tag is set the YES then doxygen will generate a
+# verbatim copy of the header file for each class for which an include is
+# specified. Set to NO to disable this.
+# See also: Section \class.
+# The default value is: YES.
+
+VERBATIM_HEADERS = YES
+
+#---------------------------------------------------------------------------
+# Configuration options related to the alphabetical class index
+#---------------------------------------------------------------------------
+
+# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index of all
+# compounds will be generated. Enable this if the project contains a lot of
+# classes, structs, unions or interfaces.
+# The default value is: YES.
+
+ALPHABETICAL_INDEX = YES
+
+# The COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns in
+# which the alphabetical index list will be split.
+# Minimum value: 1, maximum value: 20, default value: 5.
+# This tag requires that the tag ALPHABETICAL_INDEX is set to YES.
+
+COLS_IN_ALPHA_INDEX = 5
+
+# In case all classes in a project start with a common prefix, all classes will
+# be put under the same header in the alphabetical index. The IGNORE_PREFIX tag
+# can be used to specify a prefix (or a list of prefixes) that should be ignored
+# while generating the index headers.
+# This tag requires that the tag ALPHABETICAL_INDEX is set to YES.
+
+IGNORE_PREFIX =
+
+#---------------------------------------------------------------------------
+# Configuration options related to the HTML output
+#---------------------------------------------------------------------------
+
+# If the GENERATE_HTML tag is set to YES, doxygen will generate HTML output
+# The default value is: YES.
+
+GENERATE_HTML = YES
+
+# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. If a
+# relative path is entered the value of OUTPUT_DIRECTORY will be put in front of
+# it.
+# The default directory is: html.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_OUTPUT = api-html
+
+# The HTML_FILE_EXTENSION tag can be used to specify the file extension for each
+# generated HTML page (for example: .htm, .php, .asp).
+# The default value is: .html.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_FILE_EXTENSION = .html
+
+# The HTML_HEADER tag can be used to specify a user-defined HTML header file for
+# each generated HTML page. If the tag is left blank doxygen will generate a
+# standard header.
+#
+# To get valid HTML the header file that includes any scripts and style sheets
+# that doxygen needs, which is dependent on the configuration options used (e.g.
+# the setting GENERATE_TREEVIEW). It is highly recommended to start with a
+# default header using
+# doxygen -w html new_header.html new_footer.html new_stylesheet.css
+# YourConfigFile
+# and then modify the file new_header.html. See also section "Doxygen usage"
+# for information on how to generate the default header that doxygen normally
+# uses.
+# Note: The header is subject to change so you typically have to regenerate the
+# default header when upgrading to a newer version of doxygen. For a description
+# of the possible markers and block names see the documentation.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_HEADER =
+
+# The HTML_FOOTER tag can be used to specify a user-defined HTML footer for each
+# generated HTML page. If the tag is left blank doxygen will generate a standard
+# footer. See HTML_HEADER for more information on how to generate a default
+# footer and what special commands can be used inside the footer. See also
+# section "Doxygen usage" for information on how to generate the default footer
+# that doxygen normally uses.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_FOOTER =
+
+# The HTML_STYLESHEET tag can be used to specify a user-defined cascading style
+# sheet that is used by each HTML page. It can be used to fine-tune the look of
+# the HTML output. If left blank doxygen will generate a default style sheet.
+# See also section "Doxygen usage" for information on how to generate the style
+# sheet that doxygen normally uses.
+# Note: It is recommended to use HTML_EXTRA_STYLESHEET instead of this tag, as
+# it is more robust and this tag (HTML_STYLESHEET) will in the future become
+# obsolete.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_STYLESHEET =
+
+# The HTML_EXTRA_STYLESHEET tag can be used to specify additional user-defined
+# cascading style sheets that are included after the standard style sheets
+# created by doxygen. Using this option one can overrule certain style aspects.
+# This is preferred over using HTML_STYLESHEET since it does not replace the
+# standard style sheet and is therefore more robust against future updates.
+# Doxygen will copy the style sheet files to the output directory.
+# Note: The order of the extra style sheet files is of importance (e.g. the last
+# style sheet in the list overrules the setting of the previous ones in the
+# list). For an example see the documentation.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_EXTRA_STYLESHEET =
+
+# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or
+# other source files which should be copied to the HTML output directory. Note
+# that these files will be copied to the base HTML output directory. Use the
+# $relpath^ marker in the HTML_HEADER and/or HTML_FOOTER files to load these
+# files. In the HTML_STYLESHEET file, use the file name only. Also note that the
+# files will be copied as-is; there are no commands or markers available.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_EXTRA_FILES =
+
+# The HTML_COLORSTYLE_HUE tag controls the color of the HTML output. Doxygen
+# will adjust the colors in the style sheet and background images according to
+# this color. Hue is specified as an angle on a colorwheel, see
+# http://en.wikipedia.org/wiki/Hue for more information. For instance the value
+# 0 represents red, 60 is yellow, 120 is green, 180 is cyan, 240 is blue, 300
+# purple, and 360 is red again.
+# Minimum value: 0, maximum value: 359, default value: 220.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_COLORSTYLE_HUE = 203
+
+# The HTML_COLORSTYLE_SAT tag controls the purity (or saturation) of the colors
+# in the HTML output. For a value of 0 the output will use grayscales only. A
+# value of 255 will produce the most vivid colors.
+# Minimum value: 0, maximum value: 255, default value: 100.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_COLORSTYLE_SAT = 150
+
+# The HTML_COLORSTYLE_GAMMA tag controls the gamma correction applied to the
+# luminance component of the colors in the HTML output. Values below 100
+# gradually make the output lighter, whereas values above 100 make the output
+# darker. The value divided by 100 is the actual gamma applied, so 80 represents
+# a gamma of 0.8, The value 220 represents a gamma of 2.2, and 100 does not
+# change the gamma.
+# Minimum value: 40, maximum value: 240, default value: 80.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_COLORSTYLE_GAMMA = 80
+
+# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML
+# page will contain the date and time when the page was generated. Setting this
+# to NO can help when comparing the output of multiple runs.
+# The default value is: YES.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_TIMESTAMP = NO
+
+# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML
+# documentation will contain sections that can be hidden and shown after the
+# page has loaded.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_DYNAMIC_SECTIONS = YES
+
+# With HTML_INDEX_NUM_ENTRIES one can control the preferred number of entries
+# shown in the various tree structured indices initially; the user can expand
+# and collapse entries dynamically later on. Doxygen will expand the tree to
+# such a level that at most the specified number of entries are visible (unless
+# a fully collapsed tree already exceeds this amount). So setting the number of
+# entries 1 will produce a full collapsed tree by default. 0 is a special value
+# representing an infinite number of entries and will result in a full expanded
+# tree by default.
+# Minimum value: 0, maximum value: 9999, default value: 100.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+HTML_INDEX_NUM_ENTRIES = 100
+
+# If the GENERATE_DOCSET tag is set to YES, additional index files will be
+# generated that can be used as input for Apple's Xcode 3 integrated development
+# environment (see: http://developer.apple.com/tools/xcode/), introduced with
+# OSX 10.5 (Leopard). To create a documentation set, doxygen will generate a
+# Makefile in the HTML output directory. Running make will produce the docset in
+# that directory and running make install will install the docset in
+# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find it at
+# startup. See http://developer.apple.com/tools/creatingdocsetswithdoxygen.html
+# for more information.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+GENERATE_DOCSET = NO
+
+# This tag determines the name of the docset feed. A documentation feed provides
+# an umbrella under which multiple documentation sets from a single provider
+# (such as a company or product suite) can be grouped.
+# The default value is: Doxygen generated docs.
+# This tag requires that the tag GENERATE_DOCSET is set to YES.
+
+DOCSET_FEEDNAME = "Doxygen generated docs"
+
+# This tag specifies a string that should uniquely identify the documentation
+# set bundle. This should be a reverse domain-name style string, e.g.
+# com.mycompany.MyDocSet. Doxygen will append .docset to the name.
+# The default value is: org.doxygen.Project.
+# This tag requires that the tag GENERATE_DOCSET is set to YES.
+
+DOCSET_BUNDLE_ID = org.doxygen.Project
+
+# The DOCSET_PUBLISHER_ID tag specifies a string that should uniquely identify
+# the documentation publisher. This should be a reverse domain-name style
+# string, e.g. com.mycompany.MyDocSet.documentation.
+# The default value is: org.doxygen.Publisher.
+# This tag requires that the tag GENERATE_DOCSET is set to YES.
+
+DOCSET_PUBLISHER_ID = org.doxygen.Publisher
+
+# The DOCSET_PUBLISHER_NAME tag identifies the documentation publisher.
+# The default value is: Publisher.
+# This tag requires that the tag GENERATE_DOCSET is set to YES.
+
+DOCSET_PUBLISHER_NAME = Publisher
+
+# If the GENERATE_HTMLHELP tag is set to YES then doxygen generates three
+# additional HTML index files: index.hhp, index.hhc, and index.hhk. The
+# index.hhp is a project file that can be read by Microsoft's HTML Help Workshop
+# (see: http://www.microsoft.com/en-us/download/details.aspx?id=21138) on
+# Windows.
+#
+# The HTML Help Workshop contains a compiler that can convert all HTML output
+# generated by doxygen into a single compiled HTML file (.chm). Compiled HTML
+# files are now used as the Windows 98 help format, and will replace the old
+# Windows help format (.hlp) on all Windows platforms in the future. Compressed
+# HTML files also contain an index, a table of contents, and you can search for
+# words in the documentation. The HTML workshop also contains a viewer for
+# compressed HTML files.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+GENERATE_HTMLHELP = NO
+
+# The CHM_FILE tag can be used to specify the file name of the resulting .chm
+# file. You can add a path in front of the file if the result should not be
+# written to the html output directory.
+# This tag requires that the tag GENERATE_HTMLHELP is set to YES.
+
+CHM_FILE =
+
+# The HHC_LOCATION tag can be used to specify the location (absolute path
+# including file name) of the HTML help compiler (hhc.exe). If non-empty,
+# doxygen will try to run the HTML help compiler on the generated index.hhp.
+# The file has to be specified with full path.
+# This tag requires that the tag GENERATE_HTMLHELP is set to YES.
+
+HHC_LOCATION =
+
+# The GENERATE_CHI flag controls if a separate .chi index file is generated
+# (YES) or that it should be included in the master .chm file (NO).
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTMLHELP is set to YES.
+
+GENERATE_CHI = NO
+
+# The CHM_INDEX_ENCODING is used to encode HtmlHelp index (hhk), content (hhc)
+# and project file content.
+# This tag requires that the tag GENERATE_HTMLHELP is set to YES.
+
+CHM_INDEX_ENCODING =
+
+# The BINARY_TOC flag controls whether a binary table of contents is generated
+# (YES) or a normal table of contents (NO) in the .chm file. Furthermore it
+# enables the Previous and Next buttons.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTMLHELP is set to YES.
+
+BINARY_TOC = NO
+
+# The TOC_EXPAND flag can be set to YES to add extra items for group members to
+# the table of contents of the HTML help documentation and to the tree view.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTMLHELP is set to YES.
+
+TOC_EXPAND = NO
+
+# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and
+# QHP_VIRTUAL_FOLDER are set, an additional index file will be generated that
+# can be used as input for Qt's qhelpgenerator to generate a Qt Compressed Help
+# (.qch) of the generated HTML documentation.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+GENERATE_QHP = NO
+
+# If the QHG_LOCATION tag is specified, the QCH_FILE tag can be used to specify
+# the file name of the resulting .qch file. The path specified is relative to
+# the HTML output folder.
+# This tag requires that the tag GENERATE_QHP is set to YES.
+
+QCH_FILE =
+
+# The QHP_NAMESPACE tag specifies the namespace to use when generating Qt Help
+# Project output. For more information please see Qt Help Project / Namespace
+# (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#namespace).
+# The default value is: org.doxygen.Project.
+# This tag requires that the tag GENERATE_QHP is set to YES.
+
+QHP_NAMESPACE = org.doxygen.Project
+
+# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating Qt
+# Help Project output. For more information please see Qt Help Project / Virtual
+# Folders (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#virtual-
+# folders).
+# The default value is: doc.
+# This tag requires that the tag GENERATE_QHP is set to YES.
+
+QHP_VIRTUAL_FOLDER = doc
+
+# If the QHP_CUST_FILTER_NAME tag is set, it specifies the name of a custom
+# filter to add. For more information please see Qt Help Project / Custom
+# Filters (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#custom-
+# filters).
+# This tag requires that the tag GENERATE_QHP is set to YES.
+
+QHP_CUST_FILTER_NAME =
+
+# The QHP_CUST_FILTER_ATTRS tag specifies the list of the attributes of the
+# custom filter to add. For more information please see Qt Help Project / Custom
+# Filters (see: http://qt-project.org/doc/qt-4.8/qthelpproject.html#custom-
+# filters).
+# This tag requires that the tag GENERATE_QHP is set to YES.
+
+QHP_CUST_FILTER_ATTRS =
+
+# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this
+# project's filter section matches. Qt Help Project / Filter Attributes (see:
+# http://qt-project.org/doc/qt-4.8/qthelpproject.html#filter-attributes).
+# This tag requires that the tag GENERATE_QHP is set to YES.
+
+QHP_SECT_FILTER_ATTRS =
+
+# The QHG_LOCATION tag can be used to specify the location of Qt's
+# qhelpgenerator. If non-empty doxygen will try to run qhelpgenerator on the
+# generated .qhp file.
+# This tag requires that the tag GENERATE_QHP is set to YES.
+
+QHG_LOCATION =
+
+# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files will be
+# generated, together with the HTML files, they form an Eclipse help plugin. To
+# install this plugin and make it available under the help contents menu in
+# Eclipse, the contents of the directory containing the HTML and XML files needs
+# to be copied into the plugins directory of eclipse. The name of the directory
+# within the plugins directory should be the same as the ECLIPSE_DOC_ID value.
+# After copying Eclipse needs to be restarted before the help appears.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+GENERATE_ECLIPSEHELP = NO
+
+# A unique identifier for the Eclipse help plugin. When installing the plugin
+# the directory name containing the HTML and XML files should also have this
+# name. Each documentation set should have its own identifier.
+# The default value is: org.doxygen.Project.
+# This tag requires that the tag GENERATE_ECLIPSEHELP is set to YES.
+
+ECLIPSE_DOC_ID = org.doxygen.Project
+
+# If you want full control over the layout of the generated HTML pages it might
+# be necessary to disable the index and replace it with your own. The
+# DISABLE_INDEX tag can be used to turn on/off the condensed index (tabs) at top
+# of each HTML page. A value of NO enables the index and the value YES disables
+# it. Since the tabs in the index contain the same information as the navigation
+# tree, you can set this option to YES if you also set GENERATE_TREEVIEW to YES.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+DISABLE_INDEX = NO
+
+# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index
+# structure should be generated to display hierarchical information. If the tag
+# value is set to YES, a side panel will be generated containing a tree-like
+# index structure (just like the one that is generated for HTML Help). For this
+# to work a browser that supports JavaScript, DHTML, CSS and frames is required
+# (i.e. any modern browser). Windows users are probably better off using the
+# HTML help feature. Via custom style sheets (see HTML_EXTRA_STYLESHEET) one can
+# further fine-tune the look of the index. As an example, the default style
+# sheet generated by doxygen has an example that shows how to put an image at
+# the root of the tree instead of the PROJECT_NAME. Since the tree basically has
+# the same information as the tab index, you could consider setting
+# DISABLE_INDEX to YES when enabling this option.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+GENERATE_TREEVIEW = NO
+
+# The ENUM_VALUES_PER_LINE tag can be used to set the number of enum values that
+# doxygen will group on one line in the generated HTML documentation.
+#
+# Note that a value of 0 will completely suppress the enum values from appearing
+# in the overview section.
+# Minimum value: 0, maximum value: 20, default value: 4.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+ENUM_VALUES_PER_LINE = 4
+
+# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be used
+# to set the initial width (in pixels) of the frame in which the tree is shown.
+# Minimum value: 0, maximum value: 1500, default value: 250.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+TREEVIEW_WIDTH = 250
+
+# If the EXT_LINKS_IN_WINDOW option is set to YES, doxygen will open links to
+# external symbols imported via tag files in a separate window.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+EXT_LINKS_IN_WINDOW = NO
+
+# Use this tag to change the font size of LaTeX formulas included as images in
+# the HTML documentation. When you change the font size after a successful
+# doxygen run you need to manually remove any form_*.png images from the HTML
+# output directory to force them to be regenerated.
+# Minimum value: 8, maximum value: 50, default value: 10.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+FORMULA_FONTSIZE = 10
+
+# Use the FORMULA_TRANPARENT tag to determine whether or not the images
+# generated for formulas are transparent PNGs. Transparent PNGs are not
+# supported properly for IE 6.0, but are supported on all modern browsers.
+#
+# Note that when changing this option you need to delete any form_*.png files in
+# the HTML output directory before the changes have effect.
+# The default value is: YES.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+FORMULA_TRANSPARENT = YES
+
+# Enable the USE_MATHJAX option to render LaTeX formulas using MathJax (see
+# http://www.mathjax.org) which uses client side Javascript for the rendering
+# instead of using pre-rendered bitmaps. Use this if you do not have LaTeX
+# installed or if you want to formulas look prettier in the HTML output. When
+# enabled you may also need to install MathJax separately and configure the path
+# to it using the MATHJAX_RELPATH option.
+# The default value is: NO.
+# This tag requires that the tag GENERATE_HTML is set to YES.
+
+USE_MATHJAX = NO
+
+# When MathJax is enabled you can set the default output format to be used for
+# the MathJax output. See the MathJax site (see:
+# http://docs.mathjax.org/en/latest/output.html) for more details.
+# Possible values are: HTML-CSS (which is slower, but has the best
+# compatibility), NativeMML (i.e. MathML) and SVG.
+# The default value is: HTML-CSS.
+# This tag requires that the tag USE_MATHJAX is set to YES.
+
+MATHJAX_FORMAT = HTML-CSS
+
+# When MathJax is enabled you need to specify the location relative to the HTML
+# output directory using the MATHJAX_RELPATH option. The destination directory
+# should contain the MathJax.js script. For instance, if the mathjax directory
+# is located at the same level as the HTML output directory, then
+# MATHJAX_RELPATH should be ../mathjax. The default value points to the MathJax
+# Content Delivery Network so you can quickly see the result without installing
+# MathJax. However, it is strongly recommended to install a local copy of
+# MathJax from http://www.mathjax.org before deployment.
+# The default value is: http://cdn.mathjax.org/mathjax/latest.
+# This tag requires that the tag USE_MATHJAX is set to YES.
+
+MATHJAX_RELPATH = http://cdn.mathjax.org/mathjax/latest
+
+# The MATHJAX_EXTENSIONS tag can be used to specify one or more MathJax
+# extension names that should be enabled during MathJax rendering. For example
+# MATHJAX_EXTENSIONS = TeX/AMSmath TeX/AMSsymbols
+# This tag requires that the tag USE_MATHJAX is set to YES.
+
+MATHJAX_EXTENSIONS =
+
+# The MATHJAX_CODEFILE tag can be used to specify a file with javascript pieces
+# of code that will be used on startup of the MathJax code. See the MathJax site
+# (see: http://docs.mathjax.org/en/latest/output.html) for more details. For an
+# example see the documentation.
+# This tag requires that the tag USE_MATHJAX is set to YES.
+
+MATHJAX_CODEFILE =
+
+# When the SEARCHENGINE tag is enabled doxygen will generate a search box for
+# the HTML output. The underlying search engine uses javascript and DHTML and
+# should work on any modern browser. Note that when using HTML help
+# (GENERATE_HTMLHELP), Qt help (GENERATE_QHP), or docsets (GENERATE_DOCSET)
+# there is already a search function so this one should typically be disabled.
+# For large projects the javascript based search engine can be slow, then
+# enabling SERVER_BASED_SEARCH may provide a better solution. It is possible to
+# search using the keyboard; to jump to the search box use + S
+# (what the is depends on the OS and browser, but it is typically
+# , /
+
+./cpphoaf
+
+
+
Alternatively, you have downloaded a precompiled cpphoaf binary from the website.
+
+
+Here are some examples for the command-line cpphoaf tool:
+
+
+
Parsing (validating) an automaton in HOA format
+
+
+./cpphoaf parse automaton-file.hoa
+
+
+Some of the semantic validations can be disabled by the command-line option
+--no-validate.
+
+
+
Printing an automaton in HOA format to standard output
+Further details on the command-line tool can be found here.
+
+
The HOA Parser Library
+
+
The cpphoafparser library can also be used to parse HOA automata.
+For example, you might want to read such automata in a tool or
+you might want to implement your own automata transformations.
+
+
+
+As a first step, download the source code of the library from the
+website.
+Then, build a local copy of the API documentation with the Doxygen tool:
+
+
+doxygen Doxyfile
+
+
This produces the API documentation in the docs/api-html subdirectory.
+The alternative Doxyfile.all configuration file produces documentation for all
+the private/implementation details as well. If you do not have the dot utility
+installed, set HAVE_DOT = NO in Doxyfile.
+
+A good starting point is the API documentation of the HOAConsumer
+interface and the source code of src/cpphoaf.cc,
+where you can see how the parser is invoked.
+To parse automata using the cpphoafparser library,
+an application provides the parser with a class which implements the HOAConsumer interface.
+The parser then invokes the functions corresponding to the element in the HOA file format while parsing the automaton.
+
+
+
The Parser Library: Further information
+
+
More details and an overview over the cpphoafparser architecture can be found here.
+
+
If you have further questions, find bugs or want to tell
+us about your use of the cpphoafparser library, please feel free to contact us!
+
+
(c) 2015-2016
+Joachim Klein <klein@tcs.inf.tu-dresden.de>,
+David Müller <david.mueller@tcs.inf.tu-dresden.de>
+
+
+
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/atom_acceptance.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/atom_acceptance.hh
new file mode 100644
index 000000000..f5022020c
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/atom_acceptance.hh
@@ -0,0 +1,115 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+
+#ifndef CPPHOAFPARSER_ATOMACCEPTANCE_H
+#define CPPHOAFPARSER_ATOMACCEPTANCE_H
+
+#include
+#include
+
+namespace cpphoafparser {
+
+/**
+ * Atom of an acceptance condition, either Fin(accSet), Fin(!accSet), Inf(accSet) or Inf(!accSet)
+ */
+class AtomAcceptance {
+public:
+ /** A shared_ptr wrapping an AtomAcceptance */
+ typedef std::shared_ptr ptr;
+
+ /** The type of the temporal operator (Fin / Inf) */
+ enum AtomType {TEMPORAL_FIN, TEMPORAL_INF};
+
+ /**
+ * Constructor.
+ * @param kind the type of the temporal operator (Fin / Inf)
+ * @param accSet the acceptance set index
+ * @param negated is the acceptance set negated?
+ **/
+ AtomAcceptance(AtomType kind, unsigned int accSet, bool negated)
+ : kind(kind), accSet(accSet), negated(negated) {
+ }
+
+ /** Static constructor for a Fin(accSet) atom. */
+ static ptr Fin(unsigned int accSet) {
+ return ptr(new AtomAcceptance(TEMPORAL_FIN, accSet, false));
+ }
+
+ /** Static constructor for a Fin(!accSet) atom. */
+ static ptr FinNot(unsigned int accSet) {
+ return ptr(new AtomAcceptance(TEMPORAL_FIN, accSet, true));
+ }
+
+ /** Static constructor for an Inf(accSet) atom. */
+ static ptr Inf(unsigned int accSet) {
+ return ptr(new AtomAcceptance(TEMPORAL_INF, accSet, false));
+ }
+
+ /** Static constructor for a Inf(!accSet) atom. */
+ static ptr InfNot(unsigned int accSet) {
+ return ptr(new AtomAcceptance(TEMPORAL_INF, accSet, true));
+ }
+
+ /** Get the temporal operator type of this atom. */
+ AtomType getType() const {return kind;}
+ /** Get the acceptance set index of this atom. */
+ unsigned int getAcceptanceSet() const {return accSet;}
+ /** Is the acceptance set negated? */
+ bool isNegated() const {return negated;}
+
+ /** Output operator, renders atom in HOA syntax */
+ friend std::ostream& operator<<(std::ostream& out, const AtomAcceptance& atom) {
+ out << (atom.kind == TEMPORAL_FIN ? "Fin" : "Inf");
+ out << "(";
+ if (atom.negated) out << "!";
+ out << atom.accSet;
+ out << ")";
+ return out;
+ }
+
+ /** Equality operator */
+ bool operator==(const AtomAcceptance& other) const {
+ return
+ this->kind == other.kind &&
+ this->accSet == other.accSet &&
+ this->negated == other.negated;
+ }
+
+private:
+ /** The temporal operator of this atom */
+ AtomType kind;
+ /** The acceptance set index of this atom */
+ unsigned int accSet;
+ /** Is the acceptance set negated? */
+ bool negated;
+};
+
+}
+
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/atom_label.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/atom_label.hh
new file mode 100644
index 000000000..dcc852c79
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/atom_label.hh
@@ -0,0 +1,120 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_ATOMLABEL_HH
+#define CPPHOAFPARSER_ATOMLABEL_HH
+
+#include
+#include
+#include
+
+namespace cpphoafparser {
+
+/**
+ * Atom of a label expression (either an atomic proposition index or an alias reference)
+ */
+class AtomLabel {
+public:
+ /** A shared_ptr wrapping an AtomLabel */
+ typedef std::shared_ptr ptr;
+
+ /** Static constructor for an atomic proposition atom */
+ static AtomLabel::ptr createAPIndex(unsigned int apIndex) {
+ return AtomLabel::ptr(new AtomLabel(apIndex));
+ }
+
+ /** Static constructor for an alias reference (name has to be without leading @) */
+ static AtomLabel::ptr createAlias(const std::string name) {
+ return AtomLabel::ptr(new AtomLabel(name));
+ }
+
+ /** Copy constructor. */
+ AtomLabel(const AtomLabel& other) : apIndex(0), aliasName(nullptr) {
+ if (other.isAlias()) {
+ aliasName = std::shared_ptr(new std::string(*other.aliasName));
+ } else {
+ apIndex = other.apIndex;
+ }
+ }
+
+ /** Returns true if this atom is an alias reference */
+ bool isAlias() const {return (bool)aliasName;}
+
+ /**
+ * Returns the alias name (for an alias reference atom).
+ * May only be called if `isAlias() == true`.
+ */
+ const std::string& getAliasName() const {
+ if (!isAlias()) {throw std::logic_error("Illegal access");}
+ return *aliasName;
+ }
+
+ /**
+ * Returns the atomic proposition index (for an AP atom).
+ * May only be called if `isAlias() == false`.
+ */
+ unsigned int getAPIndex() const {
+ if (isAlias()) {throw std::logic_error("Illegal access");}
+ return apIndex;
+ }
+
+ /** Output operator, renders in HOA syntax */
+ friend std::ostream& operator<<(std::ostream& out, const AtomLabel& atom) {
+ if (atom.isAlias()) {
+ out << "@" << *atom.aliasName;
+ } else {
+ out << atom.apIndex;
+ }
+ return out;
+ }
+
+ /** Equality operator. */
+ bool operator==(const AtomLabel& other) const {
+ if (isAlias()) {
+ return other.isAlias() && getAliasName() == other.getAliasName();
+ } else {
+ return !other.isAlias() && getAPIndex() == other.getAPIndex();
+ }
+ }
+
+
+private:
+ /** The AP index (if applicable) */
+ unsigned int apIndex;
+ /** The aliasName (empty pointer if AP atom) */
+ std::shared_ptr aliasName;
+
+ /** Private constructor (AP atom) */
+ AtomLabel(unsigned int apIndex) : apIndex(apIndex), aliasName(nullptr) {}
+ /** Private constructor (alias reference atom) */
+ AtomLabel(const std::string& name) : apIndex(0), aliasName(new std::string(name)) {}
+};
+
+}
+
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/boolean_expression.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/boolean_expression.hh
new file mode 100644
index 000000000..b173d6013
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/boolean_expression.hh
@@ -0,0 +1,302 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_BOOLEANEXPRESSION_H
+#define CPPHOAFPARSER_BOOLEANEXPRESSION_H
+
+#include
+#include
+#include
+#include
+
+namespace cpphoafparser {
+
+/**
+ * This represents (a node of) an abstract syntax tree
+ * of a boolean expression, parametrized with the type
+ * of leaf nodes (atoms).
+ *
+ * The nodes are designed to be immutable, which allows
+ * sharing of subexpression in a safe way between multiple
+ * trees.
+ *
+ * For unary operator (NOT), the child is stored as the
+ * left child of the not.
+ *
+ * With AtomLabel, this represents a label expression
+ * over atomic propositions, with AtomAcceptance an
+ * expression of Fin/Inf acceptance conditions.
+ *
+ * @tparam The atoms (leaf nodes) in the abstract syntax tree.
+ */
+template
+class BooleanExpression {
+public:
+ /** A shared_ptr to a node in this AST */
+ typedef std::shared_ptr< BooleanExpression > ptr;
+ /** A shared_ptr to an atom (leaf node) in this AST */
+ typedef std::shared_ptr< Atoms> atom_ptr;
+
+ /** The node types of this AST */
+ enum OperatorType {
+ EXP_AND,
+ EXP_OR,
+ EXP_NOT,
+ EXP_TRUE,
+ EXP_FALSE,
+ EXP_ATOM
+ };
+
+ /** Get the node type for this node */
+ OperatorType getType() {
+ return kind;
+ }
+
+ /** Static constructor for a node representing a TRUE leaf */
+ static ptr True() {return ptr(new BooleanExpression(true));}
+ /** Static constructor for a node representing a FALSE leaf */
+ static ptr False() {return ptr(new BooleanExpression(false));}
+ /** Static constructor for a node representing an atom leaf */
+ static ptr Atom(atom_ptr atom) {return ptr(new BooleanExpression(atom));}
+
+ /**
+ * Constructor for a node, providing the type and left and right child nodes.
+ *
+ * For unary operators, the `right` node should be an empty pointer.
+ **/
+ BooleanExpression(OperatorType kind, ptr left, ptr right) :
+ kind(kind), left(left), right(right), atom(nullptr) {
+ }
+
+ /**
+ * Constructor for a TRUE/FALSE leaf node.
+ */
+ BooleanExpression(bool value) :
+ left(nullptr), right(nullptr), atom(nullptr) {
+ if (value) {
+ kind = EXP_TRUE;
+ } else {
+ kind = EXP_FALSE;
+ }
+ }
+
+ /** Constructor for an atom node */
+ BooleanExpression(atom_ptr atom) :
+ kind(EXP_ATOM), left(nullptr), right(nullptr), atom(atom) {
+ }
+
+ /** Constructor for an atom node (copies atom) */
+ BooleanExpression(const Atoms& atom) :
+ kind(EXP_ATOM), left(nullptr), right(nullptr), atom(new Atoms(atom)) {
+ }
+
+ /** Perform a deep copy (recursive) of this AST and return the result */
+ ptr deepCopy() {
+ switch (kind) {
+ case EXP_AND:
+ return ptr(new BooleanExpression(EXP_AND, left->deepCopy(), right->deepCopy()));
+ case EXP_OR:
+ return ptr(new BooleanExpression(EXP_OR, left->deepCopy(), right->deepCopy()));
+ case EXP_NOT:
+ return ptr(new BooleanExpression(EXP_NOT, left->deepCopy(), nullptr));
+ case EXP_TRUE:
+ return True();
+ case EXP_FALSE:
+ return False();
+ case EXP_ATOM:
+ return ptr(new BooleanExpression(*atom));
+ }
+ throw std::logic_error("Unsupported operator");
+ }
+
+ /** Get the left child node (might be an empty pointer) */
+ ptr getLeft() const {return left;}
+ /** Get the right child node (might be an empty pointer) */
+ ptr getRight() const {return right;}
+ /** Get the atom for an EXP_ATOM node. May only be called if `isAtom() == true` */
+ const Atoms& getAtom() const {
+ if (!isAtom()) throw std::logic_error("Illegal access");
+ return *atom;
+ }
+
+ /** Returns true if this node is an EXP_AND node */
+ bool isAND() const {return kind==EXP_AND;}
+ /** Returns true if this node is an EXP_OR node */
+ bool isOR() const {return kind==EXP_OR;}
+ /** Returns true if this node is an EXP_NOT node */
+ bool isNOT() const {return kind==EXP_NOT;}
+ /** Returns true if this node is an EXP_TRUE node */
+ bool isTRUE() const {return kind==EXP_TRUE;}
+ /** Returns true if this node is an EXP_FALSE node */
+ bool isFALSE() const {return kind==EXP_FALSE;}
+ /** Returns true if this node is an EXP_ATOM node */
+ bool isAtom() const {return kind==EXP_ATOM;}
+
+ /** Conjunction operator */
+ friend ptr operator&(ptr left, ptr right) {
+ return ptr(new BooleanExpression(EXP_AND, left, right));
+ }
+
+ /** Disjunction operator */
+ friend ptr operator|(ptr left, ptr right) {
+ return ptr(new BooleanExpression(EXP_OR, left, right));
+ }
+
+ /** Negation operator */
+ friend ptr operator!(ptr other) {
+ return ptr(new BooleanExpression(EXP_NOT, other, nullptr));
+ }
+
+ /** Output operator, renders in HOA syntax */
+ friend std::ostream& operator<<(std::ostream& out, const BooleanExpression& expr) {
+ switch (expr.kind) {
+ case EXP_AND: {
+ bool paren = expr.left->needsParentheses(EXP_AND);
+ if (paren) out << "(";
+ out << *expr.left;
+ if (paren) out << ")";
+
+ out << " & ";
+
+ paren = expr.right->needsParentheses(EXP_AND);
+ if (paren) out << "(";
+ out << *expr.right;
+ if (paren) out << ")";
+ return out;
+ }
+ case EXP_OR: {
+ bool paren = expr.left->needsParentheses(EXP_OR);
+ if (paren) out << "(";
+ out << *expr.left;
+ if (paren) out << ")";
+
+ out << " | ";
+
+ paren = expr.right->needsParentheses(EXP_OR);
+ if (paren) out << "(";
+ out << *expr.right;
+ if (paren) out << ")";
+ return out;
+ }
+ case EXP_NOT: {
+ bool paren = expr.left->needsParentheses(EXP_NOT);
+ out << "!";
+ if (paren) out << "(";
+ out << *expr.left;
+ if (paren) out << ")";
+ return out;
+ }
+ case EXP_TRUE:
+ out << "t";
+ return out;
+ case EXP_FALSE:
+ out << "f";
+ return out;
+ case EXP_ATOM:
+ out << *(expr.atom);
+ return out;
+ }
+ throw std::logic_error("Unhandled operator");
+ }
+
+ /** Return a string representation of this AST (HOA syntax) */
+ std::string toString() const {
+ std::stringstream ss;
+ ss << *this;
+ return ss.str();
+ }
+
+ /**
+ * Returns `true` if `expr1` and `expr2` are syntactically equal.
+ * Two AST are syntactically equal if the trees match and the
+ * atoms are equal.
+ */
+ static bool areSyntacticallyEqual(ptr expr1, ptr expr2)
+ {
+ if (!expr1.get() || !expr2.get()) return false;
+ if (expr1->getType() != expr2->getType()) return false;
+
+ switch (expr1->getType()) {
+ case EXP_TRUE:
+ case EXP_FALSE:
+ return true;
+ case EXP_AND:
+ case EXP_OR:
+ if (!areSyntacticallyEqual(expr1->getLeft(), expr2->getLeft())) return false;
+ if (!areSyntacticallyEqual(expr1->getRight(), expr2->getRight())) return false;
+ return true;
+ case EXP_NOT:
+ if (!areSyntacticallyEqual(expr1->getLeft(), expr2->getLeft())) return false;
+ return true;
+ case EXP_ATOM:
+ return expr1->getAtom() == expr2->getAtom();
+ }
+ throw std::logic_error("Unknown operator in expression: "+expr1->toString());
+}
+
+private:
+ /** The node type */
+ OperatorType kind;
+ /** The left child (if applicable) */
+ ptr left;
+ /** The right child (if applicable) */
+ ptr right;
+ /** The atom (if applicable) */
+ atom_ptr atom;
+
+ /**
+ * Returns true if outputing this node in infix syntax needs parentheses,
+ * if the operator above is of `enclosingType`
+ */
+ bool needsParentheses(OperatorType enclosingType) const {
+ switch (kind) {
+ case EXP_ATOM:
+ case EXP_TRUE:
+ case EXP_FALSE:
+ return false;
+ case EXP_AND:
+ if (enclosingType==EXP_NOT) return true;
+ if (enclosingType==EXP_AND) return false;
+ if (enclosingType==EXP_OR) return false;
+ break;
+ case EXP_OR:
+ if (enclosingType==EXP_NOT) return true;
+ if (enclosingType==EXP_AND) return true;
+ if (enclosingType==EXP_OR) return false;
+ break;
+ case EXP_NOT:
+ return false;
+ }
+ throw std::logic_error("Unhandled operator");
+ }
+
+};
+
+}
+
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer.hh
new file mode 100644
index 000000000..52800e351
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer.hh
@@ -0,0 +1,218 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_HOACONSUMER_H
+#define CPPHOAFPARSER_HOACONSUMER_H
+
+#include
+#include
+
+#include "cpphoafparser/ast/boolean_expression.hh"
+#include "cpphoafparser/ast/atom_label.hh"
+#include "cpphoafparser/ast/atom_acceptance.hh"
+#include "cpphoafparser/util/int_or_string.hh"
+
+#include "cpphoafparser/consumer/hoa_consumer_exception.hh"
+
+namespace cpphoafparser {
+
+/**
+ * Abstract class defining the interface for consuming parse events generated by HOAParser.
+ *
+ * The HOAConsumer abstract class is the basic means of interacting with the parser and
+ * the other infrastructure provided by cpphoafparser.
+ *
+ * Most of the functions in this class correspond to the various events that happen
+ * during parsing of a HOA input, e.g., marking the occurrence of the various header
+ * elements, the start of the automaton body, the states and edges, etc.
+ * In the documentation for each function, additional information is provided whether
+ * the corresponding element in a HOA input is considered optional or mandatory and
+ * whether it can occur once or multiple times. For error handling, a consumer is
+ * supposed to throw HOAConsumerException.
+ *
+ * Additionally, the consumer can indicate to the parser that aliases
+ * have to be resolved before invoking any of the event methods in the consumer.
+ *
+ * To chain HOAConsumers, see the HOAIntermediate interface.
+ */
+class HOAConsumer {
+public:
+ /** A shared_ptr wrapping a HOAConsumer */
+ typedef std::shared_ptr ptr;
+ /** A label expression */
+ typedef BooleanExpression label_expr;
+ /** An acceptance expression */
+ typedef BooleanExpression acceptance_expr;
+ /** A list of integers */
+ typedef std::vector int_list;
+
+ /** Destructor */
+ virtual ~HOAConsumer() {}
+
+ /**
+ * This function is called by the parser to query the consumer whether aliases should be
+ * resolved by the parser (return `true` or whether the consumer would like to
+ * see the aliases unresolved (return `false`). This function should always return
+ * a constant value.
+ **/
+ virtual bool parserResolvesAliases() = 0;
+
+ /** Called by the parser for the "HOA: version" item [mandatory, once]. */
+ virtual void notifyHeaderStart(const std::string& version) = 0;
+
+ /** Called by the parser for the "States: int(numberOfStates)" item [optional, once]. */
+ virtual void setNumberOfStates(unsigned int numberOfStates) = 0;
+
+ /**
+ * Called by the parser for each "Start: state-conj" item [optional, multiple].
+ * @param stateConjunction a list of state indizes, interpreted as a conjunction
+ **/
+ virtual void addStartStates(const int_list& stateConjunction) = 0;
+
+ /**
+ * Called by the parser for each "Alias: alias-def" item [optional, multiple].
+ * Will be called no matter the return value of `parserResolvesAliases()`.
+ *
+ * @param name the alias name (without @)
+ * @param labelExpr a boolean expression over labels
+ **/
+ virtual void addAlias(const std::string& name, label_expr::ptr labelExpr) = 0;
+
+ /**
+ * Called by the parser for the "AP: ap-def" item [optional, once].
+ * @param aps the list of atomic propositions
+ */
+ virtual void setAPs(const std::vector& aps) = 0;
+
+ /**
+ * Called by the parser for the "Acceptance: acceptance-def" item [mandatory, once].
+ * @param numberOfSets the number of acceptance sets used to tag state / transition acceptance
+ * @param accExpr a boolean expression over acceptance atoms
+ **/
+ virtual void setAcceptanceCondition(unsigned int numberOfSets, acceptance_expr::ptr accExpr) = 0;
+
+ /**
+ * Called by the parser for each "acc-name: ..." item [optional, multiple].
+ * @param name the provided name
+ * @param extraInfo the additional information for this item
+ * */
+ virtual void provideAcceptanceName(const std::string& name, const std::vector& extraInfo) = 0;
+
+ /**
+ * Called by the parser for the "name: ..." item [optional, once].
+ **/
+ virtual void setName(const std::string& name) = 0;
+
+ /**
+ * Called by the parser for the "tool: ..." item [optional, once].
+ * @param name the tool name
+ * @param version the tool version (option, empty pointer if not provided)
+ **/
+ virtual void setTool(const std::string& name, std::shared_ptr version) = 0;
+
+ /**
+ * Called by the parser for the "properties: ..." item [optional, multiple].
+ * @param properties a list of properties
+ */
+ virtual void addProperties(const std::vector& properties) = 0;
+
+ /**
+ * Called by the parser for each unknown header item [optional, multiple].
+ * @param name the name of the header (without ':')
+ * @param content a list of extra information provided by the header
+ */
+ virtual void addMiscHeader(const std::string& name, const std::vector& content) = 0;
+
+ /**
+ * Called by the parser to notify that the BODY of the automaton has started [mandatory, once].
+ */
+ virtual void notifyBodyStart() = 0;
+
+ /**
+ * Called by the parser for each "State: ..." item [multiple].
+ * @param id the identifier for this state
+ * @param info an optional string providing additional information about the state (empty pointer if not provided)
+ * @param labelExpr an optional boolean expression over labels (state-labeled) (empty pointer if not provided)
+ * @param accSignature an optional list of acceptance set indizes (state-labeled acceptance) (empty pointer if not provided)
+ */
+ virtual void addState(unsigned int id, std::shared_ptr info, label_expr::ptr labelExpr, std::shared_ptr accSignature) = 0;
+
+ /**
+ * Called by the parser for each implicit edge definition [multiple], i.e.,
+ * where the edge label is deduced from the index of the edge.
+ *
+ * If the edges are provided in implicit form, after every `addState()` there should be 2^|AP| calls to
+ * `addEdgeImplicit`. The corresponding boolean expression over labels / BitSet
+ * can be obtained by calling BooleanExpression.fromImplicit(i-1) for the i-th call of this function per state.
+ *
+ * @param stateId the index of the 'from' state
+ * @param conjSuccessors a list of successor state indizes, interpreted as a conjunction
+ * @param accSignature an optional list of acceptance set indizes (transition-labeled acceptance) (empty pointer if not provided)
+ */
+ virtual void addEdgeImplicit(unsigned int stateId, const int_list& conjSuccessors, std::shared_ptr accSignature) = 0;
+
+ /**
+ * Called by the parser for each explicit edge definition [optional, multiple], i.e.,
+ * where the label is either specified for the edge or as a state-label.
+ *
+ * @param stateId the index of the 'from' state
+ * @param labelExpr a boolean expression over labels (empty pointer if none provided, only in case of state-labeled states)
+ * @param conjSuccessors a list of successors state indizes, interpreted as a conjunction
+ * @param accSignature an optional list of acceptance set indizes (transition-labeled acceptance) (empty pointer if none provided)
+ */
+ virtual void addEdgeWithLabel(unsigned int stateId, label_expr::ptr labelExpr, const int_list& conjSuccessors, std::shared_ptr accSignature) = 0;
+
+ /**
+ * Called by the parser to notify the consumer that the definition for state `stateId`
+ * has ended [multiple].
+ */
+ virtual void notifyEndOfState(unsigned int stateId) = 0;
+
+ /**
+ * Called by the parser to notify the consumer that the automata definition has ended [mandatory, once].
+ */
+ virtual void notifyEnd() = 0;
+
+ /**
+ * Called by the parser to notify the consumer that an "ABORT" message has been encountered
+ * (at any time, indicating error, the automaton should be discarded).
+ */
+ virtual void notifyAbort() = 0;
+
+
+ /**
+ * Is called whenever a condition is encountered that merits a (non-fatal) warning.
+ * The consumer is free to handle this situation as it wishes.
+ */
+ virtual void notifyWarning(const std::string& warning) = 0;
+
+};
+
+}
+
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_exception.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_exception.hh
new file mode 100644
index 000000000..2fcc8bff0
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_exception.hh
@@ -0,0 +1,48 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_HOACONSUMEREXCEPTION_H
+#define CPPHOAFPARSER_HOACONSUMEREXCEPTION_H
+
+#include
+
+namespace cpphoafparser {
+
+/**
+ * An exception that allows a HOAConsumer or HOAIntermediate
+ * to signal that an error has occurred.
+ */
+class HOAConsumerException : public std::runtime_error {
+public:
+ /** Constructor */
+ HOAConsumerException(const std::string& what) : std::runtime_error(what) {}
+};
+
+}
+
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_null.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_null.hh
new file mode 100644
index 000000000..de9101c98
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_null.hh
@@ -0,0 +1,109 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_HOACONSUMERNULL_H
+#define CPPHOAFPARSER_HOACONSUMERNULL_H
+
+#include "cpphoafparser/consumer/hoa_consumer.hh"
+
+
+namespace cpphoafparser {
+
+/**
+ * A no-operation HOAConsumer.
+ * Provides no-op implementations for all the functions required by the
+ * HOAConsumer interface.
+ */
+class HOAConsumerNull : public HOAConsumer {
+public:
+
+ virtual bool parserResolvesAliases() override {
+ return false;
+ }
+
+ virtual void notifyHeaderStart(const std::string& version) override {
+ }
+
+ virtual void setNumberOfStates(unsigned int numberOfStates) override {
+ }
+
+ virtual void addStartStates(const int_list& stateConjunction) override {
+ }
+
+ virtual void addAlias(const std::string& name, label_expr::ptr labelExpr) override {
+ }
+
+ virtual void setAPs(const std::vector& aps) override {
+ }
+
+ virtual void setAcceptanceCondition(unsigned int numberOfSets, acceptance_expr::ptr accExpr) override {
+ }
+
+ virtual void provideAcceptanceName(const std::string& name, const std::vector& extraInfo) override {
+ }
+
+ virtual void setName(const std::string& name) override {
+ }
+
+ virtual void setTool(const std::string& name, std::shared_ptr version) override {
+ }
+
+ virtual void addProperties(const std::vector& properties) override {
+ }
+
+ virtual void addMiscHeader(const std::string& name, const std::vector& content) override {
+ }
+
+ virtual void notifyBodyStart() override {
+ }
+
+ virtual void addState(unsigned int id, std::shared_ptr info, label_expr::ptr labelExpr, std::shared_ptr accSignature) override {
+ }
+
+ virtual void addEdgeImplicit(unsigned int stateId, const int_list& conjSuccessors, std::shared_ptr accSignature) override {
+ }
+
+ virtual void addEdgeWithLabel(unsigned int stateId, label_expr::ptr labelExpr, const int_list& conjSuccessors, std::shared_ptr accSignature) override {
+ }
+
+ virtual void notifyEndOfState(unsigned int stateId) override {
+ }
+
+ virtual void notifyEnd() override {
+ }
+
+ virtual void notifyAbort() {
+ }
+
+ virtual void notifyWarning(const std::string& warning) {
+ }
+};
+
+}
+
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_print.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_print.hh
new file mode 100644
index 000000000..cf775c395
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_print.hh
@@ -0,0 +1,238 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_HOACONSUMERPRINT_H
+#define CPPHOAFPARSER_HOACONSUMERPRINT_H
+
+#include
+
+#include "cpphoafparser/consumer/hoa_consumer.hh"
+#include "cpphoafparser/parser/hoa_parser_helper.hh"
+
+namespace cpphoafparser {
+
+/**
+ * A HOAConsumer implementation that provides printing functionality.
+ *
+ * Outputs the HOA automaton corresponding to the function calls on the given output stream.
+ * Can be used as a "pretty-printer", as it will output the various syntax elements with
+ * a consistent layout of white-space and line breaks.
+ */
+
+class HOAConsumerPrint : public HOAConsumer {
+public:
+
+ /** Constructor, providing a reference to the output stream */
+ HOAConsumerPrint(std::ostream& out) : out(out) {}
+
+ virtual bool parserResolvesAliases() override {
+ return false;
+ }
+
+ virtual void notifyHeaderStart(const std::string& version) override {
+ out << "HOA: " << version << std::endl;
+ }
+
+ virtual void setNumberOfStates(unsigned int numberOfStates) override {
+ out << "States: " << numberOfStates << std::endl;
+ }
+
+ virtual void addStartStates(const int_list& stateConjunction) override {
+ out << "Start: ";
+ bool first = true;
+ for (unsigned int state : stateConjunction) {
+ if (!first) out << " & ";
+ first=false;
+ out << state;
+ }
+ out << std::endl;
+ }
+
+ virtual void addAlias(const std::string& name, label_expr::ptr labelExpr) override {
+ out << "Alias: @" << name << " " << *labelExpr << std::endl;
+ }
+
+ virtual void setAPs(const std::vector& aps) override {
+ out << "AP: " << aps.size();
+ for (const std::string& ap : aps) {
+ out << " ";
+ HOAParserHelper::print_quoted(out, ap);
+ }
+ out << std::endl;
+ }
+
+ virtual void setAcceptanceCondition(unsigned int numberOfSets, acceptance_expr::ptr accExpr) override {
+ out << "Acceptance: " << numberOfSets << " " << *accExpr << std::endl;
+ }
+
+ virtual void provideAcceptanceName(const std::string& name, const std::vector& extraInfo) override {
+ out << "acc-name: " << name;
+ for (const IntOrString& extra : extraInfo) {
+ out << " " << extra;
+ }
+ out << std::endl;
+ }
+
+ virtual void setName(const std::string& name) override {
+ out << "name: ";
+ HOAParserHelper::print_quoted(out, name);
+ out << std::endl;
+ }
+
+ virtual void setTool(const std::string& name, std::shared_ptr version) override {
+ out << "tool: ";
+ HOAParserHelper::print_quoted(out, name);
+ if (version) {
+ out << " ";
+ HOAParserHelper::print_quoted(out, *version);
+ }
+ out << std::endl;
+ }
+
+ virtual void addProperties(const std::vector& properties) override {
+ out << "properties:";
+ for (const std::string& property : properties) {
+ out << " " << property;
+ }
+ out << std::endl;
+ }
+
+ virtual void addMiscHeader(const std::string& name, const std::vector& content) override {
+ out << name << ":";
+ for (const IntOrString& extra : content) {
+ out << " " << extra;
+ }
+ out << std::endl;
+ }
+
+ virtual void notifyBodyStart() override {
+ out << "--BODY--" << std::endl;
+ }
+
+ virtual void addState(unsigned int id,
+ std::shared_ptr info,
+ label_expr::ptr labelExpr,
+ std::shared_ptr accSignature) override {
+ out << "State: ";
+ if (labelExpr) {
+ out << "[" << *labelExpr << "] ";
+ }
+ out << id;
+ if (info) {
+ out << " ";
+ HOAParserHelper::print_quoted(out, *info);
+ }
+ if (accSignature) {
+ out << " {";
+ bool first = true;
+ for (unsigned int acc : *accSignature) {
+ if (!first) out << " ";
+ first = false;
+ out << acc;
+ }
+ out << "}";
+ }
+ out << std::endl;
+ }
+
+ virtual void addEdgeImplicit(unsigned int stateId,
+ const int_list& conjSuccessors,
+ std::shared_ptr accSignature) override {
+ bool first = true;
+ for (unsigned int succ : conjSuccessors) {
+ if (!first) out << "&";
+ first = false;
+ out << succ;
+ }
+ if (accSignature) {
+ out << " {";
+ first = true;
+ for (unsigned int acc : *accSignature) {
+ if (!first) out << " ";
+ first = false;
+ out << acc;
+ }
+ out << "}";
+ }
+ out << std::endl;
+ }
+
+ virtual void addEdgeWithLabel(unsigned int stateId,
+ label_expr::ptr labelExpr,
+ const int_list& conjSuccessors,
+ std::shared_ptr accSignature) override {
+ if (labelExpr) {
+ out << "[" << *labelExpr << "] ";
+ }
+
+ bool first = true;
+ for (unsigned int succ : conjSuccessors) {
+ if (!first) out << "&";
+ first = false;
+ out << succ;
+ }
+
+ if (accSignature) {
+ out << " {";
+ first = true;
+ for (unsigned int acc : *accSignature) {
+ if (!first) out << " ";
+ first = false;
+ out << acc;
+ }
+ out << "}";
+ }
+ out << std::endl;
+ }
+
+ virtual void notifyEndOfState(unsigned int stateId) override {
+ // nothing to do
+ }
+
+ virtual void notifyEnd() override {
+ out << "--END--" << std::endl;
+ out.flush();
+ }
+
+ virtual void notifyAbort() override {
+ out << "--ABORT--" << std::endl;
+ out.flush();
+ }
+
+ virtual void notifyWarning(const std::string& warning) override {
+ std::cerr << "Warning: " << warning << std::endl;
+ }
+
+private:
+ /** Reference to the output stream */
+ std::ostream& out;
+};
+
+}
+
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate.hh
new file mode 100644
index 000000000..f0b2dd84a
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate.hh
@@ -0,0 +1,148 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_HOAINTERMEDIATE_H
+#define CPPHOAFPARSER_HOAINTERMEDIATE_H
+
+#include "cpphoafparser/consumer/hoa_consumer.hh"
+
+namespace cpphoafparser {
+
+/**
+ * The HOAIntermediate class provides a mechanism to chain
+ * multiple HOAConsumer together.
+ * Implementing the HOAConsumer interface, the default behavior
+ * is to simply propagate method calls to the `next` consumer.
+ *
+ * By overriding functions, this behavior can be customized, e.g.,
+ * validating constraints on the input (HOAIntermediateCheckValidity) or
+ * performing on-the-fly transformations (HOAIntermediateResolveAliases).
+ */
+
+class HOAIntermediate : public HOAConsumer {
+public:
+
+ /** Constructor, providing the `next` HOAConsumer */
+ HOAIntermediate(HOAConsumer::ptr next) : next(next) {}
+
+ virtual bool parserResolvesAliases() override {
+ return next->parserResolvesAliases();
+ }
+
+ virtual void notifyHeaderStart(const std::string& version) override {
+ next->notifyHeaderStart(version);
+ }
+
+ virtual void setNumberOfStates(unsigned int numberOfStates) override {
+ next->setNumberOfStates(numberOfStates);
+ }
+
+ virtual void addStartStates(const int_list& stateConjunction) override {
+ next->addStartStates(stateConjunction);
+ }
+
+ virtual void addAlias(const std::string& name, label_expr::ptr labelExpr) override {
+ next->addAlias(name, labelExpr);
+ }
+
+ virtual void setAPs(const std::vector& aps) override {
+ next->setAPs(aps);
+ }
+
+ virtual void setAcceptanceCondition(unsigned int numberOfSets, acceptance_expr::ptr accExpr) override {
+ next->setAcceptanceCondition(numberOfSets, accExpr);
+ }
+
+ virtual void provideAcceptanceName(const std::string& name, const std::vector& extraInfo) override {
+ next->provideAcceptanceName(name, extraInfo);
+ }
+
+ virtual void setName(const std::string& name) override {
+ next->setName(name);
+ }
+
+ virtual void setTool(const std::string& name, std::shared_ptr version) override {
+ next->setTool(name, version);
+ }
+
+ virtual void addProperties(const std::vector& properties) override {
+ next->addProperties(properties);
+ }
+
+ virtual void addMiscHeader(const std::string& name, const std::vector& content) override {
+ next->addMiscHeader(name, content);
+ }
+
+ virtual void notifyBodyStart() override {
+ next->notifyBodyStart();
+ }
+
+ virtual void addState(unsigned int id,
+ std::shared_ptr info,
+ label_expr::ptr labelExpr,
+ std::shared_ptr accSignature) override {
+ next->addState(id, info, labelExpr, accSignature);
+ }
+
+ virtual void addEdgeImplicit(unsigned int stateId,
+ const int_list& conjSuccessors,
+ std::shared_ptr accSignature) override {
+ next->addEdgeImplicit(stateId, conjSuccessors, accSignature);
+ }
+
+ virtual void addEdgeWithLabel(unsigned int stateId,
+ label_expr::ptr labelExpr,
+ const int_list& conjSuccessors,
+ std::shared_ptr accSignature) override {
+ next->addEdgeWithLabel(stateId, labelExpr, conjSuccessors, accSignature);
+ }
+
+ virtual void notifyEndOfState(unsigned int stateId) override {
+ next->notifyEndOfState(stateId);
+ }
+
+ virtual void notifyEnd() override {
+ next->notifyEnd();
+ }
+
+ virtual void notifyAbort() override {
+ next->notifyAbort();
+ }
+
+ virtual void notifyWarning(const std::string& warning) override {
+ next->notifyWarning(warning);
+ }
+
+protected:
+ /** The next consumer */
+ HOAConsumer::ptr next;
+};
+
+}
+
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_check_validity.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_check_validity.hh
new file mode 100644
index 000000000..554404c95
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_check_validity.hh
@@ -0,0 +1,828 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_HOAINTERMEDIATECHECKVALIDITY_H
+#define CPPHOAFPARSER_HOAINTERMEDIATECHECKVALIDITY_H
+
+#include "cpphoafparser/consumer/hoa_intermediate.hh"
+#include "cpphoafparser/util/dynamic_bitset.hh"
+#include "cpphoafparser/util/implicit_edge_helper.hh"
+#include "cpphoafparser/util/acceptance_repository_standard.hh"
+
+#include
+#include
+
+namespace cpphoafparser {
+
+// TODO Accurately reflect status in the doc!
+/**
+ * HOAIntermediate that checks that the parsed HOA automaton is well-formed.
+ *
+ * Among others, checks for
+ *
+ *
Conformance of stated properties with the automaton structure.
+ *
Conformance of Acceptance and acc-name headers.
+ *
Definedness of aliases.
+ *
Well-formedness of label expressions (only using atomic proposition indizes that are defined).
+ *
Well-formedness of acceptance (only using acceptance set indizes that are defined).
+ *
+ */
+class HOAIntermediateCheckValidity : public HOAIntermediate
+{
+public:
+
+ /** Constructor, providing the `next` HOAConsumer */
+ HOAIntermediateCheckValidity(HOAConsumer::ptr next)
+ : HOAIntermediate(next),
+ implicitEdgeHelper(0) {}
+
+ /**
+ * Add (semantically-relevant) headers not defined in the format specification that
+ * can be handled.
+ */
+ template
+ void setSupportedMiscHeaders(InputIterator first, InputIterator last) {
+ supportedMiscHeaders.insert(first, last);
+ }
+ /**
+ * Add (semantically-relevant) header not defined in the format specification that
+ * can be handled.
+ */
+ void addSupportedMiscHeader(const std::string& supportedMiscHeader) {
+ supportedMiscHeaders.insert(supportedMiscHeader);
+ }
+
+ virtual bool parserResolvesAliases() override {
+ return next->parserResolvesAliases();
+ }
+
+ virtual void notifyHeaderStart(const std::string& version) override {
+ if (version != "v1") {
+ throw HOAConsumerException("Can only parse HOA format v1");
+ }
+ next->notifyHeaderStart(version);
+ }
+
+ virtual void setNumberOfStates(unsigned int numberOfStates) override {
+ headerAtMostOnce("States");
+ this->numberOfStates.reset(new unsigned int(numberOfStates));
+ next->setNumberOfStates(numberOfStates);
+ }
+
+ virtual void addStartStates(const int_list& stateConjunction) override {
+ numberOfStartHeaders++;
+ if (stateConjunction.size()>1) {
+ hasUniversalBranching = true;
+ }
+
+ for (unsigned int state : stateConjunction) {
+ checkStateIndex(state);
+ startStates.set(state);
+ }
+ next->addStartStates(stateConjunction);
+ }
+
+ virtual void addAlias(const std::string& name, label_expr::ptr labelExpr) override {
+ usedHeaders.insert("Alias");
+
+ checkAliasesAreDefined(labelExpr);
+ aliases.insert(name);
+
+ gatherLabels(labelExpr, apsInAliases);
+
+ next->addAlias(name, labelExpr);
+ }
+
+ virtual void setAPs(const std::vector& aps) {
+ headerAtMostOnce("AP");
+
+ numberOfAPs.reset(new unsigned int(aps.size()));
+
+ std::unordered_set apSet;
+ for (const std::string& ap : aps) {
+ if (apSet.insert(ap).second == false) {
+ throw HOAConsumerException("Atomic proposition "+ap+" appears more than once in AP-header");
+ }
+ }
+
+ next->setAPs(aps);
+ }
+
+ virtual void setAcceptanceCondition(unsigned int numberOfSets, acceptance_expr::ptr accExpr) override {
+ headerAtMostOnce("Acceptance");
+ numberOfAcceptanceSets.reset(new unsigned int(numberOfSets));
+
+ checkAcceptanceCondition(accExpr);
+ acceptance = accExpr->deepCopy();
+
+ next->setAcceptanceCondition(numberOfSets, accExpr);
+ }
+
+ virtual void provideAcceptanceName(const std::string& name, const std::vector& extraInfo) override {
+ headerAtMostOnce("acc-name");
+ accName.reset(new std::string(name));
+
+ accExtraInfo = extraInfo;
+ next->provideAcceptanceName(name, extraInfo);
+ }
+
+
+ virtual void setName(const std::string& name) override {
+ headerAtMostOnce("name");
+ next->setName(name);
+ }
+
+ virtual void setTool(const std::string& name, std::shared_ptr version) override {
+ headerAtMostOnce("tool");
+ next->setTool(name, version);
+ }
+
+ virtual void addProperties(const std::vector& properties) {
+ usedHeaders.insert("properties");
+
+ for (const std::string& property : properties) {
+ if (property == "state_labels") {
+ property_state_labels = true;
+ } else if (property == "trans_labels") {
+ property_trans_labels = true;
+ } else if (property == "implicit_labels") {
+ property_implicit_labels = true;
+ } else if (property == "explicit_labels") {
+ property_explicit_labels = true;
+ } else if (property == "state_acc") {
+ property_state_acc = true;
+ } else if (property == "trans_acc") {
+ property_trans_acc = true;
+ } else if (property == "univ_branch") {
+ property_univ_branch = true;
+ } else if (property == "no_univ_branch") {
+ property_no_univ_branch = true;
+ } else if (property == "deterministic") {
+ property_deterministic = true;
+ } else if (property == "complete") {
+ property_complete = true;
+ } else if (property == "colored") {
+ property_colored = true;
+ } else {
+ // do nothing
+ }
+ }
+
+ next->addProperties(properties);
+ }
+
+ virtual void addMiscHeader(const std::string& name, const std::vector& content) override {
+ usedHeaders.insert(name);
+ if (name.at(0) >= 'A' && name.at(0) <= 'Z') {
+ // first character is upper case -> if we don't know what to do with this header,
+ // raise exception as this may change the semantics of the automaton
+ if (supportedMiscHeaders.find(name) != supportedMiscHeaders.end())
+ throw HOAConsumerException("Header "+name+" potentially has semantic relevance, but is not supported");
+ }
+ next->addMiscHeader(name, content);
+ }
+
+ virtual void notifyBodyStart() {
+ // check for existence of mandatory headers
+ headerIsMandatory("Acceptance");
+
+ // check that all AP indizes in aliases are valid
+ if (!numberOfAPs) {
+ // there was no AP-header, equivalent to AP: 0
+ numberOfAPs.reset(new unsigned int(0));
+ }
+ std::pair highestAPIndex = apsInAliases.getHighestSetBit();
+ if (highestAPIndex.second && highestAPIndex.first >= *numberOfAPs) {
+ throw HOAConsumerException("AP index "
+ + std::to_string(highestAPIndex.first)
+ + " in some alias definition is out of range (0 - "
+ + std::to_string(*numberOfAPs-1)
+ +")");
+ }
+
+ if (accName) {
+ checkAccName();
+ }
+
+ // check whether the start states violate properties
+ if (property_no_univ_branch && hasUniversalBranching) {
+ throw HOAConsumerException("Property 'no_univ_branching' is violated by the start states");
+ }
+ if (property_deterministic && numberOfStartHeaders != 1) {
+ throw HOAConsumerException("Property 'deterministic' is violated by having "+std::to_string(numberOfStartHeaders)+" Start-headers");
+ }
+
+ implicitEdgeHelper = ImplicitEdgeHelper(*numberOfAPs);
+
+ next->notifyBodyStart();
+ }
+
+ virtual void addState(unsigned int id, std::shared_ptr info, label_expr::ptr labelExpr, std::shared_ptr accSignature) override {
+ checkStateIndex(id);
+ if (statesWithDefinition.get(id)) {
+ throw HOAConsumerException("State "+std::to_string(id)+" is defined multiple times");
+ }
+ statesWithDefinition.set(id);
+ currentState = id;
+
+ if (accSignature) {
+ checkAcceptanceSignature(*accSignature, false);
+ currentStateIsColored = (accSignature->size() == 1);
+ } else {
+ currentStateIsColored = false;
+ }
+
+ if (property_colored && *numberOfAcceptanceSets>0 && !currentStateIsColored) {
+ if (property_state_acc) {
+ // we already know that the automaton is in violation...
+ throw HOAConsumerException("State "+std::to_string(id)+" is not colored");
+ }
+ }
+
+ if (labelExpr) {
+ checkLabelExpression(labelExpr);
+ }
+
+ // reset flags
+ currentStateHasStateLabel = (bool)labelExpr;
+ currentStateHasTransitionLabel = false;
+ currentStateHasImplicitEdge = false;
+ currentStateHasExplicitEdge = false;
+ currentStateHasStateAcceptance = (bool)accSignature;
+ currentStateHasTransitionAcceptance = false;
+
+ implicitEdgeHelper.startOfState(id);
+
+ next->addState(id, info, labelExpr, accSignature);
+ }
+
+ virtual void addEdgeImplicit(unsigned int stateId,
+ const int_list& conjSuccessors,
+ std::shared_ptr accSignature) override {
+ assert(stateId == currentState);
+
+ for (unsigned int succ : conjSuccessors) {
+ checkStateIndexTarget(succ);
+ }
+
+ if (conjSuccessors.size() > 1) {
+ hasUniversalBranching = true;
+ }
+
+ bool edgeIsColored = false;
+ if (accSignature) {
+ checkAcceptanceSignature(*accSignature, true);
+ edgeIsColored = (accSignature->size() == 1);
+ }
+
+ if (property_colored && *numberOfAcceptanceSets > 0) {
+ if (!currentStateIsColored && !edgeIsColored) {
+ throw HOAConsumerException("In state "+std::to_string(stateId)+", there is a transition that is not colored...");
+ } else if (currentStateIsColored && edgeIsColored) {
+ throw HOAConsumerException("In state "+std::to_string(stateId)+", there is a transition that is colored even though the state is colored already...");
+ }
+ }
+
+ if (currentStateHasExplicitEdge) {
+ throw HOAConsumerException("Can not mix explicit and implicit edge definitions (state "+std::to_string(stateId)+")");
+ }
+ currentStateHasImplicitEdge = true;
+
+ currentStateHasTransitionLabel = true;
+ if (currentStateHasStateLabel) {
+ throw new HOAConsumerException("Can not mix state labels and implicit edge definitions (state "+std::to_string(stateId)+")");
+ }
+
+ implicitEdgeHelper.nextImplicitEdge();
+ next->addEdgeImplicit(stateId, conjSuccessors, accSignature);
+ }
+
+ virtual void addEdgeWithLabel(unsigned int stateId,
+ label_expr::ptr labelExpr,
+ const int_list& conjSuccessors,
+ std::shared_ptr accSignature) override {
+ assert(stateId == currentState);
+
+ for (unsigned int succ : conjSuccessors) {
+ checkStateIndexTarget(succ);
+ }
+
+ if (conjSuccessors.size() > 1) {
+ hasUniversalBranching = true;
+ }
+
+ bool edgeIsColored = false;
+ if (accSignature) {
+ checkAcceptanceSignature(*accSignature, true);
+ edgeIsColored = (accSignature->size() == 1);
+ }
+
+ if (property_colored && *numberOfAcceptanceSets > 0) {
+ if (!currentStateIsColored && !edgeIsColored) {
+ throw HOAConsumerException("In state "+std::to_string(stateId)+", there is a transition that is not colored...");
+ } else if (currentStateIsColored && edgeIsColored) {
+ throw HOAConsumerException("In state "+std::to_string(stateId)+", there is a transition that is colored even though the state is colored already...");
+ }
+ }
+
+ if (labelExpr) {
+ checkLabelExpression(labelExpr);
+ }
+
+ if (labelExpr) {
+ currentStateHasTransitionLabel = true;
+ if (currentStateHasStateLabel) {
+ throw HOAConsumerException("Can not mix state and transition labeling (state "+std::to_string(stateId)+")");
+ }
+ }
+
+ if (currentStateHasImplicitEdge) {
+ throw HOAConsumerException("Can not mix explicit and implicit edge definitions (state "+std::to_string(stateId)+")");
+ }
+ currentStateHasExplicitEdge = true;
+
+ next->addEdgeWithLabel(stateId, labelExpr, conjSuccessors, accSignature);
+ }
+
+ virtual void notifyEndOfState(unsigned int stateId) override {
+ implicitEdgeHelper.endOfState();
+
+ // check for property violations
+ if (property_state_labels && currentStateHasTransitionLabel) {
+ throw HOAConsumerException("Property 'state-labels' is violated by having transition labels in state "+std::to_string(stateId));
+ }
+ if (property_trans_labels && currentStateHasStateLabel) {
+ throw HOAConsumerException("Property 'trans-labels' is violated by having a state label in state "+std::to_string(stateId));
+
+ }
+ if (property_implicit_labels && currentStateHasExplicitEdge) {
+ throw HOAConsumerException("Property 'implicit-label' is violated by having a label expression on a transition in state "+std::to_string(stateId));
+ }
+ if (property_explicit_labels && currentStateHasImplicitEdge) {
+ throw HOAConsumerException("Property 'explicit-label' is violated by having implicit transition(s) in state "+std::to_string(stateId));
+ }
+ if (property_state_acc && currentStateHasTransitionAcceptance) {
+ throw HOAConsumerException("Property 'state-acc' is violated by having transition acceptance in state "+std::to_string(stateId));
+ }
+ if (property_trans_acc && currentStateHasStateAcceptance) {
+ throw HOAConsumerException("Property 'trans-acc' is violated by having state acceptance in state "+std::to_string(stateId));
+ }
+ if (property_no_univ_branch && hasUniversalBranching) {
+ throw HOAConsumerException("Property 'no-univ-branch' is violated by having universal branching in state "+std::to_string(stateId));
+ }
+
+ // TODO: deterministic
+ // for implicit edges, this is done via the ImplicitEdgeHelper
+ // for explicit edges, check would need to keep track of overlapping label expressions
+
+ // TODO: complete
+ // for implicit edges, this is done via the ImplicitEdgeHelper
+ // for explicit edges, check would need to keep track of overlapping label expressions
+
+ next->notifyEndOfState(stateId);
+ }
+
+ virtual void notifyEnd() override {
+ // check sanity of state definitions and target states
+ checkStates();
+
+ if (property_univ_branch && !hasUniversalBranching) {
+ throw HOAConsumerException("Property 'univ-branch' is violated by not having universal branching in the automaton");
+ }
+
+ next->notifyEnd();
+ }
+
+ virtual void notifyAbort() {
+ next->notifyAbort();
+ }
+
+protected:
+
+ // ----------------------------------------------------------------------------
+
+ /** Send a warning */
+ void doWarning(const std::string& warning)
+ {
+ next->notifyWarning(warning);
+ }
+
+ // ----------------------------------------------------------------------------
+
+ /** Check that a mandatory header has been seen */
+ void headerIsMandatory(const std::string& name)
+ {
+ if (usedHeaders.find(name) == usedHeaders.end()) {
+ throw HOAConsumerException("Mandatory header "+name+" is missing");
+ }
+ }
+
+ /** Check that a 'once' header has not been seen multiple times */
+ void headerAtMostOnce(const std::string& headerName)
+ {
+ if (usedHeaders.insert(headerName).second == false) {
+ throw HOAConsumerException("Header "+headerName+" occurs multiple times, but is allowed only once.");
+ }
+ }
+
+ /** Check that a states index is in range */
+ void checkStateIndex(unsigned int index)
+ {
+ if (numberOfStates) {
+ if (index >= *numberOfStates) {
+ throw HOAConsumerException("State index "
+ + std::to_string(index)
+ + " is out of range (0 - "
+ + std::to_string(*numberOfStates-1)
+ + ")");
+ }
+ }
+ }
+
+ /** Checks that the target state index of a transition is valid */
+ void checkStateIndexTarget(unsigned int index)
+ {
+ if (numberOfStates) {
+ if (index >= *numberOfStates) {
+ throw HOAConsumerException("State index "
+ + std::to_string(index)
+ + " is out of range (0 - "
+ + std::to_string(*numberOfStates-1)
+ + ")");
+ }
+ }
+ targetStatesOfTransitions.set(index);
+ }
+
+ /** Check that the states have been properly defined */
+ void checkStates()
+ {
+ bool haveComplainedAboutMissingStates = false;
+
+ // if numberOfStates is set, check that all states are in range
+ if (numberOfStates) {
+ // the states with a definition
+ std::pair highestStateIndex = statesWithDefinition.getHighestSetBit();
+ if (highestStateIndex.second && highestStateIndex.first >= *numberOfStates) {
+ throw HOAConsumerException("State index "
+ + std::to_string(highestStateIndex.first)
+ + " is out of range (0 - "
+ + std::to_string(*numberOfStates-1)
+ + ")");
+ }
+
+ // the states occurring as targets
+ highestStateIndex = targetStatesOfTransitions.getHighestSetBit();
+ if (highestStateIndex.second && highestStateIndex.first >= *numberOfStates) {
+ throw HOAConsumerException("State index "
+ + std::to_string(highestStateIndex.first)
+ + " (target in a transition) is out of range (0 - "
+ + std::to_string(*numberOfStates-1)
+ +")");
+ }
+
+ // the start states
+ highestStateIndex = startStates.getHighestSetBit();
+ if (highestStateIndex.second && highestStateIndex.first >= *numberOfStates) {
+ throw HOAConsumerException("State index "
+ + std::to_string(highestStateIndex.first)
+ + " (start state) is out of range (0 - "
+ + std::to_string(*numberOfStates-1)
+ +")");
+ }
+
+ if (statesWithDefinition.cardinality() != *numberOfStates) {
+ std::size_t missing = *numberOfStates - statesWithDefinition.cardinality();
+ doWarning("There are "+std::to_string(missing)+" states without definition");
+ haveComplainedAboutMissingStates = true;
+ }
+ }
+
+ dynamic_bitset targetsButNoDefinition(targetStatesOfTransitions);
+ targetsButNoDefinition.andNot(statesWithDefinition);
+ if (!targetsButNoDefinition.isEmpty() && !haveComplainedAboutMissingStates) {
+ doWarning("There are "
+ + std::to_string(targetsButNoDefinition.cardinality())
+ + " states that are targets of transitions but that have no definition");
+ haveComplainedAboutMissingStates = true;
+ }
+
+ dynamic_bitset startStatesButNoDefinition(startStates);
+ startStatesButNoDefinition.andNot(statesWithDefinition);
+ if (!startStatesButNoDefinition.isEmpty() && !haveComplainedAboutMissingStates) {
+ doWarning("There are "
+ + std::to_string(startStatesButNoDefinition.cardinality())
+ + " states that are start states but that have no definition");
+ haveComplainedAboutMissingStates = true;
+ }
+
+
+ if (haveComplainedAboutMissingStates && property_colored && *numberOfAcceptanceSets > 0) {
+ // states without definition are not colored
+ throw HOAConsumerException("An automaton with property 'colored' can not have states missing a definition");
+ }
+ }
+
+ /**
+ * Check that the acceptance condition is well-formed.
+ * In particular, that no boolean negation occurs and
+ * that the referenced acceptance sets are defined.
+ */
+ void checkAcceptanceCondition(acceptance_expr::ptr accExpr)
+ {
+ assert (numberOfAcceptanceSets);
+
+ switch (accExpr->getType()) {
+ case acceptance_expr::EXP_TRUE:
+ case acceptance_expr::EXP_FALSE:
+ return;
+ case acceptance_expr::EXP_AND:
+ case acceptance_expr::EXP_OR:
+ checkAcceptanceCondition(accExpr->getLeft());
+ checkAcceptanceCondition(accExpr->getRight());
+ return;
+ case acceptance_expr::EXP_NOT:
+ throw HOAConsumerException("Acceptance condition contains boolean negation, not allowed");
+ case acceptance_expr::EXP_ATOM:
+ unsigned int acceptanceSet = accExpr->getAtom().getAcceptanceSet();
+ if (acceptanceSet >= *numberOfAcceptanceSets) {
+ throw HOAConsumerException("Acceptance condition contains acceptance set with index "
+ + std::to_string(acceptanceSet)
+ + ", valid range is 0 - "
+ + std::to_string(*numberOfAcceptanceSets-1));
+ }
+ return;
+ }
+ throw std::logic_error("Unknown operator in acceptance condition: "+accExpr->toString());
+ }
+
+ /**
+ * Check that an acceptance signature is well-formed.
+ * In particular, that the referenced acceptance sets are defined.
+ */
+ void checkAcceptanceSignature(const int_list& accSignature, bool inTransition)
+ {
+ for (unsigned int acceptanceSet : accSignature) {
+ if (acceptanceSet >= *numberOfAcceptanceSets) {
+ throw HOAConsumerException("Acceptance signature "
+ + (inTransition ? std::string("(in transition) ") : std::string(""))
+ + "for state index "
+ + std::to_string(currentState)
+ + " contains acceptance set with index "
+ + std::to_string(acceptanceSet)
+ + ", valid range is 0 - "
+ + std::to_string(*numberOfAcceptanceSets-1));
+ }
+ }
+ }
+
+ /**
+ * Check that all alias references in a label expression are
+ * properly defined
+ */
+ void checkAliasesAreDefined(label_expr::ptr expr)
+ {
+ switch (expr->getType()) {
+ case label_expr::EXP_TRUE:
+ case label_expr::EXP_FALSE:
+ return;
+ case label_expr::EXP_AND:
+ case label_expr::EXP_OR:
+ checkAliasesAreDefined(expr->getLeft());
+ checkAliasesAreDefined(expr->getRight());
+ return;
+ case label_expr::EXP_NOT:
+ checkAliasesAreDefined(expr->getLeft());
+ return;
+ case label_expr::EXP_ATOM:
+ if (expr->getAtom().isAlias()) {
+ if (aliases.find(expr->getAtom().getAliasName()) != aliases.end()) {
+ throw HOAConsumerException("Alias @"+expr->getAtom().getAliasName()+" is not defined");
+ }
+ }
+ return;
+ }
+ throw std::logic_error("Unknown operator in label expression: "+expr->toString());
+ }
+
+ /**
+ * Traverse the expression and, for every label encountered, set the corresponding bit in the
+ * `result` bitset.
+ * @param expr the expression
+ * @param[out] result a bitset where the additional bits corresponding to APs are set
+ */
+ void gatherLabels(label_expr::ptr expr, dynamic_bitset& result) {
+ switch (expr->getType()) {
+ case label_expr::EXP_TRUE:
+ case label_expr::EXP_FALSE:
+ return;
+ case label_expr::EXP_AND:
+ case label_expr::EXP_OR:
+ gatherLabels(expr->getLeft(), result);
+ gatherLabels(expr->getRight(), result);
+ return;
+ case label_expr::EXP_NOT:
+ gatherLabels(expr->getLeft(), result);
+ return;
+ case label_expr::EXP_ATOM:
+ if (!expr->getAtom().isAlias()) {
+ result.set(expr->getAtom().getAPIndex());
+ }
+ return;
+ }
+ throw std::logic_error("Unknown operator in label expression: "+expr->toString());
+ }
+
+ /** Check a label expression for well-formedness */
+ void checkLabelExpression(label_expr::ptr expr)
+ {
+ switch (expr->getType()) {
+ case label_expr::EXP_TRUE:
+ case label_expr::EXP_FALSE:
+ return;
+ case label_expr::EXP_AND:
+ case label_expr::EXP_OR:
+ checkLabelExpression(expr->getLeft());
+ checkLabelExpression(expr->getRight());
+ return;
+ case label_expr::EXP_NOT:
+ checkLabelExpression(expr->getLeft());
+ return;
+ case label_expr::EXP_ATOM:
+ if (expr->getAtom().isAlias()) {
+ if (aliases.find(expr->getAtom().getAliasName()) == aliases.end()) {
+ throw HOAConsumerException("Alias @"+expr->getAtom().getAliasName()+" is not defined");
+ }
+ } else {
+ assert(numberOfAPs);
+ unsigned int apIndex = expr->getAtom().getAPIndex();
+ if (apIndex >= *numberOfAPs) {
+ if (*numberOfAPs == 0) {
+ throw HOAConsumerException("AP index "+std::to_string(apIndex)+" in expression is out of range (no APs): "+expr->toString());
+ } else {
+ throw HOAConsumerException("AP index "
+ + std::to_string(apIndex)
+ + " in expression is out of range (from 0 to "
+ + std::to_string(*numberOfAPs-1)
+ + "): "
+ + expr->toString());
+ }
+ }
+ }
+ return;
+ }
+ throw std::logic_error("Unknown operator in label expression: "+expr->toString());
+ }
+
+ // ----------------------------------------------------------------------------
+
+ /**
+ * Check that the canonical expression for an acc-name (if known) matches that
+ * given by the Acceptance header.
+ */
+ void checkAccName(){
+ AcceptanceRepository::ptr repository(new AcceptanceRepositoryStandard());
+
+
+ acceptance_expr::ptr canonical;
+ try {
+ canonical = repository->getCanonicalAcceptanceExpression(*accName, accExtraInfo);
+ if (!(bool)canonical) {
+ // acceptance name is not known
+ return;
+ }
+ } catch (AcceptanceRepository::IllegalArgumentException& e) {
+ throw HOAConsumerException(e.what());
+ }
+
+ assert((bool)acceptance);
+
+ //std::cerr << "Canonical: " << *canonical << std::endl;
+ //std::cerr << "Acceptance: " << *acceptance << std::endl;
+
+ if (!acceptance_expr::areSyntacticallyEqual(acceptance, canonical)) {
+ throw HOAConsumerException(std::string("The acceptance given by the Acceptance and by the acc-name headers do not match syntactically:")
+ + "\nFrom Acceptance-header: "+acceptance->toString()
+ + "\nCanonical expression for acc-name-header: "+canonical->toString());
+ }
+}
+
+// ----------------- member variables
+
+protected:
+ /** A set of headers that are supported beyond the standard headers of the format */
+ std::unordered_set supportedMiscHeaders;
+
+ /** The header names that have occurred so far in the automaton definition */
+ std::unordered_set usedHeaders;
+
+ /** The number of states that have been specified in the header (optional) */
+ std::shared_ptr numberOfStates;
+
+ /** The number of acceptance sets (mandatory) */
+ std::shared_ptr numberOfAcceptanceSets;
+
+ /** The set of states for which addState has been called */
+ dynamic_bitset statesWithDefinition;
+
+ /** The set of states that occur as target states of some transition */
+ dynamic_bitset targetStatesOfTransitions;
+
+ /** The set of states that are start states */
+ dynamic_bitset startStates;
+
+ /** The set of alias names that have been defined (Alias-header) */
+ std::unordered_set aliases;
+ /** Atomic propositions that are referenced in some alias definition */
+ dynamic_bitset apsInAliases;
+
+ /** The number of atomic propositions */
+ std::shared_ptr numberOfAPs;
+
+ /** The acc-name (optional) */
+ std::shared_ptr accName;
+ /** extraInfo parameters for acc-name */
+ std::vector accExtraInfo;
+
+ /** The acceptance condition */
+ acceptance_expr::ptr acceptance;
+
+ /** The current state */
+ std::size_t currentState = 0;
+ /** Does the current state have a state label? */
+ bool currentStateHasStateLabel = false;
+ /** Does the current state have transitions with transition label? */
+ bool currentStateHasTransitionLabel = false;
+ /** Does the current state have implicit edges? */
+ bool currentStateHasImplicitEdge = false;
+ /** Does the current state have edges with explicit labels? */
+ bool currentStateHasExplicitEdge = false;
+ /** Does the current state have state acceptance? */
+ bool currentStateHasStateAcceptance = false;
+ /** Does the current state have transition acceptance? */
+ bool currentStateHasTransitionAcceptance = false;
+ /** Is the current state colored ? */
+ bool currentStateIsColored = false;
+
+
+ /** The implicit edge helper */
+ ImplicitEdgeHelper implicitEdgeHelper;
+
+ // properties: set to true if the given property is asserted by the HOA automaton
+ /** hints that the automaton uses only state labels */
+ bool property_state_labels = false;
+ /** hints that the automaton uses only transition labels */
+ bool property_trans_labels = false;
+ /** hints that the automaton uses only implicit transitions labels */
+ bool property_implicit_labels = false;
+ /** hints that the automaton uses only explicit transitions labels */
+ bool property_explicit_labels = false;
+ /** hints that the automaton uses only state-based acceptance specifications */
+ bool property_state_acc = false;
+ /** hints that the automaton uses only transition-based acceptance specifications */
+ bool property_trans_acc = false;
+ /** hints that the automaton uses universal branching for at least one transition or for the initial state */
+ bool property_univ_branch = false;
+ /** hints that the automaton does not use universal branching */
+ bool property_no_univ_branch = false;
+ /** hints that the automaton is deterministic, i.e., it has at most one initial state, and the outgoing transitions of each state have disjoint labels (note that this also applies in the presence of universal branching) */
+ bool property_deterministic = false;
+ /** hints that the automaton is complete, i.e., it has at least one state, and the transition function is total */
+ bool property_complete = false;
+ /** hints that each transition (or each state, for state-based acceptance) of the automaton belongs to exactly one acceptance set; this is typically the case in parity automata */
+ bool property_colored = false;
+
+ /** The number of Start-definitions (more than 1 = non-deterministic start states) */
+ int numberOfStartHeaders = 0;
+ /** Has this automaton universal branching? */
+ bool hasUniversalBranching = false;
+};
+
+}
+
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_resolve_aliases.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_resolve_aliases.hh
new file mode 100644
index 000000000..ff53e0364
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_resolve_aliases.hh
@@ -0,0 +1,185 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_HOAINTERMEDIATERESOLVEALIASES_H
+#define CPPHOAFPARSER_HOAINTERMEDIATERESOLVEALIASES_H
+
+#include
+
+#include "cpphoafparser/consumer/hoa_intermediate.hh"
+
+namespace cpphoafparser {
+
+/**
+ * A HOAIntermediate that resolves aliases on-the-fly.
+ *
+ * Stores the definition of aliases from the header and resolves
+ * any aliases in label expressions before passing the events to
+ * the next consumer.
+ */
+class HOAIntermediateResolveAliases : public HOAIntermediate
+{
+public:
+ /** Constructor, providing the `next` HOAConsumer */
+ HOAIntermediateResolveAliases(HOAConsumer::ptr next) : HOAIntermediate(next) {}
+
+ /** Store alias definition */
+ virtual void addAlias(const std::string& name, label_expr::ptr labelExpr) override {
+ if (aliases.find(name) != aliases.end()) {
+ throw new HOAConsumerException("Alias "+name+" is defined multiple times!");
+ }
+
+ if (containsAliases(labelExpr)) {
+ // check that all the aliases in the expression are already defined
+ checkAliasDefinedness(labelExpr);
+
+ // resolve aliases in the expression
+ labelExpr = resolveAliases(labelExpr);
+ }
+
+ aliases[name]=labelExpr;
+ }
+
+ /** Resolve alias references in state label, pass on to next HOAConsumer */
+ virtual void addState(unsigned int id,
+ std::shared_ptr info,
+ label_expr::ptr labelExpr,
+ std::shared_ptr accSignature) override {
+ if (labelExpr && containsAliases(labelExpr)) {
+ labelExpr = resolveAliases(labelExpr);
+ }
+ next->addState(id, info, labelExpr, accSignature);
+ }
+
+ /** Resolve alias references in edge label, pass on to next HOAConsumer */
+ virtual void addEdgeWithLabel(unsigned int stateId,
+ label_expr::ptr labelExpr,
+ const int_list& conjSuccessors,
+ std::shared_ptr accSignature) override {
+ if (labelExpr && containsAliases(labelExpr)) {
+ labelExpr = resolveAliases(labelExpr);
+ }
+
+ next->addEdgeWithLabel(stateId, labelExpr, conjSuccessors, accSignature);
+ }
+
+private:
+ /** Map for mapping alias names to alias definitions */
+ std::unordered_map aliases;
+
+ /** Returns `true` if the label expression contains an alias reference */
+ bool containsAliases(label_expr::ptr labelExpr) {
+ switch (labelExpr->getType()) {
+ case label_expr::EXP_FALSE:
+ case label_expr::EXP_TRUE:
+ return false;
+ case label_expr::EXP_AND:
+ case label_expr::EXP_OR:
+ if (containsAliases(labelExpr->getLeft())) return true;
+ if (containsAliases(labelExpr->getRight())) return true;
+ return false;
+ case label_expr::EXP_NOT:
+ if (containsAliases(labelExpr->getLeft())) return true;
+ return false;
+ case label_expr::EXP_ATOM:
+ return labelExpr->getAtom().isAlias();
+ }
+ throw HOAConsumerException("Unhandled boolean expression type");
+ }
+
+ /**
+ * Checks that all alias references occuring in the label expression are defined.
+ * If that is not the case, a HOAConsumerExeption is thrown.
+ */
+ void checkAliasDefinedness(label_expr::ptr labelExpr) {
+ switch (labelExpr->getType()) {
+ case label_expr::EXP_FALSE:
+ case label_expr::EXP_TRUE:
+ return;
+ case label_expr::EXP_AND:
+ case label_expr::EXP_OR:
+ checkAliasDefinedness(labelExpr->getLeft());
+ checkAliasDefinedness(labelExpr->getRight());
+ return;
+ case label_expr::EXP_NOT:
+ checkAliasDefinedness(labelExpr->getLeft());
+ return;
+ case label_expr::EXP_ATOM:
+ if (labelExpr->getAtom().isAlias()) {
+ const std::string& aliasName = labelExpr->getAtom().getAliasName();
+ if (aliases.find(aliasName) == aliases.end()) {
+ throw HOAConsumerException("Expression "+labelExpr->toString()+" uses undefined alias @"+aliasName);
+ }
+ }
+ return;
+ }
+ throw HOAConsumerException("Unhandled boolean expression type");
+
+ }
+
+ /**
+ * Returns a label expression, with all alias references resolved.
+ */
+ label_expr::ptr resolveAliases(label_expr::ptr labelExpr) {
+ switch (labelExpr->getType()) {
+ case label_expr::EXP_TRUE:
+ case label_expr::EXP_FALSE:
+ return labelExpr;
+ case label_expr::EXP_AND:
+ case label_expr::EXP_OR:
+ return label_expr::ptr(new label_expr(labelExpr->getType(),
+ resolveAliases(labelExpr->getLeft()),
+ resolveAliases(labelExpr->getRight())));
+ case label_expr::EXP_NOT:
+ return label_expr::ptr(new label_expr(labelExpr->getType(),
+ resolveAliases(labelExpr->getLeft()),
+ nullptr));
+ case label_expr::EXP_ATOM:
+ if (!labelExpr->getAtom().isAlias()) {
+ return labelExpr;
+ } else {
+ auto it = aliases.find(labelExpr->getAtom().getAliasName());
+ if (it == aliases.end()) {
+ throw HOAConsumerException("Can not resolve alias @"+labelExpr->getAtom().getAliasName());
+ }
+
+ label_expr::ptr resolved = it->second;
+ if (containsAliases(resolved)) {
+ resolved = resolveAliases(resolved);
+ }
+
+ return resolved;
+ }
+ }
+ throw HOAConsumerException("Unhandled boolean expression type");
+ }
+
+};
+
+}
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_trace.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_trace.hh
new file mode 100644
index 000000000..a235c4502
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_trace.hh
@@ -0,0 +1,255 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_HOAINTERMEDIATE_TRACE_H
+#define CPPHOAFPARSER_HOAINTERMEDIATE_TRACE_H
+
+#include
+
+#include "cpphoafparser/consumer/hoa_intermediate.hh"
+
+namespace cpphoafparser {
+
+/**
+ * Traces the function calls to HOAConsumer, prints function name and arguments to stream.
+ */
+class HOAIntermediateTrace : public HOAIntermediate {
+public:
+
+ /** Constructor, providing the `next` HOAConsumer */
+ HOAIntermediateTrace(HOAConsumer::ptr next) : HOAIntermediate(next), out(std::cout) {}
+
+ /** Constructor, providing the `next` HOAConsumer */
+ HOAIntermediateTrace(HOAConsumer::ptr next, std::ostream& out) : HOAIntermediate(next), out(out) {}
+
+ virtual bool parserResolvesAliases() override {
+ return next->parserResolvesAliases();
+ }
+
+ virtual void notifyHeaderStart(const std::string& version) override {
+ traceFunction("notifyHeaderStart");
+ traceArgument("version", version);
+
+ next->notifyHeaderStart(version);
+ }
+
+ virtual void setNumberOfStates(unsigned int numberOfStates) override {
+ traceFunction("setNumberOfStates");
+ traceArgument("numberOfStates", numberOfStates);
+
+ next->setNumberOfStates(numberOfStates);
+ }
+
+ virtual void addStartStates(const int_list& stateConjunction) override {
+ traceFunction("addStartStates");
+ traceArgument("stateConjunction", stateConjunction);
+
+ next->addStartStates(stateConjunction);
+ }
+
+ virtual void addAlias(const std::string& name, label_expr::ptr labelExpr) override {
+ traceFunction("addAlias");
+ traceArgument("labelExpr", labelExpr);
+
+ next->addAlias(name, labelExpr);
+ }
+
+ virtual void setAPs(const std::vector& aps) override {
+ traceFunction("setAPs");
+ traceArgument("aps", aps);
+
+ next->setAPs(aps);
+ }
+
+ virtual void setAcceptanceCondition(unsigned int numberOfSets, acceptance_expr::ptr accExpr) override {
+ traceFunction("setAcceptanceCondition");
+ traceArgument("numberOfSets", numberOfSets);
+ traceArgument("accExpr", accExpr);
+
+ next->setAcceptanceCondition(numberOfSets, accExpr);
+ }
+
+ virtual void provideAcceptanceName(const std::string& name, const std::vector& extraInfo) override {
+ traceFunction("setAcceptanceCondition");
+ traceArgument("name", name);
+ traceArgument("extraInfo", extraInfo);
+
+ next->provideAcceptanceName(name, extraInfo);
+ }
+
+ virtual void setName(const std::string& name) override {
+ traceFunction("setName");
+ traceArgument("name", name);
+
+ next->setName(name);
+ }
+
+ virtual void setTool(const std::string& name, std::shared_ptr version) override {
+ traceFunction("setTool");
+ traceArgument("name", name);
+ traceArgument("version", version);
+
+ next->setTool(name, version);
+ }
+
+ virtual void addProperties(const std::vector& properties) override {
+ traceFunction("addProperties");
+ traceArgument("properties", properties);
+
+ next->addProperties(properties);
+ }
+
+ virtual void addMiscHeader(const std::string& name, const std::vector& content) override {
+ traceFunction("addMiscHeader");
+ traceArgument("content", content);
+
+ next->addMiscHeader(name, content);
+ }
+
+ virtual void notifyBodyStart() override {
+ traceFunction("notifyBodyStart");
+
+ next->notifyBodyStart();
+ }
+
+ virtual void addState(unsigned int id,
+ std::shared_ptr info,
+ label_expr::ptr labelExpr,
+ std::shared_ptr accSignature) override {
+ traceFunction("addState");
+ traceArgument("id", id);
+ traceArgument("info", info);
+ traceArgument("labelExpr", labelExpr);
+ traceArgument("accSignature", accSignature);
+
+ next->addState(id, info, labelExpr, accSignature);
+ }
+
+ virtual void addEdgeImplicit(unsigned int stateId,
+ const int_list& conjSuccessors,
+ std::shared_ptr accSignature) override {
+ traceFunction("addEdgeImplicit");
+ traceArgument("stateId", stateId);
+ traceArgument("conjSuccessors", conjSuccessors);
+ traceArgument("accSignature", accSignature);
+
+ next->addEdgeImplicit(stateId, conjSuccessors, accSignature);
+ }
+
+ virtual void addEdgeWithLabel(unsigned int stateId,
+ label_expr::ptr labelExpr,
+ const int_list& conjSuccessors,
+ std::shared_ptr accSignature) override {
+ traceFunction("addEdgeWithLabel");
+ traceArgument("stateId", stateId);
+ traceArgument("labelExpr", labelExpr);
+ traceArgument("conjSuccessors", conjSuccessors);
+ traceArgument("accSignature", accSignature);
+
+ next->addEdgeWithLabel(stateId, labelExpr, conjSuccessors, accSignature);
+ }
+
+ virtual void notifyEndOfState(unsigned int stateId) override {
+ traceFunction("notifyEndOfState");
+ traceArgument("stateId", stateId);
+
+ next->notifyEndOfState(stateId);
+ }
+
+ virtual void notifyEnd() override {
+ traceFunction("notifyEnd");
+
+ next->notifyEnd();
+ }
+
+ virtual void notifyAbort() override {
+ traceFunction("notifyAbort");
+
+ next->notifyAbort();
+ }
+
+ virtual void notifyWarning(const std::string& warning) override {
+ traceFunction("notifyWarning");
+ traceArgument("warning", warning);
+
+ next->notifyWarning(warning);
+ }
+
+protected:
+ /** The output stream */
+ std::ostream& out;
+
+ /** Trace function call */
+ void traceFunction(const std::string& function) {
+ out << "=> " << function << std::endl;
+ }
+
+ /** Trace argument (string) */
+ void traceArgument(const std::string& name, const std::string& value) {
+ out << " " << name << " = " << value << std::endl;
+ }
+
+ /** Trace argument (int) */
+ void traceArgument(const std::string& name, unsigned int value) {
+ out << " " << name << " = " << value << std::endl;
+ }
+
+ /** Trace argument (BooleanExpression) */
+ template
+ void traceArgument(const std::string& name, const BooleanExpression& expr) {
+ out << " " << name << " = " << expr << std::endl;
+ }
+
+ /** Trace argument (vector) */
+ template
+ void traceArgument(const std::string& name, const std::vector& list) {
+ out << " " << name << " = ";
+ out << "[";
+ bool first= true;
+ for (const T& element : list) {
+ if (!first) out << ","; else first = false;
+ out << element;
+ }
+ out << "]" << std::endl;
+ }
+
+ /** Trace argument (shared_ptr) */
+ template
+ void traceArgument(const std::string& name, typename std::shared_ptr o) {
+ if ((bool)o) {
+ traceArgument(name, *o);
+ } else {
+ traceArgument(name, "null");
+ }
+ }
+
+};
+
+}
+
+#endif
diff --git a/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_lexer.hh b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_lexer.hh
new file mode 100644
index 000000000..25a2893bd
--- /dev/null
+++ b/resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_lexer.hh
@@ -0,0 +1,534 @@
+//==============================================================================
+//
+// Copyright (c) 2015-
+// Authors:
+// * Joachim Klein
+// * David Mueller
+//
+//------------------------------------------------------------------------------
+//
+// This file is part of the cpphoafparser library,
+// http://automata.tools/hoa/cpphoafparser/
+//
+// The cpphoafparser library is free software; you can redistribute it and/or
+// modify it under the terms of the GNU Lesser General Public
+// License as published by the Free Software Foundation; either
+// version 2.1 of the License, or (at your option) any later version.
+//
+// The cpphoafparser library is distributed in the hope that it will be useful,
+// but WITHOUT ANY WARRANTY; without even the implied warranty of
+// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
+// Lesser General Public License for more details.
+//
+// You should have received a copy of the GNU Lesser General Public
+// License along with this library; if not, write to the Free Software
+// Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA
+//
+//==============================================================================
+
+#ifndef CPPHOAFPARSER_HOALEXER_H
+#define CPPHOAFPARSER_HOALEXER_H
+
+#include