Rust DBM Library: Use EDBM instead of UDBM everywhere

.github/workflows/build_artifacts.yaml

@@ -14,15 +14,8 @@ jobs:
       - uses: actions/checkout@v2
         with:
           submodules: 'true'
-      - name: Install compiler tools
-        run: |
-          sudo apt-get update
-          sudo apt-get install llvm automake libxml2-dev gperf build-essential libboost-all-dev cmake make protobuf-compiler
-      - name: Compile UDBM wrapper
-        run: |
-          cd dbm
-          cmake -B build/
-          cmake --build build/
+      - name: Install llvm-config
+        run: sudo apt-get install llvm protobuf-compiler
       - uses: actions-rs/toolchain@v1
         with:
           profile: minimal
@@ -45,15 +38,8 @@ jobs:
       - uses: actions/checkout@v2
         with:
           submodules: 'true'
-      - name: Install compiler tools
-        run: |
-          sudo apt-get update
-          sudo apt-get install llvm automake libxml2-dev gperf build-essential libboost-all-dev cmake make protobuf-compiler mingw-w64
-      - name: Compile UDBM wrapper
-        run: |
-          cd dbm
-          cmake -B build/ -D CMAKE_TOOLCHAIN_FILE=toolchain-x86_64-w64-mingw32.cmake
-          cmake --build build/
+      - name: Install llvm-config
+        run: sudo apt-get install llvm protobuf-compiler mingw-w64
       - uses: actions-rs/toolchain@v1
         with:
           profile: minimal

.github/workflows/ci.yaml

@@ -11,15 +11,8 @@ jobs:
       - uses: actions/checkout@v2
         with:
           submodules: 'true'
-      - name: Install compiler tools
-        run: |
-          sudo apt-get update
-          sudo apt-get install llvm automake libxml2-dev gperf build-essential libboost-all-dev cmake make protobuf-compiler
-      - name: Compile UDBM wrapper
-        run: |
-          cd dbm
-          cmake -B build/
-          cmake --build build/
+      - name: Install llvm-config 
+        run: sudo apt-get install llvm protobuf-compiler
       - uses: actions-rs/toolchain@v1
         with:
           profile: minimal
@@ -28,7 +21,6 @@ jobs:
       - uses: actions-rs/cargo@v1
         with:
           command: test
-          args: -- --skip "DBMLib::lib_dbm::UDBM::bindgen_test_layout_dbm_idbm_t"
   fmt:
     name: Check code is formatted
     runs-on: ubuntu-latest

Cargo.toml

@@ -32,11 +32,14 @@ simple-error = "0.2.3"
 force_graph = "0.3.2"
 rand = "0.8.5"
 futures = "0.3.21"
+edbm = {git = "https://github.com/Ecdar/EDBM"}
 
 
+# Enable optimizations for EDBM in debug mode, but not for our code:
+[profile.dev.package.edbm]
+opt-level = 3
+
 [build-dependencies]
-bindgen = "0.60.0"
-cc = "1.0.73"
 tonic-build = "0.5.*"
 
 

README.md

@@ -3,38 +3,22 @@
 ## About
 This is a model checking engine for ECDAR (Environment for Compositional Design and Analysis of Real Time Systems) written in rust. 
 
+#### DBM Library
+The engine uses the ECDAR DBM Library for operations on zones of time (https://www.github.com/ECDAR/EDBM).
+
 ## Prerequisites 
-- A rust compiler and C++ compiler installed (https://www.rust-lang.org/learn/get-started) 
-- [clang](https://clang.llvm.org/) for compiling the library (for the Ubuntu linux distribution, run the command ```apt install llvm-dev libclang-dev clang``` to properly install the clang dependencies)
+- A rust compiler installed (https://www.rust-lang.org/learn/get-started) 
 - A folder containing the model components to check
 - ProtoBuf compiler protoc (for the Ubuntu linux distribution ```apt install protobuf-compiler```)
 - Download ProtoBuf definitions with ```git submodule update --init --recursive```
 
-## Building the DBM library
-
-Navigate into the dbm folder and make sure no build folder already exists. Then use cmake to build the dbm library, the files should be created in a `out` folder where Reveaal use them from.
-
-```bash
-cd dbm
-cmake -B build/
-cmake --build build/
-```
-
 ## Building the project
 - Build the project using `cargo build`
 - Optionally run the tests using `cargo test`
 
-## Cross compiling from Linux to Windows
-Build the DBM library using the x86_64-w64-mingw32 toolchain:
-
-```bash
-cd dbm
-cmake -B buildw/ -D CMAKE_TOOLCHAIN_FILE=toolchain-x86_64-w64-mingw32.cmake
-cmake --build buildw/
-```
+## Cross compiling
+The project is pure just so one should be able to crosscompile to any platform with a rust target.
 
+### Compiling to Windows
 Ensure that the rustc windows target is installed with `rustup target add x86_64-pc-windows-gnu` and build with cargo:
-
 `cargo build --target x86_64-pc-windows-gnu`
-
-The rust compiler is configured to pick the library for the current target, so you dont have to recompile the dbm library when switching compile target.