This repository contains TLA+ specifications for snapshot isolation along with analysis tools for processing model checker outputs and visualizing transaction conflict graphs. These specs were originally developed to explore ideas around alternate snapshot isolation definitions that are based around prevention of G-nonadjacent cycles, a special case of G2 anomalies that generalize SI beyond classic write-write conflict based implementations.
You can interactively explore a model of the spec here (4 transactions).
To check a model and generate a visualization of the counterexample and its serialization graph, you can run the check.sh script, which will output a visualization into the ccgraph.png file.
