Merge pull request #3 from VeriFIT/maintain-updates

Maintenance updates

.github/workflows/ubuntu.yml → .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

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}"))
-```
+
+## 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. 

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