Generate new input from the result of Z3
Store mappings before starting execution
Pack the simple usage of the FSM into a solve function
Add scheduler & analyzer and refactor some code