h0nzzik/llvm-nts-partialorderreduction

Implements Partial Order Reduction on NTS formalism in order to ease LLVM model checking

llvm-nts-partialorderreduction's Issues

Conditions C0 and C2 are not checked

For condition C2, add some parametrization of POVisitor in order to allow user specify set of interesting global variables.

Use smallest (nonempty) ample

In "Static partial order reduction" by "R.P.Kurschan" is said"

Each process sets a global combinational flag to
true or false depending on its ampleness at a global state. From all the ample
processes at a state, a process with the least number of outgoing transitions is
chosen as the candidate for execution.
It sounds like an easy optimization.