Commit 44e70427 authored by Hans Vrapi's avatar Hans Vrapi
Browse files

update transformer

parent 1399dae5
##Third-Party libs
resources/3rdparty/l3pp/.git/
resources/3rdparty/gtest-1.7.0/
resources/3rdparty/gmm-5.2/
resources/3rdparty/cudd-3.0.0/
resources/3rdparty/xercesc-3.1.2/
#Visual Studio files
*.[Oo]bj
*.user
*.aps
*.pch
*.vspscc
*.vssscc
*_i.c
*_p.c
*.ncb
*.suo
*.tlb
*.tlh
*.bak
*.[Cc]ache
*.ilk
*.log
*.lib
*.sbr
*.sdf
*.tlog
*.lastbuildstate
*.pdb
*.idb
*.opensdf
*.unsuccessfulbuild
ipch/
obj/
CMakeFiles/
CPackConfig.cmake
# The build Dir
/*build*/
build//CMakeLists.txt
/*.vcxproj
/*.filters
/*.sln
#Temp texteditor files
*.orig
*.*~
nbproject/
.DS_Store
.idea
.vscode
*.out
resources/3rdparty/cudd-3.0.0/Makefile.in
resources/3rdparty/cudd-3.0.0/aclocal.m4
# Travis helpers
travis/mtime_cache/cache.json
# Caroline
CMakeCache.txt
*.cmake
DartConfiguration.tcl
Makefile
/bin/
/googletest-prefix/
/include/
/l3pp_ext-prefix/
/resources/3rdparty/
/storm-version.cpp
/storm.cbp
# Default ignored files
/shelf/
/workspace.xml
# Editor-based HTTP Client requests
/httpRequests/
# Datasource local storage ignored files
/dataSources/
/dataSources.local.xml
storm
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<module classpath="CMake" type="CPP_MODULE" version="4" />
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<project version="4">
<component name="CMakeWorkspace" PROJECT_DIR="$PROJECT_DIR$" />
</project>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<project version="4">
<component name="ProjectModuleManager">
<modules>
<module fileurl="file://$PROJECT_DIR$/.idea/bn-mc-transformer.iml" filepath="$PROJECT_DIR$/.idea/bn-mc-transformer.iml" />
</modules>
</component>
</project>
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8"?>
<project version="4">
<component name="VcsDirectoryMappings">
<mapping directory="$PROJECT_DIR$" vcs="Git" />
<mapping directory="$PROJECT_DIR$/build/include/resources/3rdparty/StormEigen" vcs="Git" />
<mapping directory="$PROJECT_DIR$/cmake-build-debug/include/resources/3rdparty/StormEigen" vcs="Git" />
<mapping directory="$PROJECT_DIR$/resources/3rdparty/l3pp" vcs="Git" />
</component>
</project>
\ No newline at end of file
{
"files.associations": {
"fstream": "cpp",
"*.tpp": "cpp",
"cctype": "cpp",
"clocale": "cpp",
"cmath": "cpp",
"cstdarg": "cpp",
"cstddef": "cpp",
"cstdio": "cpp",
"cstdlib": "cpp",
"cstring": "cpp",
"cwchar": "cpp",
"cwctype": "cpp",
"array": "cpp",
"atomic": "cpp",
"*.tcc": "cpp",
"bitset": "cpp",
"chrono": "cpp",
"complex": "cpp",
"condition_variable": "cpp",
"cstdint": "cpp",
"deque": "cpp",
"forward_list": "cpp",
"list": "cpp",
"unordered_map": "cpp",
"unordered_set": "cpp",
"vector": "cpp",
"exception": "cpp",
"algorithm": "cpp",
"functional": "cpp",
"iterator": "cpp",
"map": "cpp",
"memory": "cpp",
"memory_resource": "cpp",
"numeric": "cpp",
"optional": "cpp",
"random": "cpp",
"set": "cpp",
"string": "cpp",
"string_view": "cpp",
"system_error": "cpp",
"tuple": "cpp",
"type_traits": "cpp",
"utility": "cpp",
"initializer_list": "cpp",
"iomanip": "cpp",
"iosfwd": "cpp",
"iostream": "cpp",
"istream": "cpp",
"limits": "cpp",
"mutex": "cpp",
"new": "cpp",
"ostream": "cpp",
"sstream": "cpp",
"stdexcept": "cpp",
"streambuf": "cpp",
"thread": "cpp",
"cinttypes": "cpp",
"typeinfo": "cpp",
"ratio": "cpp",
"bit": "cpp",
"ctime": "cpp",
"typeindex": "cpp",
"variant": "cpp"
}
}
\ No newline at end of file
include(InstallRequiredSystemLibraries)
# For help take a look at:
# http://www.cmake.org/Wiki/CMake:CPackConfiguration
### general settings
set(CPACK_PACKAGE_NAME "Storm")
set(CPACK_PACKAGE_VENDOR "RWTH Aachen University")
set(CPACK_PACKAGE_DESCRIPTION_SUMMARY "Storm - A probabilistic model checker written in C++.")
set(CPACK_RESOURCE_FILE_LICENSE "${CMAKE_SOURCE_DIR}/LICENSE")
### versions
set(CPACK_PACKAGE_VERSION_MAJOR "${STORM_CPP_VERSION_MAJOR}")
set(CPACK_PACKAGE_VERSION_MINOR "${STORM_CPP_VERSION_MINOR}")
set(CPACK_PACKAGE_VERSION_PATCH "${STORM_CPP_VERSION_PATCH}")
set(CPACK_PACKAGE_VERSION "${CPACK_PACKAGE_VERSION_MAJOR}.${CPACK_PACKAGE_VERSION_MINOR}.${CPACK_PACKAGE_VERSION_PATCH}-${STORM_CPP_VERSION_HASH}")
set(CPACK_GENERATOR "ZIP")
set(CPACK_PACKAGE_INSTALL_DIRECTORY "${CPACK_PACKAGE_NAME}-${CPACK_PACKAGE_VERSION}")
### source package settings
set(CPACK_SOURCE_GENERATOR "ZIP")
set(CPACK_SOURCE_IGNORE_FILES "~$;[.]swp$;/[.]svn/;/[.]git/;.gitignore;/build/;tags;cscope.*")
set(CPACK_SOURCE_PACKAGE_FILE_NAME "${CPACK_PACKAGE_NAME}-${CPACK_PACKAGE_VERSION}-src")
include(CPack)
\ No newline at end of file
This diff is collapsed.
project(carlext)
cmake_minimum_required(VERSION 3.3)
include(ExternalProject)
option(STORM_3RDPARTY_BINARY_DIR "3rd party bin dir")
message(STATUS "Carl - Storm 3rdparty binary dir: ${STORM_3RDPARTY_BINARY_DIR}")
ExternalProject_Add(carl-config
GIT_REPOSITORY https://github.com/ths-rwth/carl
GIT_TAG master14
PREFIX here
SOURCE_DIR source_dir
BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl
CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=ON -DEXPORT_TO_CMAKE=ON -DTHREAD_SAFE=ON -DUSE_CLN_NUMBERS=ON -DUSE_GINAC=ON -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=ON -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl
BUILD_IN_SOURCE 0
LOG_UPDATE OFF
LOG_CONFIGURE OFF
BUILD_COMMAND "" # Disable build step.
INSTALL_COMMAND "" # Disable install step too.
)
add_custom_target(build-carl)
add_dependencies(build-carl carl-config)
message(STATUS "Carl - Finished configuration.")
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
# 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
==============================================================================
|
| 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 -
.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; }
\ No newline at end of file
<!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>