Verigraph

Software specification and verification tool based on graph rewriting.

Tutorial

In depth "how to" tutorials are available for each stable version at Releases.

Quick Start

Installing via Stack

First you must assure that stack is in version 1.6.0 or later. You can check the stack version with the command:

   $ stack --version

If the stack version is older, you can upgrade it by running:

  $ stack upgrade
  $ echo "export PATH=~/.local/bin:${PATH}" >> ~/.bashrc
  $ source ~/.bashrc

You may remove the previous installed stack package. Once you have cloned this repository, install verigraph by running:

  $ stack setup # Will download and configure ghc if it is not installed yet
  $ stack install

If there is an error saying /usr/bin/ld: cannot find -ltinfo, it means you don't have libtinfo.so in your /usr/lib directory (see judah/haskeline#57). You may install the lib package to fix this (In ubuntu the package libtinfo-dev installs this lib), and then run stack install again

If there is an error saying recompile with -fPIC, it can be fixed by the following command (see commercialhaskell/stack#2712).

  $ shopt -s globstar && sed -i 's/-fno-PIE/-no-pie/g' ~/.stack/programs/**/ghc-*/settings`

Installing via Cabal

Once you have cloned this repository, install verigraph by running:

  $ cabal install
  $ echo "export PATH=${PATH}:~/.cabal/bin" >> ~/.bashrc
  $ source ~/.bashrc

Usage

Run verigraph helper:

  $ verigraph --help

Some example grammars are provided in the grammars directory, try something like:

  $ verigraph analysis grammars/Pacman/pacman.ggx

If you use bash, you can enable autocompletion of verigraph options for the current session by running the following command.

  $ source <(verigraph --bash-completion-script "$(which verigraph)")

Modelling and Visualization

We use AGG to read and write the .ggx and .cpx files with the Graph Grammars and their analysis.

Contributing

We encourage you to contribute to Verigraph. Please check out the Contributing guidelines about how to proceed.

Everyone interacting in Verigraph and/or its tutorials, sub-projects' codebases and issue trackers is expected to follow the Contributor Covenant Code of Conduct.

License

Verigraph is released under the Apache 2.0 License