-
Notifications
You must be signed in to change notification settings - Fork 7
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pr #24: refactor valuation and replace base::pointer with std::…
…vector Refactor Valuation to use std::vector instead of base::pointer
- Loading branch information
Showing
23 changed files
with
453 additions
and
475 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,6 +1,7 @@ | ||
| /build | ||
| /build-* | ||
| /cmake-build-* | ||
| /libs | ||
| /local | ||
| compile_commands.json | ||
|
|
||
| /.idea | ||
|
|
||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,28 +1,62 @@ | ||
| # UPPAAL DBM Library | ||
| UDBM is a DBM library developed for the UPPAAL project. | ||
| <acronym title="Difference Bound Matrix">DBM</acronym>s [[dill89, rokicki93, lpw:fct95, bengtsson02]](#-References) are efficient data structures to represent clock constraints in timed automata [[ad90]](#-References). | ||
| They are used in UPPAAL [[lpy97, by04, bdl04]](#-References) as the core data structure to represent time. | ||
| The library features all the common operations such as up (delay, or future), down (past), general updates, different extrapolation functions, etc. on DBMs and federations. | ||
| The library also supports subtractions. | ||
| The API is in C and C++. The C++ part uses active clocks and hides (to some extent) memory management. | ||
|
|
||
| DBM stands for Difference Bound Matrix and used to capture and reason about clock constraints described in Timed Automata models. | ||
| * Reliable <br/> | ||
| The DBM library has an extensive test suite with an extra alternative implementation of the algorithms. This implementation has also been tested on countless case studies. | ||
| * Performant <br/> | ||
| The DBM library is the fruit of many years of development of UPPAAL, bringing to the mainstream efficient algorithms to manipulate DBMs. The API is available in C and C++. | ||
| * Current <br/> | ||
| The DBM library is based on the latest internal development version of UPPAAL, containing the latest performance and language improvements. | ||
|
|
||
| The general form of the constraints is the following: `x_i - x_j <=> c_ij`, where `x_i` and `x_j` are clocks (one of them can be "zero clock" which is always zero) and `<=` can be one of {`<`, `<=`, `=`, `>=`, `>`} and `c_ij` is an integer constant. | ||
|
|
||
| For more details please see [wiki pages](https://github.com/UPPAALModelChecker/UDBM/wiki). | ||
|
|
||
| ## Build | ||
| The following packages need to be installed: | ||
| * cmake | ||
| * gcc | ||
| * xxHash | ||
| ## Build | ||
| The following packages need to be installed: | ||
| * [bash](https://www.gnu.org/software/bash/) | ||
| * [cmake](https://cmake.org/) | ||
| * [GCC](https://gcc.gnu.org/), [clang](https://clang.llvm.org/) or other C++17 compiler. | ||
| * [xxHash](https://github.com/Cyan4973/xxHash) | ||
| * [UUtils](https://github.com/UPPAALModelChecker/UUtils) | ||
| * doctest (test only) | ||
| * boost (test only) | ||
| * [doctest](https://github.com/doctest/doctest) (just for unit tests) | ||
|
|
||
| Compile source: | ||
| ```sh | ||
| cmake -B build/ -DCMAKE_BUILD_TYPE=Release | ||
| cmake --build build/ | ||
| The dependencies can be installed locally into `local` directory by running `getlibs.sh`: | ||
| ```shell | ||
| ./getlibs.sh | ||
| ``` | ||
|
|
||
| You can also insall dependencies locally by running: | ||
| Compile source with **release** optimizations: | ||
| ```shell | ||
| cmake -B build-release -DCMAKE_BUILD_TYPE=Release -DCMAKE_PREFIX_PATH=$PWD/local | ||
| cmake --build build-release | ||
| ``` | ||
| ./getlibs.sh | ||
|
|
||
| Compile source with **release** optimizations and **unit tests**: | ||
| ```shell | ||
| cmake -B build-release -DCMAKE_BUILD_TYPE=Release -DCMAKE_PREFIX_PATH=$PWD/local -DTESTING=ON | ||
| cmake --build build-release | ||
| (cd build-release/test ; ctest) | ||
| ``` | ||
|
|
||
| Compile source with **debug**, **sanitizers** and **unit tests**: | ||
| ```shell | ||
| cmake -B build-debug -DCMAKE_BUILD_TYPE=Debug -DCMAKE_PREFIX_PATH=$PWD/local -DTESTING=ON -DSSP=ON -DUBSAN=ON -DASAN=ON | ||
| cmake --build build-debug | ||
| (cd build-debug/test ; ctest) | ||
| ``` | ||
|
|
||
| ## References | ||
|
|
||
| * [[dill89]](https://doi.org/10.1007/3-540-52148-8_17) David L. Dill. _Timing Assumptions and Verification of Finite-State Concurrent Systems._ LNCS 407\. Springer Berlin 1989, pp 197-212. | ||
| * [rokicki93] Tomas Gerhard Rokicki. _Representing and Modeling Digital Circuits._ Ph.D. thesis, Standford University 1993. | ||
| * [[lpw:fct95]](https://doi.org/10.1007/3-540-60249-6_41) Kim G. Larsen, Paul Pettersson, and Wang Yi. _Model-Checking for Real-Time Systems._ Fundamentals of Computation Theory 1995, LNCS 965 pages 62-88. | ||
| * [[bengtsson02]](http://uu.diva-portal.org/smash/record.jsf?pid=diva2:161779) Johan Bengtsson. _Clocks, DBM, and States in Timed Systems._ Ph.D. thesis, Uppsala University 2002. | ||
| * [[ad90]](https://doi.org/10.1007/BFb0032042) Rajeev Alur and David L. Dill. _Automata for Modeling Real-Time Systems._ International Colloquium on Algorithms, Languages, and Programming 1990, LNCS 443 pages 322-335. | ||
| * [[lpy97]](https://doi.org/10.1007/s100090050010) Kim G. Larsen, Paul Pettersson, and Wang Yi. _UPPAAL in a Nutshell._ International Journal on Software Tools for Technology Transfer , October 1997, number 1-2 pages 134-152. | ||
| * [[by04]](https://doi.org/10.1007/978-3-540-27755-2_3) Johan Bengtsson and Wang Yi. [_Timed Automata: Semantics, Algorithms and Tools._](https://homes.cs.aau.dk/~adavid/UDBM/materials/by04-bookchapter.pdf) Concurrency and Petri Nets 2004, LNCS 3098. | ||
| * [[bdl04]](https://www.it.uu.se/research/group/darts/papers/texts/new-tutorial.pdf) Gerd Behrmann, Alexandre David, and Kim G. Larsen. _A Tutorial on UPPAAL._ 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems (SFM-RT'04), LNCS 3185. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,37 +1,52 @@ | ||
| #!/usr/bin/env bash | ||
| set -euxo pipefail | ||
|
|
||
| # Cursed line that should also work on macos | ||
| # https://stackoverflow.com/questions/59895/how-can-i-get-the-source-directory-of-a-bash-script-from-within-the-script-itsel | ||
| SOURCE_DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" >/dev/null 2>&1 && pwd )" | ||
| mkdir -p "$SOURCE_DIR/libs/sources"; | ||
| CMAKE_PREFIX_PATH="$SOURCE_DIR/libs/" | ||
|
|
||
| CMAKE_ARGS="-DCMAKE_BUILD_TYPE=Release -DCMAKE_PREFIX_PATH=$CMAKE_PREFIX_PATH" | ||
| PREFIX="$SOURCE_DIR/local" | ||
| SOURCES="$SOURCE_DIR/local/sources" | ||
| mkdir -p "$SOURCES" | ||
|
|
||
| CMAKE_PREFIX_PATH="$PREFIX" | ||
|
|
||
| CMAKE_ARGS="-DCMAKE_BUILD_TYPE=Release -DCMAKE_PREFIX_PATH=$CMAKE_PREFIX_PATH -DCMAKE_INSTALL_PREFIX=$PREFIX" | ||
| if [ -z ${CMAKE_TOOLCHAIN_FILE+x} ]; then | ||
| echo "Not using a custom toolchain"; | ||
| else | ||
| echo "Using toolchain $CMAKE_TOOLCHAIN_FILE"; | ||
| CMAKE_ARGS="$CMAKE_ARGS -DCMAKE_TOOLCHAIN_FILE=$CMAKE_TOOLCHAIN_FILE"; | ||
| fi | ||
|
|
||
| # doctest for unit testing | ||
| cd "$SOURCES" | ||
| curl -L https://github.com/doctest/doctest/archive/refs/tags/v2.4.9.tar.gz -o doctest-2.4.9.tar.gz | ||
| tar -xf doctest-2.4.9.tar.gz | ||
| SOURCE_DIR="$SOURCES/doctest-2.4.9" | ||
| BUILD_DIR="$SOURCE_DIR/build" | ||
| mkdir -p "$BUILD_DIR" | ||
| cmake $CMAKE_ARGS -DDOCTEST_WITH_TESTS=OFF -B "$BUILD_DIR" "$SOURCE_DIR" | ||
| cmake --build "$BUILD_DIR" --config Release | ||
| cmake --install "$BUILD_DIR" --config Release | ||
|
|
||
| cd $SOURCE_DIR/libs/sources; | ||
| curl -L https://github.com/Cyan4973/xxHash/archive/refs/tags/v0.8.0.tar.gz -o v0.8.0.tar.gz | ||
| tar -xvf v0.8.0.tar.gz | ||
| mkdir -p "$SOURCE_DIR/libs/sources/xxHash-0.8.0/build" | ||
| cd "$SOURCE_DIR/libs/sources/xxHash-0.8.0/build" | ||
| cmake $CMAKE_ARGS -DCMAKE_INSTALL_PREFIX="$SOURCE_DIR/libs/xxHash" -DBUILD_SHARED_LIBS=OFF ../cmake_unofficial | ||
| cmake --build . --config Release | ||
| cmake --install . --config Release | ||
| # xxHash for fast high quality hashing | ||
| cd "$SOURCES" | ||
| curl -L https://github.com/Cyan4973/xxHash/archive/refs/tags/v0.8.0.tar.gz -o xxHash-0.8.0.tar.gz | ||
| tar -xf xxHash-0.8.0.tar.gz | ||
| SOURCE_DIR="$SOURCES/xxHash-0.8.0" | ||
| BUILD_DIR="$SOURCE_DIR/build" | ||
| mkdir -p "$BUILD_DIR" | ||
| cmake $CMAKE_ARGS -DBUILD_SHARED_LIBS=OFF -B "$BUILD_DIR" "$SOURCE_DIR/cmake_unofficial" | ||
| cmake --build "$BUILD_DIR" --config Release | ||
| cmake --install "$BUILD_DIR" --config Release | ||
|
|
||
| # UUtils various low level Uppaal utilities | ||
| #git clone https://github.com/UPPAALModelChecker/UUtils "$SOURCE_DIR/libs/sources/UUtils"; | ||
| cd $SOURCE_DIR/libs/sources; | ||
| curl -L https://github.com/UPPAALModelChecker/UUtils/archive/refs/tags/v1.1.1.tar.gz -o v1.1.1.tar.gz | ||
| tar -xvf v1.1.1.tar.gz | ||
| mkdir -p "$SOURCE_DIR/libs/sources/UUtils-1.1.1/build" | ||
| cd "$SOURCE_DIR/libs/sources/UUtils-1.1.1" | ||
| cd build | ||
| cmake $CMAKE_ARGS -DCMAKE_INSTALL_PREFIX="$SOURCE_DIR/libs/UUtils" .. | ||
| cmake --build . --config Release | ||
| cmake --install . --config Release | ||
| cd "$SOURCES" | ||
| curl -L https://github.com/UPPAALModelChecker/UUtils/archive/refs/tags/v1.1.1.tar.gz -o UUtils-1.1.1.tar.gz | ||
| tar -xf UUtils-1.1.1.tar.gz | ||
| SOURCE_DIR="$SOURCES/UUtils-1.1.1" | ||
| BUILD_DIR="$SOURCE_DIR/build" | ||
| mkdir -p "$BUILD_DIR" | ||
| cmake $CMAKE_ARGS -B "$BUILD_DIR" "$SOURCE_DIR" | ||
| cmake --build "$BUILD_DIR" --config Release | ||
| cmake --install "$BUILD_DIR" --config Release |
Oops, something went wrong.