diff --git a/.github/workflows/ubuntu.yml b/.github/workflows/build.yml similarity index 67% rename from .github/workflows/ubuntu.yml rename to .github/workflows/build.yml index 990af64..5d56f56 100644 --- a/.github/workflows/ubuntu.yml +++ b/.github/workflows/build.yml @@ -1,6 +1,4 @@ -# copied from https://github.com/VeriFIT/mata/blob/84590550390b0d4003c83cd618c532b1959c752a/.github/workflows/ubuntu.yml - -name: Ubuntu (build-&-test) +name: Various platforms (build-&-test) on: push: @@ -16,7 +14,8 @@ on: jobs: - setup: + ubuntu-build: + name: "Ubuntu (build-&-test)" runs-on: ubuntu-latest steps: - name: Check out repository code @@ -30,3 +29,14 @@ jobs: run: make release - name: Test release run: make test + macos-build: + name: "MacOS (build-&-test)" + 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 diff --git a/.github/workflows/macos.yml b/.github/workflows/macos.yml deleted file mode 100644 index d47cabf..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-12 - 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/README.md b/README.md index 21f89a4..7009e23 100644 --- a/README.md +++ b/README.md @@ -1,73 +1,68 @@ -# 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 +![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 -[COLA](https://github.com/liyong31/COLA). +[COLA](https://github.com/liyong31/COLA). + + +## 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: -### Requirements * [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`. +Then you will get an executable in `build/src/kofola`. Alternatively you can +run `make release` in the root directory. -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 -``` +## 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: -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 +./kofola A.hoa --complement ``` -### 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-- +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: + ``` -#### 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: +./kofola A.hoa B.hoa --inclusion ``` - f ::= ((forall trace_var.)* (exists trace_var.)*)* LTL - trace_var ::= string + +Additional parameters might be passed using `--params`, e.g., `--params=merge_iwa=True`. +In order to get a program help, run + ``` -An example of a property for the above system: +./kofola --help ``` -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 + +## 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