From 90613cfae799cd69729db451c059c8f2d205565a Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 19 Dec 2024 20:31:15 +0100 Subject: [PATCH 1/7] update macos workflow --- .github/workflows/macos.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml index d47cabf..76dc490 100644 --- a/.github/workflows/macos.yml +++ b/.github/workflows/macos.yml @@ -12,7 +12,7 @@ on: jobs: setup: - runs-on: macos-12 + runs-on: macos-15 steps: - uses: actions/checkout@v3 - name: Building MacOS dependencies From 418c262cb33d0e7cf0cafd9011171b731c4599df Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 19 Dec 2024 21:01:25 +0100 Subject: [PATCH 2/7] README: updates --- README.md | 74 ++++++++++++++----------------------------------------- 1 file changed, 19 insertions(+), 55 deletions(-) diff --git a/README.md b/README.md index 21f89a4..dc82872 100644 --- a/README.md +++ b/README.md @@ -1,73 +1,37 @@ -# Kofola: modular complementation and inclusion checking for omega automata +# Kofola: Modular Complementation and Inclusion Checking for Omega Automata -Kofola has been built on top of [SPOT](https://spot.lrde.epita.fr/) and +Kofola is an open source tool for an efficient complementation and inclusion checking +of automata over infinite words (omega automata). Kofola has been built on top of [SPOT](https://spot.lrde.epita.fr/) and inspired by [Seminator](https://github.com/mklokocka/seminator) and -[COLA](https://github.com/liyong31/COLA). +[COLA](https://github.com/liyong31/COLA). -### Requirements +### Requirements and dependencies + +For a successful build of Kofola, `cmake` of version 3.16 (or higher) together with a C++ compiler with a support of C++-17 standard is required. Additional requirements +include: + * [Spot](https://spot.lrde.epita.fr/) +For Debian-like systems, Spot can be installed using the package `libspot-dev`. +For building Spot from sources, download the recent version and run: ``` -./configure --enable-max-accsets=128 +./configure ``` -One can set the maximal number of colors for an automaton when configuring Spot with --enable-max-accsets=INT +One can set the maximal number of colors for an automaton when configuring Spot with `--enable-max-accsets=INT`. ``` -make && make install +make +sudo make install ``` -### Compilation +### Building Kofola Please run the following steps to compile Kofola after cloning this repo: ``` mkdir build && cd build -cmake .. +cmake -DCMAKE_BUILD_TYPE=Release .. make ``` -Then you will get an executable in `build/src/kofola`. - -To use `kofola` for HyperLTL model checking, an example of execution is as follows (assuming we are in `build` directory): -``` -./src/kofola --hyperltl_mc ../hyperltl_ex/bp/concur_p1_1bit.hoa ../hyperltl_ex/bp/gni.hq -``` - -To use `kofola` for inclusion checking, an example of execution is as follows (assuming we are in `build` directory): -``` -./src/kofola --inclusion ../inclusion_ex/bakery_3procs_bakery_formula_S2_3proc_A.hoa ../inclusion_ex/bakery_3procs_bakery_formula_S2_3proc_B.hoa -``` +Then you will get an executable in `build/src/kofola`. Alternatively you can +run `make release` in the root directory. -### HyperLTL MC input formats -#### System -As input format for system behavior, we decided to use the HOA format so that it can -be easily parsed and stored by Spot as a Kripke structure. An example: -``` -HOA: v1 -States: 4 -Start: 3 -AP: 3 "h_0" "l_0" "o_0" -acc-name: all -Acceptance: 0 t -properties: state-labels explicit-labels state-acc deterministic ---BODY-- -State: [!0&!1&!2] 2 -3 -State: [!0&!1&!2] 3 -4 -State: [2&!0&!1] 4 -5 -State: [2&!0&!1] 5 -2 ---END-- -``` -#### Formula -For LTL body of the HyperLTL formula we support the exact format that `Spot` supports. However, each atomic proposition (AP) -is of the format `{ap_sys}_{trace_var}` with `ap_sys` standing for the atomic proposition used within the system and -`trace_var` stands for the quantified trace. The `f` formula with quantifiers is then generated by the following syntax: -``` - f ::= ((forall trace_var.)* (exists trace_var.)*)* LTL - trace_var ::= string -``` -An example of a property for the above system: -``` -forall A. forall B. exists C. (G ("{h_0}_{A}" <-> "{h_0}_{C}")) & (G("{l_0}_{B}" <-> "{l_0}_{C}")) -``` \ No newline at end of file From e9a78532e36eb3997f61431f78cad0c9c1e0b61d Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 19 Dec 2024 21:03:07 +0100 Subject: [PATCH 3/7] actions: various platform build workflow --- .github/workflows/build.yml | 40 +++++++++++++++++++++++++++++++++++++ 1 file changed, 40 insertions(+) create mode 100644 .github/workflows/build.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml new file mode 100644 index 0000000..9dac702 --- /dev/null +++ b/.github/workflows/build.yml @@ -0,0 +1,40 @@ +name: Various platforms (build-&-test) + +on: + push: + branches: + - master + - devel + pull_request: + branches: + - master + - devel + # allows to run the action from GitHub UI + workflow_dispatch: + + +jobs: + setup: + runs-on: ubuntu-latest + steps: + - name: Check out repository code + uses: actions/checkout@v3 + - name: Install dependencies + run: sudo wget -O /etc/apt/trusted.gpg.d/lrde.gpg https://www.lrde.epita.fr/repo/debian.gpg + - run: sudo sudo sh -c "echo 'deb http://www.lrde.epita.fr/repo/debian/ unstable/' >> /etc/apt/sources.list" + - run: sudo apt-get update + - run: sudo apt-get install -y spot libspot-dev python3-spot libspot0 libspotgen0 libspotltsmin0 + - name: Compile release + run: make release + - name: Test release + run: make test + setup: + runs-on: macos-15 + steps: + - uses: actions/checkout@v3 + - name: Building MacOS dependencies + run: brew install spot + - name: Compile + run: make release + - name: Test the library + run: make test \ No newline at end of file From 7d2e605ee73c6d49cb874f5f07b1fbf6da14117a Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 19 Dec 2024 21:06:44 +0100 Subject: [PATCH 4/7] actions: build.yml fixing --- .github/workflows/build.yml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 9dac702..3d038c7 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -14,7 +14,8 @@ on: jobs: - setup: + ubuntu-build: + name: "Ubuntu (build-&-test)" runs-on: ubuntu-latest steps: - name: Check out repository code @@ -28,7 +29,8 @@ jobs: run: make release - name: Test release run: make test - setup: + macos-build: + name: "MACOS (build-&-test)" runs-on: macos-15 steps: - uses: actions/checkout@v3 From 88eb17b8554217229b3038da5c80bcfc5ae40b7f Mon Sep 17 00:00:00 2001 From: vhavlena Date: Thu, 19 Dec 2024 21:10:10 +0100 Subject: [PATCH 5/7] action: update workflow; README build result --- .github/workflows/build.yml | 2 +- .github/workflows/macos.yml | 23 ----------------------- .github/workflows/ubuntu.yml | 32 -------------------------------- README.md | 2 ++ 4 files changed, 3 insertions(+), 56 deletions(-) delete mode 100644 .github/workflows/macos.yml delete mode 100644 .github/workflows/ubuntu.yml diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 3d038c7..5d56f56 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -30,7 +30,7 @@ jobs: - name: Test release run: make test macos-build: - name: "MACOS (build-&-test)" + name: "MacOS (build-&-test)" runs-on: macos-15 steps: - uses: actions/checkout@v3 diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml deleted file mode 100644 index 76dc490..0000000 --- a/.github/workflows/macos.yml +++ /dev/null @@ -1,23 +0,0 @@ -name: MacOS (build-&-test) - -on: - push: - branches: - - master - - devel - pull_request: - branches: - - master - - devel - -jobs: - setup: - runs-on: macos-15 - steps: - - uses: actions/checkout@v3 - - name: Building MacOS dependencies - run: brew install spot - - name: Compile - run: make release - - name: Test the library - run: make test diff --git a/.github/workflows/ubuntu.yml b/.github/workflows/ubuntu.yml deleted file mode 100644 index 990af64..0000000 --- a/.github/workflows/ubuntu.yml +++ /dev/null @@ -1,32 +0,0 @@ -# copied from https://github.com/VeriFIT/mata/blob/84590550390b0d4003c83cd618c532b1959c752a/.github/workflows/ubuntu.yml - -name: Ubuntu (build-&-test) - -on: - push: - branches: - - master - - devel - pull_request: - branches: - - master - - devel - # allows to run the action from GitHub UI - workflow_dispatch: - - -jobs: - setup: - runs-on: ubuntu-latest - steps: - - name: Check out repository code - uses: actions/checkout@v3 - - name: Install dependencies - run: sudo wget -O /etc/apt/trusted.gpg.d/lrde.gpg https://www.lrde.epita.fr/repo/debian.gpg - - run: sudo sudo sh -c "echo 'deb http://www.lrde.epita.fr/repo/debian/ unstable/' >> /etc/apt/sources.list" - - run: sudo apt-get update - - run: sudo apt-get install -y spot libspot-dev python3-spot libspot0 libspotgen0 libspotltsmin0 - - name: Compile release - run: make release - - name: Test release - run: make test diff --git a/README.md b/README.md index dc82872..a6b0457 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,7 @@ # Kofola: Modular Complementation and Inclusion Checking for Omega Automata +![build workflow](https://github.com/VeriFIT/kofola/actions/workflows/build.yml/badge.svg) + Kofola is an open source tool for an efficient complementation and inclusion checking of automata over infinite words (omega automata). Kofola has been built on top of [SPOT](https://spot.lrde.epita.fr/) and inspired by [Seminator](https://github.com/mklokocka/seminator) and From dfd834e4a24451aadd1c4dc2b5b1ce0aa14e641e Mon Sep 17 00:00:00 2001 From: vhavlena Date: Fri, 20 Dec 2024 20:57:21 +0100 Subject: [PATCH 6/7] README: usage and publications --- README.md | 29 +++++++++++++++++++++++++++++ src/main.cpp | 2 +- 2 files changed, 30 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index a6b0457..093df8c 100644 --- a/README.md +++ b/README.md @@ -37,3 +37,32 @@ make Then you will get an executable in `build/src/kofola`. Alternatively you can run `make release` in the root directory. +### Basic usage +Kofola assumes input omega automata in HOA format. The following command +translates general (nondeterministic) omega-automaton stored in file `A.hoa` into a complementary +omega automaton and prints it to the standard output: + +``` +./kofola A.hoa --complement +``` + +Note that Kofola produces automata with a general accepting condition (different output type might be specified +by `--tba` for transition-based Büchi automata or `--tgba` for transition-based +generalized Büchi automata). + +The following command then checks if the language specified by the omega automaton `A.hoa` +is included in the language specified by `B.hoa` and prints the result to the standard output: + +``` +./kofola A.hoa B.hoa --inclusion +``` + +Additional parameters might be passed using `--params`, e.g., `--params=merge_iwa=True`. +In order to get a program help, run + +``` +./kofola --help +``` + +### Publications +- V. Havlena, O. Lengál, Y. Li, B. Šmahlíková and A. Turrini. [Modular Mix-and-Match Complementation of Büchi Automata](https://link.springer.com/chapter/10.1007/978-3-031-30823-9_13). In *Proc. of TACAS'23*, volume 13993 of LNCS, pages 249-270, 2023. Springer. \ No newline at end of file diff --git a/src/main.cpp b/src/main.cpp index 6700f6d..69b2ee2 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -189,7 +189,7 @@ int process_args(int argc, char *argv[], kofola::options* params) { // {{{ assert(nullptr !=params); - args::ArgumentParser parser("kofola: modular complementation of omega-automata."); + args::ArgumentParser parser("kofola: Modular complementation and inclusion checking of omega-automata."); args::CompletionFlag completion(parser, {"complete"}); // inputs From 790a8e8e4d4454aadae439f896a889b0d562e917 Mon Sep 17 00:00:00 2001 From: vhavlena Date: Fri, 20 Dec 2024 20:58:25 +0100 Subject: [PATCH 7/7] README: headline font size --- README.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index 093df8c..7009e23 100644 --- a/README.md +++ b/README.md @@ -8,7 +8,7 @@ inspired by [Seminator](https://github.com/mklokocka/seminator) and [COLA](https://github.com/liyong31/COLA). -### Requirements and dependencies +## Requirements and dependencies For a successful build of Kofola, `cmake` of version 3.16 (or higher) together with a C++ compiler with a support of C++-17 standard is required. Additional requirements include: @@ -26,7 +26,7 @@ make sudo make install ``` -### Building Kofola +## Building Kofola Please run the following steps to compile Kofola after cloning this repo: ``` mkdir build && cd build @@ -37,7 +37,7 @@ make Then you will get an executable in `build/src/kofola`. Alternatively you can run `make release` in the root directory. -### Basic usage +## Basic usage Kofola assumes input omega automata in HOA format. The following command translates general (nondeterministic) omega-automaton stored in file `A.hoa` into a complementary omega automaton and prints it to the standard output: @@ -64,5 +64,5 @@ In order to get a program help, run ./kofola --help ``` -### Publications +## Publications - V. Havlena, O. Lengál, Y. Li, B. Šmahlíková and A. Turrini. [Modular Mix-and-Match Complementation of Büchi Automata](https://link.springer.com/chapter/10.1007/978-3-031-30823-9_13). In *Proc. of TACAS'23*, volume 13993 of LNCS, pages 249-270, 2023. Springer. \ No newline at end of file