Because Rumur is attempting to appeal to CMurphi users, it is helpful to compare the feature set of the two. In this document we give a brief run down of the relevant differences.
CMurphi produces a single-threaded verifier. If you have a multicore system, the verifier will only take advantage of a single core. Rumur produces a multi-threaded verifier by default, which will use as many cores as you have available. You can tune how many threads are used with the --threads command line option when generating the verifier.
CMurphi seems intended to run on Linux and older Unix-style platforms. Rumur should run on any POSIX operating system. However, the verifier’s code does make use of C extensions that may only be supported by GCC and Clang.
CMurphi considers the operator == an error, while Rumur treats it as an alias of = that is usable in comparisons. This is mainly to ease the life of C/C++ programmers.
Rumur supports various single character operator alternatives, e.g. ≤. These are nicer for presentation of a model in a mathematical context. These more concise operators are generally recommended for use in models that are expected to be read more often than they are edited.
The keywords assert and invariant are distinct in CMurphi, whereas they are considered synonyms by Rumur. If one of these appears within a rule or function it is considered an assertion and if it appears at the top level it is considered an invariant. Rumur also accepts the optional string message of an assertion or invariant on either side of the asserted expression.
CMurphi supports real arithmetic using the real data type. Rumur does not support this type and there are no plans to implement this or any floating point support. Similarly, Rumur does not support the union type and there are no plans to add it.
In addition to assertions and invariants that are supported by CMurphi, Rumur supports assumptions with the keyword assume. Any state that fails an assumption is considered irrelevant and discarded. You can read more about this in properties.rst.
Another addition to the properties supported by CMurphi, is the Rumur-specific liveness. From every state that is reached during checking, there must be a state reachable from it that satisfies the liveness property. You can read more about this in properties.rst.
CMurphi has a limitation that = and != can only be used to compare simple values (enums, ranges or scalarsets). Rumur lets you compare any compatible values; that is, it also supports records and arrays. The semantics are equivalent to writing out a long form comparison of every one of the complex values’ members.
The operators & and | are used for logical AND and OR, respectively. Rumur allows && and || as synonyms for these. Rumur also supports a set of bitwise arithmetic operators, documented in bitwise-operators.rst.
CMurphi has a set of command-line options, and its generated verifier has another set of command-line options. Rumur has some similar command-line options, but its generated verifier has none at all. The intent with this design is to expose as much information to the C compiler as possible. In some cases this can make a significant difference by allowing your C compiler to more aggressively optimise during compilation.
The verifier can detect “deadlocks” in your state graph, where there are no transitions that make progress. CMurphi considers a deadlock to have occurred in any state that only has enabled transitions that lead back to itself. Rumur has two deadlock modes that can be selected with the --deadlock-detection command line option: “stuttering” and “stuck”. Stuttering, the default, matches CMurphi’s definition. Stuck uses a weaker definition that considers a deadlock to have occurred only when a state has no enabled transitions.
CMurphi requires the step in a quantifier expression to be a generation-time constant. I.e. in the code:
for i := l to u by s do
...
end;s must have a known constant value when the verifier is being generated. Rumur has no such restrictions. However steps that are 0 at generation-time are rejected and steps that turn out to be 0 or incrementing in the wrong direction at runtime will be raised as a runtime error by the verifier.
CMurphi considers an infinite loop to be a runtime error that the verifier should be capable of detecting and notifying the user about. It has an iteration bound (by default 1000), after which it will consider a loop to be non-terminating and will raise an error.
Rumur trusts the user not to write an infinite while loop. If you write an infinite loop, your verifier will run forever. You have been warned.
Rumur’s generated verifier attempts to imitate CMurphi’s verifier’s output to smooth the transition for users, but by default Rumur colourises its output using ANSI terminal sequences. This behaviour is controllable via command-line options.