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

(DA) Add cpphoafparser 0.99.2 

Add cpphoafparser 0.99.2 as 3rdparty library (for HOA automata parsing).
tempestpy_adaptions
Joachim Klein 4 years ago
committed by Stefan Pranger
parent
f4fb0188be
commit
8d680749cd
35 changed files with 10645 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 10
      resources/3rdparty/CMakeLists.txt
  2. 24
      resources/3rdparty/cpphoafparser-0.99.2/ChangeLog
  3. 2362
      resources/3rdparty/cpphoafparser-0.99.2/Doxyfile
  4. 2362
      resources/3rdparty/cpphoafparser-0.99.2/Doxyfile.all
  5. 20
      resources/3rdparty/cpphoafparser-0.99.2/Makefile
  6. 63
      resources/3rdparty/cpphoafparser-0.99.2/README
  7. 13
      resources/3rdparty/cpphoafparser-0.99.2/docs/cpp2html.css
  8. 243
      resources/3rdparty/cpphoafparser-0.99.2/docs/cpphoaf-tool.html
  9. 183
      resources/3rdparty/cpphoafparser-0.99.2/docs/cpphoafparser-library.html
  10. 110
      resources/3rdparty/cpphoafparser-0.99.2/docs/cpphoafparser.css
  11. 145
      resources/3rdparty/cpphoafparser-0.99.2/docs/index.html
  12. 115
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/atom_acceptance.hh
  13. 120
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/atom_label.hh
  14. 302
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/boolean_expression.hh
  15. 218
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer.hh
  16. 48
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_exception.hh
  17. 109
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_null.hh
  18. 238
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_print.hh
  19. 148
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate.hh
  20. 828
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_check_validity.hh
  21. 185
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_resolve_aliases.hh
  22. 255
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_trace.hh
  23. 534
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_lexer.hh
  24. 692
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_parser.hh
  25. 58
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_parser_exception.hh
  26. 122
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_parser_helper.hh
  27. 77
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/util/acceptance_repository.hh
  28. 388
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/util/acceptance_repository_standard.hh
  29. 124
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/util/dynamic_bitset.hh
  30. 156
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/util/implicit_edge_helper.hh
  31. 116
      resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/util/int_or_string.hh
  32. 15
      resources/3rdparty/cpphoafparser-0.99.2/src/CMakeLists.txt
  33. 19
      resources/3rdparty/cpphoafparser-0.99.2/src/basic_parser_1.cc
  34. 40
      resources/3rdparty/cpphoafparser-0.99.2/src/basic_parser_2.cc
  35. 203
      resources/3rdparty/cpphoafparser-0.99.2/src/cpphoaf.cc

10
resources/3rdparty/CMakeLists.txt
View File

@ -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

24
resources/3rdparty/cpphoafparser-0.99.2/ChangeLog
View File

@ -0,0 +1,24 @@
2016-02-26 Joachim Klein <klein@tcs.inf.tu-dresden.de>
* 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 <stdexcept> 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 <klein@tcs.inf.tu-dresden.de>
* Release version 0.99.1: Initial (preliminary) release

2362
resources/3rdparty/cpphoafparser-0.99.2/Doxyfile
File diff suppressed because it is too large
View File

2362
resources/3rdparty/cpphoafparser-0.99.2/Doxyfile.all
File diff suppressed because it is too large
View File

20
resources/3rdparty/cpphoafparser-0.99.2/Makefile
View File

@ -0,0 +1,20 @@
# CXXFLAGS for debugging:
# CXXFLAGS=-g -O1 -Wall
# CXXFLAGS for production
CXXFLAGS=-O3 -Wall
cpphoaf : src/cpphoaf.cc include/cpphoafparser/*/*.hh
$(CXX) $(CXXFLAGS) -I include --std=c++11 -o $@ $<
# The example parsers
basic_parser_1 : src/basic_parser_1.cc include/cpphoafparser/*/*.hh
$(CXX) $(CXXFLAGS) -I include --std=c++11 -o $@ $<
basic_parser_2 : src/basic_parser_2.cc include/cpphoafparser/*/*.hh
$(CXX) $(CXXFLAGS) -I include --std=c++11 -o $@ $<
.PHONY: all
all: cpphoaf basic_parser_1 basic_parser_2

63
resources/3rdparty/cpphoafparser-0.99.2/README
View File

@ -0,0 +1,63 @@
==============================================================================
|
| cpphoafparser library (version 0.99.2)
|
| C++-based parser for the Hanoi Omega Automata Format
|
| http://automata.tools/hoa/cpphoafparser/
=============================================================================
Copyright (c) 2015-
Authors:
* Joachim Klein <klein@tcs.inf.tu-dresden.de>
* David Mueller <david.mueller@tcs.inf.tu-dresden.de>
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
-----------------------------------------------------------------------------
Quick start
-----------------------------------------------------------------------------
(0) Have a look at the documentation in docs/index.html or at
http://automata.tools/hoa/cpphoafparser/
(1) Compile the library. In this directory, execute
make
(2) Using the command-line tool:
./cpphoaf parse automaton.hoa
Parse the automaton.hoa file and check for errors
./cpphoaf print automaton.hoa
Parse the automaton.hoa file and print back the parsed automaton
./cpphoaf print --resolve-aliases automaton.hoa
Parse the automaton.hoa file, resolve any aliases and
print back the parsed automaton
./cpphoaf help
Print additional options
Instead of a file, use - to read from standard input, i.e.,
tool-that-writes-hoa-to-stdout | ./cpphoaf parse -

13
resources/3rdparty/cpphoafparser-0.99.2/docs/cpp2html.css
View File

@ -0,0 +1,13 @@
.comment { color: #008000; font-style: italic; }
.pre { color: #000099; }
.string { color: #009900; }
.char { color: #009900; }
.float { color: #996600; }
.int { color: #000080; }
.bool { color: #000000; font-weight: bold; }
.type { color: #0000FF; }
.flow { color: #800000; }
.keyword { color: #000000; }
.operator { color: #000000; font-weight: bold; }
.operator { color: #000000; font-weight: bold; }

243
resources/3rdparty/cpphoafparser-0.99.2/docs/cpphoaf-tool.html
View File

@ -0,0 +1,243 @@
<!DOCTYPE HTML>
<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<link href="cpphoafparser.css" rel="stylesheet">
<title>The cpphoaf command-line tool [cpphoafparser Library for the Hanoi Omega-Automata Format (HOAF), version 0.99.2]</title>
</head>
<body>
<div class="nav"><a class="nav" href="index.html">^ Overview</a></div>
<h1>
The <span class="blue1">cpp</span><span class="blue2">hoaf</span> Command-Line Tool<br/>
<span style="font-size:70%">The <span class="blue">cpphoafparser</span>
Library for the Hanoi Omega-Automata Format (HOAF), version 0.99.2</span>
</h1>
<p>
The cpphoafparser library provides a command-line interface to some of
the functionality. This can be roughly divided into two broad areas:
</p>
<ul>
<li><em>Validating</em> an automaton (no syntax errors, declared properties are correct, ...)</li>
<li><em>Transforming</em> an automaton (translating from state- to transition-based acceptance, ...)</li>
</ul>
<p>We assume here that the reader is familiar with the basic concepts of
the <a href="http://adl.github.io/hoaf/">Hanoi Omega-Automata Format (HOAF)</a>.
</p>
<h2><a name="general">General</a></h2>
<h3>Obtaining and invoking the command-line tool</h3>
We assume here that you have downloaded the source code archive
from the <a href="http://automata.tools/hoa/cpphoafparser/">website</a>.
Unpack and build (Linux, OS X, ...):
<pre class="command">
tar xzvf cpphoafparser-xx.yy.tgz
cd cpphoafparser-xx.yy
make
</pre>
<p>
where <i>xx.yy</i> is the version.</p>
<p>Alternatively, for Windows, you can download a precompiled binary.</p>
<p>There is also a <span class="classname">CMakeLists.txt</span>
configuration for <a href="http://www.cmake.org/">CMake</a> available. In the top-level directory, execute:
<pre class="command">
mkdir build
cd build
cmake ../src
make
</pre>
<p>CMake can alse be used to generate Visual Studio project files.</p>
<h3>Getting Help</h3>
<p>With</p>
<pre class="command">
./cpphoaf help
</pre>
<p>you'll obtain a brief description of the supported commands and
flags.</p>
<h3>Input / Output</h3>
<p>
The command-line tool reads the file specified on the command-line, performs the required
processing and outputs the result to the standard output.
The hyphen character '-' can be used instead of the filename for reading from standard input.
Below, we provide some examples of invoking the command-line tool:
</p>
<p>
In the simplest case, the following command parses the automaton
from automaton.hoa and prints the result
(the parsed automaton without comments, extra whitespace, etc) to the
console:
</p>
<pre class="command">
./cpphoaf print automaton.hoa
</pre>
<p>
In the next example, we pipe the output of some other tool to the
input of cpphoaf:
</p>
<pre class="command">
./some-hoa-producer | ./cpphoaf print -
</pre>
<p>
The output can be captured as usual to a file using redirection:
</p>
<pre class="command">
./some-hoa-producer | ./cpphoaf print - > result.hoa
</pre>
<p>
Note: Take care that you do not simultaneously read and write from/to the same file!
</p>
<h3>Commands and Flags</h3>
<p>
The general structure of invoking the command line-tool is
</p>
<pre class="command">
./cpphoaf command flag(s) file(s)
</pre>
<h3>Multiple automata</h3>
<p>
The HOA format supports the streaming of automata, i.e., the ability to represent a
sequence of automata in a single file.
</p>
<p>
Please note that, currently, the <span class="prog">cpphoaf</span> tool only supports parsing
a single automaton.
</p>
<h3>Exit value</h3>
<p>
If you want to use the command-line tool in scripts, the value returned by the tool on exit
is useful for diagnosing errors. The tool will return 0 for success/no errors. If there are
errors during the processing of the automata, the value 1 will be returned. If there are problems
with the invocation (invalid command-line arguments, ...), the value 2
will be returned.
</p>
<h2><a name="validating">Validating Automata</a></h2>
<p>To check that an automaton in HOA format can be successfully parsed, run
</p>
<pre class="commandWithOutput">
./cpphoaf parse automaton-file.hoa
</pre>
<pre class="output">
Parsing OK
</pre>
<p>If everything went fine, the tool will output that parsing was OK,
otherwise there will be an error message indicating what went wrong.</p>
<p>Upon success, the automaton</p>
<ul>
<li>has been successfully parsed (syntax conforms to the HOA
format),</li>
<li>properties specified in the header have been verified to be
correct (violations of <em>state-labels</em>, <em>trans-labels</em>,
<em>implicit-labels</em>, <em>explicit-labels</em>, <em>state-acc</em>,
<em>trans-acc</em>, <em>no-univ-branch</em>, <em>colored</em> are currently detected;
for the <em>deterministic</em> and <em>complete</em> properties, violations are
currently only detected when implicit transition labels are used),
</li>
<li>if an <em>acc-name</em> header has been provided and is one
of the standard acceptance conditions specified in the format, the
correspondence with the <em>Acceptance</em> header has been verified
</li>
<li>the number, ordering and names of the states are valid with regard to
the restrictions specified in the HOA format,
</li>
<li>if implicit transition labels are used, the required number is present,
</li>
<li>alias definitions are non-recursive and all aliases, atomic propositions and
acceptance sets that are used are defined.
</li>
</ul>
<p>
The semantic validations can be disabled by the command-line
option <span class="cmdline">--no-validate</span>. The following command
will only check the syntactic correctness according to the HOA format:
</p>
<pre class="command">
./cpphoaf parse --no-validate automaton.hoa
</pre>
<h2>Transforming the Automaton</h2>
<h3>Pretty-printing the Automaton</h3>
<p>The simplest transformation is barely a transformation at all. Via</p>
<pre class="command">
./cpphoaf print automaton-file.hoa
</pre>
<p>the automaton is simply parsed and printed back to the standard output.</p>
<p>
As comments and superfluous whitespace are ignored by the parser, this transforms the
automaton into some kind of canonical form, with the different elements of the HOA format
each placed on a single line.
</p>
<h3>Resolving Aliases</h3>
<p>
The command-line option <span class="cmdline">--resolve-aliases</span> activates a transformation
that (1) removes the <em>Alias:</em> <a class="explanationref" href="http://adl.github.io/hoaf/#alias" target="_blank">?</a>
definitions and (2) resolves all <em>@alias</em> references in
transition labels.</p>
<p>The following command reads the automaton, resolves the aliases and prints the resulting automaton:</p>
<pre class="command">
./cpphoaf print --resolve-aliases automaton-file.hoa
</pre>
<p>
The option <span class="cmdline">--resolve-aliases</span>
can be used with all other commands and options.
</p>
<h2>Tracing, Implementation Details</h2>
<p>If you wish to implement your own transformations or want to use the cpphoafparser library,
it might be interesting to play around with the <span class="cmdline">--trace</span> option:</p>
<pre class="command">
./cpphoaf parse --trace automaton-file.hoa
</pre>
<p>
If activated, tracing will output the sequence of method calls into
the <em>HOAConsumer</em> by
the parser. This can be used to study the correspondence of syntactical elements in the
HOA format and the method calls.
</p>
<p>
The command-line utility is implemented in the
<span class="classname">src/cpphoaf.cc</span>. It relies on the various
<em>HOAConsumers</em> for the functionality and is a good entry-point for further investigations.
</p>
<hr>
<p>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!</p>
<p>(c) 2015-2016
Joachim Klein &lt;klein&#064;tcs.inf.tu-dresden.de&gt;,
David M&uuml;ller &lt;david.mueller&#064;tcs.inf.tu-dresden.de&gt;
</body>
</html>

183
resources/3rdparty/cpphoafparser-0.99.2/docs/cpphoafparser-library.html
View File

@ -0,0 +1,183 @@
<!DOCTYPE HTML>
<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<link href="cpphoafparser.css" rel="stylesheet">
<link href="cpp2html.css" rel="stylesheet">
<title>Using the cpphoafparser Library [cpphoafparser Library for the Hanoi Omega-Automata Format (HOAF), version 0.99.2]</title>
</head>
<body>
<div class="nav"><a class="nav" href="index.html">^ Overview</a></div>
<h1>
Using the <span class="blue1">cpp</span><span class="blue2">hoaf</span><span class="blue3">parser</span> Library<br/>
<span style="font-size:70%">The <span class="blue">cpphoafparser</span>
Library for the Hanoi Omega-Automata Format (HOAF), version 0.99.2</span>
</h1>
<p>The cpphoafparser library can be used to parse and process &omega;-automata
in the HOA format. We assume here that the reader is familiar with the basic concepts of
the <a href="http://adl.github.io/hoaf/">Hanoi Omega-Automata Format (HOAF)</a>.
</p>
<h2><a name="general">General Structure</a></h2>
<p>
The two main building blocks of the parser library are the <em>parser</em> and
classes implementing the <em>HOAConsumer</em> interface. A <em>HOAConsumer</em> has functions
corresponding to the various elements that can occur in a HOA automaton. While parsing, the parser
calls each of these functions to indicate that this particular element has just occurred.
</p>
<p>cpphoafparser is a <emph>header-only</emph> C++ library, i.e., it suffices to
add the <span class="classname">include</span> directory to the include path of your compiler
and include the corresponding header files. All cpphoafparser elements are contained in the
<span class="classname">cpphoafparser</span> namespace. It uses C++11 features, so ensure that your
compiler is configured to support this standard version.
</p>
<h3>A Basic Parser</h3>
<p>The most basic use of the cpphoafparser library is shown in the following code snippet
(<span class="classname">src/basic_parser_1.cc</span></span>):</p>
<div class="code">
<pre><span class="pre">#include "cpphoafparser/consumer/hoa_consumer_print.hh"
#include "cpphoafparser/parser/hoa_parser.hh"
</span><span class="keyword">
using namespace</span> cpphoafparser<span class="operator">;</span><span class="comment">
/** The most basic HOA parser: Read an automaton from input and print it to the output. */</span><span class="type">
int</span><span class="keyword"> main</span><span class="operator">(</span><span class="type">int</span> argc<span class="operator">,</span><span class="keyword"> const</span><span class="type"> char</span><span class="operator">*</span> argv<span class="operator">[]) {</span>
HOAConsumer<span class="operator">::</span>ptr consumer<span class="operator">(</span><span class="keyword">new</span> HOAConsumerPrint<span class="operator">(</span>std<span class="operator">::</span>cout<span class="operator">));</span><span class="flow">
try</span><span class="operator"> {</span>
HOAParser<span class="operator">::</span>parse<span class="operator">(</span>std<span class="operator">::</span>cin<span class="operator">,</span> consumer<span class="operator">);
}</span><span class="flow"> catch</span><span class="operator"> (</span>std<span class="operator">::</span>exception<span class="operator">&amp;</span> e<span class="operator">) {</span>
std<span class="operator">::</span>cerr<span class="operator"> &lt;&lt;</span> e<span class="operator">.</span>what<span class="operator">() &lt;&lt;</span> std<span class="operator">::</span>endl<span class="operator">;</span><span class="flow">
return</span><span class="int"> 1</span><span class="operator">;
}</span><span class="flow">
return</span><span class="int"> 0</span><span class="operator">;
}</span>
</pre>
</div>
<p>
Here, the parser reads from <span class="classname">std::cin</span>
and calls into a <span class="classname">HOAConsumerPrint</span>
object that just outputs the elements to <span class="classname">std::cout</span>.</p>
<h3>Chaining Multiple HOAConsumers: HOAIntermediate</h3>
<p>The <span class="classname">HOAIntermediate</span> class, which itself
implements the <span class="classname">HOAConsumer</span> interface, provides the basis for chaining multiple
<span class="classname">HOAConsumers</span>, one after another, each reading the output of the previous one.
</p>
<p>
Consider the following example
(<span class="classname">src/basic_parser_2.cc</span></span>):</p>
<div class="code">
<pre><span class="pre">#include "cpphoafparser/consumer/hoa_intermediate.hh"
#include "cpphoafparser/consumer/hoa_consumer_null.hh"
#include "cpphoafparser/parser/hoa_parser.hh"
</span><span class="keyword">
using namespace</span> cpphoafparser<span class="operator">;</span><span class="comment">
/* An HOAIntermediate that counts invocations of addState */</span><span class="keyword">
class</span> CountStates<span class="operator"> :</span><span class="keyword"> public</span> HOAIntermediate<span class="operator"> {</span><span class="keyword">
public</span><span class="operator">:</span><span class="keyword">
typedef</span> std<span class="operator">::</span>shared_ptr<span class="operator">&lt;</span>CountStates<span class="operator">&gt;</span> ptr<span class="operator">;</span><span class="type">
unsigned int</span> count<span class="operator"> =</span><span class="int"> 0</span><span class="operator">;</span>
CountStates<span class="operator">(</span>HOAConsumer<span class="operator">::</span>ptr next<span class="operator">) :</span> HOAIntermediate<span class="operator">(</span>next<span class="operator">) {
}</span><span class="keyword">
virtual</span><span class="type"> void</span> addState<span class="operator">(</span><span class="type">unsigned int</span> id<span class="operator">,</span>
std<span class="operator">::</span>shared_ptr<span class="operator">&lt;</span>std<span class="operator">::</span>string<span class="operator">&gt;</span> info<span class="operator">,</span>
label_expr<span class="operator">::</span>ptr labelExpr<span class="operator">,</span>
std<span class="operator">::</span>shared_ptr<span class="operator">&lt;</span>int_list<span class="operator">&gt;</span> accSignature<span class="operator">)</span> override<span class="operator"> {</span>
count<span class="operator">++;</span>
next<span class="operator">-&gt;</span>addState<span class="operator">(</span>id<span class="operator">,</span> info<span class="operator">,</span> labelExpr<span class="operator">,</span> accSignature<span class="operator">);
}
};</span><span class="comment">
/** Demonstrating the use of HOAIntermediates */</span><span class="type">
int</span><span class="keyword"> main</span><span class="operator">(</span><span class="type">int</span> argc<span class="operator">,</span><span class="keyword"> const</span><span class="type"> char</span><span class="operator">*</span> argv<span class="operator">[]) {</span>
HOAConsumer<span class="operator">::</span>ptr hoaNull<span class="operator">(</span><span class="keyword">new</span> HOAConsumerNull<span class="operator">());</span>
CountStates<span class="operator">::</span>ptr counter<span class="operator">(</span><span class="keyword">new</span> CountStates<span class="operator">(</span>hoaNull<span class="operator">));</span><span class="flow">
try</span><span class="operator"> {</span>
HOAParser<span class="operator">::</span>parse<span class="operator">(</span>std<span class="operator">::</span>cin<span class="operator">,</span> counter<span class="operator">);</span>
std<span class="operator">::</span>cout<span class="operator"> &lt;&lt;</span><span class="string"> "Number of state definitions = "</span><span class="operator"> &lt;&lt;</span> counter<span class="operator">-&gt;</span>count<span class="operator"> &lt;&lt;</span> std<span class="operator">::</span>endl<span class="operator">;
}</span><span class="flow"> catch</span><span class="operator"> (</span>std<span class="operator">::</span>exception<span class="operator">&amp;</span> e<span class="operator">) {</span>
std<span class="operator">::</span>cerr<span class="operator"> &lt;&lt;</span> e<span class="operator">.</span>what<span class="operator">() &lt;&lt;</span> std<span class="operator">::</span>endl<span class="operator">;</span><span class="flow">
return</span><span class="int"> 1</span><span class="operator">;
}</span><span class="flow">
return</span><span class="int"> 0</span><span class="operator">;
}</span>
</pre>
</div>
<p>We derive <span class="classname">CountStates</span> from <span class="classname">HOAIntermediate</span>.
Its constructor takes the next <span class="classname">HOAConsumer</span> in the chain, which can
again be a <span class="classname">HOAIntermediate</span>. Here, we are passing a
<span class="classname">HOAConsumerNull</span> object, which does nothing when called, acting as a "no-operation"
end of the consumer chain. Inside the <span class="classname">CountStates</span>, we override the
<span class="classname">addState</span> method, which is called for each <em>State:</em>
definition in the automaton.
We count the number of definitions and pass along the arguments to the next consumer.
In the end, we just output the count of the definitions.
</p>
<h2>The HOAConsumer API</h2>
<p>
A good starting point for learning about the HOAConsumer API is the
<a
href="http://automata.tools/hoa/cpphoafparser/docs/api-html/classcpphoafparser_1_1_h_o_a_consumer.html">documentation of the HOAConsumer interface</a>
as well as the rest of the <a href="http://automata.tools/hoa/cpphoafparser/docs/api-html/index.html">API documentation</a>.
<p>Another good introduction is the source code of the <span class="classname">HOAConsumerPrint</span> class,
as it translates back from the method calls in the <span class="classname">HOAConsumer</span> interface to the
textual representation of the HOA format.
</p>
<p>Some further tidbits that might be useful:</p>
<ul>
<li>The boolean expressions for the explicit transition labels and the acceptance condition
are represented by
<a href="http://automata.tools/hoa/cpphoafparser/docs/api-html/classcpphoafparser_1_1_boolean_expression.html"><span class="classname">BooleanExpression</span></a>,
with appropriate <span class="classname">Atoms</span> for the leaf nodes in the abstract syntax tree.
The <span class="classname">BooleanExpressions</span> are designed to
be <em>immutable</em>. Therefore, subtrees can be safely shared between expressions.
</li>
<li>
If you encounter an error inside one of the <span class="classname">HOAConsumer</span> method calls, throw an
<a href="http://automata.tools/hoa/cpphoafparser/docs/api-html/classcpphoafparser_1_1_h_o_a_consumer_exception.html">HOAConsumerException</a>.
</li>
<li>Memory managment is generally handled via <span class="classname">shared_ptr</span> pointers.</li>
<li>
To trace the method calls into a <span class="classname">HOAConsumer</span> or <span class="classname">HOAIntermediate</span>,
wrap it into a <a href="http://automata.tools//hoa/cpphoafparser/docs/api-html/classcpphoafparser_1_1_h_o_a_intermediate_trace.html"><span class="classname">HOAIntermediateTrace</span></a>
object. This will print all the function invocations to the standard output, including the parameters.
</li>
</ul>
<hr>
<p>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!</p>
<p>(c) 2015-2016
Joachim Klein &lt;klein&#064;tcs.inf.tu-dresden.de&gt;,
David M&uuml;ller &lt;david.mueller&#064;tcs.inf.tu-dresden.de&gt;
</body>
</html>

110
resources/3rdparty/cpphoafparser-0.99.2/docs/cpphoafparser.css
View File

@ -0,0 +1,110 @@
body {font-family:sans-serif;
margin: auto;
max-width: 60em;
text-align: justify;
line-height: 1.4;
font-size: 1em;
}
div.nav { margin-top:1em; position: absolute; top:0em; left:0em}
a.nav {text-decoration: none; color:grey; margin:1em}
.prog {
font-weight: bold;
font-family: monospace;
font-size: larger;
}
.cmdline {
font-weight: normal;
font-family: monospace;
font-size: larger;
}
.classname {
font-weight: normal;
font-family: monospace;
font-size: larger;
}
.alert {
background-color: #ffd0d0;
border: 1px solid #c0d0d0;
}
h1 {
padding-top: 1em;
border-bottom: 3px solid #4F8BAB;
text-align: center;
}
h2 {
background-color: #6FC5EB;
padding: 0.3em;
margin-left: -.5em;
margin-right: -.5em;
margin-top: 2em;
border: 1px solid grey;
border-radius: 0.2em;
}
h3 {
background-color: #E0F0FF;
padding: 0.3em;
margin-left: -0.5em;
margin-top: 2em;
border: 1px solid black;
border-radius: 0.2em;
}
.blue1 { color: #4F8BAB; }
.blue2 { color: #4F9BC9; }
.blue3 { color: #64B3DF; }
:link, :visited { color: #4f4fe0; text-decoration: none }
a.explanationref {font-size:70%; vertical-align: super}
div.block {
margin-left: 2em;
margin-right: 2em;
padding: 0.5em;
border: 1px solid blue;
margin-bottom: 1em;
}
li {
padding-bottom: 0.5em;
}
pre {
font-size: 120%
}
pre.command {
background-color: #f0f0f0;
margin: 1em 2em;
padding: 0.5em 0em 0.5em 2em;
border-radius: 0.15em;
}
pre.commandWithOutput {
background-color: #f0f0f0;
margin: 1em 2em 0em 2em;
padding: 0.5em 0em 0.5em 2em;
border-radius: 0.15em;
}
pre.output {
background-color: #e0e0e0;
margin: 0em 2em 1em 3em;
padding: 0.5em 0em 0.5em 2em;
border-radius: 0.15em;
}
div.code {
margin: 0.5em; padding: 0.5em; border: 1px solid #c0c0c0;
}

145
resources/3rdparty/cpphoafparser-0.99.2/docs/index.html
View File

@ -0,0 +1,145 @@
<!DOCTYPE HTML>
<html>
<head>
<meta http-equiv="content-type" content="text/html; charset=utf-8">
<link href="cpphoafparser.css" rel="stylesheet">
<title>The cpphoafparser Library for the Hanoi Omega-Automata Format (HOAF): Documentation (version 0.99.2)</title>
</head>
<body>
<div class="nav"></div>
<h1>
The <span class="blue1">cpp</span><span class="blue2">hoaf</span><span class="blue3">parser</span> Library
for the <br>Hanoi Omega-Automata Format (HOAF):<br/> Documentation (version 0.99.2)
</h1>
<h2><a name="overview">Overview</a></h2>
<p>The <a href="http://adl.github.io/hoaf/">Hanoi Omega-Automata
Format (HOAF)</a>
provides a flexible and robust mechanism for exchanging
&omega;-automata between different tools.
With the <span class="prog">cpphoafparser</span> library, we provide (1)
a C++-based parser library for parsing HOA files that can be used
by applications and tools that want to read HOA files and (2) a
command-line tool for performing basic automata operations.
</p>
<p>You can find the most current version of the library at
<a href="http://automata.tools/hoa/cpphoafparser/">http://automata.tools/hoa/cpphoafparser/</a>,
as well as links to example automata.
</p>
<p>If you are interested in a Java-based variant of this library,
check out <a href="http://automata.tools/hoa/jhoafparser/">jhoafparser</a>.
<span class="prog">cpphoafparser</span> and <span class="prog">jhoafparser</span>
share the same design, but may differ in some of the features that are implemented.
</p>
<p><span class="prog">cpphoafparser</span> is free software and
released under the terms of the GNU Lesser General Public License, version 2.1.</p>
<h2>The Command-Line Tool</h2>
<h3>The Command-Line Tool: First Steps</h3>
<p>
We assume here that you have downloaded the source code archive from the website and built the tool
using</p>
<pre class="command">
make
</pre>
which allows you to invoke the tool via
</p>
<pre class="command">
./cpphoaf
</pre>
<p>Alternatively, you have downloaded a precompiled <span class="prog">cpphoaf</span> binary from the website.</p>
<p>
Here are some examples for the command-line <span class="prog">cpphoaf</span> tool:
</p>
<p><b>Parsing (validating) an automaton in HOA format</b></p>
<pre class="command">
./cpphoaf parse automaton-file.hoa
</pre>
<p>
Some of the semantic validations can be disabled by the command-line option
<span class="cmdline">--no-validate</span>.
</p>
<p><b>Printing an automaton in HOA format</b> to standard output</p>
<pre class="command">
./cpphoaf print automaton-file.hoa
</pre>
<p><b>Resolving aliases</b></p>
<pre class="command">
./cpphoaf print --resolve-aliases automaton-file.hoa
</pre>
<h3>The Command-Line Tool: Further information</h3>
<p>
Further details on the command-line tool can be found <a href="cpphoaf-tool.html">here</a>.</p>
<h2>The HOA Parser Library</h2>
<p>The <span class="prog">cpphoafparser</span> 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.
</p>
<p>
As a first step, download the source code of the library from the
<a href="http://automata.tools/hoa/cpphoafparser/">website</a>.
Then, build a local copy of the API documentation with the <a href="http://www.doxygen.org">Doxygen</a> tool:
</p>
<pre class="command">
doxygen Doxyfile
</pre>
<p>This produces the API documentation in the <span class="cmdline">docs/api-html</span> subdirectory.
The alternative <span class="classname">Doxyfile.all</span> configuration file produces documentation for all
the private/implementation details as well. If you do not have the <a href="http://www.graphviz.org/">dot</a> utility
installed, set <span class="classname">HAVE_DOT = NO</span> in <span class="classname">Doxyfile</span>.
</p>
<p>
The API documentation of the current version of the library is available as well on the website at
<a href="http://automata.tools/hoa/cpphoafparser/docs/api-html/">http://automata.tools/hoa/cpphoafparser/docs/api-html/</a>.
</p>
<p>
A good starting point is the API documentation of the <span class="classname">HOAConsumer</span>
interface and the source code of <span class="classname">src/cpphoaf.cc</span>,
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 <span class="cmdline">HOAConsumer</span> interface.
The parser then invokes the functions corresponding to the element in the HOA file format while parsing the automaton.
</p>
<h3>The Parser Library: Further information</h3>
<p>More details and an overview over the cpphoafparser architecture can be found <a href="cpphoafparser-library.html">here</a>.
<h2><a name="links">Additional links</a></h2>
<ul>
<li>The <a href="http://adl.github.io/hoaf/">specification</a> of the Hanoi Omega-Automata Format (HOAF).
</li>
<li>A <a href="http://adl.github.io/hoaf/support.html">page listing tools</a> that support HOAF.</li>
<li>A <a href="https://github.com/adl/hoaf-tests">GitHub repository with HOA automata for testing</a>.</li>
</ul>
<hr>
<p>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!</p>
<p>(c) 2015-2016
Joachim Klein &lt;klein&#064;tcs.inf.tu-dresden.de&gt;,
David M&uuml;ller &lt;david.mueller&#064;tcs.inf.tu-dresden.de&gt;
</body>
</html>

115
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/atom_acceptance.hh
View File

@ -0,0 +1,115 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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 <memory>
#include <iostream>
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<AtomAcceptance> 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

120
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/atom_label.hh
View File

@ -0,0 +1,120 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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 <memory>
#include <string>
#include <iostream>
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<AtomLabel> 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<std::string>(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<std::string> 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

302
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/ast/boolean_expression.hh
View File

@ -0,0 +1,302 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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 <memory>
#include <iostream>
#include <sstream>
#include <stdexcept>
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 <Atoms> The atoms (leaf nodes) in the abstract syntax tree.
*/
template <typename Atoms>
class BooleanExpression {
public:
/** A shared_ptr to a node in this AST */
typedef std::shared_ptr< BooleanExpression<Atoms> > 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<Atoms>(EXP_AND, left, right));
}
/** Disjunction operator */
friend ptr operator|(ptr left, ptr right) {
return ptr(new BooleanExpression<Atoms>(EXP_OR, left, right));
}
/** Negation operator */
friend ptr operator!(ptr other) {
return ptr(new BooleanExpression<Atoms>(EXP_NOT, other, nullptr));
}
/** Output operator, renders in HOA syntax */
friend std::ostream& operator<<(std::ostream& out, const BooleanExpression<Atoms>& 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

218
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer.hh
View File

@ -0,0 +1,218 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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 <vector>
#include <memory>
#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<HOAConsumer> ptr;
/** A label expression */
typedef BooleanExpression<AtomLabel> label_expr;
/** An acceptance expression */
typedef BooleanExpression<AtomAcceptance> acceptance_expr;
/** A list of integers */
typedef std::vector<unsigned int> 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<std::string>& 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<IntOrString>& 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<std::string> version) = 0;
/**
* Called by the parser for the "properties: ..." item [optional, multiple].
* @param properties a list of properties
*/
virtual void addProperties(const std::vector<std::string>& 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<IntOrString>& 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<std::string> info, label_expr::ptr labelExpr, std::shared_ptr<int_list> 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<int_list> 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.
* <br/>
* @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<int_list> 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

48
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_exception.hh
View File

@ -0,0 +1,48 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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 <stdexcept>
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

109
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_null.hh
View File

@ -0,0 +1,109 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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<std::string>& aps) override {
}
virtual void setAcceptanceCondition(unsigned int numberOfSets, acceptance_expr::ptr accExpr) override {
}
virtual void provideAcceptanceName(const std::string& name, const std::vector<IntOrString>& extraInfo) override {
}
virtual void setName(const std::string& name) override {
}
virtual void setTool(const std::string& name, std::shared_ptr<std::string> version) override {
}
virtual void addProperties(const std::vector<std::string>& properties) override {
}
virtual void addMiscHeader(const std::string& name, const std::vector<IntOrString>& content) override {
}
virtual void notifyBodyStart() override {
}
virtual void addState(unsigned int id, std::shared_ptr<std::string> info, label_expr::ptr labelExpr, std::shared_ptr<int_list> accSignature) override {
}
virtual void addEdgeImplicit(unsigned int stateId, const int_list& conjSuccessors, std::shared_ptr<int_list> accSignature) override {
}
virtual void addEdgeWithLabel(unsigned int stateId, label_expr::ptr labelExpr, const int_list& conjSuccessors, std::shared_ptr<int_list> accSignature) override {
}
virtual void notifyEndOfState(unsigned int stateId) override {
}
virtual void notifyEnd() override {
}
virtual void notifyAbort() {
}
virtual void notifyWarning(const std::string& warning) {
}
};
}
#endif

238
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_consumer_print.hh
View File

@ -0,0 +1,238 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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 <iostream>
#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<std::string>& 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<IntOrString>& 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<std::string> 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<std::string>& 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<IntOrString>& 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<std::string> info,
label_expr::ptr labelExpr,
std::shared_ptr<int_list> 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<int_list> 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<int_list> 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

148
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate.hh
View File

@ -0,0 +1,148 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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<std::string>& 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<IntOrString>& 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<std::string> version) override {
next->setTool(name, version);
}
virtual void addProperties(const std::vector<std::string>& properties) override {
next->addProperties(properties);
}
virtual void addMiscHeader(const std::string& name, const std::vector<IntOrString>& content) override {
next->addMiscHeader(name, content);
}
virtual void notifyBodyStart() override {
next->notifyBodyStart();
}
virtual void addState(unsigned int id,
std::shared_ptr<std::string> info,
label_expr::ptr labelExpr,
std::shared_ptr<int_list> accSignature) override {
next->addState(id, info, labelExpr, accSignature);
}
virtual void addEdgeImplicit(unsigned int stateId,
const int_list& conjSuccessors,
std::shared_ptr<int_list> accSignature) override {
next->addEdgeImplicit(stateId, conjSuccessors, accSignature);
}
virtual void addEdgeWithLabel(unsigned int stateId,
label_expr::ptr labelExpr,
const int_list& conjSuccessors,
std::shared_ptr<int_list> 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

828
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_check_validity.hh
View File

@ -0,0 +1,828 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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 <unordered_set>
#include <cassert>
namespace cpphoafparser {
// TODO Accurately reflect status in the doc!
/**
* HOAIntermediate that checks that the parsed HOA automaton is well-formed.
*
* Among others, checks for
* <ul>
* <li>Conformance of stated properties with the automaton structure.
* <li>Conformance of Acceptance and acc-name headers.
* <li>Definedness of aliases.
* <li>Well-formedness of label expressions (only using atomic proposition indizes that are defined).
* <li>Well-formedness of acceptance (only using acceptance set indizes that are defined).
* </ul>
*/
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 <class InputIterator>
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<std::string>& aps) {
headerAtMostOnce("AP");
numberOfAPs.reset(new unsigned int(aps.size()));
std::unordered_set<std::string> 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<IntOrString>& 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<std::string> version) override {
headerAtMostOnce("tool");
next->setTool(name, version);
}
virtual void addProperties(const std::vector<std::string>& 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<IntOrString>& 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<std::size_t, bool> 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<std::string> info, label_expr::ptr labelExpr, std::shared_ptr<int_list> 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<int_list> 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<int_list> 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<std::size_t, bool> 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<std::string> supportedMiscHeaders;
/** The header names that have occurred so far in the automaton definition */
std::unordered_set<std::string> usedHeaders;
/** The number of states that have been specified in the header (optional) */
std::shared_ptr<unsigned int > numberOfStates;
/** The number of acceptance sets (mandatory) */
std::shared_ptr<unsigned int> 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<std::string> aliases;
/** Atomic propositions that are referenced in some alias definition */
dynamic_bitset apsInAliases;
/** The number of atomic propositions */
std::shared_ptr<unsigned int> numberOfAPs;
/** The acc-name (optional) */
std::shared_ptr<std::string> accName;
/** extraInfo parameters for acc-name */
std::vector<IntOrString> 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

185
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_resolve_aliases.hh
View File

@ -0,0 +1,185 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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 <unordered_map>
#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<std::string> info,
label_expr::ptr labelExpr,
std::shared_ptr<int_list> 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<int_list> 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<std::string, label_expr::ptr> 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

255
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/consumer/hoa_intermediate_trace.hh
View File

@ -0,0 +1,255 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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 <iostream>
#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<std::string>& 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<IntOrString>& 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<std::string> version) override {
traceFunction("setTool");
traceArgument("name", name);
traceArgument("version", version);
next->setTool(name, version);
}
virtual void addProperties(const std::vector<std::string>& properties) override {
traceFunction("addProperties");
traceArgument("properties", properties);
next->addProperties(properties);
}
virtual void addMiscHeader(const std::string& name, const std::vector<IntOrString>& 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<std::string> info,
label_expr::ptr labelExpr,
std::shared_ptr<int_list> 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<int_list> 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<int_list> 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 <typename Atom>
void traceArgument(const std::string& name, const BooleanExpression<Atom>& expr) {
out << " " << name << " = " << expr << std::endl;
}
/** Trace argument (vector) */
template <typename T>
void traceArgument(const std::string& name, const std::vector<T>& 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 <typename O>
void traceArgument(const std::string& name, typename std::shared_ptr<O> o) {
if ((bool)o) {
traceArgument(name, *o);
} else {
traceArgument(name, "null");
}
}
};
}
#endif

534
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_lexer.hh
View File

@ -0,0 +1,534 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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 <map>
#include <string>
#include <stdexcept>
#include "cpphoafparser/parser/hoa_parser_exception.hh"
namespace cpphoafparser {
/** Lexer for tokenizing a HOA stream (used internally by HOAParser). */
class HOALexer {
public:
/** The type of the tokens in a HOA stream. */
enum TokenType {
TOKEN_INT,
TOKEN_IDENT,
TOKEN_STRING,
TOKEN_HEADER_NAME,
TOKEN_ALIAS_NAME,
TOKEN_EOF,
TOKEN_BODY,
TOKEN_END,
TOKEN_ABORT,
TOKEN_HOA,
TOKEN_STATE,
TOKEN_STATES,
TOKEN_START,
TOKEN_AP,
TOKEN_ALIAS,
TOKEN_ACCEPTANCE,
TOKEN_ACCNAME,
TOKEN_TOOL,
TOKEN_NAME,
TOKEN_PROPERTIES,
// Punctuation, etc.
TOKEN_NOT,
TOKEN_AND,
TOKEN_OR,
TOKEN_LPARENTH,
TOKEN_RPARENTH,
TOKEN_LBRACKET,
TOKEN_RBRACKET,
TOKEN_LCURLY,
TOKEN_RCURLY,
TOKEN_TRUE,
TOKEN_FALSE
};
/** A token in the HOA stream. */
struct Token {
/** The kind of the token. */
TokenType kind;
/** The string representation of this token (if applicable) */
std::string vString;
/** The integer representation of this token (if applicable) */
unsigned int vInteger;
/** The line where this token started */
unsigned int line;
/** The column where this token started */
unsigned int col;
/** EOF (end-of-file) constructor. */
Token() : kind(TOKEN_EOF), vString(""), vInteger(0), line(0), col(0) {}
/** Constructor for syntactic element */
Token(TokenType kind, unsigned int line, unsigned int col) : kind(kind), vString(""), vInteger(0), line(line), col(col) {}
/** Constructor for a token having variable string content (e.g., TOKEN_IDENTIFIER, TOKEN_ALIAS, TOKEN_STRING, ...) */
Token(TokenType kind, const std::string vString, unsigned int line, unsigned int col) : kind(kind), vString(vString), vInteger(0), line(line), col(col) {}
/** Constructor for an unsigned integer token */
Token(unsigned int vInteger, unsigned int line, unsigned int col) : kind(TOKEN_INT), vString(""), vInteger(vInteger), line(line), col(col) {}
/** Returns true if this token represents the end-of-file. */
bool isEOF() const {return kind == TOKEN_EOF;}
/** Returns a string name for the given token type. */
static std::string typeAsString(TokenType kind) {
switch (kind) {
case TOKEN_INT: return std::string("INT");
case TOKEN_IDENT: return std::string("IDENT");
case TOKEN_STRING: return std::string("STRING");
case TOKEN_HEADER_NAME: return std::string("HEADER_NAME");
case TOKEN_ALIAS_NAME: return std::string("ALIAS_NAME");
case TOKEN_EOF: return std::string("EOF");
case TOKEN_BODY: return std::string("BODY");
case TOKEN_END: return std::string("END");
case TOKEN_ABORT: return std::string("ABORT");
case TOKEN_HOA: return std::string("HOA");
case TOKEN_STATE: return std::string("STATE");
case TOKEN_STATES: return std::string("STATES");
case TOKEN_START: return std::string("START");
case TOKEN_AP: return std::string("AP");
case TOKEN_ALIAS: return std::string("ALIAS");
case TOKEN_ACCEPTANCE: return std::string("ACCEPTANCE");
case TOKEN_ACCNAME: return std::string("ACCNAME");
case TOKEN_TOOL: return std::string("TOOL");
case TOKEN_NAME: return std::string("NAME");
case TOKEN_PROPERTIES: return std::string("PROPERTIES");
// Punctuation: etc.
case TOKEN_NOT: return std::string("NOT");
case TOKEN_AND: return std::string("AND");
case TOKEN_OR: return std::string("OR");
case TOKEN_LPARENTH: return std::string("LPARENTH");
case TOKEN_RPARENTH: return std::string("RPARENTH");
case TOKEN_LBRACKET: return std::string("LBRACKET");
case TOKEN_RBRACKET: return std::string("RBRACKET");
case TOKEN_LCURLY: return std::string("LCURLY");
case TOKEN_RCURLY: return std::string("RCURLY");
case TOKEN_TRUE: return std::string("TRUE");
case TOKEN_FALSE: return std::string("FALSE");
}
throw std::logic_error("Unhandled token type");
}
/** Returns a string name for the given token type (for use in error messages). */
static std::string forErrorMessage(TokenType kind) {
switch (kind) {
case TOKEN_INT: return std::string("INTEGER");
case TOKEN_IDENT: return std::string("IDENTIFIER");
case TOKEN_STRING: return std::string("STRING");
case TOKEN_HEADER_NAME: return std::string("HEADER_NAME");
case TOKEN_ALIAS_NAME: return std::string("ALIAS_NAME");
case TOKEN_EOF: return std::string("END-OF_FILE");
case TOKEN_BODY: return std::string("--BODY--");
case TOKEN_END: return std::string("--END--");
case TOKEN_ABORT: return std::string("--ABORT--");
case TOKEN_HOA: return std::string("HOA:");
case TOKEN_STATE: return std::string("State:");
case TOKEN_STATES: return std::string("States:");
case TOKEN_START: return std::string("Start:");
case TOKEN_AP: return std::string("AP:");
case TOKEN_ALIAS: return std::string("Alias:");
case TOKEN_ACCEPTANCE: return std::string("Acceptance:");
case TOKEN_ACCNAME: return std::string("acc-name:");
case TOKEN_TOOL: return std::string("tool:");
case TOKEN_NAME: return std::string("name:");
case TOKEN_PROPERTIES: return std::string("properties:");
// Punctuation: etc.
case TOKEN_NOT: return std::string("!");
case TOKEN_AND: return std::string("&");
case TOKEN_OR: return std::string("|");
case TOKEN_LPARENTH: return std::string("(");
case TOKEN_RPARENTH: return std::string(")");
case TOKEN_LBRACKET: return std::string("[");
case TOKEN_RBRACKET: return std::string("]");
case TOKEN_LCURLY: return std::string("{");
case TOKEN_RCURLY: return std::string("}");
case TOKEN_TRUE: return std::string("t");
case TOKEN_FALSE: return std::string("f");
}
throw std::logic_error("Unhandled token type");
}
/** Returns a string representation of a given token (for error messages). */
static std::string forErrorMessage(Token token) {
switch (token.kind) {
case TOKEN_INT: return std::string("INTEGER ")+std::to_string(token.vInteger);
case TOKEN_IDENT: return std::string("IDENTIFIER ")+token.vString;
case TOKEN_STRING: return std::string("STRING ")+token.vString;
case TOKEN_HEADER_NAME: return std::string("HEADER ")+token.vString;
case TOKEN_ALIAS_NAME: return std::string("ALIAS ")+token.vString;
case TOKEN_EOF: return std::string("END-OF-FILE");
case TOKEN_BODY: return std::string("--BODY--");
case TOKEN_END: return std::string("--END--");
case TOKEN_ABORT: return std::string("--ABORT--");
case TOKEN_HOA: return std::string("HEADER HOA");
case TOKEN_STATES: return std::string("HEADER States");
case TOKEN_START: return std::string("HEADERr Start");
case TOKEN_AP: return std::string("HEADER AP");
case TOKEN_ALIAS: return std::string("HEADER Alias");
case TOKEN_ACCEPTANCE: return std::string("HEADER Acceptance");
case TOKEN_ACCNAME: return std::string("HEADER acc-name");
case TOKEN_TOOL: return std::string("HEADER tool");
case TOKEN_NAME: return std::string("HEADER name");
case TOKEN_PROPERTIES: return std::string("HEADER properties");
case TOKEN_STATE: return std::string("DEFINITION State");
// Punctuation: etc.
case TOKEN_NOT: return std::string("!");
case TOKEN_AND: return std::string("&");
case TOKEN_OR: return std::string("|");
case TOKEN_LPARENTH: return std::string("(");
case TOKEN_RPARENTH: return std::string(")");
case TOKEN_LBRACKET: return std::string("[");
case TOKEN_RBRACKET: return std::string("]");
case TOKEN_LCURLY: return std::string("{");
case TOKEN_RCURLY: return std::string("}");
case TOKEN_TRUE: return std::string("TRUE t");
case TOKEN_FALSE: return std::string("FALSE f");
}
throw std::logic_error("Unhandled token type");
}
/** Output function for a given token. */
friend std::ostream& operator<<(std::ostream& out, const Token& token) {
out << "<" << token.typeAsString(token.kind) << "> ";
if (token.kind == TOKEN_INT) {
out << token.vInteger;
} else {
out << token.vString;
}
out << " (" << token.line << "," << token.col << ")";
return out;
}
};
/** Constructor for a lexer, reading from the given input stream. */
HOALexer(std::istream& in)
: in(in), line(1), col(0), ch(0) {
// The headers we know
knownHeaders["HOA:"] = TOKEN_HOA;
knownHeaders["State:"] = TOKEN_STATE;
knownHeaders["States:"] = TOKEN_STATES;
knownHeaders["Start:"] = TOKEN_START;
knownHeaders["AP:"] = TOKEN_AP;
knownHeaders["Alias:"] = TOKEN_ALIAS;
knownHeaders["Acceptance:"] = TOKEN_ACCEPTANCE;
knownHeaders["acc-name:"] = TOKEN_ACCNAME;
knownHeaders["tool:"] = TOKEN_TOOL;
knownHeaders["name:"] = TOKEN_NAME;
knownHeaders["properties:"] = TOKEN_PROPERTIES;
}
/** Get the next token from the input stream. */
Token nextToken() {
// first, skip any whitespace
skip();
if (ch == EOF) return Token(TOKEN_EOF, line, col);
// handle the simple syntactic elements
switch (ch) {
case '!': return Token(TOKEN_NOT, line, col);
case '&': return Token(TOKEN_AND, line, col);
case '|': return Token(TOKEN_OR, line, col);
case '(': return Token(TOKEN_LPARENTH, line, col);
case ')': return Token(TOKEN_RPARENTH, line, col);
case '[': return Token(TOKEN_LBRACKET, line, col);
case ']': return Token(TOKEN_RBRACKET, line, col);
case '{': return Token(TOKEN_LCURLY, line, col);
case '}': return Token(TOKEN_RCURLY, line, col);
}
// remember where the token began
unsigned int lineStart = line;
unsigned int colStart = col;
// handle --XYZ-- style markers
if (ch == '-') {
unsigned int index=0;
bool canBeAbort = true;
bool canBeBody = true;
bool canBeEnd = true;
std::string abort("-ABORT--");
std::string body("-BODY--");
std::string end("-END--");
while (canBeAbort || canBeBody || canBeEnd) {
nextChar();
if (ch == EOF) {throw error("Premature end-of-file inside token", lineStart, colStart);}
if (canBeAbort && ch == abort.at(index)) {
if (index == abort.length()-1) {
return Token(TOKEN_ABORT, lineStart, colStart);
}
} else {
canBeAbort=false;
}
if (canBeBody && ch == body.at(index)) {
if (index == body.length()-1) {
return Token(TOKEN_BODY, lineStart, colStart);
}
} else {
canBeBody=false;
}
if (canBeEnd && ch == end.at(index)) {
if (index == end.length()-1) {
return Token(TOKEN_END, lineStart, colStart);
}
} else {
canBeEnd=false;
}
index++;
if (index >= abort.length()) canBeAbort = false;
if (index >= body.length()) canBeBody = false;
if (index >= end.length()) canBeEnd = false;
}
throw error("Lexical error: For token starting with '-', expected either '--BODY--', '--END--' or '--ABORT--'", lineStart, colStart);
}
// handle quoted strings
if (ch == '"') {
std::string text(1, (char)ch);
bool last_was_quote = false;
while (true) {
nextChar();
if (ch == EOF) {throw error("Premature end-of-file in quoted string", lineStart, colStart);}
text+=(char)ch;
if (ch == '"' && !last_was_quote) break;
if (ch == '\\' && !last_was_quote) {
last_was_quote = true;
} else {
last_was_quote = false;
}
}
return Token(TOKEN_STRING, text, lineStart, colStart);
}
// handle integers
if (ch >= '0' && ch <= '9') {
std::string text(1, (char)ch);
while (true) {
int next = peekChar();
if (next >= '0' && next <= '9') {
nextChar();
text+=(char)ch;
} else {
break;
}
}
if (text.at(0)=='0' && text.length() > 1) {
throw error("Syntax error parsing integer, starts with 0: "+text, lineStart, colStart);
}
try {
unsigned int vInteger = std::stoi(text);
return Token(vInteger, lineStart, colStart);
} catch (std::invalid_argument& e) {
throw error("Syntax error: "+text+" is not an integer", lineStart, colStart);
} catch (std::out_of_range& e) {
throw error("Syntax error: integer "+text+" is too big to represent as an unsigned int", lineStart, colStart);
}
} else if (ch == '@' || ch == '_' || (ch >= 'a' && ch <= 'z') || (ch >= 'A' && ch <= 'Z')) {
// handle identifiers, @alias-names, headers, t and f
std::string text(1, (char)ch);
bool alias = (ch == '@');
while (true) {
int next = peekChar();
if (next == EOF) break;
if (next == ':') {
if (alias) break;
// consume ':'
nextChar();
text+=':';
break;
}
if (next == '_' ||
next == '-' ||
(next >= 'a' && next <= 'z') ||
(next >= 'A' && next <= 'Z') ||
(next >= '0' && next <= '9')) {
nextChar();
text+=(char)ch;
continue;
} else {
break;
}
}
if (alias) {
return Token(TOKEN_ALIAS_NAME, text, lineStart, colStart);
}
if (text.back() == ':') {
auto it = knownHeaders.find(text);
if (it != knownHeaders.end()) {
return Token((*it).second, text, lineStart, colStart);
}
return Token(TOKEN_HEADER_NAME, text, lineStart, colStart);
}
if (text == "t") {
return Token(TOKEN_TRUE, text, lineStart, colStart);
} else if (text == "f") {
return Token(TOKEN_FALSE, text, lineStart, colStart);
}
return Token(TOKEN_IDENT, text, lineStart, colStart);
}
throw error("Syntax error, illegal character '"+std::string(1, (char)ch)+"'", lineStart, colStart);
}
private:
/** Skip whitespace. */
void skip() {
while (true) {
nextChar();
if (ch == EOF) { // EOF
return;
}
if (ch == '/') {
skipComment();
continue;
}
if (ch == ' ' || ch == '\t') {
continue;
}
if (ch == '\n' || ch == '\r') {
line++;
col=0;
continue;
}
break;
}
}
/** Skip a comment */
void skipComment() {
nextChar();
if (ch != '*') {
throw error("Malformed start of comment", line, col);
}
bool last_was_slash = false;
bool last_was_star = false;
unsigned int nesting = 0;
while (true) {
nextChar();
if (ch == EOF) {throw error("End-of-file inside comment", line, col);}
if (ch == '\n' || ch == '\r') {
line++;
col=0;
last_was_slash = false;
last_was_star = false;
continue;
}
if (ch == '/') {
if (last_was_star) {
if (nesting == 0) {
return;
} else {
nesting--;
}
} else {
last_was_slash = true;
}
continue;
}
if (ch == '*') {
if (last_was_slash) {
nesting++;
} else {
last_was_star = true;
continue;
}
}
last_was_slash = false;
last_was_star = false;
}
}
/** Read the next char in the input stream, store in `ch` */
void nextChar() {
ch = in.get();
if (ch != EOF) {
col++;
}
}
/** Peek at the next char in the input stream without consuming */
int peekChar() {
return in.peek();
}
/**
* Construct a HOAParserExeption for a lexer error.
* @param msg the error message
* @param errLine the line number where the error occured
* @param errCol column number where the error occured
*/
HOAParserException error(const std::string& msg, unsigned int errLine, unsigned int errCol) {
return HOAParserException(msg+" (at line "+std::to_string(errLine)+", col "+std::to_string(errCol)+")", errLine, errCol);
}
private:
/** The input stream */
std::istream& in;
/** The current line number */
unsigned int line;
/** The current column number */
unsigned int col;
/** The current character (or EOF) */
int ch;
/** A map for mapping the known header names to the corresponding token types */
std::map<std::string, TokenType> knownHeaders;
};
}
#endif

692
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_parser.hh
View File

@ -0,0 +1,692 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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_HOAPARSER_H
#define CPPHOAFPARSER_HOAPARSER_H
#include <set>
#include <string>
#include <sstream>
#include "cpphoafparser/parser/hoa_lexer.hh"
#include "cpphoafparser/consumer/hoa_consumer.hh"
#include "cpphoafparser/consumer/hoa_intermediate_check_validity.hh"
#include "cpphoafparser/consumer/hoa_intermediate_resolve_aliases.hh"
#include "cpphoafparser/parser/hoa_parser_exception.hh"
/** @mainpage cpphoafparser API documentation
*
* API documentation for the <a href="http://automata.tools/hoa/cpphoafparser/">cpphoafparser</a> library.
*/
/** @namespace cpphoafparser
* The `cpphoafparser` namespace contains all the classes of the
* cpphoafparser library.
*/
namespace cpphoafparser {
/**
* Parser class for parsing HOA files.
*
* Provides a static function for parsing a HOA automaton from an input stream,
* calling into a HOAConsumer for every syntax element encountered during the parse.
*
* The parser is implemented as a simple, hand-written recursive-descent parser,
* with functions corresponding to grammar rules.
**/
class HOAParser {
public:
/**
* Function for parsing a single HOA automaton.
*
* On error, will throw HOAParserException, the consumers will generally throw
* HOAConsumerException.
*
* @param in std::istream from which the automaton will be read
* @param consumer a shared_ptr to the HOAConsumer whose functions will
* be called for each element of the HOA automaton
* @param check_validity Should the validity of the HOA be checked?
* These are checks beyond the basic syntactic well-formedness guaranteed by the grammar.
**/
static void parse(std::istream& in, HOAConsumer::ptr consumer, bool check_validity=true) {
if (consumer->parserResolvesAliases()) {
consumer.reset(new HOAIntermediateResolveAliases(consumer));
}
if (check_validity) {
consumer.reset(new HOAIntermediateCheckValidity(consumer));
}
HOAParser parser(in, consumer);
parser.nextToken();
parser.Automaton();
}
private:
/** The registered consumer */
HOAConsumer::ptr consumer;
/** The lexer for tokenizing the input stream */
HOALexer lexer;
/** The current token */
HOALexer::Token token;
/** true if we are currently in a State: definition */
bool inState;
/** the index of the current state*/
unsigned int currentState;
/** true if the current state has state labeling */
bool currentStateHasStateLabel;
/** Private constructor. */
HOAParser(std::istream& in, HOAConsumer::ptr consumer) :
consumer(consumer), lexer(in), inState(false), currentState(0), currentStateHasStateLabel(false) {
}
/** Advance to the next token. Handles TOKEN_ABORT */
void nextToken() {
token = lexer.nextToken();
if (token.kind == HOALexer::TOKEN_ABORT) {
consumer->notifyAbort();
throw "aborted";
}
}
/** Advances to the next token if it is of the expected kind, otherwise throw an error. */
void expect(HOALexer::TokenType kind, const std::string& context="") {
if (token.kind != kind) {
throw error(HOALexer::Token::forErrorMessage(kind), context);
}
// eat token
nextToken();
}
/**
* Constructs a HOAParserExeption for a syntax error.
* @param expectedTokenTypes a string detailing which token types were expected
* @param context optionally, some context for the error message */
HOAParserException error(const std::string& expectedTokenTypes, const std::string& context="") {
std::stringstream ss;
ss << "Syntax error";
if (context != "") {
ss << " (while reading " << context << ")";
}
ss << ": Expected " << expectedTokenTypes;
ss << ", got " << HOALexer::Token::forErrorMessage(token);
ss << " (line " << std::to_string(token.line) << ", col " << std::to_string(token.col) << ")";
return HOAParserException(ss.str(), token.line, token.col);
}
/** Grammar rule for the whole Automaton */
void Automaton() {
Header();
expect(HOALexer::TOKEN_BODY);
consumer->notifyBodyStart();
Body();
expect(HOALexer::TOKEN_END);
if (inState) {
consumer->notifyEndOfState(currentState);
}
consumer->notifyEnd();
}
/** Grammar rule for the HOA header */
void Header() {
Format();
HeaderItems();
}
/** Grammar rule for the HOA: header */
void Format() {
expect(HOALexer::TOKEN_HOA);
std::string version = Identifier("version");
// TODO: check format version
consumer->notifyHeaderStart(version);
}
/** Grammar rule for the remaining header items, returns if there are not more headers */
void HeaderItems() {
while (true) {
switch (token.kind) {
case HOALexer::TOKEN_STATES: HeaderItemStates(); break;
case HOALexer::TOKEN_START: HeaderItemStart(); break;
case HOALexer::TOKEN_AP: HeaderItemAP(); break;
case HOALexer::TOKEN_ALIAS: HeaderItemAlias(); break;
case HOALexer::TOKEN_ACCEPTANCE: HeaderItemAcceptance(); break;
case HOALexer::TOKEN_ACCNAME: HeaderItemAccName(); break;
case HOALexer::TOKEN_TOOL: HeaderItemTool(); break;
case HOALexer::TOKEN_NAME: HeaderItemName(); break;
case HOALexer::TOKEN_PROPERTIES: HeaderItemProperties(); break;
case HOALexer::TOKEN_HEADER_NAME: HeaderMiscItem(); break;
default:
// not a header, return
return;
}
}
}
/** Grammar rule for the States-header */
void HeaderItemStates() {
expect(HOALexer::TOKEN_STATES);
unsigned int states = Integer("number of states in States-header");
consumer->setNumberOfStates(states);
}
/** Grammar rule for the Start-header */
void HeaderItemStart() {
expect(HOALexer::TOKEN_START);
std::vector<unsigned int> stateConjunction;
unsigned int state = Integer("Start: index of start state");
stateConjunction.push_back(state);
while (token.kind == HOALexer::TOKEN_AND) {
expect(HOALexer::TOKEN_AND);
state = Integer("Start: index of start state in conjunction");
stateConjunction.push_back(state);
}
consumer->addStartStates(stateConjunction);
}
/** Grammar rule for the AP-header */
void HeaderItemAP() {
expect(HOALexer::TOKEN_AP);
unsigned int apCount = Integer("AP: number of atomic propositions");
std::vector<std::string> apList;
std::set<std::string> aps;
while (token.kind == HOALexer::TOKEN_STRING) {
std::string ap = QuotedString();
if (aps.find(ap) != aps.end()) {
throw HOAConsumerException("Atomic proposition \""+ap+"\" is a duplicate!");
}
aps.insert(ap);
apList.push_back(ap);
}
if (apList.size() != apCount) {
throw HOAConsumerException("Number of provided APs (" + std::to_string(apList.size()) + ") does not match number of APs that was specified (" + std::to_string(apCount) + ")");
}
consumer->setAPs(apList);
}
/** Grammar rule for the Alias-header */
void HeaderItemAlias() {
expect(HOALexer::TOKEN_ALIAS);
std::string aliasName = AliasName();
HOAConsumer::label_expr::ptr labelExpr = LabelExpr();
consumer->addAlias(aliasName, labelExpr);
}
/** Grammar rule for the Acceptance-header */
void HeaderItemAcceptance() {
expect(HOALexer::TOKEN_ACCEPTANCE);
unsigned int numberOfSets = Integer("Acceptance: number of acceptance sets");
HOAConsumer::acceptance_expr::ptr accExpr = AcceptanceCondition();
consumer->setAcceptanceCondition(numberOfSets, accExpr);
}
/** Grammar rule for the acc-name-header */
void HeaderItemAccName() {
expect(HOALexer::TOKEN_ACCNAME);
std::string accName = Identifier("acceptance name");
std::vector<IntOrString> extraInfo;
while (true) {
if (token.kind == HOALexer::TOKEN_IDENT) {
extraInfo.push_back(IntOrString(Identifier()));
} else if (token.kind == HOALexer::TOKEN_INT) {
extraInfo.push_back(IntOrString(Integer()));
} else if (token.kind == HOALexer::TOKEN_TRUE) {
extraInfo.push_back(IntOrString("t"));
expect(HOALexer::TOKEN_TRUE); // munch
} else if (token.kind == HOALexer::TOKEN_FALSE) {
extraInfo.push_back(IntOrString("f"));
expect(HOALexer::TOKEN_FALSE); // munch
} else {
break;
}
// TODO
// if (settings == null || !settings.getFlagIgnoreAccName()) {
// consumer.provideAcceptanceName(accName, extraInfo);
//}
}
consumer->provideAcceptanceName(accName, extraInfo);
}
/** Grammar rule for the tool-header */
void HeaderItemTool() {
expect(HOALexer::TOKEN_TOOL);
std::string tool = QuotedString();
std::shared_ptr<std::string> version;
if (token.kind == HOALexer::TOKEN_STRING) {
version.reset(new std::string(QuotedString()));
}
consumer->setTool(tool, version);
}
/** Grammar rule for the name-header */
void HeaderItemName() {
expect(HOALexer::TOKEN_NAME);
std::string name = QuotedString();
consumer->setName(name);
}
/** Grammar rule for the properties-header */
void HeaderItemProperties() {
expect(HOALexer::TOKEN_PROPERTIES);
std::vector<std::string> properties;
while (true) {
if (token.kind == HOALexer::TOKEN_IDENT) {
std::string property = Identifier();
properties.push_back(property);
} else if (token.kind == HOALexer::TOKEN_TRUE) {
// t does not have the special boolean meaning here, back to string
properties.push_back("t");
expect(HOALexer::TOKEN_TRUE); // eat
} else if (token.kind == HOALexer::TOKEN_FALSE) {
// f does not have the special boolean meaning here, back to string
properties.push_back("f");
expect(HOALexer::TOKEN_FALSE); // eat
} else {
// no more properties...
break;
}
}
consumer->addProperties(properties);
}
/** Grammar rule for a misc header (not known from the format specification) */
void HeaderMiscItem() {
std::string headerName = token.vString;
headerName = headerName.substr(0, headerName.length()-1);
expect(HOALexer::TOKEN_HEADER_NAME);
std::vector<IntOrString> content;
while (true) {
if (token.kind == HOALexer::TOKEN_INT) {
content.push_back(Integer());
} else if (token.kind == HOALexer::TOKEN_IDENT) {
content.push_back(Identifier());
} else if (token.kind == HOALexer::TOKEN_STRING) {
content.push_back(IntOrString(QuotedString(), true));
} else if (token.kind == HOALexer::TOKEN_TRUE) {
// t does not have the special boolean meaning here, back to string
content.push_back(IntOrString("t", false));
expect(HOALexer::TOKEN_TRUE); // eat
} else if (token.kind == HOALexer::TOKEN_FALSE) {
// f does not have the special boolean meaning here, back to string
content.push_back(IntOrString("f", false));
expect(HOALexer::TOKEN_FALSE); // eat
} else {
break;
}
}
consumer->addMiscHeader(headerName, content);
}
/** Grammar rule for the automaton body */
void Body() {
while (true) {
switch (token.kind) {
case HOALexer::TOKEN_STATE:
StateName();
break;
case HOALexer::TOKEN_END:
return;
case HOALexer::TOKEN_EOF:
return;
default:
if (inState) {
Edge();
} else {
throw error("either State: or --END--");
}
}
}
}
/** Grammar rule for the State definition */
void StateName() {
expect(HOALexer::TOKEN_STATE);
HOAConsumer::label_expr::ptr labelExpr;
std::shared_ptr<std::string> stateComment;
std::shared_ptr<HOAConsumer::int_list> accSignature;
if (token.kind == HOALexer::TOKEN_LBRACKET) {
labelExpr = Label();
}
unsigned int state = Integer(); // name of the state
if (token.kind == HOALexer::TOKEN_STRING) {
stateComment.reset(new std::string(QuotedString())); // state comment
}
if (token.kind == HOALexer::TOKEN_LCURLY) {
accSignature = AcceptanceSignature();
}
if (inState) {
consumer->notifyEndOfState(currentState);
}
consumer->addState(state, stateComment, labelExpr, accSignature);
// store global information:
inState = true;
currentState = state;
currentStateHasStateLabel = (bool)(labelExpr);
}
/** Grammar rule for an automaton edge */
void Edge() {
HOAConsumer::label_expr::ptr labelExpr;
std::shared_ptr<HOAConsumer::int_list> conjStates;
std::shared_ptr<HOAConsumer::int_list> accSignature;
if (token.kind == HOALexer::TOKEN_LBRACKET) {
labelExpr = Label();
}
conjStates = StateConjunction("edge");
if (token.kind == HOALexer::TOKEN_LCURLY) {
accSignature = AcceptanceSignature();
}
if (labelExpr || currentStateHasStateLabel) {
consumer->addEdgeWithLabel(currentState, labelExpr, *conjStates, accSignature);
} else {
consumer->addEdgeImplicit(currentState, *conjStates, accSignature);
}
}
/**
* Grammar rule for a state conjunction
* @param context contextual information for error messages
*/
std::shared_ptr<HOAConsumer::int_list> StateConjunction(const std::string& context) {
std::shared_ptr<HOAConsumer::int_list> stateConjunction (new HOAConsumer::int_list());
unsigned int state = Integer(context);
stateConjunction->push_back(state);
while (token.kind == HOALexer::TOKEN_AND) {
expect(HOALexer::TOKEN_AND);
state = Integer(context);
stateConjunction->push_back(state);
}
return stateConjunction;
}
/** Grammar rule for a [label-expr] */
HOAConsumer::label_expr::ptr Label() {
HOAConsumer::label_expr::ptr result;
expect(HOALexer::TOKEN_LBRACKET);
result = LabelExpr();
expect(HOALexer::TOKEN_RBRACKET);
return result;
}
/** Grammar rule for an acceptance signature */
std::shared_ptr<HOAConsumer::int_list> AcceptanceSignature() {
std::shared_ptr<HOAConsumer::int_list> result(new HOAConsumer::int_list());
expect(HOALexer::TOKEN_LCURLY);
while (token.kind == HOALexer::TOKEN_INT) {
unsigned int accSet = Integer();
result->push_back(accSet);
}
expect(HOALexer::TOKEN_RCURLY);
return result;
}
/** Grammar rule for an acceptance condition expression (handle disjunction)*/
HOAConsumer::acceptance_expr::ptr AcceptanceCondition() {
HOAConsumer::acceptance_expr::ptr left = AcceptanceConditionAnd();
while (token.kind == HOALexer::TOKEN_OR) {
expect(HOALexer::TOKEN_OR);
HOAConsumer::acceptance_expr::ptr right = AcceptanceConditionAnd();
left = left | right;
}
return left;
}
/** Grammar rule for conjunction in an acceptance condition */
HOAConsumer::acceptance_expr::ptr AcceptanceConditionAnd() {
HOAConsumer::acceptance_expr::ptr left = AcceptanceConditionAtom();
while (token.kind == HOALexer::TOKEN_AND) {
expect(HOALexer::TOKEN_AND);
HOAConsumer::acceptance_expr::ptr right = AcceptanceConditionAtom();
left = left & right;
}
return left;
}
/** Grammar rule for the atoms in an acceptance condition */
HOAConsumer::acceptance_expr::ptr AcceptanceConditionAtom() {
HOAConsumer::acceptance_expr::ptr result;
switch (token.kind) {
case HOALexer::TOKEN_LPARENTH:
expect(HOALexer::TOKEN_LPARENTH);
result = AcceptanceCondition();
expect(HOALexer::TOKEN_RPARENTH);
return result;
case HOALexer::TOKEN_TRUE:
expect(HOALexer::TOKEN_TRUE);
result.reset(new HOAConsumer::acceptance_expr(true));
return result;
case HOALexer::TOKEN_FALSE:
expect(HOALexer::TOKEN_FALSE);
result.reset(new HOAConsumer::acceptance_expr(false));
return result;
case HOALexer::TOKEN_IDENT:
result.reset(new HOAConsumer::acceptance_expr(AcceptanceConditionTemporalOperator()));
return result;
default:
throw error("acceptance condition");
}
}
/** Grammar rule for a temporal operator (Fin/Inf) in an acceptance condition */
AtomAcceptance::ptr AcceptanceConditionTemporalOperator() {
AtomAcceptance::AtomType atomType = AtomAcceptance::TEMPORAL_FIN;
bool negated = false;
unsigned int accSetIndex;
std::string temporalOperator = Identifier();
if (temporalOperator == "Fin") {
atomType = AtomAcceptance::TEMPORAL_FIN;
} else if (temporalOperator == "Inf") {
atomType = AtomAcceptance::TEMPORAL_INF;
} else {
throw error("either 'Fin' or 'Inf'", "acceptance condition");
}
expect(HOALexer::TOKEN_LPARENTH, "acceptance condition");
if (token.kind == HOALexer::TOKEN_NOT) {
expect(HOALexer::TOKEN_NOT);
negated = true;
}
accSetIndex = Integer("acceptance set index");
expect(HOALexer::TOKEN_RPARENTH, "acceptance condition");
return AtomAcceptance::ptr(new AtomAcceptance(atomType, accSetIndex, negated));
}
/** Grammar rule for a label expression (handle disjunction) */
HOAConsumer::label_expr::ptr LabelExpr() {
HOAConsumer::label_expr::ptr left = LabelExprAnd();
while (token.kind == HOALexer::TOKEN_OR) {
expect(HOALexer::TOKEN_OR);
HOAConsumer::label_expr::ptr right = LabelExprAnd();
left = left | right;
}
return left;
}
/** Grammar rule for a label expression (handle conjunction) */
HOAConsumer::label_expr::ptr LabelExprAnd() {
HOAConsumer::label_expr::ptr left = LabelExprAtom();
while (token.kind == HOALexer::TOKEN_AND) {
expect(HOALexer::TOKEN_AND);
HOAConsumer::label_expr::ptr right = LabelExprAtom();
left = left & right;
}
return left;
}
/** Grammar rule for a label expression (handle atoms) */
HOAConsumer::label_expr::ptr LabelExprAtom() {
HOAConsumer::label_expr::ptr result;
switch (token.kind) {
case HOALexer::TOKEN_LPARENTH:
expect(HOALexer::TOKEN_LPARENTH);
result = LabelExpr();
expect(HOALexer::TOKEN_RPARENTH);
return result;
case HOALexer::TOKEN_TRUE:
expect(HOALexer::TOKEN_TRUE);
result.reset(new HOAConsumer::label_expr(true));
return result;
case HOALexer::TOKEN_FALSE:
expect(HOALexer::TOKEN_FALSE);
result.reset(new HOAConsumer::label_expr(false));
return result;
case HOALexer::TOKEN_NOT:
expect(HOALexer::TOKEN_NOT);
result = LabelExprAtom();
return !result;
case HOALexer::TOKEN_INT: {
unsigned int apIndex = Integer();
result.reset(new HOAConsumer::label_expr(AtomLabel::createAPIndex(apIndex)));
return result;
}
case HOALexer::TOKEN_ALIAS_NAME: {
std::string aliasName = AliasName();
result.reset(new HOAConsumer::label_expr(AtomLabel::createAlias(aliasName)));
return result;
}
default:
throw error("label expression");
}
}
/** Grammar rule for a quoted string */
std::string QuotedString(const std::string& context="") {
if (token.kind != HOALexer::TOKEN_STRING) {
expect(HOALexer::TOKEN_STRING, context);
}
std::string result = token.vString;
// eat token
nextToken();
result = HOAParserHelper::unquote(result);
return result;
}
/** Grammar rule for a HOA identifier */
std::string Identifier(const std::string& context="") {
if (token.kind != HOALexer::TOKEN_IDENT) {
expect(HOALexer::TOKEN_IDENT, context);
}
std::string result = token.vString;
// eat token
nextToken();
return result;
}
/** Grammar rule for an @@alias-name. Returns the name without the leading @@. */
std::string AliasName() {
if (token.kind != HOALexer::TOKEN_ALIAS_NAME) {
expect(HOALexer::TOKEN_ALIAS_NAME);
}
std::string result = token.vString;
// eat token
nextToken();
// eat @
result = result.substr(1);
return result;
}
/** Grammar rule for an unsigned integer */
unsigned int Integer(const std::string& context="") {
if (token.kind != HOALexer::TOKEN_INT) {
expect(HOALexer::TOKEN_INT, context);
}
unsigned int result = token.vInteger;
// eat token
nextToken();
return result;
}
};
}
#endif

58
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_parser_exception.hh
View File

@ -0,0 +1,58 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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_HOAPARSEREXCEPTION_H
#define CPPHOAFPARSER_HOAPARSEREXCEPTION_H
#include <stdexcept>
namespace cpphoafparser {
/** Exception thrown to indicate an error during parsing, mostly for syntax errors. */
class HOAParserException : public std::runtime_error {
public:
/** Constructor for simple error message. */
HOAParserException(const std::string& what) :
std::runtime_error(what), hasLocation(false), line(0), col(0) {}
/** Constructor for error message with location (line/column) information. */
HOAParserException(const std::string& what, int line, int col) :
std::runtime_error(what), hasLocation(true), line(line), col(col) {}
private:
/** True if we have location information */
bool hasLocation;
/** The line number */
unsigned int line;
/** The column number */
unsigned int col;
};
}
#endif

122
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/parser/hoa_parser_helper.hh
View File

@ -0,0 +1,122 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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_HOAPARSERHELPER_H
#define CPPHOAFPARSER_HOAPARSERHELPER_H
#include <iostream>
#include <string>
#include <sstream>
#include "cpphoafparser/parser/hoa_parser_exception.hh"
namespace cpphoafparser {
/** Helper function for dealing with quoted strings */
class HOAParserHelper {
public:
/**
* Outputs a quoted version of the string to the ostream.
* The string is quoted to conform the to double-quoted
* string syntax of the HOA format.
*/
static void print_quoted(std::ostream& out, const std::string& s) {
std::string::size_type pos = s.find_first_of("\\\""); // find next \ or "
if (pos == std::string::npos) {
// nothing to quote
out << "\"" << s << "\"";
return;
}
out << "\"";
std::string::size_type last_pos = 0;
do {
out << s.substr(last_pos, pos); // characters that don't need to be quoted
out << "\\"; // add quote
out << s.substr(pos,1); // add character
last_pos = pos+1;
pos = s.find_first_of("\\\"", last_pos); // find next \ or "
} while (pos != std::string::npos);
if (last_pos < s.length()) {
out << s.substr(last_pos); // remaining
}
out << "\"";
}
/** Returns a double-quoted version of the string (HOA syntax and quoting rules). */
static std::string quote(const std::string& s) {
std::stringstream ss;
print_quoted(ss, s);
return ss.str();
}
/**
* Performs unquoting of a double-quoted string (HOA syntax and quoting rules).
* If the string is not a validly quoted string, a HOAParserException is thrown.
* @returns the unquoted string
**/
static std::string unquote(const std::string& s) {
if (s.length() == 0 || s.at(0) != '"') {
throw HOAParserException("String not quoted : " + s);
}
if (s.back() != '"') {
throw HOAParserException("String does not end with quote: " + s);
}
std::string::size_type pos = s.find_first_of("\\", 1); // find first '\'
if (pos == std::string::npos) {
// nothing to unquote, just remove outer quotes
return s.substr(1, s.length()-2);
}
std::stringstream ss;
std::string::size_type last_pos = 1;
do {
ss << s.substr(last_pos, pos); // characters that don't need to be quoted
if (pos+1 >= s.length()) {
throw HOAParserException("String ends with \\ character: s");
}
ss << s.substr(pos+1,1); // the quoted character
last_pos = pos+2; // skip quote character
pos = s.find_first_of("\\\"", last_pos); // find next '\'
} while (pos != std::string::npos);
if (last_pos < s.length()-1) {
ss << s.substr(last_pos, s.length()-1-last_pos); // remaining
}
return ss.str();
}
};
}
#endif

77
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/util/acceptance_repository.hh
View File

@ -0,0 +1,77 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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_ACCEPTANCEREPOSITORY_H
#define CPPHOAFPARSER_ACCEPTANCEREPOSITORY_H
#include <stdexcept>
#include <memory>
#include "cpphoafparser/consumer/hoa_consumer.hh"
namespace cpphoafparser {
/**
* Virtual base class defining the interface to a repository of known acceptance names.
* This can be used to construct the canonical acceptance expression for a given acc-name header,
* i.e., the acceptance name (with the extra parameters) for known acceptance names.
*/
class AcceptanceRepository
{
public:
/** A shared_ptr wrapping an AcceptanceRepository */
typedef std::shared_ptr<AcceptanceRepository> ptr;
/** An acceptance condition expression */
typedef HOAConsumer::acceptance_expr acceptance_expr;
/** This exception is thrown if the extra arguments of an acc-name are malformed */
class IllegalArgumentException : public std::runtime_error {
public:
/** Constructor */
IllegalArgumentException(const std::string& s) : std::runtime_error(s) {}
};
/** Destructor */
virtual ~AcceptanceRepository() {}
/**
* For a given acc-name header, construct the corresponding canonical acceptance expression.
* If the acc-name is not known, returns an empty pointer.
*
* @param accName the acceptance name, as passed in an acc-name header
* @param extraInfo extra info, as passed in an acc-name header
* @return the canonical acceptance expression for this name, empty pointer if not known
* @throws IllegalParameterException if the acceptance name is known, but there is an error with the extraInfo
*/
virtual acceptance_expr::ptr getCanonicalAcceptanceExpression(const std::string& accName, const std::vector<IntOrString>& extraInfo) = 0;
};
}
#endif

388
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/util/acceptance_repository_standard.hh
View File

@ -0,0 +1,388 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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_ACCEPTANCEREPOSITORYSTANDARD_H
#define CPPHOAFPARSER_ACCEPTANCEREPOSITORYSTANDARD_H
#include "cpphoafparser/util/acceptance_repository.hh"
namespace cpphoafparser {
/**
* An acceptance repository with all the acceptance conditions specified
* in the format specification.
*/
class AcceptanceRepositoryStandard : public AcceptanceRepository
{
public:
/**
* @name acc-name constants
* String constants for the various acceptance condition names */
/**@{*/
const char* ACC_ALL = "all";
const char* ACC_NONE = "none";
const char* ACC_BUCHI = "Buchi";
const char* ACC_COBUCHI = "coBuchi";
const char* ACC_GENERALIZED_BUCHI = "generalized-Buchi";
const char* ACC_GENERALIZED_COBUCHI = "generalized-coBuchi";
const char* ACC_RABIN = "Rabin";
const char* ACC_STREETT = "Streett";
const char* ACC_GENERALIZED_RABIN = "generalized-Rabin";
const char* ACC_PARITY = "parity";
/**@}*/
virtual acceptance_expr::ptr getCanonicalAcceptanceExpression(const std::string& accName,
const std::vector<IntOrString>& extraInfo) override {
if (accName == ACC_ALL)
return forAll(extraInfo);
if (accName == ACC_NONE)
return forNone(extraInfo);
if (accName == ACC_BUCHI)
return forBuchi(extraInfo);
if (accName == ACC_COBUCHI)
return forCoBuchi(extraInfo);
if (accName == ACC_GENERALIZED_BUCHI)
return forGenBuchi(extraInfo);
if (accName == ACC_GENERALIZED_COBUCHI)
return forGenCoBuchi(extraInfo);
if (accName == ACC_RABIN)
return forRabin(extraInfo);
if (accName == ACC_STREETT)
return forStreett(extraInfo);
if (accName == ACC_GENERALIZED_RABIN)
return forGeneralizedRabin(extraInfo);
if (accName == ACC_PARITY)
return forParity(extraInfo);
return acceptance_expr::ptr();
}
/** Construct canonical acceptance condition for 'all' */
acceptance_expr::ptr forAll(const std::vector<IntOrString>& extraInfo) {
checkNumberOfArguments(ACC_ALL, extraInfo, 0);
return acceptance_expr::True();
}
/** Construct canonical acceptance condition for 'none' */
acceptance_expr::ptr forNone(const std::vector<IntOrString>& extraInfo) {
checkNumberOfArguments(ACC_ALL, extraInfo, 0);
return acceptance_expr::False();
}
/** Construct canonical acceptance condition for 'Buchi' */
acceptance_expr::ptr forBuchi(const std::vector<IntOrString>& extraInfo) {
checkNumberOfArguments(ACC_BUCHI, extraInfo, 0);
return acceptance_expr::Atom(AtomAcceptance::Inf(0));
}
/** Construct canonical acceptance condition for 'coBuchi' */
acceptance_expr::ptr forCoBuchi(const std::vector<IntOrString>& extraInfo) {
checkNumberOfArguments(ACC_COBUCHI, extraInfo, 0);
return acceptance_expr::Atom(AtomAcceptance::Fin(0));
}
/** Construct canonical acceptance condition for 'generalized-Buchi' */
acceptance_expr::ptr forGenBuchi(const std::vector<IntOrString>& extraInfo) {
checkNumberOfArguments(ACC_GENERALIZED_BUCHI, extraInfo, 1);
unsigned int numberOfInf = extraInfoToIntegerList(ACC_GENERALIZED_BUCHI, extraInfo).at(0);
if (numberOfInf == 0) {
return acceptance_expr::True();
}
acceptance_expr::ptr result;
for (unsigned int i = 0; i < numberOfInf; i++) {
acceptance_expr::ptr inf = acceptance_expr::Atom(AtomAcceptance::Inf(i));
if (i == 0) {
result = inf;
} else {
result = result & inf;
}
}
return result;
}
/** Construct canonical acceptance condition for 'generalized-co-Buchi' */
acceptance_expr::ptr forGenCoBuchi(const std::vector<IntOrString>& extraInfo) {
checkNumberOfArguments(ACC_GENERALIZED_COBUCHI, extraInfo, 1);
unsigned int numberOfFin = extraInfoToIntegerList(ACC_GENERALIZED_COBUCHI, extraInfo).at(0);
if (numberOfFin == 0) {
return acceptance_expr::False();
}
acceptance_expr::ptr result;
for (unsigned int i = 0; i < numberOfFin; i++) {
acceptance_expr::ptr fin = acceptance_expr::Atom(AtomAcceptance::Fin(i));
if (i == 0) {
result = fin;
} else {
result = result & fin;
}
}
return result;
}
/** Construct canonical acceptance condition for 'Rabin' */
acceptance_expr::ptr forRabin(const std::vector<IntOrString>& extraInfo) {
checkNumberOfArguments(ACC_RABIN, extraInfo, 1);
unsigned int numberOfPairs = extraInfoToIntegerList(ACC_RABIN, extraInfo).at(0);
if (numberOfPairs == 0) {
return acceptance_expr::False();
}
acceptance_expr::ptr result;
for (unsigned int i = 0; i < numberOfPairs; i++) {
acceptance_expr::ptr fin = acceptance_expr::Atom(AtomAcceptance::Fin(2*i));
acceptance_expr::ptr inf = acceptance_expr::Atom(AtomAcceptance::Inf(2*i+1));
acceptance_expr::ptr pair = fin & inf;
if (i == 0) {
result = pair;
} else {
result = result | pair;
}
}
return result;
}
/** Construct canonical acceptance condition for 'Streett' */
acceptance_expr::ptr forStreett(const std::vector<IntOrString>& extraInfo) {
checkNumberOfArguments(ACC_STREETT, extraInfo, 1);
unsigned int numberOfPairs = extraInfoToIntegerList(ACC_STREETT, extraInfo).at(0);
if (numberOfPairs == 0) {
return acceptance_expr::True();
}
acceptance_expr::ptr result;
for (unsigned int i = 0; i < numberOfPairs; i++) {
acceptance_expr::ptr fin = acceptance_expr::Atom(AtomAcceptance::Fin(2*i));
acceptance_expr::ptr inf = acceptance_expr::Atom(AtomAcceptance::Inf(2*i+1));
acceptance_expr::ptr pair = fin | inf;
if (i == 0) {
result = pair;
} else {
result = result & pair;
}
}
return result;
}
/** Construct canonical acceptance condition for 'generalized-Rabin' */
acceptance_expr::ptr forGeneralizedRabin(const std::vector<IntOrString>& extraInfo) {
std::vector<unsigned int> parameters = extraInfoToIntegerList(ACC_GENERALIZED_RABIN, extraInfo);
if (parameters.size() == 0) {
throw IllegalArgumentException(std::string("Acceptance ")+ACC_GENERALIZED_RABIN+" needs at least one argument");
}
unsigned int numberOfPairs = parameters.at(0);
if (parameters.size() != numberOfPairs + 1) {
throw IllegalArgumentException(std::string("Acceptance ")+ACC_GENERALIZED_RABIN+" with " + std::to_string(numberOfPairs) +" generalized pairs: There is not exactly one argument per pair");
}
acceptance_expr::ptr result;
int currentIndex = 0;
for (unsigned int i = 0; i < numberOfPairs; i++) {
unsigned int numberOfInf = parameters.at(i+1);
acceptance_expr::ptr fin = acceptance_expr::Atom(AtomAcceptance::Fin(currentIndex++));
acceptance_expr::ptr pair = fin;
for (unsigned int j = 0; j< numberOfInf; j++) {
acceptance_expr::ptr inf = acceptance_expr::Atom(AtomAcceptance::Inf(currentIndex++));
pair = pair & inf;
}
if (i == 0) {
result = pair;
} else {
result = result | pair;
}
}
return result;
}
/** Construct canonical acceptance condition for 'parity' */
acceptance_expr::ptr forParity(const std::vector<IntOrString>& extraInfo) {
checkNumberOfArguments(ACC_PARITY, extraInfo, 3);
bool min = false;
bool even = false;
const std::string& minMax = extraInfoToString(ACC_PARITY, extraInfo, 0);
if (minMax == "min") {
min = true;
} else if (minMax == "max") {
min = false;
} else {
throw IllegalArgumentException(std::string("For acceptance ") + ACC_PARITY +", the first argument has to be either 'min' or 'max'");
}
const std::string& evenOdd = extraInfoToString(ACC_PARITY, extraInfo, 1);
if (evenOdd == "even") {
even = true;
} else if (evenOdd == "odd") {
even = false;
} else {
throw IllegalArgumentException(std::string("For acceptance ") + ACC_PARITY +", the second argument has to be either 'even' or 'odd'");
}
unsigned int colors;
if (!(extraInfo.at(2).isInteger())) {
throw IllegalArgumentException(std::string("For acceptance ") + ACC_PARITY + ", the third argument has to be the number of colors");
}
colors = extraInfo.at(2).getInteger();
if (colors == 0) {
if ( min && even) return BooleanExpression<AtomAcceptance>::True();
if (!min && even) return BooleanExpression<AtomAcceptance>::False();
if ( min && !even) return BooleanExpression<AtomAcceptance>::False();
if (!min && !even) return BooleanExpression<AtomAcceptance>::True();
}
acceptance_expr::ptr result;
bool reversed = min;
bool infOnOdd = !even;
for (unsigned int i = 0; i < colors; i++) {
unsigned int color = (reversed ? colors-i-1 : i);
bool produceInf;
if (color % 2 == 0) {
produceInf = !infOnOdd;
} else {
produceInf = infOnOdd;
}
acceptance_expr::ptr node;
if (produceInf) {
node.reset(new BooleanExpression<AtomAcceptance>(AtomAcceptance::Inf(color)));
} else {
node.reset(new BooleanExpression<AtomAcceptance>(AtomAcceptance::Fin(color)));
}
if (result) {
if (produceInf) {
// Inf always with |
result = node | result;
} else {
// Fin always with &
result = node & result;
}
} else {
result = node;
}
}
return result;
}
private:
/**
* Convert an extra info vector to an integer list.
* @param accName the name of the acceptance condition (for error messages)
* @param extraInfo the vector
*/
std::vector<unsigned int> extraInfoToIntegerList(const std::string& accName, const std::vector<IntOrString>& extraInfo)
{
std::vector<unsigned int> result;
for (IntOrString i : extraInfo) {
if (!(i.isInteger())) {
throw IllegalArgumentException("For acceptance " + accName + ", all arguments have to be integers");
}
result.push_back(i.getInteger());
}
return result;
}
/** Extract a string from extraInfo at a given index, throw exception otherwise.
* @param accName the name of the acceptance condition (for error messages)
* @param extraInfo the vector
* @param index the index into the extraInfo vector
*/
const std::string& extraInfoToString(const std::string& accName, const std::vector<IntOrString>& extraInfo, unsigned int index) {
if (!extraInfo.at(index).isString()) {
throw IllegalArgumentException(std::string("Argument ")+std::to_string(index-1)+" for acceptance " + accName +" has to be a string!");
}
return extraInfo.at(index).getString();
}
/**
* Check that the number of arguments in the extraInfo vector is as expected.
* If that's not the case, throw an IllegalArgumentException.
* @param accName the acceptance condition name (for error message)
* @param extraInfo the extraInfo vector
* @param expectedNumberOfArguments the expected number of elements in the extraInfo vector
*/
void checkNumberOfArguments(const std::string& accName, const std::vector<IntOrString>& extraInfo, unsigned int expectedNumberOfArguments)
{
if (expectedNumberOfArguments != extraInfo.size()) {
throw IllegalArgumentException("For acceptance "
+ accName
+ ", expected "
+ std::to_string(expectedNumberOfArguments)
+ " arguments, got "
+ std::to_string(extraInfo.size()));
}
}
};
}
#endif

124
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/util/dynamic_bitset.hh
View File

@ -0,0 +1,124 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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_DYNAMICBITSET_H
#define CPPHOAFPARSER_DYNAMICBITSET_H
#include <vector>
namespace cpphoafparser {
/**
* A dynamic bitset that grows automatically.
* Inherits the functionality of std::vector<bool>, adding
* convenience functions.
**/
class dynamic_bitset : public std::vector<bool> {
public:
/**
* Set the bit at the given `index` to `value`.
* It `index` is larger than the highest set bit,
* the intermediate bits are set to `false`.
*/
void set(std::size_t index, bool value=true) {
if (index >= size()) {
resize(index+1, false);
}
at(index) = value;
}
/**
* Get the bit at the given `index`.
* If `index` is beyond the highest set bit
* then return false.
*/
bool get(std::size_t index) const {
if (index >= size()) {
return false;
}
return at(index);
}
/**
* Returns the index of the highest set bit.
* The actual return value is a pair, where the first
* element is the index of the highest set bit (if there
* are any) and the second element being false
* if there is no set bit at all.
*/
std::pair<std::size_t,bool> getHighestSetBit() const {
if (size() == 0) {
return std::make_pair(0, false);
}
for (std::size_t index = size(); index > 0; index--) {
if ((*this)[index-1]) {
return std::make_pair(index-1, true);
}
}
return std::make_pair(0, false);
}
/**
* Returns the cardinality (the number of set bits) of this
* bitset.
*/
std::size_t cardinality() const {
std::size_t result = 0;
for (bool b : *this) {
if (b) result++;
}
return result;
}
/**
* Perform andNot operator on this bitset.
* After calling this function a bit is set in this bitset
* if it was set before and if the corresponding bit in
* `other` is not set.
*/
void andNot(const dynamic_bitset& other) {
for (std::size_t index = 0; index < size() && index < other.size(); index++) {
at(index) = at(index) & !other.at(index);
}
}
/** Returns `true` if there are not set bits */
bool isEmpty() const {
for (bool b : *this) {
if (b) return false;
}
return true;
}
};
}
#endif

156
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/util/implicit_edge_helper.hh
View File

@ -0,0 +1,156 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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_IMPLICITEDGEHELPER_H
#define CPPHOAFPARSER_IMPLICITEDGEHELPER_H
#include "cpphoafparser/consumer/hoa_consumer_exception.hh"
#include <exception>
#include <string>
namespace cpphoafparser {
/**
* Helper for keeping track of implicit edges.
*
* In `notifyBodyStart()`, call:<br>
* `helper = new ImplicitEdgeHelper(numberOfAPs);`
*
* In `addState()`, call:<br>
* `helper.startOfState(stateId);`
*
* In `addEdgeImplicit()`, call:<br>
* edgeIndex = helper.nextImplicitEdge();`
*
* In `notifyEndOfState()`, call:<br>
* `helper.endOfState();`
*/
class ImplicitEdgeHelper
{
public:
/** Constructor, pass number of atomic propositions */
ImplicitEdgeHelper(unsigned int numberOfAPs) :
numberOfAPs(numberOfAPs), stateId(0)
{
edgesPerState = ((std::size_t)1) << numberOfAPs;
}
/** Return the expected number of edges per state, i.e., 2^|AP|. */
std::size_t getEdgesPerState()
{
return edgesPerState;
}
/** Notify the ImplicitEdgeHelper that a new state definition has been encountered.
* @param newStateId the state index (for error message)
* @throws std::logic_error if `startOfState()` is called before another state is finished with a call to `endOfState()
*/
void startOfState(unsigned int newStateId)
{
if (inState) {
throw std::logic_error("ImplicitEdgeHelper: startOfState("
+ std::to_string(newStateId)
+ ") without previous call to endOfState()");
}
edgeIndex = 0;
stateId = newStateId;
inState = true;
}
/** Notify the ImplicitEdgeHelper that the next implicit edge for the current state has been encountered.
* Return the edge index.
* @return the index of the current edge
* @throws HOAConsumerException if the number of edges is more than 2^numberOfAPs
* @throws std::logic_error if this function is called without a previous call to `startOfState()
* */
std::size_t nextImplicitEdge()
{
if (!inState) {
throw std::logic_error("ImplicitEdgeHelper: nextImplicitEdge() without previous call to startOfState()");
}
unsigned long currentEdgeIndex = edgeIndex;
edgeIndex++;
if (currentEdgeIndex >= edgesPerState) {
throw HOAConsumerException("For state "
+std::to_string(stateId)
+", more edges than allowed for "
+std::to_string(numberOfAPs)
+" atomic propositions");
}
return currentEdgeIndex;
}
/** Notify the ImplicitEdgeHelper that the current state definition is finished.
* Checks the number of encountered implicit edges against the expected number.
* If there are no implicit edges for the current state, that's fine as well.
* @throws HOAConsumerException if there are more then zero and less then 2^numberOfAPs edges
* @throws std::logic_error if `endOfState()` is called without previous call to `startOfState()`
*/
void endOfState()
{
if (!inState) {
throw std::logic_error("ImplicitEdgeHelper: endOfState() without previous call to startOfState()");
}
inState = false;
if (edgeIndex >0 && edgeIndex != edgesPerState) {
throw HOAConsumerException("For state "
+ std::to_string(stateId)
+ ", less edges than required for "
+ std::to_string(numberOfAPs)
+ " atomic propositions");
}
}
private:
/** The number of atomic propositions */
unsigned int numberOfAPs;
/** The index of the current edge */
std::size_t edgeIndex = 0;
/** The required number of edges per state */
std::size_t edgesPerState;
/** Are we currently in a state definition? */
bool inState = false;
/** The current state index (for error message) */
std::size_t stateId = 0;
};
}
#endif

116
resources/3rdparty/cpphoafparser-0.99.2/include/cpphoafparser/util/int_or_string.hh
View File

@ -0,0 +1,116 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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_INTORSTRING_H
#define CPPHOAFPARSER_INTORSTRING_H
#include <string>
#include <stdexcept>
#include "cpphoafparser/parser/hoa_parser_helper.hh"
namespace cpphoafparser {
/**
* Utility class for storing either an integer or a string value.
* The stored value is immutable.
*/
class IntOrString {
public:
/** Constructor for storing an integer. */
IntOrString(unsigned int vInteger) : vInteger(vInteger), vString(nullptr), wasQuoted(false) {}
/**
* Constructor for storing a string.
* @param vString the string to store
* @param wasQuoted remember that the string was originally quoted
*/
IntOrString(const std::string& vString, bool wasQuoted = false) : vInteger(0), vString(new std::string(vString)), wasQuoted(false) {}
/** Returns true if the stored value is a string */
bool isString() const {return (bool)vString;}
/** Returns true if the stored value is an integer */
bool isInteger() const {return !isString();}
/**
* Returns whether this string was originally quoted.
* May only be called if `isString() == true`.
**/
bool wasStringQuoted() const {
if (!isString()) {throw std::logic_error("Illegal access");}
return wasQuoted;
}
/**
* Returns (a const reference to) the stored string.
* May only be called if `isString() == true`.
**/
const std::string& getString() const {
if (!isString()) {throw std::logic_error("Illegal access");}
return *vString;
}
/**
* Returns the stored integer.
* May only be called if `isInteger() == true`.
**/
unsigned int getInteger() const {
if (!isInteger()) {throw std::logic_error("Illegal access");}
return vInteger;
}
/**
* Stream output operator for IntOrString.
* If the stored value is a string that is marked as having been quoted,
* will quote the string before output.
*/
friend std::ostream& operator<<(std::ostream& out, const IntOrString& intOrString) {
if (intOrString.isInteger()) {
out << intOrString.getInteger();
} else {
if (intOrString.wasQuoted) {
HOAParserHelper::print_quoted(out, intOrString.getString());
} else {
out << intOrString.getString();
}
}
return out;
}
private:
/** The stored integer value */
unsigned int vInteger;
/** The stored string value */
std::shared_ptr<std::string> vString;
/** Was this string originally quoted? */
bool wasQuoted;
};
}
#endif

15
resources/3rdparty/cpphoafparser-0.99.2/src/CMakeLists.txt
View File

@ -0,0 +1,15 @@
cmake_minimum_required(VERSION 2.6)
cmake_policy(SET CMP0054 OLD)
PROJECT( cpphoaf )
INCLUDE_DIRECTORIES("../include")
IF ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
"${CMAKE_CXX_COMPILER_ID}" STREQUAL "GNU")
IF ("${CMAKE_CXX_FLAGS}" STREQUAL "")
# Only set flags if there has been no flag set
SET (CMAKE_CXX_FLAGS "-std=c++11 -Wall" CACHE STRING "Flags used by the compiler during all build types." FORCE)
ENDIF()
ENDIF()
ADD_EXECUTABLE ( cpphoaf cpphoaf.cc )

19
resources/3rdparty/cpphoafparser-0.99.2/src/basic_parser_1.cc
View File

@ -0,0 +1,19 @@
#include "cpphoafparser/consumer/hoa_consumer_print.hh"
#include "cpphoafparser/parser/hoa_parser.hh"
using namespace cpphoafparser;
/** The most basic HOA parser: Read an automaton from input and print it to the output. */
int main(int argc, const char* argv[]) {
HOAConsumer::ptr consumer(new HOAConsumerPrint(std::cout));
try {
HOAParser::parse(std::cin, consumer);
} catch (std::exception& e) {
std::cerr << e.what() << std::endl;
return 1;
}
return 0;
}

40
resources/3rdparty/cpphoafparser-0.99.2/src/basic_parser_2.cc
View File

@ -0,0 +1,40 @@
#include "cpphoafparser/consumer/hoa_intermediate.hh"
#include "cpphoafparser/consumer/hoa_consumer_null.hh"
#include "cpphoafparser/parser/hoa_parser.hh"
using namespace cpphoafparser;
/* An HOAIntermediate that counts invocations of addState */
class CountStates : public HOAIntermediate {
public:
typedef std::shared_ptr<CountStates> ptr;
unsigned int count = 0;
CountStates(HOAConsumer::ptr next) : HOAIntermediate(next) {
}
virtual void addState(unsigned int id,
std::shared_ptr<std::string> info,
label_expr::ptr labelExpr,
std::shared_ptr<int_list> accSignature) override {
count++;
next->addState(id, info, labelExpr, accSignature);
}
};
/** Demonstrating the use of HOAIntermediates */
int main(int argc, const char* argv[]) {
HOAConsumer::ptr hoaNull(new HOAConsumerNull());
CountStates::ptr counter(new CountStates(hoaNull));
try {
HOAParser::parse(std::cin, counter);
std::cout << "Number of state definitions = " << counter->count << std::endl;
} catch (std::exception& e) {
std::cerr << e.what() << std::endl;
return 1;
}
return 0;
}

203
resources/3rdparty/cpphoafparser-0.99.2/src/cpphoaf.cc
View File

@ -0,0 +1,203 @@
//==============================================================================
//
// Copyright (c) 2015-
// Authors:
// * Joachim Klein <klein@tcs.inf.tu-dresden.de>
// * David Mueller <david.mueller@tcs.inf.tu-dresden.de>
//
//------------------------------------------------------------------------------
//
// 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
//
//==============================================================================
#include <queue>
#include <iostream>
#include <fstream>
#include "cpphoafparser/consumer/hoa_consumer_print.hh"
#include "cpphoafparser/consumer/hoa_consumer_null.hh"
#include "cpphoafparser/consumer/hoa_intermediate_trace.hh"
#include "cpphoafparser/consumer/hoa_intermediate_resolve_aliases.hh"
#include "cpphoafparser/parser/hoa_parser.hh"
using namespace cpphoafparser;
/** The version */
static const char* version = "0.99.2";
/** Print version to out, verbose? */
static void printVersion(std::ostream& out, bool verbose) {
out << "cpphoafparser library - command line tool (version " << version << ")" << std::endl;
out << " (C) Copyright 2015- Joachim Klein, David Mueller" << std::endl;
out << " http://automata.tools/hoa/cpphoafparser/" << std::endl;
out << std::endl;
if (verbose) {
out << "The cpphoafparser library is free software; you can redistribute it and/or" << std::endl;
out << "modify it under the terms of the GNU Lesser General Public" << std::endl;
out << "License as published by the Free Software Foundation; either" << std::endl;
out << "version 2.1 of the License, or (at your option) any later version." << std::endl;
out << std::endl;
out << "The cpphoafparser library is distributed in the hope that it will be useful," << std::endl;
out << "but WITHOUT ANY WARRANTY; without even the implied warranty of" << std::endl;
out << "MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU" << std::endl;
out << "Lesser General Public License for more details." << std::endl;
}
}
/** Print usage information, and optionally error message */
static unsigned int usage(const std::string& error = "") {
printVersion(std::cerr, false);
if (error != "") {
std::cerr << "Command-line arguments error: " << error << std::endl;
std::cerr << "Use argument 'help' to get usage information." << std::endl;
return 2;
}
std::cerr << "Arguments:" << std::endl;
std::cerr << " command [flags]* file" << std::endl << std::endl;
std::cerr << " Valid commands:" << std::endl;
std::cerr << " parse Parse the HOAF file and check for errors" << std::endl;
std::cerr << " print Parse the HOAF file, perform any specified transformations" << std::endl;
std::cerr << " and print the parsed automata to standard out" << std::endl;
std::cerr << " version Print the version and exit" << std::endl;
std::cerr << " help Print this help screen and exit" << std::endl;
std::cerr << std::endl;
std::cerr << " file can be a filename or - to request reading from standard input" << std::endl;
std::cerr << std::endl;
std::cerr << " Valid flags:" << std::endl;
std::cerr << " --resolve-aliases Resolve aliases" << std::endl;
std::cerr << " --no-validate Do not perform semantic validation" << std::endl;
std::cerr << " --trace Debugging: Trace the function calls to HOAConsumer" << std::endl;
// std::cerr << " --verbose Increase verbosity" << std::endl;
return (error != "" ? 2 : 0);
}
int main(int argc, char* argv[]) {
bool verbose = false;
bool resolve_aliases = false;
bool trace = false;
bool validate = true;
std::queue<std::string> arguments;
for (int i=1; i<argc; i++) {
arguments.push(argv[i]);
}
if (arguments.size() == 0) {
return usage();
}
std::string command = arguments.front();
arguments.pop();
if (command == "help" || command == "--help") {
return usage();
}
if (command == "version") {
printVersion(std::cout, true);
return 0;
}
while (!arguments.empty()) {
const std::string& arg = arguments.front();
if (arg.compare(0, 2, "--") == 0) {
// is an argument
arguments.pop();
if (arg == "--resolve-aliases") {
resolve_aliases = true;
} else if (arg == "--trace") {
trace = true;
} else if (arg == "--no-validate") {
validate = false;
} else if (arg == "--") {
// end of arguments
break;
} else {
return usage("Unknown argument "+arg);
}
}
// not an argument
break;
}
if (arguments.empty()) {
return usage("Missing filename (or - for standard input)");
}
if (arguments.size() > 1) {
return usage("More than one filename, currently only supports single file");
}
std::string filename = arguments.front();
arguments.pop();
std::shared_ptr<std::ifstream> f_in;
if (filename != "-") {
f_in.reset(new std::ifstream(filename.c_str()));
if (!*f_in) {
std::cerr << "Error opening file " + filename << std::endl;
return 1;
}
}
std::istream& in = (filename == "-" ? std::cin : *f_in);
if (verbose) {
std::cerr << "Reading from " + (filename != "-" ? "file "+filename : "standard input") << std::endl;
}
HOAConsumer::ptr consumer;
if (command == "print") {
consumer.reset(new HOAConsumerPrint(std::cout));
} else if (command == "parse") {
consumer.reset(new HOAConsumerNull());
} else {
return usage("Unknown command: "+command);
}
if (resolve_aliases) {
consumer.reset(new HOAIntermediateResolveAliases(consumer));
}
if (trace) {
consumer.reset(new HOAIntermediateTrace(consumer));
}
try {
HOAParser::parse(in, consumer, validate);
if (command == "parse") {
std::cout << "Parsing OK" << std::endl;
}
return 0;
} catch (HOAParserException& e) {
std::cerr << e.what() << std::endl;
} catch (HOAConsumerException& e) {
std::cerr << "Exception: " << e.what() << std::endl;
}
return 1;
}
Write Preview
Loading…
Cancel
Save