Extending HCTL syntax (#19)

* Add option to use hybrid operator names in formulas.

* Update CI.

* Update syntax details in readme.

.github/workflows/build.yml

@@ -1,7 +1,8 @@
 name: build
+
 # This should ensure that the workflow won't run on `dev-*` branches, but will
-# otherwise execute on any other branch and any pull request (including dev
-# branches).
+# otherwise execute on any other branch and any pull request (including PRs
+# from dev branches).
 on:
   push:
     branches-ignore:
@@ -16,86 +17,85 @@ env:
   # Make sure to update this from time to time.
   RUST_VERSION: "1.77.0"
 jobs:
-  # Check formatting
+  # Checks syntax formatting.
   fmt:
     name: Rustfmt
     runs-on: ubuntu-latest
     env:
       RUSTFLAGS: "-D warnings"
     steps:
-      - name: Checkout.
-        uses: actions/checkout@v3
-      - name: Install Rust toolchain.
-        run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
-      - name: Rust format check.
-        run: cargo fmt --all -- --check
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: ${{ env.RUST_VERSION }}
+          components: rustfmt
+      - run: cargo fmt --all -- --check
 
-  # Run basic code validity check
+  # Run basic code validity check.
   check:
     needs: fmt
     name: Check
     runs-on: ubuntu-latest
     env:
       RUSTFLAGS: "-D warnings"
     steps:
-      - name: Checkout.
-        uses: actions/checkout@v3
-      - name: Install Rust toolchain.
-        run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
-      - name: Rust code validity check.
-        run: cargo check
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: ${{ env.RUST_VERSION }}
+      - run: cargo check --all-features
 
-  # Run all tests
+  # Run tests.
   test:
     needs: check
-    name: Test Suite
+    name: Test Suite (linux)
     runs-on: ubuntu-latest
     env:
       RUSTFLAGS: "-D warnings"
     steps:
-      - uses: actions/checkout@v3
-      - name: Checkout.
-        uses: actions/checkout@v3
-      - name: Install Rust toolchain.
-        run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
-      - name: Run tests.
-        run: cargo test --all-features
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: ${{ env.RUST_VERSION }}
+          components: rustfmt
+      - run: cargo test --all-features
 
-  # Check code style
+  # Checks code style.
   clippy:
     needs: check
     name: Clippy
     runs-on: ubuntu-latest
     env:
       RUSTFLAGS: "-D warnings"
     steps:
-      - name: Checkout.
-        uses: actions/checkout@v3
-      - name: Install Rust toolchain.
-        run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
-      - name: Run clippy.
-        run: cargo clippy
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: ${{ env.RUST_VERSION }}
+          components: clippy
+      - run: cargo clippy --all-features
 
   # Compute code coverage
   codecov:
     needs: test
     name: Code coverage
     runs-on: ubuntu-latest
     steps:
-      - name: Checkout.
-        uses: actions/checkout@v3
-      - name: Install Rust toolchain.
-        run: curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain ${{ env.RUST_VERSION }}
-      - name: Setup cargo-tarpaulin.
-        run: cargo install cargo-tarpaulin
-      - name: Run tarpaulin to compute coverage.
-        run: cargo tarpaulin --verbose --lib --examples --all-features --out xml
+      - uses: actions/checkout@v4
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          toolchain: ${{ env.RUST_VERSION }}
+      # Install action using cargo-binstall, which is faster because we don't have to compile tarpaulin every time.
+      - uses: taiki-e/install-action@v2
+        with:
+          tool: cargo-tarpaulin
+      - run: cargo tarpaulin --verbose --lib --examples --all-features --out xml
       - name: Upload to codecov.io
-        uses: codecov/codecov-action@v1.0.2
+        uses: codecov/codecov-action@v4
         with:
           token: ${{ secrets.CODECOV_TOKEN }}
       - name: Archive code coverage results
-        uses: actions/upload-artifact@v1
+        uses: actions/upload-artifact@v4
         with:
           name: code-coverage-report
           path: cobertura.xml

Cargo.toml

@@ -1,6 +1,6 @@
 [package]
 name = "biodivine-hctl-model-checker"
-version = "0.3.0"
+version = "0.3.1"
 authors = ["Ondřej Huvar <[email protected]>", "Samuel Pastva <[email protected]>"]
 edition = "2021"
 description = "Library for symbolic HCTL model checking on partially defined Boolean networks."
@@ -25,8 +25,8 @@ name = "convert-aeon-to-bnet"
 path = "src/bin/convert_aeon_to_bnet.rs"
 
 [dependencies]
-biodivine-lib-bdd = ">=0.5.7, <1.0.0"
-biodivine-lib-param-bn = ">=0.5.1, <1.0.0"
+biodivine-lib-bdd = ">=0.5.22, <1.0.0"
+biodivine-lib-param-bn = ">=0.5.13, <1.0.0"
 clap = { version = "4.1.4", features = ["derive"] }
 rand = "0.8.5"
 termcolor = "1.1.2"

README.md

@@ -83,6 +83,10 @@ We use the following syntax:
   * forall x: `V{x}:`
 * parentheses: `(`, `)`
 
+We also allow to specify the hybrid operators using their names (prefixed by backslash): `\bind`, `\jump`, `\exists`, `\forall`.
+You can use this syntax to write a formula like `\bind {x}: AG EF {x}`.
+Note that the default for serialization is the short format above.
+
 The operator precedence is following (the lower, the stronger):
 * unary operators (negation + temporal): 1
 * binary temporal operators: 2