graphedit-ntta

Networks of Tick Tock Automata (NTTA) for graphedit: a plugin that provides the syntax of NTTA models, checks them while they are edited, and imports and exports H-UPPAAL projects. Run and verify the models with aaltitoad.

This is the C++/Qt edition of the NTTA plugin of graphedit 1.x (the Java edition, nttals), whose models it reads.

Features

• The NTTA syntax: templates of tick tock automata made of locations (initial, final and immediate ones), nails that carry the guards, updates and comments of edges, and subcomponents that instantiate other templates. See the syntax.
• Views: locations as circles (immediate ones as squares, with an arrow at the initial and a double outline at the final location), nails in the colors of their kinds with their expressions next to them, subcomponents as boxes, and a frame from the initial to the final location of templates (like the components of H-UPPAAL).
• Editing: Shift + click a connection to put a nail on it, G/U/C make nails guards, updates and comments, I makes locations immediate.
• The NTTA checker: a language server that checks the structure of templates, the syntax of guards, updates and declarations and how templates instantiate each other across the network. See checking models.
• H-UPPAAL import and export: components become templates and part files declarations, faithfully enough to import the whole Safecon3 project, and the export writes NTTA models as H-UPPAAL projects, which the current release of aaltitoad runs. See H-UPPAAL projects.
• aaltitoad (optional): aaltitoad-ls checks what only aaltitoad knows about a network (e.g. undeclared variables) and debugs networks in the editor: step through ticks, set breakpoints, change variables. See Debugging.
• graphedit 1.x models of the hawk syntax are converted when they are opened.
• Everything works headless as well: agents build, check, import and export models 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 (NTTA_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). scripts/ci.sh runs the complete verification pipeline, and the docker directory has container images for it.

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 installation contains graphedit with the plugin in its plugin directory. Built against an installed graphedit (CPM_USE_LOCAL_PACKAGES), only the plugin is installed, into the plugin directory of that graphedit (NTTA_PLUGIN_INSTALL_DIR changes that). The plugins panel of graphedit also installs the plugin from the plugin database, which lists the libraries of the releases (for Linux on x86-64, with Qt 6.5 or newer). Then, for example:

graphedit-cli init lights && cd lights
graphedit-cli call model.create model=light.json syntax=NTTA 'name=Light(id)'
graphedit-cli call syntax.describe syntax=NTTA
graphedit-cli call project.import importer=huppaal 'paths:=["/path/to/h-uppaal/project"]'
graphedit-cli validate
graphedit-cli call model.export exporter=huppaal directory=out    # an H-UPPAAL project for aaltitoad

Documentation

Document	Contents
The syntax	Locations, nails, subcomponents, templates, expressions and the file format
Checking models	The diagnostics of the checker, and how aaltitoad joins in
Debugging	Debugging networks with aaltitoad
H-UPPAAL projects	How H-UPPAAL projects become NTTA models, and NTTA models H-UPPAAL projects
AGENTS.md	Guidelines for working on the code (humans and AI agents)

Repository layout

Directory	Contents
src/graphedit/ntta	the syntax, the checker, H-UPPAAL import and export, the tools and aaltitoad
src/graphedit/ntta/gui	the views of the syntax (Qt Widgets)
src/plugin	the plugins: NTTA and NTTA Views (graphical)
tests	the tests (QtTest), with test data and a stand-in for aaltitoad
docs	documentation
scripts, docker, cmake	developer scripts, container images and build helpers

License

MIT, see LICENSE.