Tallulah, a Tool to Support the Axiomatic Approach to Causal-Consistent Reversibility

The axiomatic approach to causal-consistent reversibility allows one to prove relevant properties of concurrent reversible formalisms, such as causal consistency, causal safety and causal liveness, by checking a few simple axioms. The approach works on Labeled Transition Systems equipped with a notion of Independence (LTSIs). Even if the axioms are quite simple, verifying them on non-trivial LTSIs is time consuming and involves a few subtleties. We present Tallulah, a tool which allows one to automatically verify various axioms on concrete LTSIs, suggests how to patch the LTSI when some axiom does not hold, and colors the transitions to highlight when they belong to the same event.