Actually, what StateFlow does is different than Spec Explorer. In StateFlow you model a system with a graphic language, StateCharts. In Spec Explorer, you model a system with a full-fledged programming language, C#, which is significantly more expressive. We then generate a state machine from this C# model, just for the purpose of visualization for the user. So the state machine is not input, but output of the tool chain.