Merge remote-tracking branch 'origin/main' into bench-symbol-6

.github/workflows/build_artifacts.yaml

@@ -1,95 +1,84 @@
-name: Build artifacts
+name: Build Artifacts
 
 on:
-  pull_request:
-    branches:
-      - main
   workflow_dispatch:
+  push:
 
 jobs:   
-  build-macos:
+  macos:
+    name: 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
+        path: target/release/reveaal
         if-no-files-found: error
+        retention-days: 7
 
-  build-win:
+  win:
+    name: Build Windows
     runs-on: windows-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-windows
-        path: target/release/Reveaal.exe
+        path: target/release/reveaal.exe
         if-no-files-found: error
-
-  build-ubuntu:
+        retention-days: 7
+
+  ubuntu:
+    name: Build Ubuntu
     runs-on: ubuntu-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-ubuntu
-        path: target/release/Reveaal
-        if-no-files-found: error
+        path: target/release/reveaal
+        if-no-files-found: error
+        retention-days: 7

.github/workflows/check_format.yaml

@@ -0,0 +1,45 @@
+name: Check formatting
+
+on:
+  workflow_dispatch:
+  push:
+
+jobs:
+  fmt:
+    name: cargo fmt
+    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
+
+  clippy:
+    name: 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: clippy
+      - uses: Swatinem/rust-cache@v2
+        with:
+          cache-on-failure: true
+      - 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,3 @@
 [submodule "Ecdar-ProtoBuf"]
 	path = Ecdar-ProtoBuf
-	url = https://github.com/Ecdar/Ecdar-ProtoBuf.git
-	branch = main
+	url = https://github.com/ECDAR-AAU-SW-P5/Ecdar-ProtoBuf.git

Cargo.toml

@@ -10,7 +10,7 @@ name = "reveaal"
 path = "src/lib.rs"
 
 [[bin]]
-name = "Reveaal"
+name = "reveaal"
 path = "src/main.rs"
 
 [features]

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/clock_reduction_bench.rs

@@ -75,7 +75,6 @@ static SAMPLES: u64 = 10;
 
 mod bench_helper;
 use reveaal::parse_queries::parse_to_query;
-use reveaal::TransitionSystems::TransitionSystem;
 
 // const QUERY: &str = "refinement: (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) // (Adm2 && HalfAdm1 && HalfAdm2)) // Researcher) <= (((((Adm2 && HalfAdm1 && HalfAdm2) || Machine || Researcher) && ((Adm2 && HalfAdm1) || Machine || Researcher) && ((Adm2 && HalfAdm2) || Machine || Researcher) && ((HalfAdm1 && HalfAdm2) || Machine || Researcher) && (Adm2 || Machine || Researcher)) // (Adm2 && HalfAdm1 && HalfAdm2)) // Researcher)";
 const REACHABILITY_QUERY: &str = "reachability: Machine || Researcher @ Machine.L5 && Researcher.L6 -> Machine.L4 && Researcher.L9";

benches/reachability_bench.rs

@@ -3,7 +3,7 @@ pub mod bench_helper;
 pub mod flamegraph;
 use flamegraph::flamegraph_profiler::FlamegraphProfiler;
 use reveaal::extract_system_rep::create_executable_query;
-use reveaal::ModelObjects::Query;
+use reveaal::model_objects::Query;
 use reveaal::{parse_queries, ComponentLoader};
 
 fn bench_reachability(c: &mut Criterion, query: &str, loader: &mut Box<dyn ComponentLoader>) {

benches/refinement_bench.rs

@@ -5,9 +5,9 @@ pub mod flamegraph;
 
 use flamegraph::flamegraph_profiler::FlamegraphProfiler;
 use reveaal::extract_system_rep::create_executable_query;
-use reveaal::ModelObjects::Query;
-use reveaal::System::executable_query::ExecutableQuery;
-use reveaal::System::query_failures::QueryResult;
+use reveaal::model_objects::Query;
+use reveaal::system::executable_query::ExecutableQuery;
+use reveaal::system::query_failures::QueryResult;
 use reveaal::{parse_queries, ComponentLoader};
 
 fn construct_query<'a>(