SW5 (#177)

.github/workflows/build_artifacts.yaml

@@ -1,95 +1,36 @@
-name: Build artifacts
+name: Build Artifacts
 
 on:
-  pull_request:
-    branches:
-      - main
   workflow_dispatch:
+  push:
+
+jobs:
+  build:
+    strategy:
+      matrix:
+        os: [ ubuntu-latest, windows-latest, macos-latest ]
+    name: Build ${{ matrix.os }}
+    runs-on: ${{ matrix.os }}
 
-jobs:   
-  build-macos:
-    runs-on: macos-latest
     steps:
     - uses: actions/checkout@v3
       with:
         submodules: 'true'
-    - uses: arduino/setup-protoc@v1.1.2
+    - uses: arduino/setup-protoc@v2
       with:
         repo-token: ${{ secrets.GITHUB_TOKEN }}
-    - uses: actions-rs/toolchain@v1
-      with:
-        profile: minimal
-        toolchain: stable
-        override: true
+    - uses: dtolnay/rust-toolchain@stable
     - uses: Swatinem/rust-cache@v2
       with:
         cache-on-failure: true
-    - name: Build
-      uses: actions-rs/cargo@v1
+    - name: cargo build --release
+      uses: clechasseur/rs-cargo@v1
       with:
         command: build
         args: --release
-    - name: Upload artifacts 
-      uses: actions/upload-artifact@v2
+    - uses: actions/upload-artifact@v3
       with:
-        name: reveaal-macos
-        path: target/release/Reveaal
+        name: reveaal-${{ matrix.os }}
+        path: ${{ runner.os == 'Windows' && 'target/release/reveaal.exe' || 'target/release/reveaal' }}
         if-no-files-found: error
-
-  build-win:
-    runs-on: windows-latest
-    steps:
-    - uses: actions/checkout@v3
-      with:
-        submodules: 'true'
-    - uses: arduino/[email protected]
-      with:
-        repo-token: ${{ secrets.GITHUB_TOKEN }}
-    - uses: actions-rs/toolchain@v1
-      with:
-        profile: minimal
-        toolchain: stable
-        override: true
-    - uses: Swatinem/rust-cache@v2
-      with:
-        cache-on-failure: true
-    - name: Build
-      uses: actions-rs/cargo@v1
-      with:
-        command: build
-        args: --release
-    - name: Upload artifacts 
-      uses: actions/upload-artifact@v2
-      with:
-        name: reveaal-windows
-        path: target/release/Reveaal.exe
-        if-no-files-found: error
-
-  build-ubuntu:
-    runs-on: ubuntu-latest
-    steps:
-    - uses: actions/checkout@v3
-      with:
-        submodules: 'true'
-    - uses: arduino/[email protected]
-      with:
-        repo-token: ${{ secrets.GITHUB_TOKEN }}
-    - uses: actions-rs/toolchain@v1
-      with:
-        profile: minimal
-        toolchain: stable
-        override: true
-    - uses: Swatinem/rust-cache@v2
-      with:
-        cache-on-failure: true
-    - name: Build
-      uses: actions-rs/cargo@v1
-      with:
-        command: build
-        args: --release
-    - name: Upload artifacts 
-      uses: actions/upload-artifact@v2
-      with:
-        name: reveaal-ubuntu
-        path: target/release/Reveaal
-        if-no-files-found: error
+        retention-days: 7

.github/workflows/check_format.yaml

@@ -0,0 +1,30 @@
+name: Check formatting
+
+on:
+  workflow_dispatch:
+  push:
+
+jobs:
+  fmt:
+    name: cargo fmt & Clippy lint and check
+    runs-on: ubuntu-latest
+    steps:
+      - run: sudo apt-get install llvm protobuf-compiler
+      - uses: actions/checkout@v3
+        with:
+          submodules: 'true'
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          components: rustfmt
+      - uses: Swatinem/rust-cache@v2
+        with:
+          cache-on-failure: true
+      - name: cargo fmt --all
+        uses: clechasseur/rs-cargo@v1
+        with:
+          command: fmt
+          args: --all -- --check
+      - name: clippy --all-targets --all-features
+        uses: clechasseur/rs-clippy-check@v3
+        with:
+          args: --all-targets --all-features -- -D warnings

.github/workflows/run_tests.yaml

@@ -0,0 +1,25 @@
+name: Run Tests
+
+on:
+  workflow_dispatch:
+  push:
+
+jobs:
+  ubuntu:
+    name: Tests Ubuntu
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: 'true'
+      - run: sudo apt-get install llvm protobuf-compiler
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          components: clippy
+      - uses: Swatinem/rust-cache@v2
+        with:
+          cache-on-failure: true
+      - name: cargo test
+        uses: clechasseur/rs-cargo@v1
+        with:
+          command: test

.gitmodules

@@ -1,4 +1,4 @@
 [submodule "Ecdar-ProtoBuf"]
-	path = Ecdar-ProtoBuf
-	url = https://github.com/Ecdar/Ecdar-ProtoBuf.git
-	branch = main
+    path = Ecdar-ProtoBuf
+    url = git@github.com:Ecdar/Ecdar-ProtoBuf.git
+    branch = SW5

Cargo.toml

@@ -3,14 +3,14 @@ name = "reveaal"
 version = "0.1.0"
 build = "src/build.rs"
 authors = ["Thomas Lohse", "Sebastian Lund", "Thorulf Neustrup", "Peter Greve"]
-edition = "2018"
+edition = "2021"
 
 [lib]
 name = "reveaal"
 path = "src/lib.rs"
 
 [[bin]]
-name = "Reveaal"
+name = "reveaal"
 path = "src/main.rs"
 
 [features]
@@ -27,39 +27,39 @@ xml-rs = "0.8.3"
 serde-xml-rs = "0.6.0"
 elementtree = "1.2.2"
 dyn-clone = "1.0"
-tonic = "0.8.3"
-prost = "0.11.0"
-tokio = { version = "1.0", features = ["macros", "rt"] }
+tonic = "0.11.0"
+prost = "0.12.3"
+tokio = { version = "1.36.0", features = ["macros", "rt"] }
 colored = "2.0.0"
-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" }
 log = "0.4.17"
-env_logger = { version = "0.9.0", optional = true }
+env_logger = { version = "0.11.2", optional = true }
 chrono = { version = "0.4.22", optional = true }
-test-case = "2.2.2"
+test-case = "3.3.1"
 num_cpus = "1.13.1"
-lru = "0.8.1"
-itertools = "0.10.5"
+lru = "0.12.2"
+itertools = "0.12.1"
 regex = "1"
 rayon = "1.6.1"
 lazy_static = "1.4.0"
+num = "0.4.1"
 
 # Enable optimizations for EDBM in debug mode, but not for our code:
 [profile.dev.package.edbm]
 opt-level = 3
 
 [build-dependencies]
-tonic-build = "0.8.2"
+tonic-build = "0.11.0"
 
 [dev-dependencies]
-test-case = "2.2.2"
-criterion = { version = "0.4.0", features = ["async_futures"] }
+test-case = "3.3.1"
+criterion = { version = "0.5.1", features = ["async_futures"] }
 
 [target.'cfg(unix)'.dev-dependencies]
-pprof = { version = "0.10.1", features = ["flamegraph"] }
+pprof = { version = "0.13.0", features = ["flamegraph"] }
 
 [[bench]]
 name = "refinement_bench"

README.md

@@ -6,25 +6,32 @@ This is a model checking engine for ECDAR (Environment for Compositional Design
 #### DBM Library
 The engine uses the ECDAR DBM Library for operations on zones of time (https://www.github.com/ECDAR/EDBM).
 
-## Prerequisites 
+## Building
+
+### Prerequisites 
 - A rust compiler installed (https://www.rust-lang.org/learn/get-started)
 - A folder containing the model components to check
 - Download ProtoBuf definitions with ```git submodule update --init --recursive```
 
-### Compiling on Linux
-You may need the ProtoBuf compiler protoc (for the Ubuntu linux distribution ```apt install protobuf-compiler```)
+**Windows**:
+We recommend installing and using the default ```x86_64-pc-windows-msvc``` Rust targets.
+If you instead (not recommended) are using ```x86_64-pc-windows-gnu``` targets on Windows you need to install mingw and add it to your PATH variable to build.
+
+#### Protobuf
+**Debian based (Ubuntu, mint etc.)**: ```apt install protobuf-compiler```
+
+**Arch based (Endeavour etc.)**: ```yay protobuf-c```
 
-### Compiling on Windows
-We recommend installing and using the default `x86_64-pc-windows-msvc` Rust targets.
-If you instead (not recommended) are using `x86_64-pc-windows-gnu` targets on Windows you need to install mingw and add it to your PATH variable to build.
+**Windows**: Download protobuf (https://github.com/protocolbuffers/protobuf/releases/)
+Add the bin folder to your path environment variable (https://www.computerhope.com/issues/ch000549.htm)
 
-## Building the project
-- Build the project using `cargo build`
-- Optionally run the tests using `cargo test`
+### Compiling and running
+- Build the project using ```cargo build```
+- Optionally run the tests using ```cargo test```
 
-## Cross compiling from Linux
+#### Cross compiling
 The project is pure Rust so one should be able to crosscompile to any platform with a rust target.
 
-### Compiling to Windows from Linux
-Make sure you have mingw installed `sudo apt-get install mingw-w64` and 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`
+**Debian -> Windows**
+Make sure you have mingw installed ```sudo apt-get install mingw-w64``` and 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```

benches/bench_helper.rs

@@ -1,10 +1,10 @@
-use reveaal::tests::TEST_SETTINGS;
+use reveaal::DEFAULT_SETTINGS;
 use reveaal::{ComponentLoader, JsonProjectLoader};
 
 const UNI_PATH: &str = "samples/json/EcdarUniversity";
 
 pub fn get_uni_loader() -> Box<dyn ComponentLoader + 'static> {
-    let mut loader = JsonProjectLoader::new_loader(UNI_PATH, TEST_SETTINGS).to_comp_loader();
+    let mut loader = JsonProjectLoader::new_loader(UNI_PATH, DEFAULT_SETTINGS).to_comp_loader();
     let _ = loader.get_component("Adm2");
     let _ = loader.get_component("Administration");
     let _ = loader.get_component("HalfAdm1");