Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .editorconfig
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ indent_size = 4
insert_final_newline = true
trim_trailing_whitespace = true

[*.{md,toml,yml,yaml,nix,html,css}]
[{*.{md,toml,yml,yaml,nix,html,css,just},justfile}]
indent_size = 2

[{**/Makefile,**/CMakeLists.txt}]
Expand Down
39 changes: 22 additions & 17 deletions CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -121,43 +121,48 @@ add_subdirectory (3rdparty/re2 EXCLUDE_FROM_ALL)
add_subdirectory (3rdparty/simlib EXCLUDE_FROM_ALL)
add_subdirectory (3rdparty/cudd EXCLUDE_FROM_ALL)

if (MATA_BUILD_EXAMPLES)
if ((CMAKE_PROJECT_NAME STREQUAL PROJECT_NAME) AND MATA_BUILD_EXAMPLES)
message ("-- Building examples")
add_subdirectory (examples)
endif ()

# Build tests only if Mata is the main project and we enabled testing
if ((CMAKE_PROJECT_NAME STREQUAL PROJECT_NAME) AND BUILD_TESTING)
message ("-- Building tests")
add_subdirectory (tests)
add_subdirectory (tests-integration)
endif ()


##### INSTALLING AND UNINSTALLING #####
install (TARGETS libmata cudd_headers simlib_headers
EXPORT mataTargets
install (
TARGETS libmata cudd_headers simlib_headers
EXPORT mataTargets
ARCHIVE DESTINATION lib
)
# TODO: should headers be installed in some nicer way? there is something called FILE_SET in cmake, but I do not feel it will make it better
install(
DIRECTORY
${PROJECT_SOURCE_DIR}/include/
${PROJECT_SOURCE_DIR}/3rdparty/cudd/include/ # TODO remove this after we remove PUBLIC dependency on CUDD
${PROJECT_SOURCE_DIR}/3rdparty/simlib/include/ # TODO remove this after we remove PUBLIC dependency on simlib
DESTINATION include
DIRECTORY
${PROJECT_SOURCE_DIR}/include/
${PROJECT_SOURCE_DIR}/3rdparty/cudd/include/ # TODO remove this after we remove PUBLIC dependency on CUDD
${PROJECT_SOURCE_DIR}/3rdparty/simlib/include/ # TODO remove this after we remove PUBLIC dependency on simlib
DESTINATION include
)
install(EXPORT mataTargets
# NAMESPACE mata:: # for modern cmake, commented out because I am not sure what could break with it
DESTINATION lib/cmake/mata
install(
EXPORT mataTargets
# NAMESPACE mata:: # for modern cmake, commented out because I am not sure what could break with it
DESTINATION lib/cmake/mata
)

include(CMakePackageConfigHelpers)
configure_package_config_file(
cmake/mataConfig.cmake.in # your template
"${CMAKE_CURRENT_BINARY_DIR}/mataConfig.cmake" # output
INSTALL_DESTINATION lib/cmake/mata
configure_package_config_file(cmake/mataConfig.cmake.in
"${CMAKE_CURRENT_BINARY_DIR}/mataConfig.cmake"
INSTALL_DESTINATION lib/cmake/mata
)
install(
FILES "${CMAKE_CURRENT_BINARY_DIR}/mataConfig.cmake"
DESTINATION lib/cmake/mata
)
install(FILES "${CMAKE_CURRENT_BINARY_DIR}/mataConfig.cmake"
DESTINATION lib/cmake/mata)


# Uninstall target from https://gitlab.kitware.com/cmake/community/-/wikis/FAQ#can-i-do-make-uninstall-with-cmake
Expand Down
37 changes: 24 additions & 13 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -49,34 +49,34 @@ The Mata library further depends on the following libraries, included in the `./

To build the library, run the following:

```
```shell
git clone https://github.com/VeriFIT/mata
cd mata
make release
```

In order to install the library, you can run

```
```shell
sudo make install
```

In order to verify the functionality of the library, you can run the test suite:

```
```shell
make test
```

You might, need to install the dependencies to measure the coverage of the tests.
Run the following to install the dependencies for MacOS:

```
```shell
brew install lcov gcovr
```

Run the following to install the dependencies for Ubuntu:

```
```shell
sudo apt install -y build-essential lcov gcovr xdg-utils
```

Expand All @@ -87,9 +87,12 @@ package on your system as follows.

### Installation from PyPI

To install a latest version from the PyPI repository, run
To install a latest version from the PyPI repository, run:

```
```shell
# Using uv:
uv add libmata
# Or using pip:
pip3 install libmata
```

Expand All @@ -98,7 +101,15 @@ pip3 install libmata
To build from sources first, install the necessary requirements for Python and your
system. We recommend using the virtual environemnt (`venv`) to install and use the library.

Using `uv`:

```shell
uv sync --python 3.13
```

Or using `pip`:

```shell
python -m pip install --upgrade pip
make -C bindings/python init

Expand All @@ -108,13 +119,13 @@ sudo apt -qq install -y graphviz graphviz-dev

Now, you can install the library.

```
```shell
make -C bindings/python install
```

Finally, you can verify the binding woks as expected by running the test suite:

```
```shell
make -C bindings/python test
```

Expand All @@ -125,21 +136,21 @@ This directory contains examples of various usage in form of:

1. C/C++ example programs. By default, they are built with the library. To run for example the first example:

```
```shell
./build/examples/example01-simple
```

3. Python example scripts. To run the scripts run the following.

```
python examples/example01-python-binding.py
```shell
python3 examples/example01-python-binding.py
```

4. Python jupyter notebooks. To run the jupyter notebook, one needs to have jupyter installed as
a prerequisite. The run the jupyter notebook, that creates an instance on your local server.
Navigate to generated link to see the available jupyter notebooks:

```
```shell
pip3 install jupyter
jupyter notebook
```
Expand Down
14 changes: 7 additions & 7 deletions bindings/python/libmata/nfa/nfa.pyx
Original file line number Diff line number Diff line change
Expand Up @@ -326,17 +326,17 @@ cdef class Nfa:
"""
self.thisptr.get().final.erase(state)

def clear_final(self) -> Self:
def clear_final(self) -> Nfa:
"""Clears final state set of the automaton."""
self.thisptr.get().final.clear()
return self

def unify_initial(self, bool force_new_state = False) -> Self:
def unify_initial(self, bool force_new_state = False) -> Nfa:
"""Unify initial states into a single new initial state."""
self.thisptr.get().unify_initial(force_new_state)
return self

def unify_final(self, bool force_new_state = False) -> Self:
def unify_final(self, bool force_new_state = False) -> Nfa:
"""Unify final states into a single new final state."""
self.thisptr.get().unify_final(force_new_state)

Expand Down Expand Up @@ -518,7 +518,7 @@ cdef class Nfa:
Remove states which are not accessible (unreachable; state is accessible when the state is the endpoint of a path
starting from an initial state) or not co-accessible (non-terminating; state is co-accessible when the state is
the starting point of a path ending in a final state).
:return: Self.
:return: Nfa.
"""
self.thisptr.get().trim(NULL)
return self
Expand All @@ -530,7 +530,7 @@ cdef class Nfa:
starting from an initial state) or not co-accessible (non-terminating; state is co-accessible when the state is
the starting point of a path ending in a final state).

:return: Self, State map of original to new states.
:return: Nfa, State map of original to new states.
"""
cdef StateRenaming state_map
self.thisptr.get().trim(&state_map)
Expand All @@ -539,15 +539,15 @@ cdef class Nfa:
def concatenate(self, Nfa other) -> Nfa:
"""Concatenate 'self' with 'other' in-place.

:return: Self
:return: Nfa
"""
self.thisptr.get().concatenate(dereference(other.thisptr.get()))
return self

def union(self, Nfa other) -> Nfa:
"""Make union of 'self' with 'other' in-place.

:return: Self
:return: Nfa
"""
self.thisptr.get().unite_nondet_with(dereference(other.thisptr.get()))
return self
Expand Down
26 changes: 21 additions & 5 deletions bindings/python/pyproject.toml
Original file line number Diff line number Diff line change
@@ -1,24 +1,40 @@
[project]
name = "libmata"
dynamic = ["version"]
description = "Mata Python bindings"
description = "Python bindings for Mata: A fast and simple automata library"
readme = "README.md"
requires-python = ">=3.13"
keywords = ["automata", "finite automata", "alternating automata"]
authors = [
{ name = "Lukáš Holík", email = "holik@fit.vutbr.cz" },
{ name = "Ondřej Lengál", email = "lengal@fit.vutbr.cz" },
{ name = "Martin Hruška", email = "ihruskam@fit.vutbr.cz" },
{ name = "Tomáš Fiedor", email = "ifiedortom@fit.vutbr.cz" },
{ name = "David Chocholatý", email = "chocholaty.david@protonmail.com" },
{ name = "Juraj Síč", email = "sicjuraj@fit.vutbr.cz" },
{ name = "Tomáš Vojnar", email = "vojnar@fit.vutbr.cz" },
]
dependencies = [
"coverage>=6.4.1",
"cython>=0.29.32",
"graphviz>=0.20.0",
"ipykernel>=7.2.0",
"graphviz>=0.20.1",
"ipykernel>=7.1.0",
"ipython>=7.9.0",
"networkx>=2.6.3",
"pandas>=1.3.5",
"papermill>=2.7.0",
"papermill>=2.6.0",
"pytest>=3.6.4",
"pytest-cov>=3.0.0",
"seaborn>=0.13.2",
"setuptools>=82.0.1",
"tabulate>=0.8.10",
]

[project.urls]
Homepage = "https://github.com/VeriFIT/mata"

[tool.setuptools]
packages = ["libmata", "libmata.nfa"]

[build-system]
requires = ["setuptools", "wheel", "Cython>=0.29.32"]
build-backend = "setuptools.build_meta"
35 changes: 2 additions & 33 deletions bindings/python/setup.py
Original file line number Diff line number Diff line change
Expand Up @@ -249,38 +249,7 @@ def run_safely_external_command(


setup(
name="libmata",
packages=["libmata", "libmata.nfa"],
package_dir={'libmata': 'libmata', 'libmata.nfa': os.path.join('libmata', 'nfa')},
version=get_version(),
ext_modules=cythonize(
extensions,
compiler_directives={'language_level': "3"}
),
description="The automata library",
author="Lukáš Holík <holik@fit.vutbr.cz>, "
"Ondřej Lengál <lengal@fit.vutbr.cz>, "
"Martin Hruška <ihruskam@fit.vutbr.cz>, "
"Tomáš Fiedor <ifiedortom@fit.vutbr.cz>, "
"David Chocholatý <chocholaty.david@protonmail.com>, "
"Juraj Síč <sicjuraj@fit.vutbr.cz>, "
"Tomáš Vojnar <vojnar@fit.vutbr.cz>",
author_email="holik@fit.vutbr.cz",
long_description=README_MD,
long_description_content_type="text/markdown",
keywords="automata, finite automata, alternating automata",
url="https://github.com/verifit/mata",
cmdclass={
'sdist': sdist,
'build_ext': build_ext
},
# Requirements from install for pip
install_requires=[
'Cython>=0.29.32',
'tabulate>=0.8.10',
'ipython>=7.9.0',
'pandas>=1.3.5',
'networkx>=2.6.3',
'graphviz>=0.10.1',
]
ext_modules=cythonize(extensions, compiler_directives={"language_level": "3"}),
cmdclass={"sdist": sdist, "build_ext": build_ext},
)
12 changes: 7 additions & 5 deletions examples/CMakeLists.txt
Original file line number Diff line number Diff line change
@@ -1,6 +1,8 @@
file(GLOB MATA_EXAMPLES "${CMAKE_CURRENT_SOURCE_DIR}/*.cc")
file(GLOB_RECURSE MATA_EXAMPLES CONFIGURE_DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/*.cc")
foreach(MATA_EXAMPLE ${MATA_EXAMPLES})
get_filename_component(MATA_EXAMPLE_NAME ${MATA_EXAMPLE} NAME_WE)
add_executable(${MATA_EXAMPLE_NAME} ${MATA_EXAMPLE})
target_link_libraries(${MATA_EXAMPLE_NAME} PRIVATE libmata)
endforeach()
file(RELATIVE_PATH MATA_EXAMPLE_REL "${CMAKE_CURRENT_SOURCE_DIR}" "${MATA_EXAMPLE}")
string(REPLACE "/" "-" MATA_EXAMPLE_NAME "${MATA_EXAMPLE_REL}")
string(REPLACE ".cc" "" MATA_EXAMPLE_NAME "${MATA_EXAMPLE_NAME}")
add_executable(${MATA_EXAMPLE_NAME} ${MATA_EXAMPLE})
target_link_libraries(${MATA_EXAMPLE_NAME} PRIVATE libmata)
endforeach()
24 changes: 24 additions & 0 deletions examples/Makefile
Original file line number Diff line number Diff line change
@@ -0,0 +1,24 @@
# Makefile wrapper for building/running selected MATA examples via CMake.

ROOT_DIR ?= ..
BUILD_DIR ?= $(ROOT_DIR)/build
CMAKE_BUILD_TYPE ?= Debug
JOBS ?= 6

EXAMPLE ?= example01-simple

.PHONY: all configure build run clean

all: build

configure:
cmake -S $(ROOT_DIR) -B $(BUILD_DIR) -DCMAKE_BUILD_TYPE=$(CMAKE_BUILD_TYPE)

build: configure
cmake --build $(BUILD_DIR) --parallel $(JOBS)

run: build
$(BUILD_DIR)/examples/$(EXAMPLE)

clean:
rm -f $(BUILD_DIR)/examples/$(EXAMPLE)
1 change: 1 addition & 0 deletions examples/notebooks/jupytext.toml
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
formats = "ipynb,py:percent"
16 changes: 10 additions & 6 deletions examples/notebooks/run_papermill_examples.sh
Original file line number Diff line number Diff line change
@@ -1,9 +1,13 @@
#!/usr/bin/env sh
#!/usr/bin/env bash

set -euo pipefail

papermill ./example-01-ws1s-formulae.ipynb tmp_out.ipynb
papermill ./example-02-redos-attacks.ipynb tmp_out.ipynb
papermill ./example-03-exploring-maze.ipynb tmp_out.ipynb
papermill ./example-04-visualization.ipynb tmp_out.ipynb
rm tmp_out.ipynb
SCRIPT_DIR="$(dirname "$0")"

TMP_OUT="$(mktemp --tmpdir mata-papermill-XXXXXX.ipynb)"
trap 'rm -f "$TMP_OUT"' EXIT

for file in "$SCRIPT_DIR"/*.ipynb; do
echo "Running: $file."
papermill "$file" "$TMP_OUT"
done
Loading
Loading