File: README.rst

package info (click to toggle)
rumur 2020.12.20-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, sid
  • size: 3,292 kB
  • sloc: cpp: 17,090; ansic: 2,537; objc: 1,542; python: 1,120; sh: 538; yacc: 536; lex: 229; lisp: 15; makefile: 5
file content (99 lines) | stat: -rw-r--r-- 2,653 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
Rumur
=====
Rumur is a `model checker`_, a formal verification tool for proving safety and
security properties of systems represented as state machines. It is based on a
previous tool, CMurphi_, and intended to be close to a drop-in replacement.
Rumur takes the same input format as CMurphi, the Murphi modelling language,
with some extensions and generates a C program that implements a verifier.

Quickstart
----------

Installation on Ubuntu ≥ 20.04 or Debian Unstable
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

.. code-block:: sh

  apt install rumur

Installation on FreeBSD
~~~~~~~~~~~~~~~~~~~~~~~

.. code-block:: sh

  pkg install rumur

Thanks to `yuri@FreeBSD`_ for packaging.

.. _`yuri@FreeBSD`: https://github.com/yurivict

Building from Source
~~~~~~~~~~~~~~~~~~~~
First you will need to have the following dependencies installed:

* Either GCC_ or Clang_
* Bison_
* CMake_
* Flex_
* Libgmp_
* Python_ ≥ 3.6

Then:

.. code-block:: sh

  # Download Rumur
  git clone https://github.com/Smattr/rumur
  cd rumur

  # Configure and compile
  mkdir build
  cd build
  cmake ..
  make
  make install

  # Generate a checker
  rumur my-model.m --output my-model.c

  # Compile the checker (also pass -mcx16 if using GCC on x86-64)
  cc -std=c11 -O3 my-model.c -lpthread

  # Run the checker
  ./a.out

Compilation produces several artefacts including the `rumur` binary itself:

* rumur: Tool for translating a Murphi model into a program that implements
  a checker;
* murphi2c: Tool for translating a Murphi model into C code for use in a
  simulator;
* murphi2murphi: A preprocessor for Murphi models;
* murphi2xml: Tool for emitting an XML representation of a Murphi model’s
  Abstract Syntax Tree;
* librumur.a: A library for building your own Murphi model tools; and
* include/rumur/: The API for the above library.

Comparison with CMurphi
-----------------------
If you are migrating from CMurphi, you can read a comparison between the two
model checkers at `doc/vs-cmurphi.rst`_.

.. _doc/vs-cmurphi.rst: doc/vs-cmurphi.rst

Legal
-----
Everything in this repository is in the public domain, under the terms of
`the Unlicense`_. For the full text, see LICENSE_.

.. _Bison: https://www.gnu.org/software/bison/
.. _CMake: https://cmake.org/
.. _CMurphi: http://mclab.di.uniroma1.it/site/index.php/software/18-cmurphi
.. _Clang: https://clang.llvm.org/
.. _Flex: https://github.com/westes/flex
.. _GCC: https://gcc.gnu.org/
.. _Libgmp: https://gmplib.org/
.. _LICENSE: ./LICENSE
.. _`model checker`: https://en.wikipedia.org/wiki/Model_checking
.. _Python: https://www.python.org/
.. _`the Unlicense`: http://unlicense.org/