search

ModelInference / synoptic

Inferring models of systems from observations of their behavior
Other
81 stars 25 forks source link

Add state-based model output #403

Closed ohmann closed 8 years ago

ohmann commented 8 years ago

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. Non-minimal state-based model

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 commented 8 years ago

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