graphedit-tapn

Timed-arc Petri nets (TAPN) for graphedit: a plugin that provides the syntax of timed-arc Petri nets as TAPAAL knows them, checks and debugs them with verifytapn-ls (the language server of TAPAAL's verification engine verifytapn), and imports and exports TAPAAL nets.

Features

• The TAPN syntax: places with tokens of ages and invariants, transitions (urgent and shared ones), arcs with intervals, transport arcs and inhibitor arcs. The models of a project are the components of one net, which share places and transitions like the components of TAPAAL. Queries (done: EF Done >= 1) are written in the declarations. See the syntax.
• Views: places are circles with their tokens, transitions are bars (urgent ones with a dot), shared elements have a double outline, and arcs show their intervals, transport groups and weights (transport arcs are dashed, inhibitor arcs end in a circle). Labels show names and invariants and can be dragged.
• Editing: N names unnamed places and transitions the way TAPAAL does (P0, T0...), S shares or unshares them.
• Checking with verifytapn-ls: what keeps verifytapn from verifying the net (urgent transitions, weights, invalid inscriptions and names, unpaired transport arcs, invalid queries...) and what is probably a mistake (dead transitions, places that are never marked, guards that the invariants rule out...). See verifytapn.
• Debugging with verifytapn-ls: simulate the net in the editor, step by step (fire transitions, let time pass), with breakpoints, and verify a query with verifytapn and follow its trace.
• TAPAAL import and export of .tapn files: components, shared places and transitions, transport and inhibitor arcs, token ages, constants and queries. See TAPAAL nets.
• Everything works headless as well: agents build, check, import, export and debug nets with graphedit-cli and its Model Context Protocol server.

Build

Requirements: what graphedit requires: a C++20 compiler, CMake 3.25+, Ninja and Qt 6.5+ (Core, Network, Gui, Widgets and Svg).

cmake --preset debug            # configure (see CMakePresets.json for the other presets)
cmake --build --preset debug    # build graphedit and the plugin
ctest --preset debug            # run the tests

graphedit is built with the plugin: CPM.cmake fetches its release (TAPN_GRAPHEDIT_VERSION in CMakeLists.txt) into .cpm-cache. -DCPM_graphedit_SOURCE=../graphedit-qt builds a checkout of graphedit-qt instead, and -DCPM_USE_LOCAL_PACKAGES=ON uses an installed graphedit of the release (set CMAKE_PREFIX_PATH). -DTAPN_VERIFYTAPN_LS=<path to verifytapn-ls> runs the end-to-end tests with verifytapn-ls (they are skipped without it). scripts/ci.sh runs the complete verification pipeline, and the docker directory has a container image that builds the plugin libraries of releases.

Usage

build/debug/_deps/graphedit-build/bin/graphedit --plugin-dir build/debug/plugins my-project  # the editor and the plugin
cmake --install build/release --prefix ~/.local                                             # or install both

The plugins panel of graphedit also installs the plugin from the plugin database: install both TAPN and TAPN Views. Then install verifytapn-ls (see verifytapn), for example next to the plugins, in ~/.local/share/graphedit/plugins. Then, for example:

graphedit-cli init lights && cd lights
graphedit-cli call model.create model=net.json syntax=TAPN name=Net
graphedit-cli call syntax.describe syntax=TAPN
graphedit-cli call project.import importer=tapn 'paths:=["/path/to/net.tapn"]'
graphedit-cli validate
graphedit-cli call model.export exporter=tapn directory=out    # TAPAAL nets

Documentation

Document	Contents
The syntax	Places, transitions, arcs, components, queries, editing and the file format
verifytapn	Checking and debugging nets with verifytapn-ls
TAPAAL nets	How TAPAAL nets become TAPN models, and TAPN models TAPAAL nets
AGENTS.md	Guidelines for working on the code (humans and AI agents)

Repository layout

Directory	Contents
src/graphedit/tapn	the syntax, the TAPAAL import and export, the tool and the language server
src/graphedit/tapn/gui	the views of the syntax (Qt Widgets)
src/plugin	the plugins: TAPN and TAPN Views (graphical)
tests	the tests (QtTest), with test data
docs	documentation
scripts, docker, cmake	developer scripts, the container image of releases and build helpers

License

MIT, see LICENSE.