Add state-based model output

[ohmann]

Convert Synoptic's internal event-based model to a state-based model for output, if requested. As a first step, this could be done only for JSON output where this feature is currently desired.

Some strategy should be employed during conversion to ensure no unnecessary states are created in the state-based model, since naive conversion strategies have the potential to create non-minimal state-based models. For example, the Perfume frontend currently takes the Perfume backend's (event-based) JSON output and leverages the naive strategy of simply pushing all node labels into the outgoing edges. Below is an example of a non-minimal model it produces.

Running this command allows Perfume to infer the same shopping cart model that Synoptic does:

./perfume.sh -c traces/abstract/shopping-cart-example/args-perfume.txt traces/abstract/shopping-cart-example/trace.txt

But using the same arguments in the Perfume frontend, the following non-minimal state-based model is produced. Both of the top two check-out.php edges should lead to the same state.

Issue #370 is related; it discusses the impact event logging strategies have on the correctness of an event-based model converted into a state-based model.

[ohmann]

Resolved in a basic way via #406. Models are currently not guaranteed to be minimal.